--- a/CONTRIBUTORS Wed Mar 31 11:24:46 2021 +0200
+++ b/CONTRIBUTORS Wed Mar 31 18:18:03 2021 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* March 2021: Lukas Stevens
+ New order prover
+
* March 2021: Florian Haftmann
Dedicated session for combinatorics.
--- a/src/HOL/Analysis/Interval_Integral.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Wed Mar 31 18:18:03 2021 +0200
@@ -438,8 +438,9 @@
by (rule interval_integral_endpoints_reverse)
show ?thesis
using integrable
- by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
- (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
+ apply (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
+ apply simp_all (* remove some looping cases *)
+ by (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
qed
lemma interval_integrable_isCont:
--- a/src/HOL/Data_Structures/Brother12_Map.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Data_Structures/Brother12_Map.thy Wed Mar 31 18:18:03 2021 +0200
@@ -83,8 +83,11 @@
lemma inorder_del:
"t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
-by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
+ apply (induction h arbitrary: t)
+ apply (auto simp: del_list_simps inorder_n2)
+ apply (auto simp: del_list_simps inorder_n2
inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
+ done
lemma inorder_delete:
"t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
--- a/src/HOL/Data_Structures/Brother12_Set.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Wed Mar 31 18:18:03 2021 +0200
@@ -199,8 +199,11 @@
lemma inorder_del:
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
-by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
+ apply (induction h arbitrary: t)
+ apply (auto simp: del_list_simps inorder_n2 split: option.splits)
+ apply (auto simp: del_list_simps inorder_n2
inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
+ done
lemma inorder_delete:
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
--- a/src/HOL/Data_Structures/Selection.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Data_Structures/Selection.thy Wed Mar 31 18:18:03 2021 +0200
@@ -343,7 +343,8 @@
have mset_eq: "mset xs = mset ls + mset es + mset gs"
unfolding ls_def es_def gs_def by (induction xs) auto
have length_eq: "length xs = length ls + length es + length gs"
- unfolding ls_def es_def gs_def by (induction xs) auto
+ unfolding ls_def es_def gs_def
+ using [[simp_depth_limit = 1]] by (induction xs) auto
have [simp]: "select i es = x" if "i < length es" for i
proof -
have "select i es \<in> set (sort es)" unfolding select_def
@@ -555,7 +556,8 @@
have tw: "(ls, es, gs) = partition3 x xs"
unfolding partition3_def defs One_nat_def ..
have length_eq: "length xs = nl + ne + length gs"
- unfolding nl_def ne_def ls_def es_def gs_def by (induction xs) auto
+ unfolding nl_def ne_def ls_def es_def gs_def
+ using [[simp_depth_limit = 1]] by (induction xs) auto
note IH = "1.IH"(2,3)[OF False x_def tw refl refl]
have "mom_select k xs = (if k < nl then mom_select k ls else if k < nl + ne then x
--- a/src/HOL/Data_Structures/Set2_Join.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Wed Mar 31 18:18:03 2021 +0200
@@ -94,7 +94,27 @@
proof(induction t arbitrary: l b r rule: tree2_induct)
case Leaf thus ?case by simp
next
- case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
+ case (Node y a b z l c r)
+ consider (LT) l1 xin l2 where "(l1,xin,l2) = split y x"
+ and "split \<langle>y, (a, b), z\<rangle> x = (l1, xin, join l2 a z)" and "cmp x a = LT"
+ | (GT) r1 xin r2 where "(r1,xin,r2) = split z x"
+ and "split \<langle>y, (a, b), z\<rangle> x = (join y a r1, xin, r2)" and "cmp x a = GT"
+ | (EQ) "split \<langle>y, (a, b), z\<rangle> x = (y, True, z)" and "cmp x a = EQ"
+ by (force split: cmp_val.splits prod.splits if_splits)
+
+ thus ?case
+ proof cases
+ case (LT l1 xin l2)
+ with Node.IH(1)[OF \<open>(l1,xin,l2) = split y x\<close>[symmetric]] Node.prems
+ show ?thesis by (force intro!: bst_join)
+ next
+ case (GT r1 xin r2)
+ with Node.IH(2)[OF \<open>(r1,xin,r2) = split z x\<close>[symmetric]] Node.prems
+ show ?thesis by (force intro!: bst_join)
+ next
+ case EQ
+ with Node.prems show ?thesis by auto
+ qed
qed
lemma split_inv: "split t x = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
--- a/src/HOL/Library/RBT_Impl.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Wed Mar 31 18:18:03 2021 +0200
@@ -1052,11 +1052,7 @@
end
theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
- apply(induct t)
- apply auto
- apply(rename_tac a b c, subgoal_tac "x = a")
- apply auto
- done
+ by (induct t) (auto simp: antisym_conv3)
(* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
by (induct t) auto *)
@@ -2508,9 +2504,10 @@
lemma rbt_split_min_rbt_lookup: "rbt_split_min t = (a,b,t') \<Longrightarrow> rbt_sorted t \<Longrightarrow> t \<noteq> RBT_Impl.Empty \<Longrightarrow>
rbt_lookup t k = (if k < a then None else if k = a then Some b else rbt_lookup t' k)"
- by (induction t arbitrary: a b t')
- (auto simp: rbt_less_trans antisym_conv3 rbt_less_prop rbt_split_min_set rbt_lookup_rbt_join
- rbt_split_min_rbt_sorted split!: if_splits prod.splits)
+ apply (induction t arbitrary: a b t')
+ apply(simp_all split: if_splits prod.splits)
+ apply(auto simp: rbt_less_prop rbt_split_min_set rbt_lookup_rbt_join rbt_split_min_rbt_sorted)
+ done
lemma rbt_sorted_rbt_join2: "rbt_sorted l \<Longrightarrow> rbt_sorted r \<Longrightarrow>
\<forall>x \<in> set (RBT_Impl.keys l). \<forall>y \<in> set (RBT_Impl.keys r). x < y \<Longrightarrow> rbt_sorted (rbt_join2 l r)"
@@ -2528,9 +2525,11 @@
set (RBT_Impl.keys l) = {a \<in> set (RBT_Impl.keys t). a < x} \<and>
set (RBT_Impl.keys r) = {a \<in> set (RBT_Impl.keys t). x < a} \<and>
rbt_sorted l \<and> rbt_sorted r"
- by (induction t arbitrary: l r)
- (force simp: Let_def set_rbt_join rbt_greater_prop rbt_less_prop
- split: if_splits prod.splits intro!: rbt_sorted_rbt_join)+
+ apply (induction t arbitrary: l r)
+ apply(simp_all split!: prod.splits if_splits)
+ apply(force simp: set_rbt_join rbt_greater_prop rbt_less_prop
+ intro: rbt_sorted_rbt_join)+
+ done
lemma rbt_split_lookup: "rbt_split t x = (l,\<beta>,r) \<Longrightarrow> rbt_sorted t \<Longrightarrow>
rbt_lookup t k = (if k < x then rbt_lookup l k else if k = x then \<beta> else rbt_lookup r k)"
@@ -2884,6 +2883,7 @@
| Some v \<Rightarrow> (case rbt_lookup t2 k of None \<Rightarrow> Some v | _ \<Rightarrow> None))"
using not_small rbt_lookup_iff_keys(2)[of l1] rbt_lookup_iff_keys(3)[of l1]
rbt_lookup_iff_keys(3)[of r1] rbt_split_t1_props
+ using [[simp_depth_limit = 2]]
by (auto simp: rbt_minus_rec.simps[of t1] Branch rbt_split_t1 rbt_lookup_join2
minus_l1_l2(2) minus_r1_r2(2) rbt_split_lookup[OF rbt_split_t1 1(4)] lookup_l1_r1_a
split: option.splits)
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Wed Mar 31 18:18:03 2021 +0200
@@ -189,8 +189,6 @@
apply (drule_tac x = m in spec)
apply (drule subsetD)
apply auto
- apply (drule_tac x = "injf_max m E" in order_less_trans)
- apply auto
done
lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> inj (\<lambda>n. injf_max n E)"
--- a/src/HOL/Orderings.thy Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Orderings.thy Wed Mar 31 18:18:03 2021 +0200
@@ -9,7 +9,8 @@
keywords "print_orders" :: diag
begin
-ML_file \<open>~~/src/Provers/order.ML\<close>
+ML_file \<open>~~/src/Provers/order_procedure.ML\<close>
+ML_file \<open>~~/src/Provers/order_tac.ML\<close>
subsection \<open>Abstract ordering\<close>
@@ -520,114 +521,59 @@
subsection \<open>Reasoning tools setup\<close>
ML \<open>
-signature ORDERS =
-sig
- val print_structures: Proof.context -> unit
- val order_tac: Proof.context -> thm list -> int -> tactic
- val add_struct: string * term list -> string -> attribute
- val del_struct: string * term list -> attribute
-end;
-
-structure Orders: ORDERS =
-struct
-
-(* context data *)
-
-fun struct_eq ((s1: string, ts1), (s2, ts2)) =
- s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
+structure Logic_Signature : LOGIC_SIGNATURE = struct
+ val mk_Trueprop = HOLogic.mk_Trueprop
+ val dest_Trueprop = HOLogic.dest_Trueprop
+ val Trueprop_conv = HOLogic.Trueprop_conv
+ val Not = HOLogic.Not
+ val conj = HOLogic.conj
+ val disj = HOLogic.disj
+
+ val notI = @{thm notI}
+ val ccontr = @{thm ccontr}
+ val conjI = @{thm conjI}
+ val conjE = @{thm conjE}
+ val disjE = @{thm disjE}
-structure Data = Generic_Data
-(
- type T = ((string * term list) * Order_Tac.less_arith) list;
- (* Order structures:
- identifier of the structure, list of operations and record of theorems
- needed to set up the transitivity reasoner,
- identifier and operations identify the structure uniquely. *)
- val empty = [];
- val extend = I;
- fun merge data = AList.join struct_eq (K fst) data;
-);
+ val not_not_conv = Conv.rewr_conv @{thm eq_reflection[OF not_not]}
+ val de_Morgan_conj_conv = Conv.rewr_conv @{thm eq_reflection[OF de_Morgan_conj]}
+ val de_Morgan_disj_conv = Conv.rewr_conv @{thm eq_reflection[OF de_Morgan_disj]}
+ val conj_disj_distribL_conv = Conv.rewr_conv @{thm eq_reflection[OF conj_disj_distribL]}
+ val conj_disj_distribR_conv = Conv.rewr_conv @{thm eq_reflection[OF conj_disj_distribR]}
+end
-fun print_structures ctxt =
+structure HOL_Base_Order_Tac = Base_Order_Tac(
+ structure Logic_Sig = Logic_Signature;
+ (* Exclude types with specialised solvers. *)
+ val excluded_types = [HOLogic.natT, HOLogic.intT, HOLogic.realT]
+)
+
+structure HOL_Order_Tac = Order_Tac(structure Base_Tac = HOL_Base_Order_Tac)
+
+fun print_orders ctxt0 =
let
- val structs = Data.get (Context.Proof ctxt);
+ val ctxt = Config.put show_sorts true ctxt0
+ val orders = HOL_Order_Tac.Data.get (Context.Proof ctxt)
fun pretty_term t = Pretty.block
[Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
Pretty.str "::", Pretty.brk 1,
- Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
- fun pretty_struct ((s, ts), _) = Pretty.block
- [Pretty.str s, Pretty.str ":", Pretty.brk 1,
- Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
+ Pretty.quote (Syntax.pretty_typ ctxt (type_of t)), Pretty.brk 1]
+ fun pretty_order ({kind = kind, ops = ops, ...}, _) =
+ Pretty.block ([Pretty.str (@{make_string} kind), Pretty.str ":", Pretty.brk 1]
+ @ map pretty_term ops)
in
- Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
- end;
+ Pretty.writeln (Pretty.big_list "order structures:" (map pretty_order orders))
+ end
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_orders\<close>
"print order structures available to transitivity reasoner"
- (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of)));
-
-
-(* tactics *)
+ (Scan.succeed (Toplevel.keep (print_orders o Toplevel.context_of)))
-fun struct_tac ((s, ops), thms) ctxt facts =
- let
- val [eq, le, less] = ops;
- fun decomp thy (\<^const>\<open>Trueprop\<close> $ t) =
- let
- fun excluded t =
- (* exclude numeric types: linear arithmetic subsumes transitivity *)
- let val T = type_of t
- in
- T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
- end;
- fun rel (bin_op $ t1 $ t2) =
- if excluded t1 then NONE
- else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
- else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
- else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
- else NONE
- | rel _ = NONE;
- fun dec (Const (\<^const_name>\<open>Not\<close>, _) $ t) =
- (case rel t of NONE =>
- NONE
- | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
- | dec x = rel x;
- in dec t end
- | decomp _ _ = NONE;
- in
- (case s of
- "order" => Order_Tac.partial_tac decomp thms ctxt facts
- | "linorder" => Order_Tac.linear_tac decomp thms ctxt facts
- | _ => error ("Unknown order kind " ^ quote s ^ " encountered in transitivity reasoner"))
- end
-
-fun order_tac ctxt facts =
- FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt)));
-
-
-(* attributes *)
-
-fun add_struct s tag =
- Thm.declaration_attribute
- (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
-fun del_struct s =
- Thm.declaration_attribute
- (fn _ => Data.map (AList.delete struct_eq s));
-
-end;
\<close>
-attribute_setup order = \<open>
- Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
- Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag
- | ((NONE, n), ts) => Orders.del_struct (n, ts))
-\<close> "theorems controlling transitivity reasoner"
-
method_setup order = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (HOL_Order_Tac.tac [] ctxt))
\<close> "transitivity reasoner"
@@ -636,93 +582,43 @@
context order
begin
-(* The type constraint on @{term (=}) below is necessary since the operation
- is not a parameter of the locale. *)
-
-declare less_irrefl [THEN notE, order add less_reflE: order "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "(<=)" "(<)"]
-
-declare order_refl [order add le_refl: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_le [order add less_imp_le: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order.antisym [order add eqI: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_refl [order add eqD1: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare sym [THEN eq_refl, order add eqD2: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+lemma nless_le: "(\<not> a < b) \<longleftrightarrow> (\<not> a \<le> b) \<or> a = b"
+ using local.dual_order.order_iff_strict by blast
-declare less_trans [order add less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_le_trans [order add less_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_less_trans [order add le_less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order_trans [order add le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_neq_trans [order add le_neq_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare neq_le_trans [order add neq_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_neq [order add less_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_sym [order add not_sym: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+local_setup \<open>
+ HOL_Order_Tac.declare_order {
+ ops = {eq = @{term \<open>(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>}, le = @{term \<open>(\<le>)\<close>}, lt = @{term \<open>(<)\<close>}},
+ thms = {trans = @{thm order_trans}, refl = @{thm order_refl}, eqD1 = @{thm eq_refl},
+ eqD2 = @{thm eq_refl[OF sym]}, antisym = @{thm order_antisym}, contr = @{thm notE}},
+ conv_thms = {less_le = @{thm eq_reflection[OF less_le]},
+ nless_le = @{thm eq_reflection[OF nless_le]}}
+ }
+\<close>
end
context linorder
begin
-declare [[order del: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]]
-
-declare less_irrefl [THEN notE, order add less_reflE: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order_refl [order add le_refl: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_le [order add less_imp_le: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_less [THEN iffD2, order add not_lessI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_le [THEN iffD2, order add not_leI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_less [THEN iffD1, order add not_lessD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_le [THEN iffD1, order add not_leD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order.antisym [order add eqI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_refl [order add eqD1: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+lemma nle_le: "(\<not> a \<le> b) \<longleftrightarrow> b \<le> a \<and> b \<noteq> a"
+ using not_le less_le by simp
-declare sym [THEN eq_refl, order add eqD2: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_trans [order add less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_le_trans [order add less_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_less_trans [order add le_less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order_trans [order add le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_neq_trans [order add le_neq_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare neq_le_trans [order add neq_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_neq [order add less_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_sym [order add not_sym: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+local_setup \<open>
+ HOL_Order_Tac.declare_linorder {
+ ops = {eq = @{term \<open>(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>}, le = @{term \<open>(\<le>)\<close>}, lt = @{term \<open>(<)\<close>}},
+ thms = {trans = @{thm order_trans}, refl = @{thm order_refl}, eqD1 = @{thm eq_refl},
+ eqD2 = @{thm eq_refl[OF sym]}, antisym = @{thm order_antisym}, contr = @{thm notE}},
+ conv_thms = {less_le = @{thm eq_reflection[OF less_le]},
+ nless_le = @{thm eq_reflection[OF not_less]},
+ nle_le = @{thm eq_reflection[OF nle_le]}}
+ }
+\<close>
end
setup \<open>
map_theory_simpset (fn ctxt0 => ctxt0 addSolver
- mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt)))
- (*Adding the transitivity reasoners also as safe solvers showed a slight
- speed up, but the reasoning strength appears to be not higher (at least
- no breaking of additional proofs in the entire HOL distribution, as
- of 5 March 2004, was observed).*)
+ mk_solver "Transitivity" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt))
\<close>
ML \<open>
@@ -765,7 +661,7 @@
| SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
end
| SOME thm => SOME (mk_meta_eq (thm RS @{thm antisym_conv2})))
- end handle THM _ => NONE)
+ end handle THM _ => NONE)
| _ => NONE);
end;
@@ -1226,6 +1122,7 @@
case False with \<open>x \<le> y\<close> have "x < y" by simp
with assms strict_monoD have "f x < f y" by auto
then show ?thesis by simp
+
qed
qed
--- a/src/Provers/order.ML Wed Mar 31 11:24:46 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1264 +0,0 @@
-(* Title: Provers/order.ML
- Author: Oliver Kutter, TU Muenchen
-
-Transitivity reasoner for partial and linear orders.
-*)
-
-(* TODO: reduce number of input thms *)
-
-(*
-
-The package provides tactics partial_tac and linear_tac that use all
-premises of the form
-
- t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
-
-to
-1. either derive a contradiction,
- in which case the conclusion can be any term,
-2. or prove the conclusion, which must be of the same form as the
- premises (excluding ~(t < u) and ~(t <= u) for partial orders)
-
-The package is not limited to the relation <= and friends. It can be
-instantiated to any partial and/or linear order --- for example, the
-divisibility relation "dvd". In order to instantiate the package for
-a partial order only, supply dummy theorems to the rules for linear
-orders, and don't use linear_tac!
-
-*)
-
-signature ORDER_TAC =
-sig
- (* Theorems required by the reasoner *)
- type less_arith
- val empty : thm -> less_arith
- val update : string -> thm -> less_arith -> less_arith
-
- (* Tactics *)
- val partial_tac:
- (theory -> term -> (term * string * term) option) -> less_arith ->
- Proof.context -> thm list -> int -> tactic
- val linear_tac:
- (theory -> term -> (term * string * term) option) -> less_arith ->
- Proof.context -> thm list -> int -> tactic
-end;
-
-structure Order_Tac: ORDER_TAC =
-struct
-
-(* Record to handle input theorems in a convenient way. *)
-
-type less_arith =
- {
- (* Theorems for partial orders *)
- less_reflE: thm, (* x < x ==> P *)
- le_refl: thm, (* x <= x *)
- less_imp_le: thm, (* x < y ==> x <= y *)
- eqI: thm, (* [| x <= y; y <= x |] ==> x = y *)
- eqD1: thm, (* x = y ==> x <= y *)
- eqD2: thm, (* x = y ==> y <= x *)
- less_trans: thm, (* [| x < y; y < z |] ==> x < z *)
- less_le_trans: thm, (* [| x < y; y <= z |] ==> x < z *)
- le_less_trans: thm, (* [| x <= y; y < z |] ==> x < z *)
- le_trans: thm, (* [| x <= y; y <= z |] ==> x <= z *)
- le_neq_trans : thm, (* [| x <= y ; x ~= y |] ==> x < y *)
- neq_le_trans : thm, (* [| x ~= y ; x <= y |] ==> x < y *)
- not_sym : thm, (* x ~= y ==> y ~= x *)
-
- (* Additional theorems for linear orders *)
- not_lessD: thm, (* ~(x < y) ==> y <= x *)
- not_leD: thm, (* ~(x <= y) ==> y < x *)
- not_lessI: thm, (* y <= x ==> ~(x < y) *)
- not_leI: thm, (* y < x ==> ~(x <= y) *)
-
- (* Additional theorems for subgoals of form x ~= y *)
- less_imp_neq : thm, (* x < y ==> x ~= y *)
- eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
- }
-
-fun empty dummy_thm =
- {less_reflE= dummy_thm, le_refl= dummy_thm, less_imp_le= dummy_thm, eqI= dummy_thm,
- eqD1= dummy_thm, eqD2= dummy_thm,
- less_trans= dummy_thm, less_le_trans= dummy_thm, le_less_trans= dummy_thm,
- le_trans= dummy_thm, le_neq_trans = dummy_thm, neq_le_trans = dummy_thm,
- not_sym = dummy_thm,
- not_lessD= dummy_thm, not_leD= dummy_thm, not_lessI= dummy_thm, not_leI= dummy_thm,
- less_imp_neq = dummy_thm, eq_neq_eq_imp_neq = dummy_thm}
-
-fun change thms f =
- let
- val {less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq} = thms;
- val (less_reflE', le_refl', less_imp_le', eqI', eqD1', eqD2', less_trans',
- less_le_trans', le_less_trans', le_trans', le_neq_trans', neq_le_trans',
- not_sym', not_lessD', not_leD', not_lessI', not_leI', less_imp_neq',
- eq_neq_eq_imp_neq') =
- f (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq)
- in {less_reflE = less_reflE', le_refl= le_refl',
- less_imp_le = less_imp_le', eqI = eqI', eqD1 = eqD1', eqD2 = eqD2',
- less_trans = less_trans', less_le_trans = less_le_trans',
- le_less_trans = le_less_trans', le_trans = le_trans', le_neq_trans = le_neq_trans',
- neq_le_trans = neq_le_trans', not_sym = not_sym',
- not_lessD = not_lessD', not_leD = not_leD', not_lessI = not_lessI',
- not_leI = not_leI',
- less_imp_neq = less_imp_neq', eq_neq_eq_imp_neq = eq_neq_eq_imp_neq'}
- end;
-
-fun update "less_reflE" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (thm, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "le_refl" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, thm, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "less_imp_le" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, thm, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "eqI" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, thm, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "eqD1" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, thm, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "eqD2" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, thm, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "less_trans" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, thm,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "less_le_trans" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- thm, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "le_less_trans" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, thm, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "le_trans" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, thm, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "le_neq_trans" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, thm, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "neq_le_trans" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, thm,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "not_sym" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- thm, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "not_lessD" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, thm, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "not_leD" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, thm, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "not_lessI" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, thm, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
- | update "not_leI" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, thm, less_imp_neq, eq_neq_eq_imp_neq))
- | update "less_imp_neq" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, thm, eq_neq_eq_imp_neq))
- | update "eq_neq_eq_imp_neq" thm thms =
- change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
- eq_neq_eq_imp_neq) =>
- (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
- less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
- not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm));
-
-(* Internal datatype for the proof *)
-datatype proof
- = Asm of int
- | Thm of proof list * thm;
-
-exception Cannot;
- (* Internal exception, raised if conclusion cannot be derived from
- assumptions. *)
-exception Contr of proof;
- (* Internal exception, raised if contradiction ( x < x ) was derived *)
-
-fun prove asms =
- let
- fun pr (Asm i) = nth asms i
- | pr (Thm (prfs, thm)) = map pr prfs MRS thm;
- in pr end;
-
-(* Internal datatype for inequalities *)
-datatype less
- = Less of term * term * proof
- | Le of term * term * proof
- | NotEq of term * term * proof;
-
-(* Misc functions for datatype less *)
-fun lower (Less (x, _, _)) = x
- | lower (Le (x, _, _)) = x
- | lower (NotEq (x,_,_)) = x;
-
-fun upper (Less (_, y, _)) = y
- | upper (Le (_, y, _)) = y
- | upper (NotEq (_,y,_)) = y;
-
-fun getprf (Less (_, _, p)) = p
-| getprf (Le (_, _, p)) = p
-| getprf (NotEq (_,_, p)) = p;
-
-
-(* ************************************************************************ *)
-(* *)
-(* mkasm_partial *)
-(* *)
-(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *)
-(* translated to an element of type less. *)
-(* Partial orders only. *)
-(* *)
-(* ************************************************************************ *)
-
-fun mkasm_partial decomp (less_thms : less_arith) sign (n, t) =
- case decomp sign t of
- SOME (x, rel, y) => (case rel of
- "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
- else [Less (x, y, Asm n)]
- | "~<" => []
- | "<=" => [Le (x, y, Asm n)]
- | "~<=" => []
- | "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
- Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
- | "~=" => if (x aconv y) then
- raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
- else [ NotEq (x, y, Asm n),
- NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
- | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^
- "''returned by decomp."))
- | NONE => [];
-
-(* ************************************************************************ *)
-(* *)
-(* mkasm_linear *)
-(* *)
-(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *)
-(* translated to an element of type less. *)
-(* Linear orders only. *)
-(* *)
-(* ************************************************************************ *)
-
-fun mkasm_linear decomp (less_thms : less_arith) sign (n, t) =
- case decomp sign t of
- SOME (x, rel, y) => (case rel of
- "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
- else [Less (x, y, Asm n)]
- | "~<" => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))]
- | "<=" => [Le (x, y, Asm n)]
- | "~<=" => if (x aconv y) then
- raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms)))
- else [Less (y, x, Thm ([Asm n], #not_leD less_thms))]
- | "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
- Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
- | "~=" => if (x aconv y) then
- raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
- else [ NotEq (x, y, Asm n),
- NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
- | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^
- "''returned by decomp."))
- | NONE => [];
-
-(* ************************************************************************ *)
-(* *)
-(* mkconcl_partial *)
-(* *)
-(* Translates conclusion t to an element of type less. *)
-(* Partial orders only. *)
-(* *)
-(* ************************************************************************ *)
-
-fun mkconcl_partial decomp (less_thms : less_arith) sign t =
- case decomp sign t of
- SOME (x, rel, y) => (case rel of
- "<" => ([Less (x, y, Asm ~1)], Asm 0)
- | "<=" => ([Le (x, y, Asm ~1)], Asm 0)
- | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
- Thm ([Asm 0, Asm 1], #eqI less_thms))
- | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0)
- | _ => raise Cannot)
- | NONE => raise Cannot;
-
-(* ************************************************************************ *)
-(* *)
-(* mkconcl_linear *)
-(* *)
-(* Translates conclusion t to an element of type less. *)
-(* Linear orders only. *)
-(* *)
-(* ************************************************************************ *)
-
-fun mkconcl_linear decomp (less_thms : less_arith) sign t =
- case decomp sign t of
- SOME (x, rel, y) => (case rel of
- "<" => ([Less (x, y, Asm ~1)], Asm 0)
- | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], #not_lessI less_thms))
- | "<=" => ([Le (x, y, Asm ~1)], Asm 0)
- | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], #not_leI less_thms))
- | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
- Thm ([Asm 0, Asm 1], #eqI less_thms))
- | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0)
- | _ => raise Cannot)
- | NONE => raise Cannot;
-
-
-(*** The common part for partial and linear orders ***)
-
-(* Analysis of premises and conclusion: *)
-(* decomp (`x Rel y') should yield (x, Rel, y)
- where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
- other relation symbols cause an error message *)
-
-fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems =
-
-let
-
-fun decomp sign t = Option.map (fn (x, rel, y) =>
- (Envir.beta_eta_contract x, rel, Envir.beta_eta_contract y)) (decomp' sign t);
-
-(* ******************************************************************* *)
-(* *)
-(* mergeLess *)
-(* *)
-(* Merge two elements of type less according to the following rules *)
-(* *)
-(* x < y && y < z ==> x < z *)
-(* x < y && y <= z ==> x < z *)
-(* x <= y && y < z ==> x < z *)
-(* x <= y && y <= z ==> x <= z *)
-(* x <= y && x ~= y ==> x < y *)
-(* x ~= y && x <= y ==> x < y *)
-(* x < y && x ~= y ==> x < y *)
-(* x ~= y && x < y ==> x < y *)
-(* *)
-(* ******************************************************************* *)
-
-fun mergeLess (Less (x, _, p) , Less (_ , z, q)) =
- Less (x, z, Thm ([p,q] , #less_trans less_thms))
-| mergeLess (Less (x, _, p) , Le (_ , z, q)) =
- Less (x, z, Thm ([p,q] , #less_le_trans less_thms))
-| mergeLess (Le (x, _, p) , Less (_ , z, q)) =
- Less (x, z, Thm ([p,q] , #le_less_trans less_thms))
-| mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
- if (x aconv x' andalso z aconv z' )
- then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms))
- else error "linear/partial_tac: internal error le_neq_trans"
-| mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
- if (x aconv x' andalso z aconv z')
- then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms))
- else error "linear/partial_tac: internal error neq_le_trans"
-| mergeLess (NotEq (x, z, p) , Less (x' , z', q)) =
- if (x aconv x' andalso z aconv z')
- then Less ((x' , z', q))
- else error "linear/partial_tac: internal error neq_less_trans"
-| mergeLess (Less (x, z, p) , NotEq (x', z', q)) =
- if (x aconv x' andalso z aconv z')
- then Less (x, z, p)
- else error "linear/partial_tac: internal error less_neq_trans"
-| mergeLess (Le (x, _, p) , Le (_ , z, q)) =
- Le (x, z, Thm ([p,q] , #le_trans less_thms))
-| mergeLess (_, _) =
- error "linear/partial_tac: internal error: undefined case";
-
-
-(* ******************************************************************** *)
-(* tr checks for valid transitivity step *)
-(* ******************************************************************** *)
-
-infix tr;
-fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' )
- | (Le (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
- | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
- | (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' )
- | _ tr _ = false;
-
-
-(* ******************************************************************* *)
-(* *)
-(* transPath (Lesslist, Less): (less list * less) -> less *)
-(* *)
-(* If a path represented by a list of elements of type less is found, *)
-(* this needs to be contracted to a single element of type less. *)
-(* Prior to each transitivity step it is checked whether the step is *)
-(* valid. *)
-(* *)
-(* ******************************************************************* *)
-
-fun transPath ([],lesss) = lesss
-| transPath (x::xs,lesss) =
- if lesss tr x then transPath (xs, mergeLess(lesss,x))
- else error "linear/partial_tac: internal error transpath";
-
-(* ******************************************************************* *)
-(* *)
-(* less1 subsumes less2 : less -> less -> bool *)
-(* *)
-(* subsumes checks whether less1 implies less2 *)
-(* *)
-(* ******************************************************************* *)
-
-infix subsumes;
-fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
- (x aconv x' andalso y aconv y')
- | (Less (x, y, _)) subsumes (Less (x', y', _)) =
- (x aconv x' andalso y aconv y')
- | (Le (x, y, _)) subsumes (Le (x', y', _)) =
- (x aconv x' andalso y aconv y')
- | (Less (x, y, _)) subsumes (NotEq (x', y', _)) =
- (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
- | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) =
- (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
- | (Le _) subsumes (Less _) =
- error "linear/partial_tac: internal error: Le cannot subsume Less"
- | _ subsumes _ = false;
-
-(* ******************************************************************* *)
-(* *)
-(* triv_solv less1 : less -> proof option *)
-(* *)
-(* Solves trivial goal x <= x. *)
-(* *)
-(* ******************************************************************* *)
-
-fun triv_solv (Le (x, x', _)) =
- if x aconv x' then SOME (Thm ([], #le_refl less_thms))
- else NONE
-| triv_solv _ = NONE;
-
-(* ********************************************************************* *)
-(* Graph functions *)
-(* ********************************************************************* *)
-
-
-
-(* ******************************************************************* *)
-(* *)
-(* General: *)
-(* *)
-(* Inequalities are represented by various types of graphs. *)
-(* *)
-(* 1. (Term.term * (Term.term * less) list) list *)
-(* - Graph of this type is generated from the assumptions, *)
-(* it does contain information on which edge stems from which *)
-(* assumption. *)
-(* - Used to compute strongly connected components *)
-(* - Used to compute component subgraphs *)
-(* - Used for component subgraphs to reconstruct paths in components*)
-(* *)
-(* 2. (int * (int * less) list ) list *)
-(* - Graph of this type is generated from the strong components of *)
-(* graph of type 1. It consists of the strong components of *)
-(* graph 1, where nodes are indices of the components. *)
-(* Only edges between components are part of this graph. *)
-(* - Used to reconstruct paths between several components. *)
-(* *)
-(* ******************************************************************* *)
-
-
-(* *********************************************************** *)
-(* Functions for constructing graphs *)
-(* *********************************************************** *)
-
-fun addEdge (v,d,[]) = [(v,d)]
-| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
- else (u,dl):: (addEdge(v,d,el));
-
-(* ********************************************************************* *)
-(* *)
-(* mkGraphs constructs from a list of objects of type less a graph g, *)
-(* by taking all edges that are candidate for a <=, and a list neqE, by *)
-(* taking all edges that are candiate for a ~= *)
-(* *)
-(* ********************************************************************* *)
-
-fun mkGraphs [] = ([],[],[])
-| mkGraphs lessList =
- let
-
-fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE)
-| buildGraphs (l::ls, leqG,neqG, neqE) = case l of
- (Less (x,y,p)) =>
- buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) ,
- addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE)
-| (Le (x,y,p)) =>
- buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE)
-| (NotEq (x,y,p)) =>
- buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ;
-
- in buildGraphs (lessList, [], [], []) end;
-
-
-(* *********************************************************************** *)
-(* *)
-(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *)
-(* *)
-(* List of successors of u in graph g *)
-(* *)
-(* *********************************************************************** *)
-
-fun adjacent eq_comp ((v,adj)::el) u =
- if eq_comp (u, v) then adj else adjacent eq_comp el u
-| adjacent _ [] _ = []
-
-
-(* *********************************************************************** *)
-(* *)
-(* transpose g: *)
-(* (''a * ''a list) list -> (''a * ''a list) list *)
-(* *)
-(* Computes transposed graph g' from g *)
-(* by reversing all edges u -> v to v -> u *)
-(* *)
-(* *********************************************************************** *)
-
-fun transpose eq_comp g =
- let
- (* Compute list of reversed edges for each adjacency list *)
- fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
- | flip (_,[]) = []
-
- (* Compute adjacency list for node u from the list of edges
- and return a likewise reduced list of edges. The list of edges
- is searches for edges starting from u, and these edges are removed. *)
- fun gather (u,(v,w)::el) =
- let
- val (adj,edges) = gather (u,el)
- in
- if eq_comp (u, v) then (w::adj,edges)
- else (adj,(v,w)::edges)
- end
- | gather (_,[]) = ([],[])
-
- (* For every node in the input graph, call gather to find all reachable
- nodes in the list of edges *)
- fun assemble ((u,_)::el) edges =
- let val (adj,edges) = gather (u,edges)
- in (u,adj) :: assemble el edges
- end
- | assemble [] _ = []
-
- (* Compute, for each adjacency list, the list with reversed edges,
- and concatenate these lists. *)
- val flipped = maps flip g
-
- in assemble g flipped end
-
-(* *********************************************************************** *)
-(* *)
-(* scc_term : (term * term list) list -> term list list *)
-(* *)
-(* The following is based on the algorithm for finding strongly connected *)
-(* components described in Introduction to Algorithms, by Cormon, Leiserson*)
-(* and Rivest, section 23.5. The input G is an adjacency list description *)
-(* of a directed graph. The output is a list of the strongly connected *)
-(* components (each a list of vertices). *)
-(* *)
-(* *)
-(* *********************************************************************** *)
-
-fun scc_term G =
- let
- (* Ordered list of the vertices that DFS has finished with;
- most recently finished goes at the head. *)
- val finish : term list Unsynchronized.ref = Unsynchronized.ref []
-
- (* List of vertices which have been visited. *)
- val visited : term list Unsynchronized.ref = Unsynchronized.ref []
-
- fun been_visited v = exists (fn w => w aconv v) (!visited)
-
- (* Given the adjacency list rep of a graph (a list of pairs),
- return just the first element of each pair, yielding the
- vertex list. *)
- val members = map (fn (v,_) => v)
-
- (* Returns the nodes in the DFS tree rooted at u in g *)
- fun dfs_visit g u : term list =
- let
- val _ = visited := u :: !visited
- val descendents =
- List.foldr (fn ((v,l),ds) => if been_visited v then ds
- else v :: dfs_visit g v @ ds)
- [] (adjacent (op aconv) g u)
- in
- finish := u :: !finish;
- descendents
- end
- in
-
- (* DFS on the graph; apply dfs_visit to each vertex in
- the graph, checking first to make sure the vertex is
- as yet unvisited. *)
- List.app (fn u => if been_visited u then ()
- else (dfs_visit G u; ())) (members G);
- visited := [];
-
- (* We don't reset finish because its value is used by
- foldl below, and it will never be used again (even
- though dfs_visit will continue to modify it). *)
-
- (* DFS on the transpose. The vertices returned by
- dfs_visit along with u form a connected component. We
- collect all the connected components together in a
- list, which is what is returned. *)
- fold (fn u => fn comps =>
- if been_visited u then comps
- else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) []
-end;
-
-
-(* *********************************************************************** *)
-(* *)
-(* dfs_int_reachable g u: *)
-(* (int * int list) list -> int -> int list *)
-(* *)
-(* Computes list of all nodes reachable from u in g. *)
-(* *)
-(* *********************************************************************** *)
-
-fun dfs_int_reachable g u =
- let
- (* List of vertices which have been visited. *)
- val visited : int list Unsynchronized.ref = Unsynchronized.ref []
-
- fun been_visited v = exists (fn w => w = v) (!visited)
-
- fun dfs_visit g u : int list =
- let
- val _ = visited := u :: !visited
- val descendents =
- List.foldr (fn ((v,l),ds) => if been_visited v then ds
- else v :: dfs_visit g v @ ds)
- [] (adjacent (op =) g u)
- in descendents end
-
- in u :: dfs_visit g u end;
-
-
-fun indexNodes IndexComp =
- maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
-
-fun getIndex v [] = ~1
-| getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
-
-
-
-(* *********************************************************************** *)
-(* *)
-(* dfs eq_comp g u v: *)
-(* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *)
-(* 'a -> 'a -> (bool * ('a * less) list) *)
-(* *)
-(* Depth first search of v from u. *)
-(* Returns (true, path(u, v)) if successful, otherwise (false, []). *)
-(* *)
-(* *********************************************************************** *)
-
-fun dfs eq_comp g u v =
- let
- val pred = Unsynchronized.ref [];
- val visited = Unsynchronized.ref [];
-
- fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
-
- fun dfs_visit u' =
- let val _ = visited := u' :: (!visited)
-
- fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
-
- in if been_visited v then ()
- else (List.app (fn (v',l) => if been_visited v' then () else (
- update (v',l);
- dfs_visit v'; ()) )) (adjacent eq_comp g u')
- end
- in
- dfs_visit u;
- if (been_visited v) then (true, (!pred)) else (false , [])
- end;
-
-
-(* *********************************************************************** *)
-(* *)
-(* completeTermPath u v g: *)
-(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list *)
-(* -> less list *)
-(* *)
-(* Complete the path from u to v in graph g. Path search is performed *)
-(* with dfs_term g u v. This yields for each node v' its predecessor u' *)
-(* and the edge u' -> v'. Allows traversing graph backwards from v and *)
-(* finding the path u -> v. *)
-(* *)
-(* *********************************************************************** *)
-
-
-fun completeTermPath u v g =
- let
- val (found, tmp) = dfs (op aconv) g u v ;
- val pred = map snd tmp;
-
- fun path x y =
- let
-
- (* find predecessor u of node v and the edge u -> v *)
-
- fun lookup v [] = raise Cannot
- | lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
-
- (* traverse path backwards and return list of visited edges *)
- fun rev_path v =
- let val l = lookup v pred
- val u = lower l;
- in
- if u aconv x then [l]
- else (rev_path u) @ [l]
- end
- in rev_path y end;
-
- in
- if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))]
- else path u v ) else raise Cannot
-end;
-
-
-(* *********************************************************************** *)
-(* *)
-(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal: *)
-(* *)
-(* (int * (int * less) list) list * less list * (Term.term * int) list *)
-(* * ((term * (term * less) list) list) list -> Less -> proof *)
-(* *)
-(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *)
-(* proof for subgoal. Raises exception Cannot if this is not possible. *)
-(* *)
-(* *********************************************************************** *)
-
-fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
-let
-
- (* complete path x y from component graph *)
- fun completeComponentPath x y predlist =
- let
- val xi = getIndex x ntc
- val yi = getIndex y ntc
-
- fun lookup k [] = raise Cannot
- | lookup k ((h: int,l)::us) = if k = h then l else lookup k us;
-
- fun rev_completeComponentPath y' =
- let val edge = lookup (getIndex y' ntc) predlist
- val u = lower edge
- val v = upper edge
- in
- if (getIndex u ntc) = xi then
- completeTermPath x u (nth sccSubgraphs xi) @ [edge] @
- completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
- else
- rev_completeComponentPath u @ [edge] @
- completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
- end
- in
- if x aconv y then
- [(Le (x, y, (Thm ([], #le_refl less_thms))))]
- else if xi = yi then completeTermPath x y (nth sccSubgraphs xi)
- else rev_completeComponentPath y
- end;
-
-(* ******************************************************************* *)
-(* findLess e x y xi yi xreachable yreachable *)
-(* *)
-(* Find a path from x through e to y, of weight < *)
-(* ******************************************************************* *)
-
- fun findLess e x y xi yi xreachable yreachable =
- let val u = lower e
- val v = upper e
- val ui = getIndex u ntc
- val vi = getIndex v ntc
-
- in
- if member (op =) xreachable ui andalso member (op =) xreachable vi andalso
- member (op =) yreachable ui andalso member (op =) yreachable vi then (
-
- (case e of (Less (_, _, _)) =>
- let
- val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
- in
- if xufound then (
- let
- val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi
- in
- if vyfound then (
- let
- val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
- val xyLesss = transPath (tl xypath, hd xypath)
- in
- if xyLesss subsumes subgoal then SOME (getprf xyLesss)
- else NONE
- end)
- else NONE
- end)
- else NONE
- end
- | _ =>
- let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc)
- in
- if uvfound then (
- let
- val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
- in
- if xufound then (
- let
- val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi
- in
- if vyfound then (
- let
- val uvpath = completeComponentPath u v uvpred
- val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
- val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
- val xyLesss = transPath (tl xypath, hd xypath)
- in
- if xyLesss subsumes subgoal then SOME (getprf xyLesss)
- else NONE
- end )
- else NONE
- end)
- else NONE
- end )
- else NONE
- end )
- ) else NONE
-end;
-
-
-in
- (* looking for x <= y: any path from x to y is sufficient *)
- case subgoal of (Le (x, y, _)) => (
- if null sccGraph then raise Cannot else (
- let
- val xi = getIndex x ntc
- val yi = getIndex y ntc
- (* searches in sccGraph a path from xi to yi *)
- val (found, pred) = dfs (op =) sccGraph xi yi
- in
- if found then (
- let val xypath = completeComponentPath x y pred
- val xyLesss = transPath (tl xypath, hd xypath)
- in
- (case xyLesss of
- (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))
- else raise Cannot
- | _ => if xyLesss subsumes subgoal then (getprf xyLesss)
- else raise Cannot)
- end )
- else raise Cannot
- end
- )
- )
- (* looking for x < y: particular path required, which is not necessarily
- found by normal dfs *)
- | (Less (x, y, _)) => (
- if null sccGraph then raise Cannot else (
- let
- val xi = getIndex x ntc
- val yi = getIndex y ntc
- val sccGraph_transpose = transpose (op =) sccGraph
- (* all components that can be reached from component xi *)
- val xreachable = dfs_int_reachable sccGraph xi
- (* all comonents reachable from y in the transposed graph sccGraph' *)
- val yreachable = dfs_int_reachable sccGraph_transpose yi
- (* for all edges u ~= v or u < v check if they are part of path x < y *)
- fun processNeqEdges [] = raise Cannot
- | processNeqEdges (e::es) =
- case (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf
- | _ => processNeqEdges es
-
- in
- processNeqEdges neqE
- end
- )
- )
-| (NotEq (x, y, _)) => (
- (* if there aren't any edges that are candidate for a ~= raise Cannot *)
- if null neqE then raise Cannot
- (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
- else if null sccSubgraphs then (
- (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
- ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
- if (x aconv x' andalso y aconv y') then p
- else Thm ([p], #not_sym less_thms)
- | ( SOME (Less (x, y, p)), NotEq (x', y', _)) =>
- if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms))
- else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms))
- | _ => raise Cannot)
- ) else (
-
- let val xi = getIndex x ntc
- val yi = getIndex y ntc
- val sccGraph_transpose = transpose (op =) sccGraph
- val xreachable = dfs_int_reachable sccGraph xi
- val yreachable = dfs_int_reachable sccGraph_transpose yi
-
- fun processNeqEdges [] = raise Cannot
- | processNeqEdges (e::es) = (
- let val u = lower e
- val v = upper e
- val ui = getIndex u ntc
- val vi = getIndex v ntc
-
- in
- (* if x ~= y follows from edge e *)
- if e subsumes subgoal then (
- case e of (Less (u, v, q)) => (
- if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
- else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
- )
- | (NotEq (u,v, q)) => (
- if u aconv x andalso v aconv y then q
- else (Thm ([q], #not_sym less_thms))
- )
- )
- (* if SCC_x is linked to SCC_y via edge e *)
- else if ui = xi andalso vi = yi then (
- case e of (Less (_, _,_)) => (
- let
- val xypath =
- completeTermPath x u (nth sccSubgraphs ui) @ [e] @
- completeTermPath v y (nth sccSubgraphs vi)
- val xyLesss = transPath (tl xypath, hd xypath)
- in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
- | _ => (
- let
- val xupath = completeTermPath x u (nth sccSubgraphs ui)
- val uxpath = completeTermPath u x (nth sccSubgraphs ui)
- val vypath = completeTermPath v y (nth sccSubgraphs vi)
- val yvpath = completeTermPath y v (nth sccSubgraphs vi)
- val xuLesss = transPath (tl xupath, hd xupath)
- val uxLesss = transPath (tl uxpath, hd uxpath)
- val vyLesss = transPath (tl vypath, hd vypath)
- val yvLesss = transPath (tl yvpath, hd yvpath)
- val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
- val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
- in
- (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms))
- end
- )
- ) else if ui = yi andalso vi = xi then (
- case e of (Less (_, _,_)) => (
- let
- val xypath =
- completeTermPath y u (nth sccSubgraphs ui) @ [e] @
- completeTermPath v x (nth sccSubgraphs vi)
- val xyLesss = transPath (tl xypath, hd xypath)
- in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end )
- | _ => (
-
- let val yupath = completeTermPath y u (nth sccSubgraphs ui)
- val uypath = completeTermPath u y (nth sccSubgraphs ui)
- val vxpath = completeTermPath v x (nth sccSubgraphs vi)
- val xvpath = completeTermPath x v (nth sccSubgraphs vi)
- val yuLesss = transPath (tl yupath, hd yupath)
- val uyLesss = transPath (tl uypath, hd uypath)
- val vxLesss = transPath (tl vxpath, hd vxpath)
- val xvLesss = transPath (tl xvpath, hd xvpath)
- val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
- val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
- in
- (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
- end
- )
- ) else (
- (* there exists a path x < y or y < x such that
- x ~= y may be concluded *)
- case (findLess e x y xi yi xreachable yreachable) of
- (SOME prf) => (Thm ([prf], #less_imp_neq less_thms))
- | NONE => (
- let
- val yr = dfs_int_reachable sccGraph yi
- val xr = dfs_int_reachable sccGraph_transpose xi
- in
- case (findLess e y x yi xi yr xr) of
- (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms))
- | _ => processNeqEdges es
- end)
- ) end)
- in processNeqEdges neqE end)
- )
-end;
-
-
-(* ******************************************************************* *)
-(* *)
-(* mk_sccGraphs components leqG neqG ntc : *)
-(* Term.term list list -> *)
-(* (Term.term * (Term.term * less) list) list -> *)
-(* (Term.term * (Term.term * less) list) list -> *)
-(* (Term.term * int) list -> *)
-(* (int * (int * less) list) list * *)
-(* ((Term.term * (Term.term * less) list) list) list *)
-(* *)
-(* *)
-(* Computes, from graph leqG, list of all its components and the list *)
-(* ntc (nodes, index of component) a graph whose nodes are the *)
-(* indices of the components of g. Egdes of the new graph are *)
-(* only the edges of g linking two components. Also computes for each *)
-(* component the subgraph of leqG that forms this component. *)
-(* *)
-(* For each component SCC_i is checked if there exists a edge in neqG *)
-(* that leads to a contradiction. *)
-(* *)
-(* We have a contradiction for edge u ~= v and u < v if: *)
-(* - u and v are in the same component, *)
-(* that is, a path u <= v and a path v <= u exist, hence u = v. *)
-(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *)
-(* *)
-(* ******************************************************************* *)
-
-fun mk_sccGraphs _ [] _ _ = ([],[])
-| mk_sccGraphs components leqG neqG ntc =
- let
- (* Liste (Index der Komponente, Komponente *)
- val IndexComp = map_index I components;
-
-
- fun handleContr edge g =
- (case edge of
- (Less (x, y, _)) => (
- let
- val xxpath = edge :: (completeTermPath y x g )
- val xxLesss = transPath (tl xxpath, hd xxpath)
- val q = getprf xxLesss
- in
- raise (Contr (Thm ([q], #less_reflE less_thms )))
- end
- )
- | (NotEq (x, y, _)) => (
- let
- val xypath = (completeTermPath x y g )
- val yxpath = (completeTermPath y x g )
- val xyLesss = transPath (tl xypath, hd xypath)
- val yxLesss = transPath (tl yxpath, hd yxpath)
- val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss ))
- in
- raise (Contr (Thm ([q], #less_reflE less_thms )))
- end
- )
- | _ => error "trans_tac/handleContr: invalid Contradiction");
-
-
- (* k is index of the actual component *)
-
- fun processComponent (k, comp) =
- let
- (* all edges with weight <= of the actual component *)
- val leqEdges = maps (adjacent (op aconv) leqG) comp;
- (* all edges with weight ~= of the actual component *)
- val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp);
-
- (* find an edge leading to a contradiction *)
- fun findContr [] = NONE
- | findContr (e::es) =
- let val ui = (getIndex (lower e) ntc)
- val vi = (getIndex (upper e) ntc)
- in
- if ui = vi then SOME e
- else findContr es
- end;
-
- (* sort edges into component internal edges and
- edges pointing away from the component *)
- fun sortEdges [] (intern,extern) = (intern,extern)
- | sortEdges ((v,l)::es) (intern, extern) =
- let val k' = getIndex v ntc in
- if k' = k then
- sortEdges es (l::intern, extern)
- else sortEdges es (intern, (k',l)::extern) end;
-
- (* Insert edge into sorted list of edges, where edge is
- only added if
- - it is found for the first time
- - it is a <= edge and no parallel < edge was found earlier
- - it is a < edge
- *)
- fun insert (h: int,l) [] = [(h,l)]
- | insert (h,l) ((k',l')::es) = if h = k' then (
- case l of (Less (_, _, _)) => (h,l)::es
- | _ => (case l' of (Less (_, _, _)) => (h,l')::es
- | _ => (k',l)::es) )
- else (k',l'):: insert (h,l) es;
-
- (* Reorganise list of edges such that
- - duplicate edges are removed
- - if a < edge and a <= edge exist at the same time,
- remove <= edge *)
- fun reOrganizeEdges [] sorted = sorted: (int * less) list
- | reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted);
-
- (* construct the subgraph forming the strongly connected component
- from the edge list *)
- fun sccSubGraph [] g = g
- | sccSubGraph (l::ls) g =
- sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
-
- val (intern, extern) = sortEdges leqEdges ([], []);
- val subGraph = sccSubGraph intern [];
-
- in
- case findContr neqEdges of SOME e => handleContr e subGraph
- | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
- end;
-
- val tmp = map processComponent IndexComp
-in
- ( (map fst tmp), (map snd tmp))
-end;
-
-
-(** Find proof if possible. **)
-
-fun gen_solve mkconcl sign (asms, concl) =
- let
- val (leqG, neqG, neqE) = mkGraphs asms
- val components = scc_term leqG
- val ntc = indexNodes (map_index I components)
- val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
- in
- let
- val (subgoals, prf) = mkconcl decomp less_thms sign concl
- fun solve facts less =
- (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
- | SOME prf => prf )
- in
- map (solve asms) subgoals
- end
- end;
-
-in
- SUBGOAL (fn (A, n) => fn st =>
- let
- val thy = Proof_Context.theory_of ctxt;
- val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
- val Hs =
- map Thm.prop_of prems @
- map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
- val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
- val lesss = flat (map_index (mkasm decomp less_thms thy) Hs)
- val prfs = gen_solve mkconcl thy (lesss, C);
- val (subgoals, prf) = mkconcl decomp less_thms thy C;
- in
- Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} =>
- let val thms = map (prove (prems @ asms)) prfs
- in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st
- end
- handle Contr p =>
- (Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} =>
- resolve_tac ctxt' [prove asms p] 1) ctxt n st
- handle General.Subscript => Seq.empty)
- | Cannot => Seq.empty
- | General.Subscript => Seq.empty)
-end;
-
-(* partial_tac - solves partial orders *)
-val partial_tac = gen_order_tac mkasm_partial mkconcl_partial;
-
-(* linear_tac - solves linear/total orders *)
-val linear_tac = gen_order_tac mkasm_linear mkconcl_linear;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/order_procedure.ML Wed Mar 31 18:18:03 2021 +0200
@@ -0,0 +1,604 @@
+structure Order_Procedure : sig
+ datatype int = Int_of_integer of IntInf.int
+ val integer_of_int : int -> IntInf.int
+ datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm |
+ Neg of 'a fm
+ datatype trm = Const of string | App of trm * trm | Var of int
+ datatype prf_trm = PThm of string | Appt of prf_trm * trm |
+ AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm |
+ Conv of trm * prf_trm * prf_trm
+ datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int
+ val lo_contr_prf : (bool * o_atom) fm -> prf_trm option
+ val po_contr_prf : (bool * o_atom) fm -> prf_trm option
+end = struct
+
+datatype int = Int_of_integer of IntInf.int;
+
+fun integer_of_int (Int_of_integer k) = k;
+
+fun equal_inta k l = (((integer_of_int k) : IntInf.int) = (integer_of_int l));
+
+type 'a equal = {equal : 'a -> 'a -> bool};
+val equal = #equal : 'a equal -> 'a -> 'a -> bool;
+
+val equal_int = {equal = equal_inta} : int equal;
+
+fun less_eq_int k l = IntInf.<= (integer_of_int k, integer_of_int l);
+
+type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
+val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool;
+val less = #less : 'a ord -> 'a -> 'a -> bool;
+
+fun less_int k l = IntInf.< (integer_of_int k, integer_of_int l);
+
+val ord_int = {less_eq = less_eq_int, less = less_int} : int ord;
+
+type 'a preorder = {ord_preorder : 'a ord};
+val ord_preorder = #ord_preorder : 'a preorder -> 'a ord;
+
+type 'a order = {preorder_order : 'a preorder};
+val preorder_order = #preorder_order : 'a order -> 'a preorder;
+
+val preorder_int = {ord_preorder = ord_int} : int preorder;
+
+val order_int = {preorder_order = preorder_int} : int order;
+
+type 'a linorder = {order_linorder : 'a order};
+val order_linorder = #order_linorder : 'a linorder -> 'a order;
+
+val linorder_int = {order_linorder = order_int} : int linorder;
+
+fun eq A_ a b = equal A_ a b;
+
+fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2;
+
+fun equal_prod A_ B_ = {equal = equal_proda A_ B_} : ('a * 'b) equal;
+
+fun less_eq_prod A_ B_ (x1, y1) (x2, y2) =
+ less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less_eq B_ y1 y2;
+
+fun less_prod A_ B_ (x1, y1) (x2, y2) =
+ less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less B_ y1 y2;
+
+fun ord_prod A_ B_ = {less_eq = less_eq_prod A_ B_, less = less_prod A_ B_} :
+ ('a * 'b) ord;
+
+fun preorder_prod A_ B_ =
+ {ord_preorder = ord_prod (ord_preorder A_) (ord_preorder B_)} :
+ ('a * 'b) preorder;
+
+fun order_prod A_ B_ =
+ {preorder_order = preorder_prod (preorder_order A_) (preorder_order B_)} :
+ ('a * 'b) order;
+
+fun linorder_prod A_ B_ =
+ {order_linorder = order_prod (order_linorder A_) (order_linorder B_)} :
+ ('a * 'b) linorder;
+
+datatype nat = Zero_nat | Suc of nat;
+
+datatype color = R | B;
+
+datatype ('a, 'b) rbta = Empty |
+ Branch of color * ('a, 'b) rbta * 'a * 'b * ('a, 'b) rbta;
+
+datatype ('b, 'a) rbt = RBT of ('b, 'a) rbta;
+
+datatype 'a set = Set of 'a list | Coset of 'a list;
+
+datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm |
+ Neg of 'a fm;
+
+datatype trm = Const of string | App of trm * trm | Var of int;
+
+datatype prf_trm = PThm of string | Appt of prf_trm * trm |
+ AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm |
+ Conv of trm * prf_trm * prf_trm;
+
+datatype ('a, 'b) mapping = Mapping of ('a, 'b) rbt;
+
+datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int;
+
+fun id x = (fn xa => xa) x;
+
+fun impl_of B_ (RBT x) = x;
+
+fun folda f (Branch (c, lt, k, v, rt)) x = folda f rt (f k v (folda f lt x))
+ | folda f Empty x = x;
+
+fun fold A_ x xc = folda x (impl_of A_ xc);
+
+fun gen_keys kts (Branch (c, l, k, v, r)) = gen_keys ((k, r) :: kts) l
+ | gen_keys ((k, t) :: kts) Empty = k :: gen_keys kts t
+ | gen_keys [] Empty = [];
+
+fun keysb x = gen_keys [] x;
+
+fun keys A_ x = keysb (impl_of A_ x);
+
+fun maps f [] = []
+ | maps f (x :: xs) = f x @ maps f xs;
+
+fun empty A_ = RBT Empty;
+
+fun foldl f a [] = a
+ | foldl f a (x :: xs) = foldl f (f a x) xs;
+
+fun foldr f [] = id
+ | foldr f (x :: xs) = f x o foldr f xs;
+
+fun balance (Branch (R, a, w, x, b)) s t (Branch (R, c, y, z, d)) =
+ Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, d))
+ | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z Empty =
+ Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, Empty))
+ | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z
+ (Branch (B, va, vb, vc, vd)) =
+ Branch
+ (R, Branch (B, a, w, x, b), s, t,
+ Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+ | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z Empty =
+ Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty))
+ | balance
+ (Branch (R, Branch (B, va, vb, vc, vd), w, x, Branch (R, b, s, t, c))) y z
+ Empty =
+ Branch
+ (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+ Branch (B, c, y, z, Empty))
+ | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z
+ (Branch (B, va, vb, vc, vd)) =
+ Branch
+ (R, Branch (B, Empty, w, x, b), s, t,
+ Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+ | balance
+ (Branch (R, Branch (B, ve, vf, vg, vh), w, x, Branch (R, b, s, t, c))) y z
+ (Branch (B, va, vb, vc, vd)) =
+ Branch
+ (R, Branch (B, Branch (B, ve, vf, vg, vh), w, x, b), s, t,
+ Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+ | balance Empty w x (Branch (R, b, s, t, Branch (R, c, y, z, d))) =
+ Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, d))
+ | balance (Branch (B, va, vb, vc, vd)) w x
+ (Branch (R, b, s, t, Branch (R, c, y, z, d))) =
+ Branch
+ (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+ Branch (B, c, y, z, d))
+ | balance Empty w x (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) =
+ Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty))
+ | balance Empty w x
+ (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, va, vb, vc, vd))) =
+ Branch
+ (R, Branch (B, Empty, w, x, b), s, t,
+ Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+ | balance (Branch (B, va, vb, vc, vd)) w x
+ (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) =
+ Branch
+ (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+ Branch (B, c, y, z, Empty))
+ | balance (Branch (B, va, vb, vc, vd)) w x
+ (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, ve, vf, vg, vh))) =
+ Branch
+ (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+ Branch (B, c, y, z, Branch (B, ve, vf, vg, vh)))
+ | balance Empty s t Empty = Branch (B, Empty, s, t, Empty)
+ | balance Empty s t (Branch (B, va, vb, vc, vd)) =
+ Branch (B, Empty, s, t, Branch (B, va, vb, vc, vd))
+ | balance Empty s t (Branch (v, Empty, vb, vc, Empty)) =
+ Branch (B, Empty, s, t, Branch (v, Empty, vb, vc, Empty))
+ | balance Empty s t (Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty)) =
+ Branch
+ (B, Empty, s, t, Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty))
+ | balance Empty s t (Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi))) =
+ Branch
+ (B, Empty, s, t, Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi)))
+ | balance Empty s t
+ (Branch (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi)))
+ = Branch
+ (B, Empty, s, t,
+ Branch
+ (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi)))
+ | balance (Branch (B, va, vb, vc, vd)) s t Empty =
+ Branch (B, Branch (B, va, vb, vc, vd), s, t, Empty)
+ | balance (Branch (B, va, vb, vc, vd)) s t (Branch (B, ve, vf, vg, vh)) =
+ Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (B, ve, vf, vg, vh))
+ | balance (Branch (B, va, vb, vc, vd)) s t (Branch (v, Empty, vf, vg, Empty))
+ = Branch
+ (B, Branch (B, va, vb, vc, vd), s, t, Branch (v, Empty, vf, vg, Empty))
+ | balance (Branch (B, va, vb, vc, vd)) s t
+ (Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty)) =
+ Branch
+ (B, Branch (B, va, vb, vc, vd), s, t,
+ Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty))
+ | balance (Branch (B, va, vb, vc, vd)) s t
+ (Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm))) =
+ Branch
+ (B, Branch (B, va, vb, vc, vd), s, t,
+ Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm)))
+ | balance (Branch (B, va, vb, vc, vd)) s t
+ (Branch (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm)))
+ = Branch
+ (B, Branch (B, va, vb, vc, vd), s, t,
+ Branch
+ (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm)))
+ | balance (Branch (v, Empty, vb, vc, Empty)) s t Empty =
+ Branch (B, Branch (v, Empty, vb, vc, Empty), s, t, Empty)
+ | balance (Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh))) s t Empty =
+ Branch
+ (B, Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh)), s, t, Empty)
+ | balance (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty)) s t Empty =
+ Branch
+ (B, Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty), s, t, Empty)
+ | balance
+ (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)))
+ s t Empty =
+ Branch
+ (B, Branch
+ (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)),
+ s, t, Empty)
+ | balance (Branch (v, Empty, vf, vg, Empty)) s t (Branch (B, va, vb, vc, vd))
+ = Branch
+ (B, Branch (v, Empty, vf, vg, Empty), s, t, Branch (B, va, vb, vc, vd))
+ | balance (Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl))) s t
+ (Branch (B, va, vb, vc, vd)) =
+ Branch
+ (B, Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl)), s, t,
+ Branch (B, va, vb, vc, vd))
+ | balance (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty)) s t
+ (Branch (B, va, vb, vc, vd)) =
+ Branch
+ (B, Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty), s, t,
+ Branch (B, va, vb, vc, vd))
+ | balance
+ (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp)))
+ s t (Branch (B, va, vb, vc, vd)) =
+ Branch
+ (B, Branch
+ (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp)),
+ s, t, Branch (B, va, vb, vc, vd));
+
+fun rbt_ins A_ f k v Empty = Branch (R, Empty, k, v, Empty)
+ | rbt_ins A_ f k v (Branch (B, l, x, y, r)) =
+ (if less A_ k x then balance (rbt_ins A_ f k v l) x y r
+ else (if less A_ x k then balance l x y (rbt_ins A_ f k v r)
+ else Branch (B, l, x, f k y v, r)))
+ | rbt_ins A_ f k v (Branch (R, l, x, y, r)) =
+ (if less A_ k x then Branch (R, rbt_ins A_ f k v l, x, y, r)
+ else (if less A_ x k then Branch (R, l, x, y, rbt_ins A_ f k v r)
+ else Branch (R, l, x, f k y v, r)));
+
+fun paint c Empty = Empty
+ | paint c (Branch (uu, l, k, v, r)) = Branch (c, l, k, v, r);
+
+fun rbt_insert_with_key A_ f k v t = paint B (rbt_ins A_ f k v t);
+
+fun rbt_insert A_ = rbt_insert_with_key A_ (fn _ => fn _ => fn nv => nv);
+
+fun insert A_ xc xd xe =
+ RBT (rbt_insert ((ord_preorder o preorder_order o order_linorder) A_) xc xd
+ (impl_of A_ xe));
+
+fun rbt_lookup A_ Empty k = NONE
+ | rbt_lookup A_ (Branch (uu, l, x, y, r)) k =
+ (if less A_ k x then rbt_lookup A_ l k
+ else (if less A_ x k then rbt_lookup A_ r k else SOME y));
+
+fun lookup A_ x =
+ rbt_lookup ((ord_preorder o preorder_order o order_linorder) A_)
+ (impl_of A_ x);
+
+fun member A_ [] y = false
+ | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y;
+
+fun hd (x21 :: x22) = x21;
+
+fun tl [] = []
+ | tl (x21 :: x22) = x22;
+
+fun remdups A_ [] = []
+ | remdups A_ (x :: xs) =
+ (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs);
+
+fun dnf_and_fm (Or (phi_1, phi_2)) psi =
+ Or (dnf_and_fm phi_1 psi, dnf_and_fm phi_2 psi)
+ | dnf_and_fm (Atom v) (Or (phi_1, phi_2)) =
+ Or (dnf_and_fm (Atom v) phi_1, dnf_and_fm (Atom v) phi_2)
+ | dnf_and_fm (And (v, va)) (Or (phi_1, phi_2)) =
+ Or (dnf_and_fm (And (v, va)) phi_1, dnf_and_fm (And (v, va)) phi_2)
+ | dnf_and_fm (Neg v) (Or (phi_1, phi_2)) =
+ Or (dnf_and_fm (Neg v) phi_1, dnf_and_fm (Neg v) phi_2)
+ | dnf_and_fm (Atom v) (Atom va) = And (Atom v, Atom va)
+ | dnf_and_fm (Atom v) (And (va, vb)) = And (Atom v, And (va, vb))
+ | dnf_and_fm (Atom v) (Neg va) = And (Atom v, Neg va)
+ | dnf_and_fm (And (v, va)) (Atom vb) = And (And (v, va), Atom vb)
+ | dnf_and_fm (And (v, va)) (And (vb, vc)) = And (And (v, va), And (vb, vc))
+ | dnf_and_fm (And (v, va)) (Neg vb) = And (And (v, va), Neg vb)
+ | dnf_and_fm (Neg v) (Atom va) = And (Neg v, Atom va)
+ | dnf_and_fm (Neg v) (And (va, vb)) = And (Neg v, And (va, vb))
+ | dnf_and_fm (Neg v) (Neg va) = And (Neg v, Neg va);
+
+fun dnf_fm (And (phi_1, phi_2)) = dnf_and_fm (dnf_fm phi_1) (dnf_fm phi_2)
+ | dnf_fm (Or (phi_1, phi_2)) = Or (dnf_fm phi_1, dnf_fm phi_2)
+ | dnf_fm (Atom v) = Atom v
+ | dnf_fm (Neg v) = Neg v;
+
+fun keysa A_ (Mapping t) = Set (keys A_ t);
+
+fun amap_fm h (Atom a) = h a
+ | amap_fm h (And (phi_1, phi_2)) = And (amap_fm h phi_1, amap_fm h phi_2)
+ | amap_fm h (Or (phi_1, phi_2)) = Or (amap_fm h phi_1, amap_fm h phi_2)
+ | amap_fm h (Neg phi) = Neg (amap_fm h phi);
+
+fun emptya A_ = Mapping (empty A_);
+
+fun lookupa A_ (Mapping t) = lookup A_ t;
+
+fun update A_ k v (Mapping t) = Mapping (insert A_ k v t);
+
+fun gen_length n (x :: xs) = gen_length (Suc n) xs
+ | gen_length n [] = n;
+
+fun size_list x = gen_length Zero_nat x;
+
+fun card A_ (Set xs) = size_list (remdups A_ xs);
+
+fun conj_list (And (phi_1, phi_2)) = conj_list phi_1 @ conj_list phi_2
+ | conj_list (Atom a) = [a];
+
+fun trm_of_fm f (Atom a) = f a
+ | trm_of_fm f (And (phi_1, phi_2)) =
+ App (App (Const "conj", trm_of_fm f phi_1), trm_of_fm f phi_2)
+ | trm_of_fm f (Or (phi_1, phi_2)) =
+ App (App (Const "disj", trm_of_fm f phi_1), trm_of_fm f phi_2)
+ | trm_of_fm f (Neg phi) = App (Const "Not", trm_of_fm f phi);
+
+fun dnf_and_fm_prf (Or (phi_1, phi_2)) psi =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+ [PThm "conj_disj_distribR_conv",
+ foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv",
+ hd [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi]),
+ hd (tl [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi])]]
+ | dnf_and_fm_prf (Atom v) (Or (phi_1, phi_2)) =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+ [PThm "conj_disj_distribL_conv",
+ foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv",
+ hd [dnf_and_fm_prf (Atom v) phi_1,
+ dnf_and_fm_prf (Atom v) phi_2]),
+ hd (tl [dnf_and_fm_prf (Atom v) phi_1,
+ dnf_and_fm_prf (Atom v) phi_2])]]
+ | dnf_and_fm_prf (And (v, va)) (Or (phi_1, phi_2)) =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+ [PThm "conj_disj_distribL_conv",
+ foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv",
+ hd [dnf_and_fm_prf (And (v, va)) phi_1,
+ dnf_and_fm_prf (And (v, va)) phi_2]),
+ hd (tl [dnf_and_fm_prf (And (v, va)) phi_1,
+ dnf_and_fm_prf (And (v, va)) phi_2])]]
+ | dnf_and_fm_prf (Neg v) (Or (phi_1, phi_2)) =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+ [PThm "conj_disj_distribL_conv",
+ foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv",
+ hd [dnf_and_fm_prf (Neg v) phi_1,
+ dnf_and_fm_prf (Neg v) phi_2]),
+ hd (tl [dnf_and_fm_prf (Neg v) phi_1,
+ dnf_and_fm_prf (Neg v) phi_2])]]
+ | dnf_and_fm_prf (Atom v) (Atom va) = PThm "all_conv"
+ | dnf_and_fm_prf (Atom v) (And (va, vb)) = PThm "all_conv"
+ | dnf_and_fm_prf (Atom v) (Neg va) = PThm "all_conv"
+ | dnf_and_fm_prf (And (v, va)) (Atom vb) = PThm "all_conv"
+ | dnf_and_fm_prf (And (v, va)) (And (vb, vc)) = PThm "all_conv"
+ | dnf_and_fm_prf (And (v, va)) (Neg vb) = PThm "all_conv"
+ | dnf_and_fm_prf (Neg v) (Atom va) = PThm "all_conv"
+ | dnf_and_fm_prf (Neg v) (And (va, vb)) = PThm "all_conv"
+ | dnf_and_fm_prf (Neg v) (Neg va) = PThm "all_conv";
+
+fun dnf_fm_prf (And (phi_1, phi_2)) =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+ [foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]),
+ hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])],
+ dnf_and_fm_prf (dnf_fm phi_1) (dnf_fm phi_2)]
+ | dnf_fm_prf (Or (phi_1, phi_2)) =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]),
+ hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])]
+ | dnf_fm_prf (Atom v) = PThm "all_conv"
+ | dnf_fm_prf (Neg v) = PThm "all_conv";
+
+fun of_alist A_ xs = foldr (fn (a, b) => update A_ a b) xs (emptya A_);
+
+fun deneg (true, LESS (x, y)) =
+ And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y)))
+ | deneg (false, LESS (x, y)) = Atom (true, LEQ (y, x))
+ | deneg (false, LEQ (x, y)) =
+ And (Atom (true, LEQ (y, x)), Atom (false, EQ (y, x)))
+ | deneg (false, EQ (v, vb)) = Atom (false, EQ (v, vb))
+ | deneg (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc))
+ | deneg (true, LEQ (vb, vc)) = Atom (true, LEQ (vb, vc));
+
+fun from_conj_prf trm_of_atom p (And (a, b)) =
+ foldl (fn aa => fn ba => AppP (aa, ba)) (PThm "conjE")
+ [Bound (trm_of_fm trm_of_atom (And (a, b))),
+ AbsP (trm_of_fm trm_of_atom a,
+ AbsP (trm_of_fm trm_of_atom b,
+ from_conj_prf trm_of_atom (from_conj_prf trm_of_atom p b)
+ a))]
+ | from_conj_prf trm_of_atom p (Atom a) = p;
+
+fun contr_fm_prf trm_of_atom contr_atom_prf (Or (c, d)) =
+ (case (contr_fm_prf trm_of_atom contr_atom_prf c,
+ contr_fm_prf trm_of_atom contr_atom_prf d)
+ of (NONE, _) => NONE | (SOME _, NONE) => NONE
+ | (SOME p1, SOME p2) =>
+ SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "disjE")
+ [Bound (trm_of_fm trm_of_atom (Or (c, d))),
+ AbsP (trm_of_fm trm_of_atom c, p1),
+ AbsP (trm_of_fm trm_of_atom d, p2)]))
+ | contr_fm_prf trm_of_atom contr_atom_prf (And (a, b)) =
+ (case contr_atom_prf (conj_list (And (a, b))) of NONE => NONE
+ | SOME p => SOME (from_conj_prf trm_of_atom p (And (a, b))))
+ | contr_fm_prf trm_of_atom contr_atom_prf (Atom a) = contr_atom_prf [a];
+
+fun deless (true, LESS (x, y)) =
+ And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y)))
+ | deless (false, LESS (x, y)) =
+ Or (Atom (false, LEQ (x, y)), Atom (true, EQ (x, y)))
+ | deless (false, EQ (v, vb)) = Atom (false, EQ (v, vb))
+ | deless (false, LEQ (v, vb)) = Atom (false, LEQ (v, vb))
+ | deless (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc))
+ | deless (v, LEQ (vb, vc)) = Atom (v, LEQ (vb, vc));
+
+fun deneg_prf (true, LESS (x, y)) = PThm "less_le"
+ | deneg_prf (false, LESS (x, y)) = PThm "nless_le"
+ | deneg_prf (false, LEQ (x, y)) = PThm "nle_le"
+ | deneg_prf (false, EQ (v, vb)) = PThm "all_conv"
+ | deneg_prf (v, EQ (vb, vc)) = PThm "all_conv"
+ | deneg_prf (true, LEQ (vb, vc)) = PThm "all_conv";
+
+val one_nat : nat = Suc Zero_nat;
+
+fun map_option f NONE = NONE
+ | map_option f (SOME x2) = SOME (f x2);
+
+fun deless_prf (true, LESS (x, y)) = PThm "less_le"
+ | deless_prf (false, LESS (x, y)) = PThm "nless_le"
+ | deless_prf (false, EQ (v, vb)) = PThm "all_conv"
+ | deless_prf (false, LEQ (v, vb)) = PThm "all_conv"
+ | deless_prf (v, EQ (vb, vc)) = PThm "all_conv"
+ | deless_prf (v, LEQ (vb, vc)) = PThm "all_conv";
+
+fun trm_of_oatom (EQ (x, y)) = App (App (Const "eq", Var x), Var y)
+ | trm_of_oatom (LEQ (x, y)) = App (App (Const "le", Var x), Var y)
+ | trm_of_oatom (LESS (x, y)) = App (App (Const "lt", Var x), Var y);
+
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
+ | minus_nat Zero_nat n = Zero_nat
+ | minus_nat m Zero_nat = m;
+
+fun mapping_fold A_ f (Mapping t) a = fold A_ f t a;
+
+fun relcomp1_mapping A_ (B1_, B2_) x y1 pxy pm pma =
+ mapping_fold (linorder_prod B2_ B2_)
+ (fn (y2, z) => fn pyz => fn pmb =>
+ (if eq B1_ y1 y2 andalso not (eq B1_ y2 z)
+ then update (linorder_prod A_ B2_) (x, z)
+ (foldl (fn a => fn b => AppP (a, b)) (PThm "trans") [pxy, pyz])
+ pmb
+ else pmb))
+ pm pma;
+
+fun relcomp_mapping (A1_, A2_) pm1 pm2 pma =
+ mapping_fold (linorder_prod A2_ A2_)
+ (fn (x, y) => fn pxy => fn pm =>
+ (if eq A1_ x y then pm
+ else relcomp1_mapping A2_ (A1_, A2_) x y pxy pm2 pm))
+ pm1 pma;
+
+fun ntrancl_mapping (A1_, A2_) Zero_nat m = m
+ | ntrancl_mapping (A1_, A2_) (Suc k) m =
+ let
+ val trclm = ntrancl_mapping (A1_, A2_) k m;
+ in
+ relcomp_mapping (A1_, A2_) trclm m trclm
+ end;
+
+fun trancl_mapping (A1_, A2_) m =
+ ntrancl_mapping (A1_, A2_)
+ (minus_nat (card (equal_prod A1_ A1_) (keysa (linorder_prod A2_ A2_) m))
+ one_nat)
+ m;
+
+fun is_in_leq leqm l =
+ let
+ val (x, y) = l;
+ in
+ (if equal_inta x y then SOME (Appt (PThm "refl", Var x))
+ else lookupa (linorder_prod linorder_int linorder_int) leqm l)
+ end;
+
+fun is_in_eq leqm l =
+ let
+ val (x, y) = l;
+ in
+ (case (is_in_leq leqm (x, y), is_in_leq leqm (y, x)) of (NONE, _) => NONE
+ | (SOME _, NONE) => NONE
+ | (SOME p1, SOME p2) =>
+ SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "antisym") [p1, p2]))
+ end;
+
+fun trm_of_oliteral (true, a) = trm_of_oatom a
+ | trm_of_oliteral (false, a) = App (Const "Not", trm_of_oatom a);
+
+fun contr1_list leqm (false, LEQ (x, y)) =
+ map_option
+ (fn a =>
+ AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, LEQ (x, y)))),
+ a))
+ (is_in_leq leqm (x, y))
+ | contr1_list leqm (false, EQ (x, y)) =
+ map_option
+ (fn a =>
+ AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, EQ (x, y)))),
+ a))
+ (is_in_eq leqm (x, y))
+ | contr1_list uu (true, va) = NONE
+ | contr1_list uu (v, LESS (vb, vc)) = NONE;
+
+fun contr_list_aux leqm [] = NONE
+ | contr_list_aux leqm (l :: ls) =
+ (case contr1_list leqm l of NONE => contr_list_aux leqm ls
+ | SOME a => SOME a);
+
+fun leq1_member_list (true, LEQ (x, y)) =
+ [((x, y), Bound (trm_of_oliteral (true, LEQ (x, y))))]
+ | leq1_member_list (true, EQ (x, y)) =
+ [((x, y), AppP (PThm "eqD1", Bound (trm_of_oliteral (true, EQ (x, y))))),
+ ((y, x), AppP (PThm "eqD2", Bound (trm_of_oliteral (true, EQ (x, y)))))]
+ | leq1_member_list (false, va) = []
+ | leq1_member_list (v, LESS (vb, vc)) = [];
+
+fun leq1_list a = maps leq1_member_list a;
+
+fun leq1_mapping a =
+ of_alist (linorder_prod linorder_int linorder_int) (leq1_list a);
+
+fun contr_list a =
+ contr_list_aux (trancl_mapping (equal_int, linorder_int) (leq1_mapping a)) a;
+
+fun contr_prf atom_conv phi =
+ contr_fm_prf trm_of_oliteral contr_list (dnf_fm (amap_fm atom_conv phi));
+
+fun amap_f_m_prf ap (Atom a) = AppP (PThm "atom_conv", ap a)
+ | amap_f_m_prf ap (And (phi_1, phi_2)) =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv",
+ hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]),
+ hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])]
+ | amap_f_m_prf ap (Or (phi_1, phi_2)) =
+ foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+ [AppP (PThm "arg_conv",
+ hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]),
+ hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])]
+ | amap_f_m_prf ap (Neg phi) = AppP (PThm "arg_conv", amap_f_m_prf ap phi);
+
+fun lo_contr_prf phi =
+ map_option
+ ((fn a =>
+ Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deneg_prf phi, a)) o
+ (fn a =>
+ Conv (trm_of_fm trm_of_oliteral (amap_fm deneg phi),
+ dnf_fm_prf (amap_fm deneg phi), a)))
+ (contr_prf deneg phi);
+
+fun po_contr_prf phi =
+ map_option
+ ((fn a =>
+ Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deless_prf phi, a)) o
+ (fn a =>
+ Conv (trm_of_fm trm_of_oliteral (amap_fm deless phi),
+ dnf_fm_prf (amap_fm deless phi), a)))
+ (contr_prf deless phi);
+
+end; (*struct Order_Procedure*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/order_tac.ML Wed Mar 31 18:18:03 2021 +0200
@@ -0,0 +1,456 @@
+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 * int Termtab.table * term Inttab.table)
+
+ val empty = (0, Termtab.empty, Inttab.empty)
+
+ fun get_var t (tab as (max_var, termtab, inttab)) =
+ (case Termtab.lookup termtab t of
+ SOME v => (v, tab)
+ | NONE => (max_var,
+ (max_var + 1, Termtab.update (t, max_var) termtab, Inttab.update (max_var, t) inttab))
+ )
+
+ fun get_term v (_, _, inttab) = Inttab.lookup inttab v
+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.o_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 matches_skeleton t s = t = Term.dummy orelse
+ (case (t, s) of
+ (t0 $ t1, s0 $ s1) => matches_skeleton t0 s0 andalso matches_skeleton t1 s1
+ | _ => t aconv s)
+
+ fun dest_binop t =
+ let
+ val binop_skel = Term.dummy $ Term.dummy $ Term.dummy
+ val not_binop_skel = Logic_Sig.Not $ binop_skel
+ in
+ if matches_skeleton not_binop_skel t
+ then (case t of (_ $ (t1 $ t2 $ t3)) => (false, (t1, t2, t3)))
+ else if matches_skeleton binop_skel t
+ then (case t of (t1 $ t2 $ t3) => (true, (t1, t2, t3)))
+ else raise TERM ("Not a binop literal", [t])
+ end
+
+ fun find_term t = Library.find_first (fn (t', _) => t' aconv t)
+
+ fun reify_order_atom (eq, le, lt) t reifytab =
+ let
+ val (b, (t0, t1, t2)) =
+ (dest_binop t) handle TERM (_, _) => raise TERM ("Can't reify order literal", [t])
+ val binops = [(eq, EQ), (le, LEQ), (lt, LESS)]
+ in
+ case find_term t0 binops of
+ SOME (_, reified_bop) =>
+ reifytab
+ |> Reifytab.get_var t1 ||> Reifytab.get_var t2
+ |> (fn (v1, (v2, vartab')) =>
+ ((b, reified_bop (Int_of_integer v1, Int_of_integer v2)), vartab'))
+ |>> Atom
+ | NONE => raise TERM ("Can't reify order literal", [t])
+ end
+
+ fun reify consts reify_atom t reifytab =
+ let
+ fun reify' (t1 $ t2) reifytab =
+ let
+ val (t0, ts) = strip_comb (t1 $ t2)
+ val consts_of_arity = filter (fn (_, (_, ar)) => length ts = ar) consts
+ in
+ (case find_term t0 consts_of_arity of
+ SOME (_, (reified_op, _)) => fold_map reify' ts reifytab |>> reified_op
+ | NONE => reify_atom (t1 $ t2) reifytab)
+ end
+ | reify' t reifytab = reify_atom t reifytab
+ in
+ reify' t reifytab
+ 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 reify_order_conj ord_ops =
+ let
+ val consts = map (apsnd (list_curry2 o curry)) [(Logic_Sig.conj, And), (Logic_Sig.disj, Or)]
+ in
+ reify consts (reify_order_atom ord_ops)
+ 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 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 is_binop_term t =
+ let
+ fun is_included t = forall (curry (op <>) (t |> fastype_of |> domain_type)) excluded_types
+ in
+ (case dest_binop (Logic_Sig.dest_Trueprop t) of
+ (_, (binop, t1, t2)) =>
+ is_included binop andalso
+ (* Exclude terms with schematic variables since the solver can't deal with them.
+ More specifically, the solver uses Assumption.assume which does not allow schematic
+ variables in the assumed cterm.
+ *)
+ Term.add_var_names (binop $ t1 $ t2) [] = []
+ ) handle TERM (_, _) => false
+ end
+
+ fun partition_matches ctxt term_of pats ys =
+ let
+ val thy = Proof_Context.theory_of ctxt
+
+ fun find_match t env =
+ Library.get_first (try (fn pat => Pattern.match thy (pat, t) env)) pats
+
+ fun filter_matches xs = fold (fn x => fn (mxs, nmxs, env) =>
+ case find_match (term_of x) env of
+ SOME env' => (x::mxs, nmxs, env')
+ | NONE => (mxs, x::nmxs, env)) xs ([], [], (Vartab.empty, Vartab.empty))
+
+ fun partition xs =
+ case filter_matches xs of
+ ([], _, _) => []
+ | (mxs, nmxs, env) => (env, mxs) :: partition nmxs
+ in
+ partition ys
+ end
+
+ fun limit_not_less [_, _, lt] ctxt 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 dest_binop (Logic_Sig.dest_Trueprop t) of
+ (false, (t0, _, _)) => Pattern.matches thy (lt, t0)
+ | _ => false)
+ handle TERM _ => false
+
+ val not_less_prems = filter (is_not_less_term o Thm.prop_of) 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) prems @
+ take limit not_less_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 binop_prems = filter (is_binop_term o Thm.prop_of) (prems @ simp_prems)
+ val strip_binop = (fn (x, _, _) => x) o snd o dest_binop
+ val binop_of = strip_binop o Logic_Sig.dest_Trueprop o Thm.prop_of
+
+ (* Due to local_setup, the operators of the order may contain schematic term and type
+ variables. We partition the premises according to distinct instances of those operators.
+ *)
+ val part_prems = partition_matches ctxt binop_of (#ops octxt) binop_prems
+ |> (case #kind octxt of
+ Order => map (fn (env, prems) =>
+ (env, limit_not_less (#ops octxt) ctxt prems))
+ | _ => I)
+
+ fun order_tac' (_, []) = no_tac
+ | order_tac' (env, prems) =
+ let
+ val [eq, le, lt] = #ops octxt
+ val subst_contract = Envir.eta_contract o Envir.subst_term env
+ val ord_ops = (subst_contract eq,
+ subst_contract le,
+ subst_contract lt)
+
+ val _ = if trace then @{print} (ord_ops, prems) else (ord_ops, prems)
+
+ val prems_conj_thm = foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) prems
+ |> Conv.fconv_rule Thm.eta_conversion
+ val prems_conj = prems_conj_thm |> Thm.prop_of
+ val (reified_prems_conj, reifytab) =
+ reify_order_conj ord_ops (Logic_Sig.dest_Trueprop prems_conj) Reifytab.empty
+
+ val proof = raw_order_proc reified_prems_conj
+
+ val assmtab = Termtab.make [(prems_conj, prems_conj_thm)]
+ val replay = replay_order_prf_trm ord_ops octxt ctxt reifytab assmtab
+ in
+ case proof of
+ NONE => no_tac
+ | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1
+ end
+ in
+ FIRST (map order_tac' part_prems)
+ 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
+ | SOME _ => resolve0_tac [Logic_Sig.ccontr] i
+ | NONE => resolve0_tac [Logic_Sig.ccontr] i)
+
+ 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
+
+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 = []
+ val extend = I
+ 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