equal
deleted
inserted
replaced
112 apply(drule_tac pi="pia" in a) |
112 apply(drule_tac pi="pia" in a) |
113 apply(simp) |
113 apply(simp) |
114 done |
114 done |
115 |
115 |
116 lemma alpha_gen_compose_eqvt: |
116 lemma alpha_gen_compose_eqvt: |
117 assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)" |
117 fixes pia |
|
118 assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)" |
118 and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)" |
119 and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)" |
119 and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
120 and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
120 shows "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s)" |
121 shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)" |
121 using b |
122 using b |
122 apply - |
123 apply - |
123 apply(erule exE) |
|
124 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
125 apply(simp add: alpha_gen.simps) |
124 apply(simp add: alpha_gen.simps) |
126 apply(erule conjE)+ |
125 apply(erule conjE)+ |
127 apply(rule conjI) |
126 apply(rule conjI) |
128 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
127 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
129 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
128 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
417 apply(simp add: fresh_star_def fresh_def) |
416 apply(simp add: fresh_star_def fresh_def) |
418 apply(blast) |
417 apply(blast) |
419 apply(simp add: supp_swap) |
418 apply(simp add: supp_swap) |
420 done |
419 done |
421 |
420 |
|
421 (* |
422 thm supp_perm |
422 thm supp_perm |
423 |
423 |
424 lemma perm_induct_test: |
424 lemma perm_induct_test: |
425 fixes P :: "perm => bool" |
425 fixes P :: "perm => bool" |
426 assumes zero: "P 0" |
426 assumes zero: "P 0" |
500 using a |
500 using a |
501 apply(case_tac "a = b") |
501 apply(case_tac "a = b") |
502 apply(simp) |
502 apply(simp) |
503 oops |
503 oops |
504 |
504 |
505 |
505 *) |
506 end |
506 end |
507 |
507 |