118 valid :: "(name \<times> ty) list \<Rightarrow> bool" |
118 valid :: "(name \<times> ty) list \<Rightarrow> bool" |
119 where |
119 where |
120 "valid []" |
120 "valid []" |
121 | "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)" |
121 | "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)" |
122 |
122 |
123 ML {* |
|
124 fun my_tac ctxt intros = |
|
125 Nominal_Permeq.eqvt_strict_tac ctxt [] [] |
|
126 THEN' resolve_tac intros |
|
127 THEN_ALL_NEW |
|
128 (atac ORELSE' |
|
129 EVERY' |
|
130 [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}), |
|
131 Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], |
|
132 atac ]) |
|
133 *} |
|
134 |
|
135 lemma [eqvt]: |
|
136 assumes a: "valid Gamma" |
|
137 shows "valid (p \<bullet> Gamma)" |
|
138 using a |
|
139 apply(induct) |
|
140 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
|
141 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
|
142 done |
|
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 |
|
156 thm eqvts |
|
157 thm eqvts_raw |
|
158 |
|
159 inductive |
123 inductive |
160 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
124 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
161 where |
125 where |
162 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
126 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
163 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
127 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : 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" |
128 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
165 |
129 |
166 |
130 |
167 ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *} |
131 ML {* |
|
132 fun map_term f t = |
|
133 (case f t of |
|
134 NONE => map_term' f t |
|
135 | x => x) |
|
136 and map_term' f (t $ u) = |
|
137 (case (map_term f t, map_term f u) of |
|
138 (NONE, NONE) => NONE |
|
139 | (SOME t'', NONE) => SOME (t'' $ u) |
|
140 | (NONE, SOME u'') => SOME (t $ u'') |
|
141 | (SOME t'', SOME u'') => SOME (t'' $ u'')) |
|
142 | map_term' f (Abs (s, T, t)) = |
|
143 (case map_term f t of |
|
144 NONE => NONE |
|
145 | SOME t'' => SOME (Abs (s, T, t''))) |
|
146 | map_term' _ _ = NONE; |
|
147 |
|
148 fun map_thm_tac ctxt tac thm = |
|
149 let |
|
150 val monos = Inductive.get_monos ctxt |
|
151 in |
|
152 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
|
153 REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), |
|
154 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
|
155 end |
|
156 |
|
157 (* |
|
158 proves F[f t] from F[t] where F[t] is the given theorem |
|
159 |
|
160 - F needs to be monotone |
|
161 - f returns either SOME for a term it fires |
|
162 and NONE elsewhere |
|
163 *) |
|
164 fun map_thm ctxt f tac thm = |
|
165 let |
|
166 val opt_goal_trm = map_term f (prop_of thm) |
|
167 fun prove goal = |
|
168 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
|
169 in |
|
170 case opt_goal_trm of |
|
171 NONE => thm |
|
172 | SOME goal => prove goal |
|
173 end |
|
174 |
|
175 fun transform_prem ctxt names thm = |
|
176 let |
|
177 fun split_conj names (Const ("op &", _) $ p $ q) = |
|
178 (case head_of p of |
|
179 Const (name, _) => if name mem names then SOME q else NONE |
|
180 | _ => NONE) |
|
181 | split_conj _ _ = NONE; |
|
182 in |
|
183 map_thm ctxt (split_conj names) (etac conjunct2 1) thm |
|
184 end |
|
185 *} |
|
186 |
|
187 ML {* |
|
188 open Nominal_Permeq |
|
189 *} |
|
190 |
|
191 ML {* |
|
192 fun single_case_tac ctxt pred_names pi intro = |
|
193 let |
|
194 val rule = Drule.instantiate' [] [SOME pi] @{thm permute_boolE} |
|
195 in |
|
196 eqvt_strict_tac ctxt [] [] THEN' |
|
197 SUBPROOF (fn {prems, context as ctxt, ...} => |
|
198 let |
|
199 val prems' = map (transform_prem ctxt pred_names) prems |
|
200 val side_cond_tac = EVERY' |
|
201 [ rtac rule, |
|
202 eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], |
|
203 resolve_tac prems' ] |
|
204 in |
|
205 HEADGOAL (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) |
|
206 end) ctxt |
|
207 end |
|
208 *} |
|
209 |
|
210 ML {* |
|
211 fun eqvt_rel_tac pred_name = |
|
212 let |
|
213 val thy = ProofContext.theory_of ctxt |
|
214 val ({names, ...}, {raw_induct, intrs, ...}) = |
|
215 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
|
216 val param_no = length (Inductive.params_of raw_induct) |
|
217 val (([raw_concl], [pi]), ctxt') = |
|
218 ctxt |> Variable.import_terms false [concl_of raw_induct] |
|
219 ||>> Variable.variant_fixes ["pi"]; |
|
220 val preds = map (fst o HOLogic.dest_imp) |
|
221 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
|
222 in |
|
223 |
|
224 end |
|
225 *} |
|
226 |
|
227 |
|
228 |
|
229 lemma [eqvt]: |
|
230 assumes a: "valid Gamma" |
|
231 shows "valid (p \<bullet> Gamma)" |
|
232 using a |
|
233 apply(induct) |
|
234 apply(tactic {* my_tac @{context} ["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(1)} 1 *}) |
|
235 apply(tactic {* my_tac @{context }["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(2)} 1 *}) |
|
236 done |
168 |
237 |
169 lemma |
238 lemma |
170 shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
239 shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
171 ML_prf {* |
240 ML_prf {* |
172 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
241 val ({names, ...}, {raw_induct, ...}) = |
173 Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") |
242 Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") |
174 *} |
243 *} |
175 apply(tactic {* rtac raw_induct 1 *}) |
244 apply(tactic {* rtac raw_induct 1 *}) |
176 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
245 apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(1)} 1 *}) |
177 apply(perm_strict_simp) |
246 apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(2)} 1 *}) |
178 apply(rule typing.intros) |
247 apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(3)} 1 *}) |
179 oops |
248 done |
180 |
249 |
181 lemma uu[eqvt]: |
250 lemma uu[eqvt]: |
182 assumes a: "Gamma \<turnstile> t : T" |
251 assumes a: "Gamma \<turnstile> t : T" |
183 shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
252 shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
184 using a |
253 using a |