--- a/src/Provers/order_tac.ML Fri Jan 31 16:59:12 2025 +0100
+++ b/src/Provers/order_tac.ML Fri Jan 31 17:01:27 2025 +0100
@@ -1,557 +1,567 @@
signature REIFY_TABLE =
sig
- type table
- val empty : table
- val get_var : term -> table -> (int * table)
- val get_term : int -> table -> term option
+
+type table
+val empty : table
+val get_var : term -> table -> (int * table)
+val get_term : int -> table -> term option
+
end
structure Reifytab: REIFY_TABLE =
struct
- type table = (int * (term * int) list)
-
- val empty = (0, [])
-
- fun get_var t (max_var, tis) =
- (case AList.lookup Envir.aeconv tis t of
- SOME v => (v, (max_var, tis))
- | NONE => (max_var, (max_var + 1, (t, max_var) :: tis))
- )
-
- fun get_term v (_, tis) = Library.find_first (fn (_, v2) => v = v2) tis
- |> Option.map fst
+type table = (int * (term * int) list)
+
+val empty = (0, [])
+
+fun get_var t (max_var, tis) =
+ (case AList.lookup Envir.aeconv tis t of
+ SOME v => (v, (max_var, tis))
+ | NONE => (max_var, (max_var + 1, (t, max_var) :: tis))
+ )
+
+fun get_term v (_, tis) = Library.find_first (fn (_, v2) => v = v2) tis
+ |> Option.map fst
+
end
signature LOGIC_SIGNATURE =
sig
- val mk_Trueprop : term -> term
- val dest_Trueprop : term -> term
- val Trueprop_conv : conv -> conv
- val Not : term
- val conj : term
- val disj : term
-
- val notI : thm (* (P \<Longrightarrow> False) \<Longrightarrow> \<not> P *)
- val ccontr : thm (* (\<not> P \<Longrightarrow> False) \<Longrightarrow> P *)
- val conjI : thm (* P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q *)
- val conjE : thm (* P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R *)
- val disjE : thm (* P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R *)
+
+val mk_Trueprop : term -> term
+val dest_Trueprop : term -> term
+val Trueprop_conv : conv -> conv
+val Not : term
+val conj : term
+val disj : term
- val not_not_conv : conv (* \<not> (\<not> P) \<equiv> P *)
- val de_Morgan_conj_conv : conv (* \<not> (P \<and> Q) \<equiv> \<not> P \<or> \<not> Q *)
- val de_Morgan_disj_conv : conv (* \<not> (P \<or> Q) \<equiv> \<not> P \<and> \<not> Q *)
- val conj_disj_distribL_conv : conv (* P \<and> (Q \<or> R) \<equiv> (P \<and> Q) \<or> (P \<and> R) *)
- val conj_disj_distribR_conv : conv (* (Q \<or> R) \<and> P \<equiv> (Q \<and> P) \<or> (R \<and> P) *)
+val notI : thm (* (P \<Longrightarrow> False) \<Longrightarrow> \<not> P *)
+val ccontr : thm (* (\<not> P \<Longrightarrow> False) \<Longrightarrow> P *)
+val conjI : thm (* P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q *)
+val conjE : thm (* P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R *)
+val disjE : thm (* P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R *)
+
+val not_not_conv : conv (* \<not> (\<not> P) \<equiv> P *)
+val de_Morgan_conj_conv : conv (* \<not> (P \<and> Q) \<equiv> \<not> P \<or> \<not> Q *)
+val de_Morgan_disj_conv : conv (* \<not> (P \<or> Q) \<equiv> \<not> P \<and> \<not> Q *)
+val conj_disj_distribL_conv : conv (* P \<and> (Q \<or> R) \<equiv> (P \<and> Q) \<or> (P \<and> R) *)
+val conj_disj_distribR_conv : conv (* (Q \<or> R) \<and> P \<equiv> (Q \<and> P) \<or> (R \<and> P) *)
+
end
signature BASE_ORDER_TAC_BASE =
sig
- val order_trace_cfg : bool Config.T
- val order_split_limit_cfg : int Config.T
-
- datatype order_kind = Order | Linorder
-
- type order_literal = (bool * Order_Procedure.order_atom)
-
- type order_ops = { eq : term, le : term, lt : term }
-
- val map_order_ops : (term -> term) -> order_ops -> order_ops
-
- type order_context = {
- kind : order_kind,
- ops : order_ops,
- thms : (string * thm) list, conv_thms : (string * thm) list
- }
+val order_trace_cfg : bool Config.T
+val order_split_limit_cfg : int Config.T
+
+datatype order_kind = Order | Linorder
+
+type order_literal = (bool * Order_Procedure.order_atom)
+
+type order_ops = { eq : term, le : term, lt : term }
+
+val map_order_ops : (term -> term) -> order_ops -> order_ops
+
+type order_context = {
+ kind : order_kind,
+ ops : order_ops,
+ thms : (string * thm) list, conv_thms : (string * thm) list
+ }
end
structure Base_Order_Tac_Base : BASE_ORDER_TAC_BASE =
struct
- (* Control tracing output of the solver. *)
- val order_trace_cfg = Attrib.setup_config_bool @{binding "order_trace"} (K false)
- (* In partial orders, literals of the form \<not> x < y will force the order solver to perform case
- distinctions, which leads to an exponential blowup of the runtime. The split limit controls
- the number of literals of this form that are passed to the solver.
- *)
- val order_split_limit_cfg = Attrib.setup_config_int @{binding "order_split_limit"} (K 8)
-
- datatype order_kind = Order | Linorder
-
- type order_literal = (bool * Order_Procedure.order_atom)
-
- type order_ops = { eq : term, le : term, lt : term }
-
- fun map_order_ops f {eq, le, lt} = {eq = f eq, le = f le, lt = f lt}
-
- type order_context = {
- kind : order_kind,
- ops : order_ops,
- thms : (string * thm) list, conv_thms : (string * thm) list
- }
+(* Control tracing output of the solver. *)
+val order_trace_cfg = Attrib.setup_config_bool @{binding "order_trace"} (K false)
+(* In partial orders, literals of the form \<not> x < y will force the order solver to perform case
+ distinctions, which leads to an exponential blowup of the runtime. The split limit controls
+ the number of literals of this form that are passed to the solver.
+ *)
+val order_split_limit_cfg = Attrib.setup_config_int @{binding "order_split_limit"} (K 8)
+
+datatype order_kind = Order | Linorder
+
+type order_literal = (bool * Order_Procedure.order_atom)
+
+type order_ops = { eq : term, le : term, lt : term }
+
+fun map_order_ops f {eq, le, lt} = {eq = f eq, le = f le, lt = f lt}
+
+type order_context = {
+ kind : order_kind,
+ ops : order_ops,
+ thms : (string * thm) list, conv_thms : (string * thm) list
+ }
end
signature BASE_ORDER_TAC =
sig
- include BASE_ORDER_TAC_BASE
-
- type insert_prems_hook =
- order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list
- -> thm list
+
+include BASE_ORDER_TAC_BASE
+
+type insert_prems_hook =
+ order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list
+ -> thm list
- val declare_insert_prems_hook :
- (binding * insert_prems_hook) -> local_theory -> local_theory
+val declare_insert_prems_hook :
+ (binding * insert_prems_hook) -> local_theory -> local_theory
- val insert_prems_hook_names : Proof.context -> binding list
+val insert_prems_hook_names : Proof.context -> binding list
- val tac :
- (order_literal Order_Procedure.fm -> Order_Procedure.prf_trm option)
- -> order_context -> thm list
- -> Proof.context -> int -> tactic
+val tac :
+ (order_literal Order_Procedure.fm -> Order_Procedure.prf_trm option)
+ -> order_context -> thm list
+ -> Proof.context -> int -> tactic
+
end
functor Base_Order_Tac(
structure Logic_Sig : LOGIC_SIGNATURE; val excluded_types : typ list) : BASE_ORDER_TAC =
struct
- open Base_Order_Tac_Base
- open Order_Procedure
+
+open Base_Order_Tac_Base
+open Order_Procedure
+
+fun expect _ (SOME x) = x
+ | expect f NONE = f ()
+
+fun list_curry0 f = (fn [] => f, 0)
+fun list_curry1 f = (fn [x] => f x, 1)
+fun list_curry2 f = (fn [x, y] => f x y, 2)
- fun expect _ (SOME x) = x
- | expect f NONE = f ()
+fun dereify_term consts reifytab t =
+ let
+ fun dereify_term' (App (t1, t2)) = (dereify_term' t1) $ (dereify_term' t2)
+ | dereify_term' (Const s) =
+ AList.lookup (op =) consts s
+ |> expect (fn () => raise TERM ("Const " ^ s ^ " not in", map snd consts))
+ | dereify_term' (Var v) = Reifytab.get_term (integer_of_int v) reifytab |> the
+ in
+ dereify_term' t
+ end
- fun list_curry0 f = (fn [] => f, 0)
- fun list_curry1 f = (fn [x] => f x, 1)
- fun list_curry2 f = (fn [x, y] => f x y, 2)
+fun dereify_order_fm (eq, le, lt) reifytab t =
+ let
+ val consts = [
+ ("eq", eq), ("le", le), ("lt", lt),
+ ("Not", Logic_Sig.Not), ("disj", Logic_Sig.disj), ("conj", Logic_Sig.conj)
+ ]
+ in
+ dereify_term consts reifytab t
+ end
- fun dereify_term consts reifytab t =
- let
- fun dereify_term' (App (t1, t2)) = (dereify_term' t1) $ (dereify_term' t2)
- | dereify_term' (Const s) =
- AList.lookup (op =) consts s
- |> expect (fn () => raise TERM ("Const " ^ s ^ " not in", map snd consts))
- | dereify_term' (Var v) = Reifytab.get_term (integer_of_int v) reifytab |> the
- in
- dereify_term' t
- end
+fun strip_AppP t =
+ let fun strip (AppP (f, s), ss) = strip (f, s::ss)
+ | strip x = x
+ in strip (t, []) end
+
+fun replay_conv convs cvp =
+ let
+ val convs = convs @
+ [("all_conv", list_curry0 Conv.all_conv)] @
+ map (apsnd list_curry1) [
+ ("atom_conv", I),
+ ("neg_atom_conv", I),
+ ("arg_conv", Conv.arg_conv)] @
+ map (apsnd list_curry2) [
+ ("combination_conv", Conv.combination_conv),
+ ("then_conv", curry (op then_conv))]
+
+ fun lookup_conv convs c = AList.lookup (op =) convs c
+ |> expect (fn () => error ("Can't replay conversion: " ^ c))
+
+ fun rp_conv t =
+ (case strip_AppP t ||> map rp_conv of
+ (PThm c, cvs) =>
+ let val (conv, arity) = lookup_conv convs c
+ in if arity = length cvs
+ then conv cvs
+ else error ("Expected " ^ Int.toString arity ^ " arguments for conversion " ^
+ c ^ " but got " ^ (length cvs |> Int.toString) ^ " arguments")
+ end
+ | _ => error "Unexpected constructor in conversion proof")
+ in
+ rp_conv cvp
+ end
- fun dereify_order_fm (eq, le, lt) reifytab t =
- let
- val consts = [
- ("eq", eq), ("le", le), ("lt", lt),
- ("Not", Logic_Sig.Not), ("disj", Logic_Sig.disj), ("conj", Logic_Sig.conj)
- ]
- in
- dereify_term consts reifytab t
- end
-
- fun strip_AppP t =
- let fun strip (AppP (f, s), ss) = strip (f, s::ss)
- | strip x = x
- in strip (t, []) end
+fun replay_prf_trm replay_conv dereify ctxt thmtab assmtab p =
+ let
+ fun replay_prf_trm' _ (PThm s) =
+ AList.lookup (op =) thmtab s
+ |> expect (fn () => error ("Cannot replay theorem: " ^ s))
+ | replay_prf_trm' assmtab (Appt (p, t)) =
+ replay_prf_trm' assmtab p
+ |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (dereify t))]
+ | replay_prf_trm' assmtab (AppP (p1, p2)) =
+ apply2 (replay_prf_trm' assmtab) (p2, p1) |> op COMP
+ | replay_prf_trm' assmtab (AbsP (reified_t, p)) =
+ let
+ val t = dereify reified_t
+ val t_thm = Logic_Sig.mk_Trueprop t |> Thm.cterm_of ctxt |> Assumption.assume ctxt
+ val rp = replay_prf_trm' (Termtab.update (Thm.prop_of t_thm, t_thm) assmtab) p
+ in
+ Thm.implies_intr (Thm.cprop_of t_thm) rp
+ end
+ | replay_prf_trm' assmtab (Bound reified_t) =
+ let
+ val t = dereify reified_t |> Logic_Sig.mk_Trueprop
+ in
+ Termtab.lookup assmtab t
+ |> expect (fn () => raise TERM ("Assumption not found:", t::Termtab.keys assmtab))
+ end
+ | replay_prf_trm' assmtab (Conv (t, cp, p)) =
+ let
+ val thm = replay_prf_trm' assmtab (Bound t)
+ val conv = Logic_Sig.Trueprop_conv (replay_conv cp)
+ val conv_thm = Conv.fconv_rule conv thm
+ val conv_term = Thm.prop_of conv_thm
+ in
+ replay_prf_trm' (Termtab.update (conv_term, conv_thm) assmtab) p
+ end
+ in
+ replay_prf_trm' assmtab p
+ end
- fun replay_conv convs cvp =
- let
- val convs = convs @
- [("all_conv", list_curry0 Conv.all_conv)] @
- map (apsnd list_curry1) [
- ("atom_conv", I),
- ("neg_atom_conv", I),
- ("arg_conv", Conv.arg_conv)] @
- map (apsnd list_curry2) [
- ("combination_conv", Conv.combination_conv),
- ("then_conv", curry (op then_conv))]
+fun replay_order_prf_trm ord_ops {thms = thms, conv_thms = conv_thms, ...} ctxt reifytab assmtab =
+ let
+ val thmtab = thms @ [
+ ("conjE", Logic_Sig.conjE), ("conjI", Logic_Sig.conjI), ("disjE", Logic_Sig.disjE)
+ ]
+ val convs = map (apsnd list_curry0) (
+ map (apsnd Conv.rewr_conv) conv_thms @
+ [
+ ("not_not_conv", Logic_Sig.not_not_conv),
+ ("de_Morgan_conj_conv", Logic_Sig.de_Morgan_conj_conv),
+ ("de_Morgan_disj_conv", Logic_Sig.de_Morgan_disj_conv),
+ ("conj_disj_distribR_conv", Logic_Sig.conj_disj_distribR_conv),
+ ("conj_disj_distribL_conv", Logic_Sig.conj_disj_distribL_conv)
+ ])
+
+ val dereify = dereify_order_fm ord_ops reifytab
+ in
+ replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab
+ end
- fun lookup_conv convs c = AList.lookup (op =) convs c
- |> expect (fn () => error ("Can't replay conversion: " ^ c))
+fun strip_Not (nt $ t) = if nt = Logic_Sig.Not then t else nt $ t
+ | strip_Not t = t
+
+fun limit_not_less lt ctxt decomp_prems =
+ let
+ val trace = Config.get ctxt order_trace_cfg
+ val limit = Config.get ctxt order_split_limit_cfg
+
+ fun is_not_less_term t =
+ case try (strip_Not o Logic_Sig.dest_Trueprop) t of
+ SOME (binop $ _ $ _) => binop = lt
+ | _ => false
- fun rp_conv t =
- (case strip_AppP t ||> map rp_conv of
- (PThm c, cvs) =>
- let val (conv, arity) = lookup_conv convs c
- in if arity = length cvs
- then conv cvs
- else error ("Expected " ^ Int.toString arity ^ " arguments for conversion " ^
- c ^ " but got " ^ (length cvs |> Int.toString) ^ " arguments")
- end
- | _ => error "Unexpected constructor in conversion proof")
- in
- rp_conv cvp
- end
+ val not_less_prems = filter (is_not_less_term o Thm.prop_of o fst) decomp_prems
+ val _ = if trace andalso length not_less_prems > limit
+ then tracing "order split limit exceeded"
+ else ()
+ in
+ filter_out (is_not_less_term o Thm.prop_of o fst) decomp_prems @
+ take limit not_less_prems
+ end
+
+fun decomp {eq, le, lt} ctxt t =
+ let
+ fun decomp'' (binop $ t1 $ t2) =
+ let
+ fun is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types
+
+ open Order_Procedure
+ val thy = Proof_Context.theory_of ctxt
+ fun try_match pat = try (Pattern.match thy (pat, binop)) (Vartab.empty, Vartab.empty)
+ in if is_excluded t1 then NONE
+ else case (try_match eq, try_match le, try_match lt) of
+ (SOME env, _, _) => SOME ((true, EQ, (t1, t2)), env)
+ | (_, SOME env, _) => SOME ((true, LEQ, (t1, t2)), env)
+ | (_, _, SOME env) => SOME ((true, LESS, (t1, t2)), env)
+ | _ => NONE
+ end
+ | decomp'' _ = NONE
+
+ fun decomp' (nt $ t) =
+ if nt = Logic_Sig.Not
+ then decomp'' t |> Option.map (fn ((b, c, p), e) => ((not b, c, p), e))
+ else decomp'' (nt $ t)
+ | decomp' t = decomp'' t
+ in
+ try Logic_Sig.dest_Trueprop t |> Option.mapPartial decomp'
+ end
+
+fun maximal_envs envs =
+ let
+ fun test_opt p (SOME x) = p x
+ | test_opt _ NONE = false
+
+ fun leq_env (tyenv1, tenv1) (tyenv2, tenv2) =
+ Vartab.forall (fn (v, ty) =>
+ Vartab.lookup tyenv2 v |> test_opt (fn ty2 => ty2 = ty)) tyenv1
+ andalso
+ Vartab.forall (fn (v, (ty, t)) =>
+ Vartab.lookup tenv2 v |> test_opt (fn (ty2, t2) => ty2 = ty andalso t2 aconv t)) tenv1
+
+ fun fold_env (i, env) es = fold_index (fn (i2, env2) => fn es =>
+ if i = i2 then es else if leq_env env env2 then (i, i2) :: es else es) envs es
+
+ val env_order = fold_index fold_env envs []
+
+ val graph = fold_index (fn (i, env) => fn g => Int_Graph.new_node (i, env) g)
+ envs Int_Graph.empty
+ val graph = fold Int_Graph.add_edge env_order graph
+
+ val strong_conns = Int_Graph.strong_conn graph
+ val maximals =
+ filter (fn comp => length comp = length (Int_Graph.all_succs graph comp)) strong_conns
+ in
+ map (Int_Graph.all_preds graph) maximals
+ end
- fun replay_prf_trm replay_conv dereify ctxt thmtab assmtab p =
- let
- fun replay_prf_trm' _ (PThm s) =
- AList.lookup (op =) thmtab s
- |> expect (fn () => error ("Cannot replay theorem: " ^ s))
- | replay_prf_trm' assmtab (Appt (p, t)) =
- replay_prf_trm' assmtab p
- |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (dereify t))]
- | replay_prf_trm' assmtab (AppP (p1, p2)) =
- apply2 (replay_prf_trm' assmtab) (p2, p1) |> op COMP
- | replay_prf_trm' assmtab (AbsP (reified_t, p)) =
- let
- val t = dereify reified_t
- val t_thm = Logic_Sig.mk_Trueprop t |> Thm.cterm_of ctxt |> Assumption.assume ctxt
- val rp = replay_prf_trm' (Termtab.update (Thm.prop_of t_thm, t_thm) assmtab) p
- in
- Thm.implies_intr (Thm.cprop_of t_thm) rp
- end
- | replay_prf_trm' assmtab (Bound reified_t) =
- let
- val t = dereify reified_t |> Logic_Sig.mk_Trueprop
- in
- Termtab.lookup assmtab t
- |> expect (fn () => raise TERM ("Assumption not found:", t::Termtab.keys assmtab))
- end
- | replay_prf_trm' assmtab (Conv (t, cp, p)) =
- let
- val thm = replay_prf_trm' assmtab (Bound t)
- val conv = Logic_Sig.Trueprop_conv (replay_conv cp)
- val conv_thm = Conv.fconv_rule conv thm
- val conv_term = Thm.prop_of conv_thm
- in
- replay_prf_trm' (Termtab.update (conv_term, conv_thm) assmtab) p
- end
- in
- replay_prf_trm' assmtab p
- end
+fun partition_prems octxt ctxt prems =
+ let
+ fun these' _ [] = []
+ | these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs
+
+ val (decomp_prems, envs) =
+ these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems
+ |> map_split (fn (thm, (l, env)) => ((thm, l), env))
+
+ val env_groups = maximal_envs envs
+ in
+ map (fn is => (map (nth decomp_prems) is, nth envs (hd is))) env_groups
+ end
+
+local
+ fun pretty_term_list ctxt =
+ Pretty.list "" "" o map (Syntax.pretty_term (Config.put show_types true ctxt))
+ fun pretty_type_of ctxt t = Pretty.block
+ [ Pretty.str "::", Pretty.brk 1
+ , Pretty.quote (Syntax.pretty_typ ctxt (Term.fastype_of t)) ]
+in
+ fun pretty_order_kind (okind : order_kind) = Pretty.str (@{make_string} okind)
+ fun pretty_order_ops ctxt ({eq, le, lt} : order_ops) =
+ Pretty.block [pretty_term_list ctxt [eq, le, lt], Pretty.brk 1, pretty_type_of ctxt le]
+end
+
+type insert_prems_hook =
+ order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list
+ -> thm list
+
+structure Insert_Prems_Hook_Data = Generic_Data(
+ type T = (binding * insert_prems_hook) list
+ val empty = []
+ val merge = Library.merge ((op =) o apply2 fst)
+)
- fun replay_order_prf_trm ord_ops {thms = thms, conv_thms = conv_thms, ...} ctxt reifytab assmtab =
- let
- val thmtab = thms @ [
- ("conjE", Logic_Sig.conjE), ("conjI", Logic_Sig.conjI), ("disjE", Logic_Sig.disjE)
- ]
- val convs = map (apsnd list_curry0) (
- map (apsnd Conv.rewr_conv) conv_thms @
- [
- ("not_not_conv", Logic_Sig.not_not_conv),
- ("de_Morgan_conj_conv", Logic_Sig.de_Morgan_conj_conv),
- ("de_Morgan_disj_conv", Logic_Sig.de_Morgan_disj_conv),
- ("conj_disj_distribR_conv", Logic_Sig.conj_disj_distribR_conv),
- ("conj_disj_distribL_conv", Logic_Sig.conj_disj_distribL_conv)
- ])
-
- val dereify = dereify_order_fm ord_ops reifytab
- in
- replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab
- end
+fun declare_insert_prems_hook (binding, hook) lthy =
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
+ (fn phi => fn context =>
+ let
+ val binding = Morphism.binding phi binding
+ in
+ context
+ |> Insert_Prems_Hook_Data.map (Library.insert ((op =) o apply2 fst) (binding, hook))
+ end)
+
+val insert_prems_hook_names = Context.Proof #> Insert_Prems_Hook_Data.get #> map fst
- fun strip_Not (nt $ t) = if nt = Logic_Sig.Not then t else nt $ t
- | strip_Not t = t
+fun eval_insert_prems_hook kind order_ops ctxt decomp_prems (hookN, hook : insert_prems_hook) =
+ let
+ fun dereify_order_op' (EQ _) = #eq order_ops
+ | dereify_order_op' (LEQ _) = #le order_ops
+ | dereify_order_op' (LESS _) = #lt order_ops
+ fun dereify_order_op oop = (~1, ~1) |> apply2 Int_of_integer |> oop |> dereify_order_op'
+ val decomp_prems =
+ decomp_prems
+ |> map (apsnd (fn (b, oop, (t1, t2)) => (b, dereify_order_op oop, (t1, t2))))
+ fun unzip (acc1, acc2) [] = (rev acc1, rev acc2)
+ | unzip (acc1, acc2) ((thm, NONE) :: ps) = unzip (acc1, thm :: acc2) ps
+ | unzip (acc1, acc2) ((thm, SOME dp) :: ps) = unzip ((thm, dp) :: acc1, acc2) ps
+ val (decomp_extra_prems, invalid_extra_prems) =
+ hook kind order_ops ctxt decomp_prems
+ |> map (swap o ` (decomp order_ops ctxt o Thm.prop_of))
+ |> unzip ([], [])
- fun limit_not_less lt ctxt decomp_prems =
+ val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt)
+ fun pretty_trace () =
+ [ ("order kind:", pretty_order_kind kind)
+ , ("order operators:", pretty_order_ops ctxt order_ops)
+ , ("inserted premises:", pretty_thm_list (map fst decomp_extra_prems))
+ , ("invalid premises:", pretty_thm_list invalid_extra_prems)
+ ]
+ |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp])
+ |> Pretty.big_list ("insert premises hook " ^ Pretty.string_of (Binding.pretty hookN)
+ ^ " called with the parameters")
+ val trace = Config.get ctxt order_trace_cfg
+ val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else ()
+ in
+ map (apsnd fst) decomp_extra_prems
+ end
+
+fun order_tac raw_order_proc octxt simp_prems =
+ Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} =>
let
val trace = Config.get ctxt order_trace_cfg
- val limit = Config.get ctxt order_split_limit_cfg
-
- fun is_not_less_term t =
- case try (strip_Not o Logic_Sig.dest_Trueprop) t of
- SOME (binop $ _ $ _) => binop = lt
- | _ => false
-
- val not_less_prems = filter (is_not_less_term o Thm.prop_of o fst) decomp_prems
- val _ = if trace andalso length not_less_prems > limit
- then tracing "order split limit exceeded"
- else ()
- in
- filter_out (is_not_less_term o Thm.prop_of o fst) decomp_prems @
- take limit not_less_prems
- end
-
- fun decomp {eq, le, lt} ctxt t =
- let
- fun decomp'' (binop $ t1 $ t2) =
- let
- fun is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types
-
- open Order_Procedure
- val thy = Proof_Context.theory_of ctxt
- fun try_match pat = try (Pattern.match thy (pat, binop)) (Vartab.empty, Vartab.empty)
- in if is_excluded t1 then NONE
- else case (try_match eq, try_match le, try_match lt) of
- (SOME env, _, _) => SOME ((true, EQ, (t1, t2)), env)
- | (_, SOME env, _) => SOME ((true, LEQ, (t1, t2)), env)
- | (_, _, SOME env) => SOME ((true, LESS, (t1, t2)), env)
- | _ => NONE
- end
- | decomp'' _ = NONE
-
- fun decomp' (nt $ t) =
- if nt = Logic_Sig.Not
- then decomp'' t |> Option.map (fn ((b, c, p), e) => ((not b, c, p), e))
- else decomp'' (nt $ t)
- | decomp' t = decomp'' t
- in
- try Logic_Sig.dest_Trueprop t |> Option.mapPartial decomp'
- end
-
- fun maximal_envs envs =
- let
- fun test_opt p (SOME x) = p x
- | test_opt _ NONE = false
+
+ fun order_tac' ([], _) = no_tac
+ | order_tac' (decomp_prems, env) =
+ let
+ val (order_ops as {eq, le, lt}) =
+ #ops octxt |> map_order_ops (Envir.eta_contract o Envir.subst_term env)
+
+ val insert_prems_hooks = Insert_Prems_Hook_Data.get (Context.Proof ctxt)
+ val inserted_decomp_prems =
+ insert_prems_hooks
+ |> maps (eval_insert_prems_hook (#kind octxt) order_ops ctxt decomp_prems)
- fun leq_env (tyenv1, tenv1) (tyenv2, tenv2) =
- Vartab.forall (fn (v, ty) =>
- Vartab.lookup tyenv2 v |> test_opt (fn ty2 => ty2 = ty)) tyenv1
- andalso
- Vartab.forall (fn (v, (ty, t)) =>
- Vartab.lookup tenv2 v |> test_opt (fn (ty2, t2) => ty2 = ty andalso t2 aconv t)) tenv1
-
- fun fold_env (i, env) es = fold_index (fn (i2, env2) => fn es =>
- if i = i2 then es else if leq_env env env2 then (i, i2) :: es else es) envs es
-
- val env_order = fold_index fold_env envs []
-
- val graph = fold_index (fn (i, env) => fn g => Int_Graph.new_node (i, env) g)
- envs Int_Graph.empty
- val graph = fold Int_Graph.add_edge env_order graph
-
- val strong_conns = Int_Graph.strong_conn graph
- val maximals =
- filter (fn comp => length comp = length (Int_Graph.all_succs graph comp)) strong_conns
- in
- map (Int_Graph.all_preds graph) maximals
- end
+ val decomp_prems = decomp_prems @ inserted_decomp_prems
+ val decomp_prems =
+ case #kind octxt of
+ Order => limit_not_less lt ctxt decomp_prems
+ | _ => decomp_prems
+
+ fun reify_prem (_, (b, ctor, (x, y))) (ps, reifytab) =
+ (Reifytab.get_var x ##>> Reifytab.get_var y) reifytab
+ |>> (fn vp => (b, ctor (apply2 Int_of_integer vp)) :: ps)
+ val (reified_prems, reifytab) = fold_rev reify_prem decomp_prems ([], Reifytab.empty)
- fun partition_prems octxt ctxt prems =
- let
- fun these' _ [] = []
- | these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs
-
- val (decomp_prems, envs) =
- these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems
- |> map_split (fn (thm, (l, env)) => ((thm, l), env))
-
- val env_groups = maximal_envs envs
- in
- map (fn is => (map (nth decomp_prems) is, nth envs (hd is))) env_groups
- end
-
- local
- fun pretty_term_list ctxt =
- Pretty.list "" "" o map (Syntax.pretty_term (Config.put show_types true ctxt))
- fun pretty_type_of ctxt t = Pretty.block
- [ Pretty.str "::", Pretty.brk 1
- , Pretty.quote (Syntax.pretty_typ ctxt (Term.fastype_of t)) ]
- in
- fun pretty_order_kind (okind : order_kind) = Pretty.str (@{make_string} okind)
- fun pretty_order_ops ctxt ({eq, le, lt} : order_ops) =
- Pretty.block [pretty_term_list ctxt [eq, le, lt], Pretty.brk 1, pretty_type_of ctxt le]
- end
-
- type insert_prems_hook =
- order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list
- -> thm list
-
- structure Insert_Prems_Hook_Data = Generic_Data(
- type T = (binding * insert_prems_hook) list
- val empty = []
- val merge = Library.merge ((op =) o apply2 fst)
- )
+ val reified_prems_conj = foldl1 (fn (x, a) => And (x, a)) (map Atom reified_prems)
+ val prems_conj_thm = map fst decomp_prems
+ |> foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a])
+ |> Conv.fconv_rule Thm.eta_conversion
+ val prems_conj = prems_conj_thm |> Thm.prop_of
+
+ val proof = raw_order_proc reified_prems_conj
- fun declare_insert_prems_hook (binding, hook) lthy =
- lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
- (fn phi => fn context =>
- let
- val binding = Morphism.binding phi binding
- in
- context
- |> Insert_Prems_Hook_Data.map (Library.insert ((op =) o apply2 fst) (binding, hook))
- end)
-
- val insert_prems_hook_names = Context.Proof #> Insert_Prems_Hook_Data.get #> map fst
-
- fun eval_insert_prems_hook kind order_ops ctxt decomp_prems (hookN, hook : insert_prems_hook) =
- let
- fun dereify_order_op' (EQ _) = #eq order_ops
- | dereify_order_op' (LEQ _) = #le order_ops
- | dereify_order_op' (LESS _) = #lt order_ops
- fun dereify_order_op oop = (~1, ~1) |> apply2 Int_of_integer |> oop |> dereify_order_op'
- val decomp_prems =
- decomp_prems
- |> map (apsnd (fn (b, oop, (t1, t2)) => (b, dereify_order_op oop, (t1, t2))))
- fun unzip (acc1, acc2) [] = (rev acc1, rev acc2)
- | unzip (acc1, acc2) ((thm, NONE) :: ps) = unzip (acc1, thm :: acc2) ps
- | unzip (acc1, acc2) ((thm, SOME dp) :: ps) = unzip ((thm, dp) :: acc1, acc2) ps
- val (decomp_extra_prems, invalid_extra_prems) =
- hook kind order_ops ctxt decomp_prems
- |> map (swap o ` (decomp order_ops ctxt o Thm.prop_of))
- |> unzip ([], [])
+ val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt)
+ fun pretty_trace () =
+ [ ("order kind:", pretty_order_kind (#kind octxt))
+ , ("order operators:", pretty_order_ops ctxt order_ops)
+ , ("premises:", pretty_thm_list prems)
+ , ("selected premises:", pretty_thm_list (map fst decomp_prems))
+ , ("reified premises:", Pretty.str (@{make_string} reified_prems))
+ , ("contradiction:", Pretty.str (@{make_string} (Option.isSome proof)))
+ ]
+ |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp])
+ |> Pretty.big_list "order solver called with the parameters"
+ val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else ()
- val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt)
- fun pretty_trace () =
- [ ("order kind:", pretty_order_kind kind)
- , ("order operators:", pretty_order_ops ctxt order_ops)
- , ("inserted premises:", pretty_thm_list (map fst decomp_extra_prems))
- , ("invalid premises:", pretty_thm_list invalid_extra_prems)
- ]
- |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp])
- |> Pretty.big_list ("insert premises hook " ^ Pretty.string_of (Binding.pretty hookN)
- ^ " called with the parameters")
- val trace = Config.get ctxt order_trace_cfg
- val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else ()
- in
- map (apsnd fst) decomp_extra_prems
- end
-
- fun order_tac raw_order_proc octxt simp_prems =
- Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} =>
- let
- val trace = Config.get ctxt order_trace_cfg
-
- fun order_tac' ([], _) = no_tac
- | order_tac' (decomp_prems, env) =
- let
- val (order_ops as {eq, le, lt}) =
- #ops octxt |> map_order_ops (Envir.eta_contract o Envir.subst_term env)
-
- val insert_prems_hooks = Insert_Prems_Hook_Data.get (Context.Proof ctxt)
- val inserted_decomp_prems =
- insert_prems_hooks
- |> maps (eval_insert_prems_hook (#kind octxt) order_ops ctxt decomp_prems)
-
- val decomp_prems = decomp_prems @ inserted_decomp_prems
- val decomp_prems =
- case #kind octxt of
- Order => limit_not_less lt ctxt decomp_prems
- | _ => decomp_prems
-
- fun reify_prem (_, (b, ctor, (x, y))) (ps, reifytab) =
- (Reifytab.get_var x ##>> Reifytab.get_var y) reifytab
- |>> (fn vp => (b, ctor (apply2 Int_of_integer vp)) :: ps)
- val (reified_prems, reifytab) = fold_rev reify_prem decomp_prems ([], Reifytab.empty)
+ val assmtab = Termtab.make [(prems_conj, prems_conj_thm)]
+ val replay = replay_order_prf_trm (eq, le, lt) octxt ctxt reifytab assmtab
+ in
+ case proof of
+ NONE => no_tac
+ | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1
+ end
- val reified_prems_conj = foldl1 (fn (x, a) => And (x, a)) (map Atom reified_prems)
- val prems_conj_thm = map fst decomp_prems
- |> foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a])
- |> Conv.fconv_rule Thm.eta_conversion
- val prems_conj = prems_conj_thm |> Thm.prop_of
-
- val proof = raw_order_proc reified_prems_conj
-
- val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt)
- fun pretty_trace () =
- [ ("order kind:", pretty_order_kind (#kind octxt))
- , ("order operators:", pretty_order_ops ctxt order_ops)
- , ("premises:", pretty_thm_list prems)
- , ("selected premises:", pretty_thm_list (map fst decomp_prems))
- , ("reified premises:", Pretty.str (@{make_string} reified_prems))
- , ("contradiction:", Pretty.str (@{make_string} (Option.isSome proof)))
- ]
- |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp])
- |> Pretty.big_list "order solver called with the parameters"
- val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else ()
+ val prems = simp_prems @ prems
+ |> filter (fn p => null (Term.add_vars (Thm.prop_of p) []))
+ |> map (Conv.fconv_rule Thm.eta_conversion)
+ in
+ partition_prems octxt ctxt prems |> map order_tac' |> FIRST
+ end)
- val assmtab = Termtab.make [(prems_conj, prems_conj_thm)]
- val replay = replay_order_prf_trm (eq, le, lt) octxt ctxt reifytab assmtab
- in
- case proof of
- NONE => no_tac
- | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1
- end
+val ad_absurdum_tac = SUBGOAL (fn (A, i) =>
+ case try (Logic_Sig.dest_Trueprop o Logic.strip_assums_concl) A of
+ SOME (nt $ _) =>
+ if nt = Logic_Sig.Not
+ then resolve0_tac [Logic_Sig.notI] i
+ else resolve0_tac [Logic_Sig.ccontr] i
+ | _ => resolve0_tac [Logic_Sig.ccontr] i)
- val prems = simp_prems @ prems
- |> filter (fn p => null (Term.add_vars (Thm.prop_of p) []))
- |> map (Conv.fconv_rule Thm.eta_conversion)
- in
- partition_prems octxt ctxt prems |> map order_tac' |> FIRST
- end)
-
- val ad_absurdum_tac = SUBGOAL (fn (A, i) =>
- case try (Logic_Sig.dest_Trueprop o Logic.strip_assums_concl) A of
- SOME (nt $ _) =>
- if nt = Logic_Sig.Not
- then resolve0_tac [Logic_Sig.notI] i
- else resolve0_tac [Logic_Sig.ccontr] i
- | _ => resolve0_tac [Logic_Sig.ccontr] i)
-
- fun tac raw_order_proc octxt simp_prems ctxt =
- ad_absurdum_tac THEN' order_tac raw_order_proc octxt simp_prems ctxt
+fun tac raw_order_proc octxt simp_prems ctxt =
+ ad_absurdum_tac THEN' order_tac raw_order_proc octxt simp_prems ctxt
end
functor Order_Tac(structure Base_Tac : BASE_ORDER_TAC) = struct
- open Base_Tac
+
+open Base_Tac
+
+fun order_context_eq ({kind = kind1, ops = ops1, ...}, {kind = kind2, ops = ops2, ...}) =
+ let
+ fun ops_list ops = [#eq ops, #le ops, #lt ops]
+ in
+ kind1 = kind2 andalso eq_list (op aconv) (apply2 ops_list (ops1, ops2))
+ end
+val order_data_eq = order_context_eq o apply2 fst
- fun order_context_eq ({kind = kind1, ops = ops1, ...}, {kind = kind2, ops = ops2, ...}) =
- let
- fun ops_list ops = [#eq ops, #le ops, #lt ops]
- in
- kind1 = kind2 andalso eq_list (op aconv) (apply2 ops_list (ops1, ops2))
- end
- val order_data_eq = order_context_eq o apply2 fst
-
- structure Data = Generic_Data(
- type T = (order_context * (order_context -> thm list -> Proof.context -> int -> tactic)) list
- val empty = []
- fun merge data = Library.merge order_data_eq data
- )
+structure Data = Generic_Data(
+ type T = (order_context * (order_context -> thm list -> Proof.context -> int -> tactic)) list
+ val empty = []
+ fun merge data = Library.merge order_data_eq data
+)
- fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy =
- lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
- (fn phi => fn context =>
- let
- val ops = map_order_ops (Morphism.term phi) (#ops octxt)
- val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt)
- val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt)
- val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms}
- in
- context |> Data.map (Library.insert order_data_eq (octxt', raw_proc))
- end)
+fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy =
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
+ (fn phi => fn context =>
+ let
+ val ops = map_order_ops (Morphism.term phi) (#ops octxt)
+ val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt)
+ val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt)
+ val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms}
+ in
+ context |> Data.map (Library.insert order_data_eq (octxt', raw_proc))
+ end)
- fun declare_order {
- ops = ops,
- thms = {
- trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *)
- refl = refl, (* x \<le> x *)
- eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *)
- eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *)
- antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *)
- contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *)
- },
- conv_thms = {
- less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *)
- nless_le = nless_le (* \<not> a < b \<equiv> \<not> a \<le> b \<or> a = b *)
- }
- } =
- declare {
- kind = Order,
- ops = ops,
- thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2),
- ("antisym", antisym), ("contr", contr)],
- conv_thms = [("less_le", less_le), ("nless_le", nless_le)],
- raw_proc = Base_Tac.tac Order_Procedure.po_contr_prf
- }
+fun declare_order {
+ ops = ops,
+ thms = {
+ trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *)
+ refl = refl, (* x \<le> x *)
+ eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *)
+ eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *)
+ antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *)
+ contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *)
+ },
+ conv_thms = {
+ less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *)
+ nless_le = nless_le (* \<not> a < b \<equiv> \<not> a \<le> b \<or> a = b *)
+ }
+ } =
+ declare {
+ kind = Order,
+ ops = ops,
+ thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2),
+ ("antisym", antisym), ("contr", contr)],
+ conv_thms = [("less_le", less_le), ("nless_le", nless_le)],
+ raw_proc = Base_Tac.tac Order_Procedure.po_contr_prf
+ }
- fun declare_linorder {
- ops = ops,
- thms = {
- trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *)
- refl = refl, (* x \<le> x *)
- eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *)
- eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *)
- antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *)
- contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *)
- },
- conv_thms = {
- less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *)
- nless_le = nless_le, (* \<not> x < y \<equiv> y \<le> x *)
- nle_le = nle_le (* \<not> a \<le> b \<equiv> b \<le> a \<and> b \<noteq> a *)
- }
- } =
- declare {
- kind = Linorder,
- ops = ops,
- thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2),
- ("antisym", antisym), ("contr", contr)],
- conv_thms = [("less_le", less_le), ("nless_le", nless_le), ("nle_le", nle_le)],
- raw_proc = Base_Tac.tac Order_Procedure.lo_contr_prf
- }
+fun declare_linorder {
+ ops = ops,
+ thms = {
+ trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *)
+ refl = refl, (* x \<le> x *)
+ eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *)
+ eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *)
+ antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *)
+ contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *)
+ },
+ conv_thms = {
+ less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *)
+ nless_le = nless_le, (* \<not> x < y \<equiv> y \<le> x *)
+ nle_le = nle_le (* \<not> a \<le> b \<equiv> b \<le> a \<and> b \<noteq> a *)
+ }
+ } =
+ declare {
+ kind = Linorder,
+ ops = ops,
+ thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2),
+ ("antisym", antisym), ("contr", contr)],
+ conv_thms = [("less_le", less_le), ("nless_le", nless_le), ("nle_le", nle_le)],
+ raw_proc = Base_Tac.tac Order_Procedure.lo_contr_prf
+ }
- (* Try to solve the goal by calling the order solver with each of the declared orders. *)
- fun tac simp_prems ctxt =
- let fun app_tac (octxt, tac0) = CHANGED o tac0 octxt simp_prems ctxt
- in FIRST' (map app_tac (Data.get (Context.Proof ctxt))) end
-end
+(* Try to solve the goal by calling the order solver with each of the declared orders. *)
+fun tac simp_prems ctxt =
+ let fun app_tac (octxt, tac0) = CHANGED o tac0 octxt simp_prems ctxt
+ in FIRST' (map app_tac (Data.get (Context.Proof ctxt))) end
+
+end
\ No newline at end of file