--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/lethe_proof.ML Mon Mar 14 07:12:48 2022 +0100
@@ -0,0 +1,785 @@
+(* Title: HOL/Tools/SMT/Lethe_Proof.ML
+ Author: Mathias Fleury, ENS Rennes
+ Author: Sascha Boehme, TU Muenchen
+
+Lethe proofs: parsing and abstract syntax tree.
+*)
+
+signature LETHE_PROOF =
+sig
+ (*proofs*)
+ datatype lethe_step = Lethe_Step of {
+ id: string,
+ rule: string,
+ prems: string list,
+ proof_ctxt: term list,
+ concl: term,
+ fixes: string list}
+
+ datatype lethe_replay_node = Lethe_Replay_Node of {
+ id: string,
+ rule: string,
+ args: term list,
+ prems: string list,
+ proof_ctxt: term list,
+ concl: term,
+ bounds: (string * typ) list,
+ declarations: (string * term) list,
+ insts: term Symtab.table,
+ subproof: (string * typ) list * term list * term list * lethe_replay_node list}
+
+ val mk_replay_node: string -> string -> term list -> string list -> term list ->
+ term -> (string * typ) list -> term Symtab.table -> (string * term) list ->
+ (string * typ) list * term list * term list * lethe_replay_node list -> lethe_replay_node
+
+ (*proof parser*)
+ val parse: typ Symtab.table -> term Symtab.table -> string list ->
+ Proof.context -> lethe_step list * Proof.context
+ val parse_replay: typ Symtab.table -> term Symtab.table -> string list ->
+ Proof.context -> lethe_replay_node list * Proof.context
+
+ val step_prefix : string
+ val input_rule: string
+ val keep_app_symbols: string -> bool
+ val keep_raw_lifting: string -> bool
+ val normalized_input_rule: string
+ val la_generic_rule : string
+ val rewrite_rule : string
+ val simp_arith_rule : string
+ val lethe_deep_skolemize_rule : string
+ val lethe_def : string
+ val subproof_rule : string
+ val local_input_rule : string
+ val not_not_rule : string
+ val contract_rule : string
+ val ite_intro_rule : string
+ val eq_congruent_rule : string
+ val eq_congruent_pred_rule : string
+ val skolemization_steps : string list
+ val theory_resolution2_rule: string
+ val equiv_pos2_rule: string
+ val th_resolution_rule: string
+
+ val is_skolemization: string -> bool
+ val is_skolemization_step: lethe_replay_node -> bool
+
+ val number_of_steps: lethe_replay_node list -> int
+
+end;
+
+structure Lethe_Proof: LETHE_PROOF =
+struct
+
+open SMTLIB_Proof
+
+datatype raw_lethe_node = Raw_Lethe_Node of {
+ id: string,
+ rule: string,
+ args: SMTLIB.tree,
+ prems: string list,
+ concl: SMTLIB.tree,
+ declarations: (string * SMTLIB.tree) list,
+ subproof: raw_lethe_node list}
+
+fun mk_raw_node id rule args prems declarations concl subproof =
+ Raw_Lethe_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations,
+ concl = concl, subproof = subproof}
+
+datatype lethe_node = Lethe_Node of {
+ id: string,
+ rule: string,
+ prems: string list,
+ proof_ctxt: term list,
+ concl: term}
+
+fun mk_node id rule prems proof_ctxt concl =
+ Lethe_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl}
+
+datatype lethe_replay_node = Lethe_Replay_Node of {
+ id: string,
+ rule: string,
+ args: term list,
+ prems: string list,
+ proof_ctxt: term list,
+ concl: term,
+ bounds: (string * typ) list,
+ insts: term Symtab.table,
+ declarations: (string * term) list,
+ subproof: (string * typ) list * term list * term list * lethe_replay_node list}
+
+fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof =
+ Lethe_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
+ concl = concl, bounds = bounds, insts = insts, declarations = declarations,
+ subproof = subproof}
+
+datatype lethe_step = Lethe_Step of {
+ id: string,
+ rule: string,
+ prems: string list,
+ proof_ctxt: term list,
+ concl: term,
+ fixes: string list}
+
+fun mk_step id rule prems proof_ctxt concl fixes =
+ Lethe_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
+ fixes = fixes}
+
+val step_prefix = ".c"
+val input_rule = "input"
+val la_generic_rule = "la_generic"
+val normalized_input_rule = "__normalized_input" (*arbitrary*)
+val rewrite_rule = "__rewrite" (*arbitrary*)
+val subproof_rule = "subproof"
+val local_input_rule = "__local_input" (*arbitrary*)
+val simp_arith_rule = "simp_arith"
+val lethe_def = "__skolem_definition" (*arbitrary*)
+val not_not_rule = "not_not"
+val contract_rule = "contraction"
+val eq_congruent_pred_rule = "eq_congruent_pred"
+val eq_congruent_rule = "eq_congruent"
+val ite_intro_rule = "ite_intro"
+val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*)
+val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*)
+val equiv_pos2_rule = "equiv_pos2"
+val th_resolution_rule = "th_resolution"
+
+val skolemization_steps = ["sko_forall", "sko_ex"]
+val is_skolemization = member (op =) skolemization_steps
+val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
+val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
+val is_SH_trivial = member (op =) [not_not_rule, contract_rule]
+
+fun is_skolemization_step (Lethe_Replay_Node {id, ...}) = is_skolemization id
+
+(* Even the lethe developers do not know if the following rule can still appear in proofs: *)
+val lethe_deep_skolemize_rule = "deep_skolemize"
+
+fun number_of_steps [] = 0
+ | number_of_steps ((Lethe_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) =
+ 1 + number_of_steps subproof + number_of_steps pf
+
+(* proof parser *)
+
+fun node_of p cx =
+ ([], cx)
+ ||>> `(with_fresh_names (term_of p))
+ |>> snd
+
+fun synctactic_var_subst old_name new_name (u $ v) =
+ (synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v)
+ | synctactic_var_subst old_name new_name (Abs (v, T, u)) =
+ Abs (if String.isPrefix old_name v then new_name else v, T,
+ synctactic_var_subst old_name new_name u)
+ | synctactic_var_subst old_name new_name (Free (v, T)) =
+ if String.isPrefix old_name v then Free (new_name, T) else Free (v, T)
+ | synctactic_var_subst _ _ t = t
+
+fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) =
+ Const(\<^const_name>\<open>HOL.eq\<close>, T) $ synctactic_var_subst old_name new_name t1 $ t2
+ | synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>Trueprop\<close>, T) $ t1) =
+ Const(\<^const_name>\<open>Trueprop\<close>, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1)
+ | synctatic_rew_in_lhs_subst _ _ t = t
+
+fun add_bound_variables_to_ctxt cx =
+ fold (update_binding o
+ (fn (s, SOME typ) => (s, Term (Free (s, type_of cx typ)))))
+
+local
+ fun extract_symbols bds =
+ bds
+ |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => [([x, y], typ)]
+ | t => raise (Fail ("match error " ^ @{make_string} t)))
+ |> flat
+
+ (* onepoint can bind a variable to another variable or to a constant *)
+ fun extract_qnt_symbols cx bds =
+ bds
+ |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) =>
+ (case node_of (SMTLIB.Sym y) cx of
+ ((_, []), _) => [([x], typ)]
+ | _ => [([x, y], typ)])
+ | (SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _), typ) => [([x], typ)]
+ | t => raise (Fail ("match error " ^ @{make_string} t)))
+ |> flat
+
+ fun extract_symbols_map bds =
+ bds
+ |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _], typ) => [([x], typ)])
+ |> flat
+in
+
+fun declared_csts _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [(x, typ)]
+ | declared_csts _ "__skolem_definition" t = raise (Fail ("unrecognized skolem_definition " ^ @{make_string} t))
+ | declared_csts _ _ _ = []
+
+fun skolems_introduced_by_rule (SMTLIB.S bds) =
+ fold (fn (SMTLIB.S [SMTLIB.Sym "=", _, SMTLIB.Sym y]) => curry (op ::) y) bds []
+
+(*FIXME there is probably a way to use the information given by onepoint*)
+fun bound_vars_by_rule _ "bind" (bds) = extract_symbols bds
+ | bound_vars_by_rule cx "onepoint" bds = extract_qnt_symbols cx bds
+ | bound_vars_by_rule _ "sko_forall" bds = extract_symbols_map bds
+ | bound_vars_by_rule _ "sko_ex" bds = extract_symbols_map bds
+ | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [([x], SOME typ)]
+ | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [_, SMTLIB.Sym x, _], _)] = [([x], NONE)]
+ | bound_vars_by_rule _ _ _ = []
+
+(* Lethe adds "?" before some variables. *)
+fun remove_all_qm (SMTLIB.Sym v :: l) =
+ SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l
+ | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l'
+ | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l
+ | remove_all_qm (v :: l) = v :: remove_all_qm l
+ | remove_all_qm [] = []
+
+fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v)
+ | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l)
+ | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v
+ | remove_all_qm2 v = v
+
+end
+
+datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM
+
+fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) :
+ (raw_lethe_node list * SMTLIB.tree list * name_bindings) =
+ let
+ fun rotate_pair (a, (b, c)) = ((a, b), c)
+ fun step_kind [] = (NO_STEP, SMTLIB.S [], [])
+ | step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l)
+ | step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l)
+ | step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l)
+ | step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l)
+ | step_kind p = raise (Fail ("step_kind unrec: " ^ @{make_string} p))
+ fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ,
+ SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx =
+ (*replace the name binding by the constant instead of the full term in order to reduce
+ the size of the generated terms and therefore the reconstruction time*)
+ let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx
+ |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id))
+ in
+ (mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
+ (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
+ end
+ | parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, SMTLIB.S l]) cx =
+ let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx
+ in
+ (mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
+ (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
+ end
+ | parse_skolem t _ = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t)
+ fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx))
+ | get_id_cx t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t)
+ fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l)
+ | get_id t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t)
+ fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) =
+ (SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx))
+ | parse_source (l, cx) = (NONE, (l, cx))
+ fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx))
+ | parse_rule t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t)
+ fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx))
+ | parse_anchor_step t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t)
+ fun parse_args (SMTLIB.Key "args" :: args :: l, cx) =
+ let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx
+ in (args, (l, cx)) end
+ | parse_args (l, cx) = (SMTLIB.S [], (l, cx))
+ fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) =
+ (SMTLIB.Sym "false", (l, cx))
+ | parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) =
+ let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx
+ in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end
+ | parse_and_clausify_conclusion t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t)
+ val parse_normal_step =
+ get_id_cx
+ ##> parse_and_clausify_conclusion
+ #> rotate_pair
+ ##> parse_rule
+ #> rotate_pair
+ ##> parse_source
+ #> rotate_pair
+ ##> parse_args
+ #> rotate_pair
+
+ fun to_raw_node subproof ((((id, concl), rule), prems), args) =
+ mk_raw_node id rule args (the_default [] prems) [] concl subproof
+ fun at_discharge NONE _ = false
+ | at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2)
+ in
+ case step_kind ls of
+ (NO_STEP, _, _) => ([],[], cx)
+ | (NORMAL_STEP, p, l) =>
+ if at_discharge limit p then ([], ls, cx) else
+ let
+ (*ignores content of "discharge": Isabelle is keeping track of it via the context*)
+ val (s, (_, cx)) = (p, cx)
+ |> parse_normal_step
+ |>> (to_raw_node [])
+ val (rp, rl, cx) = parse_raw_proof_steps limit l cx
+ in (s :: rp, rl, cx) end
+ | (ASSUME, p, l) =>
+ let
+ val (id, t :: []) = p
+ |> get_id
+ val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx
+ val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t []
+ val (rp, rl, cx) = parse_raw_proof_steps limit l cx
+ in (s :: rp, rl, cx) end
+ | (ANCHOR, p, l) =>
+ let
+ val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args)
+ val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx
+ val (curss, (_, cx)) = parse_normal_step (discharge_step, cx)
+ val s = to_raw_node subproof (fst curss, anchor_args)
+ val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx
+ in (s :: rp, rl, cx) end
+ | (SKOLEM, p, l) =>
+ let
+ val (s, cx) = parse_skolem p cx
+ val (rp, rl, cx) = parse_raw_proof_steps limit l cx
+ in (s :: rp, rl, cx) end
+ end
+
+fun proof_ctxt_of_rule "bind" t = t
+ | proof_ctxt_of_rule "sko_forall" t = t
+ | proof_ctxt_of_rule "sko_ex" t = t
+ | proof_ctxt_of_rule "let" t = t
+ | proof_ctxt_of_rule "onepoint" t = t
+ | proof_ctxt_of_rule _ _ = []
+
+fun args_of_rule "bind" t = t
+ | args_of_rule "la_generic" t = t
+ | args_of_rule _ _ = []
+
+fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t
+ | insts_of_forall_inst _ _ = []
+
+fun id_of_last_step prems =
+ if null prems then []
+ else
+ let val Lethe_Replay_Node {id, ...} = List.last prems in [id] end
+
+fun extract_assumptions_from_subproof subproof =
+ let fun extract_assumptions_from_subproof (Lethe_Replay_Node {rule, concl, ...}) assms =
+ if rule = local_input_rule then concl :: assms else assms
+ in
+ fold extract_assumptions_from_subproof subproof []
+ end
+
+fun normalized_rule_name id rule =
+ (case (rule = input_rule, can SMTLIB_Interface.role_and_index_of_assert_name id) of
+ (true, true) => normalized_input_rule
+ | (true, _) => local_input_rule
+ | _ => rule)
+
+fun is_assm_repetition id rule =
+ rule = input_rule andalso can SMTLIB_Interface.role_and_index_of_assert_name id
+
+fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice)
+ | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t)
+
+(* The preprocessing takes care of:
+ 1. unfolding the shared terms
+ 2. extract the declarations of skolems to make sure that there are not unfolded
+*)
+fun preprocess compress step =
+ let
+ fun expand_assms cs =
+ map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a)
+ fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args]
+ | expand_lonely_arguments (x as SMTLIB.S [SMTLIB.Sym var, _]) = [SMTLIB.S [SMTLIB.Sym "=", x, SMTLIB.Sym var]]
+
+ fun preprocess (Raw_Lethe_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms) =
+ let
+ val (skolem_names, stripped_args) = args
+ |> (fn SMTLIB.S args => args)
+ |> map
+ (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y]
+ | x => x)
+ |> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments)
+ |> `(if rule = lethe_def then single o extract_skolem else K [])
+ ||> SMTLIB.S
+
+ val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat
+ val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms)
+ (* declare variables in the context *)
+ val declarations =
+ if rule = lethe_def
+ then skolem_names |> map (fn (name, _, choice) => (name, choice))
+ else []
+ in
+ if compress andalso rule = "or"
+ then ([], (cx, remap_assms))
+ else ([Raw_Lethe_Node {id = id, rule = rule, args = stripped_args,
+ prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}],
+ (cx, remap_assms))
+ end
+ in preprocess step end
+
+fun filter_split _ [] = ([], [])
+ | filter_split f (a :: xs) =
+ (if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs)
+
+fun extract_types_of_args (SMTLIB.S [var, typ, t as SMTLIB.S [SMTLIB.Sym "choice", _, _]]) =
+ (SMTLIB.S [var, typ, t], SOME typ)
+ |> single
+ | extract_types_of_args (SMTLIB.S t) =
+ let
+ fun extract_types_of_arg (SMTLIB.S [eq, SMTLIB.S [var, typ], t]) = (SMTLIB.S [eq, var, t], SOME typ)
+ | extract_types_of_arg t = (t, NONE)
+ in
+ t
+ |> map extract_types_of_arg
+ end
+
+fun collect_skolem_defs (Raw_Lethe_Node {rule, subproof = subproof, args, ...}) =
+ (if is_skolemization rule then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule args) else []) @
+ flat (map collect_skolem_defs subproof)
+
+(*The postprocessing does:
+ 1. translate the terms to Isabelle syntax, taking care of free variables
+ 2. remove the ambiguity in the proof terms:
+ x \<leadsto> y |- x = x
+ means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term
+ by:
+ xy \<leadsto> y |- xy = x.
+ This is now does not have an ambiguity and we can safely move the "xy \<leadsto> y" to the proof
+ assumptions.
+*)
+fun postprocess_proof compress ctxt step cx =
+ let
+ fun postprocess (Raw_Lethe_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) =
+ let
+ val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl))
+
+ val args = extract_types_of_args args
+ val globally_bound_vars = declared_csts cx rule args
+ val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ)))))
+ globally_bound_vars cx
+
+ (*find rebound variables specific to the LHS of the equivalence symbol*)
+ val bound_vars = bound_vars_by_rule cx rule args
+ val bound_vars_no_typ = map fst bound_vars
+ val rhs_vars =
+ fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars_no_typ []
+
+ fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso
+ not (member (op =) rhs_vars t)
+ val (shadowing_vars, rebound_lhs_vars) = bound_vars
+ |> filter_split (fn ([t, _], typ) => not_already_bound cx t | _ => true)
+ |>> map (apfst (hd))
+ |>> (fn vars => vars @ flat (map (fn ([_, t], typ) => [(t, typ)] | _ => []) bound_vars))
+ val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t'))
+ (map fst rebound_lhs_vars) rew
+ val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t')
+ subproof_rew
+
+ val ((concl, bounds), cx') = node_of concl cx
+
+ val extra_lhs_vars = map (fn ([a,b], typ) => (a, a^b, typ)) rebound_lhs_vars
+ val old_lhs_vars = map (fn (a, _, typ) => (a, typ)) extra_lhs_vars
+ val new_lhs_vars = map (fn (_, newvar, typ) => (newvar, typ)) extra_lhs_vars
+
+ (* postprocess conclusion *)
+ val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl)
+
+ val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl))
+ val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx',
+ "bound_vars =", bound_vars))
+
+ val bound_tvars =
+ map (fn (s, SOME typ) => (s, type_of cx typ))
+ (shadowing_vars @ new_lhs_vars)
+ val subproof_cx =
+ add_bound_variables_to_ctxt cx (shadowing_vars @ new_lhs_vars) cx
+
+ fun could_unify (Bound i, Bound j) = i = j
+ | could_unify (Var v, Var v') = v = v'
+ | could_unify (Free v, Free v') = v = v'
+ | could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty'
+ | could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy')
+ | could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v')
+ | could_unify _ = false
+ fun is_alpha_renaming t =
+ t
+ |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq
+ |> could_unify
+ handle TERM _ => false
+ val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl
+
+ val can_remove_subproof =
+ compress andalso (is_skolemization rule orelse alpha_conversion)
+ val (fixed_subproof : lethe_replay_node list, _) =
+ fold_map postprocess (if can_remove_subproof then [] else subproof)
+ (subproof_cx, subproof_rew)
+
+ val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter
+
+ (* postprocess assms *)
+ val stripped_args = map fst args
+ val sanitized_args = proof_ctxt_of_rule rule stripped_args
+
+ val arg_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ old_lhs_vars) subproof_cx
+ val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst)
+ val normalized_args = map unsk_and_rewrite termified_args
+
+ val subproof_assms = proof_ctxt_of_rule rule normalized_args
+
+ (* postprocess arguments *)
+ val rule_args = args_of_rule rule stripped_args
+ val (termified_args, _) = fold_map term_of rule_args subproof_cx
+ val normalized_args = map unsk_and_rewrite termified_args
+ val rule_args = map subproof_rewriter normalized_args
+
+ val raw_insts = insts_of_forall_inst rule stripped_args
+ fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end
+ val (termified_args, _) = fold_map termify_term raw_insts subproof_cx
+ val insts = Symtab.empty
+ |> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args
+ |> Symtab.map (K unsk_and_rewrite)
+
+ (* declarations *)
+ val (declarations, _) = fold_map termify_term declarations cx
+ |> apfst (map (apsnd unsk_and_rewrite))
+
+ (* fix step *)
+ val _ = if bounds <> [] then raise (Fail "found dangling variable in concl") else ()
+
+ val skolem_defs = (if is_skolemization rule
+ then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule (SMTLIB.S (map fst args))) else [])
+ val skolems_of_subproof = (if is_skolemization rule
+ then flat (map collect_skolem_defs subproof) else [])
+ val fixed_prems =
+ prems @ (if is_assm_repetition id rule then [id] else []) @
+ skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof)
+
+ (* fix subproof *)
+ val normalized_rule = normalized_rule_name id rule
+ |> (if compress andalso alpha_conversion then K "refl" else I)
+
+ val extra_assms2 =
+ (if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else [])
+
+ val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl
+ [] insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof)
+
+ in
+ (step, (cx', rew))
+ end
+ in
+ postprocess step (cx, [])
+ |> (fn (step, (cx, _)) => (step, cx))
+ end
+
+fun combine_proof_steps ((step1 : lethe_replay_node) :: step2 :: steps) =
+ let
+ val (Lethe_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1,
+ proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1,
+ declarations = declarations1,
+ subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1
+ val (Lethe_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2,
+ proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2,
+ declarations = declarations2,
+ subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2
+ val goals1 =
+ (case concl1 of
+ _ $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $
+ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.Not\<close>, _) $a) $ b)) => [a,b]
+ | _ => [])
+ val goal2 = (case concl2 of _ $ a => a)
+ in
+ if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1
+ andalso member (op =) goals1 goal2
+ then
+ mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2)
+ proof_ctxt2 concl2 bounds2 insts2 declarations2
+ (bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) ::
+ combine_proof_steps steps
+ else
+ mk_replay_node id1 rule1 args1 prems1
+ proof_ctxt1 concl1 bounds1 insts1 declarations1
+ (bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) ::
+ combine_proof_steps (step2 :: steps)
+ end
+ | combine_proof_steps steps = steps
+
+
+val linearize_proof =
+ let
+ fun map_node_concl f (Lethe_Node {id, rule, prems, proof_ctxt, concl}) =
+ mk_node id rule prems proof_ctxt (f concl)
+ fun linearize (Lethe_Replay_Node {id = id, rule = rule, args = _, prems = prems,
+ proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _,
+ subproof = (bounds', assms, inputs, subproof)}) =
+ let
+ val bounds = distinct (op =) bounds
+ val bounds' = distinct (op =) bounds'
+ fun mk_prop_of_term concl =
+ concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close>
+ fun remove_assumption_id assumption_id prems =
+ filter_out (curry (op =) assumption_id) prems
+ fun add_assumption assumption concl =
+ \<^Const>\<open>Pure.imp for \<open>mk_prop_of_term assumption\<close> \<open>mk_prop_of_term concl\<close>\<close>
+ fun inline_assumption assumption assumption_id
+ (Lethe_Node {id, rule, prems, proof_ctxt, concl}) =
+ mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
+ (add_assumption assumption concl)
+ fun find_input_steps_and_inline [] = []
+ | find_input_steps_and_inline
+ (Lethe_Node {id = id', rule, prems, concl, ...} :: steps) =
+ if rule = input_rule then
+ find_input_steps_and_inline (map (inline_assumption concl id') steps)
+ else
+ mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps
+
+ fun free_bounds bounds (concl) =
+ fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl
+ val subproof = subproof
+ |> flat o map linearize
+ |> map (map_node_concl (fold add_assumption (assms @ inputs)))
+ |> map (map_node_concl (free_bounds (bounds @ bounds')))
+ |> find_input_steps_and_inline
+ val concl = free_bounds bounds concl
+ in
+ subproof @ [mk_node id rule prems proof_ctxt concl]
+ end
+ in linearize end
+
+fun rule_of (Lethe_Replay_Node {rule,...}) = rule
+fun subproof_of (Lethe_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof
+
+
+(* Massage Skolems for Sledgehammer.
+
+We have to make sure that there is an "arrow" in the graph for skolemization steps.
+
+
+A. The normal easy case
+
+This function detects the steps of the form
+ P \<longleftrightarrow> Q :skolemization
+ Q :resolution with P
+and replace them by
+ Q :skolemization
+Throwing away the step "P \<longleftrightarrow> Q" completely. This throws away a lot of information, but it does not
+matter too much for Sledgehammer.
+
+
+B. Skolems in subproofs
+Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer
+does not support more features like definitions. lethe is able to generate proofs with skolemization
+happening in subproofs inside the formula.
+ (assume "A \<or> P"
+ ...
+ P \<longleftrightarrow> Q :skolemization in the subproof
+ ...)
+ hence A \<or> P \<longrightarrow> A \<or> Q :lemma
+ ...
+ R :something with some rule
+and replace them by
+ R :skolemization with some rule
+Without any subproof
+*)
+fun remove_skolem_definitions_proof steps =
+ let
+ fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\<open>HOL.eq\<close>, typ) $ arg1) $ arg2)) =
+ judgement $ ((Const(\<^const_name>\<open>HOL.implies\<close>, typ) $ arg1) $ arg2)
+ | replace_equivalent_by_imp a = a (*This case is probably wrong*)
+ fun remove_skolem_definitions (Lethe_Replay_Node {id = id, rule = rule, args = args,
+ prems = prems,
+ proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts,
+ declarations = declarations,
+ subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) =
+ let
+ val prems = prems
+ |> filter_out (member (op =) prems_to_remove)
+ val trivial_step = is_SH_trivial rule
+ fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st)
+ else fold has_skolem_substep (subproof_of st) NONE
+ | has_skolem_substep _ a = a
+ val promote_to_skolem = exists (fn t => member (op =) skolems t) prems
+ val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE
+ val promote_step = promote_to_skolem orelse promote_from_assms
+ val skolem_step_to_skip = is_skolemization rule orelse
+ (promote_from_assms andalso length prems > 1)
+ val is_skolem = is_skolemization rule orelse promote_step
+ val prems = prems
+ |> filter_out (fn t => member (op =) skolems t)
+ |> is_skolem ? filter_out (String.isPrefix id)
+ val rule = (if promote_step then default_skolem_rule else rule)
+ val subproof = subproof
+ |> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*)
+ |> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems)))
+ (*no new definitions in subproofs*)
+ |> flat
+ val concl = concl
+ |> is_skolem ? replace_equivalent_by_imp
+ val step = (if skolem_step_to_skip orelse rule = lethe_def orelse trivial_step then []
+ else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations
+ (vars, assms', extra_assms', subproof)
+ |> single)
+ val defs = (if rule = lethe_def orelse trivial_step then id :: prems_to_remove
+ else prems_to_remove)
+ val skolems = (if skolem_step_to_skip then id :: skolems else skolems)
+ in
+ (step, (defs, skolems))
+ end
+ in
+ fold_map remove_skolem_definitions steps ([], [])
+ |> fst
+ |> flat
+ end
+
+local
+ (*TODO useful?*)
+ fun remove_pattern (SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.S _])) = t
+ | remove_pattern (SMTLIB.S xs) = SMTLIB.S (map remove_pattern xs)
+ | remove_pattern p = p
+
+ fun import_proof_and_post_process typs funs lines ctxt =
+ let
+ val compress = SMT_Config.compress_verit_proofs ctxt
+ val smtlib_lines_without_qm =
+ lines
+ |> map single
+ |> map SMTLIB.parse
+ |> map remove_all_qm2
+ |> map remove_pattern
+ val (raw_steps, _, _) =
+ parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding
+
+ fun process step (cx, cx') =
+ let fun postprocess step (cx, cx') =
+ let val (step, cx) = postprocess_proof compress ctxt step cx
+ in (step, (cx, cx')) end
+ in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end
+ val step =
+ (empty_context ctxt typs funs, [])
+ |> fold_map process raw_steps
+ |> (fn (steps, (cx, _)) => (flat steps, cx))
+ |> compress? apfst combine_proof_steps
+ in step end
+in
+
+fun parse typs funs lines ctxt =
+ let
+ val (u, env) = import_proof_and_post_process typs funs lines ctxt
+ val t = u
+ |> remove_skolem_definitions_proof
+ |> flat o (map linearize_proof)
+ fun node_to_step (Lethe_Node {id, rule, prems, concl, ...}) =
+ mk_step id rule prems [] concl []
+ in
+ (map node_to_step t, ctxt_of env)
+ end
+
+fun parse_replay typs funs lines ctxt =
+ let
+ val (u, env) = import_proof_and_post_process typs funs lines ctxt
+ val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u)
+ in
+ (u, ctxt_of env)
+ end
+end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML Mon Mar 14 07:12:48 2022 +0100
@@ -0,0 +1,1191 @@
+(* Title: HOL/Tools/SMT/verit_replay_methods.ML
+ Author: Mathias Fleury, MPII, JKU, University Freiburg
+
+Proof method for replaying veriT proofs.
+*)
+
+signature LETHE_REPLAY_METHODS =
+sig
+
+
+ datatype verit_rule =
+ False | True |
+
+ (*input: a repeated (normalized) assumption of assumption of in a subproof*)
+ Normalized_Input | Local_Input |
+ (*Subproof:*)
+ Subproof |
+ (*Conjunction:*)
+ And | Not_And | And_Pos | And_Neg |
+ (*Disjunction""*)
+ Or | Or_Pos | Not_Or | Or_Neg |
+ (*Disjunction:*)
+ Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 |
+ (*Equivalence:*)
+ Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 |
+ (*If-then-else:*)
+ ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 |
+ (*Equality:*)
+ Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong |
+ (*Arithmetics:*)
+ LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq |
+ NLA_Generic |
+ (*Quantifiers:*)
+ Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex |
+ (*Resolution:*)
+ Theory_Resolution | Resolution |
+ (*Temporary rules, that the verit developers want to remove:*)
+ AC_Simp |
+ Bfun_Elim |
+ Qnt_CNF |
+ (*Used to introduce skolem constants*)
+ Definition |
+ (*Former cong rules*)
+ Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify |
+ Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify |
+ Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify | All_Simplify |
+ Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals |
+ (*Unsupported rule*)
+ Unsupported |
+ (*For compression*)
+ Theory_Resolution2 |
+ (*Extended rules*)
+ Symm | Not_Symm | Reordering | Tmp_Quantifier_Simplify
+
+ val requires_subproof_assms : string list -> string -> bool
+ val requires_local_input: string list -> string -> bool
+
+ val string_of_verit_rule: verit_rule -> string
+
+ type lethe_tac_args = Proof.context -> thm list -> term list -> term -> thm
+ type lethe_tac = Proof.context -> thm list -> term -> thm
+ type lethe_tac2 = Proof.context -> thm list -> term list -> term Symtab.table -> term -> thm
+ val bind: lethe_tac_args
+ val and_rule: lethe_tac
+ val and_neg_rule: lethe_tac
+ val and_pos: lethe_tac
+ val rewrite_and_simplify: lethe_tac
+ val rewrite_bool_simplify: lethe_tac
+ val rewrite_comp_simplify: lethe_tac
+ val rewrite_minus_simplify: lethe_tac
+ val rewrite_not_simplify: lethe_tac
+ val rewrite_eq_simplify: lethe_tac
+ val rewrite_equiv_simplify: lethe_tac
+ val rewrite_implies_simplify: lethe_tac
+ val rewrite_or_simplify: lethe_tac
+ val cong: lethe_tac
+ val rewrite_connective_def: lethe_tac
+ val duplicate_literals: lethe_tac
+ val eq_congruent: lethe_tac
+ val eq_congruent_pred: lethe_tac
+ val eq_reflexive: lethe_tac
+ val eq_transitive: lethe_tac
+ val equiv1: lethe_tac
+ val equiv2: lethe_tac
+ val equiv_neg1: lethe_tac
+ val equiv_neg2: lethe_tac
+ val equiv_pos1: lethe_tac
+ val equiv_pos2: lethe_tac
+ val false_rule: lethe_tac
+ val forall_inst: lethe_tac2
+ val implies_rules: lethe_tac
+ val implies_neg1: lethe_tac
+ val implies_neg2: lethe_tac
+ val implies_pos: lethe_tac
+ val ite1: lethe_tac
+ val ite2: lethe_tac
+ val ite_intro: lethe_tac
+ val ite_neg1: lethe_tac
+ val ite_neg2: lethe_tac
+ val ite_pos1: lethe_tac
+ val ite_pos2: lethe_tac
+ val rewrite_ite_simplify: lethe_tac
+ val la_disequality: lethe_tac
+ val la_generic: lethe_tac_args
+ val la_rw_eq: lethe_tac
+ val lia_generic: lethe_tac
+ val refl: lethe_tac
+ val normalized_input: lethe_tac
+ val not_and_rule: lethe_tac
+ val not_equiv1: lethe_tac
+ val not_equiv2: lethe_tac
+ val not_implies1: lethe_tac
+ val not_implies2: lethe_tac
+ val not_ite1: lethe_tac
+ val not_ite2: lethe_tac
+ val not_not: lethe_tac
+ val not_or_rule: lethe_tac
+ val or: lethe_tac
+ val or_neg_rule: lethe_tac
+ val or_pos_rule: lethe_tac
+ val theory_resolution2: lethe_tac
+ val prod_simplify: lethe_tac
+ val qnt_join: lethe_tac
+ val qnt_rm_unused: lethe_tac
+ val onepoint: lethe_tac
+ val qnt_simplify: lethe_tac
+ val all_simplify: lethe_tac
+ val unit_res: lethe_tac
+ val skolem_ex: lethe_tac
+ val skolem_forall: lethe_tac
+ val subproof: lethe_tac
+ val sum_simplify: lethe_tac
+ val tautological_clause: lethe_tac
+ val tmp_AC_rule: lethe_tac
+ val bfun_elim: lethe_tac
+ val qnt_cnf: lethe_tac
+ val trans: lethe_tac
+ val symm: lethe_tac
+ val not_symm: lethe_tac
+ val reordering: lethe_tac
+
+(*
+ val : lethe_tac
+*)
+ val REPEAT_CHANGED: ('a -> tactic) -> 'a -> tactic
+ val TRY': ('a -> tactic) -> 'a -> tactic
+
+end;
+
+
+structure Lethe_Replay_Methods: LETHE_REPLAY_METHODS =
+struct
+
+type lethe_tac_args = Proof.context -> thm list -> term list -> term -> thm
+type lethe_tac = Proof.context -> thm list -> term -> thm
+type lethe_tac2 = Proof.context -> thm list -> term list -> term Symtab.table -> term -> thm
+
+(*Some general comments on the proof format:
+ 1. Double negations are not always removed. This means for example that the equivalence rules
+ cannot assume that the double negations have already been removed. Therefore, we match the
+ term, instantiate the theorem, then use simp (to remove double negations), and finally use
+ assumption.
+ 2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule
+ is doing much more that is supposed to do. Moreover types can make trivial goals (for the
+ boolean structure) impossible to prove.
+ 3. Duplicate literals are sometimes removed, mostly by the SAT solver.
+
+ Rules unsupported on purpose:
+ * Distinct_Elim, XOR, let (we don't need them).
+ * deep_skolemize (because it is not clear if verit still generates using it).
+*)
+
+
+datatype verit_rule =
+ False | True |
+
+ (*input: a repeated (normalized) assumption of assumption of in a subproof*)
+ Normalized_Input | Local_Input |
+ (*Subproof:*)
+ Subproof |
+ (*Conjunction:*)
+ And | Not_And | And_Pos | And_Neg |
+ (*Disjunction""*)
+ Or | Or_Pos | Not_Or | Or_Neg |
+ (*Disjunction:*)
+ Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 |
+ (*Equivalence:*)
+ Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 |
+ (*If-then-else:*)
+ ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 |
+ (*Equality:*)
+ Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong |
+ (*Arithmetics:*)
+ LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq |
+ NLA_Generic |
+ (*Quantifiers:*)
+ Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex |
+ (*Resolution:*)
+ Theory_Resolution | Resolution |
+ (*Temporary rules, that the verit developpers want to remove:*)
+ AC_Simp |
+ Bfun_Elim |
+ Qnt_CNF |
+ (*Used to introduce skolem constants*)
+ Definition |
+ (*Former cong rules*)
+ Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify |
+ Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify |
+ Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify | All_Simplify |
+ Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals |
+ (*Unsupported rule*)
+ Unsupported |
+ (*For compression*)
+ Theory_Resolution2 |
+ (*Extended rules*)
+ Symm | Not_Symm | Reordering | Tmp_Quantifier_Simplify
+
+fun string_of_verit_rule Bind = "Bind"
+ | string_of_verit_rule Cong = "Cong"
+ | string_of_verit_rule Refl = "Refl"
+ | string_of_verit_rule Equiv1 = "Equiv1"
+ | string_of_verit_rule Equiv2 = "Equiv2"
+ | string_of_verit_rule Equiv_pos1 = "Equiv_pos1"
+ | string_of_verit_rule Equiv_pos2 = "Equiv_pos2"
+ | string_of_verit_rule Equiv_neg1 = "Equiv_neg1"
+ | string_of_verit_rule Equiv_neg2 = "Equiv_neg2"
+ | string_of_verit_rule Skolem_Forall = "Skolem_Forall"
+ | string_of_verit_rule Skolem_Ex = "Skolem_Ex"
+ | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive"
+ | string_of_verit_rule Theory_Resolution = "Theory_Resolution"
+ | string_of_verit_rule Theory_Resolution2 = "Theory_Resolution2"
+ | string_of_verit_rule Forall_Inst = "forall_inst"
+ | string_of_verit_rule Or = "Or"
+ | string_of_verit_rule Not_Or = "Not_Or"
+ | string_of_verit_rule Resolution = "Resolution"
+ | string_of_verit_rule Eq_Congruent = "eq_congruent"
+ | string_of_verit_rule Trans = "trans"
+ | string_of_verit_rule False = "false"
+ | string_of_verit_rule And = "and"
+ | string_of_verit_rule And_Pos = "and_pos"
+ | string_of_verit_rule Not_And = "not_and"
+ | string_of_verit_rule And_Neg = "and_neg"
+ | string_of_verit_rule Or_Pos = "or_pos"
+ | string_of_verit_rule Or_Neg = "or_neg"
+ | string_of_verit_rule AC_Simp = "ac_simp"
+ | string_of_verit_rule Not_Equiv1 = "not_equiv1"
+ | string_of_verit_rule Not_Equiv2 = "not_equiv2"
+ | string_of_verit_rule Not_Implies1 = "not_implies1"
+ | string_of_verit_rule Not_Implies2 = "not_implies2"
+ | string_of_verit_rule Implies_Neg1 = "implies_neg1"
+ | string_of_verit_rule Implies_Neg2 = "implies_neg2"
+ | string_of_verit_rule Implies = "implies"
+ | string_of_verit_rule Bfun_Elim = "bfun_elim"
+ | string_of_verit_rule ITE1 = "ite1"
+ | string_of_verit_rule ITE2 = "ite2"
+ | string_of_verit_rule Not_ITE1 = "not_ite1"
+ | string_of_verit_rule Not_ITE2 = "not_ite2"
+ | string_of_verit_rule ITE_Pos1 = "ite_pos1"
+ | string_of_verit_rule ITE_Pos2 = "ite_pos2"
+ | string_of_verit_rule ITE_Neg1 = "ite_neg1"
+ | string_of_verit_rule ITE_Neg2 = "ite_neg2"
+ | string_of_verit_rule ITE_Intro = "ite_intro"
+ | string_of_verit_rule LA_Disequality = "la_disequality"
+ | string_of_verit_rule LA_Generic = "la_generic"
+ | string_of_verit_rule LIA_Generic = "lia_generic"
+ | string_of_verit_rule LA_Tautology = "la_tautology"
+ | string_of_verit_rule LA_RW_Eq = "la_rw_eq"
+ | string_of_verit_rule LA_Totality = "LA_Totality"
+ | string_of_verit_rule NLA_Generic = "nla_generic"
+ | string_of_verit_rule Eq_Transitive = "eq_transitive"
+ | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused"
+ | string_of_verit_rule Onepoint = "onepoint"
+ | string_of_verit_rule Qnt_Join = "qnt_join"
+ | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred"
+ | string_of_verit_rule Normalized_Input = Lethe_Proof.normalized_input_rule
+ | string_of_verit_rule Local_Input = Lethe_Proof.local_input_rule
+ | string_of_verit_rule Subproof = "subproof"
+ | string_of_verit_rule Bool_Simplify = "bool_simplify"
+ | string_of_verit_rule Equiv_Simplify = "equiv_simplify"
+ | string_of_verit_rule Eq_Simplify = "eq_simplify"
+ | string_of_verit_rule Not_Simplify = "not_simplify"
+ | string_of_verit_rule And_Simplify = "and_simplify"
+ | string_of_verit_rule Or_Simplify = "or_simplify"
+ | string_of_verit_rule ITE_Simplify = "ite_simplify"
+ | string_of_verit_rule Implies_Simplify = "implies_simplify"
+ | string_of_verit_rule Connective_Def = "connective_def"
+ | string_of_verit_rule Minus_Simplify = "minus_simplify"
+ | string_of_verit_rule Sum_Simplify = "sum_simplify"
+ | string_of_verit_rule Prod_Simplify = "prod_simplify"
+ | string_of_verit_rule All_Simplify = "all_simplify"
+ | string_of_verit_rule Comp_Simplify = "comp_simplify"
+ | string_of_verit_rule Qnt_Simplify = "qnt_simplify"
+ | string_of_verit_rule Symm = "symm"
+ | string_of_verit_rule Not_Symm = "not_symm"
+ | string_of_verit_rule Reordering = "reordering"
+ | string_of_verit_rule Not_Not = Lethe_Proof.not_not_rule
+ | string_of_verit_rule Tautological_Clause = "tautology"
+ | string_of_verit_rule Duplicate_Literals = Lethe_Proof.contract_rule
+ | string_of_verit_rule Qnt_CNF = "qnt_cnf"
+ | string_of_verit_rule r = "Unknown rule: " ^ \<^make_string> r
+
+fun replay_error ctxt msg rule thms t =
+ SMT_Replay_Methods.replay_error ctxt msg (string_of_verit_rule rule) thms t
+
+(* utility function *)
+
+fun eqsubst_all ctxt thms =
+ K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_asm_tac ctxt [0] thms))
+ THEN' K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_tac ctxt [0] thms))
+
+fun simplify_tac ctxt thms =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
+ |> Simplifier.asm_full_simp_tac
+
+(* sko_forall requires the assumptions to be able to prove the equivalence in case of double
+skolemization. See comment below. *)
+fun requires_subproof_assms _ t =
+ member (op =) ["refl", "sko_forall", "sko_ex", "cong"] t
+
+fun requires_local_input _ t =
+ member (op =) [Lethe_Proof.local_input_rule] t
+
+(*This is a weaker simplification form. It is weaker, but is also less likely to loop*)
+fun partial_simplify_tac ctxt thms =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
+ |> Simplifier.full_simp_tac
+
+val try_provers = SMT_Replay_Methods.try_provers "verit"
+
+fun TRY' tac = fn i => TRY (tac i)
+fun REPEAT' tac = fn i => REPEAT (tac i)
+fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i))
+
+
+(* Bind *)
+
+(*The bind rule is non-obvious due to the handling of quantifiers:
+ "\<And>x y a. x = y ==> (\<forall>b. P a b x) \<longleftrightarrow> (\<forall>b. P' a b y)"
+ ------------------------------------------------------
+ \<forall>a. (\<forall>b x. P a b x) \<longleftrightarrow> (\<forall>b y. P' a b y)
+is a valid application.*)
+
+val bind_thms =
+ [@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
+ @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
+ @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
+ @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
+
+val bind_thms_same_name =
+ [@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
+ @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
+ @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
+ @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
+
+fun extract_quantified_names_q (_ $ Abs (name, _, t)) =
+ apfst (curry (op ::) name) (extract_quantified_names_q t)
+ | extract_quantified_names_q t = ([], t)
+
+fun extract_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, ty, t)) =
+ (name, ty) :: (extract_forall_quantified_names_q t)
+ | extract_forall_quantified_names_q _ = []
+
+fun extract_all_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, _, t)) =
+ name :: (extract_all_forall_quantified_names_q t)
+ | extract_all_forall_quantified_names_q (t $ u) =
+ extract_all_forall_quantified_names_q t @ extract_all_forall_quantified_names_q u
+ | extract_all_forall_quantified_names_q _ = []
+
+val extract_quantified_names_ba =
+ SMT_Replay_Methods.dest_prop
+ #> extract_quantified_names_q
+ ##> HOLogic.dest_eq
+ ##> fst
+ ##> extract_quantified_names_q
+ ##> fst
+
+val extract_quantified_names =
+ extract_quantified_names_ba
+ #> (op @)
+
+val extract_all_forall_quantified_names =
+ SMT_Replay_Methods.dest_prop
+ #> HOLogic.dest_eq
+ #> fst
+ #> extract_all_forall_quantified_names_q
+
+
+fun extract_all_exists_quantified_names_q (Const(\<^const_name>\<open>HOL.Ex\<close>, _) $ Abs (name, _, t)) =
+ name :: (extract_all_exists_quantified_names_q t)
+ | extract_all_exists_quantified_names_q (t $ u) =
+ extract_all_exists_quantified_names_q t @ extract_all_exists_quantified_names_q u
+ | extract_all_exists_quantified_names_q _ = []
+
+val extract_all_exists_quantified_names =
+ SMT_Replay_Methods.dest_prop
+ #> HOLogic.dest_eq
+ #> fst
+ #> extract_all_exists_quantified_names_q
+
+
+val extract_bind_names =
+ HOLogic.dest_eq
+ #> apply2 (fn (Free (name, _)) => name)
+
+fun combine_quant ctxt ((n1, n2) :: bounds) (n1' :: formula) =
+ TRY' (if n1 = n1'
+ then if n1 <> n2
+ then
+ resolve_tac ctxt bind_thms
+ THEN' TRY'(resolve_tac ctxt [@{thm refl}])
+ THEN' combine_quant ctxt bounds formula
+ else resolve_tac ctxt bind_thms_same_name THEN' combine_quant ctxt bounds formula
+ else resolve_tac ctxt @{thms allI} THEN' combine_quant ctxt ((n1, n2) :: bounds) formula)
+ | combine_quant _ _ _ = K all_tac
+
+fun bind_quants ctxt args t =
+ combine_quant ctxt (map extract_bind_names args) (extract_quantified_names t)
+
+fun generalize_prems_q [] prems = prems
+ | generalize_prems_q (_ :: quants) prems =
+ generalize_prems_q quants (@{thm spec} OF [prems])
+
+fun generalize_prems t = generalize_prems_q (fst (extract_quantified_names_ba t))
+
+fun bind ctxt [prems] args t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ bind_quants ctxt args t
+ THEN' TRY' (SOLVED' (resolve_tac ctxt [generalize_prems t prems]
+ THEN_ALL_NEW TRY' (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms refl}))))
+ | bind ctxt thms _ t = replay_error ctxt "invalid bind application" Bind thms t
+
+
+(* Congruence/Refl *)
+
+fun cong ctxt thms = try_provers ctxt
+ (string_of_verit_rule Cong) [
+ ("basic", SMT_Replay_Methods.cong_basic ctxt thms),
+ ("unfolding then reflexivity", SMT_Replay_Methods.cong_unfolding_trivial ctxt thms),
+ ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms),
+ ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms
+
+fun refl ctxt thm t =
+ (case find_first (fn thm => t = Thm.full_prop_of thm) thm of
+ SOME thm => thm
+ | NONE =>
+ (case try (fn t => SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}) t of
+ NONE => cong ctxt thm t
+ | SOME thm => thm))
+
+(* Instantiation *)
+
+local
+fun dropWhile _ [] = []
+ | dropWhile f (x :: xs) = if f x then dropWhile f xs else x :: xs
+in
+
+fun forall_inst ctxt _ _ insts t =
+ let
+ fun instantiate_and_solve i ({context = ctxt, prems = [prem], ...}: Subgoal.focus) =
+ let
+ val t = Thm.prop_of prem
+ val quants = t
+ |> SMT_Replay_Methods.dest_prop
+ |> extract_forall_quantified_names_q
+ val insts = map (Symtab.lookup insts o fst) (rev quants)
+ |> dropWhile (curry (op =) NONE)
+ |> rev
+ fun option_map _ NONE = NONE
+ | option_map f (SOME a) = SOME (f a)
+ fun instantiate_with inst prem =
+ Drule.infer_instantiate' ctxt [NONE, inst] @{thm spec} OF [prem]
+ val inst_thm =
+ fold instantiate_with
+ (map (option_map (Thm.cterm_of ctxt)) insts)
+ prem
+ in
+ (Method.insert_tac ctxt [inst_thm]
+ THEN' TRY' (fn i => assume_tac ctxt i)
+ THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) i
+ end
+ | instantiate_and_solve _ ({context = ctxt, prems = thms, ...}: Subgoal.focus) =
+ replay_error ctxt "invalid application" Forall_Inst thms t
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ match_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
+ THEN' (fn i => Subgoal.FOCUS (instantiate_and_solve i) ctxt i))
+ end
+end
+
+
+(* Or *)
+
+fun or _ (thm :: _) _ = thm
+ | or ctxt thms t = replay_error ctxt "invalid bind application" Or thms t
+
+
+(* Implication *)
+
+val implies_pos_thm =
+ [@{lemma \<open>\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B\<close> by blast},
+ @{lemma \<open>\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B\<close> by blast}]
+
+fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt implies_pos_thm)
+
+(* Skolemization *)
+
+fun extract_rewrite_rule_assumption _ thms =
+ let
+ fun is_rewrite_rule thm =
+ (case Thm.prop_of thm of
+ \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Free(_, _)) => true
+ | _ => false)
+ fun is_context_rule thm =
+ (case Thm.prop_of thm of
+ \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ Free(_, _) $ Free(_, _)) => true
+ | _ => false)
+ val ctxt_eq =
+ thms
+ |> filter is_context_rule
+ val rew =
+ thms
+ |> filter_out is_context_rule
+ |> filter is_rewrite_rule
+ in
+ (ctxt_eq, rew)
+ end
+
+local
+ fun rewrite_all_skolems thm_indirect ctxt (SOME thm :: thms) =
+ EqSubst.eqsubst_tac ctxt [0] [thm_indirect OF [thm]]
+ THEN' (partial_simplify_tac ctxt (@{thms eq_commute}))
+ THEN' rewrite_all_skolems thm_indirect ctxt thms
+ | rewrite_all_skolems thm_indirect ctxt (NONE :: thms) = rewrite_all_skolems thm_indirect ctxt thms
+ | rewrite_all_skolems _ _ [] = K (all_tac)
+
+ fun extract_var_name (thm :: thms) =
+ let val name = Thm.concl_of thm
+ |> SMT_Replay_Methods.dest_prop
+ |> HOLogic.dest_eq
+ |> fst
+ |> (fn Const(_,_) $ Abs(name, _, _) => [(name,@{thm sym} OF [thm])]
+ | _ => [])
+ in name :: extract_var_name thms end
+ | extract_var_name [] = []
+
+fun skolem_tac extractor thm1 thm2 ctxt thms t =
+ let
+ val (ctxt_eq, ts) = extract_rewrite_rule_assumption ctxt thms
+ fun ordered_definitions () =
+ let
+ val var_order = extractor t
+ val thm_names_with_var = extract_var_name ts |> flat
+ in map (AList.lookup (op =) thm_names_with_var) var_order end
+
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ K (unfold_tac ctxt ctxt_eq)
+ THEN' ((SOLVED' (K (unfold_tac ctxt (map (fn thm => thm1 OF [@{thm sym} OF [thm]]) ts))))
+ ORELSE'
+ (rewrite_all_skolems thm2 ctxt (ordered_definitions ())
+ THEN' partial_simplify_tac ctxt @{thms eq_commute})))
+ end
+in
+
+val skolem_forall =
+ skolem_tac extract_all_forall_quantified_names @{thm verit_sko_forall_indirect}
+ @{thm verit_sko_forall_indirect2}
+
+val skolem_ex =
+ skolem_tac extract_all_exists_quantified_names @{thm verit_sko_ex_indirect}
+ @{thm verit_sko_ex_indirect2}
+
+end
+
+fun eq_reflexive ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}
+
+local
+ fun not_not_prove ctxt _ =
+ K (unfold_tac ctxt @{thms not_not})
+ THEN' match_tac ctxt @{thms verit_or_simplify_1}
+
+ fun duplicate_literals_prove ctxt prems =
+ Method.insert_tac ctxt prems
+ THEN' match_tac ctxt @{thms ccontr}
+ THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
+ THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE})
+ THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE})
+ THEN' REPEAT' (ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt))
+
+ fun tautological_clause_prove ctxt _ =
+ match_tac ctxt @{thms verit_or_neg}
+ THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]})
+ THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt)
+
+ val theory_resolution2_lemma = @{lemma \<open>a \<Longrightarrow> a = b \<Longrightarrow> b\<close> by blast}
+
+in
+
+fun prove_abstract abstracter tac ctxt thms t =
+ let
+ val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
+ val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
+ val (_, t2) = Logic.dest_equals (Thm.prop_of t')
+ val thm =
+ SMT_Replay_Methods.prove_abstract ctxt thms t2 tac (
+ fold_map (abstracter o SMT_Replay_Methods.dest_thm) thms ##>>
+ abstracter (SMT_Replay_Methods.dest_prop t2))
+ in
+ @{thm verit_Pure_trans} OF [t', thm]
+ end
+
+val not_not = prove_abstract SMT_Replay_Methods.abstract_bool_shallow not_not_prove
+
+val tautological_clause =
+ prove_abstract SMT_Replay_Methods.abstract_bool_shallow tautological_clause_prove
+
+val duplicate_literals =
+ prove_abstract SMT_Replay_Methods.abstract_bool_shallow duplicate_literals_prove
+
+val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac
+
+(*match_instantiate does not work*)
+fun theory_resolution2 ctxt prems t =
+ SMT_Replay_Methods.prove ctxt t (fn _ => match_tac ctxt [theory_resolution2_lemma OF prems])
+
+end
+
+
+fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems
+ THEN' TRY' (K (unfold_tac ctxt @{thms SMT.trigger_def}))
+ THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute}))
+
+val false_rule_thm = @{lemma \<open>\<not>False\<close> by blast}
+
+fun false_rule ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t false_rule_thm
+
+
+(* Transitivity *)
+
+val trans_bool_thm =
+ @{lemma \<open>P = Q \<Longrightarrow> Q \<Longrightarrow> P\<close> by blast}
+
+fun trans ctxt thms t =
+ let
+ val prop_of = HOLogic.dest_Trueprop o Thm.full_prop_of
+ fun combine_thms [thm1, thm2] =
+ (case (prop_of thm1, prop_of thm2) of
+ ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2),
+ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ t4)) =>
+ if t2 aconv t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
+ else if t2 aconv t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans})))
+ else if t1 aconv t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans}))
+ else raise Fail "invalid trans theorem"
+ | _ => trans_bool_thm OF [thm1, thm2])
+ | combine_thms (thm1 :: thm2 :: thms) =
+ combine_thms (combine_thms [thm1, thm2] :: thms)
+ | combine_thms thms = replay_error ctxt "invalid bind application" Trans thms t
+ val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
+ val (_, t2) = Logic.dest_equals (Thm.prop_of t')
+ val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
+ val trans_thm = combine_thms thms
+ in
+ (case (prop_of trans_thm, t2) of
+ ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _),
+ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ _)) =>
+ if t1 aconv t3 then trans_thm else trans_thm RS sym
+ | _ => trans_thm (*to be on the safe side*))
+ end
+
+
+fun tmp_AC_rule ctxt thms t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt thms
+ THEN' REPEAT_ALL_NEW (partial_simplify_tac ctxt @{thms eq_commute}
+ THEN' TRY' (simplify_tac ctxt @{thms ac_simps conj_ac})
+ THEN' TRY' (Classical.fast_tac ctxt)))
+
+
+(* And/Or *)
+
+local
+ fun not_and_rule_prove ctxt prems =
+ Method.insert_tac ctxt prems
+ THEN' K (unfold_tac ctxt @{thms de_Morgan_conj})
+ THEN_ALL_NEW TRY' (assume_tac ctxt)
+
+ fun or_pos_prove ctxt _ =
+ K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
+ THEN' match_tac ctxt @{thms verit_and_pos}
+ THEN' K (unfold_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not})
+ THEN' TRY' (assume_tac ctxt)
+
+ fun not_or_rule_prove ctxt prems =
+ Method.insert_tac ctxt prems
+ THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
+ THEN' TRY' (REPEAT' (match_tac ctxt @{thms conjI}))
+ THEN_ALL_NEW ((REPEAT' (ematch_tac ctxt @{thms conjE}))
+ THEN' TRY' (assume_tac ctxt))
+
+ fun and_rule_prove ctxt prems =
+ Method.insert_tac ctxt prems
+ THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1)))
+ THEN' TRY' (assume_tac ctxt)
+
+ fun and_neg_rule_prove ctxt _ =
+ match_tac ctxt @{thms verit_and_neg}
+ THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not})
+ THEN' TRY' (assume_tac ctxt)
+
+ fun prover tac = prove_abstract SMT_Replay_Methods.abstract_prop tac
+
+in
+
+val and_rule = prover and_rule_prove
+
+val not_and_rule = prover not_and_rule_prove
+
+val not_or_rule = prover not_or_rule_prove
+
+val or_pos_rule = prover or_pos_prove
+
+val and_neg_rule = prover and_neg_rule_prove
+
+val or_neg_rule = prove_abstract SMT_Replay_Methods.abstract_bool (fn ctxt => fn _ =>
+ resolve_tac ctxt @{thms verit_or_neg}
+ THEN' K (unfold_tac ctxt @{thms not_not})
+ THEN_ALL_NEW
+ (REPEAT'
+ (SOLVED' (match_tac ctxt @{thms disjI1} THEN_ALL_NEW assume_tac ctxt)
+ ORELSE' (match_tac ctxt @{thms disjI2} THEN' TRY' (assume_tac ctxt)))))
+
+fun and_pos ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos})
+ THEN' TRY' (assume_tac ctxt))
+
+end
+
+
+(* Equivalence Transformation *)
+
+local
+ fun prove_equiv equiv_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [equiv_thm OF [thm]]
+ THEN' TRY' (assume_tac ctxt))
+ | prove_equiv _ ctxt thms t = replay_error ctxt "invalid application in some equiv rule" Unsupported thms t
+in
+
+val not_equiv1 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B\<close> by blast}
+val not_equiv2 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B\<close> by blast}
+val equiv1 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B\<close> by blast}
+val equiv2 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B\<close> by blast}
+val not_implies1 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow> B) \<Longrightarrow> A\<close> by blast}
+val not_implies2 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B\<close> by blast}
+
+end
+
+
+(* Equivalence Lemma *)
+(*equiv_pos2 is very important for performance. We have tried various tactics, including
+a specialisation of SMT_Replay_Methods.match_instantiate, but there never was a measurable
+and consistent gain.*)
+local
+ fun prove_equiv_pos_neg2 thm ctxt _ t =
+ SMT_Replay_Methods.match_instantiate ctxt t thm
+in
+
+val equiv_pos1_thm = @{lemma \<open>\<not>(a \<longleftrightarrow> b) \<or> a \<or> \<not>b\<close> by blast+}
+val equiv_pos1 = prove_equiv_pos_neg2 equiv_pos1_thm
+
+val equiv_pos2_thm = @{lemma \<open>\<And>a b. (a \<noteq> b) \<or> \<not>a \<or> b\<close> by blast+}
+val equiv_pos2 = prove_equiv_pos_neg2 equiv_pos2_thm
+
+val equiv_neg1_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> \<not>a \<or> \<not>b\<close> by blast+}
+val equiv_neg1 = prove_equiv_pos_neg2 equiv_neg1_thm
+
+val equiv_neg2_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> a \<or> b\<close> by blast}
+val equiv_neg2 = prove_equiv_pos_neg2 equiv_neg2_thm
+
+end
+
+
+local
+ fun implies_pos_neg_term ctxt thm (\<^term>\<open>Trueprop\<close> $
+ (\<^term>\<open>HOL.disj\<close> $ (\<^term>\<open>HOL.implies\<close> $ a $ b) $ _)) =
+ Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
+ | implies_pos_neg_term ctxt thm t =
+ replay_error ctxt "invalid application in Implies" Unsupported [thm] t
+
+ fun prove_implies_pos_neg thm ctxt _ t =
+ let val thm = implies_pos_neg_term ctxt thm t
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [thm]
+ THEN' TRY' (assume_tac ctxt))
+ end
+in
+
+val implies_neg1_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> a\<close> by blast}
+val implies_neg1 = prove_implies_pos_neg implies_neg1_thm
+
+val implies_neg2_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> \<not>b\<close> by blast}
+val implies_neg2 = prove_implies_pos_neg implies_neg2_thm
+
+val implies_thm = @{lemma \<open>(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b\<close> by blast}
+fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [implies_thm OF prems]
+ THEN' TRY' (assume_tac ctxt))
+
+end
+
+
+(* BFun *)
+
+local
+ val bfun_theorems = @{thms verit_bfun_elim}
+in
+
+fun bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems
+ THEN' TRY' (eqsubst_all ctxt bfun_theorems)
+ THEN' TRY' (simplify_tac ctxt @{thms eq_commute all_conj_distrib ex_disj_distrib}))
+
+end
+
+
+(* If-Then-Else *)
+
+local
+ fun prove_ite ite_thm thm ctxt =
+ resolve_tac ctxt [ite_thm OF [thm]]
+ THEN' TRY' (assume_tac ctxt)
+in
+
+val ite_pos1_thm =
+ @{lemma \<open>\<not>(if x then P else Q) \<or> x \<or> Q\<close> by auto}
+
+fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [ite_pos1_thm])
+
+val ite_pos2_thms =
+ @{lemma \<open>\<not>(if x then P else Q) \<or> \<not>x \<or> P\<close> \<open>\<not>(if \<not>x then P else Q) \<or> x \<or> P\<close> by auto}
+
+fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_pos2_thms)
+
+val ite_neg1_thms =
+ @{lemma \<open>(if x then P else Q) \<or> x \<or> \<not>Q\<close> \<open>(if x then P else \<not>Q) \<or> x \<or> Q\<close> by auto}
+
+fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg1_thms)
+
+val ite_neg2_thms =
+ @{lemma \<open>(if x then P else Q) \<or> \<not>x \<or> \<not>P\<close> \<open>(if \<not>x then P else Q) \<or> x \<or> \<not>P\<close>
+ \<open>(if x then \<not>P else Q) \<or> \<not>x \<or> P\<close> \<open>(if \<not>x then \<not>P else Q) \<or> x \<or> P\<close>
+ by auto}
+
+fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg2_thms)
+
+val ite1_thm =
+ @{lemma \<open>(if x then P else Q) \<Longrightarrow> x \<or> Q\<close> by (auto split: if_splits) }
+
+fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite1_thm thm ctxt)
+
+val ite2_thm =
+ @{lemma \<open>(if x then P else Q) \<Longrightarrow> \<not>x \<or> P\<close> by (auto split: if_splits) }
+
+fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite2_thm thm ctxt)
+
+val not_ite1_thm =
+ @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q\<close> by (auto split: if_splits) }
+
+fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite1_thm thm ctxt)
+
+val not_ite2_thm =
+ @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P\<close> by (auto split: if_splits) }
+
+fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite2_thm thm ctxt)
+
+(*ite_intro can introduce new terms that are in the proof exactly the sames as the old one, but are
+not internally, hence the possible reordering.*)
+fun ite_intro ctxt _ t =
+ let
+ fun simplify_ite ctxt thms =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel})
+ |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong}
+ |> Simplifier.full_simp_tac
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt []
+ THEN' TRY' (simplify_ite ctxt @{thms eq_commute}))
+ end
+end
+
+
+(* Quantifiers *)
+
+local
+ val rm_unused = @{lemma \<open>(\<forall>x. P) = P\<close> \<open>(\<exists>x. P) = P\<close> by blast+}
+
+ fun qnt_cnf_tac ctxt =
+ simplify_tac ctxt @{thms de_Morgan_conj de_Morgan_disj imp_conv_disj
+ iff_conv_conj_imp if_bool_eq_disj ex_simps all_simps ex_disj_distrib
+ verit_connective_def(3) all_conj_distrib}
+ THEN' TRY' (Blast.blast_tac ctxt)
+in
+fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ K (unfold_tac ctxt rm_unused))
+
+fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems
+ THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt)
+ addsimps @{thms HOL.simp_thms HOL.all_simps}
+ addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}])
+ THEN' TRY' (Blast.blast_tac ctxt)
+ THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt []))
+
+fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t Classical.fast_tac
+
+fun qnt_cnf ctxt _ t = SMT_Replay_Methods.prove ctxt t qnt_cnf_tac
+
+fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ partial_simplify_tac ctxt [])
+
+end
+
+(* Equality *)
+
+fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}])
+ THEN' REPEAT' (resolve_tac ctxt @{thms impI})
+ THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
+ THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1))
+ THEN' resolve_tac ctxt @{thms refl})
+
+local
+ fun find_rew rews t t' =
+ (case AList.lookup (op =) rews (t, t') of
+ SOME thm => SOME (thm COMP @{thm symmetric})
+ | NONE =>
+ (case AList.lookup (op =) rews (t', t) of
+ SOME thm => SOME thm
+ | NONE => NONE))
+
+ fun eq_pred_conv rews t ctxt ctrm =
+ (case find_rew rews t (Thm.term_of ctrm) of
+ SOME thm => Conv.rewr_conv thm ctrm
+ | NONE =>
+ (case t of
+ f $ arg =>
+ (Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv
+ Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm
+ | Abs (_, _, f) => Conv.abs_conv (eq_pred_conv rews f o snd) ctxt ctrm
+ | _ => Conv.all_conv ctrm))
+
+ fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) =
+ let
+ val rews = prems
+ |> map_filter (try (apfst (HOLogic.dest_eq o Thm.term_of o Object_Logic.dest_judgment ctxt o
+ Thm.cconcl_of) o `(fn x => x)))
+ |> map (apsnd (fn x => @{thm eq_reflection} OF [x]))
+ fun conv_left conv = Conv.arg_conv (Conv.arg_conv conv)
+ fun conv_left_neg conv = Conv.arg_conv (Conv.arg_conv (Conv.arg_conv conv))
+ val (t1, conv_term) =
+ (case Thm.term_of (Object_Logic.dest_judgment ctxt concl) of
+ Const(_, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ t1) $ _ => (t1, conv_left)
+ | Const(_, _) $ t1 $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ _) => (t1, conv_left_neg)
+ | Const(_, _) $ t1 $ _ => (t1, conv_left)
+ | t1 => (t1, conv_left))
+ fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
+ in
+ throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt))
+ end
+in
+
+fun eq_congruent_pred ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}])
+ THEN' (fn i => Subgoal.FOCUS (fn focus => eq_pred_rewrite_tac focus i) ctxt i)
+ THEN' (resolve_tac ctxt @{thms refl excluded_middle excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]}
+ ORELSE' assume_tac ctxt))
+
+val eq_congruent = eq_congruent_pred
+
+end
+
+
+(* Subproof *)
+
+fun subproof ctxt [prem] t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (REPEAT' (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}],
+ @{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]])
+ THEN' resolve_tac ctxt [prem]
+ THEN_ALL_NEW assume_tac ctxt
+ THEN' TRY' (assume_tac ctxt))
+ ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt))
+ | subproof ctxt prems t =
+ replay_error ctxt "invalid application, only one assumption expected" Subproof prems t
+
+
+(* Simplifying Steps *)
+
+(* The reconstruction is a bit tricky: At first we only rewrite only based on the rules that are
+passed as argument. Then we simply use simp_thms to reconstruct all the proofs (and these theorems
+cover all the simplification below).
+*)
+local
+ fun rewrite_only_thms ctxt thms =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps thms)
+ |> Simplifier.full_simp_tac
+ fun rewrite_only_thms_tmp ctxt thms =
+ rewrite_only_thms ctxt thms
+ THEN' TRY' (K (Clasimp.auto_tac ctxt)) (*TODO: TEMP until cvc5 produces fine grained simplification steps *)
+
+ fun rewrite_thms ctxt thms =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
+ |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms})
+ |> Simplifier.full_simp_tac
+
+ fun chain_rewrite_thms ctxt thms =
+ TRY' (rewrite_only_thms ctxt thms)
+ THEN' TRY' (rewrite_thms ctxt thms)
+ THEN' TRY' (K (Clasimp.auto_tac ctxt)) (*TODO: TEMP until cvc5 produces fine grained simplification steps *)
+
+ fun chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 =
+ TRY' (rewrite_only_thms ctxt thms1)
+ THEN' TRY' (rewrite_thms ctxt thms2)
+ THEN' TRY' (K (Clasimp.auto_tac ctxt)) (*TODO: TEMP until cvc5 produces fine grained simplification steps *)
+
+ fun chain_rewrite_thms_two_step ctxt thms1 thms2 thms3 thms4 =
+ chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2
+ THEN' TRY' (chain_rewrite_two_step_with_ac_simps ctxt thms3 thms4)
+
+ val imp_refl = @{lemma \<open>(P \<longrightarrow> P) = True\<close> by blast}
+
+in
+fun rewrite_bool_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (chain_rewrite_thms ctxt @{thms verit_bool_simplify}))
+
+fun rewrite_and_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_and_simplify verit_and_simplify1}
+ @{thms verit_and_simplify}))
+
+fun rewrite_or_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_or_simplify verit_or_simplify_1}
+ @{thms verit_or_simplify})
+ THEN' TRY' (REPEAT' (match_tac ctxt @{thms verit_and_pos}) THEN' assume_tac ctxt))
+
+fun rewrite_not_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (rewrite_only_thms_tmp ctxt @{thms verit_not_simplify}))
+
+fun rewrite_equiv_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (rewrite_only_thms_tmp ctxt @{thms verit_equiv_simplify}))
+
+fun rewrite_eq_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (chain_rewrite_two_step_with_ac_simps ctxt
+ @{thms verit_eq_simplify}
+ (Named_Theorems.get ctxt @{named_theorems ac_simps})))
+
+fun rewrite_implies_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (rewrite_only_thms_tmp ctxt @{thms verit_implies_simplify}))
+
+(* It is more efficient to first fold the implication symbols.
+ That is however not enough when symbols appears within
+ expressions, hence we also unfold implications in the
+ other direction. *)
+fun rewrite_connective_def ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ chain_rewrite_thms_two_step ctxt
+ (imp_refl :: @{thms not_not verit_connective_def[symmetric]})
+ (@{thms verit_connective_def[symmetric]})
+ (imp_refl :: @{thms not_not verit_connective_def})
+ (@{thms verit_connective_def}))
+
+fun rewrite_minus_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ chain_rewrite_two_step_with_ac_simps ctxt
+ @{thms arith_simps verit_minus_simplify}
+ (Named_Theorems.get ctxt @{named_theorems ac_simps} @
+ @{thms numerals arith_simps arith_special
+ numeral_class.numeral.numeral_One}))
+
+fun rewrite_comp_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ chain_rewrite_thms ctxt @{thms verit_comp_simplify})
+
+fun rewrite_ite_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (rewrite_only_thms_tmp ctxt @{thms verit_ite_simplify}))
+end
+
+
+(* Simplifications *)
+
+local
+ fun simplify_arith ctxt thms = partial_simplify_tac ctxt
+ (thms @ Named_Theorems.get ctxt @{named_theorems ac_simps} @ @{thms arith_simps})
+in
+
+fun sum_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ simplify_arith ctxt @{thms verit_sum_simplify arith_special}
+ THEN' TRY' (K (Clasimp.auto_tac ctxt))) (*TODO: TEMP until cvc5 produces fine grained simplification steps *)
+
+fun prod_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ simplify_arith ctxt @{thms verit_prod_simplify}
+ THEN' TRY' (K (Clasimp.auto_tac ctxt))) (*TODO: TEMP until cvc5 produces fine grained simplification steps *)
+end
+
+fun all_simplify ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ TRY' (K (Clasimp.auto_tac ctxt))) (*TODO: TEMP until cvc5 produces fine grained simplification steps *)
+
+(* Arithmetics *)
+local
+
+val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close> by auto}
+in
+fun la_rw_eq ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t la_rw_eq_thm
+
+fun la_generic_prove args ctxt _ = SMT_Replay_Arith.la_farkas args ctxt
+
+fun la_generic ctxt _ args =
+ prove_abstract (SMT_Replay_Methods.abstract_arith_shallow ctxt) (la_generic_prove args) ctxt []
+
+fun lia_generic ctxt _ t =
+ SMT_Replay_Methods.prove_arith_rewrite SMT_Replay_Methods.abstract_neq ctxt t
+
+fun la_disequality ctxt _ t =
+ SMT_Replay_Methods.match_instantiate ctxt t @{thm verit_la_disequality}
+
+end
+
+
+(* Symm and Not_Symm*)
+
+local
+ fun prove_symm symm_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [symm_thm OF [thm]]
+ THEN' TRY' (assume_tac ctxt))
+ | prove_symm _ ctxt thms t = replay_error ctxt "invalid application in some symm rule" Unsupported thms t
+in
+ val symm_thm =
+ @{lemma \<open>(B = A) \<Longrightarrow> A = B\<close> by blast }
+ val symm = prove_symm symm_thm
+
+ val not_symm_thm =
+ @{lemma \<open>\<not>(B = A) \<Longrightarrow> \<not>(A = B)\<close> by blast }
+ val not_symm = prove_symm not_symm_thm
+end
+
+(* Reordering *)
+local
+ fun prove_reordering ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>(
+ Method.insert_tac ctxt [thm]
+ THEN' match_tac ctxt @{thms ccontr}
+ THEN' K (unfold_tac ctxt @{thms de_Morgan_disj})
+ THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE})
+ THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE})
+ THEN' REPEAT'(ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt))
+ ))
+ | prove_reordering ctxt thms t =
+ replay_error ctxt "invalid application in some reordering rule" Unsupported thms t
+in
+ val reordering = prove_reordering
+end
+
+end;
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML Tue Mar 22 19:08:47 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Mon Mar 14 07:12:48 2022 +0100
@@ -10,9 +10,6 @@
val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table ->
(string * term) list -> term -> thm
- val requires_subproof_assms : string list -> string -> bool
- val requires_local_input: string list -> string -> bool
- val eq_congruent_pred: Proof.context -> 'a -> term -> thm
val discharge: Proof.context -> thm list -> term -> thm
end;
@@ -20,63 +17,7 @@
structure Verit_Replay_Methods: VERIT_REPLAY_METHODS =
struct
-(*Some general comments on the proof format:
- 1. Double negations are not always removed. This means for example that the equivalence rules
- cannot assume that the double negations have already been removed. Therefore, we match the
- term, instantiate the theorem, then use simp (to remove double negations), and finally use
- assumption.
- 2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule
- is doing much more that is supposed to do. Moreover types can make trivial goals (for the
- boolean structure) impossible to prove.
- 3. Duplicate literals are sometimes removed, mostly by the SAT solver.
-
- Rules unsupported on purpose:
- * Distinct_Elim, XOR, let (we don't need them).
- * deep_skolemize (because it is not clear if verit still generates using it).
-*)
-
-datatype verit_rule =
- False | True |
-
- (*input: a repeated (normalized) assumption of assumption of in a subproof*)
- Normalized_Input | Local_Input |
- (*Subproof:*)
- Subproof |
- (*Conjunction:*)
- And | Not_And | And_Pos | And_Neg |
- (*Disjunction""*)
- Or | Or_Pos | Not_Or | Or_Neg |
- (*Disjunction:*)
- Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 |
- (*Equivalence:*)
- Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 |
- (*If-then-else:*)
- ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 |
- (*Equality:*)
- Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong |
- (*Arithmetics:*)
- LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq |
- NLA_Generic |
- (*Quantifiers:*)
- Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex |
- (*Resolution:*)
- Theory_Resolution | Resolution |
- (*Temporary rules, that the verit developpers want to remove:*)
- AC_Simp |
- Bfun_Elim |
- Qnt_CNF |
- (*Used to introduce skolem constants*)
- Definition |
- (*Former cong rules*)
- Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify |
- Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify |
- Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify |
- Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals |
- (*Unsupported rule*)
- Unsupported |
- (*For compression*)
- Theory_Resolution2
-
+open Lethe_Replay_Methods
fun verit_rule_of "bind" = Bind
| verit_rule_of "cong" = Cong
@@ -149,944 +90,19 @@
| verit_rule_of "tautology" = Tautological_Clause
| verit_rule_of "qnt_cnf" = Qnt_CNF
| verit_rule_of r =
- if r = Verit_Proof.normalized_input_rule then Normalized_Input
- else if r = Verit_Proof.local_input_rule then Local_Input
- else if r = Verit_Proof.veriT_def then Definition
- else if r = Verit_Proof.not_not_rule then Not_Not
- else if r = Verit_Proof.contract_rule then Duplicate_Literals
- else if r = Verit_Proof.ite_intro_rule then ITE_Intro
- else if r = Verit_Proof.eq_congruent_rule then Eq_Congruent
- else if r = Verit_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred
- else if r = Verit_Proof.theory_resolution2_rule then Theory_Resolution2
- else if r = Verit_Proof.th_resolution_rule then Theory_Resolution
- else if r = Verit_Proof.equiv_pos2_rule then Equiv_pos2
+ if r = Lethe_Proof.normalized_input_rule then Normalized_Input
+ else if r = Lethe_Proof.local_input_rule then Local_Input
+ else if r = Lethe_Proof.lethe_def then Definition
+ else if r = Lethe_Proof.not_not_rule then Not_Not
+ else if r = Lethe_Proof.contract_rule then Duplicate_Literals
+ else if r = Lethe_Proof.ite_intro_rule then ITE_Intro
+ else if r = Lethe_Proof.eq_congruent_rule then Eq_Congruent
+ else if r = Lethe_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred
+ else if r = Lethe_Proof.theory_resolution2_rule then Theory_Resolution2
+ else if r = Lethe_Proof.th_resolution_rule then Theory_Resolution
+ else if r = Lethe_Proof.equiv_pos2_rule then Equiv_pos2
else (@{print} ("Unsupport rule", r); Unsupported)
-fun string_of_verit_rule Bind = "Bind"
- | string_of_verit_rule Cong = "Cong"
- | string_of_verit_rule Refl = "Refl"
- | string_of_verit_rule Equiv1 = "Equiv1"
- | string_of_verit_rule Equiv2 = "Equiv2"
- | string_of_verit_rule Equiv_pos1 = "Equiv_pos1"
- | string_of_verit_rule Equiv_pos2 = "Equiv_pos2"
- | string_of_verit_rule Equiv_neg1 = "Equiv_neg1"
- | string_of_verit_rule Equiv_neg2 = "Equiv_neg2"
- | string_of_verit_rule Skolem_Forall = "Skolem_Forall"
- | string_of_verit_rule Skolem_Ex = "Skolem_Ex"
- | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive"
- | string_of_verit_rule Theory_Resolution = "Theory_Resolution"
- | string_of_verit_rule Theory_Resolution2 = "Theory_Resolution2"
- | string_of_verit_rule Forall_Inst = "forall_inst"
- | string_of_verit_rule Or = "Or"
- | string_of_verit_rule Not_Or = "Not_Or"
- | string_of_verit_rule Resolution = "Resolution"
- | string_of_verit_rule Eq_Congruent = "eq_congruent"
- | string_of_verit_rule Trans = "trans"
- | string_of_verit_rule False = "false"
- | string_of_verit_rule And = "and"
- | string_of_verit_rule And_Pos = "and_pos"
- | string_of_verit_rule Not_And = "not_and"
- | string_of_verit_rule And_Neg = "and_neg"
- | string_of_verit_rule Or_Pos = "or_pos"
- | string_of_verit_rule Or_Neg = "or_neg"
- | string_of_verit_rule AC_Simp = "ac_simp"
- | string_of_verit_rule Not_Equiv1 = "not_equiv1"
- | string_of_verit_rule Not_Equiv2 = "not_equiv2"
- | string_of_verit_rule Not_Implies1 = "not_implies1"
- | string_of_verit_rule Not_Implies2 = "not_implies2"
- | string_of_verit_rule Implies_Neg1 = "implies_neg1"
- | string_of_verit_rule Implies_Neg2 = "implies_neg2"
- | string_of_verit_rule Implies = "implies"
- | string_of_verit_rule Bfun_Elim = "bfun_elim"
- | string_of_verit_rule ITE1 = "ite1"
- | string_of_verit_rule ITE2 = "ite2"
- | string_of_verit_rule Not_ITE1 = "not_ite1"
- | string_of_verit_rule Not_ITE2 = "not_ite2"
- | string_of_verit_rule ITE_Pos1 = "ite_pos1"
- | string_of_verit_rule ITE_Pos2 = "ite_pos2"
- | string_of_verit_rule ITE_Neg1 = "ite_neg1"
- | string_of_verit_rule ITE_Neg2 = "ite_neg2"
- | string_of_verit_rule ITE_Intro = "ite_intro"
- | string_of_verit_rule LA_Disequality = "la_disequality"
- | string_of_verit_rule LA_Generic = "la_generic"
- | string_of_verit_rule LIA_Generic = "lia_generic"
- | string_of_verit_rule LA_Tautology = "la_tautology"
- | string_of_verit_rule LA_RW_Eq = "la_rw_eq"
- | string_of_verit_rule LA_Totality = "LA_Totality"
- | string_of_verit_rule NLA_Generic = "nla_generic"
- | string_of_verit_rule Eq_Transitive = "eq_transitive"
- | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused"
- | string_of_verit_rule Onepoint = "onepoint"
- | string_of_verit_rule Qnt_Join = "qnt_join"
- | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred"
- | string_of_verit_rule Normalized_Input = Verit_Proof.normalized_input_rule
- | string_of_verit_rule Local_Input = Verit_Proof.local_input_rule
- | string_of_verit_rule Subproof = "subproof"
- | string_of_verit_rule Bool_Simplify = "bool_simplify"
- | string_of_verit_rule Equiv_Simplify = "equiv_simplify"
- | string_of_verit_rule Eq_Simplify = "eq_simplify"
- | string_of_verit_rule Not_Simplify = "not_simplify"
- | string_of_verit_rule And_Simplify = "and_simplify"
- | string_of_verit_rule Or_Simplify = "or_simplify"
- | string_of_verit_rule ITE_Simplify = "ite_simplify"
- | string_of_verit_rule Implies_Simplify = "implies_simplify"
- | string_of_verit_rule Connective_Def = "connective_def"
- | string_of_verit_rule Minus_Simplify = "minus_simplify"
- | string_of_verit_rule Sum_Simplify = "sum_simplify"
- | string_of_verit_rule Prod_Simplify = "prod_simplify"
- | string_of_verit_rule Comp_Simplify = "comp_simplify"
- | string_of_verit_rule Qnt_Simplify = "qnt_simplify"
- | string_of_verit_rule Not_Not = Verit_Proof.not_not_rule
- | string_of_verit_rule Tautological_Clause = "tautology"
- | string_of_verit_rule Duplicate_Literals = Verit_Proof.contract_rule
- | string_of_verit_rule Qnt_CNF = "qnt_cnf"
- | string_of_verit_rule r = "Unknown rule: " ^ \<^make_string> r
-
-fun replay_error ctxt msg rule thms t =
- SMT_Replay_Methods.replay_error ctxt msg (string_of_verit_rule rule) thms t
-
-
-(* utility function *)
-
-fun eqsubst_all ctxt thms =
- K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_asm_tac ctxt [0] thms))
- THEN' K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_tac ctxt [0] thms))
-
-fun simplify_tac ctxt thms =
- ctxt
- |> empty_simpset
- |> put_simpset HOL_basic_ss
- |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
- |> Simplifier.asm_full_simp_tac
-
-(* sko_forall requires the assumptions to be able to prove the equivalence in case of double
-skolemization. See comment below. *)
-fun requires_subproof_assms _ t =
- member (op =) ["refl", "sko_forall", "sko_ex", "cong"] t
-
-fun requires_local_input _ t =
- member (op =) [Verit_Proof.local_input_rule] t
-
-(*This is a weaker simplification form. It is weaker, but is also less likely to loop*)
-fun partial_simplify_tac ctxt thms =
- ctxt
- |> empty_simpset
- |> put_simpset HOL_basic_ss
- |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
- |> Simplifier.full_simp_tac
-
-val try_provers = SMT_Replay_Methods.try_provers "verit"
-
-fun TRY' tac = fn i => TRY (tac i)
-fun REPEAT' tac = fn i => REPEAT (tac i)
-fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i))
-
-
-(* Bind *)
-
-(*The bind rule is non-obvious due to the handling of quantifiers:
- "\<And>x y a. x = y ==> (\<forall>b. P a b x) \<longleftrightarrow> (\<forall>b. P' a b y)"
- ------------------------------------------------------
- \<forall>a. (\<forall>b x. P a b x) \<longleftrightarrow> (\<forall>b y. P' a b y)
-is a valid application.*)
-
-val bind_thms =
- [@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
- @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
- @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
- @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
-
-val bind_thms_same_name =
- [@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
- @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
- @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
- @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
-
-fun extract_quantified_names_q (_ $ Abs (name, _, t)) =
- apfst (curry (op ::) name) (extract_quantified_names_q t)
- | extract_quantified_names_q t = ([], t)
-
-fun extract_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, ty, t)) =
- (name, ty) :: (extract_forall_quantified_names_q t)
- | extract_forall_quantified_names_q _ = []
-
-fun extract_all_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, _, t)) =
- name :: (extract_all_forall_quantified_names_q t)
- | extract_all_forall_quantified_names_q (t $ u) =
- extract_all_forall_quantified_names_q t @ extract_all_forall_quantified_names_q u
- | extract_all_forall_quantified_names_q _ = []
-
-val extract_quantified_names_ba =
- SMT_Replay_Methods.dest_prop
- #> extract_quantified_names_q
- ##> HOLogic.dest_eq
- ##> fst
- ##> extract_quantified_names_q
- ##> fst
-
-val extract_quantified_names =
- extract_quantified_names_ba
- #> (op @)
-
-val extract_all_forall_quantified_names =
- SMT_Replay_Methods.dest_prop
- #> HOLogic.dest_eq
- #> fst
- #> extract_all_forall_quantified_names_q
-
-
-fun extract_all_exists_quantified_names_q (Const(\<^const_name>\<open>HOL.Ex\<close>, _) $ Abs (name, _, t)) =
- name :: (extract_all_exists_quantified_names_q t)
- | extract_all_exists_quantified_names_q (t $ u) =
- extract_all_exists_quantified_names_q t @ extract_all_exists_quantified_names_q u
- | extract_all_exists_quantified_names_q _ = []
-
-val extract_all_exists_quantified_names =
- SMT_Replay_Methods.dest_prop
- #> HOLogic.dest_eq
- #> fst
- #> extract_all_exists_quantified_names_q
-
-
-val extract_bind_names =
- HOLogic.dest_eq
- #> apply2 (fn (Free (name, _)) => name)
-
-fun combine_quant ctxt ((n1, n2) :: bounds) (n1' :: formula) =
- TRY' (if n1 = n1'
- then if n1 <> n2
- then
- resolve_tac ctxt bind_thms
- THEN' TRY'(resolve_tac ctxt [@{thm refl}])
- THEN' combine_quant ctxt bounds formula
- else resolve_tac ctxt bind_thms_same_name THEN' combine_quant ctxt bounds formula
- else resolve_tac ctxt @{thms allI} THEN' combine_quant ctxt ((n1, n2) :: bounds) formula)
- | combine_quant _ _ _ = K all_tac
-
-fun bind_quants ctxt args t =
- combine_quant ctxt (map extract_bind_names args) (extract_quantified_names t)
-
-fun generalize_prems_q [] prems = prems
- | generalize_prems_q (_ :: quants) prems =
- generalize_prems_q quants (@{thm spec} OF [prems])
-
-fun generalize_prems t = generalize_prems_q (fst (extract_quantified_names_ba t))
-
-fun bind ctxt [prems] args t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- bind_quants ctxt args t
- THEN' TRY' (SOLVED' (resolve_tac ctxt [generalize_prems t prems]
- THEN_ALL_NEW TRY' (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms refl}))))
- | bind ctxt thms _ t = replay_error ctxt "invalid bind application" Bind thms t
-
-
-(* Congruence/Refl *)
-
-fun cong ctxt thms = try_provers ctxt
- (string_of_verit_rule Cong) [
- ("basic", SMT_Replay_Methods.cong_basic ctxt thms),
- ("unfolding then reflexivity", SMT_Replay_Methods.cong_unfolding_trivial ctxt thms),
- ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms),
- ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms
-
-fun refl ctxt thm t =
- (case find_first (fn thm => t = Thm.full_prop_of thm) thm of
- SOME thm => thm
- | NONE =>
- (case try (fn t => SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}) t of
- NONE => cong ctxt thm t
- | SOME thm => thm))
-
-
-(* Instantiation *)
-
-local
-fun dropWhile _ [] = []
- | dropWhile f (x :: xs) = if f x then dropWhile f xs else x :: xs
-in
-
-fun forall_inst ctxt _ _ insts t =
- let
- fun instantiate_and_solve i ({context = ctxt, prems = [prem], ...}: Subgoal.focus) =
- let
- val t = Thm.prop_of prem
- val quants = t
- |> SMT_Replay_Methods.dest_prop
- |> extract_forall_quantified_names_q
- val insts = map (Symtab.lookup insts o fst) (rev quants)
- |> dropWhile (curry (op =) NONE)
- |> rev
- fun option_map _ NONE = NONE
- | option_map f (SOME a) = SOME (f a)
- fun instantiate_with inst prem =
- Drule.infer_instantiate' ctxt [NONE, inst] @{thm spec} OF [prem]
- val inst_thm =
- fold instantiate_with
- (map (option_map (Thm.cterm_of ctxt)) insts)
- prem
- in
- (Method.insert_tac ctxt [inst_thm]
- THEN' TRY' (fn i => assume_tac ctxt i)
- THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) i
- end
- | instantiate_and_solve _ ({context = ctxt, prems = thms, ...}: Subgoal.focus) =
- replay_error ctxt "invalid application" Forall_Inst thms t
- in
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- match_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
- THEN' (fn i => Subgoal.FOCUS (instantiate_and_solve i) ctxt i))
- end
-end
-
-
-(* Or *)
-
-fun or _ (thm :: _) _ = thm
- | or ctxt thms t = replay_error ctxt "invalid bind application" Or thms t
-
-
-(* Implication *)
-
-val implies_pos_thm =
- [@{lemma \<open>\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B\<close> by blast},
- @{lemma \<open>\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B\<close> by blast}]
-
-fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- resolve_tac ctxt implies_pos_thm)
-
-fun extract_rewrite_rule_assumption _ thms =
- let
- fun is_rewrite_rule thm =
- (case Thm.prop_of thm of
- \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Free(_, _)) => true
- | _ => false)
- fun is_context_rule thm =
- (case Thm.prop_of thm of
- \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ Free(_, _) $ Free(_, _)) => true
- | _ => false)
- val ctxt_eq =
- thms
- |> filter is_context_rule
- val rew =
- thms
- |> filter_out is_context_rule
- |> filter is_rewrite_rule
- in
- (ctxt_eq, rew)
- end
-
-local
- fun rewrite_all_skolems thm_indirect ctxt (SOME thm :: thms) =
- EqSubst.eqsubst_tac ctxt [0] [thm_indirect OF [thm]]
- THEN' (partial_simplify_tac ctxt (@{thms eq_commute}))
- THEN' rewrite_all_skolems thm_indirect ctxt thms
- | rewrite_all_skolems thm_indirect ctxt (NONE :: thms) = rewrite_all_skolems thm_indirect ctxt thms
- | rewrite_all_skolems _ _ [] = K (all_tac)
-
- fun extract_var_name (thm :: thms) =
- let val name = Thm.concl_of thm
- |> SMT_Replay_Methods.dest_prop
- |> HOLogic.dest_eq
- |> fst
- |> (fn Const(_,_) $ Abs(name, _, _) => [(name,@{thm sym} OF [thm])]
- | _ => [])
- in name :: extract_var_name thms end
- | extract_var_name [] = []
-
-fun skolem_tac extractor thm1 thm2 ctxt thms t =
- let
- val (ctxt_eq, ts) = extract_rewrite_rule_assumption ctxt thms
- fun ordered_definitions () =
- let
- val var_order = extractor t
- val thm_names_with_var = extract_var_name ts |> flat
- in map (AList.lookup (op =) thm_names_with_var) var_order end
-
- in
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- K (unfold_tac ctxt ctxt_eq)
- THEN' ((SOLVED' (K (unfold_tac ctxt (map (fn thm => thm1 OF [@{thm sym} OF [thm]]) ts))))
- ORELSE'
- (rewrite_all_skolems thm2 ctxt (ordered_definitions ())
- THEN' partial_simplify_tac ctxt @{thms eq_commute})))
- end
-in
-
-val skolem_forall =
- skolem_tac extract_all_forall_quantified_names @{thm verit_sko_forall_indirect}
- @{thm verit_sko_forall_indirect2}
-
-val skolem_ex =
- skolem_tac extract_all_exists_quantified_names @{thm verit_sko_ex_indirect}
- @{thm verit_sko_ex_indirect2}
-
-end
-
-fun eq_reflexive ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}
-
-local
- fun not_not_prove ctxt _ =
- K (unfold_tac ctxt @{thms not_not})
- THEN' match_tac ctxt @{thms verit_or_simplify_1}
-
- fun duplicate_literals_prove ctxt prems =
- Method.insert_tac ctxt prems
- THEN' match_tac ctxt @{thms ccontr}
- THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
- THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE})
- THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE})
- THEN' REPEAT' (ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt))
-
- fun tautological_clause_prove ctxt _ =
- match_tac ctxt @{thms verit_or_neg}
- THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]})
- THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt)
-
- val theory_resolution2_lemma = @{lemma \<open>a \<Longrightarrow> a = b \<Longrightarrow> b\<close> by blast}
-in
-
-fun prove_abstract abstracter tac ctxt thms t =
- let
- val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
- val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
- val (_, t2) = Logic.dest_equals (Thm.prop_of t')
- val thm =
- SMT_Replay_Methods.prove_abstract ctxt thms t2 tac (
- fold_map (abstracter o SMT_Replay_Methods.dest_thm) thms ##>>
- abstracter (SMT_Replay_Methods.dest_prop t2))
- in
- @{thm verit_Pure_trans} OF [t', thm]
- end
-
-val not_not = prove_abstract SMT_Replay_Methods.abstract_bool_shallow not_not_prove
-
-val tautological_clause =
- prove_abstract SMT_Replay_Methods.abstract_bool_shallow tautological_clause_prove
-
-val duplicate_literals =
- prove_abstract SMT_Replay_Methods.abstract_bool_shallow duplicate_literals_prove
-
-val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac
-
-(*match_instantiate does not work*)
-fun theory_resolution2 ctxt prems t =
- SMT_Replay_Methods.prove ctxt t (fn _ => match_tac ctxt [theory_resolution2_lemma OF prems])
-
-end
-
-
-fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- Method.insert_tac ctxt prems
- THEN' TRY' (K (unfold_tac ctxt @{thms SMT.trigger_def}))
- THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute}))
-
-val false_rule_thm = @{lemma \<open>\<not>False\<close> by blast}
-
-fun false_rule ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t false_rule_thm
-
-
-(* Transitivity *)
-
-val trans_bool_thm =
- @{lemma \<open>P = Q \<Longrightarrow> Q \<Longrightarrow> P\<close> by blast}
-
-fun trans ctxt thms t =
- let
- val prop_of = HOLogic.dest_Trueprop o Thm.full_prop_of
- fun combine_thms [thm1, thm2] =
- (case (prop_of thm1, prop_of thm2) of
- ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2),
- (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ t4)) =>
- if t2 aconv t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
- else if t2 aconv t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans})))
- else if t1 aconv t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans}))
- else raise Fail "invalid trans theorem"
- | _ => trans_bool_thm OF [thm1, thm2])
- | combine_thms (thm1 :: thm2 :: thms) =
- combine_thms (combine_thms [thm1, thm2] :: thms)
- | combine_thms thms = replay_error ctxt "invalid bind application" Trans thms t
- val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
- val (_, t2) = Logic.dest_equals (Thm.prop_of t')
- val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
- val trans_thm = combine_thms thms
- in
- (case (prop_of trans_thm, t2) of
- ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _),
- (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ _)) =>
- if t1 aconv t3 then trans_thm else trans_thm RS sym
- | _ => trans_thm (*to be on the safe side*))
- end
-
-
-fun tmp_AC_rule ctxt thms t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- Method.insert_tac ctxt thms
- THEN' REPEAT_ALL_NEW (partial_simplify_tac ctxt @{thms eq_commute}
- THEN' TRY' (simplify_tac ctxt @{thms ac_simps conj_ac})
- THEN' TRY' (Classical.fast_tac ctxt)))
-
-
-(* And/Or *)
-
-local
- fun not_and_rule_prove ctxt prems =
- Method.insert_tac ctxt prems
- THEN' K (unfold_tac ctxt @{thms de_Morgan_conj})
- THEN_ALL_NEW TRY' (assume_tac ctxt)
-
- fun or_pos_prove ctxt _ =
- K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
- THEN' match_tac ctxt @{thms verit_and_pos}
- THEN' K (unfold_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not})
- THEN' TRY' (assume_tac ctxt)
-
- fun not_or_rule_prove ctxt prems =
- Method.insert_tac ctxt prems
- THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
- THEN' TRY' (REPEAT' (match_tac ctxt @{thms conjI}))
- THEN_ALL_NEW ((REPEAT' (ematch_tac ctxt @{thms conjE}))
- THEN' TRY' (assume_tac ctxt))
-
- fun and_rule_prove ctxt prems =
- Method.insert_tac ctxt prems
- THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1)))
- THEN' TRY' (assume_tac ctxt)
-
- fun and_neg_rule_prove ctxt _ =
- match_tac ctxt @{thms verit_and_neg}
- THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not})
- THEN' TRY' (assume_tac ctxt)
-
- fun prover tac = prove_abstract SMT_Replay_Methods.abstract_prop tac
-
-in
-
-val and_rule = prover and_rule_prove
-
-val not_and_rule = prover not_and_rule_prove
-
-val not_or_rule = prover not_or_rule_prove
-
-val or_pos_rule = prover or_pos_prove
-
-val and_neg_rule = prover and_neg_rule_prove
-
-val or_neg_rule = prove_abstract SMT_Replay_Methods.abstract_bool (fn ctxt => fn _ =>
- resolve_tac ctxt @{thms verit_or_neg}
- THEN' K (unfold_tac ctxt @{thms not_not})
- THEN_ALL_NEW
- (REPEAT'
- (SOLVED' (match_tac ctxt @{thms disjI1} THEN_ALL_NEW assume_tac ctxt)
- ORELSE' (match_tac ctxt @{thms disjI2} THEN' TRY' (assume_tac ctxt)))))
-
-fun and_pos ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos})
- THEN' TRY' (assume_tac ctxt))
-
-end
-
-
-(* Equivalence Transformation *)
-
-local
- fun prove_equiv equiv_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- Method.insert_tac ctxt [equiv_thm OF [thm]]
- THEN' TRY' (assume_tac ctxt))
- | prove_equiv _ ctxt thms t = replay_error ctxt "invalid application in some equiv rule" Unsupported thms t
-in
-
-val not_equiv1 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B\<close> by blast}
-val not_equiv2 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B\<close> by blast}
-val equiv1 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B\<close> by blast}
-val equiv2 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B\<close> by blast}
-val not_implies1 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow> B) \<Longrightarrow> A\<close> by blast}
-val not_implies2 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B\<close> by blast}
-
-end
-
-
-(* Equivalence Lemma *)
-(*equiv_pos2 is very important for performance. We have tried various tactics, including
-a specialisation of SMT_Replay_Methods.match_instantiate, but there never was a measurable
-and consistent gain.*)
-local
- fun prove_equiv_pos_neg2 thm ctxt _ t =
- SMT_Replay_Methods.match_instantiate ctxt t thm
-in
-
-val equiv_pos1_thm = @{lemma \<open>\<not>(a \<longleftrightarrow> b) \<or> a \<or> \<not>b\<close> by blast+}
-val equiv_pos1 = prove_equiv_pos_neg2 equiv_pos1_thm
-
-val equiv_pos2_thm = @{lemma \<open>\<And>a b. (a \<noteq> b) \<or> \<not>a \<or> b\<close> by blast+}
-val equiv_pos2 = prove_equiv_pos_neg2 equiv_pos2_thm
-
-val equiv_neg1_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> \<not>a \<or> \<not>b\<close> by blast+}
-val equiv_neg1 = prove_equiv_pos_neg2 equiv_neg1_thm
-
-val equiv_neg2_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> a \<or> b\<close> by blast}
-val equiv_neg2 = prove_equiv_pos_neg2 equiv_neg2_thm
-
-end
-
-
-local
- fun implies_pos_neg_term ctxt thm (\<^term>\<open>Trueprop\<close> $
- (\<^term>\<open>HOL.disj\<close> $ (\<^term>\<open>HOL.implies\<close> $ a $ b) $ _)) =
- Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
- | implies_pos_neg_term ctxt thm t =
- replay_error ctxt "invalid application in Implies" Unsupported [thm] t
-
- fun prove_implies_pos_neg thm ctxt _ t =
- let val thm = implies_pos_neg_term ctxt thm t
- in
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- Method.insert_tac ctxt [thm]
- THEN' TRY' (assume_tac ctxt))
- end
-in
-
-val implies_neg1_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> a\<close> by blast}
-val implies_neg1 = prove_implies_pos_neg implies_neg1_thm
-
-val implies_neg2_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> \<not>b\<close> by blast}
-val implies_neg2 = prove_implies_pos_neg implies_neg2_thm
-
-val implies_thm = @{lemma \<open>(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b\<close> by blast}
-fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- Method.insert_tac ctxt [implies_thm OF prems]
- THEN' TRY' (assume_tac ctxt))
-
-end
-
-
-(* BFun *)
-
-local
- val bfun_theorems = @{thms verit_bfun_elim}
-in
-
-fun bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- Method.insert_tac ctxt prems
- THEN' TRY' (eqsubst_all ctxt bfun_theorems)
- THEN' TRY' (simplify_tac ctxt @{thms eq_commute all_conj_distrib ex_disj_distrib}))
-
-end
-
-
-(* If-Then-Else *)
-
-local
- fun prove_ite ite_thm thm ctxt =
- resolve_tac ctxt [ite_thm OF [thm]]
- THEN' K (unfold_tac ctxt @{thms not_not})
- THEN' TRY' (assume_tac ctxt)
-in
-
-val ite_pos1_thm =
- @{lemma \<open>\<not>(if x then P else Q) \<or> x \<or> Q\<close> by auto}
-
-fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- resolve_tac ctxt [ite_pos1_thm])
-
-val ite_pos2_thms =
- @{lemma \<open>\<not>(if x then P else Q) \<or> \<not>x \<or> P\<close> \<open>\<not>(if \<not>x then P else Q) \<or> x \<or> P\<close> by auto}
-
-fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_pos2_thms)
-
-val ite_neg1_thms =
- @{lemma \<open>(if x then P else Q) \<or> x \<or> \<not>Q\<close> \<open>(if x then P else \<not>Q) \<or> x \<or> Q\<close> by auto}
-
-fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg1_thms)
-
-val ite_neg2_thms =
- @{lemma \<open>(if x then P else Q) \<or> \<not>x \<or> \<not>P\<close> \<open>(if \<not>x then P else Q) \<or> x \<or> \<not>P\<close>
- \<open>(if x then \<not>P else Q) \<or> \<not>x \<or> P\<close> \<open>(if \<not>x then \<not>P else Q) \<or> x \<or> P\<close>
- by auto}
-
-fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg2_thms)
-
-val ite1_thm =
- @{lemma \<open>(if x then P else Q) \<Longrightarrow> x \<or> Q\<close> by (auto split: if_splits) }
-
-fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite1_thm thm ctxt)
-
-val ite2_thm =
- @{lemma \<open>(if x then P else Q) \<Longrightarrow> \<not>x \<or> P\<close> by (auto split: if_splits) }
-
-fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite2_thm thm ctxt)
-
-val not_ite1_thm =
- @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q\<close> by (auto split: if_splits) }
-
-fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite1_thm thm ctxt)
-
-val not_ite2_thm =
- @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P\<close> by (auto split: if_splits) }
-
-fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite2_thm thm ctxt)
-
-(*ite_intro can introduce new terms that are in the proof exactly the sames as the old one, but are
-not internally, hence the possible reordering.*)
-fun ite_intro ctxt _ t =
- let
- fun simplify_ite ctxt thms =
- ctxt
- |> empty_simpset
- |> put_simpset HOL_basic_ss
- |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel})
- |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong}
- |> Simplifier.full_simp_tac
- in
- SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt []
- THEN' TRY' (simplify_ite ctxt @{thms eq_commute}))
- end
-end
-
-
-(* Quantifiers *)
-
-local
- val rm_unused = @{lemma \<open>(\<forall>x. P) = P\<close> \<open>(\<exists>x. P) = P\<close> by blast+}
-
- fun qnt_cnf_tac ctxt =
- simplify_tac ctxt @{thms de_Morgan_conj de_Morgan_disj imp_conv_disj
- iff_conv_conj_imp if_bool_eq_disj ex_simps all_simps ex_disj_distrib
- verit_connective_def(3) all_conj_distrib}
- THEN' TRY' (Blast.blast_tac ctxt)
-in
-fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- K (unfold_tac ctxt rm_unused))
-
-fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- Method.insert_tac ctxt prems
- THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt)
- addsimps @{thms HOL.simp_thms HOL.all_simps}
- addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}])
- THEN' TRY' (Blast.blast_tac ctxt)
- THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt []))
-
-fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t Classical.fast_tac
-
-fun qnt_cnf ctxt _ t = SMT_Replay_Methods.prove ctxt t qnt_cnf_tac
-
-fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- partial_simplify_tac ctxt [])
-
-end
-
-(* Equality *)
-
-fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
- REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}])
- THEN' REPEAT' (resolve_tac ctxt @{thms impI})
- THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
- THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1))
- THEN' resolve_tac ctxt @{thms refl})
-
-local
- fun find_rew rews t t' =
- (case AList.lookup (op =) rews (t, t') of
- SOME thm => SOME (thm COMP @{thm symmetric})
- | NONE =>
- (case AList.lookup (op =) rews (t', t) of
- SOME thm => SOME thm
- | NONE => NONE))
-
- fun eq_pred_conv rews t ctxt ctrm =
- (case find_rew rews t (Thm.term_of ctrm) of
- SOME thm => Conv.rewr_conv thm ctrm
- | NONE =>
- (case t of
- f $ arg =>
- (Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv
- Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm
- | Abs (_, _, f) => Conv.abs_conv (eq_pred_conv rews f o snd) ctxt ctrm
- | _ => Conv.all_conv ctrm))
-
- fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) =
- let
- val rews = prems
- |> map_filter (try (apfst (HOLogic.dest_eq o Thm.term_of o Object_Logic.dest_judgment ctxt o
- Thm.cconcl_of) o `(fn x => x)))
- |> map (apsnd (fn x => @{thm eq_reflection} OF [x]))
- fun conv_left conv = Conv.arg_conv (Conv.arg_conv conv)
- fun conv_left_neg conv = Conv.arg_conv (Conv.arg_conv (Conv.arg_conv conv))
- val (t1, conv_term) =
- (case Thm.term_of (Object_Logic.dest_judgment ctxt concl) of
- Const(_, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ t1) $ _ => (t1, conv_left)
- | Const(_, _) $ t1 $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ _) => (t1, conv_left_neg)
- | Const(_, _) $ t1 $ _ => (t1, conv_left)
- | t1 => (t1, conv_left))
-
- fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
- in
- throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt))
- end
-in
-
-fun eq_congruent_pred ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}])
- THEN' (fn i => Subgoal.FOCUS (fn focus => eq_pred_rewrite_tac focus i) ctxt i)
- THEN' (resolve_tac ctxt @{thms refl excluded_middle excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]}
- ORELSE' assume_tac ctxt))
-
-val eq_congruent = eq_congruent_pred
-
-end
-
-
-(* Subproof *)
-
-fun subproof ctxt [prem] t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}],
- @{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
- THEN' resolve_tac ctxt [prem]
- THEN_ALL_NEW assume_tac ctxt
- THEN' TRY' (assume_tac ctxt))
- ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt))
- | subproof ctxt prems t =
- replay_error ctxt "invalid application, only one assumption expected" Subproof prems t
-
-
-(* Simplifying Steps *)
-
-(* The reconstruction is a bit tricky: At first we only rewrite only based on the rules that are
-passed as argument. Then we simply use simp_thms to reconstruct all the proofs (and these theorems
-cover all the simplification below).
-*)
-local
- fun rewrite_only_thms ctxt thms =
- ctxt
- |> empty_simpset
- |> put_simpset HOL_basic_ss
- |> (fn ctxt => ctxt addsimps thms)
- |> Simplifier.full_simp_tac
- fun rewrite_thms ctxt thms =
- ctxt
- |> empty_simpset
- |> put_simpset HOL_basic_ss
- |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
- |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms})
- |> Simplifier.full_simp_tac
-
- fun chain_rewrite_thms ctxt thms =
- TRY' (rewrite_only_thms ctxt thms)
- THEN' TRY' (rewrite_thms ctxt thms)
-
- fun chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 =
- TRY' (rewrite_only_thms ctxt thms1)
- THEN' TRY' (rewrite_thms ctxt thms2)
-
- fun chain_rewrite_thms_two_step ctxt thms1 thms2 thms3 thms4 =
- chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2
- THEN' TRY' (chain_rewrite_two_step_with_ac_simps ctxt thms3 thms4)
-
- val imp_refl = @{lemma \<open>(P \<longrightarrow> P) = True\<close> by blast}
-
-in
-fun rewrite_bool_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (chain_rewrite_thms ctxt @{thms verit_bool_simplify}))
-
-fun rewrite_and_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_and_simplify verit_and_simplify1}
- @{thms verit_and_simplify}))
-
-fun rewrite_or_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_or_simplify verit_or_simplify_1}
- @{thms verit_or_simplify})
- THEN' TRY' (REPEAT' (match_tac ctxt @{thms verit_and_pos}) THEN' assume_tac ctxt))
-
-fun rewrite_not_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (rewrite_only_thms ctxt @{thms verit_not_simplify}))
-
-fun rewrite_equiv_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (rewrite_only_thms ctxt @{thms verit_equiv_simplify}))
-
-fun rewrite_eq_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (chain_rewrite_two_step_with_ac_simps ctxt
- @{thms verit_eq_simplify}
- (Named_Theorems.get ctxt @{named_theorems ac_simps})))
-
-fun rewrite_implies_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (rewrite_only_thms ctxt @{thms verit_implies_simplify}))
-
-(* It is more efficient to first fold the implication symbols.
- That is however not enough when symbols appears within
- expressions, hence we also unfold implications in the
- other direction. *)
-fun rewrite_connective_def ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- chain_rewrite_thms_two_step ctxt
- (imp_refl :: @{thms not_not verit_connective_def[symmetric]})
- (@{thms verit_connective_def[symmetric]})
- (imp_refl :: @{thms not_not verit_connective_def})
- (@{thms verit_connective_def}))
-
-fun rewrite_minus_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- chain_rewrite_two_step_with_ac_simps ctxt
- @{thms arith_simps verit_minus_simplify}
- (Named_Theorems.get ctxt @{named_theorems ac_simps} @
- @{thms numerals arith_simps arith_special
- numeral_class.numeral.numeral_One}))
-
-fun rewrite_comp_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- chain_rewrite_thms ctxt @{thms verit_comp_simplify})
-
-fun rewrite_ite_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- (rewrite_only_thms ctxt @{thms verit_ite_simplify}))
-end
-
-
-(* Simplifications *)
-
-local
- fun simplify_arith ctxt thms = partial_simplify_tac ctxt
- (thms @ Named_Theorems.get ctxt @{named_theorems ac_simps} @ @{thms arith_simps})
-in
-
-fun sum_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- simplify_arith ctxt @{thms verit_sum_simplify arith_special})
-
-fun prod_simplify ctxt _ t =
- SMT_Replay_Methods.prove ctxt t (fn _ =>
- simplify_arith ctxt @{thms verit_prod_simplify})
-
-end
-
-
-(* Arithmetics *)
-local
-
-val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close> by auto}
-in
-fun la_rw_eq ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t la_rw_eq_thm
-
-fun la_generic_prove args ctxt _ = SMT_Replay_Arith.la_farkas args ctxt
-
-fun la_generic ctxt _ args =
- prove_abstract (SMT_Replay_Methods.abstract_arith_shallow ctxt) (la_generic_prove args) ctxt []
-
-fun lia_generic ctxt _ t =
- SMT_Replay_Methods.prove_arith_rewrite SMT_Replay_Methods.abstract_neq ctxt t
-
-fun la_disequality ctxt _ t =
- SMT_Replay_Methods.match_instantiate ctxt t @{thm verit_la_disequality}
-
-end
(* Combining all together *)