16 bn |
16 bn |
17 where |
17 where |
18 "bn ANil = []" |
18 "bn ANil = []" |
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
20 |
20 |
|
21 print_theorems |
|
22 |
21 thm trm_assn.fv_defs |
23 thm trm_assn.fv_defs |
22 thm trm_assn.eq_iff |
24 thm trm_assn.eq_iff |
23 thm trm_assn.bn_defs |
25 thm trm_assn.bn_defs |
|
26 thm trm_assn.bn_inducts |
24 thm trm_assn.perm_simps |
27 thm trm_assn.perm_simps |
25 thm trm_assn.induct |
28 thm trm_assn.induct |
26 thm trm_assn.inducts |
29 thm trm_assn.inducts |
27 thm trm_assn.distinct |
30 thm trm_assn.distinct |
28 thm trm_assn.supp |
31 thm trm_assn.supp |
29 thm trm_assn.fresh |
32 thm trm_assn.fresh |
30 thm trm_assn.exhaust |
33 thm trm_assn.exhaust |
31 thm trm_assn.strong_exhaust |
34 thm trm_assn.strong_exhaust |
32 |
35 |
|
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 |
33 |
47 |
34 lemma lets_bla: |
48 lemma lets_bla: |
35 "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))" |
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))" |
36 by (simp add: trm_assn.eq_iff) |
50 by (simp add: trm_assn.eq_iff) |
37 |
51 |
94 by (simp add: permute_pure) |
108 by (simp add: permute_pure) |
95 |
109 |
96 (* TODO: should be provided by nominal *) |
110 (* TODO: should be provided by nominal *) |
97 lemmas [eqvt] = trm_assn.fv_bn_eqvt |
111 lemmas [eqvt] = trm_assn.fv_bn_eqvt |
98 |
112 |
|
113 thm Abs_lst_fcb |
|
114 |
|
115 (* |
99 lemma Abs_lst_fcb2: |
116 lemma Abs_lst_fcb2: |
100 fixes as bs :: "'a :: fs" |
117 fixes as bs :: "'a :: fs" |
101 and x y :: "'b :: fs" |
118 and x y :: "'b :: fs" |
102 and c::"'c::fs" |
119 and c::"'c::fs" |
103 assumes eq: "[ba as]lst. x = [ba bs]lst. y" |
120 assumes eq: "[ba as]lst. x = [ba bs]lst. y" |
104 and fcb1: "(set (ba as)) \<sharp>* f as x c" |
121 and fcb1: "set (ba as) \<sharp>* f as x c" |
105 and fresh1: "set (ba as) \<sharp>* c" |
122 and fresh1: "set (ba as) \<sharp>* c" |
106 and fresh2: "set (ba bs) \<sharp>* c" |
123 and fresh2: "set (ba bs) \<sharp>* c" |
107 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) 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" |
108 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) 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" |
109 and props: "eqvt ba" "inj ba" |
|
110 shows "f as x c = f bs y c" |
126 shows "f as x c = f bs y c" |
111 proof - |
127 proof - |
112 have "supp (as, x, c) supports (f as x c)" |
128 have "supp (as, x, c) supports (f as x c)" |
113 unfolding supports_def fresh_def[symmetric] |
129 unfolding supports_def fresh_def[symmetric] |
114 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
130 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
121 by (auto intro: supports_finite simp add: finite_supp) |
137 by (auto intro: supports_finite simp add: finite_supp) |
122 obtain q::"perm" where |
138 obtain q::"perm" where |
123 fr1: "(q \<bullet> (set (ba as))) \<sharp>* (x, c, f as x c, f bs y c)" and |
139 fr1: "(q \<bullet> (set (ba as))) \<sharp>* (x, c, f as x c, f bs y c)" and |
124 fr2: "supp q \<sharp>* ([ba as]lst. x)" and |
140 fr2: "supp q \<sharp>* ([ba as]lst. x)" and |
125 inc: "supp q \<subseteq> (set (ba as)) \<union> q \<bullet> (set (ba as))" |
141 inc: "supp q \<subseteq> (set (ba as)) \<union> q \<bullet> (set (ba as))" |
126 using at_set_avoiding3[where xs="set (ba as)" and c="(x, c, f as x c, f bs y c)" and x="[ba as]lst. x"] |
142 using at_set_avoiding3[where xs="set (ba as)" and c="(x, c, f as x c, f bs y c)" |
127 fin1 fin2 |
143 and x="[ba as]lst. x"] fin1 fin2 |
128 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
144 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
129 have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = q \<bullet> ([ba as]lst. x)" by simp |
145 have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = q \<bullet> ([ba as]lst. x)" by simp |
130 also have "\<dots> = [ba as]lst. x" |
146 also have "\<dots> = [ba as]lst. x" |
131 by (simp only: fr2 perm_supp_eq) |
147 by (simp only: fr2 perm_supp_eq) |
132 finally have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = [ba bs]lst. y" using eq by simp |
148 finally have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = [ba bs]lst. y" using eq by simp |
140 apply(erule conjE)+ |
156 apply(erule conjE)+ |
141 apply(drule_tac x="p" in meta_spec) |
157 apply(drule_tac x="p" in meta_spec) |
142 apply(simp add: set_eqvt) |
158 apply(simp add: set_eqvt) |
143 apply(blast) |
159 apply(blast) |
144 done |
160 done |
145 have qq4: "q \<bullet> as = r \<bullet> bs" using qq2 props unfolding eqvt_def inj_on_def |
|
146 apply(perm_simp) |
|
147 apply(simp) |
|
148 done |
|
149 have "(set (ba as)) \<sharp>* f as x c" by (rule fcb1) |
161 have "(set (ba as)) \<sharp>* f as x c" by (rule fcb1) |
150 then have "q \<bullet> ((set (ba as)) \<sharp>* f as x c)" |
162 then have "q \<bullet> ((set (ba as)) \<sharp>* f as x c)" |
151 by (simp add: permute_bool_def) |
163 by (simp add: permute_bool_def) |
152 then have "set (q \<bullet> (ba as)) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
164 then have "set (q \<bullet> (ba as)) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
153 apply(simp add: fresh_star_eqvt set_eqvt) |
165 apply(simp add: fresh_star_eqvt set_eqvt) |
154 apply(subst (asm) perm1) |
166 apply(subst (asm) perm1) |
155 using inc fresh1 fr1 |
167 using inc fresh1 fr1 |
156 apply(auto simp add: fresh_star_def fresh_Pair) |
168 apply(auto simp add: fresh_star_def fresh_Pair) |
157 done |
169 done |
158 then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 qq4 |
170 then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 |
159 by simp |
171 by simp |
160 then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)" |
172 then have "r \<bullet> ((set (ba bs)) \<sharp>* f (ba bs) y c)" |
161 apply(simp add: fresh_star_eqvt set_eqvt) |
173 apply(simp add: fresh_star_eqvt set_eqvt) |
162 apply(subst (asm) perm2[symmetric]) |
174 apply(subst (asm) perm2[symmetric]) |
163 using qq3 fresh2 fr1 |
175 using qq3 fresh2 fr1 |
164 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
176 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
165 done |
177 done |
166 then have fcb2: "(set (ba bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
178 then have fcb2: "(set (ba bs)) \<sharp>* f (ba bs) y c" by (simp add: permute_bool_def) |
167 have "f as x c = q \<bullet> (f as x c)" |
179 have "f (ba as) x c = q \<bullet> (f (ba as) x c)" |
168 apply(rule perm_supp_eq[symmetric]) |
180 apply(rule perm_supp_eq[symmetric]) |
169 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
181 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
170 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
182 also have "\<dots> = f (q \<bullet> (ba as)) (q \<bullet> x) c" |
171 apply(rule perm1) |
183 apply(rule perm1) |
172 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
184 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
173 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq4 by simp |
185 also have "\<dots> = f (r \<bullet> (ba bs)) (r \<bullet> y) c" using qq1 qq2 by simp |
174 also have "\<dots> = r \<bullet> (f bs y c)" |
186 also have "\<dots> = r \<bullet> (f (ba bs) y c)" |
175 apply(rule perm2[symmetric]) |
187 apply(rule perm2[symmetric]) |
176 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
188 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
177 also have "... = f bs y c" |
189 also have "... = f (ba bs) y c" |
178 apply(rule perm_supp_eq) |
190 apply(rule perm_supp_eq) |
179 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
191 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
180 finally show ?thesis by simp |
192 finally show ?thesis by simp |
181 qed |
193 qed |
182 |
194 *) |
183 (* PROBLEM: the proof needs induction on alpha_bn inside which is not possible... *) |
195 |
184 nominal_primrec |
196 nominal_primrec |
185 height_trm :: "trm \<Rightarrow> nat" |
197 height_trm :: "trm \<Rightarrow> nat" |
186 and height_assn :: "assn \<Rightarrow> nat" |
198 and height_assn :: "assn \<Rightarrow> nat" |
187 where |
199 where |
188 "height_trm (Var x) = 1" |
200 "height_trm (Var x) = 1" |
198 apply (auto)[4] |
210 apply (auto)[4] |
199 apply (drule_tac x="assn" in meta_spec) |
211 apply (drule_tac x="assn" in meta_spec) |
200 apply (drule_tac x="trm" in meta_spec) |
212 apply (drule_tac x="trm" in meta_spec) |
201 apply (simp add: alpha_bn_refl) |
213 apply (simp add: alpha_bn_refl) |
202 apply (case_tac b rule: trm_assn.exhaust(2)) |
214 apply (case_tac b rule: trm_assn.exhaust(2)) |
203 apply (auto) |
215 apply (auto)[2] |
204 apply (erule Abs_lst1_fcb) |
216 apply(simp_all) |
205 apply (simp_all add: pure_fresh) |
217 thm trm_assn.perm_bn_alpha trm_assn.permute_bn |
|
218 apply (erule_tac c="()" in Abs_lst_fcb2) |
|
219 apply (simp_all add: pure_fresh fresh_star_def)[3] |
206 apply (simp add: eqvt_at_def) |
220 apply (simp add: eqvt_at_def) |
207 apply (erule Abs_lst_fcb) |
221 apply (simp add: eqvt_at_def) |
208 apply (simp_all add: pure_fresh) |
222 apply(erule conjE) |
209 apply (simp_all add: eqvt_at_def eqvts) |
223 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]) |
|
225 apply (subgoal_tac "eqvt_at height_assn as") |
|
226 apply (subgoal_tac "eqvt_at height_assn asa") |
|
227 apply (subgoal_tac "eqvt_at height_trm b") |
|
228 apply (subgoal_tac "eqvt_at height_trm ba") |
|
229 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr as)") |
|
230 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr asa)") |
|
231 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl b)") |
|
232 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl ba)") |
|
233 defer |
|
234 apply (simp add: eqvt_at_def height_trm_def) |
|
235 apply (simp add: eqvt_at_def height_trm_def) |
|
236 apply (simp add: eqvt_at_def height_assn_def) |
|
237 apply (simp add: eqvt_at_def height_assn_def) |
|
238 apply (subgoal_tac "height_assn as = height_assn asa") |
|
239 apply (subgoal_tac "height_trm b = height_trm ba") |
|
240 apply simp |
|
241 apply (erule_tac c="()" in Abs_lst_fcb2) |
|
242 apply (simp_all add: pure_fresh fresh_star_def)[3] |
|
243 apply (simp_all add: eqvt_at_def)[2] |
|
244 apply (drule_tac c="()" in Abs_lst_fcb2) |
|
245 apply (simp_all add: pure_fresh fresh_star_def)[3] |
|
246 apply (simp_all add: eqvt_at_def)[2] |
|
247 apply(simp add: eqvt_def) |
|
248 apply(perm_simp) |
|
249 apply(simp) |
|
250 apply(simp add: inj_on_def) |
210 apply (rule arg_cong) back |
251 apply (rule arg_cong) back |
211 oops |
252 oops |
212 |
253 |
213 nominal_primrec |
254 nominal_primrec |
214 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
255 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |