|
1 theory ExCoreHaskell |
|
2 imports "../Parser" |
|
3 begin |
|
4 |
|
5 (* core haskell *) |
|
6 |
|
7 ML {* val _ = recursive := false *} |
|
8 |
|
9 atom_decl var |
|
10 atom_decl cvar |
|
11 atom_decl tvar |
|
12 |
|
13 (* there are types, coercion types and regular types list-data-structure *) |
|
14 |
|
15 ML {* val _ = alpha_type := AlphaLst *} |
|
16 nominal_datatype tkind = |
|
17 KStar |
|
18 | KFun "tkind" "tkind" |
|
19 and ckind = |
|
20 CKEq "ty" "ty" |
|
21 and ty = |
|
22 TVar "tvar" |
|
23 | TC "string" |
|
24 | TApp "ty" "ty" |
|
25 | TFun "string" "ty_lst" |
|
26 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
|
27 | TEq "ckind" "ty" |
|
28 and ty_lst = |
|
29 TsNil |
|
30 | TsCons "ty" "ty_lst" |
|
31 and co = |
|
32 CVar "cvar" |
|
33 | CConst "string" |
|
34 | CApp "co" "co" |
|
35 | CFun "string" "co_lst" |
|
36 | CAll cv::"cvar" "ckind" C::"co" bind cv in C |
|
37 | CEq "ckind" "co" |
|
38 | CRefl "ty" |
|
39 | CSym "co" |
|
40 | CCir "co" "co" |
|
41 | CAt "co" "ty" |
|
42 | CLeft "co" |
|
43 | CRight "co" |
|
44 | CSim "co" "co" |
|
45 | CRightc "co" |
|
46 | CLeftc "co" |
|
47 | CCoe "co" "co" |
|
48 and co_lst = |
|
49 CsNil |
|
50 | CsCons "co" "co_lst" |
|
51 and trm = |
|
52 Var "var" |
|
53 | K "string" |
|
54 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t |
|
55 | LAMC cv::"cvar" "ckind" t::"trm" bind cv in t |
|
56 | AppT "trm" "ty" |
|
57 | AppC "trm" "co" |
|
58 | Lam v::"var" "ty" t::"trm" bind v in t |
|
59 | App "trm" "trm" |
|
60 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
|
61 | Case "trm" "assoc_lst" |
|
62 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
|
63 and assoc_lst = |
|
64 ANil |
|
65 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t |
|
66 and pat = |
|
67 Kpat "string" "tvars" "cvars" "vars" |
|
68 and vars = |
|
69 VsNil |
|
70 | VsCons "var" "ty" "vars" |
|
71 and tvars = |
|
72 TvsNil |
|
73 | TvsCons "tvar" "tkind" "tvars" |
|
74 and cvars = |
|
75 CvsNil |
|
76 | CvsCons "cvar" "ckind" "cvars" |
|
77 binder |
|
78 bv :: "pat \<Rightarrow> atom list" |
|
79 and bv_vs :: "vars \<Rightarrow> atom list" |
|
80 and bv_tvs :: "tvars \<Rightarrow> atom list" |
|
81 and bv_cvs :: "cvars \<Rightarrow> atom list" |
|
82 where |
|
83 "bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))" |
|
84 | "bv_vs VsNil = []" |
|
85 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
|
86 | "bv_tvs TvsNil = []" |
|
87 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
|
88 | "bv_cvs CvsNil = []" |
|
89 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
|
90 |
|
91 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
|
92 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
|
93 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
|
94 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
|
95 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts |
|
96 |
|
97 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_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts |
|
98 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_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros |
|
99 |
|
100 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
|
101 unfolding fresh_star_def Ball_def |
|
102 by auto (simp_all add: fresh_minus_perm) |
|
103 |
|
104 primrec permute_bv_vs_raw |
|
105 where "permute_bv_vs_raw p VsNil_raw = VsNil_raw" |
|
106 | "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)" |
|
107 primrec permute_bv_cvs_raw |
|
108 where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw" |
|
109 | "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)" |
|
110 primrec permute_bv_tvs_raw |
|
111 where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw" |
|
112 | "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)" |
|
113 primrec permute_bv_raw |
|
114 where "permute_bv_raw p (Kpat_raw c l1 l2 l3) = |
|
115 Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)" |
|
116 |
|
117 quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars" |
|
118 is "permute_bv_vs_raw" |
|
119 quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars" |
|
120 is "permute_bv_cvs_raw" |
|
121 quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars" |
|
122 is "permute_bv_tvs_raw" |
|
123 quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat" |
|
124 is "permute_bv_raw" |
|
125 |
|
126 lemma rsp_pre: |
|
127 "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)" |
|
128 "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)" |
|
129 "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)" |
|
130 apply (erule_tac [!] alpha_inducts) |
|
131 apply simp_all |
|
132 apply (rule_tac [!] alpha_intros) |
|
133 apply simp_all |
|
134 done |
|
135 |
|
136 lemma [quot_respect]: |
|
137 "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw" |
|
138 "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw" |
|
139 "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw" |
|
140 "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw" |
|
141 apply (simp_all add: rsp_pre) |
|
142 apply clarify |
|
143 apply (erule_tac alpha_inducts) |
|
144 apply (simp_all) |
|
145 apply (rule alpha_intros) |
|
146 apply (simp_all add: rsp_pre) |
|
147 done |
|
148 |
|
149 thm permute_bv_raw.simps[no_vars] |
|
150 permute_bv_vs_raw.simps[quot_lifted] |
|
151 permute_bv_cvs_raw.simps[quot_lifted] |
|
152 permute_bv_tvs_raw.simps[quot_lifted] |
|
153 |
|
154 lemma permute_bv_pre: |
|
155 "permute_bv p (Kpat c l1 l2 l3) = |
|
156 Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)" |
|
157 by (lifting permute_bv_raw.simps) |
|
158 |
|
159 lemmas permute_bv[simp] = |
|
160 permute_bv_pre |
|
161 permute_bv_vs_raw.simps[quot_lifted] |
|
162 permute_bv_cvs_raw.simps[quot_lifted] |
|
163 permute_bv_tvs_raw.simps[quot_lifted] |
|
164 |
|
165 lemma perm_bv1: |
|
166 "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)" |
|
167 "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)" |
|
168 "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)" |
|
169 apply(induct b rule: inducts(12)) |
|
170 apply(rule TrueI) |
|
171 apply(simp_all add:permute_bv eqvts) |
|
172 apply(induct c rule: inducts(11)) |
|
173 apply(rule TrueI) |
|
174 apply(simp_all add:permute_bv eqvts) |
|
175 apply(induct d rule: inducts(10)) |
|
176 apply(rule TrueI) |
|
177 apply(simp_all add:permute_bv eqvts) |
|
178 done |
|
179 |
|
180 lemma perm_bv2: |
|
181 "p \<bullet> bv l = bv (permute_bv p l)" |
|
182 apply(induct l rule: inducts(9)) |
|
183 apply(rule TrueI) |
|
184 apply(simp_all add:permute_bv) |
|
185 apply(simp add: perm_bv1[symmetric]) |
|
186 apply(simp add: eqvts) |
|
187 done |
|
188 |
|
189 lemma alpha_perm_bn1: |
|
190 " alpha_bv_tvs tvars (permute_bv_tvs q tvars)" |
|
191 "alpha_bv_cvs cvars (permute_bv_cvs q cvars)" |
|
192 "alpha_bv_vs vars (permute_bv_vs q vars)" |
|
193 apply(induct tvars rule: inducts(11)) |
|
194 apply(simp_all add:permute_bv eqvts eq_iff) |
|
195 apply(induct cvars rule: inducts(12)) |
|
196 apply(simp_all add:permute_bv eqvts eq_iff) |
|
197 apply(induct vars rule: inducts(10)) |
|
198 apply(simp_all add:permute_bv eqvts eq_iff) |
|
199 done |
|
200 |
|
201 lemma alpha_perm_bn: |
|
202 "alpha_bv pat (permute_bv q pat)" |
|
203 apply(induct pat rule: inducts(9)) |
|
204 apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) |
|
205 done |
|
206 |
|
207 lemma ACons_subst: |
|
208 "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
|
209 apply (simp only: eq_iff) |
|
210 apply (rule_tac x="q" in exI) |
|
211 apply (simp add: alphas) |
|
212 apply (simp add: perm_bv2[symmetric]) |
|
213 apply (simp add: eqvts[symmetric]) |
|
214 apply (simp add: supp_abs) |
|
215 apply (simp add: fv_supp) |
|
216 apply (simp add: alpha_perm_bn) |
|
217 apply (rule supp_perm_eq[symmetric]) |
|
218 apply (subst supp_finite_atom_set) |
|
219 apply (rule finite_Diff) |
|
220 apply (simp add: finite_supp) |
|
221 apply (assumption) |
|
222 done |
|
223 |
|
224 lemma permute_bv_zero1: |
|
225 "permute_bv_cvs 0 b = b" |
|
226 "permute_bv_tvs 0 c = c" |
|
227 "permute_bv_vs 0 d = d" |
|
228 apply(induct b rule: inducts(12)) |
|
229 apply(rule TrueI) |
|
230 apply(simp_all add:permute_bv eqvts) |
|
231 apply(induct c rule: inducts(11)) |
|
232 apply(rule TrueI) |
|
233 apply(simp_all add:permute_bv eqvts) |
|
234 apply(induct d rule: inducts(10)) |
|
235 apply(rule TrueI) |
|
236 apply(simp_all add:permute_bv eqvts) |
|
237 done |
|
238 |
|
239 lemma permute_bv_zero2: |
|
240 "permute_bv 0 a = a" |
|
241 apply(induct a rule: inducts(9)) |
|
242 apply(rule TrueI) |
|
243 apply(simp_all add:permute_bv eqvts permute_bv_zero1) |
|
244 done |
|
245 |
|
246 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x" |
|
247 apply (induct x rule: inducts(11)) |
|
248 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
249 apply (simp_all add: eq_iff fresh_star_union) |
|
250 apply (subst supp_perm_eq) |
|
251 apply (simp_all add: fv_supp) |
|
252 done |
|
253 |
|
254 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x" |
|
255 apply (induct x rule: inducts(12)) |
|
256 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
257 apply (simp_all add: eq_iff fresh_star_union) |
|
258 apply (subst supp_perm_eq) |
|
259 apply (simp_all add: fv_supp) |
|
260 done |
|
261 |
|
262 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x" |
|
263 apply (induct x rule: inducts(10)) |
|
264 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
265 apply (simp_all add: eq_iff fresh_star_union) |
|
266 apply (subst supp_perm_eq) |
|
267 apply (simp_all add: fv_supp) |
|
268 done |
|
269 |
|
270 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x" |
|
271 apply (induct x rule: inducts(9)) |
|
272 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
273 apply (simp_all add: eq_iff fresh_star_union) |
|
274 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3) |
|
275 apply (simp add: eqvts) |
|
276 done |
|
277 |
|
278 lemma fin1: "finite (fv_bv_tvs x)" |
|
279 apply (induct x rule: inducts(11)) |
|
280 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
281 apply (simp_all add: fv_supp finite_supp) |
|
282 done |
|
283 |
|
284 lemma fin2: "finite (fv_bv_cvs x)" |
|
285 apply (induct x rule: inducts(12)) |
|
286 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
287 apply (simp_all add: fv_supp finite_supp) |
|
288 done |
|
289 |
|
290 lemma fin3: "finite (fv_bv_vs x)" |
|
291 apply (induct x rule: inducts(10)) |
|
292 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
293 apply (simp_all add: fv_supp finite_supp) |
|
294 done |
|
295 |
|
296 lemma fin_fv_bv: "finite (fv_bv x)" |
|
297 apply (induct x rule: inducts(9)) |
|
298 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
299 apply (simp add: fin1 fin2 fin3) |
|
300 done |
|
301 |
|
302 lemma finb1: "finite (set (bv_tvs x))" |
|
303 apply (induct x rule: inducts(11)) |
|
304 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
305 apply (simp_all add: fv_supp finite_supp) |
|
306 done |
|
307 |
|
308 lemma finb2: "finite (set (bv_cvs x))" |
|
309 apply (induct x rule: inducts(12)) |
|
310 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
311 apply (simp_all add: fv_supp finite_supp) |
|
312 done |
|
313 |
|
314 lemma finb3: "finite (set (bv_vs x))" |
|
315 apply (induct x rule: inducts(10)) |
|
316 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
317 apply (simp_all add: fv_supp finite_supp) |
|
318 done |
|
319 |
|
320 lemma fin_bv: "finite (set (bv x))" |
|
321 apply (induct x rule: inducts(9)) |
|
322 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
323 apply (simp add: finb1 finb2 finb3) |
|
324 done |
|
325 |
|
326 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct |
|
327 |
|
328 lemma strong_induction_principle: |
|
329 assumes a01: "\<And>b. P1 b KStar" |
|
330 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
|
331 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
|
332 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
|
333 and a05: "\<And>string b. P3 b (TC string)" |
|
334 and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)" |
|
335 and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)" |
|
336 and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk> |
|
337 \<Longrightarrow> P3 b (TAll tvar tkind ty)" |
|
338 and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)" |
|
339 and a10: "\<And>b. P4 b TsNil" |
|
340 and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)" |
|
341 and a12: "\<And>string b. P5 b (CVar string)" |
|
342 and a12a:"\<And>str b. P5 b (CConst str)" |
|
343 and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)" |
|
344 and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)" |
|
345 and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk> |
|
346 \<Longrightarrow> P5 b (CAll tvar ckind co)" |
|
347 and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)" |
|
348 and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)" |
|
349 and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)" |
|
350 and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)" |
|
351 and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)" |
|
352 and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)" |
|
353 and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)" |
|
354 and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)" |
|
355 and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)" |
|
356 and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)" |
|
357 and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)" |
|
358 and a25: "\<And>b. P6 b CsNil" |
|
359 and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)" |
|
360 and a27: "\<And>var b. P7 b (Var var)" |
|
361 and a28: "\<And>string b. P7 b (K string)" |
|
362 and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
|
363 \<Longrightarrow> P7 b (LAMT tvar tkind trm)" |
|
364 and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
|
365 \<Longrightarrow> P7 b (LAMC tvar ckind trm)" |
|
366 and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)" |
|
367 and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)" |
|
368 and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)" |
|
369 and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)" |
|
370 and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk> |
|
371 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
|
372 and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)" |
|
373 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
|
374 and a37: "\<And>b. P8 b ANil" |
|
375 and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk> |
|
376 \<Longrightarrow> P8 b (ACons pat trm assoc_lst)" |
|
377 and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk> |
|
378 \<Longrightarrow> P9 b (Kpat string tvars cvars vars)" |
|
379 and a40: "\<And>b. P10 b VsNil" |
|
380 and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)" |
|
381 and a42: "\<And>b. P11 b TvsNil" |
|
382 and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk> |
|
383 \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)" |
|
384 and a44: "\<And>b. P12 b CvsNil" |
|
385 and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk> |
|
386 \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)" |
|
387 shows "P1 (a :: 'a :: pt) tkind \<and> |
|
388 P2 (b :: 'b :: pt) ckind \<and> |
|
389 P3 (c :: 'c :: {pt,fs}) ty \<and> |
|
390 P4 (d :: 'd :: pt) ty_lst \<and> |
|
391 P5 (e :: 'e :: {pt,fs}) co \<and> |
|
392 P6 (f :: 'f :: pt) co_lst \<and> |
|
393 P7 (g :: 'g :: {pt,fs}) trm \<and> |
|
394 P8 (h :: 'h :: {pt,fs}) assoc_lst \<and> |
|
395 P9 (i :: 'i :: pt) pat \<and> |
|
396 P10 (j :: 'j :: pt) vars \<and> |
|
397 P11 (k :: 'k :: pt) tvars \<and> |
|
398 P12 (l :: 'l :: pt) cvars" |
|
399 proof - |
|
400 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_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))" |
|
401 apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts) |
|
402 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
|
403 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
|
404 |
|
405 (* GOAL1 *) |
|
406 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> |
|
407 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
|
408 apply clarify |
|
409 apply (simp only: perm) |
|
410 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
|
411 and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
|
412 apply (simp only: eq_iff) |
|
413 apply (rule_tac x="-pa" in exI) |
|
414 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
415 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
|
416 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
|
417 apply (simp add: eqvts) |
|
418 apply (simp add: eqvts[symmetric]) |
|
419 apply (rule conjI) |
|
420 apply (rule supp_perm_eq) |
|
421 apply (simp add: eqvts) |
|
422 apply (subst supp_finite_atom_set) |
|
423 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
424 apply (simp add: eqvts) |
|
425 apply (simp add: eqvts) |
|
426 apply (subst supp_perm_eq) |
|
427 apply (subst supp_finite_atom_set) |
|
428 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
429 apply (simp add: eqvts) |
|
430 apply assumption |
|
431 apply (simp add: fresh_star_minus_perm) |
|
432 apply (rule a08) |
|
433 apply simp |
|
434 apply(rotate_tac 1) |
|
435 apply(erule_tac x="(pa + p)" in allE) |
|
436 apply simp |
|
437 apply (simp add: eqvts eqvts_raw) |
|
438 apply (rule at_set_avoiding2_atom) |
|
439 apply (simp add: finite_supp) |
|
440 apply (simp add: finite_supp) |
|
441 apply (simp add: fresh_def) |
|
442 apply (simp only: supp_abs eqvts) |
|
443 apply blast |
|
444 |
|
445 (* GOAL2 *) |
|
446 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and> |
|
447 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)") |
|
448 apply clarify |
|
449 apply (simp only: perm) |
|
450 apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)" |
|
451 and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
|
452 apply (simp only: eq_iff) |
|
453 apply (rule_tac x="-pa" in exI) |
|
454 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
455 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}" |
|
456 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst) |
|
457 apply (simp add: eqvts) |
|
458 apply (simp add: eqvts[symmetric]) |
|
459 apply (rule conjI) |
|
460 apply (rule supp_perm_eq) |
|
461 apply (simp add: eqvts) |
|
462 apply (subst supp_finite_atom_set) |
|
463 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
464 apply (simp add: eqvts) |
|
465 apply (simp add: eqvts) |
|
466 apply (subst supp_perm_eq) |
|
467 apply (subst supp_finite_atom_set) |
|
468 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
469 apply (simp add: eqvts) |
|
470 apply assumption |
|
471 apply (simp add: fresh_star_minus_perm) |
|
472 apply (rule a15) |
|
473 apply simp |
|
474 apply(rotate_tac 1) |
|
475 apply(erule_tac x="(pa + p)" in allE) |
|
476 apply simp |
|
477 apply (simp add: eqvts eqvts_raw) |
|
478 apply (rule at_set_avoiding2_atom) |
|
479 apply (simp add: finite_supp) |
|
480 apply (simp add: finite_supp) |
|
481 apply (simp add: fresh_def) |
|
482 apply (simp only: supp_abs eqvts) |
|
483 apply blast |
|
484 |
|
485 |
|
486 (* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *) |
|
487 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
|
488 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
|
489 apply clarify |
|
490 apply (simp only: perm) |
|
491 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
|
492 and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst) |
|
493 apply (simp only: eq_iff) |
|
494 apply (rule_tac x="-pa" in exI) |
|
495 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
496 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
|
497 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
|
498 apply (simp add: eqvts) |
|
499 apply (simp add: eqvts[symmetric]) |
|
500 apply (rule conjI) |
|
501 apply (rule supp_perm_eq) |
|
502 apply (simp add: eqvts) |
|
503 apply (subst supp_finite_atom_set) |
|
504 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
505 apply (simp add: eqvts) |
|
506 apply (simp add: eqvts) |
|
507 apply (subst supp_perm_eq) |
|
508 apply (subst supp_finite_atom_set) |
|
509 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
510 apply (simp add: eqvts) |
|
511 apply assumption |
|
512 apply (simp add: fresh_star_minus_perm) |
|
513 apply (rule a29) |
|
514 apply simp |
|
515 apply(rotate_tac 1) |
|
516 apply(erule_tac x="(pa + p)" in allE) |
|
517 apply simp |
|
518 apply (simp add: eqvts eqvts_raw) |
|
519 apply (rule at_set_avoiding2_atom) |
|
520 apply (simp add: finite_supp) |
|
521 apply (simp add: finite_supp) |
|
522 apply (simp add: fresh_def) |
|
523 apply (simp only: supp_abs eqvts) |
|
524 apply blast |
|
525 |
|
526 (* GOAL4 a copy-and-paste *) |
|
527 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and> |
|
528 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)") |
|
529 apply clarify |
|
530 apply (simp only: perm) |
|
531 apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)" |
|
532 and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
|
533 apply (simp only: eq_iff) |
|
534 apply (rule_tac x="-pa" in exI) |
|
535 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
536 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}" |
|
537 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst) |
|
538 apply (simp add: eqvts) |
|
539 apply (simp add: eqvts[symmetric]) |
|
540 apply (rule conjI) |
|
541 apply (rule supp_perm_eq) |
|
542 apply (simp add: eqvts) |
|
543 apply (subst supp_finite_atom_set) |
|
544 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
545 apply (simp add: eqvts) |
|
546 apply (simp add: eqvts) |
|
547 apply (subst supp_perm_eq) |
|
548 apply (subst supp_finite_atom_set) |
|
549 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
550 apply (simp add: eqvts) |
|
551 apply assumption |
|
552 apply (simp add: fresh_star_minus_perm) |
|
553 apply (rule a30) |
|
554 apply simp |
|
555 apply(rotate_tac 1) |
|
556 apply(erule_tac x="(pa + p)" in allE) |
|
557 apply simp |
|
558 apply (simp add: eqvts eqvts_raw) |
|
559 apply (rule at_set_avoiding2_atom) |
|
560 apply (simp add: finite_supp) |
|
561 apply (simp add: finite_supp) |
|
562 apply (simp add: fresh_def) |
|
563 apply (simp only: supp_abs eqvts) |
|
564 apply blast |
|
565 |
|
566 |
|
567 (* GOAL5 a copy-and-paste *) |
|
568 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
|
569 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)") |
|
570 apply clarify |
|
571 apply (simp only: perm) |
|
572 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
|
573 and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst) |
|
574 apply (simp only: eq_iff) |
|
575 apply (rule_tac x="-pa" in exI) |
|
576 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
577 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
|
578 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
|
579 apply (simp add: eqvts) |
|
580 apply (simp add: eqvts[symmetric]) |
|
581 apply (rule conjI) |
|
582 apply (rule supp_perm_eq) |
|
583 apply (simp add: eqvts) |
|
584 apply (subst supp_finite_atom_set) |
|
585 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
586 apply (simp add: eqvts) |
|
587 apply (simp add: eqvts) |
|
588 apply (subst supp_perm_eq) |
|
589 apply (subst supp_finite_atom_set) |
|
590 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
591 apply (simp add: eqvts) |
|
592 apply assumption |
|
593 apply (simp add: fresh_star_minus_perm) |
|
594 apply (rule a32) |
|
595 apply simp |
|
596 apply(rotate_tac 1) |
|
597 apply(erule_tac x="(pa + p)" in allE) |
|
598 apply simp |
|
599 apply (simp add: eqvts eqvts_raw) |
|
600 apply (rule at_set_avoiding2_atom) |
|
601 apply (simp add: finite_supp) |
|
602 apply (simp add: finite_supp) |
|
603 apply (simp add: fresh_def) |
|
604 apply (simp only: supp_abs eqvts) |
|
605 apply blast |
|
606 |
|
607 |
|
608 (* GOAL6 a copy-and-paste *) |
|
609 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
|
610 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)") |
|
611 apply clarify |
|
612 apply (simp only: perm) |
|
613 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
|
614 and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst) |
|
615 apply (simp only: eq_iff) |
|
616 apply (rule_tac x="-pa" in exI) |
|
617 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
618 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
|
619 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
|
620 apply (simp add: eqvts) |
|
621 apply (simp add: eqvts[symmetric]) |
|
622 apply (rule conjI) |
|
623 apply (rule supp_perm_eq) |
|
624 apply (simp add: eqvts) |
|
625 apply (subst supp_finite_atom_set) |
|
626 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
627 apply (simp add: eqvts) |
|
628 apply (simp add: eqvts) |
|
629 apply (subst supp_perm_eq) |
|
630 apply (subst supp_finite_atom_set) |
|
631 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
632 apply (simp add: eqvts) |
|
633 apply assumption |
|
634 apply (simp add: fresh_star_minus_perm) |
|
635 apply (rule a34) |
|
636 apply simp |
|
637 apply simp |
|
638 apply(rotate_tac 2) |
|
639 apply(erule_tac x="(pa + p)" in allE) |
|
640 apply simp |
|
641 apply (simp add: eqvts eqvts_raw) |
|
642 apply (rule at_set_avoiding2_atom) |
|
643 apply (simp add: finite_supp) |
|
644 apply (simp add: finite_supp) |
|
645 apply (simp add: fresh_def) |
|
646 apply (simp only: supp_abs eqvts) |
|
647 apply blast |
|
648 |
|
649 (* MAIN ACons Goal *) |
|
650 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and> |
|
651 supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
|
652 apply clarify |
|
653 apply (simp only: perm eqvts) |
|
654 apply (subst ACons_subst) |
|
655 apply assumption |
|
656 apply (rule a38) |
|
657 apply simp |
|
658 apply(rotate_tac 1) |
|
659 apply(erule_tac x="(pa + p)" in allE) |
|
660 apply simp |
|
661 apply simp |
|
662 apply (simp add: perm_bv2[symmetric]) |
|
663 apply (simp add: eqvts eqvts_raw) |
|
664 apply (rule at_set_avoiding2) |
|
665 apply (simp add: fin_bv) |
|
666 apply (simp add: finite_supp) |
|
667 apply (simp add: supp_abs) |
|
668 apply (simp add: finite_supp) |
|
669 apply (simp add: fresh_star_def fresh_def supp_abs eqvts) |
|
670 done |
|
671 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+) |
|
672 moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+) |
|
673 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
|
674 qed |
|
675 |
|
676 end |
|
677 |