171 lemmas |
171 lemmas |
172 fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
172 fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
173 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
173 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
174 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
174 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
175 |
175 |
176 lemma lm1_supp_pre: |
176 lemma supports: |
177 shows "(supp (atom x, t)) supports (Lm1 x t) " |
177 "(supp (atom x)) supports (Vr1 x)" |
178 apply(simp add: supports_def) |
178 "(supp t \<union> supp s) supports (Ap1 t s)" |
179 apply(fold fresh_def) |
179 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
180 apply(simp add: fresh_Pair swap_fresh_fresh) |
180 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
181 apply(clarify) |
181 "{} supports BUnit" |
182 apply(subst swap_at_base_simps(3)) |
182 "(supp (atom x)) supports (BVr x)" |
|
183 "(supp a \<union> supp b) supports (BPr a b)" |
|
184 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh) |
|
185 apply(rule_tac [!] allI)+ |
|
186 apply(rule_tac [!] impI) |
|
187 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
183 apply(simp_all add: fresh_atom) |
188 apply(simp_all add: fresh_atom) |
184 done |
189 done |
185 |
190 |
186 lemma lt1_supp_pre: |
191 lemma rtrm1_bp_fs: |
187 shows "(supp (x, t, s)) supports (Lt1 t x s) " |
192 "finite (supp (x :: trm1))" |
188 apply(simp add: supports_def) |
193 "finite (supp (b :: bp))" |
189 apply(fold fresh_def) |
194 apply (induct x and b rule: trm1_bp_inducts) |
190 apply(simp add: fresh_Pair swap_fresh_fresh) |
195 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
191 done |
196 apply(simp_all add: supp_atom) |
192 |
|
193 lemma bp_supp: "finite (supp (bp :: bp))" |
|
194 apply (induct bp) |
|
195 apply(simp_all add: supp_def) |
|
196 apply(simp add: supp_at_base supp_def[symmetric]) |
|
197 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def) |
|
198 done |
197 done |
199 |
198 |
200 instance trm1 :: fs |
199 instance trm1 :: fs |
201 apply default |
200 apply default |
202 apply(induct_tac x rule: trm1_bp_inducts(1)) |
201 apply (rule rtrm1_bp_fs(1)) |
203 apply(simp_all) |
|
204 apply(simp add: supp_def alpha1_INJ eqvts) |
|
205 apply(simp add: supp_def[symmetric] supp_at_base) |
|
206 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1) |
|
207 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
208 apply(rule supports_finite) |
|
209 apply(rule lm1_supp_pre) |
|
210 apply(simp add: supp_Pair supp_atom) |
|
211 apply(rule supports_finite) |
|
212 apply(rule lt1_supp_pre) |
|
213 apply(simp add: supp_Pair supp_atom bp_supp) |
|
214 done |
202 done |
215 |
203 |
216 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
204 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
217 apply(induct bp rule: trm1_bp_inducts(2)) |
205 apply(induct bp rule: trm1_bp_inducts(2)) |
218 apply(simp_all) |
206 apply(simp_all) |