66 fun |
66 fun |
67 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
67 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
68 where |
68 where |
69 "der c (NULL) = NULL" |
69 "der c (NULL) = NULL" |
70 | "der c (EMPTY) = NULL" |
70 | "der c (EMPTY) = NULL" |
71 | "der c (CHAR c') = (if c=c' then EMPTY else NULL)" |
71 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)" |
72 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
72 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
73 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)" |
73 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)" |
74 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
74 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
75 |
75 |
76 fun |
76 fun |
77 derivative :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
77 derivative :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
78 where |
78 where |
79 "derivative [] r = r" |
79 "derivative [] r = r" |
80 | "derivative (c#s) r = derivative s (der c r)" |
80 | "derivative (c # s) r = derivative s (der c r)" |
81 |
81 |
82 fun |
82 fun |
83 matches :: "rexp \<Rightarrow> string \<Rightarrow> bool" |
83 matches :: "rexp \<Rightarrow> string \<Rightarrow> bool" |
84 where |
84 where |
85 "matches r s = nullable (derivative s r)" |
85 "matches r s = nullable (derivative s r)" |
90 lemma nullable_correctness: |
90 lemma nullable_correctness: |
91 shows "nullable r \<longleftrightarrow> [] \<in> L r" |
91 shows "nullable r \<longleftrightarrow> [] \<in> L r" |
92 by (induct r) (auto) |
92 by (induct r) (auto) |
93 |
93 |
94 lemma der_correctness: |
94 lemma der_correctness: |
95 shows "s \<in> L (der c r) \<longleftrightarrow> c#s \<in> L r" |
95 shows "s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r" |
96 proof (induct r arbitrary: s) |
96 proof (induct r arbitrary: s) |
97 case (SEQ r1 r2 s) |
97 case (SEQ r1 r2 s) |
98 have ih1: "\<And>s. s \<in> L (der c r1) \<longleftrightarrow> c#s \<in> L r1" by fact |
98 have ih1: "\<And>s. s \<in> L (der c r1) \<longleftrightarrow> c # s \<in> L r1" by fact |
99 have ih2: "\<And>s. s \<in> L (der c r2) \<longleftrightarrow> c#s \<in> L r2" by fact |
99 have ih2: "\<And>s. s \<in> L (der c r2) \<longleftrightarrow> c # s \<in> L r2" by fact |
100 show "s \<in> L (der c (SEQ r1 r2)) \<longleftrightarrow> c#s \<in> L (SEQ r1 r2)" |
100 show "s \<in> L (der c (SEQ r1 r2)) \<longleftrightarrow> c # s \<in> L (SEQ r1 r2)" |
101 using ih1 ih2 by (auto simp add: nullable_correctness Cons_eq_append_conv) |
101 using ih1 ih2 by (auto simp add: nullable_correctness Cons_eq_append_conv) |
102 next |
102 next |
103 case (STAR r s) |
103 case (STAR r s) |
104 have ih: "\<And>s. s \<in> L (der c r) \<longleftrightarrow> c#s \<in> L r" by fact |
104 have ih: "\<And>s. s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r" by fact |
105 show "s \<in> L (der c (STAR r)) \<longleftrightarrow> c#s \<in> L (STAR r)" |
105 show "s \<in> L (der c (STAR r)) \<longleftrightarrow> c # s \<in> L (STAR r)" |
106 proof |
106 proof |
107 assume "s \<in> L (der c (STAR r))" |
107 assume "s \<in> L (der c (STAR r))" |
108 then have "s \<in> L (der c r) ; L r\<star>" by simp |
108 then have "s \<in> L (der c r) ; L r\<star>" by simp |
109 then have "c#s \<in> L r ; (L r)\<star>" |
109 then have "c # s \<in> L r ; (L r)\<star>" |
110 by (auto simp add: ih Cons_eq_append_conv) |
110 by (auto simp add: ih Cons_eq_append_conv) |
111 then have "c#s \<in> (L r)\<star>" using lang_star_cases by auto |
111 then have "c # s \<in> (L r)\<star>" using lang_star_cases by auto |
112 then show "c#s \<in> L (STAR r)" by simp |
112 then show "c # s \<in> L (STAR r)" by simp |
113 next |
113 next |
114 assume "c#s \<in> L (STAR r)" |
114 assume "c # s \<in> L (STAR r)" |
115 then have "c#s \<in> (L r)\<star>" by simp |
115 then have "c # s \<in> (L r)\<star>" by simp |
116 then have "s \<in> L (der c r); (L r)\<star>" |
116 then have "s \<in> L (der c r); (L r)\<star>" |
117 by (induct x\<equiv>"c#s" rule: Star.induct) |
117 by (induct x\<equiv>"c # s" rule: Star.induct) |
118 (auto simp add: ih append_eq_Cons_conv) |
118 (auto simp add: ih append_eq_Cons_conv) |
119 then show "s \<in> L (der c (STAR r))" by simp |
119 then show "s \<in> L (der c (STAR r))" by simp |
120 qed |
120 qed |
121 qed (simp_all) |
121 qed (simp_all) |
122 |
122 |
139 |
139 |
140 function |
140 function |
141 match :: "rexp list \<Rightarrow> string \<Rightarrow> bool" |
141 match :: "rexp list \<Rightarrow> string \<Rightarrow> bool" |
142 where |
142 where |
143 "match [] [] = True" |
143 "match [] [] = True" |
144 | "match [] (c#s) = False" |
144 | "match [] (c # s) = False" |
145 | "match (NULL#rs) s = False" |
145 | "match (NULL # rs) s = False" |
146 | "match (EMPTY#rs) s = match rs s" |
146 | "match (EMPTY # rs) s = match rs s" |
147 | "match (CHAR c#rs) [] = False" |
147 | "match (CHAR c # rs) [] = False" |
148 | "match (CHAR c#rs) (d#s) = (if c = d then match rs s else False)" |
148 | "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)" |
149 | "match (ALT r1 r2#rs) s = (match (r1#rs) s \<or> match (r2#rs) s)" |
149 | "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)" |
150 | "match (SEQ r1 r2#rs) s = match (r1#r2#rs) s" |
150 | "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s" |
151 | "match (STAR r#rs) s = (match rs s \<or> match (r#(STAR r)#rs) s)" |
151 | "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)" |
152 apply(pat_completeness) |
152 apply(pat_completeness) |
153 apply(auto) |
153 apply(auto) |
154 done |
154 done |
155 |
155 |
156 end |
156 end |