156 quotient_definition |
156 quotient_definition |
157 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
157 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
158 is |
158 is |
159 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
159 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
160 |
160 |
161 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
161 instance by default |
162 |
162 (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted]) |
163 instance |
|
164 apply default |
|
165 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
|
166 apply(simp_all) |
|
167 done |
|
168 |
163 |
169 end |
164 end |
170 |
165 |
171 lemmas |
166 lemmas |
172 fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
167 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
|
168 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
173 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
169 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
174 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
170 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
175 |
171 |
176 lemma lm1_supp_pre: |
172 lemma supports: |
177 shows "(supp (atom x, t)) supports (Lm1 x t) " |
173 "(supp (atom x)) supports (Vr1 x)" |
178 apply(simp add: supports_def) |
174 "(supp t \<union> supp s) supports (Ap1 t s)" |
179 apply(fold fresh_def) |
175 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
180 apply(simp add: fresh_Pair swap_fresh_fresh) |
176 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
181 apply(clarify) |
177 "{} supports BUnit" |
182 apply(subst swap_at_base_simps(3)) |
178 "(supp (atom x)) supports (BVr x)" |
|
179 "(supp a \<union> supp b) supports (BPr a b)" |
|
180 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1) |
|
181 apply(rule_tac [!] allI)+ |
|
182 apply(rule_tac [!] impI) |
|
183 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
183 apply(simp_all add: fresh_atom) |
184 apply(simp_all add: fresh_atom) |
184 done |
185 done |
185 |
186 |
186 lemma lt1_supp_pre: |
187 lemma rtrm1_bp_fs: |
187 shows "(supp (x, t, s)) supports (Lt1 t x s) " |
188 "finite (supp (x :: trm1))" |
188 apply(simp add: supports_def) |
189 "finite (supp (b :: bp))" |
189 apply(fold fresh_def) |
190 apply (induct x and b rule: trm1_bp_inducts) |
190 apply(simp add: fresh_Pair swap_fresh_fresh) |
191 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
191 done |
192 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 |
193 done |
199 |
194 |
200 instance trm1 :: fs |
195 instance trm1 :: fs |
201 apply default |
196 apply default |
202 apply(induct_tac x rule: trm1_bp_inducts(1)) |
197 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 |
198 done |
215 |
199 |
216 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
200 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
217 apply(induct bp rule: trm1_bp_inducts(2)) |
201 apply(induct bp rule: trm1_bp_inducts(2)) |
218 apply(simp_all) |
202 apply(simp_all) |
233 apply(simp only: supp_at_base[simplified supp_def]) |
217 apply(simp only: supp_at_base[simplified supp_def]) |
234 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
218 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
235 apply(simp add: Collect_imp_eq Collect_neg_eq) |
219 apply(simp add: Collect_imp_eq Collect_neg_eq) |
236 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
220 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
237 apply(simp add: supp_Abs fv_trm1) |
221 apply(simp add: supp_Abs fv_trm1) |
238 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
222 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
239 apply(simp add: alpha1_INJ) |
223 apply(simp add: alpha1_INJ) |
240 apply(simp add: Abs_eq_iff) |
224 apply(simp add: Abs_eq_iff) |
241 apply(simp add: alpha_gen.simps) |
225 apply(simp add: alpha_gen.simps) |
242 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
226 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
243 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
227 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
244 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
228 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
245 apply(simp (no_asm) add: supp_def) |
229 apply(simp (no_asm) add: supp_def permute_trm1) |
246 apply(simp add: alpha1_INJ alpha_bp_eq) |
230 apply(simp add: alpha1_INJ alpha_bp_eq) |
247 apply(simp add: Abs_eq_iff) |
231 apply(simp add: Abs_eq_iff) |
248 apply(simp add: alpha_gen) |
232 apply(simp add: alpha_gen) |
249 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
233 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
250 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) |
234 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) |
589 quotient_definition |
573 quotient_definition |
590 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
574 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
591 is |
575 is |
592 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
576 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
593 |
577 |
594 lemma trm5_lts_zero: |
578 instance by default |
595 "0 \<bullet> (x\<Colon>trm5) = x" |
579 (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
596 "0 \<bullet> (y\<Colon>lts) = y" |
|
597 apply(induct x and y rule: trm5_lts_inducts) |
|
598 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
599 done |
|
600 |
|
601 lemma trm5_lts_plus: |
|
602 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x" |
|
603 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y" |
|
604 apply(induct x and y rule: trm5_lts_inducts) |
|
605 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
606 done |
|
607 |
|
608 instance |
|
609 apply default |
|
610 apply (simp_all add: trm5_lts_zero trm5_lts_plus) |
|
611 done |
|
612 |
580 |
613 end |
581 end |
614 |
582 |
615 lemmas |
583 lemmas |
616 permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
584 permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
617 and |
585 and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
618 alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
586 and bv5[simp] = rbv5.simps[quot_lifted] |
619 and |
587 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
620 bv5[simp] = rbv5.simps[quot_lifted] |
|
621 and |
|
622 fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
623 |
588 |
624 lemma lets_ok: |
589 lemma lets_ok: |
625 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
590 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
626 apply (subst alpha5_INJ) |
591 apply (subst alpha5_INJ) |
627 apply (rule conjI) |
592 apply (rule conjI) |