1 theory LFex |
1 theory LFex |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 atom_decl ident |
6 atom_decl ident |
7 |
7 |
8 datatype kind = |
8 datatype kind = |
9 Type |
9 Type |
10 | KPi "ty" "name" "kind" |
10 | KPi "ty" "name" "kind" |
11 and ty = |
11 and ty = |
12 TConst "ident" |
12 TConst "ident" |
13 | TApp "ty" "trm" |
13 | TApp "ty" "trm" |
14 | TPi "ty" "name" "ty" |
14 | TPi "ty" "name" "ty" |
15 and trm = |
15 and trm = |
16 Const "ident" |
16 Const "ident" |
17 | Var "name" |
17 | Var "name" |
18 | App "trm" "trm" |
18 | App "trm" "trm" |
19 | Lam "ty" "name" "trm" |
19 | Lam "ty" "name" "trm" |
20 |
20 print_theorems |
21 fun |
21 |
|
22 primrec |
22 rfv_kind :: "kind \<Rightarrow> atom set" |
23 rfv_kind :: "kind \<Rightarrow> atom set" |
23 and rfv_ty :: "ty \<Rightarrow> atom set" |
24 and rfv_ty :: "ty \<Rightarrow> atom set" |
24 and rfv_trm :: "trm \<Rightarrow> atom set" |
25 and rfv_trm :: "trm \<Rightarrow> atom set" |
25 where |
26 where |
26 "rfv_kind (Type) = {}" |
27 "rfv_kind (Type) = {}" |
27 | "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})" |
28 | "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})" |
28 | "rfv_ty (TConst i) = {}" |
29 | "rfv_ty (TConst i) = {atom i}" |
29 | "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)" |
30 | "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)" |
30 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})" |
31 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})" |
31 | "rfv_trm (Const i) = {}" |
32 | "rfv_trm (Const i) = {atom i}" |
32 | "rfv_trm (Var x) = {atom x}" |
33 | "rfv_trm (Var x) = {atom x}" |
33 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)" |
34 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)" |
34 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})" |
35 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})" |
|
36 print_theorems |
35 |
37 |
36 instantiation kind and ty and trm :: pt |
38 instantiation kind and ty and trm :: pt |
37 begin |
39 begin |
38 |
40 |
39 primrec |
41 primrec |
82 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')" |
84 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')" |
83 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)" |
85 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)" |
84 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)" |
86 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)" |
85 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')" |
87 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')" |
86 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')" |
88 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')" |
|
89 |
|
90 (* |
|
91 function(sequential) |
|
92 akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100) |
|
93 and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100) |
|
94 and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100) |
|
95 where |
|
96 a1: "(Type) \<approx>ki (Type) = True" |
|
97 | a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))" |
|
98 | "_ \<approx>ki _ = False" |
|
99 | a3: "(TConst i) \<approx>ty (TConst j) = (i = j)" |
|
100 | a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')" |
|
101 | a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))" |
|
102 | "_ \<approx>ty _ = False" |
|
103 | a6: "(Const i) \<approx>tr (Const j) = (i = j)" |
|
104 | a7: "(Var x) \<approx>tr (Var y) = (x = y)" |
|
105 | a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')" |
|
106 | a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))" |
|
107 | "_ \<approx>tr _ = False" |
|
108 apply (pat_completeness) |
|
109 apply simp_all |
|
110 done |
|
111 termination |
|
112 by (size_change) |
|
113 *) |
|
114 |
|
115 lemma akind_aty_atrm_inj: |
|
116 "(Type) \<approx>ki (Type) = True" |
|
117 "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))" |
|
118 "(TConst i) \<approx>ty (TConst j) = (i = j)" |
|
119 "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')" |
|
120 "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))" |
|
121 "(Const i) \<approx>tr (Const j) = (i = j)" |
|
122 "(Var x) \<approx>tr (Var y) = (x = y)" |
|
123 "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')" |
|
124 "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))" |
|
125 apply - |
|
126 apply (simp add: akind_aty_atrm.intros) |
|
127 |
|
128 apply rule apply (erule akind.cases) apply simp apply blast |
|
129 apply (simp only: akind_aty_atrm.intros) |
|
130 |
|
131 apply rule apply (erule aty.cases) apply simp apply simp apply simp |
|
132 apply (simp only: akind_aty_atrm.intros) |
|
133 |
|
134 apply rule apply (erule aty.cases) apply simp apply simp apply simp |
|
135 apply (simp only: akind_aty_atrm.intros) |
|
136 |
|
137 apply rule apply (erule aty.cases) apply simp apply simp apply blast |
|
138 apply (simp only: akind_aty_atrm.intros) |
|
139 |
|
140 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
|
141 apply (simp only: akind_aty_atrm.intros) |
|
142 |
|
143 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
|
144 apply (simp only: akind_aty_atrm.intros) |
|
145 |
|
146 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
|
147 apply (simp only: akind_aty_atrm.intros) |
|
148 |
|
149 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
|
150 apply (simp only: akind_aty_atrm.intros) |
|
151 done |
|
152 |
|
153 (* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *) |
|
154 |
|
155 lemma rfv_eqvt[eqvt]: |
|
156 "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))" |
|
157 "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))" |
|
158 "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))" |
|
159 apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts) |
|
160 apply(simp_all add: union_eqvt Diff_eqvt) |
|
161 apply(simp_all add: permute_set_eq atom_eqvt) |
|
162 done |
|
163 |
|
164 lemma alpha_eqvt: |
|
165 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
|
166 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
|
167 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
|
168 apply(induct rule: akind_aty_atrm.inducts) |
|
169 apply (simp_all add: akind_aty_atrm.intros) |
|
170 apply(rule a2) |
|
171 apply simp |
|
172 apply(erule conjE) |
|
173 apply(erule exE) |
|
174 apply(erule conjE) |
|
175 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
176 apply(rule conjI) |
|
177 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
178 apply(simp add: eqvts atom_eqvt) |
|
179 apply(rule conjI) |
|
180 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
181 apply(simp add: eqvts atom_eqvt) |
|
182 apply(simp add: permute_eqvt[symmetric]) |
|
183 apply(rule a5) |
|
184 apply simp |
|
185 apply(erule conjE) |
|
186 apply(erule exE) |
|
187 apply(erule conjE) |
|
188 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
189 apply(rule conjI) |
|
190 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
191 apply(simp add: eqvts atom_eqvt) |
|
192 apply(rule conjI) |
|
193 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
194 apply(simp add: eqvts atom_eqvt) |
|
195 apply(simp add: permute_eqvt[symmetric]) |
|
196 apply(rule a9) |
|
197 apply simp |
|
198 apply(erule conjE) |
|
199 apply(erule exE) |
|
200 apply(erule conjE) |
|
201 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
202 apply(rule conjI) |
|
203 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
204 apply(simp add: eqvts atom_eqvt) |
|
205 apply(rule conjI) |
|
206 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
207 apply(simp add: eqvts atom_eqvt) |
|
208 apply(simp add: permute_eqvt[symmetric]) |
|
209 done |
87 |
210 |
88 lemma al_refl: |
211 lemma al_refl: |
89 fixes K::"kind" |
212 fixes K::"kind" |
90 and A::"ty" |
213 and A::"ty" |
91 and M::"trm" |
214 and M::"trm" |
195 |
317 |
196 lemma perm_rsp[quot_respect]: |
318 lemma perm_rsp[quot_respect]: |
197 "(op = ===> akind ===> akind) permute permute" |
319 "(op = ===> akind ===> akind) permute permute" |
198 "(op = ===> aty ===> aty) permute permute" |
320 "(op = ===> aty ===> aty) permute permute" |
199 "(op = ===> atrm ===> atrm) permute permute" |
321 "(op = ===> atrm ===> atrm) permute permute" |
200 apply simp_all |
322 by (simp_all add:alpha_eqvt) |
201 sorry (* by eqvt *) |
323 |
202 |
|
203 lemma kpi_rsp[quot_respect]: |
|
204 "(aty ===> op = ===> akind ===> akind) KPi KPi" |
|
205 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry |
|
206 lemma tconst_rsp[quot_respect]: |
324 lemma tconst_rsp[quot_respect]: |
207 "(op = ===> aty) TConst TConst" |
325 "(op = ===> aty) TConst TConst" |
208 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
326 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
209 lemma tapp_rsp[quot_respect]: |
327 lemma tapp_rsp[quot_respect]: |
210 "(aty ===> atrm ===> aty) TApp TApp" |
328 "(aty ===> atrm ===> aty) TApp TApp" |
211 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
329 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
212 lemma tpi_rsp[quot_respect]: |
|
213 "(aty ===> op = ===> aty ===> aty) TPi TPi" |
|
214 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry |
|
215 lemma var_rsp[quot_respect]: |
330 lemma var_rsp[quot_respect]: |
216 "(op = ===> atrm) Var Var" |
331 "(op = ===> atrm) Var Var" |
217 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
332 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
218 lemma app_rsp[quot_respect]: |
333 lemma app_rsp[quot_respect]: |
219 "(atrm ===> atrm ===> atrm) App App" |
334 "(atrm ===> atrm ===> atrm) App App" |
220 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
335 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
221 lemma const_rsp[quot_respect]: |
336 lemma const_rsp[quot_respect]: |
222 "(op = ===> atrm) Const Const" |
337 "(op = ===> atrm) Const Const" |
223 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
338 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
|
339 |
|
340 lemma kpi_rsp[quot_respect]: |
|
341 "(aty ===> op = ===> akind ===> akind) KPi KPi" |
|
342 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) |
|
343 apply (rule a2) apply simp |
|
344 apply (rule_tac x="0" in exI) |
|
345 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv) |
|
346 done |
|
347 |
|
348 lemma tpi_rsp[quot_respect]: |
|
349 "(aty ===> op = ===> aty ===> aty) TPi TPi" |
|
350 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) |
|
351 apply (rule a5) apply simp |
|
352 apply (rule_tac x="0" in exI) |
|
353 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv) |
|
354 done |
224 lemma lam_rsp[quot_respect]: |
355 lemma lam_rsp[quot_respect]: |
225 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" |
356 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" |
226 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry |
357 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) |
|
358 apply (rule a9) apply simp |
|
359 apply (rule_tac x="0" in exI) |
|
360 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv) |
|
361 done |
|
362 |
227 lemma rfv_ty_rsp[quot_respect]: |
363 lemma rfv_ty_rsp[quot_respect]: |
228 "(aty ===> op =) rfv_ty rfv_ty" |
364 "(aty ===> op =) rfv_ty rfv_ty" |
229 by (simp add: alpha_rfv) |
365 by (simp add: alpha_rfv) |
230 lemma rfv_kind_rsp[quot_respect]: |
366 lemma rfv_kind_rsp[quot_respect]: |
231 "(akind ===> op =) rfv_kind rfv_kind" |
367 "(akind ===> op =) rfv_kind rfv_kind" |
232 by (simp add: alpha_rfv) |
368 by (simp add: alpha_rfv) |
233 lemma rfv_trm_rsp[quot_respect]: |
369 lemma rfv_trm_rsp[quot_respect]: |
234 "(atrm ===> op =) rfv_trm rfv_trm" |
370 "(atrm ===> op =) rfv_trm rfv_trm" |
235 by (simp add: alpha_rfv) |
371 by (simp add: alpha_rfv) |
236 |
372 |
237 thm akind_aty_atrm.induct |
|
238 thm kind_ty_trm.induct |
|
239 |
|
240 lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
373 lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
241 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
374 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
242 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
375 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
243 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
376 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
244 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
377 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
245 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm" |
378 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm" |
246 by (lifting kind_ty_trm.induct) |
379 by (lifting kind_ty_trm.induct) |
247 |
380 |
|
381 thm kind_ty_trm.inducts |
|
382 |
|
383 lemma KIND_TY_TRM_inducts: |
|
384 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
|
385 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
|
386 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
|
387 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
|
388 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
|
389 \<Longrightarrow> P10 kind" |
|
390 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
|
391 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
|
392 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
|
393 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
|
394 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
|
395 \<Longrightarrow> P20 ty" |
|
396 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
|
397 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
|
398 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
|
399 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
|
400 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
|
401 \<Longrightarrow> P30 trm" |
|
402 by (lifting kind_ty_trm.inducts) |
|
403 |
248 instantiation KIND and TY and TRM :: pt |
404 instantiation KIND and TY and TRM :: pt |
249 begin |
405 begin |
250 |
406 |
251 quotient_definition |
407 quotient_definition |
252 "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND" |
408 "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND" |
316 \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> |
472 \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> |
317 (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk> |
473 (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk> |
318 \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk> |
474 \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk> |
319 \<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and> |
475 \<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and> |
320 (x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)" |
476 (x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)" |
321 apply (lifting akind_aty_atrm.induct) |
477 by (lifting akind_aty_atrm.induct) |
322 done |
478 |
|
479 lemma AKIND_ATY_ATRM_inducts: |
|
480 "\<lbrakk>x10 = x20; P10 TYP TYP; |
|
481 \<And>A A' K x K' x'. |
|
482 \<lbrakk>A = A'; P20 A A'; |
|
483 \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> |
|
484 (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk> |
|
485 \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K'); |
|
486 \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j); |
|
487 \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M'); |
|
488 \<And>A A' B x B' x'. |
|
489 \<lbrakk>A = A'; P20 A A'; |
|
490 \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> |
|
491 (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk> |
|
492 \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B'); |
|
493 \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y); |
|
494 \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N'); |
|
495 \<And>A A' M x M' x'. |
|
496 \<lbrakk>A = A'; P20 A A'; |
|
497 \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> |
|
498 (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk> |
|
499 \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk> |
|
500 \<Longrightarrow> P10 x10 x20" |
|
501 "\<lbrakk>x30 = x40; P10 TYP TYP; |
|
502 \<And>A A' K x K' x'. |
|
503 \<lbrakk>A = A'; P20 A A'; |
|
504 \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> |
|
505 (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk> |
|
506 \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K'); |
|
507 \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j); |
|
508 \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M'); |
|
509 \<And>A A' B x B' x'. |
|
510 \<lbrakk>A = A'; P20 A A'; |
|
511 \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> |
|
512 (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk> |
|
513 \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B'); |
|
514 \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y); |
|
515 \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N'); |
|
516 \<And>A A' M x M' x'. |
|
517 \<lbrakk>A = A'; P20 A A'; |
|
518 \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> |
|
519 (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk> |
|
520 \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk> |
|
521 \<Longrightarrow> P20 x30 x40" |
|
522 "\<lbrakk>x50 = x60; P10 TYP TYP; |
|
523 \<And>A A' K x K' x'. |
|
524 \<lbrakk>A = A'; P20 A A'; |
|
525 \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> |
|
526 (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk> |
|
527 \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K'); |
|
528 \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j); |
|
529 \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M'); |
|
530 \<And>A A' B x B' x'. |
|
531 \<lbrakk>A = A'; P20 A A'; |
|
532 \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> |
|
533 (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk> |
|
534 \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B'); |
|
535 \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y); |
|
536 \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N'); |
|
537 \<And>A A' M x M' x'. |
|
538 \<lbrakk>A = A'; P20 A A'; |
|
539 \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> |
|
540 (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk> |
|
541 \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk> |
|
542 \<Longrightarrow> P30 x50 x60" |
|
543 by (lifting akind_aty_atrm.inducts) |
|
544 |
|
545 lemma KIND_TY_TRM_INJECT: |
|
546 "(TYP) = (TYP) = True" |
|
547 "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. (fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> (fv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) = K' \<and> (pi \<bullet> x) = x')))" |
|
548 "(TCONST i) = (TCONST j) = (i = j)" |
|
549 "(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = M')" |
|
550 "(TPI A x B) = (TPI A' x' B') = ((A = A') \<and> (\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> (fv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) = B' \<and> (pi \<bullet> x) = x'))" |
|
551 "(CONS i) = (CONS j) = (i = j)" |
|
552 "(VAR x) = (VAR y) = (x = y)" |
|
553 "(APP M N) = (APP M' N') = (M = M' \<and> N = N')" |
|
554 "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> (fv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) = M' \<and> (pi \<bullet> x) = x'))" |
|
555 by (lifting akind_aty_atrm_inj) |
|
556 |
|
557 lemma fv_kind_ty_trm: |
|
558 "fv_kind TYP = {}" |
|
559 "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})" |
|
560 "fv_ty (TCONST i) = {atom i}" |
|
561 "fv_ty (TAPP A M) = fv_ty A \<union> fv_trm M" |
|
562 "fv_ty (TPI A x B) = fv_ty A \<union> (fv_ty B - {atom x})" |
|
563 "fv_trm (CONS i) = {atom i}" |
|
564 "fv_trm (VAR x) = {atom x}" |
|
565 "fv_trm (APP M N) = fv_trm M \<union> fv_trm N" |
|
566 "fv_trm (LAM A x M) = fv_ty A \<union> (fv_trm M - {atom x})" |
|
567 by(lifting rfv_kind_rfv_ty_rfv_trm.simps) |
|
568 |
|
569 lemma fv_eqvt: |
|
570 "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)" |
|
571 "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)" |
|
572 "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)" |
|
573 by(lifting rfv_eqvt) |
|
574 |
|
575 lemma supp_fv: |
|
576 "fv_kind t1 = supp t1" |
|
577 "fv_ty t2 = supp t2" |
|
578 "fv_trm t3 = supp t3" |
|
579 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts) |
|
580 apply (simp_all add: fv_kind_ty_trm) |
|
581 apply (simp_all add: supp_def) |
|
582 sorry |
|
583 |
|
584 lemma |
|
585 "(supp ((a \<rightleftharpoons> b) \<bullet> (K::KIND)) - {atom ((a \<rightleftharpoons> b) \<bullet> (x::name))} = supp K - {atom x} \<longrightarrow> |
|
586 (a \<rightleftharpoons> b) \<bullet> A = (A::TY) \<longrightarrow> (\<forall>pi\<Colon>perm. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K \<longrightarrow> (supp K - {atom x}) \<sharp>* pi \<longrightarrow> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> x)) = |
|
587 (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x} \<and> |
|
588 (\<exists>pi\<Colon>perm. (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)}) \<sharp>* pi \<and> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> A \<noteq> A)" |
|
589 apply (case_tac "(a \<rightleftharpoons> b) \<bullet> A = A") |
|
590 apply (case_tac "supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x}") |
|
591 apply simp_all |
|
592 sorry |
|
593 |
|
594 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A" |
|
595 apply (subst supp_Pair[symmetric]) |
|
596 unfolding supp_def |
|
597 apply (simp add: permute_set_eq) |
|
598 apply(subst abs_eq) |
|
599 apply(subst KIND_TY_TRM_INJECT) |
|
600 apply(simp only: supp_fv) |
|
601 apply simp |
|
602 apply (unfold supp_def) |
|
603 sorry |
|
604 |
|
605 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
|
606 apply(subst supp_kpi_pre) |
|
607 thm supp_Abs |
|
608 (*apply(simp add: supp_Abs)*) |
|
609 sorry |
|
610 |
|
611 lemma supp_kind_ty_trm: |
|
612 "supp TYP = {}" |
|
613 "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
|
614 "supp (TCONST i) = {atom i}" |
|
615 "supp (TAPP A M) = supp A \<union> supp M" |
|
616 "supp (TPI A x B) = supp A \<union> (supp B - {atom x})" |
|
617 "supp (CONS i) = {atom i}" |
|
618 "supp (VAR x) = {atom x}" |
|
619 "supp (APP M N) = supp M \<union> supp N" |
|
620 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
|
621 apply - |
|
622 apply (simp add: supp_def) |
|
623 apply (simp add: supp_kpi) |
|
624 apply (simp add: supp_def) (* need ty.distinct lifted *) |
|
625 sorry |
|
626 |
323 |
627 |
324 end |
628 end |
325 |
629 |
326 |
630 |
327 |
631 |