File ‹induct_outer.ML›
signature INDUCT_PROOFSTEPS =
sig
val add_induct_data: string -> term * thm -> theory -> theory
val add_typed_induct_data: string -> typ * thm -> theory -> theory
val get_typed_ind_th: theory -> string -> typ -> thm
val get_term_ind_th: theory -> string -> term -> thm
val check_strong_ind_prop: term -> term list * term
val add_strong_induct_rule: thm -> theory -> theory
val add_case_induct_rule: thm -> theory -> theory
val add_prop_induct_rule: thm -> theory -> theory
val add_var_induct_rule: thm -> theory -> theory
val add_cases_rule: thm -> theory -> theory
val add_fun_induct_rule: term * thm -> theory -> theory
val strong_induct_cmd: string * string list -> Proof.state -> Proof.state
val apply_induct_hyp_cmd: string list -> Proof.state -> Proof.state
val case_induct_cmd: string -> Proof.state -> Proof.state
val prop_induct_cmd: string * string option -> Proof.state -> Proof.state
val induct_cmd:
string -> string * string option * string list * string option ->
Proof.state -> Proof.state
val is_simple_fun_induct: thm -> bool
val fun_induct_cmd:
string * string list * string option -> Proof.state -> Proof.state
end;
signature INDUCT_PROOFSTEPS_KEYWORDS =
sig
val apply_induct_hyp: string * Position.T
val case_induct: string * Position.T
val cases: string * Position.T
val fun_induct: string * Position.T
val induct: string * Position.T
val prop_induct: string * Position.T
val strong_induct: string * Position.T
val arbitrary: string parser
val with': string parser
end;
functor Induct_ProofSteps(
structure Auto2_Outer: AUTO2_OUTER;
structure Induct_ProofSteps_Keywords: INDUCT_PROOFSTEPS_KEYWORDS;
structure UtilBase: UTIL_BASE;
structure UtilLogic: UTIL_LOGIC;
) : INDUCT_PROOFSTEPS =
struct
structure Data = Theory_Data (
type T = ((term * thm) list) Symtab.table;
val empty = Symtab.empty;
val merge = Symtab.merge_list (eq_fst (op =))
)
fun add_induct_data str (t, ind_th) =
Data.map (Symtab.map_default (str, []) (cons (t, ind_th)))
fun add_typed_induct_data str (ty, ind_th) =
add_induct_data str (Term.dummy_pattern ty, ind_th)
fun get_typed_ind_th thy ind_type ty =
let
val typ_can_match =
can (fn t' => Sign.typ_match thy (type_of t', ty) Vartab.empty)
in
case Symtab.lookup (Data.get thy) ind_type of
NONE => raise Fail (ind_type ^ ": cannot find theorem.")
| SOME lst =>
case find_first (fn (t', _) => typ_can_match t') lst of
NONE => raise Fail (ind_type ^ ": cannot find theorem.")
| SOME (_, ind_th) => ind_th
end
fun get_term_ind_th thy ind_type t =
let
val data = Symtab.lookup_list (Data.get thy) ind_type
fun match_data (pat, th) =
let
val inst = Pattern.first_order_match thy (pat, t) fo_init
in
SOME (Util.subst_thm_thy thy inst th)
end
handle Pattern.MATCH => NONE
in
case get_first match_data data of
NONE => raise Fail (ind_type ^ ": cannot find theorem.")
| SOME ind_th => ind_th
end
fun check_strong_ind_prop ind_prop =
let
fun err str = "Strong induction: " ^ str
val (cond_ind, concl) =
ind_prop |> Logic.dest_implies |> apply2 UtilLogic.dest_Trueprop
val err_concl = err "concl of ind_th must be ?P [?vars]."
val (P, pat_vars) = Term.strip_comb concl
handle TERM _ => error err_concl
val _ = assert (is_Var P andalso forall is_Var pat_vars andalso
(dest_Var P |> fst |> fst) = "P") err_concl
val err_ind_hyp = err "cond_ind of ind_th must be !n. P' --> ?P vars."
fun dest_one_all var body =
case body of
Const (c, _) $ Abs (_, _, t) =>
if c = UtilBase.All_name then subst_bound (var, t)
else error err_ind_hyp
| _ => error err_ind_hyp
val (pat_subst, P_vars) =
cond_ind |> fold dest_one_all pat_vars |> UtilLogic.dest_imp
val _ = assert (P_vars aconv concl) err_ind_hyp
in
(pat_vars, pat_subst)
end
fun add_strong_induct_rule ind_th thy =
let
val name = Util.name_of_thm ind_th
val ctxt = Proof_Context.init_global thy
val ind_th' = apply_to_thm (UtilLogic.to_obj_conv_on_horn ctxt) ind_th
val (pat_var, pat_subst) =
check_strong_ind_prop (Thm.prop_of ind_th') |> apfst the_single
handle List.Empty => error "Strong induction: more than one var."
val ty_var = type_of pat_var
val _ = writeln (name ^ "\nSubstitution: " ^
(Util.string_of_terms_global thy [pat_var, pat_subst]))
in
thy |> add_typed_induct_data "strong_induct" (ty_var, ind_th')
end
fun add_case_induct_rule ind_th thy =
let
val init_assum = ind_th |> Thm.prems_of |> hd |> UtilLogic.dest_Trueprop
in
thy |> add_induct_data "case_induct" (init_assum, ind_th)
end
fun add_prop_induct_rule ind_th thy =
let
val init_assum = ind_th |> Thm.prems_of |> hd |> UtilLogic.dest_Trueprop
in
thy |> add_induct_data "prop_induct" (init_assum, ind_th)
end
fun add_var_induct_rule ind_th thy =
let
val (P, n) = ind_th |> UtilLogic.concl_of' |> Term.dest_comb
val _ = assert (Term.is_Var P andalso Term.is_Var n)
"add_var_induct_rule: concl of ind_th must be ?P ?var"
in
thy |> add_typed_induct_data "var_induct" (type_of n, ind_th)
end
fun add_cases_rule ind_th thy =
let
val (P, n) = ind_th |> UtilLogic.concl_of' |> Term.dest_comb
val _ = assert (Term.is_Var P andalso Term.is_Var n)
"add_cases_rule: concl of ind_th must be ?P ?var"
in
thy |> add_typed_induct_data "cases" (type_of n, ind_th)
end
fun add_fun_induct_rule (t, ind_th) thy =
thy |> add_induct_data "fun_induct" (t, ind_th)
fun get_induct_stmt ctxt (filt_A, ind_vars, stmt, arbitrary) =
case stmt of
NONE =>
let
val (_, (As, C)) = ctxt |> Auto2_State.get_subgoal
|> Util.strip_meta_horn
val obj_As = As |> map UtilLogic.dest_Trueprop |> filter filt_A
val obj_C = UtilLogic.dest_Trueprop C
in
(UtilLogic.list_obj_horn (arbitrary, (obj_As, obj_C)))
|> fold Util.lambda_abstract (rev ind_vars)
end
| SOME s =>
(UtilLogic.list_obj_horn (arbitrary, ([], Syntax.read_term ctxt s)))
|> fold Util.lambda_abstract (rev ind_vars)
fun apply_simple_induct_th ind_th vars arbitraries prem_only state =
let
val {context = ctxt, ...} = Proof.goal state
val prop = Auto2_State.get_selected ctxt
val (vars', _) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val ind_th =
ind_th |> apply_to_thm (Conv.binop_conv (UtilLogic.to_meta_conv ctxt))
val assum = hd (Drule.cprems_of ind_th)
val ind_th =
ind_th |> Util.send_first_to_hyps
|> fold Thm.forall_elim (map (Thm.cterm_of ctxt) arbitraries)
|> fold Thm.forall_intr (map (Thm.cterm_of ctxt) vars')
|> Thm.implies_intr assum
val t' = case Thm.prop_of ind_th of
imp $ A $ B => imp $ Util.rename_abs_term vars A $ B
| _ => raise Fail "strong_induct_cmd"
val ind_th = ind_th |> Thm.renamed_prop t'
val prop = prop |> Auto2_Outer.refine_subgoal_th ind_th
in
if prem_only then
let
val (_, (As, _)) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val stmt = UtilLogic.dest_Trueprop (hd As)
in
state |> Proof.map_contexts (Auto2_State.map_head_th (K prop))
|> Proof.map_contexts (Auto2_State.set_induct_stmt stmt)
|> Proof.map_contexts (Auto2_State.add_prem_only stmt)
end
else
state |> Proof.map_contexts (Auto2_State.map_head_th (K prop))
end
fun strong_induct_cmd (s, t) state =
let
val {context = ctxt, ...} = Proof.goal state
val thy = Proof_Context.theory_of ctxt
val var = Syntax.read_term ctxt s
val arbitraries = map (Syntax.read_term ctxt) t
val P = get_induct_stmt ctxt (K true, [var], NONE, arbitraries)
val ind_th = get_typed_ind_th thy "strong_induct" (type_of var)
val (var_P, var_n) = ind_th |> UtilLogic.concl_of' |> Term.dest_comb
val inst = fold (Pattern.match thy) [(var_P, P), (var_n, var)] fo_init
val ind_th = Util.subst_thm ctxt inst ind_th
in
state |> apply_simple_induct_th ind_th [var] arbitraries true
end
val arbitrary =
Scan.option (Induct_ProofSteps_Keywords.arbitrary |-- Scan.repeat Parse.term)
val _ =
Outer_Syntax.command Induct_ProofSteps_Keywords.strong_induct
"apply strong induction"
((Parse.term -- arbitrary) >> (fn (s, t) =>
Toplevel.proof (fn state => strong_induct_cmd (s, these t) state)))
fun apply_induct_hyp_cmd s state =
let
val {context = ctxt, ...} = Proof.goal state
val ts = Syntax.read_terms ctxt s
val induct_stmt = Auto2_State.get_last_induct_stmt ctxt
val stmt = induct_stmt |> the |> UtilLogic.mk_Trueprop |> Thm.cterm_of ctxt
handle Option.Option =>
raise Fail "apply_induct_hyp: no induct_stmt"
val prop = Auto2_State.get_selected ctxt
val (_, (As, _)) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val _ = assert (member (op aconv) As (Thm.term_of stmt))
"apply_induct_hyp: induct_stmt not found among As."
val cAs = map (Thm.cterm_of ctxt) As
val th = stmt |> Thm.assume
|> apply_to_thm (UtilLogic.to_meta_conv ctxt)
|> fold Thm.forall_elim (map (Thm.cterm_of ctxt) ts)
|> apply_to_thm (Util.normalize_meta_all_imp ctxt)
val prems = th |> Thm.prems_of
|> map (fn t => Logic.list_implies (As, t))
|> map (Thm.cterm_of ctxt)
val prems_th = (map (Auto2_Outer.auto2_solve ctxt) prems)
|> map Util.send_all_to_hyps
val concl = th |> fold Thm.elim_implies prems_th
|> fold Thm.implies_intr (rev cAs)
val _ = writeln ("Obtained " ^
Syntax.string_of_term ctxt (Thm.concl_of concl))
in
state |> Proof.map_contexts (
Auto2_State.map_head_th (Auto2_Outer.have_after_qed ctxt concl))
end
val _ =
Outer_Syntax.command Induct_ProofSteps_Keywords.apply_induct_hyp
"apply induction hypothesis"
((Scan.repeat Parse.term) >> (fn s =>
Toplevel.proof (fn state => apply_induct_hyp_cmd s state)))
fun solve_goals ind_th pats_opt filt_As state =
let
val {context = ctxt, ...} = Proof.goal state
val (_, (As, _)) = ctxt |> Auto2_State.get_subgoal
|> Util.strip_meta_horn
val use_As = filter filt_As As
val cAs = map (Thm.cterm_of ctxt) As
val ind_goals =
ind_th |> Thm.prems_of
|> map (fn t => Logic.list_implies (use_As, t))
|> map (Thm.cterm_of ctxt)
|> map (UtilLogic.to_meta_conv ctxt)
in
case pats_opt of
NONE =>
let
fun solve_eq eq =
Thm.equal_elim (meta_sym eq)
(Auto2_Outer.auto2_solve ctxt (Thm.rhs_of eq))
val ths = ind_goals |> map solve_eq
|> map Util.send_all_to_hyps
val ind_concl = ind_th |> fold Thm.elim_implies ths
|> fold Thm.implies_intr (rev cAs)
val after_qed = Auto2_Outer.have_after_qed ctxt ind_concl
in
state |> Proof.map_contexts (Auto2_State.map_head_th after_qed)
end
| SOME pats =>
let
fun after_qed ths prop =
let
val ths' =
(ind_goals ~~ ths)
|> map (fn (eq, th) => Thm.equal_elim (meta_sym eq) th)
|> map Util.send_all_to_hyps
val ind_concl =
ind_th |> fold Thm.elim_implies ths'
|> fold Thm.implies_intr (rev cAs)
in
Auto2_Outer.have_after_qed ctxt ind_concl prop
end
val _ = writeln ("Patterns: " ^ Util.string_of_terms ctxt pats)
val new_frame =
Auto2_State.multiple_frame (
pats ~~ map Thm.rhs_of ind_goals, SOME ([], after_qed))
in
state |> Proof.map_contexts (Auto2_State.push_head new_frame)
end
end
fun case_induct_cmd s state =
let
val {context = ctxt, ...} = Proof.goal state
val thy = Proof_Context.theory_of ctxt
val start = Syntax.read_term ctxt s
val ind_th = get_term_ind_th thy "case_induct" start
val (_, (_, C)) = ctxt |> Auto2_State.get_subgoal
|> Util.strip_meta_horn
val var_P = UtilLogic.concl_of' ind_th
val inst = Pattern.match thy (var_P, UtilLogic.dest_Trueprop C) fo_init
val ind_th = Util.subst_thm_thy thy inst ind_th
in
state |> solve_goals ind_th NONE (K true)
end
val _ =
Outer_Syntax.command Induct_ProofSteps_Keywords.case_induct "apply induction"
(Parse.term >>
(fn s =>
Toplevel.proof (fn state => case_induct_cmd s state)))
val for_stmt =
Scan.option (@{keyword "for"} |-- Parse.term)
fun prop_induct_cmd (s, t) state =
let
val {context = ctxt, ...} = Proof.goal state
val thy = Proof_Context.theory_of ctxt
val start = Syntax.read_term ctxt s
val ind_th = get_term_ind_th thy "prop_induct" start
val (var_P, args) = ind_th |> UtilLogic.concl_of' |> Term.strip_comb
val start_As = UtilLogic.strip_conj start
val filt_A = (fn t => not (member (op aconv) start_As t))
val P = get_induct_stmt ctxt (filt_A, args, t, [])
val _ = writeln ("Induct statement: " ^ Syntax.string_of_term ctxt P)
val inst = Pattern.match thy (var_P, P) fo_init
val ind_th = Util.subst_thm_thy thy inst ind_th
in
state |> solve_goals ind_th NONE (K true)
end
val _ =
Outer_Syntax.command Induct_ProofSteps_Keywords.prop_induct "apply induction"
((Parse.term -- for_stmt) >>
(fn (s, t) =>
Toplevel.proof (fn state => prop_induct_cmd (s, t) state)))
fun retrieve_pat ind_vars t =
let
val (vars, (_, C)) = Util.strip_meta_horn t
fun free_to_var t =
let val (x, T) = Term.dest_Free t in Var ((x,0), T) end
val pat_vars = map free_to_var vars
val args = C |> UtilLogic.dest_Trueprop |> Util.dest_args
|> map (Term.subst_atomic (vars ~~ pat_vars))
in
HOLogic.mk_tuple (map UtilBase.mk_eq (ind_vars ~~ args))
end
fun induct_cmd ind_ty_str (s, t, u, v) state =
let
val {context = ctxt, ...} = Proof.goal state
val thy = Proof_Context.theory_of ctxt
val var = Syntax.read_term ctxt s
val arbitraries = map (Syntax.read_term ctxt) u
val filt_A = Util.occurs_frees (var :: arbitraries)
val P = get_induct_stmt ctxt (filt_A, [var], t, arbitraries)
val ind_th = get_typed_ind_th thy ind_ty_str (type_of var)
val concl = UtilLogic.concl_of' ind_th
val (var_P, var_n) = Term.dest_comb concl
val inst = fold (Pattern.match thy) [(var_P, P), (var_n, var)] fo_init
val ind_th' = Util.subst_thm_thy thy inst ind_th
val pats =
case v of
NONE => NONE
| _ => SOME (map (retrieve_pat [var]) (Thm.prems_of ind_th))
in
state |> solve_goals ind_th' pats (not o filt_A)
end
val _ =
Outer_Syntax.command Induct_ProofSteps_Keywords.induct "apply induction"
(Parse.term -- for_stmt -- arbitrary -- Scan.option Induct_ProofSteps_Keywords.with' >>
(fn (((s, t), u), v) =>
Toplevel.proof (
fn state => induct_cmd "var_induct" (s, t, these u, v) state)))
val _ =
Outer_Syntax.command Induct_ProofSteps_Keywords.cases "apply induction"
(Parse.term -- Scan.option Induct_ProofSteps_Keywords.with' >>
(fn (s, v) =>
Toplevel.proof (
fn state => induct_cmd "cases" (s, NONE, [], v) state)))
fun get_fun_induct_th thy t =
let
val ind_th =
get_term_ind_th thy "fun_induct" (Term.head_of t)
handle Fail _ =>
Global_Theory.get_thm thy (Util.get_head_name t ^ ".induct")
handle ERROR _ => raise Fail "fun_induct: cannot find theorem."
val (_, args) = Term.strip_comb t
val (_, pat_args) = ind_th |> UtilLogic.concl_of' |> Term.strip_comb
val inst = Util.first_order_match_list thy (pat_args ~~ args) fo_init
in
Util.subst_thm_thy thy inst ind_th
end
fun is_simple_fun_induct ind_th =
let
val prems = Thm.prems_of ind_th
in
if length prems > 1 then false
else let
val (var, (_, C)) = Util.strip_meta_horn (the_single prems)
val (_, args) = Term.strip_comb (UtilLogic.dest_Trueprop C)
in
eq_list (op aconv) (var, args)
end
end
fun fun_induct_cmd (s, t, u) state =
let
val {context = ctxt, ...} = Proof.goal state
val thy = Proof_Context.theory_of ctxt
val expr = Syntax.read_term ctxt s
val arbitraries = map (Syntax.read_term ctxt) t
val ind_th = get_fun_induct_th thy expr
val (var_P, vars) = ind_th |> UtilLogic.concl_of' |> Term.strip_comb
in
if is_simple_fun_induct ind_th then
let
val _ = assert (is_none u) "fun_induct: simple induction."
val P = get_induct_stmt ctxt (K true, vars, NONE, arbitraries)
val inst = Pattern.match thy (var_P, P) fo_init
val ind_th = Util.subst_thm_thy thy inst ind_th
in
state |> apply_simple_induct_th ind_th vars arbitraries false
end
else
let
val filt_A = Util.occurs_frees (vars @ arbitraries)
val P = get_induct_stmt ctxt (filt_A, vars, NONE, arbitraries)
val inst = Pattern.match thy (var_P, P) fo_init
val ind_th' = ind_th |> Util.subst_thm_thy thy inst
val prems = Thm.prems_of ind_th
val pats = case u of NONE => NONE
| SOME _ => SOME (map (retrieve_pat vars) prems)
in
state |> solve_goals ind_th' pats (not o filt_A)
end
end
val _ =
Outer_Syntax.command Induct_ProofSteps_Keywords.fun_induct "apply induction"
(Parse.term -- arbitrary -- Scan.option Induct_ProofSteps_Keywords.with' >>
(fn ((s, t), u) =>
Toplevel.proof (fn state => fun_induct_cmd (s, these t, u) state)))
end