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 supports: |
172 lemma supports: |
177 "(supp (atom x)) supports (Vr1 x)" |
173 "(supp (atom x)) supports (Vr1 x)" |
179 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
175 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
180 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
176 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
181 "{} supports BUnit" |
177 "{} supports BUnit" |
182 "(supp (atom x)) supports (BVr x)" |
178 "(supp (atom x)) supports (BVr x)" |
183 "(supp a \<union> supp b) supports (BPr a b)" |
179 "(supp a \<union> supp b) supports (BPr a b)" |
184 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh) |
180 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1) |
185 apply(rule_tac [!] allI)+ |
181 apply(rule_tac [!] allI)+ |
186 apply(rule_tac [!] impI) |
182 apply(rule_tac [!] impI) |
187 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
183 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
188 apply(simp_all add: fresh_atom) |
184 apply(simp_all add: fresh_atom) |
189 done |
185 done |
221 apply(simp only: supp_at_base[simplified supp_def]) |
217 apply(simp only: supp_at_base[simplified supp_def]) |
222 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
218 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
223 apply(simp add: Collect_imp_eq Collect_neg_eq) |
219 apply(simp add: Collect_imp_eq Collect_neg_eq) |
224 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)") |
225 apply(simp add: supp_Abs fv_trm1) |
221 apply(simp add: supp_Abs fv_trm1) |
226 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) |
227 apply(simp add: alpha1_INJ) |
223 apply(simp add: alpha1_INJ) |
228 apply(simp add: Abs_eq_iff) |
224 apply(simp add: Abs_eq_iff) |
229 apply(simp add: alpha_gen.simps) |
225 apply(simp add: alpha_gen.simps) |
230 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
226 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
231 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)") |
232 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
228 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
233 apply(simp (no_asm) add: supp_def) |
229 apply(simp (no_asm) add: supp_def permute_trm1) |
234 apply(simp add: alpha1_INJ alpha_bp_eq) |
230 apply(simp add: alpha1_INJ alpha_bp_eq) |
235 apply(simp add: Abs_eq_iff) |
231 apply(simp add: Abs_eq_iff) |
236 apply(simp add: alpha_gen) |
232 apply(simp add: alpha_gen) |
237 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) |
238 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) |
577 quotient_definition |
573 quotient_definition |
578 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
574 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
579 is |
575 is |
580 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
576 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
581 |
577 |
582 lemma trm5_lts_zero: |
578 instance by default |
583 "0 \<bullet> (x\<Colon>trm5) = x" |
579 (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
584 "0 \<bullet> (y\<Colon>lts) = y" |
|
585 apply(induct x and y rule: trm5_lts_inducts) |
|
586 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
587 done |
|
588 |
|
589 lemma trm5_lts_plus: |
|
590 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x" |
|
591 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y" |
|
592 apply(induct x and y rule: trm5_lts_inducts) |
|
593 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
594 done |
|
595 |
|
596 instance |
|
597 apply default |
|
598 apply (simp_all add: trm5_lts_zero trm5_lts_plus) |
|
599 done |
|
600 |
580 |
601 end |
581 end |
602 |
582 |
603 lemmas |
583 lemmas |
604 permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
584 permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
605 and |
585 and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
606 alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
586 and bv5[simp] = rbv5.simps[quot_lifted] |
607 and |
587 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
608 bv5[simp] = rbv5.simps[quot_lifted] |
|
609 and |
|
610 fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
611 |
588 |
612 lemma lets_ok: |
589 lemma lets_ok: |
613 "(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))" |
614 apply (subst alpha5_INJ) |
591 apply (subst alpha5_INJ) |
615 apply (rule conjI) |
592 apply (rule conjI) |