File ‹auto2_outer.ML›
signature AUTO2_OUTER =
sig
val auto2_solve: Proof.context -> cterm -> thm
val init_state: Proof.state -> Proof.state
val refine_subgoal_th: thm -> thm -> thm
val have_resolve: Proof.context -> term list -> thm -> term -> thm
val have_after_qed: Proof.context -> thm -> thm -> thm
val have_cmd: bool * string * bool -> Proof.state -> Proof.state
val subgoal_cmd: string -> Proof.state -> Proof.state
val endgoal_cmd: Proof.state -> Proof.state
val end_cmd: Proof.state -> Proof.state
val qed_cmd: Proof.state -> Proof.context
val obtain_resolve: Proof.context -> term list -> thm -> term -> thm
val obtain_after_qed: Proof.context -> thm list -> thm -> thm
val obtain_cmd: string list * string list * bool -> Proof.state -> Proof.state
val case_resolve: Proof.context -> term list -> thm -> thm
val case_after_qed: Proof.context -> thm list -> thm -> thm
val case_cmd: string * bool -> Proof.state -> Proof.state
val contra_resolve: Proof.context -> term list -> term list -> term -> thm
val contra_after_qed: Proof.context -> thm -> thm
val contra_cmd: Proof.state -> Proof.state
val let_resolve: Proof.context -> term list -> term -> term list -> term -> thm
val let_after_qed: Proof.context -> term list -> thm -> thm
val let_cmd: string list -> Proof.state -> Proof.state
end;
signature AUTO2_KEYWORDS =
sig
val case': string * Position.T
val contradiction: string * Position.T
val end': string * Position.T
val endgoal: string * Position.T
val have: string * Position.T
val let': string * Position.T
val obtain: string * Position.T
val proof: string * Position.T
val qed: string * Position.T
val subgoal: string * Position.T
val rule: string parser
val with': string parser
end;
functor Auto2_Outer(
structure Auto2: AUTO2;
structure Auto2_Keywords: AUTO2_KEYWORDS;
structure UtilBase: UTIL_BASE;
structure UtilLogic: UTIL_LOGIC;
) : AUTO2_OUTER =
struct
fun auto2_solve ctxt stmt =
let
val goal = stmt |> Thm.trivial |> Goal.protect 1
in
(Auto2.auto2_tac ctxt goal)
|> Seq.hd |> Goal.conclude
end
fun init_state state =
let
val {goal, context = ctxt, ...} = Proof.goal state
val _ = assert (Auto2_State.get_num_frame ctxt = 0)
"init_state: state not empty."
val subgoals = goal |> Thm.cprop_of |> Drule.strip_imp_prems
val init_frame = Auto2_State.simple_frame (hd subgoals, NONE)
in
state |> Proof.map_contexts (Auto2_State.push_head init_frame)
end
val _ =
Outer_Syntax.command Auto2_Keywords.proof "begin auto2 proof"
(Scan.succeed (Toplevel.proof init_state))
fun refine_subgoal_th th prop =
let
val assum = hd (Drule.cprems_of th)
in
th |> Util.send_first_to_hyps
|> Thm.implies_elim prop
|> Thm.implies_intr assum
end
fun have_resolve ctxt vars th concl =
let
val prop = Thm.prop_of th
val (As, B) = Logic.strip_horn prop
val cAs = map (Thm.cterm_of ctxt) As
val c_vars = map (Thm.cterm_of ctxt) vars
val stmt = (Util.list_meta_horn (vars, (As @ [B], concl)))
|> Thm.cterm_of ctxt
val thAs = map Thm.assume cAs
val th_bc =
stmt |> Thm.assume
|> fold Thm.forall_elim c_vars
|> fold Thm.elim_implies thAs
val th_b = th |> fold Thm.elim_implies thAs
val th_c = Thm.implies_elim th_bc th_b
in
th_c |> fold Thm.implies_intr (rev cAs)
|> fold Thm.forall_intr (rev c_vars)
|> Thm.implies_intr stmt
end
fun have_after_qed ctxt th prop =
let
val (vars, (_, concl)) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val have_res = have_resolve ctxt vars th concl
in
refine_subgoal_th have_res prop
end
fun have_cmd (is_rule, t, is_with) state =
let
val {context = ctxt, ...} = Proof.goal state
val (vars, (assums, concl)) = t |> Syntax.read_term ctxt
|> UtilLogic.strip_obj_horn
val (_, (As, _)) = ctxt |> Auto2_State.get_subgoal
|> Util.strip_meta_horn
val stmt = Logic.list_implies (As @ map UtilLogic.mk_Trueprop assums,
UtilLogic.mk_Trueprop concl)
fun post_process th =
th |> funpow (length As) Util.send_first_to_hyps
|> fold Thm.forall_intr (rev (map (Thm.cterm_of ctxt) vars))
|> apply_to_thm (UtilLogic.to_obj_conv ctxt)
|> fold Thm.implies_intr (rev (map (Thm.cterm_of ctxt) As))
fun after_qed ths prop =
have_after_qed ctxt (post_process (the_single ths)) prop
val add_prem_only =
if is_rule then I
else Auto2_State.add_prem_only
(UtilLogic.list_obj_horn (vars, (assums, concl)))
val new_vars =
filter_out (Variable.is_fixed ctxt o fst o Term.dest_Free) vars
in
if not is_with then
let
val ctxt' = fold Util.declare_free_term new_vars ctxt
val th = auto2_solve ctxt' (Thm.cterm_of ctxt' stmt)
in
state |> Proof.map_contexts (Auto2_State.map_head_th (after_qed [th]))
|> Proof.map_contexts add_prem_only
end
else
let
val new_frame = Auto2_State.simple_frame (
Thm.cterm_of ctxt stmt, SOME ([], after_qed))
in
state |> Proof.map_contexts add_prem_only
|> Proof.map_contexts (fold Util.declare_free_term new_vars)
|> Proof.map_contexts (Auto2_State.push_head new_frame)
end
end
val read_rule =
Scan.option (Parse.$$$ "(" --| Auto2_Keywords.rule |-- Parse.$$$ ")")
val read_with =
Scan.option Auto2_Keywords.with'
val _ =
Outer_Syntax.command Auto2_Keywords.have "intermediate goal"
(read_rule -- Parse.term -- read_with >>
(fn ((rule_opt, t), with_opt) =>
Toplevel.proof
(fn state =>
have_cmd (is_some rule_opt, t, is_some with_opt) state)))
fun is_goal_resolved th =
not (Util.is_head (Logic.protectC) (Thm.concl_of th))
fun match_subgoal_pat thy t (i, pat) =
let
val inst = Pattern.first_order_match thy (pat, t) fo_init
val vars = rev (map Var (Term.add_vars pat []))
val ts = map (Util.subst_term_norm inst) vars
in
SOME (i, ts)
end
handle Pattern.MATCH => NONE
fun subgoal_cmd s state =
let
val {context = ctxt, ...} = Proof.goal state
val {goals, selected, ...} = Auto2_State.get_top_frame ctxt
val _ = assert (selected = NONE)
((fst Auto2_Keywords.subgoal) ^ ": already selected a subgoal.")
val thy = Proof_Context.theory_of ctxt
val t = Syntax.read_term ctxt s
val res = get_first (match_subgoal_pat thy t) (tag_list 0 (map fst goals))
in
case res of
NONE => error ((fst Auto2_Keywords.subgoal) ^ ": pattern not found")
| SOME (i, ts) =>
let
val prop = snd (nth goals i)
val _ = assert (not (is_goal_resolved prop))
((fst Auto2_Keywords.subgoal) ^ ": goal already resolved.")
val t' = case Thm.prop_of prop of
imp $ A $ B => imp $ Util.rename_abs_term ts A $ B
| _ => raise Fail "subgoal_cmd"
val prop = Thm.renamed_prop t' prop
val new_ts =
filter_out (Variable.is_fixed ctxt o fst o Term.dest_Free) ts
in
state |> Proof.map_contexts (Auto2_State.set_selected (SOME i))
|> Proof.map_contexts (Auto2_State.map_head_th (K prop))
|> Proof.map_contexts (fold Util.declare_free_term new_ts)
end
end
val _ =
Outer_Syntax.command Auto2_Keywords.subgoal "select subgoal"
(Parse.term >>
(fn s => Toplevel.proof (fn state => subgoal_cmd s state)))
fun auto2_solve_goal ctxt prop =
if is_goal_resolved prop then prop else
let
val (vars, (As, C)) =
prop |> Thm.prems_of |> the_single |> Util.strip_meta_horn
val body = Util.list_meta_horn ([], (As, C))
val th = auto2_solve ctxt (Thm.cterm_of ctxt body)
in
th |> fold Thm.forall_intr (rev (map (Thm.cterm_of ctxt) vars))
|> Thm.implies_elim prop
|> Goal.conclude
end
fun endgoal_cmd state =
let
val {context = ctxt, ...} = Proof.goal state
val {goals, selected, ...} = Auto2_State.get_top_frame ctxt
val _ = assert (length goals > 1 andalso is_some selected)
((fst Auto2_Keywords.endgoal) ^ ": called without a selection")
val prop = snd (nth goals (the selected))
val solved_prop = auto2_solve_goal ctxt prop
in
state |> Proof.map_contexts (Auto2_State.map_head_th (K solved_prop))
|> Proof.map_contexts (Auto2_State.set_selected NONE)
end
val _ =
Outer_Syntax.command Auto2_Keywords.endgoal "endgoal of with block"
(Scan.succeed (
Toplevel.proof (fn state => endgoal_cmd state)))
fun end_cmd state =
let
val {context = ctxt, ...} = Proof.goal state
val {goals, selected, after_qed, ...} = Auto2_State.get_top_frame ctxt
val _ = assert ((length goals = 1 andalso selected = SOME 0) orelse
(length goals > 1 andalso selected = NONE))
((fst Auto2_Keywords.end') ^ ": cannot call within an selection.")
val solved_props = map (auto2_solve_goal ctxt o snd) goals
val _ = assert (forall is_goal_resolved solved_props)
((fst Auto2_Keywords.end') ^ ": failed to resolve all goals")
val (new_vars, f) = the after_qed
in
state |> Proof.map_contexts Auto2_State.pop_head
|> Proof.map_contexts (Auto2_State.map_head_th (f solved_props))
|> Proof.map_contexts (fold Util.declare_free_term new_vars)
end
val _ =
Outer_Syntax.command Auto2_Keywords.end' "end of with block"
(Scan.succeed (
Toplevel.proof (fn state => end_cmd state)))
fun qed_cmd state =
let
val {context = ctxt, ...} = Proof.goal state
val _ = assert (Auto2_State.get_num_frame ctxt = 1)
"Qed should be applied outside any 'with' blocks"
val prop = Auto2_State.get_selected ctxt
val (vars, (As, C)) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val body = Util.list_meta_horn ([], (As, C))
val th = (auto2_solve ctxt (Thm.cterm_of ctxt body))
|> fold Thm.forall_intr (rev (map (Thm.cterm_of ctxt) vars))
val new_prop = Thm.implies_elim prop th
val method = K (Context_Tactic.CONTEXT_TACTIC (PRIMITIVE (K new_prop)))
in
state |> Proof.map_contexts (Auto2_State.map_head_th (K new_prop))
|> Proof.refine_singleton (Method.Basic (K method))
|> Proof.global_done_proof
end
val _ =
Outer_Syntax.command Auto2_Keywords.qed "end of proof"
(Scan.succeed (
Toplevel.end_proof (K qed_cmd)))
fun obtain_resolve ctxt vars th concl =
let
val prop = Thm.prop_of th
val (As, B) = Logic.strip_horn prop
val cAs = map (Thm.cterm_of ctxt) As
val c_vars = map (Thm.cterm_of ctxt) vars
val (new_vars, body) = UtilLogic.strip_exists (UtilLogic.dest_Trueprop B)
val As' = As @ [UtilLogic.mk_Trueprop body]
val stmt = (Util.list_meta_horn (vars @ new_vars, (As', concl)))
|> Thm.cterm_of ctxt
val thAs = map Thm.assume cAs
val th_b = th |> fold Thm.elim_implies thAs
val th_bc = stmt |> Thm.assume
|> fold Thm.forall_elim c_vars
|> fold Thm.forall_elim (map (Thm.cterm_of ctxt) new_vars)
|> fold Thm.elim_implies thAs
val th_c = (fold (UtilLogic.ex_elim ctxt) (rev new_vars) th_bc)
|> Thm.elim_implies th_b
in
th_c |> fold Thm.implies_intr (rev cAs)
|> fold Thm.forall_intr (rev c_vars)
|> Thm.implies_intr stmt
end
fun obtain_after_qed ctxt ths prop =
let
val th = the_single ths
val (vars, (As, C)) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val body = Util.list_meta_horn ([], (As, C))
val concl = Logic.strip_imp_concl body
val obtain_res = obtain_resolve ctxt vars th concl
in
refine_subgoal_th obtain_res prop
end
fun obtain_cmd (vars, conds, is_with) state =
let
val {context = ctxt, ...} = Proof.goal state
val (vars, conds) = (Syntax.read_terms ctxt (vars @ conds))
|> chop (length vars)
val (vars, conds) =
(map (fn t => if UtilLogic.is_mem t then dest_arg1 t else t) vars,
filter UtilLogic.is_mem vars @ conds)
val C = conds |> UtilLogic.list_conj |> fold UtilLogic.mk_exists (rev vars)
|> UtilLogic.mk_Trueprop
val (_, (As, _)) = ctxt |> Auto2_State.get_subgoal
|> Util.strip_meta_horn
val stmt = Logic.list_implies (As, C)
val new_vars =
filter_out (Variable.is_fixed ctxt o fst o Term.dest_Free) vars
val after_qed = obtain_after_qed ctxt
in
if not is_with then
let
val th = auto2_solve ctxt (Thm.cterm_of ctxt stmt)
in
state |> Proof.map_contexts (fold Util.declare_free_term new_vars)
|> Proof.map_contexts (Auto2_State.map_head_th (after_qed [th]))
end
else
let
val new_frame = Auto2_State.simple_frame (
Thm.cterm_of ctxt stmt, SOME (new_vars, after_qed))
in
state |> Proof.map_contexts (Auto2_State.push_head new_frame)
end
end
val obtain_param =
Scan.repeat Parse.term --
Scan.option (@{keyword "where"} |-- Scan.repeat Parse.term) --
read_with
val _ =
Outer_Syntax.command Auto2_Keywords.obtain "obtain variables"
(obtain_param >>
(fn ((vars, conds), with_opt) =>
Toplevel.proof (
fn state =>
obtain_cmd (vars, these conds, is_some with_opt) state)))
fun case_resolve ctxt vars th =
let
val prop = Thm.prop_of th
val ((As, B), C) = prop |> Logic.strip_horn |> apfst split_last
val cAs = map (Thm.cterm_of ctxt) As
val c_vars = map (Thm.cterm_of ctxt) vars
val nB = UtilLogic.mk_Trueprop (UtilLogic.Not $ (UtilLogic.dest_Trueprop B))
val stmt = (Util.list_meta_horn (vars, (As @ [nB], C)))
|> Thm.cterm_of ctxt
val thAs = map Thm.assume cAs
val th_nbc =
stmt |> Thm.assume
|> fold Thm.forall_elim c_vars
|> fold Thm.elim_implies thAs
val th_bc = th |> fold Thm.elim_implies thAs
val inst = fo_init |> Util.update_env (("P",0), UtilLogic.dest_Trueprop B)
|> Util.update_env (("Q",0), UtilLogic.dest_Trueprop C)
val th_c = (Util.subst_thm ctxt inst UtilBase.case_split_th)
|> fold Thm.elim_implies [th_bc, th_nbc]
in
th_c |> fold Thm.implies_intr (rev cAs)
|> fold Thm.forall_intr (rev c_vars)
|> Thm.implies_intr stmt
end
fun case_after_qed ctxt ths prop =
let
val th = the_single ths
val (vars, _) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val case_res = case_resolve ctxt vars th
in
refine_subgoal_th case_res prop
end
fun case_cmd (t, is_with) state =
let
val {context = ctxt, ...} = Proof.goal state
val B = t |> Syntax.read_term ctxt |> UtilLogic.mk_Trueprop
val (_, (As, C)) = ctxt |> Auto2_State.get_subgoal
|> Util.strip_meta_horn
val stmt = Logic.list_implies (As @ [B], C) |> Thm.cterm_of ctxt
val after_qed = case_after_qed ctxt
in
if not is_with then
let
val th = auto2_solve ctxt stmt
in
state |> Proof.map_contexts (Auto2_State.map_head_th (after_qed [th]))
end
else
let
val new_frame = Auto2_State.simple_frame (stmt, SOME ([], after_qed))
in
state |> Proof.map_contexts (Auto2_State.push_head new_frame)
end
end
val _ =
Outer_Syntax.command Auto2_Keywords.case' "intermediate case"
(Parse.term -- read_with >>
(fn (t, with_opt) =>
Toplevel.proof (fn state => case_cmd (t, is_some with_opt) state)))
fun contra_resolve ctxt vars As C =
let
val stmt = (Util.list_meta_horn (vars, (As @ [UtilLogic.get_neg' C], UtilLogic.pFalse)))
|> Thm.cterm_of ctxt
val cAs = map (Thm.cterm_of ctxt) As
val c_vars = map (Thm.cterm_of ctxt) vars
val thAs = map Thm.assume cAs
val th_c =
stmt |> Thm.assume
|> fold Thm.forall_elim c_vars
|> fold Thm.elim_implies thAs
|> apply_to_thm UtilLogic.rewrite_from_contra_form
in
th_c |> fold Thm.implies_intr (rev cAs)
|> fold Thm.forall_intr (rev c_vars)
|> Thm.implies_intr stmt
end
fun contra_after_qed ctxt prop =
let
val (vars, (As, C)) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val contra_res = contra_resolve ctxt vars As C
in
refine_subgoal_th contra_res prop
end
fun contra_cmd state =
let
val {context = ctxt, ...} = Proof.goal state
val after_qed = contra_after_qed ctxt
in
state |> Proof.map_contexts (Auto2_State.map_head_th after_qed)
end
val _ =
Outer_Syntax.command Auto2_Keywords.contradiction
"apply proof by contradiction"
(Scan.succeed (
Toplevel.proof (fn state => contra_cmd state)))
fun let_resolve ctxt vars eq As C =
let
val thy = Proof_Context.theory_of ctxt
val (lhs, rhs) = UtilBase.dest_eq eq
val pat_a = case UtilBase.ex_vardef_th |> UtilLogic.prop_of' |> dest_arg of
Abs (_, _, b) => dest_arg b
| _ => raise Fail "ex_vardef_th"
val (x, _) = Term.dest_Free lhs
val inst = Pattern.first_order_match thy (pat_a, rhs) fo_init
val ex_th = Util.subst_thm ctxt inst UtilBase.ex_vardef_th
val t' = case Thm.prop_of ex_th of
A $ (B $ Abs (_, T, body)) => A $ (B $ Abs (x, T, body))
| _ => error "let_resolve"
val ex_th =
ex_th |> Thm.renamed_prop t'
|> fold Thm.implies_intr (rev (map (Thm.cterm_of ctxt) As))
in
obtain_resolve ctxt vars ex_th C
end
fun let_after_qed ctxt eqs prop =
let
fun fold_one eq prop =
let
val (vars, (As, C)) = prop |> Thm.prems_of |> the_single
|> Util.strip_meta_horn
val let_res = let_resolve ctxt vars eq As C
in
refine_subgoal_th let_res prop
end
in
fold fold_one eqs prop
end
fun let_cmd eqs state =
let
val {context = ctxt, ...} = Proof.goal state
val eqs = Syntax.read_terms ctxt eqs
val vars = map (fst o UtilBase.dest_eq) eqs
val new_vars =
filter_out (Variable.is_fixed ctxt o fst o Term.dest_Free) vars
val after_qed = let_after_qed ctxt
in
state |> Proof.map_context (fold Util.declare_free_term new_vars)
|> Proof.map_contexts (Auto2_State.map_head_th (after_qed eqs))
end
val _ =
Outer_Syntax.command Auto2_Keywords.let' "define a variable"
(Scan.repeat Parse.term >>
(fn eqs => Toplevel.proof (fn state => let_cmd eqs state)))
end