27 function |
27 function |
28 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
28 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
29 where |
29 where |
30 "decode' ds ZERO = (Void, [])" |
30 "decode' ds ZERO = (Void, [])" |
31 | "decode' ds ONE = (Void, ds)" |
31 | "decode' ds ONE = (Void, ds)" |
32 | "decode' ds (CHAR d) = (Char d, ds)" |
32 | "decode' ds (CH d) = (Char d, ds)" |
33 | "decode' [] (ALT r1 r2) = (Void, [])" |
33 | "decode' [] (ALT r1 r2) = (Void, [])" |
34 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
34 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
35 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
35 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
36 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
36 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
37 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
37 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
109 fun |
109 fun |
110 erase :: "arexp \<Rightarrow> rexp" |
110 erase :: "arexp \<Rightarrow> rexp" |
111 where |
111 where |
112 "erase AZERO = ZERO" |
112 "erase AZERO = ZERO" |
113 | "erase (AONE _) = ONE" |
113 | "erase (AONE _) = ONE" |
114 | "erase (ACHAR _ c) = CHAR c" |
114 | "erase (ACHAR _ c) = CH c" |
115 | "erase (AALTs _ []) = ZERO" |
115 | "erase (AALTs _ []) = ZERO" |
116 | "erase (AALTs _ [r]) = (erase r)" |
116 | "erase (AALTs _ [r]) = (erase r)" |
117 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
117 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
118 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
118 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
119 | "erase (ASTAR _ r) = STAR (erase r)" |
119 | "erase (ASTAR _ r) = STAR (erase r)" |
127 |
127 |
128 fun nonalt :: "arexp \<Rightarrow> bool" |
128 fun nonalt :: "arexp \<Rightarrow> bool" |
129 where |
129 where |
130 "nonalt (AALTs bs2 rs) = False" |
130 "nonalt (AALTs bs2 rs) = False" |
131 | "nonalt r = True" |
131 | "nonalt r = True" |
132 |
|
133 |
|
134 fun good :: "arexp \<Rightarrow> bool" where |
|
135 "good AZERO = False" |
|
136 | "good (AONE cs) = True" |
|
137 | "good (ACHAR cs c) = True" |
|
138 | "good (AALTs cs []) = False" |
|
139 | "good (AALTs cs [r]) = False" |
|
140 | "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')" |
|
141 | "good (ASEQ _ AZERO _) = False" |
|
142 | "good (ASEQ _ (AONE _) _) = False" |
|
143 | "good (ASEQ _ _ AZERO) = False" |
|
144 | "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)" |
|
145 | "good (ASTAR cs r) = True" |
|
146 |
|
147 |
132 |
148 |
133 |
149 |
134 |
150 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
135 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
151 "fuse bs AZERO = AZERO" |
136 "fuse bs AZERO = AZERO" |
163 |
148 |
164 |
149 |
165 fun intern :: "rexp \<Rightarrow> arexp" where |
150 fun intern :: "rexp \<Rightarrow> arexp" where |
166 "intern ZERO = AZERO" |
151 "intern ZERO = AZERO" |
167 | "intern ONE = AONE []" |
152 | "intern ONE = AONE []" |
168 | "intern (CHAR c) = ACHAR [] c" |
153 | "intern (CH c) = ACHAR [] c" |
169 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
154 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
170 (fuse [S] (intern r2))" |
155 (fuse [S] (intern r2))" |
171 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
156 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
172 | "intern (STAR r) = ASTAR [] (intern r)" |
157 | "intern (STAR r) = ASTAR [] (intern r)" |
173 |
158 |
1115 shows "bsimp_AALTs bs (flts [r]) = fuse bs r" |
1100 shows "bsimp_AALTs bs (flts [r]) = fuse bs r" |
1116 using assms |
1101 using assms |
1117 apply(case_tac r) |
1102 apply(case_tac r) |
1118 apply(simp_all) |
1103 apply(simp_all) |
1119 done |
1104 done |
|
1105 |
|
1106 fun nonalt :: "arexp \<Rightarrow> bool" |
|
1107 where |
|
1108 "nonalt (AALTs bs2 rs) = False" |
|
1109 | "nonalt r = True" |
|
1110 |
|
1111 |
|
1112 fun good :: "arexp \<Rightarrow> bool" where |
|
1113 "good AZERO = False" |
|
1114 | "good (AONE cs) = True" |
|
1115 | "good (ACHAR cs c) = True" |
|
1116 | "good (AALTs cs []) = False" |
|
1117 | "good (AALTs cs [r]) = False" |
|
1118 | "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')" |
|
1119 | "good (ASEQ _ AZERO _) = False" |
|
1120 | "good (ASEQ _ (AONE _) _) = False" |
|
1121 | "good (ASEQ _ _ AZERO) = False" |
|
1122 | "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)" |
|
1123 | "good (ASTAR cs r) = True" |
1120 |
1124 |
1121 lemma bbbbs: |
1125 lemma bbbbs: |
1122 assumes "good r" "r = AALTs bs1 rs" |
1126 assumes "good r" "r = AALTs bs1 rs" |
1123 shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)" |
1127 shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)" |
1124 using assms |
1128 using assms |