139 apply(induct) |
139 apply(induct) |
140 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
140 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
141 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
141 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
142 done |
142 done |
143 |
143 |
|
144 lemma |
|
145 shows "valid Gamma \<longrightarrow> valid (p \<bullet> Gamma)" |
|
146 ML_prf {* |
|
147 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
|
148 Inductive.the_inductive @{context} (Sign.intern_const @{theory} "valid") |
|
149 *} |
|
150 apply(tactic {* rtac raw_induct 1 *}) |
|
151 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
|
152 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
|
153 done |
|
154 |
|
155 |
144 thm eqvts |
156 thm eqvts |
145 thm eqvts_raw |
157 thm eqvts_raw |
146 |
158 |
147 inductive |
159 inductive |
148 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
160 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
149 where |
161 where |
150 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
162 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
151 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
163 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
152 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
164 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
153 |
165 |
154 thm typing.induct |
166 |
155 ML {* Inductive.get_monos @{context} *} |
167 ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *} |
|
168 |
|
169 lemma |
|
170 shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
|
171 ML_prf {* |
|
172 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
|
173 Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") |
|
174 *} |
|
175 apply(tactic {* rtac raw_induct 1 *}) |
|
176 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
|
177 apply(perm_strict_simp) |
|
178 apply(rule typing.intros) |
|
179 oops |
156 |
180 |
157 lemma uu[eqvt]: |
181 lemma uu[eqvt]: |
158 assumes a: "Gamma \<turnstile> t : T" |
182 assumes a: "Gamma \<turnstile> t : T" |
159 shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
183 shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
160 using a |
184 using a |
166 prefer 3 |
190 prefer 3 |
167 apply(assumption) |
191 apply(assumption) |
168 apply(rule impI) |
192 apply(rule impI) |
169 prefer 2 |
193 prefer 2 |
170 apply(rule impI) |
194 apply(rule impI) |
171 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
195 apply(simp) |
172 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
196 apply(auto)[1] |
173 done |
197 apply(simp) |
174 |
198 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
|
199 done |
|
200 |
|
201 (* |
175 inductive |
202 inductive |
176 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
203 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
177 where |
204 where |
178 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
205 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
179 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
206 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
186 apply(induct) |
213 apply(induct) |
187 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
214 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
188 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
215 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
189 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
216 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
190 done |
217 done |
|
218 *) |
|
219 |
|
220 ML {* |
|
221 val inductive_atomize = @{thms induct_atomize}; |
|
222 |
|
223 val atomize_conv = |
|
224 MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
|
225 (HOL_basic_ss addsimps inductive_atomize); |
|
226 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); |
|
227 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
|
228 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
|
229 *} |
|
230 |
|
231 ML {* |
|
232 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
|
233 Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") |
|
234 *} |
|
235 |
|
236 ML {* val ind_params = Inductive.params_of raw_induct *} |
|
237 ML {* val raw_induct = atomize_induct @{context} raw_induct; *} |
|
238 ML {* val elims = map (atomize_induct @{context}) elims; *} |
|
239 ML {* val monos = Inductive.get_monos @{context}; *} |
|
240 |
|
241 lemma |
|
242 shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
|
243 apply(tactic {* rtac raw_induct 1 *}) |
|
244 apply(tactic {* my_tac @{context} intrs 1 *}) |
|
245 apply(perm_strict_simp) |
|
246 apply(rule typing.intros) |
|
247 oops |
|
248 |
191 |
249 |
192 thm eqvts |
250 thm eqvts |
193 thm eqvts_raw |
251 thm eqvts_raw |
194 |
252 |
195 declare permute_lam_raw.simps[eqvt] |
253 declare permute_lam_raw.simps[eqvt] |