equal
deleted
inserted
replaced
51 where |
51 where |
52 alpha_gen[simp del]: |
52 alpha_gen[simp del]: |
53 "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)" |
53 "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)" |
54 |
54 |
55 notation |
55 notation |
56 alpha_gen ("_ \<approx>gen _ _ _ _") |
56 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
57 |
57 |
58 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
58 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
59 by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps) |
59 by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps) |
60 |
60 |
61 lemma alpha_gen_refl: |
61 lemma alpha_gen_refl: |
69 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
69 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
70 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 |
71 |
72 lemma alpha_gen_atom_sym: |
72 lemma alpha_gen_atom_sym: |
73 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
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> |
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)" |
75 \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)" |
76 apply(erule exE) |
76 apply(erule exE) |
77 apply(rule_tac x="- pi" in exI) |
77 apply(rule_tac x="- pi" in exI) |
78 apply(simp add: alpha_gen.simps) |
78 apply(simp add: alpha_gen.simps) |
79 apply(erule conjE)+ |
79 apply(erule conjE)+ |
95 apply(blast) |
95 apply(blast) |
96 done |
96 done |
97 |
97 |
98 lemma alpha_gen_atom_trans: |
98 lemma alpha_gen_atom_trans: |
99 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
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); |
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> |
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)" |
102 \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)" |
103 apply(simp add: alpha_gen.simps) |
103 apply(simp add: alpha_gen.simps) |
104 apply(erule conjE)+ |
104 apply(erule conjE)+ |
105 apply(erule exE)+ |
105 apply(erule exE)+ |
129 apply(clarsimp) |
129 apply(clarsimp) |
130 done |
130 done |
131 |
131 |
132 lemma alpha_gen_atom_eqvt: |
132 lemma alpha_gen_atom_eqvt: |
133 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
133 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
134 and b: "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s)" |
134 and b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)" |
135 shows "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)" |
135 shows "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)" |
136 using b apply - |
136 using b apply - |
137 apply(erule exE) |
137 apply(erule exE) |
138 apply(rule_tac x="pi \<bullet> pia" in exI) |
138 apply(rule_tac x="pi \<bullet> pia" in exI) |
139 apply(simp add: alpha_gen.simps) |
139 apply(simp add: alpha_gen.simps) |