89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm |
90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm |
91 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff |
91 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff |
92 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts |
92 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts |
93 |
93 |
|
94 lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.inducts |
|
95 lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.intros |
|
96 |
94 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
97 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
95 unfolding fresh_star_def Ball_def |
98 unfolding fresh_star_def Ball_def |
96 by auto (simp_all add: fresh_minus_perm) |
99 by auto (simp_all add: fresh_minus_perm) |
97 |
100 |
98 (*primrec |
101 primrec permute_bv_vt_raw |
99 permute_bv_raw |
102 where "permute_bv_vt_raw p VTNil_raw = VTNil_raw" |
100 where |
103 | "permute_bv_vt_raw p (VTCons_raw v t l) = VTCons_raw (p \<bullet> v) t (permute_bv_vt_raw p l)" |
101 "permute_bv_raw p (K c l1 l2 l3) = K c (permute_.. l1) ... |
104 primrec permute_bv_tvck_raw |
102 |
105 where "permute_bv_tvck_raw p TVCKNil_raw = TVCKNil_raw" |
103 (permute_bv p (K (q \<bullet> char) (q \<bullet> tvtk_lst) (q \<bullet> tvck_lst) (q \<bullet> vt_lst) |
106 | "permute_bv_tvck_raw p (TVCKCons_raw v t l) = TVCKCons_raw (p \<bullet> v) t (permute_bv_tvck_raw p l)" |
104 *) |
107 primrec permute_bv_tvtk_raw |
105 |
108 where "permute_bv_tvtk_raw p TVTKNil_raw = TVTKNil_raw" |
106 consts |
109 | "permute_bv_tvtk_raw p (TVTKCons_raw v t l) = TVTKCons_raw (p \<bullet> v) t (permute_bv_tvtk_raw p l)" |
107 permute_bv :: "perm \<Rightarrow> pat \<Rightarrow> pat" |
110 primrec permute_bv_raw |
|
111 where "permute_bv_raw p (K_raw c l1 l2 l3) = |
|
112 K_raw c (permute_bv_tvtk_raw p l1) (permute_bv_tvck_raw p l2) (permute_bv_vt_raw p l3)" |
|
113 |
|
114 quotient_definition "permute_bv_vt :: perm \<Rightarrow> vt_lst \<Rightarrow> vt_lst" |
|
115 is "permute_bv_vt_raw" |
|
116 quotient_definition "permute_bv_tvck :: perm \<Rightarrow> tvck_lst \<Rightarrow> tvck_lst" |
|
117 is "permute_bv_tvck_raw" |
|
118 quotient_definition "permute_bv_tvtk :: perm \<Rightarrow> tvtk_lst \<Rightarrow> tvtk_lst" |
|
119 is "permute_bv_tvtk_raw" |
|
120 quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat" |
|
121 is "permute_bv_raw" |
|
122 |
|
123 lemma rsp_pre: |
|
124 "alpha_tvtk_lst_raw d a \<Longrightarrow> alpha_tvtk_lst_raw (permute_bv_tvtk_raw x d) (permute_bv_tvtk_raw x a)" |
|
125 "alpha_tvck_lst_raw e b \<Longrightarrow> alpha_tvck_lst_raw (permute_bv_tvck_raw x e) (permute_bv_tvck_raw x b)" |
|
126 "alpha_vt_lst_raw f c \<Longrightarrow> alpha_vt_lst_raw (permute_bv_vt_raw x f) (permute_bv_vt_raw x c)" |
|
127 apply (erule_tac [!] alpha_inducts) |
|
128 apply simp_all |
|
129 apply (rule_tac [!] alpha_intros) |
|
130 apply simp_all |
|
131 done |
|
132 |
|
133 lemma [quot_respect]: |
|
134 "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw" |
|
135 "(op = ===> alpha_tvtk_lst_raw ===> alpha_tvtk_lst_raw) permute_bv_tvtk_raw permute_bv_tvtk_raw" |
|
136 "(op = ===> alpha_tvck_lst_raw ===> alpha_tvck_lst_raw) permute_bv_tvck_raw permute_bv_tvck_raw" |
|
137 "(op = ===> alpha_vt_lst_raw ===> alpha_vt_lst_raw) permute_bv_vt_raw permute_bv_vt_raw" |
|
138 apply (simp_all add: rsp_pre) |
|
139 apply clarify |
|
140 apply (erule_tac alpha_inducts) |
|
141 apply (simp_all) |
|
142 apply (rule alpha_intros) |
|
143 apply (simp_all add: rsp_pre) |
|
144 done |
|
145 |
|
146 lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted] |
|
147 permute_bv_vt_raw.simps[quot_lifted] |
|
148 permute_bv_tvck_raw.simps[quot_lifted] |
|
149 permute_bv_tvtk_raw.simps[quot_lifted] |
|
150 |
|
151 lemma perm_bv1: |
|
152 "p \<bullet> bv_tvck b = bv_tvck (permute_bv_tvck p b)" |
|
153 "p \<bullet> bv_tvtk c = bv_tvtk (permute_bv_tvtk p c)" |
|
154 "p \<bullet> bv_vt d = bv_vt (permute_bv_vt p d)" |
|
155 apply(induct b rule: inducts(12)) |
|
156 apply(rule TrueI) |
|
157 apply(simp_all add:permute_bv eqvts) |
|
158 apply(induct c rule: inducts(11)) |
|
159 apply(rule TrueI) |
|
160 apply(simp_all add:permute_bv eqvts) |
|
161 apply(induct d rule: inducts(10)) |
|
162 apply(rule TrueI) |
|
163 apply(simp_all add:permute_bv eqvts) |
|
164 done |
|
165 |
|
166 lemma perm_bv2: |
|
167 "p \<bullet> bv l = bv (permute_bv p l)" |
|
168 apply(induct l rule: inducts(9)) |
|
169 apply(rule TrueI) |
|
170 apply(simp_all add:permute_bv) |
|
171 apply(simp add: perm_bv1[symmetric]) |
|
172 apply(simp add: eqvts) |
|
173 done |
108 |
174 |
109 lemma ACons_subst: |
175 lemma ACons_subst: |
110 "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
176 "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
111 sorry |
177 sorry |
112 |
178 |
113 lemma perm_bv: |
179 lemma permute_bv_zero1: |
114 "p \<bullet> bv l = bv (permute_bv p l)" |
180 "permute_bv_tvck 0 b = b" |
115 sorry |
181 "permute_bv_tvtk 0 c = c" |
116 |
182 "permute_bv_vt 0 d = d" |
117 |
183 apply(induct b rule: inducts(12)) |
|
184 apply(rule TrueI) |
|
185 apply(simp_all add:permute_bv eqvts) |
|
186 apply(induct c rule: inducts(11)) |
|
187 apply(rule TrueI) |
|
188 apply(simp_all add:permute_bv eqvts) |
|
189 apply(induct d rule: inducts(10)) |
|
190 apply(rule TrueI) |
|
191 apply(simp_all add:permute_bv eqvts) |
|
192 done |
|
193 |
|
194 lemma permute_bv_zero2: |
|
195 "permute_bv 0 a = a" |
|
196 apply(induct a rule: inducts(9)) |
|
197 apply(rule TrueI) |
|
198 apply(simp_all add:permute_bv eqvts permute_bv_zero1) |
|
199 done |
118 |
200 |
119 lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x" |
201 lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x" |
120 apply (induct x rule: inducts(11)) |
202 apply (induct x rule: inducts(11)) |
121 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
203 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
122 apply (simp_all add: eq_iff fresh_star_union) |
204 apply (simp_all add: eq_iff fresh_star_union) |
268 P9 (i :: 'i :: pt) pat \<and> |
350 P9 (i :: 'i :: pt) pat \<and> |
269 P10 (j :: 'j :: pt) vt_lst \<and> |
351 P10 (j :: 'j :: pt) vt_lst \<and> |
270 P11 (k :: 'k :: pt) tvtk_lst \<and> |
352 P11 (k :: 'k :: pt) tvtk_lst \<and> |
271 P12 (l :: 'l :: pt) tvck_lst" |
353 P12 (l :: 'l :: pt) tvck_lst" |
272 proof - |
354 proof - |
273 have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat))) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))" |
355 have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vt q (p \<bullet> vt_lst)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvtk q (p \<bullet> tvtk_lst)))" and a4:"(\<forall>p q l. P12 l (permute_bv_tvck q (p \<bullet> tvck_lst)))" |
274 apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
356 apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts) |
275 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
357 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
276 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
358 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
277 |
359 |
278 (* GOAL1 *) |
360 (* GOAL1 *) |
279 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> |
361 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> |
530 apply simp |
612 apply simp |
531 apply(rotate_tac 1) |
613 apply(rotate_tac 1) |
532 apply(erule_tac x="(pa + p)" in allE) |
614 apply(erule_tac x="(pa + p)" in allE) |
533 apply simp |
615 apply simp |
534 apply simp |
616 apply simp |
535 apply (simp add: perm_bv[symmetric]) |
617 apply (simp add: perm_bv2[symmetric]) |
536 apply (simp add: eqvts eqvts_raw) |
618 apply (simp add: eqvts eqvts_raw) |
537 apply (rule at_set_avoiding2) |
619 apply (rule at_set_avoiding2) |
538 apply (simp add: fin_bv) |
620 apply (simp add: fin_bv) |
539 apply (simp add: finite_supp) |
621 apply (simp add: finite_supp) |
540 apply (simp add: supp_Abs) |
622 apply (simp add: supp_Abs) |
541 apply (rule finite_Diff) |
623 apply (rule finite_Diff) |
542 apply (simp add: finite_supp) |
624 apply (simp add: finite_supp) |
543 apply (simp add: fresh_star_def fresh_def supp_Abs eqvts) |
625 apply (simp add: fresh_star_def fresh_def supp_Abs eqvts) |
544 (* Goal for K *) |
626 done |
545 apply (simp) |
627 then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+) |
546 sorry |
628 moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+) |
547 have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast |
629 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
548 have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast |
|
549 have g3: "P3 c (0 \<bullet> ty) \<and> |
|
550 P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and> |
|
551 P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and> |
|
552 P10 j (0 \<bullet> vt_lst) \<and> P11 k (0 \<bullet> tvtk_lst) \<and> P12 l (0 \<bullet> tvck_lst)" using a by blast |
|
553 show ?thesis using g1 g2 g3 by simp |
|
554 qed |
630 qed |
555 |
631 |
556 end |
632 end |
557 |
633 |