124 |
124 |
125 inductive |
125 inductive |
126 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
126 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
127 where |
127 where |
128 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
128 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
129 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
129 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
130 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
130 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
131 |
|
132 inductive |
|
133 typing' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<Turnstile> _ : _" [60,60,60] 60) |
|
134 where |
|
135 t'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Var x : T" |
|
136 | t'_App[intro]: "\<lbrakk>\<Gamma> \<Turnstile> t1 : T1\<rightarrow>T2 \<and> \<Gamma> \<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> App t1 t2 : T2" |
|
137 | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Lam x t : T1\<rightarrow>T2" |
|
138 |
|
139 inductive |
|
140 typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60) |
|
141 where |
|
142 t2'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Var x : T" |
|
143 | t2'_App[intro]: "\<lbrakk>\<Gamma> 2\<Turnstile> t1 : T1\<rightarrow>T2 \<or> \<Gamma> 2\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> App t1 t2 : T2" |
|
144 | t2'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> 2\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Lam x t : T1\<rightarrow>T2" |
|
145 |
|
146 inductive |
|
147 typing'' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ |\<Turnstile> _ : _" [60,60,60] 60) |
|
148 and valid' :: "(name\<times>ty) list \<Rightarrow> bool" |
|
149 where |
|
150 v1[intro]: "valid' []" |
|
151 | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)" |
|
152 | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T" |
|
153 | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2" |
|
154 | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2" |
|
155 |
131 |
156 equivariance valid |
132 equivariance valid |
157 equivariance typing |
133 equivariance typing |
158 equivariance typing' |
|
159 equivariance typing2' |
|
160 equivariance typing'' |
|
161 |
134 |
162 thm valid.eqvt |
135 thm valid.eqvt |
163 thm typing.eqvt |
136 thm typing.eqvt |
164 thm eqvts |
137 thm eqvts |
165 thm eqvts_raw |
138 thm eqvts_raw |
187 alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" |
160 alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" |
188 |
161 |
189 declare permute_lam_raw.simps[eqvt] |
162 declare permute_lam_raw.simps[eqvt] |
190 declare alpha_gen_eqvt[eqvt] |
163 declare alpha_gen_eqvt[eqvt] |
191 equivariance alpha_lam_raw' |
164 equivariance alpha_lam_raw' |
|
165 |
192 thm eqvts_raw |
166 thm eqvts_raw |
193 |
|
194 |
|
195 |
|
196 (* HERE *) |
|
197 |
|
198 lemma |
|
199 assumes a: "alpha_lam_raw' t1 t2" |
|
200 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
|
201 using a |
|
202 apply(induct) |
|
203 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
|
204 @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*}) |
|
205 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
|
206 @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*}) |
|
207 (* |
|
208 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
|
209 @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*}) |
|
210 *) |
|
211 oops |
|
212 |
167 |
213 section {* size function *} |
168 section {* size function *} |
214 |
169 |
215 lemma size_eqvt_raw: |
170 lemma size_eqvt_raw: |
216 fixes t::"lam_raw" |
171 fixes t::"lam_raw" |