equal
deleted
inserted
replaced
1 theory Classical |
1 theory Classical |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
|
4 |
4 |
5 |
5 (* example from Urban's PhD *) |
6 (* example from Urban's PhD *) |
6 |
7 |
7 atom_decl name |
8 atom_decl name |
8 atom_decl coname |
9 atom_decl coname |
175 then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)" |
176 then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)" |
176 by (simp add: permute_bool_def) |
177 by (simp add: permute_bool_def) |
177 then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c" |
178 then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c" |
178 apply(simp add: fresh_star_eqvt set_eqvt) |
179 apply(simp add: fresh_star_eqvt set_eqvt) |
179 sorry (* perm? *) |
180 sorry (* perm? *) |
180 then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 apply (simp add: inter_eqvt) |
181 then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 |
|
182 apply (simp add: inter_eqvt) |
|
183 sorry |
181 (* rest similar reversing it other way around... *) |
184 (* rest similar reversing it other way around... *) |
182 show ?thesis sorry |
185 show ?thesis sorry |
183 qed |
186 qed |
184 |
187 |
185 |
188 |
474 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
477 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
475 apply(blast) |
478 apply(blast) |
476 apply(blast) |
479 apply(blast) |
477 done |
480 done |
478 |
481 |
|
482 |
|
483 |
479 end |
484 end |
480 |
485 |
481 |
486 |
482 |
487 |