31 thm trm_assn.supp |
29 thm trm_assn.supp |
32 thm trm_assn.fresh |
30 thm trm_assn.fresh |
33 thm trm_assn.exhaust |
31 thm trm_assn.exhaust |
34 thm trm_assn.strong_exhaust |
32 thm trm_assn.strong_exhaust |
35 |
33 |
36 lemma bn_inj: |
|
37 assumes a: "alpha_bn_raw x y" |
|
38 shows "bn_raw x = bn_raw y \<Longrightarrow> x = y" |
|
39 using a |
|
40 apply(induct) |
|
41 apply(auto)[6] |
|
42 apply(simp) |
|
43 apply(simp) |
|
44 oops |
|
45 |
|
46 |
|
47 |
|
48 lemma lets_bla: |
|
49 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Let (ACons x (Var y) ANil) (Var x)) \<noteq> (Let (ACons x (Var z) ANil) (Var x))" |
|
50 by (simp add: trm_assn.eq_iff) |
|
51 |
|
52 |
|
53 lemma lets_ok: |
|
54 "(Let (ACons x (Var y) ANil) (Var x)) = (Let (ACons y (Var y) ANil) (Var y))" |
|
55 apply (simp add: trm_assn.eq_iff Abs_eq_iff ) |
|
56 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
57 apply (simp_all add: alphas atom_eqvt supp_at_base fresh_star_def trm_assn.bn_defs trm_assn.supp) |
|
58 done |
|
59 |
|
60 lemma lets_ok3: |
|
61 "x \<noteq> y \<Longrightarrow> |
|
62 (Let (ACons x (App (Var y) (Var x)) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq> |
|
63 (Let (ACons y (App (Var x) (Var y)) (ACons x (Var x) ANil)) (App (Var x) (Var y)))" |
|
64 apply (simp add: trm_assn.eq_iff) |
|
65 done |
|
66 |
|
67 |
|
68 lemma lets_not_ok1: |
|
69 "x \<noteq> y \<Longrightarrow> |
|
70 (Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq> |
|
71 (Let (ACons y (Var x) (ACons x (Var y) ANil)) (App (Var x) (Var y)))" |
|
72 apply (simp add: alphas trm_assn.eq_iff trm_assn.supp fresh_star_def atom_eqvt Abs_eq_iff trm_assn.bn_defs) |
|
73 done |
|
74 |
|
75 lemma lets_nok: |
|
76 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
77 (Let (ACons x (App (Var z) (Var z)) (ACons y (Var z) ANil)) (App (Var x) (Var y))) \<noteq> |
|
78 (Let (ACons y (Var z) (ACons x (App (Var z) (Var z)) ANil)) (App (Var x) (Var y)))" |
|
79 apply (simp add: alphas trm_assn.eq_iff fresh_star_def trm_assn.bn_defs Abs_eq_iff trm_assn.supp trm_assn.distinct) |
|
80 done |
|
81 |
|
82 lemma |
|
83 fixes a b c :: name |
|
84 assumes x: "a \<noteq> c" and y: "b \<noteq> c" |
|
85 shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)" |
|
86 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
|
87 apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt) |
|
88 by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y) |
|
89 |
|
90 lemma alpha_bn_refl: "alpha_bn x x" |
|
91 apply (induct x rule: trm_assn.inducts(2)) |
|
92 apply (rule TrueI) |
|
93 apply (auto simp add: trm_assn.eq_iff) |
|
94 done |
|
95 |
|
96 lemma alpha_bn_inducts_raw: |
34 lemma alpha_bn_inducts_raw: |
97 "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw; |
35 "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw; |
98 \<And>trm_raw trm_rawa assn_raw assn_rawa name namea. |
36 \<And>trm_raw trm_rawa assn_raw assn_rawa name namea. |
99 \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa; |
37 \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa; |
100 P3 assn_raw assn_rawa\<rbrakk> |
38 P3 assn_raw assn_rawa\<rbrakk> |
102 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
40 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
103 by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto |
41 by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto |
104 |
42 |
105 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
43 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
106 |
44 |
|
45 |
|
46 |
|
47 lemma alpha_bn_refl: "alpha_bn x x" |
|
48 by (induct x rule: trm_assn.inducts(2)) |
|
49 (rule TrueI, auto simp add: trm_assn.eq_iff) |
|
50 lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x" |
|
51 sorry |
|
52 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z" |
|
53 sorry |
|
54 |
|
55 lemma bn_inj[rule_format]: |
|
56 assumes a: "alpha_bn x y" |
|
57 shows "bn x = bn y \<longrightarrow> x = y" |
|
58 by (rule alpha_bn_inducts[OF a]) (simp_all add: trm_assn.bn_defs) |
|
59 |
|
60 (*lemma alpha_bn_permute: |
|
61 assumes a: "alpha_bn x y" |
|
62 and b: "q \<bullet> bn x = r \<bullet> bn y" |
|
63 shows "alpha_bn (q \<bullet> x) (r \<bullet> y)" |
|
64 proof - |
|
65 have "alpha_bn x (permute_bn r y)" |
|
66 by (rule alpha_bn_trans[OF a]) (rule trm_assn.perm_bn_alpha) |
|
67 then have "alpha_bn (permute_bn r y) x" |
|
68 by (rule alpha_bn_sym) |
|
69 then have "alpha_bn (permute_bn r y) (permute_bn q x)" |
|
70 by (rule alpha_bn_trans) (rule trm_assn.perm_bn_alpha) |
|
71 then have "alpha_bn (permute_bn q x) (permute_bn r y)" |
|
72 by (rule alpha_bn_sym) |
|
73 moreover have "bn (permute_bn q x) = bn (permute_bn r y)" |
|
74 using b trm_assn.permute_bn by simp |
|
75 ultimately have "permute_bn q x = permute_bn r y" |
|
76 using bn_inj by simp |
|
77 *) |
|
78 |
|
79 lemma lets_bla: |
|
80 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Let (ACons x (Var y) ANil) (Var x)) \<noteq> (Let (ACons x (Var z) ANil) (Var x))" |
|
81 by (simp add: trm_assn.eq_iff) |
|
82 |
|
83 |
|
84 lemma lets_ok: |
|
85 "(Let (ACons x (Var y) ANil) (Var x)) = (Let (ACons y (Var y) ANil) (Var y))" |
|
86 apply (simp add: trm_assn.eq_iff Abs_eq_iff ) |
|
87 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
88 apply (simp_all add: alphas atom_eqvt supp_at_base fresh_star_def trm_assn.bn_defs trm_assn.supp) |
|
89 done |
|
90 |
|
91 lemma lets_ok3: |
|
92 "x \<noteq> y \<Longrightarrow> |
|
93 (Let (ACons x (App (Var y) (Var x)) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq> |
|
94 (Let (ACons y (App (Var x) (Var y)) (ACons x (Var x) ANil)) (App (Var x) (Var y)))" |
|
95 apply (simp add: trm_assn.eq_iff) |
|
96 done |
|
97 |
|
98 lemma lets_not_ok1: |
|
99 "x \<noteq> y \<Longrightarrow> |
|
100 (Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq> |
|
101 (Let (ACons y (Var x) (ACons x (Var y) ANil)) (App (Var x) (Var y)))" |
|
102 apply (simp add: alphas trm_assn.eq_iff trm_assn.supp fresh_star_def atom_eqvt Abs_eq_iff trm_assn.bn_defs) |
|
103 done |
|
104 |
|
105 lemma lets_nok: |
|
106 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
107 (Let (ACons x (App (Var z) (Var z)) (ACons y (Var z) ANil)) (App (Var x) (Var y))) \<noteq> |
|
108 (Let (ACons y (Var z) (ACons x (App (Var z) (Var z)) ANil)) (App (Var x) (Var y)))" |
|
109 apply (simp add: alphas trm_assn.eq_iff fresh_star_def trm_assn.bn_defs Abs_eq_iff trm_assn.supp trm_assn.distinct) |
|
110 done |
|
111 |
|
112 lemma |
|
113 fixes a b c :: name |
|
114 assumes x: "a \<noteq> c" and y: "b \<noteq> c" |
|
115 shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)" |
|
116 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
|
117 apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt) |
|
118 by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y) |
|
119 |
107 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
120 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
108 by (simp add: permute_pure) |
121 by (simp add: permute_pure) |
109 |
122 |
110 (* TODO: should be provided by nominal *) |
|
111 lemmas [eqvt] = trm_assn.fv_bn_eqvt |
|
112 |
|
113 thm Abs_lst_fcb |
|
114 |
|
115 (* |
|
116 lemma Abs_lst_fcb2: |
123 lemma Abs_lst_fcb2: |
117 fixes as bs :: "'a :: fs" |
124 fixes as bs :: "'a :: fs" |
118 and x y :: "'b :: fs" |
125 and x y :: "'b :: fs" |
119 and c::"'c::fs" |
126 and c::"'c::fs" |
120 assumes eq: "[ba as]lst. x = [ba bs]lst. y" |
127 assumes eq: "[ba as]lst. x = [ba bs]lst. y" |
121 and fcb1: "set (ba as) \<sharp>* f as x c" |
128 and fcb1: "set (ba as) \<sharp>* f as x c" |
122 and fresh1: "set (ba as) \<sharp>* c" |
129 and fresh1: "set (ba as) \<sharp>* c" |
123 and fresh2: "set (ba bs) \<sharp>* c" |
130 and fresh2: "set (ba bs) \<sharp>* c" |
124 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
131 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
125 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
132 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
133 (* What we would like in this proof, and lets this proof finish *) |
|
134 and bainj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs" |
|
135 (* What the user can supply with the help of alpha_bn *) |
|
136 (* and bainj: "ba as = ba bs \<Longrightarrow> as = bs"*) |
126 shows "f as x c = f bs y c" |
137 shows "f as x c = f bs y c" |
127 proof - |
138 proof - |
128 have "supp (as, x, c) supports (f as x c)" |
139 have "supp (as, x, c) supports (f as x c)" |
129 unfolding supports_def fresh_def[symmetric] |
140 unfolding supports_def fresh_def[symmetric] |
130 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
141 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
165 apply(simp add: fresh_star_eqvt set_eqvt) |
176 apply(simp add: fresh_star_eqvt set_eqvt) |
166 apply(subst (asm) perm1) |
177 apply(subst (asm) perm1) |
167 using inc fresh1 fr1 |
178 using inc fresh1 fr1 |
168 apply(auto simp add: fresh_star_def fresh_Pair) |
179 apply(auto simp add: fresh_star_def fresh_Pair) |
169 done |
180 done |
170 then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 |
181 then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj |
171 by simp |
182 by simp |
172 then have "r \<bullet> ((set (ba bs)) \<sharp>* f (ba bs) y c)" |
183 then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)" |
173 apply(simp add: fresh_star_eqvt set_eqvt) |
184 apply(simp add: fresh_star_eqvt set_eqvt) |
174 apply(subst (asm) perm2[symmetric]) |
185 apply(subst (asm) perm2[symmetric]) |
175 using qq3 fresh2 fr1 |
186 using qq3 fresh2 fr1 |
176 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
187 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
177 done |
188 done |
178 then have fcb2: "(set (ba bs)) \<sharp>* f (ba bs) y c" by (simp add: permute_bool_def) |
189 then have fcb2: "(set (ba bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
179 have "f (ba as) x c = q \<bullet> (f (ba as) x c)" |
190 have "f as x c = q \<bullet> (f as x c)" |
180 apply(rule perm_supp_eq[symmetric]) |
191 apply(rule perm_supp_eq[symmetric]) |
181 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
192 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
182 also have "\<dots> = f (q \<bullet> (ba as)) (q \<bullet> x) c" |
193 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
183 apply(rule perm1) |
194 apply(rule perm1) |
184 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
195 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
185 also have "\<dots> = f (r \<bullet> (ba bs)) (r \<bullet> y) c" using qq1 qq2 by simp |
196 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj by simp |
186 also have "\<dots> = r \<bullet> (f (ba bs) y c)" |
197 also have "\<dots> = r \<bullet> (f bs y c)" |
187 apply(rule perm2[symmetric]) |
198 apply(rule perm2[symmetric]) |
188 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
199 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
189 also have "... = f (ba bs) y c" |
200 also have "... = f bs y c" |
190 apply(rule perm_supp_eq) |
201 apply(rule perm_supp_eq) |
191 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
202 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
192 finally show ?thesis by simp |
203 finally show ?thesis by simp |
193 qed |
204 qed |
194 *) |
|
195 |
205 |
196 nominal_primrec |
206 nominal_primrec |
197 height_trm :: "trm \<Rightarrow> nat" |
207 height_trm :: "trm \<Rightarrow> nat" |
198 and height_assn :: "assn \<Rightarrow> nat" |
208 and height_assn :: "assn \<Rightarrow> nat" |
199 where |
209 where |
212 apply (drule_tac x="trm" in meta_spec) |
222 apply (drule_tac x="trm" in meta_spec) |
213 apply (simp add: alpha_bn_refl) |
223 apply (simp add: alpha_bn_refl) |
214 apply (case_tac b rule: trm_assn.exhaust(2)) |
224 apply (case_tac b rule: trm_assn.exhaust(2)) |
215 apply (auto)[2] |
225 apply (auto)[2] |
216 apply(simp_all) |
226 apply(simp_all) |
217 thm trm_assn.perm_bn_alpha trm_assn.permute_bn |
|
218 apply (erule_tac c="()" in Abs_lst_fcb2) |
227 apply (erule_tac c="()" in Abs_lst_fcb2) |
219 apply (simp_all add: pure_fresh fresh_star_def)[3] |
228 apply (simp_all add: pure_fresh fresh_star_def)[3] |
220 apply (simp add: eqvt_at_def) |
229 apply (simp add: eqvt_at_def) |
221 apply (simp add: eqvt_at_def) |
230 apply (simp add: eqvt_at_def) |
|
231 apply assumption |
222 apply(erule conjE) |
232 apply(erule conjE) |
223 apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff]) |
233 apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff]) |
224 apply (simp add: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff]) |
234 apply (simp add: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff]) |
225 apply (subgoal_tac "eqvt_at height_assn as") |
235 apply (subgoal_tac "eqvt_at height_assn as") |
226 apply (subgoal_tac "eqvt_at height_assn asa") |
236 apply (subgoal_tac "eqvt_at height_assn asa") |
239 apply (subgoal_tac "height_trm b = height_trm ba") |
249 apply (subgoal_tac "height_trm b = height_trm ba") |
240 apply simp |
250 apply simp |
241 apply (erule_tac c="()" in Abs_lst_fcb2) |
251 apply (erule_tac c="()" in Abs_lst_fcb2) |
242 apply (simp_all add: pure_fresh fresh_star_def)[3] |
252 apply (simp_all add: pure_fresh fresh_star_def)[3] |
243 apply (simp_all add: eqvt_at_def)[2] |
253 apply (simp_all add: eqvt_at_def)[2] |
244 apply (drule_tac c="()" in Abs_lst_fcb2) |
254 apply assumption |
|
255 apply (erule_tac c="()" and ba="bn" in Abs_lst_fcb2) |
245 apply (simp_all add: pure_fresh fresh_star_def)[3] |
256 apply (simp_all add: pure_fresh fresh_star_def)[3] |
246 apply (simp_all add: eqvt_at_def)[2] |
257 apply (simp_all add: eqvt_at_def)[2] |
247 apply(simp add: eqvt_def) |
258 apply (rule bn_inj) |
248 apply(perm_simp) |
259 prefer 2 |
249 apply(simp) |
260 apply (simp add: eqvts) |
250 apply(simp add: inj_on_def) |
|
251 apply (rule arg_cong) back |
|
252 oops |
261 oops |
253 |
262 |
254 nominal_primrec |
263 nominal_primrec |
255 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
264 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
256 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |
265 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |