signature REIFY_TABLE =
sig
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
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 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
(* 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_context = {
kind : order_kind,
ops : term list, thms : (string * thm) list, conv_thms : (string * thm) list
}
signature BASE_ORDER_TAC =
sig
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 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 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 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_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 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_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 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 thy = Proof_Context.theory_of ctxt
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 $ _ $ _) => Pattern.matches thy (lt, binop)
| NONE => 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 is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types
fun decomp'' (binop $ t1 $ t2) =
let
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 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 these' _ [] = []
| these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs
val prems = simp_prems @ prems
|> filter (fn p => null (Term.add_vars (Thm.prop_of p) []))
|> map (Conv.fconv_rule Thm.eta_conversion)
val decomp_prems = these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems
fun env_of (_, (_, _, _, env)) = env
val env_groups = maximal_envs (map env_of decomp_prems)
fun order_tac' (_, []) = no_tac
| order_tac' (env, decomp_prems) =
let
val [eq, le, lt] = #ops octxt |> map (Envir.eta_contract o Envir.subst_term env)
val decomp_prems = case #kind octxt of
Order => limit_not_less (#ops octxt) 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 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_term_list =
Pretty.list "" "" o map (Syntax.pretty_term (Config.put show_types true ctxt))
val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt)
fun pretty_type_of t = Pretty.block [ Pretty.str "::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt (Term.fastype_of t)) ]
fun pretty_trace () =
[ ("order kind:", Pretty.str (@{make_string} (#kind octxt)))
, ("order operators:", Pretty.block [ pretty_term_list [eq, le, lt], Pretty.brk 1
, pretty_type_of le ])
, ("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 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
in
map (fn is => ` (env_of o hd) (map (nth decomp_prems) is) |> order_tac') env_groups
|> 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
end
functor Order_Tac(structure Base_Tac : BASE_ORDER_TAC) = struct
fun order_context_eq ({kind = kind1, ops = ops1, ...}, {kind = kind2, ops = ops2, ...}) =
kind1 = kind2 andalso eq_list (op aconv) (ops1, ops2)
fun order_data_eq (x, y) = order_context_eq (fst x, fst y)
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} (fn phi => fn context =>
let
val ops = map (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 = {eq = eq, le = le, lt = lt},
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 = [eq, le, lt],
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 = {eq = eq, le = le, lt = lt},
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 = [eq, le, lt],
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