equal
deleted
inserted
replaced
119 |
119 |
120 lemma alpha1_eqvt: |
120 lemma alpha1_eqvt: |
121 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) |
122 apply (induct t s rule: alpha1.inducts) |
123 apply (simp_all add:eqvts alpha1_inj) |
123 apply (simp_all add:eqvts alpha1_inj) |
124 sorry |
124 apply (erule exE) |
|
125 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
126 apply (simp add: alpha_gen) |
|
127 apply(erule conjE)+ |
|
128 apply(rule conjI) |
|
129 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
130 apply(simp add: atom_eqvt eqvts) |
|
131 apply(rule conjI) |
|
132 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
133 apply(simp add: eqvts atom_eqvt) |
|
134 apply(simp add: permute_eqvt[symmetric]) |
|
135 apply (erule exE) |
|
136 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
137 apply (simp add: alpha_gen) |
|
138 apply(erule conjE)+ |
|
139 apply(rule conjI) |
|
140 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
141 apply(simp add: atom_eqvt eqvts) |
|
142 apply(rule conjI) |
|
143 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
144 apply(simp add: eqvts atom_eqvt) |
|
145 apply(simp add: permute_eqvt[symmetric]) |
|
146 done |
125 |
147 |
126 lemma alpha1_equivp: "equivp alpha1" |
148 lemma alpha1_equivp: "equivp alpha1" |
127 sorry |
149 sorry |
128 |
150 |
129 quotient_type trm1 = rtrm1 / alpha1 |
151 quotient_type trm1 = rtrm1 / alpha1 |
329 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
351 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
330 apply(simp add: supp_Abs fv_trm1) |
352 apply(simp add: supp_Abs fv_trm1) |
331 apply(simp (no_asm) add: supp_def) |
353 apply(simp (no_asm) add: supp_def) |
332 apply(simp add: alpha1_INJ) |
354 apply(simp add: alpha1_INJ) |
333 apply(simp add: Abs_eq_iff) |
355 apply(simp add: Abs_eq_iff) |
334 apply(simp add: alpha_gen.simps) |
356 apply(simp add: alpha_gen) |
335 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
357 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
336 apply(simp add: Collect_imp_eq Collect_neg_eq) |
358 apply(simp add: Collect_imp_eq Collect_neg_eq) |
337 done |
359 done |
338 |
360 |
339 lemma trm1_supp: |
361 lemma trm1_supp: |