equal
deleted
inserted
replaced
1 theory Myhill_2 |
1 theory Myhill_2 |
2 imports Myhill_1 |
2 imports Myhill_1 List_Prefix Prefix_subtract |
3 begin |
3 begin |
4 |
4 |
5 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *} |
5 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *} |
6 |
6 |
7 subsection {* The scheme*} |
7 subsection {* The scheme*} |
8 |
8 |
9 text {* |
9 text {* |
10 The following convenient notation @{text "x \<approx>Lang y"} means: |
10 The following convenient notation @{text "x \<approx>A y"} means: |
11 string @{text "x"} and @{text "y"} are equivalent with respect to |
11 string @{text "x"} and @{text "y"} are equivalent with respect to |
12 language @{text "Lang"}. |
12 language @{text "A"}. |
13 *} |
13 *} |
14 |
14 |
15 definition |
15 definition |
16 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
16 str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _") |
17 where |
17 where |
18 "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)" |
18 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)" |
19 |
19 |
20 text {* |
20 text {* |
21 The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions. |
21 The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions. |
22 While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward, |
22 While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward, |
23 the inductive cases are rather involved. What we have when starting to prove these inductive caes is that |
23 the inductive cases are rather involved. What we have when starting to prove these inductive caes is that |