6 lemma in_permute_iff: |
6 lemma in_permute_iff: |
7 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
7 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
8 apply(unfold mem_def permute_fun_def)[1] |
8 apply(unfold mem_def permute_fun_def)[1] |
9 apply(simp add: permute_bool_def) |
9 apply(simp add: permute_bool_def) |
10 done |
10 done |
|
11 |
|
12 lemma fresh_plus: |
|
13 fixes p q::perm |
|
14 shows "\<lbrakk>a \<sharp> p; a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)" |
|
15 unfolding fresh_def |
|
16 using supp_plus_perm |
|
17 by(auto) |
|
18 |
|
19 lemma fresh_star_plus: |
|
20 fixes p q::perm |
|
21 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
|
22 unfolding fresh_star_def |
|
23 by (simp add: fresh_plus) |
|
24 |
11 |
25 |
12 lemma fresh_star_permute_iff: |
26 lemma fresh_star_permute_iff: |
13 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
27 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
14 apply(simp add: fresh_star_def) |
28 apply(simp add: fresh_star_def) |
15 apply(auto) |
29 apply(auto) |
46 lemma alpha_gen_sym: |
66 lemma alpha_gen_sym: |
47 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
67 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
48 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
68 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
49 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
69 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
50 using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
70 using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
|
71 |
|
72 lemma alpha_gen_atom_sym: |
|
73 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
74 shows "\<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R x2 x1 f pi ({atom b}, s) \<Longrightarrow> |
|
75 \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)" |
|
76 apply(erule exE) |
|
77 apply(rule_tac x="- pi" in exI) |
|
78 apply(simp add: alpha_gen.simps) |
|
79 apply(erule conjE)+ |
|
80 apply(rule conjI) |
|
81 apply(simp add: fresh_star_def fresh_minus_perm) |
|
82 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
83 apply simp |
|
84 apply(rule a) |
|
85 apply assumption |
|
86 done |
51 |
87 |
52 lemma alpha_gen_trans: |
88 lemma alpha_gen_trans: |
53 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
89 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
54 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
90 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
55 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
91 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
56 shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)" |
92 shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)" |
57 using a b c using supp_plus_perm |
93 using a b c using supp_plus_perm |
58 apply(simp add: alpha_gen fresh_star_def fresh_def) |
94 apply(simp add: alpha_gen fresh_star_def fresh_def) |
59 apply(blast) |
95 apply(blast) |
|
96 done |
|
97 |
|
98 lemma alpha_gen_atom_trans: |
|
99 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
100 shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x) f pi ({atom aa}, ta); |
|
101 \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk> |
|
102 \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)" |
|
103 apply(simp add: alpha_gen.simps) |
|
104 apply(erule conjE)+ |
|
105 apply(erule exE)+ |
|
106 apply(erule conjE)+ |
|
107 apply(rule_tac x="pia + pi" in exI) |
|
108 apply(simp add: fresh_star_plus) |
|
109 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
110 apply(drule mp) |
|
111 apply(rotate_tac 4) |
|
112 apply(drule_tac pi="- pia" in a) |
|
113 apply(simp) |
|
114 apply(rotate_tac 6) |
|
115 apply(drule_tac pi="pia" in a) |
|
116 apply(simp) |
60 done |
117 done |
61 |
118 |
62 lemma alpha_gen_eqvt: |
119 lemma alpha_gen_eqvt: |
63 assumes a: "(bs, x) \<approx>gen R f q (cs, y)" |
120 assumes a: "(bs, x) \<approx>gen R f q (cs, y)" |
64 and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
121 and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |