|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 section "Regular expressions" |
|
4 |
|
5 theory Regular_Exp |
|
6 imports Regular_Set |
|
7 begin |
|
8 |
|
9 datatype (atoms: 'a) rexp = |
|
10 is_Zero: Zero | |
|
11 is_One: One | |
|
12 Atom 'a | |
|
13 Plus "('a rexp)" "('a rexp)" | |
|
14 Times "('a rexp)" "('a rexp)" | |
|
15 Star "('a rexp)" |
|
16 |
|
17 primrec lang :: "'a rexp => 'a lang" where |
|
18 "lang Zero = {}" | |
|
19 "lang One = {[]}" | |
|
20 "lang (Atom a) = {[a]}" | |
|
21 "lang (Plus r s) = (lang r) Un (lang s)" | |
|
22 "lang (Times r s) = conc (lang r) (lang s)" | |
|
23 "lang (Star r) = star(lang r)" |
|
24 |
|
25 primrec nullable :: "'a rexp \<Rightarrow> bool" where |
|
26 "nullable Zero = False" | |
|
27 "nullable One = True" | |
|
28 "nullable (Atom c) = False" | |
|
29 "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" | |
|
30 "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" | |
|
31 "nullable (Star r) = True" |
|
32 |
|
33 lemma nullable_iff: "nullable r \<longleftrightarrow> [] \<in> lang r" |
|
34 by (induct r) (auto simp add: conc_def split: if_splits) |
|
35 |
|
36 text{* Composition on rhs usually complicates matters: *} |
|
37 lemma map_map_rexp: |
|
38 "map_rexp f (map_rexp g r) = map_rexp (\<lambda>r. f (g r)) r" |
|
39 unfolding rexp.map_comp o_def .. |
|
40 |
|
41 lemma map_rexp_ident[simp]: "map_rexp (\<lambda>x. x) = (\<lambda>r. r)" |
|
42 unfolding id_def[symmetric] fun_eq_iff rexp.map_id id_apply by (intro allI refl) |
|
43 |
|
44 lemma atoms_lang: "w : lang r \<Longrightarrow> set w \<subseteq> atoms r" |
|
45 proof(induction r arbitrary: w) |
|
46 case Times thus ?case by fastforce |
|
47 next |
|
48 case Star thus ?case by (fastforce simp add: star_conv_concat) |
|
49 qed auto |
|
50 |
|
51 lemma lang_eq_ext: "(lang r = lang s) = |
|
52 (\<forall>w \<in> lists(atoms r \<union> atoms s). w \<in> lang r \<longleftrightarrow> w \<in> lang s)" |
|
53 by (auto simp: atoms_lang[unfolded subset_iff]) |
|
54 |
|
55 lemma lang_eq_ext_Nil_fold_Deriv: |
|
56 fixes r s |
|
57 defines "\<BB> \<equiv> {(fold Deriv w (lang r), fold Deriv w (lang s))| w. w\<in>lists (atoms r \<union> atoms s)}" |
|
58 shows "lang r = lang s \<longleftrightarrow> (\<forall>(K, L) \<in> \<BB>. [] \<in> K \<longleftrightarrow> [] \<in> L)" |
|
59 unfolding lang_eq_ext \<BB>_def by (subst (1 2) in_fold_Deriv[of "[]", simplified, symmetric]) auto |
|
60 |
|
61 |
|
62 subsection {* Term ordering *} |
|
63 |
|
64 instantiation rexp :: (order) "{order}" |
|
65 begin |
|
66 |
|
67 fun le_rexp :: "('a::order) rexp \<Rightarrow> ('a::order) rexp \<Rightarrow> bool" |
|
68 where |
|
69 "le_rexp Zero _ = True" |
|
70 | "le_rexp _ Zero = False" |
|
71 | "le_rexp One _ = True" |
|
72 | "le_rexp _ One = False" |
|
73 | "le_rexp (Atom a) (Atom b) = (a <= b)" |
|
74 | "le_rexp (Atom _) _ = True" |
|
75 | "le_rexp _ (Atom _) = False" |
|
76 | "le_rexp (Star r) (Star s) = le_rexp r s" |
|
77 | "le_rexp (Star _) _ = True" |
|
78 | "le_rexp _ (Star _) = False" |
|
79 | "le_rexp (Plus r r') (Plus s s') = |
|
80 (if r = s then le_rexp r' s' else le_rexp r s)" |
|
81 | "le_rexp (Plus _ _) _ = True" |
|
82 | "le_rexp _ (Plus _ _) = False" |
|
83 | "le_rexp (Times r r') (Times s s') = |
|
84 (if r = s then le_rexp r' s' else le_rexp r s)" |
|
85 |
|
86 (* The class instance stuff is by Dmitriy Traytel *) |
|
87 |
|
88 definition less_eq_rexp where "r \<le> s \<equiv> le_rexp r s" |
|
89 definition less_rexp where "r < s \<equiv> le_rexp r s \<and> r \<noteq> s" |
|
90 |
|
91 lemma le_rexp_Zero: "le_rexp r Zero \<Longrightarrow> r = Zero" |
|
92 by (induction r) auto |
|
93 |
|
94 lemma le_rexp_refl: "le_rexp r r" |
|
95 by (induction r) auto |
|
96 |
|
97 lemma le_rexp_antisym: "\<lbrakk>le_rexp r s; le_rexp s r\<rbrakk> \<Longrightarrow> r = s" |
|
98 by (induction r s rule: le_rexp.induct) (auto dest: le_rexp_Zero) |
|
99 |
|
100 lemma le_rexp_trans: "\<lbrakk>le_rexp r s; le_rexp s t\<rbrakk> \<Longrightarrow> le_rexp r t" |
|
101 proof (induction r s arbitrary: t rule: le_rexp.induct) |
|
102 fix v t assume "le_rexp (Atom v) t" thus "le_rexp One t" by (cases t) auto |
|
103 next |
|
104 fix s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp One t" by (cases t) auto |
|
105 next |
|
106 fix s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp One t" by (cases t) auto |
|
107 next |
|
108 fix s t assume "le_rexp (Star s) t" thus "le_rexp One t" by (cases t) auto |
|
109 next |
|
110 fix v u t assume "le_rexp (Atom v) (Atom u)" "le_rexp (Atom u) t" |
|
111 thus "le_rexp (Atom v) t" by (cases t) auto |
|
112 next |
|
113 fix v s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto |
|
114 next |
|
115 fix v s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto |
|
116 next |
|
117 fix v s t assume "le_rexp (Star s) t" thus "le_rexp (Atom v) t" by (cases t) auto |
|
118 next |
|
119 fix r s t |
|
120 assume IH: "\<And>t. le_rexp r s \<Longrightarrow> le_rexp s t \<Longrightarrow> le_rexp r t" |
|
121 and "le_rexp (Star r) (Star s)" "le_rexp (Star s) t" |
|
122 thus "le_rexp (Star r) t" by (cases t) auto |
|
123 next |
|
124 fix r s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto |
|
125 next |
|
126 fix r s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto |
|
127 next |
|
128 fix r1 r2 s1 s2 t |
|
129 assume "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t" |
|
130 "\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> le_rexp r1 t" |
|
131 "le_rexp (Plus r1 r2) (Plus s1 s2)" "le_rexp (Plus s1 s2) t" |
|
132 thus "le_rexp (Plus r1 r2) t" by (cases t) (auto split: split_if_asm intro: le_rexp_antisym) |
|
133 next |
|
134 fix r1 r2 s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Plus r1 r2) t" by (cases t) auto |
|
135 next |
|
136 fix r1 r2 s1 s2 t |
|
137 assume "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t" |
|
138 "\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> le_rexp r1 t" |
|
139 "le_rexp (Times r1 r2) (Times s1 s2)" "le_rexp (Times s1 s2) t" |
|
140 thus "le_rexp (Times r1 r2) t" by (cases t) (auto split: split_if_asm intro: le_rexp_antisym) |
|
141 qed auto |
|
142 |
|
143 instance proof |
|
144 qed (auto simp add: less_eq_rexp_def less_rexp_def |
|
145 intro: le_rexp_refl le_rexp_antisym le_rexp_trans) |
|
146 |
|
147 end |
|
148 |
|
149 instantiation rexp :: (linorder) "{linorder}" |
|
150 begin |
|
151 |
|
152 lemma le_rexp_total: "le_rexp (r :: 'a :: linorder rexp) s \<or> le_rexp s r" |
|
153 by (induction r s rule: le_rexp.induct) auto |
|
154 |
|
155 instance proof |
|
156 qed (unfold less_eq_rexp_def less_rexp_def, rule le_rexp_total) |
|
157 |
|
158 end |
|
159 |
|
160 end |