equal
deleted
inserted
replaced
168 end) ctxt |
168 end) ctxt |
169 |
169 |
170 fun non_binder_tac prem intr_cvars Ps ctxt = |
170 fun non_binder_tac prem intr_cvars Ps ctxt = |
171 Subgoal.SUBPROOF (fn {context, params, prems, ...} => |
171 Subgoal.SUBPROOF (fn {context, params, prems, ...} => |
172 let |
172 let |
173 val thy = ProofContext.theory_of context |
173 val thy = Proof_Context.theory_of context |
174 val (prms, p, _) = split_last2 (map snd params) |
174 val (prms, p, _) = split_last2 (map snd params) |
175 val prm_tys = map (fastype_of o term_of) prms |
175 val prm_tys = map (fastype_of o term_of) prms |
176 val cperms = map (cterm_of thy o perm_const) prm_tys |
176 val cperms = map (cterm_of thy o perm_const) prm_tys |
177 val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms |
177 val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms |
178 val prem' = prem |
178 val prem' = prem |
221 |
221 |
222 |
222 |
223 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = |
223 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = |
224 Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => |
224 Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => |
225 let |
225 let |
226 val thy = ProofContext.theory_of ctxt |
226 val thy = Proof_Context.theory_of ctxt |
227 val (prms, p, c) = split_last2 (map snd params) |
227 val (prms, p, c) = split_last2 (map snd params) |
228 val prm_trms = map term_of prms |
228 val prm_trms = map term_of prms |
229 val prm_tys = map fastype_of prm_trms |
229 val prm_tys = map fastype_of prm_trms |
230 |
230 |
231 val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm |
231 val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm |
271 (fn {context, ...} => |
271 (fn {context, ...} => |
272 EVERY1 [ CONVERSION (expand_conv_bot context), |
272 EVERY1 [ CONVERSION (expand_conv_bot context), |
273 eqvt_stac context, |
273 eqvt_stac context, |
274 rtac prem', |
274 rtac prem', |
275 RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) |
275 RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) |
276 |> singleton (ProofContext.export ctxt' ctxt) |
276 |> singleton (Proof_Context.export ctxt' ctxt) |
277 in |
277 in |
278 rtac side_thm 1 |
278 rtac side_thm 1 |
279 end) ctxt |
279 end) ctxt |
280 |
280 |
281 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = |
281 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = |
298 |
298 |
299 val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp} |
299 val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp} |
300 |
300 |
301 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = |
301 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = |
302 let |
302 let |
303 val thy = ProofContext.theory_of ctxt |
303 val thy = Proof_Context.theory_of ctxt |
304 val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt |
304 val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt |
305 |
305 |
306 val (ind_prems, ind_concl) = raw_induct' |
306 val (ind_prems, ind_concl) = raw_induct' |
307 |> prop_of |
307 |> prop_of |
308 |> Logic.strip_horn |
308 |> Logic.strip_horn |
355 |
355 |
356 fun after_qed ctxt_outside user_thms ctxt = |
356 fun after_qed ctxt_outside user_thms ctxt = |
357 let |
357 let |
358 val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' |
358 val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' |
359 (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |
359 (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |
360 |> singleton (ProofContext.export ctxt ctxt_outside) |
360 |> singleton (Proof_Context.export ctxt ctxt_outside) |
361 |> Datatype_Aux.split_conj_thm |
361 |> Datatype_Aux.split_conj_thm |
362 |> map (fn thm => thm RS normalise) |
362 |> map (fn thm => thm RS normalise) |
363 |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) |
363 |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) |
364 |> map (Drule.rotate_prems (length ind_prems')) |
364 |> map (Drule.rotate_prems (length ind_prems')) |
365 |> map zero_var_indexes |
365 |> map zero_var_indexes |
381 Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt'' |
381 Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt'' |
382 end |
382 end |
383 |
383 |
384 fun prove_strong_inductive_cmd (pred_name, avoids) ctxt = |
384 fun prove_strong_inductive_cmd (pred_name, avoids) ctxt = |
385 let |
385 let |
386 val thy = ProofContext.theory_of ctxt; |
386 val thy = Proof_Context.theory_of ctxt; |
387 val ({names, ...}, {raw_induct, intrs, ...}) = |
387 val ({names, ...}, {raw_induct, intrs, ...}) = |
388 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name); |
388 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name); |
389 |
389 |
390 val rule_names = |
390 val rule_names = |
391 hd names |
391 hd names |