140 |
140 |
141 instance trm1 and bp :: fs |
141 instance trm1 and bp :: fs |
142 apply default |
142 apply default |
143 apply (rule rtrm1_bp_fs)+ |
143 apply (rule rtrm1_bp_fs)+ |
144 done |
144 done |
145 |
145 lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" |
146 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
|
147 apply(induct bp rule: trm1_bp_inducts(2)) |
146 apply(induct bp rule: trm1_bp_inducts(2)) |
148 apply(simp_all) |
147 apply(simp_all) |
|
148 done |
|
149 |
|
150 lemma fv_eq_bv: "fv_bp = bv1" |
|
151 apply(rule ext) |
|
152 apply(rule fv_eq_bv_pre) |
149 done |
153 done |
150 |
154 |
151 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}" |
155 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}" |
152 apply auto |
156 apply auto |
153 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI) |
157 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI) |
162 |
166 |
163 lemma alpha_bp_eq: "alpha_bp = (op =)" |
167 lemma alpha_bp_eq: "alpha_bp = (op =)" |
164 apply (rule ext)+ |
168 apply (rule ext)+ |
165 apply (rule alpha_bp_eq_eq) |
169 apply (rule alpha_bp_eq_eq) |
166 done |
170 done |
|
171 |
|
172 lemma ex_out: |
|
173 "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))" |
|
174 "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))" |
|
175 "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
176 "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
177 "(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W x))" |
|
178 apply (blast)+ |
|
179 done |
|
180 |
|
181 lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\<exists>p. (bs, x) \<approx>gen op = supp p (cs, y) \<and> (bs, x') \<approx>gen op = supp p (cs, y'))" |
|
182 thm Abs_eq_iff |
|
183 apply (simp add: Abs_eq_iff) |
|
184 apply (rule arg_cong[of _ _ "Ex"]) |
|
185 apply (rule ext) |
|
186 apply (simp only: alpha_gen) |
|
187 apply (simp only: supp_Pair eqvts) |
|
188 apply rule |
|
189 apply (erule conjE)+ |
|
190 oops |
|
191 |
|
192 lemma "(f (p \<bullet> bp), p \<bullet> bp) \<approx>gen op = f pi (f bp, bp) = False" |
|
193 apply (simp add: alpha_gen fresh_star_def) |
|
194 oops |
|
195 |
|
196 (* TODO: permute_ABS should be in eqvt? *) |
|
197 |
|
198 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
|
199 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
167 |
200 |
168 lemma supp_fv: |
201 lemma supp_fv: |
169 "supp t = fv_trm1 t" |
202 "supp t = fv_trm1 t" |
170 "supp b = fv_bp b" |
203 "supp b = fv_bp b" |
171 apply(induct t and b rule: trm1_bp_inducts) |
204 apply(induct t and b rule: trm1_bp_inducts) |
186 apply(simp (no_asm) add: supp_def eqvts) |
219 apply(simp (no_asm) add: supp_def eqvts) |
187 apply(fold supp_def) |
220 apply(fold supp_def) |
188 apply(simp add: supp_at_base) |
221 apply(simp add: supp_at_base) |
189 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
222 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
190 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
223 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
191 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)*) |
224 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)") |
192 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)") |
225 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*) |
193 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv) |
226 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv) |
194 apply(blast) (* Un_commute in a good place *) |
227 apply(blast) (* Un_commute in a good place *) |
195 apply(simp (no_asm) only: supp_def permute_trm1) |
228 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1) |
196 apply(simp only: alpha1_INJ) |
229 apply(simp only: alpha1_INJ permute_ABS permute_prod.simps Abs_eq_iff) |
|
230 apply(simp only: ex_out) |
197 apply(simp only: Un_commute) |
231 apply(simp only: Un_commute) |
|
232 apply(simp only: alpha_bp_eq fv_eq_bv) |
|
233 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
|
234 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
|
235 apply(simp only: ex_out) |
|
236 apply(simp only: Collect_neg_conj finite_Un Diff_cancel) |
|
237 apply(simp) |
198 apply(simp add: Collect_imp_eq) |
238 apply(simp add: Collect_imp_eq) |
199 apply(simp add: Collect_neg_eq[symmetric]) |
239 apply(simp add: Collect_neg_eq[symmetric] fresh_star_def) |
200 apply(simp only: Abs_eq_iff) |
240 apply(fold supp_def) |
201 apply(simp add: alpha_bp_eq) |
|
202 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
|
203 apply(simp add: alpha_gen fv_eq_bv supp_Pair) |
|
204 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
|
205 apply(simp add: Collect_imp_eq Collect_neg_eq Collect_disj_eq fresh_star_def helper2) |
|
206 sorry |
241 sorry |
207 |
242 |
208 lemma trm1_supp: |
243 lemma trm1_supp: |
209 "supp (Vr1 x) = {atom x}" |
244 "supp (Vr1 x) = {atom x}" |
210 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
245 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |