# HG changeset patch # User ballarin # Date 1077202654 -3600 # Node ID c5c47703f763b1bc8f0041ba9c5067833dd52eea # Parent b3b15305a1c9649aaefc62f0c7391d4198547697 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier. diff -r b3b15305a1c9 -r c5c47703f763 NEWS --- a/NEWS Thu Feb 19 10:41:32 2004 +0100 +++ b/NEWS Thu Feb 19 15:57:34 2004 +0100 @@ -6,6 +6,9 @@ *** General *** +* Provers/order.ML: new efficient reasoner for partial and linear orders. + Replaces linorder.ML. + * Pure: Greek letters (except small lambda, \), as well as gothic (\...\\...\), caligraphic (\...\), and euler (\...\), are now considered normal letters, and can therefore @@ -77,6 +80,16 @@ *** HOL *** +* Simplifier: + - Much improved handling of linear and partial orders. + Reasoners for linear and partial orders are set up for type classes + "linorder" and "order" respectively, and are added to the default simpset + as solvers. This means that the simplifier can build transitivity chains + to solve goals from the assumptions. + - INCOMPATIBILITY: old proofs break occasionally. Typically, applications + of blast or auto after simplification become unnecessary because the goal + is solved by simplification already. + * Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, all proved in axiomatic type classes for semirings, rings and fields. diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Bali/DefiniteAssignmentCorrect.thy --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Feb 19 15:57:34 2004 +0100 @@ -3429,7 +3429,7 @@ by (cases s2) (simp add: abrupt_if_def) with brkAss_C1 s1_s2 s2_s3 show ?thesis - by simp (blast intro: subset_trans) + by simp qed moreover from True nrmAss_C2 s2_s3 have "nrm C2 \ dom (locals (store s3))" diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/HOL.thy Thu Feb 19 15:57:34 2004 +0100 @@ -946,6 +946,93 @@ by (simp add: max_def) +subsubsection {* Transitivity rules for calculational reasoning *} + + +lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b" + by (simp add: order_less_le) + +lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b" + by (simp add: order_less_le) + +lemma order_less_asym': "(a::'a::order) b < a ==> P" + by (rule order_less_asym) + + +subsubsection {* Setup of transitivity reasoner *} + +lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y" + by (erule contrapos_pn, erule subst, rule order_less_irrefl) + +lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y" + by (erule subst, erule ssubst, assumption) + +ML_setup {* + +structure Trans_Tac = Trans_Tac_Fun ( + struct + val less_reflE = thm "order_less_irrefl" RS thm "notE"; + val le_refl = thm "order_refl"; + val less_imp_le = thm "order_less_imp_le"; + val not_lessI = thm "linorder_not_less" RS thm "iffD2"; + val not_leI = thm "linorder_not_le" RS thm "iffD2"; + val not_lessD = thm "linorder_not_less" RS thm "iffD1"; + val not_leD = thm "linorder_not_le" RS thm "iffD1"; + val eqI = thm "order_antisym"; + val eqD1 = thm "order_eq_refl"; + val eqD2 = thm "sym" RS thm "order_eq_refl"; + val less_trans = thm "order_less_trans"; + val less_le_trans = thm "order_less_le_trans"; + val le_less_trans = thm "order_le_less_trans"; + val le_trans = thm "order_trans"; + val le_neq_trans = thm "order_le_neq_trans"; + val neq_le_trans = thm "order_neq_le_trans"; + val less_imp_neq = thm "less_imp_neq"; + val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; + + fun decomp_gen sort sign (Trueprop $ t) = + let fun of_sort t = Sign.of_sort sign (type_of t, sort) + fun dec (Const ("Not", _) $ t) = ( + case dec t of + None => None + | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2)) + | dec (Const ("op =", _) $ t1 $ t2) = + if of_sort t1 + then Some (t1, "=", t2) + else None + | dec (Const ("op <=", _) $ t1 $ t2) = + if of_sort t1 + then Some (t1, "<=", t2) + else None + | dec (Const ("op <", _) $ t1 $ t2) = + if of_sort t1 + then Some (t1, "<", t2) + else None + | dec _ = None + in dec t end; + + val decomp_part = decomp_gen ["HOL.order"]; + val decomp_lin = decomp_gen ["HOL.linorder"]; + + end); (* struct *) + +Context.>> (fn thy => (simpset_ref_of thy := + simpset_of thy + addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac)) + addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac)); + thy)) +*} + +(* Optional methods + +method_setup trans_partial = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_partial)) *} + {* simple transitivity reasoner *} +method_setup trans_linear = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_linear)) *} + {* simple transitivity reasoner *} +*) + subsubsection "Bounded quantifiers" syntax diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/HoareParallel/Gar_Coll.thy --- a/src/HOL/HoareParallel/Gar_Coll.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/HoareParallel/Gar_Coll.thy Thu Feb 19 15:57:34 2004 +0100 @@ -496,7 +496,6 @@ apply (erule disjE) apply(simp add:psubsetI) apply(force dest:subset_antisym) -apply force done subsection {* Interference Freedom *} diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/HoareParallel/OG_Hoare.thy --- a/src/HOL/HoareParallel/OG_Hoare.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/HoareParallel/OG_Hoare.thy Thu Feb 19 15:57:34 2004 +0100 @@ -237,7 +237,6 @@ apply simp apply(rule AnnWhile) apply simp_all - apply(fast) --{* Await *} apply(frule ann_hoare_case_analysis,simp) apply clarify diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Integ/IntDef.thy Thu Feb 19 15:57:34 2004 +0100 @@ -521,7 +521,6 @@ apply (simp add: order_le_less) apply (case_tac "w < 0") apply (simp add: order_less_imp_le) - apply (blast intro: order_less_trans) apply (simp add: linorder_not_less) done diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/IsaMakefile Thu Feb 19 15:57:34 2004 +0100 @@ -75,10 +75,10 @@ $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \ - $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \ - $(SRC)/Provers/splitter.ML $(SRC)/Provers/linorder.ML \ - $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \ - $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ + $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \ + $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ + $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ + $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \ Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ @@ -87,7 +87,8 @@ HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \ Integ/cooper_dec.ML Integ/cooper_proof.ML \ Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \ - Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \ + Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy \ + Integ/int_arith1.ML \ Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \ Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \ Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \ diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/ROOT.ML Thu Feb 19 15:57:34 2004 +0100 @@ -34,7 +34,7 @@ use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; use "~~/src/Provers/Arith/extract_common_term.ML"; use "~~/src/Provers/Arith/cancel_div_mod.ML"; -use "~~/src/Provers/linorder.ML"; +use "~~/src/Provers/order.ML"; with_path "Integ" use_thy "Main"; diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Real/RealDef.thy Thu Feb 19 15:57:34 2004 +0100 @@ -467,7 +467,6 @@ apply (rule eq_Abs_REAL [of z]) apply (rule eq_Abs_REAL [of w]) apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels) -apply (cut_tac x="x+ya" and y="xa+y" in linorder_linear, auto) done diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Ring_and_Field.thy Thu Feb 19 15:57:34 2004 +0100 @@ -1526,6 +1526,7 @@ by (simp add: abs_if linorder_neq_iff) lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)" +apply (simp add: abs_if) by (simp add: abs_if order_less_not_sym [of a 0]) lemma abs_le_zero_iff [simp]: "(abs a \ (0::'a::ordered_ring)) = (a = 0)" @@ -1620,11 +1621,17 @@ lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" apply (simp add: order_less_le abs_le_iff) +apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) +apply (simp add: le_minus_self_iff linorder_neq_iff) +done +(* +apply (simp add: order_less_le abs_le_iff) apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) - apply (simp add: linorder_not_less [symmetric]) + apply (simp add: linorder_not_less [symmetric]) apply (simp add: le_minus_self_iff linorder_neq_iff) apply (simp add: linorder_not_less [symmetric]) done +*) lemma abs_triangle_ineq: "abs (a+b) \ abs a + abs (b::'a::ordered_ring)" by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono) diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Set.thy Thu Feb 19 15:57:34 2004 +0100 @@ -1963,15 +1963,6 @@ lemma set_mp: "A \ B ==> x:A ==> x:B" by (rule subsetD) -lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b" - by (simp add: order_less_le) - -lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b" - by (simp add: order_less_le) - -lemma order_less_asym': "(a::'a::order) b < a ==> P" - by (rule order_less_asym) - lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" by (rule subst) diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/SetInterval.thy Thu Feb 19 15:57:34 2004 +0100 @@ -33,48 +33,6 @@ atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") "{l..u} == {l..} Int {..u}" - -subsection {* Setup of transitivity reasoner *} - -ML {* - -structure Trans_Tac = Trans_Tac_Fun ( - struct - val less_reflE = thm "order_less_irrefl" RS thm "notE"; - val le_refl = thm "order_refl"; - val less_imp_le = thm "order_less_imp_le"; - val not_lessI = thm "linorder_not_less" RS thm "iffD2"; - val not_leI = thm "linorder_not_less" RS thm "iffD2"; - val not_lessD = thm "linorder_not_less" RS thm "iffD1"; - val not_leD = thm "linorder_not_le" RS thm "iffD1"; - val eqI = thm "order_antisym"; - val eqD1 = thm "order_eq_refl"; - val eqD2 = thm "sym" RS thm "order_eq_refl"; - val less_trans = thm "order_less_trans"; - val less_le_trans = thm "order_less_le_trans"; - val le_less_trans = thm "order_le_less_trans"; - val le_trans = thm "order_trans"; - fun decomp (Trueprop $ t) = - let fun dec (Const ("Not", _) $ t) = ( - case dec t of - None => None - | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2)) - | dec (Const (rel, _) $ t1 $ t2) = - Some (t1, implode (drop (3, explode rel)), t2) - | dec _ = None - in dec t end - | decomp _ = None - end); - -val trans_tac = Trans_Tac.trans_tac; - -*} - -method_setup trans = - {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *} - {* simple transitivity reasoner *} - - subsection {*lessThan*} lemma lessThan_iff [iff]: "(i: lessThan k) = (i greaterThan y) = (y \ (x::'a::linorder))" apply (auto simp add: greaterThan_def) apply (subst linorder_not_less [symmetric], blast) -apply (blast intro: order_le_less_trans) done lemma greaterThan_eq_iff [iff]: @@ -209,7 +160,6 @@ "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" apply (auto simp add: lessThan_def) apply (subst linorder_not_less [symmetric], blast) -apply (blast intro: order_less_le_trans) done lemma lessThan_eq_iff [iff]: @@ -270,7 +220,7 @@ "(l::'a::linorder) {)l..u(} Un {u} = {)l..u}" "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}" "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}" -by auto (elim linorder_neqE | trans+)+ +by auto (* One- and two-sided intervals *) @@ -283,7 +233,7 @@ "(l::'a::linorder) {)l..u(} Un {u..} = {)l..}" "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}" "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}" -by auto trans+ +by auto (* Two- and two-sided intervals *) @@ -296,7 +246,7 @@ "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}" "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}" "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}" -by auto trans+ +by auto lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two @@ -324,7 +274,7 @@ "{)l..u(} Int {u..} = {}" "{l..u} Int {)u..} = {}" "{l..u(} Int {u..} = {}" - by auto trans+ + by auto (* Two- and two-sided intervals *) @@ -337,7 +287,7 @@ "{)l..m} Int {)m..u} = {}" "{l..m(} Int {m..u} = {}" "{l..m} Int {)m..u} = {}" - by auto trans+ + by auto lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Transitive_Closure.thy Thu Feb 19 15:57:34 2004 +0100 @@ -129,7 +129,7 @@ lemma rtrancl_subset: "R \ S ==> S \ R^* ==> S^* = R^*" apply (drule rtrancl_mono) - apply (drule rtrancl_mono, simp, blast) + apply (drule rtrancl_mono, simp) done lemma rtrancl_Un_rtrancl: "(R^* \ S^*)^* = (R \ S)^*" diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Wellfounded_Recursion.ML --- a/src/HOL/Wellfounded_Recursion.ML Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Wellfounded_Recursion.ML Thu Feb 19 15:57:34 2004 +0100 @@ -322,7 +322,6 @@ by (res_inst_tac [("s","x")] (Least_equality RS ssubst) 1); by Auto_tac; by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym])); -by (blast_tac (claset() addIs [order_less_trans]) 1); bind_thm("wellorder_LeastI", result() RS mp RS conjunct1); bind_thm("wellorder_Least_le", result() RS mp RS conjunct2); diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/ex/BinEx.thy --- a/src/HOL/ex/BinEx.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/ex/BinEx.thy Thu Feb 19 15:57:34 2004 +0100 @@ -471,7 +471,6 @@ apply (simp add: normal_Pls_eq_0) apply (simp only: number_of_minus zminus_0 iszero_def minus_equation_iff [of _ "0"]) - apply (simp add: eq_commute) done (*The previous command should have finished the proof but the lin-arith diff -r b3b15305a1c9 -r c5c47703f763 src/Provers/linorder.ML --- a/src/Provers/linorder.ML Thu Feb 19 10:41:32 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,214 +0,0 @@ -(* - Title: Transitivity reasoner for linear orders - Id: $Id$ - Author: Clemens Ballarin, started 8 November 2002 - Copyright: TU Muenchen -*) - -(*** -This is a very simple package for transitivity reasoning over linear orders. -Simple means exponential time (and space) in the number of premises. -Should be replaced by a graph-theoretic algorithm. - -The package provides a tactic trans_tac that uses all premises of the form - - 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. - -To get rid of ~= in the premises, it is advisable to use an elimination -rule of the form - - [| t ~= u; t P; u < t ==> P |] ==> P. - -The package is implemented as an ML functor and thus not limited to the -relation <= and friends. It can be instantiated to any total order --- -for example, the divisibility relation "dvd". -***) - -(*** Credits *** - -This package is closely based on a (no longer used) transitivity reasoner for -the natural numbers, which was written by Tobias Nipkow. - -****************) - -signature LESS_ARITH = -sig - val less_reflE: thm (* x < x ==> P *) - val le_refl: thm (* x <= x *) - val less_imp_le: thm (* x < y ==> x <= y *) - val not_lessI: thm (* y <= x ==> ~(x < y) *) - val not_leI: thm (* y < x ==> ~(x <= y) *) - val not_lessD: thm (* ~(x < y) ==> y <= x *) - val not_leD: thm (* ~(x <= y) ==> y < x *) - val eqI: thm (* [| x <= y; y <= x |] ==> x = y *) - val eqD1: thm (* x = y ==> x <= y *) - val eqD2: thm (* x = y ==> y <= x *) - val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) - val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *) - val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *) - val le_trans: thm (* [| x < y; y < z |] ==> x < z *) - val decomp: term -> (term * string * term) option - (* decomp (`x Rel y') should yield (x, Rel, y) - where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=" - other relation symbols are ignored *) -end; - -signature TRANS_TAC = -sig - val trans_tac: int -> tactic -end; - -functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = -struct - -(*** Proof objects ***) - -datatype proof - = Asm of int - | Thm of proof list * thm; - -(* Turn proof objects into theorems *) - -fun prove asms = - let fun pr (Asm i) = nth_elem (i, asms) - | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm - in pr end; - -(*** Exceptions ***) - -exception Contr of proof; (* Raised when contradiction is found *) - -exception Cannot; (* Raised when goal cannot be proved *) - -(*** Internal representation of inequalities ***) - -datatype less - = Less of term * term * proof - | Le of term * term * proof; - -fun lower (Less (x, _, _)) = x - | lower (Le (x, _, _)) = x; - -fun upper (Less (_, y, _)) = y - | upper (Le (_, y, _)) = y; - -infix subsumes; - -fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y') - | (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y') - | (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y') - | _ subsumes _ = false; - -fun trivial (Le (x, x', _)) = (x = x') - | trivial _ = false; - -(*** Transitive closure ***) - -fun add new = - let fun adds([], news) = new::news - | adds(old::olds, news) = if new subsumes old then adds(olds, news) - else adds(olds, old::news) - in adds end; - -fun ctest (less as Less (x, x', p)) = - if x = x' then raise Contr (Thm ([p], Less.less_reflE)) - else less - | ctest less = less; - -fun mktrans (Less (x, _, p), Less (_, z, q)) = - Less (x, z, Thm([p, q], Less.less_trans)) - | mktrans (Less (x, _, p), Le (_, z, q)) = - Less (x, z, Thm([p, q], Less.less_le_trans)) - | mktrans (Le (x, _, p), Less (_, z, q)) = - Less (x, z, Thm([p, q], Less.le_less_trans)) - | mktrans (Le (x, _, p), Le (_, z, q)) = - Le (x, z, Thm([p, q], Less.le_trans)); - -fun trans new olds = - let fun tr (news, old) = - if upper old = lower new then mktrans (old, new)::news - else if upper new = lower old then mktrans (new, old)::news - else news - in foldl tr ([], olds) end; - -fun close1 olds new = - if trivial new orelse exists (fn old => old subsumes new) olds then olds - else let val news = trans new olds - in close (add new (olds, [])) news end -and close olds [] = olds - | close olds (new::news) = close (close1 olds (ctest new)) news; - -(*** Solving and proving goals ***) - -(* Recognise and solve trivial goal *) - -fun triv_sol (Le (x, x', _)) = - if x = x' then Some (Thm ([], Less.le_refl)) - else None - | triv_sol _ = None; - -(* Solve less starting from facts *) - -fun solve facts less = - case triv_sol less of - None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of - (None, _) => raise Cannot - | (Some (Less (_, _, p)), Less _) => p - | (Some (Le (_, _, p)), Less _) => - error "trans_tac/solve: internal error: le cannot subsume less" - | (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le) - | (Some (Le (_, _, p)), Le _) => p) - | Some prf => prf; - -(* Turn term t into Less or Le; n is position of t in list of assumptions *) - -fun mkasm (t, n) = - case Less.decomp t of - Some (x, rel, y) => (case rel of - "<" => [Less (x, y, Asm n)] - | "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))] - | "<=" => [Le (x, y, Asm n)] - | "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))] - | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), - Le (x, y, Thm ([Asm n], Less.eqD1))] - | "~=" => [] - | _ => error ("trans_tac/mkasm: unknown relation " ^ rel)) - | None => []; - -(* Turn goal t into a pair (goals, proof) where goals is a list of - Le/Less-subgoals to solve, and proof the validation that proves the concl t - Asm ~1 is dummy (denotes a goal) -*) - -fun mkconcl t = - case Less.decomp t of - Some (x, rel, y) => (case rel of - "<" => ([Less (x, y, Asm ~1)], Asm 0) - | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI)) - | "<=" => ([Le (x, y, Asm ~1)], Asm 0) - | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI)) - | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], - Thm ([Asm 0, Asm 1], Less.eqI)) - | _ => raise Cannot) - | None => raise Cannot; - -val trans_tac = SUBGOAL (fn (A, n) => - let val Hs = Logic.strip_assums_hyp A - val C = Logic.strip_assums_concl A - val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1))) - val clesss = close [] lesss - val (subgoals, prf) = mkconcl C - val prfs = map (solve clesss) subgoals - in METAHYPS (fn asms => - let val thms = map (prove asms) prfs - in rtac (prove thms prf) 1 end) n - end - handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n - | Cannot => no_tac); - -end; diff -r b3b15305a1c9 -r c5c47703f763 src/Provers/order.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Provers/order.ML Thu Feb 19 15:57:34 2004 +0100 @@ -0,0 +1,1207 @@ +(* + Title: Transitivity reasoner for partial and linear orders + Id: $Id$ + Author: Oliver Kutter + Copyright: TU Muenchen +*) + +(* TODO: reduce number of input thms, reduce code duplication *) + +(* + +The packages 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 implemented as an ML functor and thus 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 LESS_ARITH = +sig + (* Theorems for partial orders *) + val less_reflE: thm (* x < x ==> P *) + val le_refl: thm (* x <= x *) + val less_imp_le: thm (* x < y ==> x <= y *) + val eqI: thm (* [| x <= y; y <= x |] ==> x = y *) + val eqD1: thm (* x = y ==> x <= y *) + val eqD2: thm (* x = y ==> y <= x *) + val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) + val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *) + val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *) + val le_trans: thm (* [| x < y; y < z |] ==> x < z *) + val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) + val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) + + (* Additional theorems for linear orders *) + val not_lessD: thm (* ~(x < y) ==> y <= x *) + val not_leD: thm (* ~(x <= y) ==> y < x *) + val not_lessI: thm (* y <= x ==> ~(x < y) *) + val not_leI: thm (* y < x ==> ~(x <= y) *) + + (* Additional theorems for subgoals of form x ~= y *) + val less_imp_neq : thm (* x < y ==> x ~= y *) + val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *) + + (* Analysis of premises and conclusion *) + (* decomp_x (`x Rel y') should yield (x, Rel, y) + where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", + other relation symbols cause an error message *) + val decomp_part: Sign.sg -> term -> (term * string * term) option + val decomp_lin: Sign.sg -> term -> (term * string * term) option +end; + +signature TRANS_TAC = +sig + val partial_tac: int -> tactic + val linear_tac: int -> tactic +end; + +functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = +struct + +(* Extract subgoal with signature *) + +fun SUBGOAL goalfun i st = + goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st + handle Subscript => Seq.empty; + +(* 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_elem (i, asms) + | 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 sign (t, n) : Sign.sg -> (Term.term * int) -> less *) +(* *) +(* 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 sign (t, n) = + case Less.decomp_part sign t of + Some (x, rel, y) => (case rel of + "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) + else [Less (x, y, Asm n)] + | "~<" => [] + | "<=" => [Le (x, y, Asm n)] + | "~<=" => [] + | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), + Le (y, x, Thm ([Asm n], Less.eqD2))] + | "~=" => if (x aconv y) then + raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) + else [ NotEq (x, y, Asm n), + NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] (* Le (x, x, Thm ([],Less.le_refl))]*) + | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ + "''returned by decomp_part.")) + | None => []; + + + +(* ************************************************************************ *) +(* *) +(* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less *) +(* *) +(* 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 sign (t, n) = + case Less.decomp_lin sign t of + Some (x, rel, y) => (case rel of + "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) + else [Less (x, y, Asm n)] + | "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))] + | "<=" => [Le (x, y, Asm n)] + | "~<=" => if (x aconv y) then + raise (Contr (Thm ([Thm ([Asm n], Less.not_leD)], Less.less_reflE))) + else [Less (y, x, Thm ([Asm n], Less.not_leD))] + | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), + Le (y, x, Thm ([Asm n], Less.eqD2))] + | "~=" => if (x aconv y) then + raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) + else [ NotEq (x, y, Asm n), + NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] + | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ + "''returned by decomp_lin.")) + | None => []; + + +(* ************************************************************************ *) +(* *) +(* mkconcl_partial sign t : Sign.sg -> Term.term -> less *) +(* *) +(* Translates conclusion t to an element of type less. *) +(* Partial orders only. *) +(* *) +(* ************************************************************************ *) + +fun mkconcl_partial sign t = + case Less.decomp_part 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], Less.eqI)) + | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) + | _ => raise Cannot) + | None => raise Cannot; + + +(* ************************************************************************ *) +(* *) +(* mkconcl_linear sign t : Sign.sg -> Term.term -> less *) +(* *) +(* Translates conclusion t to an element of type less. *) +(* Linear orders only. *) +(* *) +(* ************************************************************************ *) + +fun mkconcl_linear sign t = + case Less.decomp_lin 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], Less.not_lessI)) + | "<=" => ([Le (x, y, Asm ~1)], Asm 0) + | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI)) + | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], + Thm ([Asm 0, Asm 1], Less.eqI)) + | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) + | _ => raise Cannot) + | None => raise Cannot; + + + +(* ******************************************************************* *) +(* *) +(* mergeLess (less1,less2): less * less -> less *) +(* *) +(* Merge to 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.less_trans)) +| mergeLess (Less (x, _, p) , Le (_ , z, q)) = + Less (x, z, Thm ([p,q] , Less.less_le_trans)) +| mergeLess (Le (x, _, p) , Less (_ , z, q)) = + Less (x, z, Thm ([p,q] , Less.le_less_trans)) +| mergeLess (Le (x, z, p) , NotEq (x', z', q)) = + if (x aconv x' andalso z aconv z' ) + then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) + 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] , Less.neq_le_trans)) + 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] , Less.le_trans)) +| 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 Library.option *) +(* *) +(* Solves trivial goal x <= x. *) +(* *) +(* ******************************************************************* *) + +fun triv_solv (Le (x, x', _)) = + if x aconv x' then Some (Thm ([], Less.le_refl)) + else None +| triv_solv _ = None; + +(* ********************************************************************* *) +(* Graph functions *) +(* ********************************************************************* *) + + + +(* ******************************************************************* *) +(* *) +(* General: *) +(* *) +(* Inequalities are represented by various types of graphs. *) +(* *) +(* 1. (Term.term * Term.term list) list *) +(* - Graph of this type is generated from the assumptions, *) +(* does not contain information on which edge stems from which *) +(* assumption. *) +(* - Used to compute strong components. *) +(* *) +(* 2. (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 reconstruct paths. *) +(* *) +(* 3. (int * (int * less) list ) list *) +(* - Graph of this type is generated from the strong components of *) +(* graph of type 2. It consists of the strong components of *) +(* graph 2, where nodes are indices of the components. *) +(* Only edges between components are part of this graph. *) +(* - Used to reconstruct paths between several components. *) +(* *) +(* 4. (int * int list) list *) +(* - Graph of this type is generated from graph of type 3, but *) +(* edge information of type less is removed. *) +(* - Used to *) +(* - Compute transposed graphs of type 4. *) +(* - Compute list of components reachable from a component. *) +(* *) +(* *) +(* ******************************************************************* *) + + +(* *********************************************************** *) +(* Functions for constructing graphs *) +(* *********************************************************** *) + +fun addLessEdge (v,d,[]) = [(v,d)] +| addLessEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) + else (u,dl):: (addLessEdge(v,d,el)); + +fun addTermEdge (v,u,[]) = [(v,[u])] +| addTermEdge (v,u,((x,adj)::el)) = if v aconv x then (v,u::adj)::el + else (x,adj) :: addTermEdge (v,u,el); + +(* ********************************************************************* *) +(* *) +(* buildGraphs constructs three graphs from a list of type less: *) +(* g1: graph for the <= relation *) +(* g2: graph for the <= relation with additional information for *) +(* proof reconstruction *) +(* neqEdges: all edges that are candidates for a ~= *) +(* *) +(* ********************************************************************* *) + + +fun buildGraphs ([],g1,g2,neqEdges) = (g1, g2, neqEdges) +| buildGraphs (l::ls,g1,g2,neqEdges) = case l of +(Less (x,y,p)) =>( + let val g1' = addTermEdge (x,y,g1) + and g2' = addLessEdge (x,[(y,(Less (x, y, p)))],g2) + in buildGraphs (ls,g1',g2',l::neqEdges) end) +| (Le (x,y,p)) => +( let val g1' = addTermEdge (x,y,g1) + and g2' = addLessEdge (x,[(y,(Le (x, y,p)))],g2) + in buildGraphs (ls,g1',g2',neqEdges) end) +| (NotEq (x,y,p)) => ( buildGraphs (ls,g1,g2,l::neqEdges) ) + + +(* *********************************************************************** *) +(* *) +(* adjacent_term g u : (Term.term * 'a list ) list -> Term.term -> 'a list *) +(* *) +(* *) +(* *********************************************************************** *) + +fun adjacent_term ((v,adj)::el) u = + if u aconv v then adj else adjacent_term el u +| adjacent_term nil _ = [] + +(* *********************************************************************** *) +(* *) +(* adjacent_term g u : (''a * 'b list ) list -> ''a -> 'b list *) +(* *) +(* List of successors of u in graph g *) +(* *) +(* *********************************************************************** *) + +fun adjacent ((v,adj)::el) u = + if u = v then adj else adjacent el u +| adjacent nil _ = [] + + +(* *********************************************************************** *) +(* *) +(* transpose_term g: *) +(* (Term.term * Term.term list) list -> (Term.term * Term.term list) list *) +(* *) +(* Computes transposed graph g' from g *) +(* by reversing all edges u -> v to v -> u *) +(* *) +(* *********************************************************************** *) + + fun transpose_term g = + let + (* Compute list of reversed edges for each adjacency list *) + fun flip (u,v::el) = (v,u) :: flip (u,el) + | flip (_,nil) = nil + + (* 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 u aconv v then (w::adj,edges) + else (adj,(v,w)::edges) + end + | gather (_,nil) = (nil,nil) + + (* 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 nil _ = nil + + (* Compute, for each adjacency list, the list with reversed edges, + and concatenate these lists. *) + val flipped = foldr (op @) ((map flip g),nil) + + in assemble g flipped end + +(* *********************************************************************** *) +(* *) +(* 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 g = + let + (* Compute list of reversed edges for each adjacency list *) + fun flip (u,v::el) = (v,u) :: flip (u,el) + | flip (_,nil) = nil + + (* 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 u = v then (w::adj,edges) + else (adj,(v,w)::edges) + end + | gather (_,nil) = (nil,nil) + + (* 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 nil _ = nil + + (* Compute, for each adjacency list, the list with reversed edges, + and concatenate these lists. *) + val flipped = foldr (op @) ((map flip g),nil) + + 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 ref = ref nil + + (* List of vertices which have been visited. *) + val visited : term list ref = ref nil + + 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 = + foldr (fn (v,ds) => if been_visited v then ds + else v :: dfs_visit g v @ ds) + ((adjacent_term g u) ,nil) + 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. *) + app (fn u => if been_visited u then () + else (dfs_visit G u; ())) (members G); + visited := nil; + + (* We don't reset finish because its value is used by + revfold 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. *) + foldl (fn (comps,u) => + if been_visited u then comps + else ((u :: dfs_visit (transpose_term G) u) :: comps)) (nil,(!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 ref = ref nil + + fun been_visited v = exists (fn w => w = v) (!visited) + + fun dfs_visit g u : int list = + let + val _ = visited := u :: !visited + val descendents = + foldr (fn (v,ds) => if been_visited v then ds + else v :: dfs_visit g v @ ds) + ( ((adjacent g u)) ,nil) + in descendents end + + in u :: dfs_visit g u end; + + +fun indexComps components = + ListPair.map (fn (a,b) => (b,a)) (components, 0 upto (length components -1)); + +fun indexNodes IndexComp = + flat (map (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; + + +(* ***************************************************************** *) +(* *) +(* evalcompgraph components g ntc : *) +(* Term.term list list -> *) +(* (Term.term * (Term.term * less) list) list -> *) +(* (Term.term * int) list -> (int * (int * less) list) list *) +(* *) +(* *) +(* Computes, from graph g, 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. *) +(* *) +(* ***************************************************************** *) + +fun evalcompgraph components g ntc = + let + (* Liste (Index der Komponente, Komponente *) + val IndexComp = indexComps components; + + (* Compute new graph with the property that it only contains edges + between components. *) + + (* k is index of current start component. *) + + fun processComponent (k, comp) = + let + (* all edges pointing away from the component *) + (* (Term.term * less) list *) + val allEdges = flat (map (adjacent_term g) comp); + + (* choose those edges pointing to nodes outside + the current component *) + + fun selectEdges [] = [] + | selectEdges ((v,l)::es) = let val k' = getIndex v ntc in + if k' = k then selectEdges es else (k', l) :: (selectEdges es) 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,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 sortEdges [] sorted = sorted: (int * less) list + | sortEdges (e::es) sorted = sortEdges es (insert e sorted); + + in + (k, (sortEdges (selectEdges allEdges) [])) + end; + + +in map processComponent IndexComp end; + +(* Remove ``less'' edge info from graph *) +(* type ('a * ('a * less) list) list *) +fun stripOffLess g = map (fn (v, desc) => (v,map (fn (u,l) => u) desc)) g; + + + +(* *********************************************************************** *) +(* *) +(* dfs_term g u v: *) +(* (Term.term *(Term.term * less) list) list -> *) +(* Term.term -> Term.term -> (bool * less list) *) +(* *) +(* Depth first search of v from u. *) +(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) +(* *) +(* *********************************************************************** *) + + +fun dfs_term g u v = + let +(* TODO: this comment is unclear *) + (* Liste der gegangenen Kanten, + die Kante e die zum Vorgaenger eines Knoten u gehoert ist jene + f�r die gilt (upper e) = u *) + val pred : less list ref = ref nil; + val visited: term list ref = ref nil; + + fun been_visited v = exists (fn w => w aconv v) (!visited) + + fun dfs_visit u' = + let val _ = visited := u' :: (!visited) + + fun update l = let val _ = pred := l ::(!pred) in () end; + + in if been_visited v then () + else (app (fn (v',l) => if been_visited v' then () else ( + update l; + dfs_visit v'; ()) )) (adjacent_term 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, pred) = dfs_term g u v; + + 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 ([], Less.le_refl))))] + else path u v ) else raise Cannot +end; + + +(* *********************************************************************** *) +(* *) +(* dfs_int g u v: *) +(* (int *(int * less) list) list -> int -> int *) +(* -> (bool *(int* less) list) *) +(* *) +(* Depth first search of v from u. *) +(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) +(* *) +(* *********************************************************************** *) + +fun dfs_int g u v = + let + val pred : (int * less ) list ref = ref nil; + val visited: int list ref = ref nil; + + fun been_visited v = exists (fn w => 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 (app (fn (v',l) => if been_visited v' then () else ( + update (v',l); + dfs_visit v'; ()) )) (adjacent g u') + + end + + in + dfs_visit u; + if (been_visited v) then (true, (!pred)) else (false , []) + end; + + +(* *********************************************************************** *) +(* *) +(* findProof (g2, cg2, neqEdges, components, ntc) subgoal: *) +(* (Term.term * (Term.term * less) list) list * *) +(* (int * (int * less) list) list * less list * Term.term list list *) +(* * ( (Term.term * int) -> proof *) +(* *) +(* findProof constructs from graphs (g2, cg2) and neqEdges a proof for *) +(* subgoal. Raises exception Cannot if this is not possible. *) +(* *) +(* *********************************************************************** *) + +fun findProof (g2, cg2, neqEdges, components, ntc ) 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,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 g2)@[edge]@(completeTermPath v y' g2) + else (rev_completeComponentPath u)@[edge]@(completeTermPath v y' g2) + end + in + if x aconv y then + [(Le (x, y, (Thm ([], Less.le_refl))))] + else ( if xi = yi then completeTermPath x y g2 + 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 ui mem Xreachable andalso vi mem Xreachable andalso + ui mem Yreachable andalso vi mem Yreachable then ( + + (case e of (Less (_, _, _)) => + let + val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) + in + if xufound then ( + let + val (vyfound, vypred) = dfs_int cg2 (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 (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) + in + if xufound then ( + let + val (uvfound, uvpred) = dfs_int cg2 (getIndex u ntc) (getIndex v ntc) + in + if uvfound then ( + let + val (vyfound, vypred) = dfs_int cg2 (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, _)) => ( + + let + val xi = getIndex x ntc + val yi = getIndex y ntc + (* sucht im Komponentengraphen einen Weg von der Komponente in der x liegt + zu der in der y liegt *) + val (found, pred) = dfs_int cg2 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.less_imp_le)) + 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, _)) => ( + let + val xi = getIndex x ntc + val yi = getIndex y ntc + val cg2' = stripOffLess cg2 + val cg2'_transpose = transpose cg2' + (* alle von x aus erreichbaren Komponenten *) + val xreachable = dfs_int_reachable cg2' xi + (* all comonents reachable from y in the transposed graph cg2' *) + val yreachable = dfs_int_reachable cg2'_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 neqEdges + end + + ) +| (NotEq (x, y, _)) => ( + + let val xi = getIndex x ntc + val yi = getIndex y ntc + val cg2' = stripOffLess cg2 + val cg2'_transpose = transpose cg2' + val xreachable = dfs_int_reachable cg2' xi + val yreachable = dfs_int_reachable cg2'_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.less_imp_neq)) + else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym")) + ) + | (NotEq (u,v, q)) => ( + if u aconv x andalso v aconv y then q + else (Thm ([q], thm "not_sym")) + ) + ) + (* 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 g2) @ [e] @ (completeTermPath v y g2) + val xyLesss = transPath (tl xypath, hd xypath) + in (Thm ([getprf xyLesss], Less.less_imp_neq)) end) + | _ => ( + let val xupath = completeTermPath x u g2 + val uxpath = completeTermPath u x g2 + val vypath = completeTermPath v y g2 + val yvpath = completeTermPath y v g2 + 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)], Less.eqI)) + val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], Less.eqI)) + in + (Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq)) + end + ) + ) else if ui = yi andalso vi = xi then ( + case e of (Less (_, _,_)) => ( + let val xypath = (completeTermPath y u g2) @ [e] @ (completeTermPath v x g2) + val xyLesss = transPath (tl xypath, hd xypath) + in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) + | _ => ( + + let val yupath = completeTermPath y u g2 + val uypath = completeTermPath u y g2 + val vxpath = completeTermPath v x g2 + val xvpath = completeTermPath x v g2 + 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)], Less.eqI)) + val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI)) + in + (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym")) + 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.less_imp_neq)) + | None => ( + let + val yr = dfs_int_reachable cg2' yi + val xr = dfs_int_reachable cg2'_transpose xi + in + case (findLess e y x yi xi yr xr) of + (Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) + | _ => processNeqEdges es + end) + ) end) + in processNeqEdges neqEdges end + ) +end; + + +(* *********************************************************************** *) +(* *) +(* checkComponents g components ntc neqEdges: *) +(* (Term.term * (Term.term * less) list) list -> Term.term list list -> *) +(* (Term.term * int) -> less list -> bool *) +(* *) +(* For each edge in the list neqEdges check if it 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 checkComponents g components ntc neqEdges = + let + (* Construct proof by contradiction for edge *) + fun handleContr edge = + (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.less_reflE ))) + 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.less_reflE ))) + end + ) + | _ => error "trans_tac/checkCompoents/handleContr: invalid Contradiction"); + + (* Check each edge in neqEdges for contradiction. + If there is a contradiction, call handleContr, otherwise do nothing. *) + fun checkNeqEdges [] = () + | checkNeqEdges (e::es) = + (case e of (Less (u, v, _)) => + if (getIndex u ntc) = (getIndex v ntc) then handleContr e g + else checkNeqEdges es + | (NotEq (u, v, _)) => + if (getIndex u ntc) = (getIndex v ntc) then handleContr e g + else checkNeqEdges es + | _ => checkNeqEdges es) + + in if g = [] then () else checkNeqEdges neqEdges end; + +(* *********************************************************************** *) +(* *) +(* solvePartialOrder sign (asms,concl) : *) +(* Sign.sg -> less list * Term.term -> proof list *) +(* *) +(* Find proof if possible for partial orders. *) +(* *) +(* *********************************************************************** *) + +fun solvePartialOrder sign (asms, concl) = + let + val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) + val components = scc_term g1 + val ntc = indexNodes (indexComps components) + val cg2 = evalcompgraph components g2 ntc + in + (* Check for contradiction within assumptions *) + checkComponents g2 components ntc neqEdges; + let + val (subgoals, prf) = mkconcl_partial sign concl + fun solve facts less = + (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less + | Some prf => prf ) + in + map (solve asms) subgoals + end + end; + +(* *********************************************************************** *) +(* *) +(* solveTotalOrder sign (asms,concl) : *) +(* Sign.sg -> less list * Term.term -> proof list *) +(* *) +(* Find proof if possible for linear orders. *) +(* *) +(* *********************************************************************** *) + +fun solveTotalOrder sign (asms, concl) = + let + val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) + val components = scc_term g1 + val ntc = indexNodes (indexComps components) + val cg2 = evalcompgraph components g2 ntc + in + checkComponents g2 components ntc neqEdges; + let + val (subgoals, prf) = mkconcl_linear sign concl + fun solve facts less = + (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less + | Some prf => prf ) + in + map (solve asms) subgoals + end + end; + + +(* partial_tac - solves linear/total orders *) + +val partial_tac = SUBGOAL (fn (A, n, sign) => + let + val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) + val Hs = 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 (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs - 1))) + val prfs = solvePartialOrder sign (lesss, C); + val (subgoals, prf) = mkconcl_partial sign C; + in + METAHYPS (fn asms => + let val thms = map (prove asms) prfs + in rtac (prove thms prf) 1 end) n + end + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n + | Cannot => no_tac + ); + +(* linear_tac - solves linear/total orders *) + +val linear_tac = SUBGOAL (fn (A, n, sign) => + let + val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) + val Hs = 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 (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs - 1))) + val prfs = solveTotalOrder sign (lesss, C); + val (subgoals, prf) = mkconcl_linear sign C; + in + METAHYPS (fn asms => + let val thms = map (prove asms) prfs + in rtac (prove thms prf) 1 end) n + end + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n + | Cannot => no_tac); + +end; +