35 fun simp_SEQ where |
35 fun simp_SEQ where |
36 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
36 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
37 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
37 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
39 |
39 |
40 lemma simp_SEQ_simps: |
40 lemma simp_SEQ_simps[simp]: |
41 "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) |
41 "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) |
42 else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) |
42 else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) |
43 else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))" |
43 else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))" |
44 apply(auto) |
44 by (induct p1 p2 rule: simp_SEQ.induct) (auto) |
45 apply(case_tac p1) |
45 |
46 apply(case_tac p2) |
46 lemma simp_ALT_simps[simp]: |
47 apply(simp) |
|
48 apply(case_tac p1) |
|
49 apply(case_tac p2) |
|
50 apply(simp) |
|
51 apply(case_tac a) |
|
52 apply(simp_all) |
|
53 apply(case_tac p1) |
|
54 apply(case_tac p2) |
|
55 apply(simp) |
|
56 apply(case_tac p1) |
|
57 apply(case_tac p2) |
|
58 apply(simp) |
|
59 apply(case_tac a) |
|
60 apply(simp_all) |
|
61 apply(case_tac aa) |
|
62 apply(simp_all) |
|
63 apply(auto) |
|
64 apply(case_tac aa) |
|
65 apply(simp_all) |
|
66 apply(case_tac aa) |
|
67 apply(simp_all) |
|
68 apply(case_tac aa) |
|
69 apply(simp_all) |
|
70 apply(case_tac aa) |
|
71 apply(simp_all) |
|
72 done |
|
73 |
|
74 lemma simp_ALT_simps: |
|
75 "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) |
47 "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) |
76 else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) |
48 else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) |
77 else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))" |
49 else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))" |
78 apply(auto) |
50 by (induct p1 p2 rule: simp_ALT.induct) (auto) |
79 apply(case_tac p1) |
|
80 apply(case_tac p2) |
|
81 apply(simp) |
|
82 apply(case_tac p1) |
|
83 apply(case_tac p2) |
|
84 apply(simp) |
|
85 apply(case_tac a) |
|
86 apply(simp_all) |
|
87 apply(case_tac p1) |
|
88 apply(case_tac p2) |
|
89 apply(simp) |
|
90 apply(case_tac p1) |
|
91 apply(case_tac p2) |
|
92 apply(simp) |
|
93 apply(case_tac a) |
|
94 apply(simp_all) |
|
95 apply(case_tac aa) |
|
96 apply(simp_all) |
|
97 apply(auto) |
|
98 apply(case_tac aa) |
|
99 apply(simp_all) |
|
100 apply(case_tac aa) |
|
101 apply(simp_all) |
|
102 apply(case_tac aa) |
|
103 apply(simp_all) |
|
104 apply(case_tac aa) |
|
105 apply(simp_all) |
|
106 done |
|
107 |
|
108 |
51 |
109 fun |
52 fun |
110 simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)" |
53 simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)" |
111 where |
54 where |
112 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
55 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
124 |
67 |
125 |
68 |
126 lemma L_fst_simp: |
69 lemma L_fst_simp: |
127 shows "L(r) = L(fst (simp r))" |
70 shows "L(r) = L(fst (simp r))" |
128 using assms |
71 using assms |
129 apply(induct r rule: rexp.induct) |
72 by (induct r) (auto) |
130 apply(auto simp add: simp_SEQ_simps simp_ALT_simps) |
73 |
131 done |
|
132 |
74 |
133 lemma |
75 lemma |
134 shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))" |
76 shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))" |
135 using assms |
77 using assms |
136 apply(induct r arbitrary: v rule: simp.induct) |
78 apply(induct r arbitrary: v rule: simp.induct) |
137 apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros) |
79 apply(auto intro: Prf.intros) |
138 using Prf_elims(3) apply blast |
80 using Prf_elims(3) apply blast |
139 apply(erule Prf_elims) |
81 apply(erule Prf_elims) |
140 apply(simp) |
82 apply(simp) |
141 apply(clarify) |
83 apply(clarify) |
142 apply(blast) |
84 apply(blast) |
208 lemma Posix_simp_nullable: |
150 lemma Posix_simp_nullable: |
209 assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v" |
151 assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v" |
210 shows "((snd (simp r)) v) = mkeps r" |
152 shows "((snd (simp r)) v) = mkeps r" |
211 using assms |
153 using assms |
212 apply(induct r arbitrary: v) |
154 apply(induct r arbitrary: v) |
213 apply(auto simp add: simp_SEQ_simps simp_ALT_simps) |
155 apply(auto) |
214 apply(erule Posix_elims) |
156 apply(erule Posix_elims) |
215 apply(simp) |
157 apply(simp) |
216 apply(erule Posix_elims) |
158 apply(erule Posix_elims) |
217 apply(clarify) |
159 apply(clarify) |
218 using Posix.intros(1) apply blast |
160 using Posix.intros(1) apply blast |
252 lemma Posix_simp: |
194 lemma Posix_simp: |
253 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
195 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
254 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
196 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
255 using assms |
197 using assms |
256 apply(induct r arbitrary: s v rule: rexp.induct) |
198 apply(induct r arbitrary: s v rule: rexp.induct) |
257 apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps) |
199 apply(auto split: if_splits) |
258 prefer 3 |
200 prefer 3 |
259 apply(erule Posix_elims) |
201 apply(erule Posix_elims) |
260 apply(clarify) |
202 apply(clarify) |
261 apply(simp) |
203 apply(simp) |
262 apply(rule Posix.intros) |
204 apply(rule Posix.intros) |
309 |
251 |
310 lemma slexer_correctness: |
252 lemma slexer_correctness: |
311 shows "slexer r s = lexer r s" |
253 shows "slexer r s = lexer r s" |
312 apply(induct s arbitrary: r) |
254 apply(induct s arbitrary: r) |
313 apply(simp) |
255 apply(simp) |
314 apply(simp) |
|
315 apply(auto split: option.split prod.split) |
256 apply(auto split: option.split prod.split) |
316 apply (metis L_fst_simp fst_conv lexer_correct_None) |
257 apply (metis L_fst_simp fst_conv lexer_correct_None) |
317 using L_fst_simp lexer_correct_None apply fastforce |
258 using L_fst_simp lexer_correct_None apply fastforce |
318 by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv) |
259 by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv) |
319 |
260 |