theory Tacs+ −
imports Main+ −
begin+ −
+ − (* General not-nominal/quotient functionality useful for proving *)+ −
+ − (* A version of case_rule_tac that takes more exhaust rules *)+ −
ML {*+ −
fun case_rules_tac ctxt0 s rules i st =+ −
let+ −
val (_, ctxt) = Variable.focus_subgoal i st ctxt0;+ −
val ty = fastype_of (ProofContext.read_term_schematic ctxt s)+ −
fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1))));+ −
val ty_rules = filter (fn x => exhaust_ty x = ty) rules;+ −
in+ −
InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st+ −
end+ −
*}+ −
+ − ML {*+ −
fun mk_conjl props =+ −
fold (fn a => fn b =>+ −
if a = @{term True} then b else+ −
if b = @{term True} then a else+ −
HOLogic.mk_conj (a, b)) (rev props) @{term True};+ −
*}+ −
+ − ML {*+ −
val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)+ −
*}+ −
+ − (* Given function for buildng a goal for an input, prepares a+ −
one common goals for all the inputs and proves it by induction+ −
together *)+ −
ML {*+ −
fun prove_by_induct tys build_goal ind utac inputs ctxt =+ −
let+ −
val names = Datatype_Prop.make_tnames tys;+ −
val (names', ctxt') = Variable.variant_fixes names ctxt;+ −
val frees = map Free (names' ~~ tys);+ −
val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';+ −
val gls = flat gls_lists;+ −
fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;+ −
val trm_gl_lists = map trm_gls_map frees;+ −
val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists+ −
val trm_gls = map mk_conjl trm_gl_lists;+ −
val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);+ −
fun tac {context,...} = (+ −
InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]+ −
THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1+ −
val th_loc = Goal.prove ctxt'' [] [] gl tac+ −
val ths_loc = HOLogic.conj_elims th_loc+ −
val ths = Variable.export ctxt'' ctxt ths_loc+ −
in+ −
filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths+ −
end+ −
*}+ −
+ − (* An induction for a single relation is "R x y \<Longrightarrow> P x y"+ −
but for multiple relations is "(R1 x y \<longrightarrow> P x y) \<and> (R2 a b \<longrightarrow> P2 a b)" *)+ −
ML {*+ −
fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct+ −
*}+ −
+ − ML {*+ −
fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =+ −
let+ −
val tys = map (domain_type o fastype_of) alphas;+ −
val names = Datatype_Prop.make_tnames tys;+ −
val (namesl, ctxt') = Variable.variant_fixes names ctxt;+ −
val (namesr, ctxt'') = Variable.variant_fixes names ctxt';+ −
val freesl = map Free (namesl ~~ tys);+ −
val freesr = map Free (namesr ~~ tys);+ −
val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';+ −
val gls = flat gls_lists;+ −
fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;+ −
val trm_gl_lists = map trm_gls_map freesl;+ −
val trm_gls = map mk_conjl trm_gl_lists;+ −
val pgls = map+ −
(fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) + −
((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))+ −
val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);+ −
fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW+ −
TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1+ −
val th_loc = Goal.prove ctxt'' [] [] gl tac+ −
val ths_loc = HOLogic.conj_elims th_loc+ −
val ths = Variable.export ctxt'' ctxt ths_loc+ −
in+ −
filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths+ −
end+ −
*}+ −
(* Code for transforming an inductive relation to a function *)+ −
ML {*+ −
fun rel_inj_tac dist_inj intrs elims =+ −
SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'+ −
(rtac @{thm iffI} THEN' RANGE [+ −
(eresolve_tac elims THEN_ALL_NEW+ −
asm_full_simp_tac (HOL_ss addsimps dist_inj)+ −
),+ −
asm_full_simp_tac (HOL_ss addsimps intrs)])+ −
*}+ −
+ − ML {*+ −
fun build_rel_inj_gl thm =+ −
let+ −
val prop = prop_of thm;+ −
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);+ −
val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);+ −
fun list_conj l = foldr1 HOLogic.mk_conj l;+ −
in+ −
if hyps = [] then concl+ −
else HOLogic.mk_eq (concl, list_conj hyps)+ −
end;+ −
*}+ −
+ − ML {*+ −
fun build_rel_inj intrs dist_inj elims ctxt =+ −
let+ −
val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;+ −
val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp;+ −
fun tac _ = rel_inj_tac dist_inj intrs elims 1;+ −
val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;+ −
in+ −
Variable.export ctxt' ctxt thms+ −
end+ −
*}+ −
+ − ML {*+ −
fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm+ −
*}+ −
+ − (* Introduces an implication and immediately eliminates it by cases *)+ −
ML {*+ −
fun imp_elim_tac case_rules =+ −
Subgoal.FOCUS (fn {concl, context, ...} =>+ −
case term_of concl of+ −
_ $ (_ $ asm $ _) =>+ −
let+ −
fun filter_fn case_rule = (+ −
case Logic.strip_assums_hyp (prop_of case_rule) of+ −
((_ $ asmc) :: _) =>+ −
let+ −
val thy = ProofContext.theory_of context+ −
in+ −
Pattern.matches thy (asmc, asm)+ −
end+ −
| _ => false)+ −
val matching_rules = filter filter_fn case_rules+ −
in+ −
(rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1+ −
end+ −
| _ => no_tac)+ −
*}+ −
+ − ML {*+ −
fun is_ex (Const ("Ex", _) $ Abs _) = true+ −
| is_ex _ = false;+ −
*}+ −
+ − ML {*+ −
fun dtyp_no_of_typ _ (TFree (_, _)) = error "dtyp_no_of_typ: Illegal free"+ −
| dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"+ −
| dtyp_no_of_typ dts (Type (tname, _)) =+ −
case try (find_index (curry op = tname o fst)) dts of+ −
NONE => error "dtyp_no_of_typ: Illegal recursion"+ −
| SOME i => i+ −
*}+ −
+ − end+ −
+ −