| changeset 2044 | 695c1ed61879 |
| parent 1958 | e2e19188576e |
| child 2064 | 2725853f43b9 |
| 2043:5098771ff041 | 2044:695c1ed61879 |
|---|---|
1 theory ExCoreHaskell |
1 theory ExCoreHaskell |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* core haskell *) |
5 (* core haskell *) |
6 |
|
7 ML {* val _ = recursive := false *} |
|
8 (* this should not be an equivariance rule *) |
|
9 (* for the moment, we force it to be *) |
|
10 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} |
|
11 thm eqvts |
|
12 (*declare permute_pure[eqvt]*) |
|
13 |
6 |
14 atom_decl var |
7 atom_decl var |
15 atom_decl cvar |
8 atom_decl cvar |
16 atom_decl tvar |
9 atom_decl tvar |
17 |
10 |
18 (* there are types, coercion types and regular types list-data-structure *) |
11 (* there are types, coercion types and regular types list-data-structure *) |
19 |
12 |
20 ML {* val _ = alpha_type := AlphaLst *} |
|
21 nominal_datatype tkind = |
13 nominal_datatype tkind = |
22 KStar |
14 KStar |
23 | KFun "tkind" "tkind" |
15 | KFun "tkind" "tkind" |
24 and ckind = |
16 and ckind = |
25 CKEq "ty" "ty" |
17 CKEq "ty" "ty" |
26 and ty = |
18 and ty = |
27 TVar "tvar" |
19 TVar "tvar" |
28 | TC "string" |
20 | TC "string" |
29 | TApp "ty" "ty" |
21 | TApp "ty" "ty" |
30 | TFun "string" "ty_lst" |
22 | TFun "string" "ty_lst" |
31 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
23 | TAll tv::"tvar" "tkind" T::"ty" bind_set tv in T |
32 | TEq "ckind" "ty" |
24 | TEq "ckind" "ty" |
33 and ty_lst = |
25 and ty_lst = |
34 TsNil |
26 TsNil |
35 | TsCons "ty" "ty_lst" |
27 | TsCons "ty" "ty_lst" |
36 and co = |
28 and co = |
37 CVar "cvar" |
29 CVar "cvar" |
38 | CConst "string" |
30 | CConst "string" |
39 | CApp "co" "co" |
31 | CApp "co" "co" |
40 | CFun "string" "co_lst" |
32 | CFun "string" "co_lst" |
41 | CAll cv::"cvar" "ckind" C::"co" bind cv in C |
33 | CAll cv::"cvar" "ckind" C::"co" bind_set cv in C |
42 | CEq "ckind" "co" |
34 | CEq "ckind" "co" |
43 | CRefl "ty" |
35 | CRefl "ty" |
44 | CSym "co" |
36 | CSym "co" |
45 | CCir "co" "co" |
37 | CCir "co" "co" |
46 | CAt "co" "ty" |
38 | CAt "co" "ty" |
54 CsNil |
46 CsNil |
55 | CsCons "co" "co_lst" |
47 | CsCons "co" "co_lst" |
56 and trm = |
48 and trm = |
57 Var "var" |
49 Var "var" |
58 | K "string" |
50 | K "string" |
59 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t |
51 | LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t |
60 | LAMC cv::"cvar" "ckind" t::"trm" bind cv in t |
52 | LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t |
61 | AppT "trm" "ty" |
53 | AppT "trm" "ty" |
62 | AppC "trm" "co" |
54 | AppC "trm" "co" |
63 | Lam v::"var" "ty" t::"trm" bind v in t |
55 | Lam v::"var" "ty" t::"trm" bind_set v in t |
64 | App "trm" "trm" |
56 | App "trm" "trm" |
65 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
57 | Let x::"var" "ty" "trm" t::"trm" bind_set x in t |
66 | Case "trm" "assoc_lst" |
58 | Case "trm" "assoc_lst" |
67 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
59 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
68 and assoc_lst = |
60 and assoc_lst = |
69 ANil |
61 ANil |
70 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t |
62 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t |
91 | "bv_tvs TvsNil = []" |
83 | "bv_tvs TvsNil = []" |
92 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
93 | "bv_cvs CvsNil = []" |
85 | "bv_cvs CvsNil = []" |
94 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
95 |
87 |
96 (* |
|
97 function |
|
98 rfv_tkind_raw and rfv_ckind_raw and rfv_ty_raw and rfv_ty_lst_raw and rfv_co_raw and rfv_co_lst_raw and rfv_trm_raw and rfv_assoc_lst_raw and rfv_bv_raw and rfv_bv_vs_raw and rfv_bv_tvs_raw and rfv_bv_cvs_raw and rfv_pat_raw and rfv_vars_raw and rfv_tvars_raw and rfv_cvars_raw |
|
99 where |
|
100 "rfv_tkind_raw KStar_raw = {}" |
|
101 | "rfv_tkind_raw (KFun_raw tkind_raw1 tkind_raw2) = rfv_tkind_raw tkind_raw1 \<union> rfv_tkind_raw tkind_raw2" |
|
102 | "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2" |
|
103 | "rfv_ty_raw (TVar_raw tvar) = {atom tvar}" |
|
104 | "rfv_ty_raw (TC_raw list) = {}" |
|
105 | "rfv_ty_raw (TApp_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2" |
|
106 | "rfv_ty_raw (TFun_raw list ty_lst_raw) = rfv_ty_lst_raw ty_lst_raw" |
|
107 | "rfv_ty_raw (TAll_raw tvar tkind_raw ty_raw) = |
|
108 rfv_tkind_raw tkind_raw \<union> (rfv_ty_raw ty_raw - {atom tvar})" |
|
109 | "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \<union> rfv_ty_raw ty_raw" |
|
110 | "rfv_ty_lst_raw TsNil_raw = {}" |
|
111 | "rfv_ty_lst_raw (TsCons_raw ty_raw ty_lst_raw) = rfv_ty_raw ty_raw \<union> rfv_ty_lst_raw ty_lst_raw" |
|
112 | "rfv_co_raw (CVar_raw cvar) = {atom cvar}" |
|
113 | "rfv_co_raw (CConst_raw list) = {}" |
|
114 | "rfv_co_raw (CApp_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
115 | "rfv_co_raw (CFun_raw list co_lst_raw) = rfv_co_lst_raw co_lst_raw" |
|
116 | "rfv_co_raw (CAll_raw cvar ckind_raw co_raw) = |
|
117 rfv_ckind_raw ckind_raw \<union> (rfv_co_raw co_raw - {atom cvar})" |
|
118 | "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \<union> rfv_co_raw co_raw" |
|
119 | "rfv_co_raw (CRefl_raw ty_raw) = rfv_ty_raw ty_raw" |
|
120 | "rfv_co_raw (CSym_raw co_raw) = rfv_co_raw co_raw" |
|
121 | "rfv_co_raw (CCir_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
122 | "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \<union> rfv_ty_raw ty_raw" |
|
123 | "rfv_co_raw (CLeft_raw co_raw) = rfv_co_raw co_raw" |
|
124 | "rfv_co_raw (CRight_raw co_raw) = rfv_co_raw co_raw" |
|
125 | "rfv_co_raw (CSim_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
126 | "rfv_co_raw (CRightc_raw co_raw) = rfv_co_raw co_raw" |
|
127 | "rfv_co_raw (CLeftc_raw co_raw) = rfv_co_raw co_raw" |
|
128 | "rfv_co_raw (CCoe_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
129 | "rfv_co_lst_raw CsNil_raw = {}" |
|
130 | "rfv_co_lst_raw (CsCons_raw co_raw co_lst_raw) = rfv_co_raw co_raw \<union> rfv_co_lst_raw co_lst_raw" |
|
131 | "rfv_trm_raw (Var_raw var) = {atom var}" |
|
132 | "rfv_trm_raw (K_raw list) = {}" |
|
133 | "rfv_trm_raw (LAMT_raw tvar tkind_raw trm_raw) = |
|
134 rfv_tkind_raw tkind_raw \<union> (rfv_trm_raw trm_raw - {atom tvar})" |
|
135 | "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) = |
|
136 rfv_ckind_raw ckind_raw \<union> (rfv_trm_raw trm_raw - {atom cvar})" |
|
137 | "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw" |
|
138 | "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \<union> rfv_co_raw co_raw" |
|
139 | "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw - {atom var})" |
|
140 | "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \<union> rfv_trm_raw trm_raw2" |
|
141 | "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) = |
|
142 rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw1 \<union> (rfv_trm_raw trm_raw2 - {atom var}))" |
|
143 | "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \<union> rfv_assoc_lst_raw assoc_lst_raw" |
|
144 | "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw" |
|
145 | "rfv_assoc_lst_raw ANil_raw = {}" |
|
146 | "rfv_assoc_lst_raw (ACons_raw pat_raw trm_raw assoc_lst_raw) = |
|
147 rfv_bv_raw pat_raw \<union> (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \<union> rfv_assoc_lst_raw assoc_lst_raw)" |
|
148 | "rfv_bv_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) = |
|
149 rfv_bv_tvs_raw tvars_raw \<union> (rfv_bv_cvs_raw cvars_raw \<union> rfv_bv_vs_raw vars_raw)" |
|
150 | "rfv_bv_vs_raw VsNil_raw = {}" |
|
151 | "rfv_bv_vs_raw (VsCons_raw var ty_raw vars_raw) = rfv_ty_raw ty_raw \<union> rfv_bv_vs_raw vars_raw" |
|
152 | "rfv_bv_tvs_raw TvsNil_raw = {}" |
|
153 | "rfv_bv_tvs_raw (TvsCons_raw tvar tkind_raw tvars_raw) = |
|
154 rfv_tkind_raw tkind_raw \<union> rfv_bv_tvs_raw tvars_raw" |
|
155 | "rfv_bv_cvs_raw CvsNil_raw = {}" |
|
156 | "rfv_bv_cvs_raw (CvsCons_raw cvar ckind_raw cvars_raw) = |
|
157 rfv_ckind_raw ckind_raw \<union> rfv_bv_cvs_raw cvars_raw" |
|
158 | "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) = |
|
159 rfv_tvars_raw tvars_raw \<union> (rfv_cvars_raw cvars_raw \<union> rfv_vars_raw vars_raw)" |
|
160 | "rfv_vars_raw VsNil_raw = {}" |
|
161 | "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) = |
|
162 {atom var} \<union> (rfv_ty_raw ty_raw \<union> rfv_vars_raw vars_raw)" |
|
163 | "rfv_tvars_raw TvsNil_raw = {}" |
|
164 | "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) = |
|
165 {atom tvar} \<union> (rfv_tkind_raw tkind_raw \<union> rfv_tvars_raw tvars_raw)" |
|
166 | "rfv_cvars_raw CvsNil_raw = {}" |
|
167 | "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) = |
|
168 {atom cvar} \<union> (rfv_ckind_raw ckind_raw \<union> rfv_cvars_raw cvars_raw)" |
|
169 apply pat_completeness |
|
170 apply auto |
|
171 done |
|
172 termination |
|
173 by lexicographic_order |
|
174 *) |
|
175 |
|
176 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
88 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
177 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
178 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
179 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
91 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
180 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts |
92 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts |
211 lemma rsp_pre: |
123 lemma rsp_pre: |
212 "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)" |
124 "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)" |
213 "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)" |
125 "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)" |
214 "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)" |
126 "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)" |
215 apply (erule_tac [!] alpha_inducts) |
127 apply (erule_tac [!] alpha_inducts) |
216 apply simp_all |
128 apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps) |
217 apply (rule_tac [!] alpha_intros) |
|
218 apply simp_all |
|
219 done |
129 done |
220 |
130 |
221 lemma [quot_respect]: |
131 lemma [quot_respect]: |
222 "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw" |
132 "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw" |
223 "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw" |
133 "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw" |
250 lemma perm_bv1: |
160 lemma perm_bv1: |
251 "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)" |
161 "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)" |
252 "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)" |
162 "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)" |
253 "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)" |
163 "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)" |
254 apply(induct b rule: inducts(12)) |
164 apply(induct b rule: inducts(12)) |
255 apply(rule TrueI) |
|
256 apply(simp_all add:permute_bv eqvts) |
165 apply(simp_all add:permute_bv eqvts) |
257 apply(induct c rule: inducts(11)) |
166 apply(induct c rule: inducts(11)) |
258 apply(rule TrueI) |
|
259 apply(simp_all add:permute_bv eqvts) |
167 apply(simp_all add:permute_bv eqvts) |
260 apply(induct d rule: inducts(10)) |
168 apply(induct d rule: inducts(10)) |
261 apply(rule TrueI) |
|
262 apply(simp_all add:permute_bv eqvts) |
169 apply(simp_all add:permute_bv eqvts) |
263 done |
170 done |
264 |
171 |
265 lemma perm_bv2: |
172 lemma perm_bv2: |
266 "p \<bullet> bv l = bv (permute_bv p l)" |
173 "p \<bullet> bv l = bv (permute_bv p l)" |
267 apply(induct l rule: inducts(9)) |
174 apply(induct l rule: inducts(9)) |
268 apply(rule TrueI) |
|
269 apply(simp_all add:permute_bv) |
175 apply(simp_all add:permute_bv) |
270 apply(simp add: perm_bv1[symmetric]) |
176 apply(simp add: perm_bv1[symmetric]) |
271 apply(simp add: eqvts) |
177 apply(simp add: eqvts) |
272 done |
178 done |
273 |
179 |
274 lemma alpha_perm_bn1: |
180 lemma alpha_perm_bn1: |
275 " alpha_bv_tvs tvars (permute_bv_tvs q tvars)" |
181 "alpha_bv_tvs tvars (permute_bv_tvs q tvars)" |
276 "alpha_bv_cvs cvars (permute_bv_cvs q cvars)" |
182 "alpha_bv_cvs cvars (permute_bv_cvs q cvars)" |
277 "alpha_bv_vs vars (permute_bv_vs q vars)" |
183 "alpha_bv_vs vars (permute_bv_vs q vars)" |
278 apply(induct tvars rule: inducts(11)) |
184 apply(induct tvars rule: inducts(11)) |
279 apply(simp_all add:permute_bv eqvts eq_iff) |
185 apply(simp_all add:permute_bv eqvts eq_iff) |
280 apply(induct cvars rule: inducts(12)) |
186 apply(induct cvars rule: inducts(12)) |
290 done |
196 done |
291 |
197 |
292 lemma ACons_subst: |
198 lemma ACons_subst: |
293 "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
199 "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
294 apply (simp only: eq_iff) |
200 apply (simp only: eq_iff) |
201 apply (simp add: alpha_perm_bn) |
|
295 apply (rule_tac x="q" in exI) |
202 apply (rule_tac x="q" in exI) |
296 apply (simp add: alphas) |
203 apply (simp add: alphas) |
297 apply (simp add: perm_bv2[symmetric]) |
204 apply (simp add: perm_bv2[symmetric]) |
298 apply (simp add: eqvts[symmetric]) |
205 apply (simp add: eqvts[symmetric]) |
299 apply (simp add: supp_abs) |
206 apply (simp add: supp_abs) |
300 apply (simp add: fv_supp) |
207 apply (simp add: fv_supp) |
301 apply (simp add: alpha_perm_bn) |
|
302 apply (rule supp_perm_eq[symmetric]) |
208 apply (rule supp_perm_eq[symmetric]) |
303 apply (subst supp_finite_atom_set) |
209 apply (subst supp_finite_atom_set) |
304 apply (rule finite_Diff) |
210 apply (rule finite_Diff) |
305 apply (simp add: finite_supp) |
211 apply (simp add: finite_supp) |
306 apply (assumption) |
212 apply (assumption) |
309 lemma permute_bv_zero1: |
215 lemma permute_bv_zero1: |
310 "permute_bv_cvs 0 b = b" |
216 "permute_bv_cvs 0 b = b" |
311 "permute_bv_tvs 0 c = c" |
217 "permute_bv_tvs 0 c = c" |
312 "permute_bv_vs 0 d = d" |
218 "permute_bv_vs 0 d = d" |
313 apply(induct b rule: inducts(12)) |
219 apply(induct b rule: inducts(12)) |
314 apply(rule TrueI) |
|
315 apply(simp_all add:permute_bv eqvts) |
220 apply(simp_all add:permute_bv eqvts) |
316 apply(induct c rule: inducts(11)) |
221 apply(induct c rule: inducts(11)) |
317 apply(rule TrueI) |
|
318 apply(simp_all add:permute_bv eqvts) |
222 apply(simp_all add:permute_bv eqvts) |
319 apply(induct d rule: inducts(10)) |
223 apply(induct d rule: inducts(10)) |
320 apply(rule TrueI) |
|
321 apply(simp_all add:permute_bv eqvts) |
224 apply(simp_all add:permute_bv eqvts) |
322 done |
225 done |
323 |
226 |
324 lemma permute_bv_zero2: |
227 lemma permute_bv_zero2: |
325 "permute_bv 0 a = a" |
228 "permute_bv 0 a = a" |
326 apply(induct a rule: inducts(9)) |
229 apply(induct a rule: inducts(9)) |
327 apply(rule TrueI) |
|
328 apply(simp_all add:permute_bv eqvts permute_bv_zero1) |
230 apply(simp_all add:permute_bv eqvts permute_bv_zero1) |
329 done |
231 done |
330 |
232 |
331 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x" |
233 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x" |
332 apply (induct x rule: inducts(11)) |
234 apply (induct x rule: inducts(11)) |
333 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
235 apply (simp_all add: eq_iff fresh_star_union) |
236 done |
|
237 |
|
238 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x" |
|
239 apply (induct x rule: inducts(12)) |
|
240 apply (rule TrueI)+ |
|
334 apply (simp_all add: eq_iff fresh_star_union) |
241 apply (simp_all add: eq_iff fresh_star_union) |
335 apply (subst supp_perm_eq) |
242 apply (subst supp_perm_eq) |
336 apply (simp_all add: fv_supp) |
243 apply (simp_all add: fv_supp) |
337 done |
244 done |
338 |
245 |
339 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x" |
246 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x" |
340 apply (induct x rule: inducts(12)) |
247 apply (induct x rule: inducts(10)) |
341 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
248 apply (rule TrueI)+ |
342 apply (simp_all add: eq_iff fresh_star_union) |
249 apply (simp_all add: fresh_star_union eq_iff) |
343 apply (subst supp_perm_eq) |
250 apply (subst supp_perm_eq) |
344 apply (simp_all add: fv_supp) |
251 apply (simp_all add: fv_supp) |
345 done |
252 done |
346 |
253 |
347 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x" |
254 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x" |
348 apply (induct x rule: inducts(10)) |
255 apply (induct x rule: inducts(9)) |
349 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
256 apply (rule TrueI)+ |
350 apply (simp_all add: eq_iff fresh_star_union) |
257 apply (simp_all add: eq_iff fresh_star_union) |
258 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3) |
|
351 apply (subst supp_perm_eq) |
259 apply (subst supp_perm_eq) |
352 apply (simp_all add: fv_supp) |
260 apply (simp_all add: fv_supp) |
353 done |
261 done |
354 |
262 |
355 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x" |
|
356 apply (induct x rule: inducts(9)) |
|
357 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
358 apply (simp_all add: eq_iff fresh_star_union) |
|
359 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3) |
|
360 apply (simp add: eqvts) |
|
361 done |
|
362 |
|
363 lemma fin1: "finite (fv_bv_tvs x)" |
263 lemma fin1: "finite (fv_bv_tvs x)" |
364 apply (induct x rule: inducts(11)) |
264 apply (induct x rule: inducts(11)) |
365 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
366 apply (simp_all add: fv_supp finite_supp) |
265 apply (simp_all add: fv_supp finite_supp) |
367 done |
266 done |
368 |
267 |
369 lemma fin2: "finite (fv_bv_cvs x)" |
268 lemma fin2: "finite (fv_bv_cvs x)" |
370 apply (induct x rule: inducts(12)) |
269 apply (induct x rule: inducts(12)) |
371 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
372 apply (simp_all add: fv_supp finite_supp) |
270 apply (simp_all add: fv_supp finite_supp) |
373 done |
271 done |
374 |
272 |
375 lemma fin3: "finite (fv_bv_vs x)" |
273 lemma fin3: "finite (fv_bv_vs x)" |
376 apply (induct x rule: inducts(10)) |
274 apply (induct x rule: inducts(10)) |
377 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
378 apply (simp_all add: fv_supp finite_supp) |
275 apply (simp_all add: fv_supp finite_supp) |
379 done |
276 done |
380 |
277 |
381 lemma fin_fv_bv: "finite (fv_bv x)" |
278 lemma fin_fv_bv: "finite (fv_bv x)" |
382 apply (induct x rule: inducts(9)) |
279 apply (induct x rule: inducts(9)) |
383 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
280 apply (rule TrueI)+ |
281 defer |
|
282 apply (rule TrueI)+ |
|
384 apply (simp add: fin1 fin2 fin3) |
283 apply (simp add: fin1 fin2 fin3) |
284 apply (rule finite_supp) |
|
385 done |
285 done |
386 |
286 |
387 lemma finb1: "finite (set (bv_tvs x))" |
287 lemma finb1: "finite (set (bv_tvs x))" |
388 apply (induct x rule: inducts(11)) |
288 apply (induct x rule: inducts(11)) |
389 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
390 apply (simp_all add: fv_supp finite_supp) |
289 apply (simp_all add: fv_supp finite_supp) |
391 done |
290 done |
392 |
291 |
393 lemma finb2: "finite (set (bv_cvs x))" |
292 lemma finb2: "finite (set (bv_cvs x))" |
394 apply (induct x rule: inducts(12)) |
293 apply (induct x rule: inducts(12)) |
395 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
396 apply (simp_all add: fv_supp finite_supp) |
294 apply (simp_all add: fv_supp finite_supp) |
397 done |
295 done |
398 |
296 |
399 lemma finb3: "finite (set (bv_vs x))" |
297 lemma finb3: "finite (set (bv_vs x))" |
400 apply (induct x rule: inducts(10)) |
298 apply (induct x rule: inducts(10)) |
401 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
402 apply (simp_all add: fv_supp finite_supp) |
299 apply (simp_all add: fv_supp finite_supp) |
403 done |
300 done |
404 |
301 |
405 lemma fin_bv: "finite (set (bv x))" |
302 lemma fin_bv: "finite (set (bv x))" |
406 apply (induct x rule: inducts(9)) |
303 apply (induct x rule: inducts(9)) |
407 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
304 apply (simp_all add: finb1 finb2 finb3) |
408 apply (simp add: finb1 finb2 finb3) |
305 done |
409 done |
|
410 |
|
411 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct |
|
412 |
306 |
413 lemma strong_induction_principle: |
307 lemma strong_induction_principle: |
414 assumes a01: "\<And>b. P1 b KStar" |
308 assumes a01: "\<And>b. P1 b KStar" |
415 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
309 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
416 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
310 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
492 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
386 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
493 apply clarify |
387 apply clarify |
494 apply (simp only: perm) |
388 apply (simp only: perm) |
495 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
389 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
496 and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
390 and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
497 apply (simp only: eq_iff) |
391 apply (simp add: eq_iff) |
498 apply (rule_tac x="-pa" in exI) |
392 apply (rule_tac x="-pa" in exI) |
499 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
393 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
500 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
394 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
501 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
395 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
502 apply (simp add: eqvts) |
396 apply (simp add: eqvts) |
532 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)") |
426 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)") |
533 apply clarify |
427 apply clarify |
534 apply (simp only: perm) |
428 apply (simp only: perm) |
535 apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)" |
429 apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)" |
536 and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
430 and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
537 apply (simp only: eq_iff) |
431 apply (simp add: eq_iff) |
538 apply (rule_tac x="-pa" in exI) |
432 apply (rule_tac x="-pa" in exI) |
539 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
433 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
540 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}" |
434 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}" |
541 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst) |
435 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst) |
542 apply (simp add: eqvts) |
436 apply (simp add: eqvts) |
573 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
467 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
574 apply clarify |
468 apply clarify |
575 apply (simp only: perm) |
469 apply (simp only: perm) |
576 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
470 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
577 and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst) |
471 and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst) |
578 apply (simp only: eq_iff) |
472 apply (simp add: eq_iff) |
579 apply (rule_tac x="-pa" in exI) |
473 apply (rule_tac x="-pa" in exI) |
580 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
474 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
581 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
475 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
582 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
476 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
583 apply (simp add: eqvts) |
477 apply (simp add: eqvts) |
613 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)") |
507 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)") |
614 apply clarify |
508 apply clarify |
615 apply (simp only: perm) |
509 apply (simp only: perm) |
616 apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)" |
510 apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)" |
617 and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
511 and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
618 apply (simp only: eq_iff) |
512 apply (simp add: eq_iff) |
619 apply (rule_tac x="-pa" in exI) |
513 apply (rule_tac x="-pa" in exI) |
620 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
514 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
621 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}" |
515 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}" |
622 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst) |
516 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst) |
623 apply (simp add: eqvts) |
517 apply (simp add: eqvts) |
654 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)") |
548 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)") |
655 apply clarify |
549 apply clarify |
656 apply (simp only: perm) |
550 apply (simp only: perm) |
657 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
551 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
658 and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst) |
552 and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst) |
659 apply (simp only: eq_iff) |
553 apply (simp add: eq_iff) |
660 apply (rule_tac x="-pa" in exI) |
554 apply (rule_tac x="-pa" in exI) |
661 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
555 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
662 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
556 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
663 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
557 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
664 apply (simp add: eqvts) |
558 apply (simp add: eqvts) |
695 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)") |
589 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)") |
696 apply clarify |
590 apply clarify |
697 apply (simp only: perm) |
591 apply (simp only: perm) |
698 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
592 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
699 and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst) |
593 and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst) |
700 apply (simp only: eq_iff) |
594 apply (simp add: eq_iff) |
701 apply (rule_tac x="-pa" in exI) |
595 apply (rule_tac x="-pa" in exI) |
702 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
596 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
703 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
597 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
704 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
598 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
705 apply (simp add: eqvts) |
599 apply (simp add: eqvts) |
758 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
652 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
759 qed |
653 qed |
760 |
654 |
761 section {* test about equivariance for alpha *} |
655 section {* test about equivariance for alpha *} |
762 |
656 |
657 (* this should not be an equivariance rule *) |
|
658 (* for the moment, we force it to be *) |
|
659 |
|
660 (*declare permute_pure[eqvt]*) |
|
661 (*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} |
|
662 |
|
763 thm eqvts |
663 thm eqvts |
764 thm eqvts_raw |
664 thm eqvts_raw |
765 |
665 |
766 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt] |
666 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt] |
767 declare alpha_gen_eqvt[eqvt] |
667 declare alpha_gen_eqvt[eqvt] |
768 |
668 |
769 equivariance alpha_tkind_raw |
669 equivariance alpha_tkind_raw |
770 |
670 |
771 thm eqvts |
671 thm eqvts |
772 thm eqvts_raw |
672 thm eqvts_raw*) |
773 |
673 |
774 end |
674 end |
775 |
675 |