equal
deleted
inserted
replaced
73 apply(simp add: fresh_star_permute_iff) |
73 apply(simp add: fresh_star_permute_iff) |
74 apply(clarsimp) |
74 apply(clarsimp) |
75 done |
75 done |
76 |
76 |
77 lemma alpha_gen_compose_sym: |
77 lemma alpha_gen_compose_sym: |
78 assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
78 fixes pi |
|
79 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
79 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
80 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
80 shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)" |
81 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
81 using b apply - |
82 using b apply - |
82 apply(erule exE) |
|
83 apply(rule_tac x="- pi" in exI) |
|
84 apply(simp add: alpha_gen.simps) |
83 apply(simp add: alpha_gen.simps) |
85 apply(erule conjE)+ |
84 apply(erule conjE)+ |
86 apply(rule conjI) |
85 apply(rule conjI) |
87 apply(simp add: fresh_star_def fresh_minus_perm) |
86 apply(simp add: fresh_star_def fresh_minus_perm) |
88 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
87 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
90 apply(rule a) |
89 apply(rule a) |
91 apply assumption |
90 apply assumption |
92 done |
91 done |
93 |
92 |
94 lemma alpha_gen_compose_trans: |
93 lemma alpha_gen_compose_trans: |
95 assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
94 fixes pi pia |
96 and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)" |
95 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
96 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
97 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
97 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
98 shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)" |
98 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
99 using b c apply - |
99 using b c apply - |
100 apply(simp add: alpha_gen.simps) |
100 apply(simp add: alpha_gen.simps) |
101 apply(erule conjE)+ |
101 apply(erule conjE)+ |
102 apply(erule exE)+ |
|
103 apply(erule conjE)+ |
|
104 apply(rule_tac x="pia + pi" in exI) |
|
105 apply(simp add: fresh_star_plus) |
102 apply(simp add: fresh_star_plus) |
106 apply(drule_tac x="- pia \<bullet> sa" in spec) |
103 apply(drule_tac x="- pia \<bullet> sa" in spec) |
107 apply(drule mp) |
104 apply(drule mp) |
108 apply(rotate_tac 4) |
105 apply(rotate_tac 4) |
109 apply(drule_tac pi="- pia" in a) |
106 apply(drule_tac pi="- pia" in a) |
112 apply(drule_tac pi="pia" in a) |
109 apply(drule_tac pi="pia" in a) |
113 apply(simp) |
110 apply(simp) |
114 done |
111 done |
115 |
112 |
116 lemma alpha_gen_compose_eqvt: |
113 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)" |
114 fixes pia |
|
115 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)" |
116 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)" |
117 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)" |
118 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 |
119 using b |
122 apply - |
120 apply - |
123 apply(erule exE) |
|
124 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
125 apply(simp add: alpha_gen.simps) |
121 apply(simp add: alpha_gen.simps) |
126 apply(erule conjE)+ |
122 apply(erule conjE)+ |
127 apply(rule conjI) |
123 apply(rule conjI) |
128 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
124 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]) |
125 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
349 "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
345 "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
350 |
346 |
351 notation |
347 notation |
352 alpha1 ("_ \<approx>abs1 _") |
348 alpha1 ("_ \<approx>abs1 _") |
353 |
349 |
|
350 thm swap_set_not_in |
|
351 |
354 lemma qq: |
352 lemma qq: |
355 fixes S::"atom set" |
353 fixes S::"atom set" |
356 assumes a: "supp p \<inter> S = {}" |
354 assumes a: "supp p \<inter> S = {}" |
357 shows "p \<bullet> S = S" |
355 shows "p \<bullet> S = S" |
358 using a |
356 using a |
415 apply(simp add: fresh_star_def fresh_def) |
413 apply(simp add: fresh_star_def fresh_def) |
416 apply(blast) |
414 apply(blast) |
417 apply(simp add: supp_swap) |
415 apply(simp add: supp_swap) |
418 done |
416 done |
419 |
417 |
|
418 (* |
420 thm supp_perm |
419 thm supp_perm |
421 |
420 |
422 lemma perm_induct_test: |
421 lemma perm_induct_test: |
423 fixes P :: "perm => bool" |
422 fixes P :: "perm => bool" |
424 assumes zero: "P 0" |
423 assumes zero: "P 0" |
498 using a |
497 using a |
499 apply(case_tac "a = b") |
498 apply(case_tac "a = b") |
500 apply(simp) |
499 apply(simp) |
501 oops |
500 oops |
502 |
501 |
503 fun |
502 *) |
504 distinct_perms |
|
505 where |
|
506 "distinct_perms [] = True" |
|
507 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)" |
|
508 |
|
509 |
|
510 |
|
511 |
|
512 |
|
513 end |
503 end |
514 |
504 |