17 | Var "name" |
17 | Var "name" |
18 | App "rtrm" "rtrm" |
18 | App "rtrm" "rtrm" |
19 | Lam "rty" "name" "rtrm" |
19 | Lam "rty" "name" "rtrm" |
20 |
20 |
21 |
21 |
22 instantiation rkind and rty and rtrm :: pt |
|
23 begin |
|
24 |
|
25 primrec |
|
26 permute_rkind |
|
27 and permute_rty |
|
28 and permute_rtrm |
|
29 where |
|
30 "permute_rkind pi Type = Type" |
|
31 | "permute_rkind pi (KPi t n k) = KPi (permute_rty pi t) (pi \<bullet> n) (permute_rkind pi k)" |
|
32 | "permute_rty pi (TConst i) = TConst (pi \<bullet> i)" |
|
33 | "permute_rty pi (TApp A M) = TApp (permute_rty pi A) (permute_rtrm pi M)" |
|
34 | "permute_rty pi (TPi A x B) = TPi (permute_rty pi A) (pi \<bullet> x) (permute_rty pi B)" |
|
35 | "permute_rtrm pi (Const i) = Const (pi \<bullet> i)" |
|
36 | "permute_rtrm pi (Var x) = Var (pi \<bullet> x)" |
|
37 | "permute_rtrm pi (App M N) = App (permute_rtrm pi M) (permute_rtrm pi N)" |
|
38 | "permute_rtrm pi (Lam A x M) = Lam (permute_rty pi A) (pi \<bullet> x) (permute_rtrm pi M)" |
|
39 |
|
40 lemma rperm_zero_ok: |
|
41 "0 \<bullet> (x :: rkind) = x" |
|
42 "0 \<bullet> (y :: rty) = y" |
|
43 "0 \<bullet> (z :: rtrm) = z" |
|
44 apply(induct x and y and z rule: rkind_rty_rtrm.inducts) |
|
45 apply(simp_all) |
|
46 done |
|
47 |
|
48 lemma rperm_plus_ok: |
|
49 "(p + q) \<bullet> (x :: rkind) = p \<bullet> q \<bullet> x" |
|
50 "(p + q) \<bullet> (y :: rty) = p \<bullet> q \<bullet> y" |
|
51 "(p + q) \<bullet> (z :: rtrm) = p \<bullet> q \<bullet> z" |
|
52 apply(induct x and y and z rule: rkind_rty_rtrm.inducts) |
|
53 apply(simp_all) |
|
54 done |
|
55 |
|
56 instance |
|
57 apply default |
|
58 apply (simp_all only:rperm_zero_ok rperm_plus_ok) |
|
59 done |
|
60 |
|
61 end |
|
62 |
|
63 (* |
|
64 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} |
22 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} |
|
23 |
65 local_setup {* |
24 local_setup {* |
66 snd o define_fv_alpha "LFex.rkind" |
25 snd o define_fv_alpha "LFex.rkind" |
67 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
26 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
68 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
27 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
69 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
28 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
73 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100) |
32 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100) |
74 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros |
33 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros |
75 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *} |
34 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *} |
76 thm alpha_rkind_alpha_rty_alpha_rtrm_inj |
35 thm alpha_rkind_alpha_rty_alpha_rtrm_inj |
77 |
36 |
78 lemma alpha_eqvt: |
|
79 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
|
80 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
|
81 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
|
82 sorry |
|
83 |
|
84 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
|
85 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
|
86 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} |
|
87 @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
|
88 @{thms rkind.distinct rty.distinct rtrm.distinct} |
|
89 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
|
90 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
|
91 thm alpha_equivps |
|
92 *) |
|
93 |
|
94 primrec |
|
95 fv_rkind :: "rkind \<Rightarrow> atom set" |
|
96 and fv_rty :: "rty \<Rightarrow> atom set" |
|
97 and fv_rtrm :: "rtrm \<Rightarrow> atom set" |
|
98 where |
|
99 "fv_rkind (Type) = {}" |
|
100 | "fv_rkind (KPi A x K) = (fv_rty A) \<union> ((fv_rkind K) - {atom x})" |
|
101 | "fv_rty (TConst i) = {atom i}" |
|
102 | "fv_rty (TApp A M) = (fv_rty A) \<union> (fv_rtrm M)" |
|
103 | "fv_rty (TPi A x B) = (fv_rty A) \<union> ((fv_rty B) - {atom x})" |
|
104 | "fv_rtrm (Const i) = {atom i}" |
|
105 | "fv_rtrm (Var x) = {atom x}" |
|
106 | "fv_rtrm (App M N) = (fv_rtrm M) \<union> (fv_rtrm N)" |
|
107 | "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})" |
|
108 |
|
109 inductive |
|
110 alpha_rkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100) |
|
111 and alpha_rty :: "rty \<Rightarrow> rty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100) |
|
112 and alpha_rtrm :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100) |
|
113 where |
|
114 a1: "(Type) \<approx>ki (Type)" |
|
115 | a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen alpha_rkind fv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')" |
|
116 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)" |
|
117 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')" |
|
118 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen alpha_rty fv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')" |
|
119 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)" |
|
120 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)" |
|
121 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')" |
|
122 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')" |
|
123 |
|
124 lemma alpha_rkind_alpha_rty_alpha_rtrm_inj: |
|
125 "(Type) \<approx>ki (Type) = True" |
|
126 "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen alpha_rkind fv_rkind pi ({atom b}, K')))" |
|
127 "(TConst i) \<approx>ty (TConst j) = (i = j)" |
|
128 "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')" |
|
129 "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen alpha_rty fv_rty pi ({atom b}, B'))))" |
|
130 "(Const i) \<approx>tr (Const j) = (i = j)" |
|
131 "(Var x) \<approx>tr (Var y) = (x = y)" |
|
132 "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')" |
|
133 "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))))" |
|
134 apply - |
|
135 apply (simp add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
136 |
|
137 apply rule apply (erule alpha_rkind.cases) apply simp apply blast |
|
138 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
139 |
|
140 apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp |
|
141 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
142 |
|
143 apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp |
|
144 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
145 |
|
146 apply rule apply (erule alpha_rty.cases) apply simp apply simp apply blast |
|
147 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
148 |
|
149 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast |
|
150 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
151 |
|
152 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast |
|
153 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
154 |
|
155 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast |
|
156 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
157 |
|
158 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast |
|
159 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
160 done |
|
161 |
|
162 lemma rfv_eqvt[eqvt]: |
37 lemma rfv_eqvt[eqvt]: |
163 "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))" |
38 "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))" |
164 "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))" |
39 "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))" |
165 "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))" |
40 "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))" |
166 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts) |
41 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts) |
167 apply(simp_all add: union_eqvt Diff_eqvt) |
42 apply(simp_all add: union_eqvt Diff_eqvt) |
168 apply(simp_all add: permute_set_eq atom_eqvt) |
43 apply(simp_all add: permute_set_eq atom_eqvt) |
169 done |
44 done |
170 |
45 |
171 lemma alpha_eqvt: |
46 lemma alpha_eqvt: |
172 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
47 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
184 apply (rule alpha_gen_atom_eqvt) |
59 apply (rule alpha_gen_atom_eqvt) |
185 apply (simp add: rfv_eqvt) |
60 apply (simp add: rfv_eqvt) |
186 apply assumption |
61 apply assumption |
187 done |
62 done |
188 |
63 |
189 lemma al_refl: |
64 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
190 fixes K::"rkind" |
65 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
191 and A::"rty" |
66 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} |
192 and M::"rtrm" |
67 @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
193 shows "K \<approx>ki K" |
68 @{thms rkind.distinct rty.distinct rtrm.distinct} |
194 and "A \<approx>ty A" |
69 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
195 and "M \<approx>tr M" |
70 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
196 apply(induct K and A and M rule: rkind_rty_rtrm.inducts) |
71 thm alpha_equivps |
197 apply(auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
198 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) |
|
199 apply auto |
|
200 apply(rule_tac x="0" in exI) |
|
201 apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen) |
|
202 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) |
|
203 apply auto |
|
204 apply(rule_tac x="0" in exI) |
|
205 apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen) |
|
206 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) |
|
207 apply auto |
|
208 apply(rule_tac x="0" in exI) |
|
209 apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen) |
|
210 done |
|
211 |
|
212 lemma al_sym: |
|
213 fixes K K'::"rkind" and A A'::"rty" and M M'::"rtrm" |
|
214 shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K" |
|
215 and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A" |
|
216 and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M" |
|
217 apply(induct K K' and A A' and M M' rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) |
|
218 apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
219 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
|
220 apply(erule alpha_gen_compose_sym) |
|
221 apply(erule alpha_eqvt) |
|
222 apply(erule alpha_gen_compose_sym) |
|
223 apply(erule alpha_eqvt) |
|
224 apply(erule alpha_gen_compose_sym) |
|
225 apply(erule alpha_eqvt) |
|
226 done |
|
227 |
|
228 lemma al_trans: |
|
229 fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm" |
|
230 shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''" |
|
231 and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''" |
|
232 and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''" |
|
233 apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) |
|
234 apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
235 apply(erule alpha_rkind.cases) |
|
236 apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
237 apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
|
238 apply(erule alpha_gen_compose_trans) |
|
239 apply(assumption) |
|
240 apply(erule alpha_eqvt) |
|
241 apply(rotate_tac 4) |
|
242 apply(erule alpha_rty.cases) |
|
243 apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
244 apply(rotate_tac 3) |
|
245 apply(erule alpha_rty.cases) |
|
246 apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
247 apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
|
248 apply(erule alpha_gen_compose_trans) |
|
249 apply(assumption) |
|
250 apply(erule alpha_eqvt) |
|
251 apply(rotate_tac 4) |
|
252 apply(erule alpha_rtrm.cases) |
|
253 apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
254 apply(rotate_tac 3) |
|
255 apply(erule alpha_rtrm.cases) |
|
256 apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
257 apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
|
258 apply(erule alpha_gen_compose_trans) |
|
259 apply(assumption) |
|
260 apply(erule alpha_eqvt) |
|
261 done |
|
262 |
|
263 lemma alpha_equivps: |
|
264 shows "equivp alpha_rkind" |
|
265 and "equivp alpha_rty" |
|
266 and "equivp alpha_rtrm" |
|
267 apply(rule equivpI) |
|
268 unfolding reflp_def symp_def transp_def |
|
269 apply(auto intro: al_refl al_sym al_trans) |
|
270 apply(rule equivpI) |
|
271 unfolding reflp_def symp_def transp_def |
|
272 apply(auto intro: al_refl al_sym al_trans) |
|
273 apply(rule equivpI) |
|
274 unfolding reflp_def symp_def transp_def |
|
275 apply(auto intro: al_refl al_sym al_trans) |
|
276 done |
|
277 |
72 |
278 quotient_type RKIND = rkind / alpha_rkind |
73 quotient_type RKIND = rkind / alpha_rkind |
279 by (rule alpha_equivps) |
74 by (rule alpha_equivps) |
280 |
75 |
281 quotient_type |
76 quotient_type |