[isabelle] Miscellany in Language Theory

[José Manuel Rodriguez Caballero]

Dear All,
Last week, after a short talk about my research, some experts in Isabelle
suggested me to make my developments in the theory of formal languages more
algorithmic, because my original approach was non-constructive (a bad habit
from classical mathematics). After reading the tutorial "Defining Recursive
Functions in Isabelle/HOL" I reformulated my definitions and I proved some
classical theorems.

For me it was a nice exercise in order to remember the theory of formal
languages. Nevertheless, I do not know if my results are already in some
library in Isabelle/HOL. If this is the case, I would prefer to use the
library. This constructive approach will allow me to do both computations
and proof in Isabelle. Before, I did the computations in SAGE.

My algorithmic definition of Dyck paths:
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-language-theory/blob/master/DyckPathsDef.thy

The classical results that I proved (exercises in any course of
introduction to formal languages):
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-language-theory/blob/master/DyckPathsCharacterization1.thy

Thank you for the previous suggestions. Any new suggestion or comment is
welcome.

Sincerely yours,
José Manuel Rodriguez Caballero

[Tobias Nipkow]

A small hint on style: just write "!x : set xs. P x" instead of defining a
recursive function that traverses xs to check if all elements satisfy P. Both
versions are equally executable but the former is more compact and proof-friendly.

Tobias

Post by José Manuel Rodriguez Caballero
Dear All,
Last week, after a short talk about my research, some experts in Isabelle
suggested me to make my developments in the theory of formal languages more
algorithmic, because my original approach was non-constructive (a bad habit
from classical mathematics). After reading the tutorial "Defining Recursive
Functions in Isabelle/HOL" I reformulated my definitions and I proved some
classical theorems.
For me it was a nice exercise in order to remember the theory of formal
languages. Nevertheless, I do not know if my results are already in some
library in Isabelle/HOL. If this is the case, I would prefer to use the
library. This constructive approach will allow me to do both computations
and proof in Isabelle. Before, I did the computations in SAGE.
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-language-theory/blob/master/DyckPathsDef.thy
The classical results that I proved (exercises in any course of
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-language-theory/blob/master/DyckPathsCharacterization1.thy
Thank you for the previous suggestions. Any new suggestion or comment is
welcome.
Sincerely yours,
José Manuel Rodriguez Caballero