101 done |
101 done |
102 |
102 |
103 lemma rfv_trm1_eqvt[eqvt]: |
103 lemma rfv_trm1_eqvt[eqvt]: |
104 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)" |
104 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)" |
105 sorry |
105 sorry |
|
106 |
|
107 (* Shouyld we derive it? But bv is given by the user? *) |
|
108 lemma bv1_eqvt[eqvt]: |
|
109 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
|
110 apply (induct x) |
|
111 apply (simp_all add: eqvts) |
|
112 apply (rule atom_eqvt) |
|
113 done |
106 |
114 |
107 lemma alpha1_eqvt: |
115 lemma alpha1_eqvt: |
108 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
116 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
109 sorry |
117 sorry |
110 |
118 |
250 "(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))" |
258 "(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))" |
251 "(Lt1 b1 t1 s1 = Lt1 b2 t2 s2) = (t1 = t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen (op =) fv_trm1 pi ((bv1 b2), s2))))" |
259 "(Lt1 b1 t1 s1 = Lt1 b2 t2 s2) = (t1 = t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen (op =) fv_trm1 pi ((bv1 b2), s2))))" |
252 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen]) |
260 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen]) |
253 done |
261 done |
254 |
262 |
|
263 instance trm1 :: fs |
|
264 apply default |
|
265 apply(induct_tac x rule: trm1_bp_inducts(1)) |
|
266 apply(simp_all) |
|
267 apply(simp add: supp_def alpha1_INJ eqvts) |
|
268 apply(simp add: supp_def[symmetric] supp_at_base) |
|
269 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1) |
|
270 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
271 sorry |
|
272 |
|
273 |
255 lemma supp_fv: |
274 lemma supp_fv: |
256 shows "supp t = fv_trm1 t" |
275 shows "supp t = fv_trm1 t" |
257 apply(induct t rule: trm1_bp_inducts(1)) |
276 apply(induct t rule: trm1_bp_inducts(1)) |
258 apply(simp_all add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
277 apply(simp_all) |
259 apply(simp_all only: supp_at_base[simplified supp_def]) |
278 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
260 apply(simp_all add: Collect_imp_eq Collect_neg_eq) |
279 apply(simp only: supp_at_base[simplified supp_def]) |
261 sorry (* Lam & Let still to do *) |
280 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
281 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
282 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
|
283 apply(simp add: supp_Abs fv_trm1) |
|
284 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
|
285 apply(simp add: alpha1_INJ) |
|
286 apply(simp add: Abs_eq_iff) |
|
287 apply(simp add: alpha_gen.simps) |
|
288 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
|
289 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
|
290 apply(simp add: supp_Abs fv_trm1) |
|
291 apply(simp (no_asm) add: supp_def) |
|
292 apply(simp add: alpha1_INJ) |
|
293 apply(simp add: Abs_eq_iff) |
|
294 apply(simp add: alpha_gen.simps) |
|
295 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
|
296 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
297 done |
262 |
298 |
263 |
299 |
264 |
300 |
265 section {*** lets with single assignments ***} |
301 section {*** lets with single assignments ***} |
266 |
302 |