98 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
98 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
99 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
99 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
100 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
100 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
101 done |
101 done |
102 |
102 |
103 lemma rfv_trm1_eqvt[eqvt]: |
|
104 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)" |
|
105 sorry |
|
106 |
|
107 (* Shouyld we derive it? But bv is given by the user? *) |
103 (* Shouyld we derive it? But bv is given by the user? *) |
108 lemma bv1_eqvt[eqvt]: |
104 lemma bv1_eqvt[eqvt]: |
109 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
105 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
110 apply (induct x) |
106 apply (induct x) |
111 apply (simp_all add: eqvts) |
107 apply (simp_all add: eqvts) |
112 apply (rule atom_eqvt) |
108 apply (rule atom_eqvt) |
113 done |
109 done |
114 |
110 |
|
111 lemma rfv_trm1_eqvt[eqvt]: |
|
112 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)" |
|
113 apply (induct t) |
|
114 apply (simp_all add: eqvts) |
|
115 apply (rule atom_eqvt) |
|
116 apply (simp add: atom_eqvt) |
|
117 done |
|
118 |
|
119 |
115 lemma alpha1_eqvt: |
120 lemma alpha1_eqvt: |
116 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
121 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
|
122 apply (induct t s rule: alpha1.inducts) |
|
123 apply (simp_all add:eqvts alpha1_inj) |
117 sorry |
124 sorry |
118 |
125 |
119 lemma alpha1_equivp: "equivp alpha1" |
126 lemma alpha1_equivp: "equivp alpha1" |
120 sorry |
127 sorry |
121 |
128 |
258 "(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))" |
265 "(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))" |
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))))" |
266 "(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))))" |
260 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen]) |
267 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen]) |
261 done |
268 done |
262 |
269 |
|
270 lemma lm1_supp_pre: |
|
271 shows "(supp (atom x, t)) supports (Lm1 x t) " |
|
272 apply(simp add: supports_def) |
|
273 apply(fold fresh_def) |
|
274 apply(simp add: fresh_Pair swap_fresh_fresh) |
|
275 apply(clarify) |
|
276 apply(subst swap_at_base_simps(3)) |
|
277 apply(simp_all add: fresh_atom) |
|
278 done |
|
279 |
|
280 lemma lt1_supp_pre: |
|
281 shows "(supp (x, t, s)) supports (Lt1 t x s) " |
|
282 apply(simp add: supports_def) |
|
283 apply(fold fresh_def) |
|
284 apply(simp add: fresh_Pair swap_fresh_fresh) |
|
285 done |
|
286 |
|
287 lemma bp_supp: "finite (supp (bp :: bp))" |
|
288 apply (induct bp) |
|
289 apply(simp_all add: supp_def) |
|
290 apply (fold supp_def) |
|
291 apply (simp add: supp_at_base) |
|
292 apply(simp add: Collect_imp_eq) |
|
293 apply(simp add: Collect_neg_eq[symmetric]) |
|
294 apply (fold supp_def) |
|
295 apply (simp) |
|
296 done |
|
297 |
263 instance trm1 :: fs |
298 instance trm1 :: fs |
264 apply default |
299 apply default |
265 apply(induct_tac x rule: trm1_bp_inducts(1)) |
300 apply(induct_tac x rule: trm1_bp_inducts(1)) |
266 apply(simp_all) |
301 apply(simp_all) |
267 apply(simp add: supp_def alpha1_INJ eqvts) |
302 apply(simp add: supp_def alpha1_INJ eqvts) |
268 apply(simp add: supp_def[symmetric] supp_at_base) |
303 apply(simp add: supp_def[symmetric] supp_at_base) |
269 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1) |
304 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1) |
270 apply(simp add: Collect_imp_eq Collect_neg_eq) |
305 apply(simp add: Collect_imp_eq Collect_neg_eq) |
271 sorry |
306 apply(rule supports_finite) |
272 |
307 apply(rule lm1_supp_pre) |
|
308 apply(simp add: supp_Pair supp_atom) |
|
309 apply(rule supports_finite) |
|
310 apply(rule lt1_supp_pre) |
|
311 apply(simp add: supp_Pair supp_atom bp_supp) |
|
312 done |
273 |
313 |
274 lemma supp_fv: |
314 lemma supp_fv: |
275 shows "supp t = fv_trm1 t" |
315 shows "supp t = fv_trm1 t" |
276 apply(induct t rule: trm1_bp_inducts(1)) |
316 apply(induct t rule: trm1_bp_inducts(1)) |
277 apply(simp_all) |
317 apply(simp_all) |