equal
deleted
inserted
replaced
1188 apply (simp_all add: alpha_gen fresh_star_def) |
1188 apply (simp_all add: alpha_gen fresh_star_def) |
1189 apply (rule a1) |
1189 apply (rule a1) |
1190 apply (rule refl) |
1190 apply (rule refl) |
1191 done |
1191 done |
1192 |
1192 |
|
1193 |
|
1194 |
|
1195 |
|
1196 |
|
1197 atom_decl name2 |
|
1198 |
1193 datatype rfoo8 = |
1199 datatype rfoo8 = |
1194 Foo0 "name" |
1200 Foo0 "name" |
1195 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo" |
1201 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo" |
1196 and rbar8 = |
1202 and rbar8 = |
1197 Bar0 "name" |
1203 Bar0 "name2" |
1198 | Bar1 "name" "name" "rbar8" --"bind second name in b" |
1204 | Bar1 "name" "name2" "rbar8" --"bind second name in b" |
1199 |
1205 |
1200 primrec |
1206 primrec |
1201 rbv8 |
1207 rbv8 |
1202 where |
1208 where |
1203 "rbv8 (Bar0 x) = {}" |
1209 "rbv8 (Bar0 x) = {}" |
1240 lemma "(alpha8b ===> op =) rbv8 rbv8" |
1246 lemma "(alpha8b ===> op =) rbv8 rbv8" |
1241 apply simp apply clarify |
1247 apply simp apply clarify |
1242 apply (erule alpha8f_alpha8b.inducts(2)) |
1248 apply (erule alpha8f_alpha8b.inducts(2)) |
1243 apply (simp_all) |
1249 apply (simp_all) |
1244 done |
1250 done |
1245 |
|
1246 lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8" |
1251 lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8" |
1247 apply simp apply clarify |
1252 apply simp apply clarify |
1248 apply (erule alpha8f_alpha8b.inducts(2)) |
1253 apply (erule alpha8f_alpha8b.inducts(2)) |
1249 apply (simp_all add:alpha_gen) |
1254 apply (simp_all add: alpha_gen) |
1250 done |
1255 done |
1251 |
1256 |
1252 lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8" |
1257 lemma "(c :: name2) \<noteq> b \<Longrightarrow> (atom (a :: name)) \<noteq> (atom b) \<Longrightarrow> \<not> (alpha8f ===> op =) rfv_foo8 rfv_foo8" |
1253 apply simp apply clarify |
1258 apply (simp_all) |
1254 apply (erule alpha8f_alpha8b.inducts(1)) |
1259 apply (rule_tac x="Foo1 (Bar1 a c (Bar0 c)) (Foo0 a)" in exI) |
1255 apply (simp_all add:alpha_gen) |
1260 apply (rule_tac x="Foo1 (Bar1 a c (Bar0 b)) (Foo0 a)" in exI) |
1256 apply (clarify) |
1261 apply (rule conjI) |
1257 sorry (* ??? *) |
1262 apply (rule a3) |
1258 |
1263 apply (rule_tac x="0 :: perm" in exI) |
1259 |
1264 apply (simp add: alpha_gen fresh_star_def) |
|
1265 apply (rule a1) |
|
1266 apply (rule refl) |
|
1267 apply simp |
|
1268 done |
1260 |
1269 |
1261 |
1270 |
1262 |
1271 |
1263 |
1272 |
1264 text {* type schemes *} |
1273 text {* type schemes *} |