--- a/src/Provers/order_tac.ML Mon Sep 06 17:03:23 2021 +0200
+++ b/src/Provers/order_tac.ML Tue Sep 07 12:48:00 2021 +0200
@@ -228,7 +228,7 @@
take limit not_less_prems
end
- fun decomp [eq, le, lt] ctxt env t =
+ fun decomp [eq, le, lt] ctxt t =
let
fun is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types
@@ -236,12 +236,12 @@
let
open Order_Procedure
val thy = Proof_Context.theory_of ctxt
- fun try_match pat = try (Pattern.match thy (pat, binop)) env
+ 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')
+ (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
@@ -255,37 +255,69 @@
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
- fun order_tac raw_order_proc octxt env simp_prems =
+ 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
- val [eq, le, lt] = #ops octxt |> map (Envir.subst_term env) |> map Envir.eta_contract
-
fun these' _ [] = []
| these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs
val prems = filter (fn p => null (Term.add_vars (Thm.prop_of p) [])) (simp_prems @ prems)
- val decomp_prems = these' (decomp [eq, le, lt] ctxt env o Thm.prop_of) prems
+ val decomp_prems = these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems
- val decomp_prems = case #kind octxt of
- Order => limit_not_less [eq, le, lt] ctxt decomp_prems
- | _ => decomp_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.subst_term env) |> map Envir.eta_contract
- 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 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)
- fun order_tac' [] _ _ = no_tac
- | order_tac' prems reified_prems reifytab =
- let
val _ = if trace then @{print} ([eq, le, lt], reified_prems, prems)
else ([eq, le, lt], reified_prems, prems)
val reified_prems_conj = foldl1 (fn (x, a) => And (x, a)) (map Atom reified_prems)
- val prems_conj_thm = foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) 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
@@ -299,7 +331,8 @@
| SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1
end
in
- order_tac' (map fst decomp_prems) reified_prems reifytab
+ 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) =>
@@ -311,16 +344,9 @@
| SOME _ => resolve0_tac [Logic_Sig.ccontr] i
| NONE => resolve0_tac [Logic_Sig.ccontr] i)
- fun tac raw_order_proc octxt simp_prems ctxt = SUBGOAL (fn (A, i) =>
- let val goal = Logic.strip_assums_concl A |> Envir.beta_eta_contract
- in
- if null (Term.add_vars goal []) then
- case decomp (#ops octxt) ctxt (Vartab.empty, Vartab.empty) goal of
- NONE => no_tac
- | SOME (_, _, _, env) => EVERY' [ ad_absurdum_tac, CONVERSION Thm.eta_conversion
- , order_tac raw_order_proc octxt env simp_prems ctxt] i
- else no_tac
- end)
+ fun tac raw_order_proc octxt simp_prems ctxt =
+ EVERY' [ ad_absurdum_tac, CONVERSION Thm.eta_conversion
+ , order_tac raw_order_proc octxt simp_prems ctxt]
end