130 [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}), |
130 [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}), |
131 Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], |
131 Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], |
132 atac ]) |
132 atac ]) |
133 *} |
133 *} |
134 |
134 |
135 |
135 ML {* try hd [1] *} |
136 lemma |
136 |
|
137 ML {* |
|
138 Skip_Proof.cheat_tac |
|
139 *} |
|
140 |
|
141 |
|
142 lemma [eqvt]: |
137 assumes a: "valid Gamma" |
143 assumes a: "valid Gamma" |
138 shows "valid (p \<bullet> Gamma)" |
144 shows "valid (p \<bullet> Gamma)" |
139 using a |
145 using a |
140 apply(induct) |
146 apply(induct) |
141 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
147 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
142 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
148 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
143 done |
149 done |
144 |
150 |
145 lemma |
151 thm eqvts |
146 "(p \<bullet> valid) = valid" |
152 thm eqvts_raw |
147 oops |
|
148 |
|
149 lemma temp[eqvt_raw]: |
|
150 "(p \<bullet> valid) \<equiv> valid" |
|
151 sorry |
|
152 |
153 |
153 inductive |
154 inductive |
154 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
155 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
155 where |
156 where |
156 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
157 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
157 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
158 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
158 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
159 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
159 |
160 |
160 lemma |
161 lemma uu[eqvt]: |
161 assumes a: "Gamma \<turnstile> t : T" |
162 assumes a: "Gamma \<turnstile> t : T" |
162 shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
163 shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
163 using a |
164 using a |
164 apply(induct) |
165 apply(induct) |
165 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
166 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
166 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
167 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
167 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
168 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
168 done |
169 done |
|
170 |
|
171 thm eqvts |
|
172 thm eqvts_raw |
169 |
173 |
170 declare permute_lam_raw.simps[eqvt] |
174 declare permute_lam_raw.simps[eqvt] |
171 |
175 |
172 thm alpha_gen_real_eqvt[no_vars] |
176 thm alpha_gen_real_eqvt[no_vars] |
173 |
177 |