Efficient, graph-based reasoner for linear and partial orders.
authorballarin
Thu Feb 19 15:57:34 2004 +0100 (2004-02-19)
changeset 14398c5c47703f763
parent 14397 b3b15305a1c9
child 14399 dc677b35e54f
Efficient, graph-based reasoner for linear and partial orders.
+ Setup as solver in the HOL simplifier.
NEWS
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/HOL.thy
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/OG_Hoare.thy
src/HOL/Integ/IntDef.thy
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/Real/RealDef.thy
src/HOL/Ring_and_Field.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded_Recursion.ML
src/HOL/ex/BinEx.thy
src/Provers/linorder.ML
src/Provers/order.ML
     1.1 --- a/NEWS	Thu Feb 19 10:41:32 2004 +0100
     1.2 +++ b/NEWS	Thu Feb 19 15:57:34 2004 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Provers/order.ML:  new efficient reasoner for partial and linear orders.
     1.8 +  Replaces linorder.ML.
     1.9 +
    1.10  * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
    1.11    (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler
    1.12    (\<a>...\<z>), are now considered normal letters, and can therefore
    1.13 @@ -77,6 +80,16 @@
    1.14  
    1.15  *** HOL ***
    1.16  
    1.17 +* Simplifier:
    1.18 +  - Much improved handling of linear and partial orders.
    1.19 +    Reasoners for linear and partial orders are set up for type classes
    1.20 +    "linorder" and "order" respectively, and are added to the default simpset
    1.21 +    as solvers.  This means that the simplifier can build transitivity chains
    1.22 +    to solve goals from the assumptions.
    1.23 +  - INCOMPATIBILITY: old proofs break occasionally.  Typically, applications
    1.24 +    of blast or auto after simplification become unnecessary because the goal
    1.25 +    is solved by simplification already.
    1.26 +
    1.27  * Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, 
    1.28      all proved in axiomatic type classes for semirings, rings and fields.
    1.29  
     2.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Feb 19 10:41:32 2004 +0100
     2.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Feb 19 15:57:34 2004 +0100
     2.3 @@ -3429,7 +3429,7 @@
     2.4              by (cases s2) (simp add: abrupt_if_def)
     2.5            with brkAss_C1 s1_s2 s2_s3
     2.6            show ?thesis
     2.7 -            by simp (blast intro: subset_trans)
     2.8 +            by simp
     2.9          qed
    2.10          moreover from True nrmAss_C2 s2_s3
    2.11          have "nrm C2 \<subseteq> dom (locals (store s3))"
     3.1 --- a/src/HOL/HOL.thy	Thu Feb 19 10:41:32 2004 +0100
     3.2 +++ b/src/HOL/HOL.thy	Thu Feb 19 15:57:34 2004 +0100
     3.3 @@ -946,6 +946,93 @@
     3.4    by (simp add: max_def)
     3.5  
     3.6  
     3.7 +subsubsection {* Transitivity rules for calculational reasoning *}
     3.8 +
     3.9 +
    3.10 +lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
    3.11 +  by (simp add: order_less_le)
    3.12 +
    3.13 +lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
    3.14 +  by (simp add: order_less_le)
    3.15 +
    3.16 +lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
    3.17 +  by (rule order_less_asym)
    3.18 +
    3.19 +
    3.20 +subsubsection {* Setup of transitivity reasoner *}
    3.21 +
    3.22 +lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
    3.23 +  by (erule contrapos_pn, erule subst, rule order_less_irrefl)
    3.24 +
    3.25 +lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
    3.26 +  by (erule subst, erule ssubst, assumption)
    3.27 +
    3.28 +ML_setup {*
    3.29 +
    3.30 +structure Trans_Tac = Trans_Tac_Fun (
    3.31 +  struct
    3.32 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
    3.33 +    val le_refl = thm "order_refl";
    3.34 +    val less_imp_le = thm "order_less_imp_le";
    3.35 +    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
    3.36 +    val not_leI = thm "linorder_not_le" RS thm "iffD2";
    3.37 +    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
    3.38 +    val not_leD = thm "linorder_not_le" RS thm "iffD1";
    3.39 +    val eqI = thm "order_antisym";
    3.40 +    val eqD1 = thm "order_eq_refl";
    3.41 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
    3.42 +    val less_trans = thm "order_less_trans";
    3.43 +    val less_le_trans = thm "order_less_le_trans";
    3.44 +    val le_less_trans = thm "order_le_less_trans";
    3.45 +    val le_trans = thm "order_trans";
    3.46 +    val le_neq_trans = thm "order_le_neq_trans";
    3.47 +    val neq_le_trans = thm "order_neq_le_trans";
    3.48 +    val less_imp_neq = thm "less_imp_neq";
    3.49 +    val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
    3.50 +
    3.51 +    fun decomp_gen sort sign (Trueprop $ t) =
    3.52 +      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
    3.53 +      fun dec (Const ("Not", _) $ t) = (
    3.54 +              case dec t of
    3.55 +                None => None
    3.56 +              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
    3.57 +            | dec (Const ("op =",  _) $ t1 $ t2) = 
    3.58 +                if of_sort t1
    3.59 +                then Some (t1, "=", t2)
    3.60 +                else None
    3.61 +            | dec (Const ("op <=",  _) $ t1 $ t2) = 
    3.62 +                if of_sort t1
    3.63 +                then Some (t1, "<=", t2)
    3.64 +                else None
    3.65 +            | dec (Const ("op <",  _) $ t1 $ t2) = 
    3.66 +                if of_sort t1
    3.67 +                then Some (t1, "<", t2)
    3.68 +                else None
    3.69 +            | dec _ = None
    3.70 +      in dec t end;
    3.71 +
    3.72 +    val decomp_part = decomp_gen ["HOL.order"];
    3.73 +    val decomp_lin = decomp_gen ["HOL.linorder"];
    3.74 +
    3.75 +  end);  (* struct *)
    3.76 +
    3.77 +Context.>> (fn thy => (simpset_ref_of thy :=
    3.78 +  simpset_of thy
    3.79 +    addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
    3.80 +    addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
    3.81 +  thy))
    3.82 +*}
    3.83 +
    3.84 +(* Optional methods
    3.85 +
    3.86 +method_setup trans_partial =
    3.87 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_partial)) *}
    3.88 +  {* simple transitivity reasoner *}	    
    3.89 +method_setup trans_linear =
    3.90 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_linear)) *}
    3.91 +  {* simple transitivity reasoner *}
    3.92 +*)
    3.93 +
    3.94  subsubsection "Bounded quantifiers"
    3.95  
    3.96  syntax
     4.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Thu Feb 19 10:41:32 2004 +0100
     4.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Thu Feb 19 15:57:34 2004 +0100
     4.3 @@ -496,7 +496,6 @@
     4.4  apply (erule disjE)
     4.5  apply(simp add:psubsetI)
     4.6   apply(force dest:subset_antisym)
     4.7 -apply force
     4.8  done
     4.9  
    4.10  subsection {* Interference Freedom *}
     5.1 --- a/src/HOL/HoareParallel/OG_Hoare.thy	Thu Feb 19 10:41:32 2004 +0100
     5.2 +++ b/src/HOL/HoareParallel/OG_Hoare.thy	Thu Feb 19 15:57:34 2004 +0100
     5.3 @@ -237,7 +237,6 @@
     5.4    apply simp
     5.5   apply(rule AnnWhile)
     5.6    apply simp_all
     5.7 - apply(fast)
     5.8  --{* Await *}
     5.9  apply(frule ann_hoare_case_analysis,simp)
    5.10  apply clarify
     6.1 --- a/src/HOL/Integ/IntDef.thy	Thu Feb 19 10:41:32 2004 +0100
     6.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Feb 19 15:57:34 2004 +0100
     6.3 @@ -521,7 +521,6 @@
     6.4  apply (simp add: order_le_less)
     6.5  apply (case_tac "w < 0")
     6.6   apply (simp add: order_less_imp_le)
     6.7 - apply (blast intro: order_less_trans)
     6.8  apply (simp add: linorder_not_less)
     6.9  done
    6.10  
     7.1 --- a/src/HOL/IsaMakefile	Thu Feb 19 10:41:32 2004 +0100
     7.2 +++ b/src/HOL/IsaMakefile	Thu Feb 19 15:57:34 2004 +0100
     7.3 @@ -75,10 +75,10 @@
     7.4    $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
     7.5    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     7.6    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
     7.7 -  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
     7.8 -  $(SRC)/Provers/splitter.ML $(SRC)/Provers/linorder.ML \
     7.9 -  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
    7.10 -  $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    7.11 +  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \
    7.12 +  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
    7.13 +  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
    7.14 +  $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    7.15    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
    7.16    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
    7.17    Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
    7.18 @@ -87,7 +87,8 @@
    7.19    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
    7.20    Integ/cooper_dec.ML Integ/cooper_proof.ML \
    7.21    Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
    7.22 -  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
    7.23 +  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy \
    7.24 +  Integ/int_arith1.ML \
    7.25    Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
    7.26    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
    7.27    Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
     8.1 --- a/src/HOL/ROOT.ML	Thu Feb 19 10:41:32 2004 +0100
     8.2 +++ b/src/HOL/ROOT.ML	Thu Feb 19 15:57:34 2004 +0100
     8.3 @@ -34,7 +34,7 @@
     8.4  use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
     8.5  use "~~/src/Provers/Arith/extract_common_term.ML";
     8.6  use "~~/src/Provers/Arith/cancel_div_mod.ML";
     8.7 -use "~~/src/Provers/linorder.ML";
     8.8 +use "~~/src/Provers/order.ML";
     8.9  
    8.10  with_path "Integ" use_thy "Main";
    8.11  
     9.1 --- a/src/HOL/Real/RealDef.thy	Thu Feb 19 10:41:32 2004 +0100
     9.2 +++ b/src/HOL/Real/RealDef.thy	Thu Feb 19 15:57:34 2004 +0100
     9.3 @@ -467,7 +467,6 @@
     9.4  apply (rule eq_Abs_REAL [of z])
     9.5  apply (rule eq_Abs_REAL [of w]) 
     9.6  apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels)
     9.7 -apply (cut_tac x="x+ya" and y="xa+y" in linorder_linear, auto) 
     9.8  done
     9.9  
    9.10  
    10.1 --- a/src/HOL/Ring_and_Field.thy	Thu Feb 19 10:41:32 2004 +0100
    10.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Feb 19 15:57:34 2004 +0100
    10.3 @@ -1526,6 +1526,7 @@
    10.4  by (simp add: abs_if linorder_neq_iff)
    10.5  
    10.6  lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)"
    10.7 +apply (simp add: abs_if)
    10.8  by (simp add: abs_if  order_less_not_sym [of a 0])
    10.9  
   10.10  lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::ordered_ring)) = (a = 0)" 
   10.11 @@ -1620,11 +1621,17 @@
   10.12  
   10.13  lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" 
   10.14  apply (simp add: order_less_le abs_le_iff)  
   10.15 +apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
   10.16 +apply (simp add: le_minus_self_iff linorder_neq_iff) 
   10.17 +done
   10.18 +(*
   10.19 +apply (simp add: order_less_le abs_le_iff)  
   10.20  apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) 
   10.21 - apply (simp add:  linorder_not_less [symmetric]) 
   10.22 + apply (simp add:  linorder_not_less [symmetric])
   10.23  apply (simp add: le_minus_self_iff linorder_neq_iff) 
   10.24  apply (simp add:  linorder_not_less [symmetric]) 
   10.25  done
   10.26 +*)
   10.27  
   10.28  lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
   10.29  by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono)
    11.1 --- a/src/HOL/Set.thy	Thu Feb 19 10:41:32 2004 +0100
    11.2 +++ b/src/HOL/Set.thy	Thu Feb 19 15:57:34 2004 +0100
    11.3 @@ -1963,15 +1963,6 @@
    11.4  lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
    11.5    by (rule subsetD)
    11.6  
    11.7 -lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
    11.8 -  by (simp add: order_less_le)
    11.9 -
   11.10 -lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
   11.11 -  by (simp add: order_less_le)
   11.12 -
   11.13 -lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
   11.14 -  by (rule order_less_asym)
   11.15 -
   11.16  lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
   11.17    by (rule subst)
   11.18  
    12.1 --- a/src/HOL/SetInterval.thy	Thu Feb 19 10:41:32 2004 +0100
    12.2 +++ b/src/HOL/SetInterval.thy	Thu Feb 19 15:57:34 2004 +0100
    12.3 @@ -33,48 +33,6 @@
    12.4    atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
    12.5    "{l..u} == {l..} Int {..u}"
    12.6  
    12.7 -
    12.8 -subsection {* Setup of transitivity reasoner *}
    12.9 -
   12.10 -ML {*
   12.11 -
   12.12 -structure Trans_Tac = Trans_Tac_Fun (
   12.13 -  struct
   12.14 -    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   12.15 -    val le_refl = thm "order_refl";
   12.16 -    val less_imp_le = thm "order_less_imp_le";
   12.17 -    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
   12.18 -    val not_leI = thm "linorder_not_less" RS thm "iffD2";
   12.19 -    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
   12.20 -    val not_leD = thm "linorder_not_le" RS thm "iffD1";
   12.21 -    val eqI = thm "order_antisym";
   12.22 -    val eqD1 = thm "order_eq_refl";
   12.23 -    val eqD2 = thm "sym" RS thm "order_eq_refl";
   12.24 -    val less_trans = thm "order_less_trans";
   12.25 -    val less_le_trans = thm "order_less_le_trans";
   12.26 -    val le_less_trans = thm "order_le_less_trans";
   12.27 -    val le_trans = thm "order_trans";
   12.28 -    fun decomp (Trueprop $ t) =
   12.29 -      let fun dec (Const ("Not", _) $ t) = (
   12.30 -              case dec t of
   12.31 -		None => None
   12.32 -	      | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
   12.33 -	    | dec (Const (rel, _) $ t1 $ t2) = 
   12.34 -                Some (t1, implode (drop (3, explode rel)), t2)
   12.35 -	    | dec _ = None
   12.36 -      in dec t end
   12.37 -      | decomp _ = None
   12.38 -  end);
   12.39 -
   12.40 -val trans_tac = Trans_Tac.trans_tac;
   12.41 -
   12.42 -*}
   12.43 -
   12.44 -method_setup trans =
   12.45 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *}
   12.46 -  {* simple transitivity reasoner *}
   12.47 -
   12.48 -
   12.49  subsection {*lessThan*}
   12.50  
   12.51  lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
   12.52 @@ -95,8 +53,6 @@
   12.53  lemma Compl_lessThan [simp]: 
   12.54      "!!k:: 'a::linorder. -lessThan k = atLeast k"
   12.55  apply (auto simp add: lessThan_def atLeast_def)
   12.56 - apply (blast intro: linorder_not_less [THEN iffD1])
   12.57 -apply (blast dest: order_le_less_trans)
   12.58  done
   12.59  
   12.60  lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
   12.61 @@ -123,8 +79,6 @@
   12.62  lemma Compl_greaterThan [simp]: 
   12.63      "!!k:: 'a::linorder. -greaterThan k = atMost k"
   12.64  apply (simp add: greaterThan_def atMost_def le_def, auto)
   12.65 -apply (blast intro: linorder_not_less [THEN iffD1])
   12.66 -apply (blast dest: order_le_less_trans)
   12.67  done
   12.68  
   12.69  lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
   12.70 @@ -153,8 +107,6 @@
   12.71  lemma Compl_atLeast [simp]: 
   12.72      "!!k:: 'a::linorder. -atLeast k = lessThan k"
   12.73  apply (simp add: lessThan_def atLeast_def le_def, auto)
   12.74 -apply (blast intro: linorder_not_less [THEN iffD1])
   12.75 -apply (blast dest: order_le_less_trans)
   12.76  done
   12.77  
   12.78  
   12.79 @@ -189,7 +141,6 @@
   12.80       "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
   12.81  apply (auto simp add: greaterThan_def) 
   12.82   apply (subst linorder_not_less [symmetric], blast) 
   12.83 -apply (blast intro: order_le_less_trans) 
   12.84  done
   12.85  
   12.86  lemma greaterThan_eq_iff [iff]:
   12.87 @@ -209,7 +160,6 @@
   12.88       "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
   12.89  apply (auto simp add: lessThan_def) 
   12.90   apply (subst linorder_not_less [symmetric], blast) 
   12.91 -apply (blast intro: order_less_le_trans) 
   12.92  done
   12.93  
   12.94  lemma lessThan_eq_iff [iff]:
   12.95 @@ -270,7 +220,7 @@
   12.96    "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
   12.97    "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
   12.98    "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
   12.99 -by auto (elim linorder_neqE | trans+)+
  12.100 +by auto
  12.101  
  12.102  (* One- and two-sided intervals *)
  12.103  
  12.104 @@ -283,7 +233,7 @@
  12.105    "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
  12.106    "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
  12.107    "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
  12.108 -by auto trans+
  12.109 +by auto
  12.110  
  12.111  (* Two- and two-sided intervals *)
  12.112  
  12.113 @@ -296,7 +246,7 @@
  12.114    "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
  12.115    "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
  12.116    "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
  12.117 -by auto trans+
  12.118 +by auto
  12.119  
  12.120  lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
  12.121  
  12.122 @@ -324,7 +274,7 @@
  12.123    "{)l..u(} Int {u..} = {}"
  12.124    "{l..u} Int {)u..} = {}"
  12.125    "{l..u(} Int {u..} = {}"
  12.126 -  by auto trans+
  12.127 +  by auto
  12.128  
  12.129  (* Two- and two-sided intervals *)
  12.130  
  12.131 @@ -337,7 +287,7 @@
  12.132    "{)l..m} Int {)m..u} = {}"
  12.133    "{l..m(} Int {m..u} = {}"
  12.134    "{l..m} Int {)m..u} = {}"
  12.135 -  by auto trans+
  12.136 +  by auto
  12.137  
  12.138  lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
  12.139  
    13.1 --- a/src/HOL/Transitive_Closure.thy	Thu Feb 19 10:41:32 2004 +0100
    13.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 19 15:57:34 2004 +0100
    13.3 @@ -129,7 +129,7 @@
    13.4  
    13.5  lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*"
    13.6    apply (drule rtrancl_mono)
    13.7 -  apply (drule rtrancl_mono, simp, blast)
    13.8 +  apply (drule rtrancl_mono, simp)
    13.9    done
   13.10  
   13.11  lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*"
    14.1 --- a/src/HOL/Wellfounded_Recursion.ML	Thu Feb 19 10:41:32 2004 +0100
    14.2 +++ b/src/HOL/Wellfounded_Recursion.ML	Thu Feb 19 15:57:34 2004 +0100
    14.3 @@ -322,7 +322,6 @@
    14.4  by (res_inst_tac [("s","x")] (Least_equality RS ssubst) 1);
    14.5  by Auto_tac;
    14.6  by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));  
    14.7 -by (blast_tac (claset() addIs [order_less_trans]) 1);
    14.8  bind_thm("wellorder_LeastI",   result() RS mp RS conjunct1);
    14.9  bind_thm("wellorder_Least_le", result() RS mp RS conjunct2);
   14.10  
    15.1 --- a/src/HOL/ex/BinEx.thy	Thu Feb 19 10:41:32 2004 +0100
    15.2 +++ b/src/HOL/ex/BinEx.thy	Thu Feb 19 15:57:34 2004 +0100
    15.3 @@ -471,7 +471,6 @@
    15.4    apply (simp add: normal_Pls_eq_0)
    15.5    apply (simp only: number_of_minus zminus_0 iszero_def
    15.6                      minus_equation_iff [of _ "0"])
    15.7 -  apply (simp add: eq_commute)
    15.8    done
    15.9  
   15.10  (*The previous command should have finished the proof but the lin-arith
    16.1 --- a/src/Provers/linorder.ML	Thu Feb 19 10:41:32 2004 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,214 +0,0 @@
    16.4 -(*
    16.5 -  Title:	Transitivity reasoner for linear orders
    16.6 -  Id:		$Id$
    16.7 -  Author:	Clemens Ballarin, started 8 November 2002
    16.8 -  Copyright:	TU Muenchen
    16.9 -*)
   16.10 -
   16.11 -(***
   16.12 -This is a very simple package for transitivity reasoning over linear orders.
   16.13 -Simple means exponential time (and space) in the number of premises.
   16.14 -Should be replaced by a graph-theoretic algorithm.
   16.15 -
   16.16 -The package provides a tactic trans_tac that uses all premises of the form
   16.17 -
   16.18 -  t = u, t < u, t <= u, ~(t < u) and ~(t <= u)
   16.19 -
   16.20 -to
   16.21 -1. either derive a contradiction,
   16.22 -   in which case the conclusion can be any term,
   16.23 -2. or prove the conclusion, which must be of the same form as the premises.
   16.24 -
   16.25 -To get rid of ~= in the premises, it is advisable to use an elimination
   16.26 -rule of the form
   16.27 -
   16.28 -  [| t ~= u; t < u ==> P; u < t ==> P |] ==> P.
   16.29 -
   16.30 -The package is implemented as an ML functor and thus not limited to the
   16.31 -relation <= and friends.  It can be instantiated to any total order ---
   16.32 -for example, the divisibility relation "dvd".
   16.33 -***)
   16.34 -
   16.35 -(*** Credits ***
   16.36 -
   16.37 -This package is closely based on a (no longer used) transitivity reasoner for
   16.38 -the natural numbers, which was written by Tobias Nipkow.
   16.39 -
   16.40 -****************)
   16.41 -
   16.42 -signature LESS_ARITH =
   16.43 -sig
   16.44 -  val less_reflE: thm  (* x < x ==> P *)
   16.45 -  val le_refl: thm  (* x <= x *)
   16.46 -  val less_imp_le: thm (* x < y ==> x <= y *)
   16.47 -  val not_lessI: thm (* y <= x  ==> ~(x < y) *)
   16.48 -  val not_leI: thm (* y < x  ==> ~(x <= y) *)
   16.49 -  val not_lessD: thm (* ~(x < y) ==> y <= x *)
   16.50 -  val not_leD: thm (* ~(x <= y) ==> y < x *)
   16.51 -  val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
   16.52 -  val eqD1: thm (* x = y ==> x <= y *)
   16.53 -  val eqD2: thm (* x = y ==> y <= x *)
   16.54 -  val less_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
   16.55 -  val less_le_trans: thm  (* [| x <= y; y < z |] ==> x < z *)
   16.56 -  val le_less_trans: thm  (* [| x < y; y <= z |] ==> x < z *)
   16.57 -  val le_trans: thm  (* [| x < y; y < z |] ==> x < z *)
   16.58 -  val decomp: term -> (term * string * term) option
   16.59 -    (* decomp (`x Rel y') should yield (x, Rel, y)
   16.60 -       where Rel is one of "<", "<=", "~<", "~<=", "=" and "~="
   16.61 -       other relation symbols are ignored *)
   16.62 -end;
   16.63 -
   16.64 -signature TRANS_TAC =
   16.65 -sig
   16.66 -  val trans_tac: int -> tactic
   16.67 -end;
   16.68 -
   16.69 -functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
   16.70 -struct
   16.71 -
   16.72 -(*** Proof objects ***)
   16.73 -
   16.74 -datatype proof
   16.75 -  = Asm of int
   16.76 -  | Thm of proof list * thm;
   16.77 -
   16.78 -(* Turn proof objects into theorems *)
   16.79 -
   16.80 -fun prove asms =
   16.81 -  let fun pr (Asm i) = nth_elem (i, asms)
   16.82 -        | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
   16.83 -  in pr end;
   16.84 -
   16.85 -(*** Exceptions ***)
   16.86 -
   16.87 -exception Contr of proof;  (* Raised when contradiction is found *)
   16.88 -
   16.89 -exception Cannot;  (* Raised when goal cannot be proved *)
   16.90 -
   16.91 -(*** Internal representation of inequalities ***)
   16.92 -
   16.93 -datatype less
   16.94 -  = Less of term * term * proof
   16.95 -  | Le of term * term * proof;
   16.96 -
   16.97 -fun lower (Less (x, _, _)) = x
   16.98 -  | lower (Le (x, _, _)) = x;
   16.99 -
  16.100 -fun upper (Less (_, y, _)) = y
  16.101 -  | upper (Le (_, y, _)) = y;
  16.102 -
  16.103 -infix subsumes;
  16.104 -
  16.105 -fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
  16.106 -  | (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y')
  16.107 -  | (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
  16.108 -  | _ subsumes _ = false;
  16.109 -
  16.110 -fun trivial (Le (x, x', _)) = (x = x')
  16.111 -  | trivial _ = false;
  16.112 -
  16.113 -(*** Transitive closure ***)
  16.114 -
  16.115 -fun add new =
  16.116 -  let fun adds([], news) = new::news
  16.117 -        | adds(old::olds, news) = if new subsumes old then adds(olds, news)
  16.118 -                                  else adds(olds, old::news)
  16.119 -  in adds end;
  16.120 -
  16.121 -fun ctest (less as Less (x, x', p)) = 
  16.122 -    if x = x' then raise Contr (Thm ([p], Less.less_reflE))
  16.123 -    else less
  16.124 -  | ctest less = less;
  16.125 -
  16.126 -fun mktrans (Less (x, _, p), Less (_, z, q)) =
  16.127 -    Less (x, z, Thm([p, q], Less.less_trans))
  16.128 -  | mktrans (Less (x, _, p), Le (_, z, q)) =
  16.129 -    Less (x, z, Thm([p, q], Less.less_le_trans))
  16.130 -  | mktrans (Le (x, _, p), Less (_, z, q)) =
  16.131 -    Less (x, z, Thm([p, q], Less.le_less_trans))
  16.132 -  | mktrans (Le (x, _, p), Le (_, z, q)) =
  16.133 -    Le (x, z, Thm([p, q], Less.le_trans));
  16.134 -
  16.135 -fun trans new olds =
  16.136 -  let fun tr (news, old) =
  16.137 -            if upper old = lower new then mktrans (old, new)::news
  16.138 -            else if upper new = lower old then mktrans (new, old)::news
  16.139 -            else news
  16.140 -  in foldl tr ([], olds) end;
  16.141 -
  16.142 -fun close1 olds new =
  16.143 -    if trivial new orelse exists (fn old => old subsumes new) olds then olds
  16.144 -    else let val news = trans new olds
  16.145 -         in close (add new (olds, [])) news end
  16.146 -and close olds [] = olds
  16.147 -  | close olds (new::news) = close (close1 olds (ctest new)) news;
  16.148 -
  16.149 -(*** Solving and proving goals ***)
  16.150 -
  16.151 -(* Recognise and solve trivial goal *)
  16.152 -
  16.153 -fun triv_sol (Le (x, x',  _)) = 
  16.154 -    if x = x' then Some (Thm ([], Less.le_refl)) 
  16.155 -    else None
  16.156 -  | triv_sol _ = None;
  16.157 -
  16.158 -(* Solve less starting from facts *)
  16.159 -
  16.160 -fun solve facts less =
  16.161 -  case triv_sol less of
  16.162 -    None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of
  16.163 -	(None, _) => raise Cannot
  16.164 -      | (Some (Less (_, _, p)), Less _) => p
  16.165 -      | (Some (Le (_, _, p)), Less _) =>
  16.166 -	   error "trans_tac/solve: internal error: le cannot subsume less"
  16.167 -      | (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le)
  16.168 -      | (Some (Le (_, _, p)), Le _) => p)
  16.169 -  | Some prf => prf;
  16.170 -
  16.171 -(* Turn term t into Less or Le; n is position of t in list of assumptions *)
  16.172 -
  16.173 -fun mkasm (t, n) =
  16.174 -  case Less.decomp t of
  16.175 -    Some (x, rel, y) => (case rel of
  16.176 -      "<"   => [Less (x, y, Asm n)]
  16.177 -    | "~<"  => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
  16.178 -    | "<="  => [Le (x, y, Asm n)]
  16.179 -    | "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))]
  16.180 -    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
  16.181 -                Le (x, y, Thm ([Asm n], Less.eqD1))]
  16.182 -    | "~="  => []
  16.183 -    | _     => error ("trans_tac/mkasm: unknown relation " ^ rel))
  16.184 -  | None => [];
  16.185 -
  16.186 -(* Turn goal t into a pair (goals, proof) where goals is a list of
  16.187 -   Le/Less-subgoals to solve, and proof the validation that proves the concl t
  16.188 -   Asm ~1 is dummy (denotes a goal)
  16.189 -*)
  16.190 -
  16.191 -fun mkconcl t =
  16.192 -  case Less.decomp t of
  16.193 -    Some (x, rel, y) => (case rel of
  16.194 -      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
  16.195 -    | "~<"  => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
  16.196 -    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
  16.197 -    | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
  16.198 -    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
  16.199 -                 Thm ([Asm 0, Asm 1], Less.eqI))
  16.200 -    | _  => raise Cannot)
  16.201 -  | None => raise Cannot;
  16.202 -
  16.203 -val trans_tac = SUBGOAL (fn (A, n) =>
  16.204 -  let val Hs = Logic.strip_assums_hyp A
  16.205 -    val C = Logic.strip_assums_concl A
  16.206 -    val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
  16.207 -    val clesss = close [] lesss
  16.208 -    val (subgoals, prf) = mkconcl C
  16.209 -    val prfs = map (solve clesss) subgoals
  16.210 -  in METAHYPS (fn asms =>
  16.211 -    let val thms = map (prove asms) prfs
  16.212 -    in rtac (prove thms prf) 1 end) n
  16.213 -  end
  16.214 -  handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
  16.215 -       | Cannot => no_tac);
  16.216 -
  16.217 -end;
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Provers/order.ML	Thu Feb 19 15:57:34 2004 +0100
    17.3 @@ -0,0 +1,1207 @@
    17.4 +(*
    17.5 +  Title:	Transitivity reasoner for partial and linear orders
    17.6 +  Id:		$Id$
    17.7 +  Author:	Oliver Kutter
    17.8 +  Copyright:	TU Muenchen
    17.9 +*)
   17.10 +
   17.11 +(* TODO: reduce number of input thms, reduce code duplication *)
   17.12 +
   17.13 +(*
   17.14 +
   17.15 +The packages provides tactics partial_tac and linear_tac that use all
   17.16 +premises of the form
   17.17 +
   17.18 +  t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
   17.19 +
   17.20 +to
   17.21 +1. either derive a contradiction,
   17.22 +   in which case the conclusion can be any term,
   17.23 +2. or prove the conclusion, which must be of the same form as the
   17.24 +   premises (excluding ~(t < u) and ~(t <= u) for partial orders)
   17.25 +
   17.26 +The package is implemented as an ML functor and thus not limited to the
   17.27 +relation <= and friends.  It can be instantiated to any partial and/or
   17.28 +linear order --- for example, the divisibility relation "dvd".  In
   17.29 +order to instantiate the package for a partial order only, supply
   17.30 +dummy theorems to the rules for linear orders, and don't use
   17.31 +linear_tac!
   17.32 +
   17.33 +*)
   17.34 +
   17.35 +signature LESS_ARITH =
   17.36 +sig
   17.37 +  (* Theorems for partial orders *)
   17.38 +  val less_reflE: thm  (* x < x ==> P *)
   17.39 +  val le_refl: thm  (* x <= x *)
   17.40 +  val less_imp_le: thm (* x < y ==> x <= y *)
   17.41 +  val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
   17.42 +  val eqD1: thm (* x = y ==> x <= y *)
   17.43 +  val eqD2: thm (* x = y ==> y <= x *)
   17.44 +  val less_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
   17.45 +  val less_le_trans: thm  (* [| x <= y; y < z |] ==> x < z *)
   17.46 +  val le_less_trans: thm  (* [| x < y; y <= z |] ==> x < z *)
   17.47 +  val le_trans: thm  (* [| x < y; y < z |] ==> x < z *)
   17.48 +  val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
   17.49 +  val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
   17.50 +
   17.51 +  (* Additional theorems for linear orders *)
   17.52 +  val not_lessD: thm (* ~(x < y) ==> y <= x *)
   17.53 +  val not_leD: thm (* ~(x <= y) ==> y < x *)
   17.54 +  val not_lessI: thm (* y <= x  ==> ~(x < y) *)
   17.55 +  val not_leI: thm (* y < x  ==> ~(x <= y) *)
   17.56 +
   17.57 +  (* Additional theorems for subgoals of form x ~= y *)
   17.58 +  val less_imp_neq : thm (* x < y ==> x ~= y *)
   17.59 +  val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
   17.60 +
   17.61 +  (* Analysis of premises and conclusion *)
   17.62 +  (* decomp_x (`x Rel y') should yield (x, Rel, y)
   17.63 +       where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
   17.64 +       other relation symbols cause an error message *)
   17.65 +  val decomp_part: Sign.sg -> term -> (term * string * term) option
   17.66 +  val decomp_lin: Sign.sg -> term -> (term * string * term) option
   17.67 +end;
   17.68 +
   17.69 +signature TRANS_TAC  =
   17.70 +sig
   17.71 +  val partial_tac: int -> tactic
   17.72 +  val linear_tac:  int -> tactic
   17.73 +end;
   17.74 +
   17.75 +functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
   17.76 +struct
   17.77 +
   17.78 +(* Extract subgoal with signature *)
   17.79 +
   17.80 +fun SUBGOAL goalfun i st =
   17.81 +  goalfun (List.nth(prems_of st, i-1),  i, sign_of_thm st) st
   17.82 +                             handle Subscript => Seq.empty;
   17.83 +
   17.84 +(* Internal datatype for the proof *)
   17.85 +datatype proof
   17.86 +  = Asm of int 
   17.87 +  | Thm of proof list * thm; 
   17.88 +  
   17.89 +exception Cannot;
   17.90 +  (* Internal exception, raised if conclusion cannot be derived from
   17.91 +     assumptions. *)
   17.92 +exception Contr of proof;
   17.93 +  (* Internal exception, raised if contradiction ( x < x ) was derived *)
   17.94 +
   17.95 +fun prove asms = 
   17.96 +  let fun pr (Asm i) = nth_elem (i, asms)
   17.97 +  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
   17.98 +  in pr end;
   17.99 +
  17.100 +(* Internal datatype for inequalities *)
  17.101 +datatype less 
  17.102 +   = Less  of term * term * proof 
  17.103 +   | Le    of term * term * proof
  17.104 +   | NotEq of term * term * proof; 
  17.105 +
  17.106 +   
  17.107 +(* Misc functions for datatype less *)
  17.108 +fun lower (Less (x, _, _)) = x
  17.109 +  | lower (Le (x, _, _)) = x
  17.110 +  | lower (NotEq (x,_,_)) = x;
  17.111 +
  17.112 +fun upper (Less (_, y, _)) = y
  17.113 +  | upper (Le (_, y, _)) = y
  17.114 +  | upper (NotEq (_,y,_)) = y;
  17.115 +
  17.116 +fun getprf   (Less (_, _, p)) = p
  17.117 +|   getprf   (Le   (_, _, p)) = p
  17.118 +|   getprf   (NotEq (_,_, p)) = p;
  17.119 +
  17.120 +
  17.121 +(* ************************************************************************ *)
  17.122 +(*                                                                          *)
  17.123 +(* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less         *)
  17.124 +(*                                                                          *)
  17.125 +(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
  17.126 +(* translated to an element of type less.                                   *)
  17.127 +(* Partial orders only.                                                     *)
  17.128 +(*                                                                          *)
  17.129 +(* ************************************************************************ *)
  17.130 +
  17.131 +fun mkasm_partial sign (t, n) =
  17.132 +  case Less.decomp_part sign t of
  17.133 +    Some (x, rel, y) => (case rel of
  17.134 +      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
  17.135 +               else [Less (x, y, Asm n)]
  17.136 +    | "~<"  => []
  17.137 +    | "<="  => [Le (x, y, Asm n)]
  17.138 +    | "~<=" => [] 
  17.139 +    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
  17.140 +                Le (y, x, Thm ([Asm n], Less.eqD2))]
  17.141 +    | "~="  => if (x aconv y) then 
  17.142 +                  raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
  17.143 +               else [ NotEq (x, y, Asm n),
  17.144 +                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] (* Le (x, x, Thm ([],Less.le_refl))]*) 
  17.145 +    | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
  17.146 +                 "''returned by decomp_part."))
  17.147 +  | None => [];
  17.148 +
  17.149 +
  17.150 +
  17.151 +(* ************************************************************************ *)
  17.152 +(*                                                                          *)
  17.153 +(* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less          *)
  17.154 +(*                                                                          *)
  17.155 +(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
  17.156 +(* translated to an element of type less.                                   *)
  17.157 +(* Linear orders only.                                                      *)
  17.158 +(*                                                                          *)
  17.159 +(* ************************************************************************ *)
  17.160 + 
  17.161 +fun mkasm_linear sign (t, n) =
  17.162 +  case Less.decomp_lin sign t of
  17.163 +    Some (x, rel, y) => (case rel of
  17.164 +      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
  17.165 +               else [Less (x, y, Asm n)]
  17.166 +    | "~<"  => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
  17.167 +    | "<="  => [Le (x, y, Asm n)]
  17.168 +    | "~<=" => if (x aconv y) then 
  17.169 +                  raise (Contr (Thm ([Thm ([Asm n], Less.not_leD)], Less.less_reflE))) 
  17.170 +               else [Less (y, x, Thm ([Asm n], Less.not_leD))] 
  17.171 +    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
  17.172 +                Le (y, x, Thm ([Asm n], Less.eqD2))]
  17.173 +    | "~="  => if (x aconv y) then 
  17.174 +                  raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
  17.175 +               else [ NotEq (x, y, Asm n),
  17.176 +                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
  17.177 +    | _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
  17.178 +                 "''returned by decomp_lin."))
  17.179 +  | None => [];
  17.180 +
  17.181 +
  17.182 +(* ************************************************************************ *)
  17.183 +(*                                                                          *)
  17.184 +(* mkconcl_partial sign t : Sign.sg -> Term.term -> less                    *)
  17.185 +(*                                                                          *)
  17.186 +(* Translates conclusion t to an element of type less.                      *)
  17.187 +(* Partial orders only.                                                     *)
  17.188 +(*                                                                          *)
  17.189 +(* ************************************************************************ *)
  17.190 +
  17.191 +fun mkconcl_partial sign t =
  17.192 +  case Less.decomp_part sign t of
  17.193 +    Some (x, rel, y) => (case rel of
  17.194 +      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
  17.195 +    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
  17.196 +    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
  17.197 +                 Thm ([Asm 0, Asm 1], Less.eqI))
  17.198 +    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
  17.199 +    | _  => raise Cannot)
  17.200 +  | None => raise Cannot;
  17.201 +
  17.202 +
  17.203 +(* ************************************************************************ *)
  17.204 +(*                                                                          *)
  17.205 +(* mkconcl_linear sign t : Sign.sg -> Term.term -> less                     *)
  17.206 +(*                                                                          *)
  17.207 +(* Translates conclusion t to an element of type less.                      *)
  17.208 +(* Linear orders only.                                                      *)
  17.209 +(*                                                                          *)
  17.210 +(* ************************************************************************ *)
  17.211 +
  17.212 +fun mkconcl_linear sign t =
  17.213 +  case Less.decomp_lin sign t of
  17.214 +    Some (x, rel, y) => (case rel of
  17.215 +      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
  17.216 +    | "~<"  => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
  17.217 +    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
  17.218 +    | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
  17.219 +    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
  17.220 +                 Thm ([Asm 0, Asm 1], Less.eqI))
  17.221 +    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
  17.222 +    | _  => raise Cannot)
  17.223 +  | None => raise Cannot;
  17.224 + 
  17.225 +
  17.226 +
  17.227 +(* ******************************************************************* *)
  17.228 +(*                                                                     *)
  17.229 +(* mergeLess (less1,less2):  less * less -> less                       *)
  17.230 +(*                                                                     *)
  17.231 +(* Merge to elements of type less according to the following rules     *)
  17.232 +(*                                                                     *)
  17.233 +(* x <  y && y <  z ==> x < z                                          *)
  17.234 +(* x <  y && y <= z ==> x < z                                          *)
  17.235 +(* x <= y && y <  z ==> x < z                                          *)
  17.236 +(* x <= y && y <= z ==> x <= z                                         *)
  17.237 +(* x <= y && x ~= y ==> x < y                                          *)
  17.238 +(* x ~= y && x <= y ==> x < y                                          *)
  17.239 +(* x <  y && x ~= y ==> x < y                                          *)
  17.240 +(* x ~= y && x <  y ==> x < y                                          *)
  17.241 +(*                                                                     *)
  17.242 +(* ******************************************************************* *)
  17.243 +
  17.244 +fun mergeLess (Less (x, _, p) , Less (_ , z, q)) =
  17.245 +      Less (x, z, Thm ([p,q] , Less.less_trans))
  17.246 +|   mergeLess (Less (x, _, p) , Le (_ , z, q)) =
  17.247 +      Less (x, z, Thm ([p,q] , Less.less_le_trans))
  17.248 +|   mergeLess (Le (x, _, p) , Less (_ , z, q)) =
  17.249 +      Less (x, z, Thm ([p,q] , Less.le_less_trans))
  17.250 +|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
  17.251 +      if (x aconv x' andalso z aconv z' ) 
  17.252 +      then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
  17.253 +      else error "linear/partial_tac: internal error le_neq_trans"
  17.254 +|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
  17.255 +      if (x aconv x' andalso z aconv z') 
  17.256 +      then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
  17.257 +      else error "linear/partial_tac: internal error neq_le_trans"
  17.258 +|   mergeLess (NotEq (x, z, p) , Less (x' , z', q)) =
  17.259 +      if (x aconv x' andalso z aconv z') 
  17.260 +      then Less ((x' , z', q))
  17.261 +      else error "linear/partial_tac: internal error neq_less_trans"
  17.262 +|   mergeLess (Less (x, z, p) , NotEq (x', z', q)) =
  17.263 +      if (x aconv x' andalso z aconv z') 
  17.264 +      then Less (x, z, p)
  17.265 +      else error "linear/partial_tac: internal error less_neq_trans"
  17.266 +|   mergeLess (Le (x, _, p) , Le (_ , z, q)) =
  17.267 +      Le (x, z, Thm ([p,q] , Less.le_trans))
  17.268 +|   mergeLess (_, _) =
  17.269 +      error "linear/partial_tac: internal error: undefined case";
  17.270 +
  17.271 +
  17.272 +(* ******************************************************************** *)
  17.273 +(* tr checks for valid transitivity step                                *)
  17.274 +(* ******************************************************************** *)
  17.275 +
  17.276 +infix tr;
  17.277 +fun (Less (_, y, _)) tr (Le (x', _, _))   = ( y aconv x' )
  17.278 +  | (Le   (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
  17.279 +  | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
  17.280 +  | (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
  17.281 +  | _ tr _ = false;
  17.282 +  
  17.283 +  
  17.284 +(* ******************************************************************* *)
  17.285 +(*                                                                     *)
  17.286 +(* transPath (Lesslist, Less): (less list * less) -> less              *)
  17.287 +(*                                                                     *)
  17.288 +(* If a path represented by a list of elements of type less is found,  *)
  17.289 +(* this needs to be contracted to a single element of type less.       *)
  17.290 +(* Prior to each transitivity step it is checked whether the step is   *)
  17.291 +(* valid.                                                              *)
  17.292 +(*                                                                     *)
  17.293 +(* ******************************************************************* *)
  17.294 +
  17.295 +fun transPath ([],lesss) = lesss
  17.296 +|   transPath (x::xs,lesss) =
  17.297 +      if lesss tr x then transPath (xs, mergeLess(lesss,x))
  17.298 +      else error "linear/partial_tac: internal error transpath";
  17.299 +  
  17.300 +(* ******************************************************************* *)
  17.301 +(*                                                                     *)
  17.302 +(* less1 subsumes less2 : less -> less -> bool                         *)
  17.303 +(*                                                                     *)
  17.304 +(* subsumes checks whether less1 implies less2                         *)
  17.305 +(*                                                                     *)
  17.306 +(* ******************************************************************* *)
  17.307 +  
  17.308 +infix subsumes;
  17.309 +fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
  17.310 +      (x aconv x' andalso y aconv y')
  17.311 +  | (Less (x, y, _)) subsumes (Less (x', y', _)) =
  17.312 +      (x aconv x' andalso y aconv y')
  17.313 +  | (Le (x, y, _)) subsumes (Le (x', y', _)) =
  17.314 +      (x aconv x' andalso y aconv y')
  17.315 +  | (Less (x, y, _)) subsumes (NotEq (x', y', _)) =
  17.316 +      (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
  17.317 +  | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) =
  17.318 +      (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
  17.319 +  | (Le _) subsumes (Less _) =
  17.320 +      error "linear/partial_tac: internal error: Le cannot subsume Less"
  17.321 +  | _ subsumes _ = false;
  17.322 +
  17.323 +(* ******************************************************************* *)
  17.324 +(*                                                                     *)
  17.325 +(* triv_solv less1 : less ->  proof Library.option                     *)
  17.326 +(*                                                                     *)
  17.327 +(* Solves trivial goal x <= x.                                         *)
  17.328 +(*                                                                     *)
  17.329 +(* ******************************************************************* *)
  17.330 +
  17.331 +fun triv_solv (Le (x, x', _)) =
  17.332 +    if x aconv x' then  Some (Thm ([], Less.le_refl)) 
  17.333 +    else None
  17.334 +|   triv_solv _ = None;
  17.335 +
  17.336 +(* ********************************************************************* *)
  17.337 +(* Graph functions                                                       *)
  17.338 +(* ********************************************************************* *)
  17.339 +
  17.340 +
  17.341 +
  17.342 +(* ******************************************************************* *)
  17.343 +(*                                                                     *)
  17.344 +(* General:                                                            *)
  17.345 +(*                                                                     *)
  17.346 +(* Inequalities are represented by various types of graphs.            *)
  17.347 +(*                                                                     *)
  17.348 +(* 1. (Term.term * Term.term list) list                                *)
  17.349 +(*    - Graph of this type is generated from the assumptions,          *)
  17.350 +(*      does not contain information on which edge stems from which    *)
  17.351 +(*      assumption.                                                    *)
  17.352 +(*    - Used to compute strong components.                             *)
  17.353 +(*                                                                     *)
  17.354 +(* 2. (Term.term * (Term.term * less) list) list                       *)
  17.355 +(*    - Graph of this type is generated from the assumptions,          *)
  17.356 +(*      it does contain information on which edge stems from which     *)
  17.357 +(*      assumption.                                                    *)
  17.358 +(*    - Used to reconstruct paths.                                     *)
  17.359 +(*                                                                     *)
  17.360 +(* 3. (int * (int * less) list ) list                                  *)
  17.361 +(*    - Graph of this type is generated from the strong components of  *)
  17.362 +(*      graph of type 2.  It consists of the strong components of      *)
  17.363 +(*      graph 2, where nodes are indices of the components.            *)
  17.364 +(*      Only edges between components are part of this graph.          *)
  17.365 +(*    - Used to reconstruct paths between several components.          *)
  17.366 +(*                                                                     *)
  17.367 +(* 4. (int * int list) list                                            *)
  17.368 +(*    - Graph of this type is generated from graph of type 3, but      *)
  17.369 +(*      edge information of type less is removed.                      *)
  17.370 +(*    - Used to                                                        *)
  17.371 +(*      - Compute transposed graphs of type 4.                         *)
  17.372 +(*      - Compute list of components reachable from a component.       *)
  17.373 +(*                                                                     *)
  17.374 +(*                                                                     *)
  17.375 +(* ******************************************************************* *)
  17.376 +
  17.377 +   
  17.378 +(* *********************************************************** *)
  17.379 +(* Functions for constructing graphs                           *)
  17.380 +(* *********************************************************** *)
  17.381 +
  17.382 +fun addLessEdge (v,d,[]) = [(v,d)]
  17.383 +|   addLessEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
  17.384 +    else (u,dl):: (addLessEdge(v,d,el));
  17.385 +
  17.386 +fun addTermEdge (v,u,[]) = [(v,[u])]
  17.387 +|   addTermEdge (v,u,((x,adj)::el)) = if v aconv x then (v,u::adj)::el
  17.388 +    else    (x,adj) :: addTermEdge (v,u,el);
  17.389 +    
  17.390 +(* ********************************************************************* *)
  17.391 +(*                                                                       *)
  17.392 +(* buildGraphs constructs three graphs from a list of type less:         *)
  17.393 +(*   g1: graph for the <= relation                                       *)
  17.394 +(*   g2: graph for the <= relation with additional information for       *)
  17.395 +(*       proof reconstruction                                            *)
  17.396 +(*   neqEdges: all edges that are candidates for a ~=                    *)
  17.397 +(*                                                                       *)
  17.398 +(* ********************************************************************* *)
  17.399 +
  17.400 +
  17.401 +fun buildGraphs ([],g1,g2,neqEdges) = (g1, g2, neqEdges)
  17.402 +|   buildGraphs (l::ls,g1,g2,neqEdges) = case l of 
  17.403 +(Less (x,y,p)) =>(
  17.404 +      let val g1' = addTermEdge (x,y,g1)
  17.405 +       and g2' = addLessEdge (x,[(y,(Less (x, y, p)))],g2)
  17.406 +      in buildGraphs (ls,g1',g2',l::neqEdges) end)
  17.407 +| (Le (x,y,p)) =>
  17.408 +( let val g1' = addTermEdge (x,y,g1)
  17.409 +       and g2' = addLessEdge (x,[(y,(Le (x, y,p)))],g2)
  17.410 +  in buildGraphs (ls,g1',g2',neqEdges) end)
  17.411 +| (NotEq  (x,y,p)) => (   buildGraphs (ls,g1,g2,l::neqEdges) )
  17.412 +
  17.413 +
  17.414 +(* *********************************************************************** *)
  17.415 +(*                                                                         *)
  17.416 +(* adjacent_term g u : (Term.term * 'a list ) list -> Term.term -> 'a list *)
  17.417 +(*                                                                         *)
  17.418 +(*                                                                         *)
  17.419 +(* *********************************************************************** *)
  17.420 +
  17.421 +fun adjacent_term ((v,adj)::el) u = 
  17.422 +    if u aconv v then adj else adjacent_term el u
  17.423 +|   adjacent_term nil _ = []
  17.424 +
  17.425 +(* *********************************************************************** *)
  17.426 +(*                                                                         *)
  17.427 +(* adjacent_term g u : (''a * 'b list ) list -> ''a -> 'b list             *)
  17.428 +(*                                                                         *)
  17.429 +(* List of successors of u in graph g                                      *)
  17.430 +(*                                                                         *)
  17.431 +(* *********************************************************************** *)
  17.432 + 
  17.433 +fun adjacent ((v,adj)::el) u = 
  17.434 +    if u = v then adj else adjacent el u
  17.435 +|   adjacent nil _ = []  
  17.436 +  
  17.437 +
  17.438 +(* *********************************************************************** *)
  17.439 +(*                                                                         *)
  17.440 +(* transpose_term g:                                                       *)
  17.441 +(* (Term.term * Term.term list) list -> (Term.term * Term.term list) list  *)
  17.442 +(*                                                                         *)
  17.443 +(* Computes transposed graph g' from g                                     *)
  17.444 +(* by reversing all edges u -> v to v -> u                                 *)
  17.445 +(*                                                                         *)
  17.446 +(* *********************************************************************** *)
  17.447 +
  17.448 + fun transpose_term g =
  17.449 +  let
  17.450 +   (* Compute list of reversed edges for each adjacency list *)
  17.451 +   fun flip (u,v::el) = (v,u) :: flip (u,el)
  17.452 +     | flip (_,nil) = nil
  17.453 +
  17.454 +   (* Compute adjacency list for node u from the list of edges
  17.455 +      and return a likewise reduced list of edges.  The list of edges
  17.456 +      is searches for edges starting from u, and these edges are removed. *)
  17.457 +   fun gather (u,(v,w)::el) =
  17.458 +    let
  17.459 +     val (adj,edges) = gather (u,el)
  17.460 +    in
  17.461 +      if u aconv v then (w::adj,edges)
  17.462 +      else (adj,(v,w)::edges)
  17.463 +    end
  17.464 +   | gather (_,nil) = (nil,nil)
  17.465 +
  17.466 +   (* For every node in the input graph, call gather to find all reachable
  17.467 +      nodes in the list of edges *)
  17.468 +   fun assemble ((u,_)::el) edges =
  17.469 +       let val (adj,edges) = gather (u,edges)
  17.470 +       in (u,adj) :: assemble el edges
  17.471 +       end
  17.472 +     | assemble nil _ = nil
  17.473 +
  17.474 +   (* Compute, for each adjacency list, the list with reversed edges,
  17.475 +      and concatenate these lists. *)
  17.476 +   val flipped = foldr (op @) ((map flip g),nil)
  17.477 +      
  17.478 + in assemble g flipped  end    
  17.479 +      
  17.480 +(* *********************************************************************** *)
  17.481 +(*                                                                         *)
  17.482 +(* transpose g:                                                            *)
  17.483 +(* (''a * ''a list) list -> (''a * ''a list) list                          *)
  17.484 +(*                                                                         *)
  17.485 +(* Computes transposed graph g' from g                                     *)
  17.486 +(* by reversing all edges u -> v to v -> u                                 *)
  17.487 +(*                                                                         *)
  17.488 +(* *********************************************************************** *)
  17.489 +
  17.490 +fun transpose g =
  17.491 +  let
  17.492 +   (* Compute list of reversed edges for each adjacency list *)
  17.493 +   fun flip (u,v::el) = (v,u) :: flip (u,el)
  17.494 +     | flip (_,nil) = nil
  17.495 +   
  17.496 +   (* Compute adjacency list for node u from the list of edges
  17.497 +      and return a likewise reduced list of edges.  The list of edges
  17.498 +      is searches for edges starting from u, and these edges are removed. *)
  17.499 +   fun gather (u,(v,w)::el) =
  17.500 +    let
  17.501 +     val (adj,edges) = gather (u,el)
  17.502 +    in
  17.503 +     if u = v then (w::adj,edges)
  17.504 +     else (adj,(v,w)::edges)
  17.505 +    end
  17.506 +   | gather (_,nil) = (nil,nil)
  17.507 +
  17.508 +   (* For every node in the input graph, call gather to find all reachable
  17.509 +      nodes in the list of edges *)
  17.510 +   fun assemble ((u,_)::el) edges =
  17.511 +       let val (adj,edges) = gather (u,edges)
  17.512 +       in (u,adj) :: assemble el edges
  17.513 +       end
  17.514 +     | assemble nil _ = nil
  17.515 +
  17.516 +   (* Compute, for each adjacency list, the list with reversed edges,
  17.517 +      and concatenate these lists. *)
  17.518 +   val flipped = foldr (op @) ((map flip g),nil)
  17.519 + 
  17.520 + in assemble g flipped end    
  17.521 +      
  17.522 +      
  17.523 +(* scc_term : (term * term list) list -> term list list *)
  17.524 +
  17.525 +(* The following is based on the algorithm for finding strongly
  17.526 +   connected components described in Introduction to Algorithms,
  17.527 +   by Cormon, Leiserson, and Rivest, section 23.5. The input G
  17.528 +   is an adjacency list description of a directed graph. The
  17.529 +   output is a list of the strongly connected components (each a
  17.530 +   list of vertices). *)          
  17.531 +     
  17.532 +fun scc_term G =
  17.533 +     let
  17.534 +  (* Ordered list of the vertices that DFS has finished with;
  17.535 +     most recently finished goes at the head. *)
  17.536 +  val finish : term list ref = ref nil
  17.537 +
  17.538 +  (* List of vertices which have been visited. *)
  17.539 +  val visited : term list ref = ref nil
  17.540 +  
  17.541 +  fun been_visited v = exists (fn w => w aconv v) (!visited)
  17.542 +  
  17.543 +  (* Given the adjacency list rep of a graph (a list of pairs),
  17.544 +     return just the first element of each pair, yielding the 
  17.545 +     vertex list. *)
  17.546 +  val members = map (fn (v,_) => v)
  17.547 +
  17.548 +  (* Returns the nodes in the DFS tree rooted at u in g *)
  17.549 +  fun dfs_visit g u : term list =
  17.550 +      let
  17.551 +   val _ = visited := u :: !visited
  17.552 +   val descendents =
  17.553 +       foldr (fn (v,ds) => if been_visited v then ds
  17.554 +            else v :: dfs_visit g v @ ds)
  17.555 +        ((adjacent_term g u) ,nil)
  17.556 +      in
  17.557 +   finish := u :: !finish;
  17.558 +   descendents
  17.559 +      end
  17.560 +     in
  17.561 +
  17.562 +  (* DFS on the graph; apply dfs_visit to each vertex in
  17.563 +     the graph, checking first to make sure the vertex is
  17.564 +     as yet unvisited. *)
  17.565 +  app (fn u => if been_visited u then ()
  17.566 +        else (dfs_visit G u; ()))  (members G);
  17.567 +  visited := nil;
  17.568 +
  17.569 +  (* We don't reset finish because its value is used by
  17.570 +     revfold below, and it will never be used again (even
  17.571 +     though dfs_visit will continue to modify it). *)
  17.572 +
  17.573 +  (* DFS on the transpose. The vertices returned by
  17.574 +     dfs_visit along with u form a connected component. We
  17.575 +     collect all the connected components together in a
  17.576 +     list, which is what is returned. *)
  17.577 +  foldl (fn (comps,u) =>  
  17.578 +      if been_visited u then comps
  17.579 +      else ((u :: dfs_visit (transpose_term G) u) :: comps))  (nil,(!finish))
  17.580 +end;
  17.581 +
  17.582 +
  17.583 +(* *********************************************************************** *)
  17.584 +(*                                                                         *)
  17.585 +(* dfs_int_reachable g u:                                                  *)
  17.586 +(* (int * int list) list -> int -> int list                                *) 
  17.587 +(*                                                                         *)
  17.588 +(* Computes list of all nodes reachable from u in g.                       *)
  17.589 +(*                                                                         *)
  17.590 +(* *********************************************************************** *)
  17.591 +
  17.592 +
  17.593 +fun dfs_int_reachable g u = 
  17.594 + let
  17.595 +  (* List of vertices which have been visited. *)
  17.596 +  val visited : int list ref = ref nil
  17.597 +  
  17.598 +  fun been_visited v = exists (fn w => w = v) (!visited)
  17.599 +
  17.600 +  fun dfs_visit g u : int list =
  17.601 +      let
  17.602 +   val _ = visited := u :: !visited
  17.603 +   val descendents =
  17.604 +       foldr (fn (v,ds) => if been_visited v then ds
  17.605 +            else v :: dfs_visit g v @ ds)
  17.606 +        ( ((adjacent g u)) ,nil)
  17.607 +   in  descendents end
  17.608 + 
  17.609 + in u :: dfs_visit g u end;
  17.610 +
  17.611 +    
  17.612 +fun indexComps components = 
  17.613 +    ListPair.map (fn (a,b) => (b,a)) (components, 0 upto (length components -1));
  17.614 +
  17.615 +fun indexNodes IndexComp = 
  17.616 +    flat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
  17.617 +    
  17.618 +fun getIndex v [] = ~1
  17.619 +|   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
  17.620 +    
  17.621 +
  17.622 +(* ***************************************************************** *)
  17.623 +(*                                                                   *)
  17.624 +(* evalcompgraph components g ntc :                                  *)
  17.625 +(* Term.term list list ->                                            *)
  17.626 +(* (Term.term * (Term.term * less) list) list ->                     *)
  17.627 +(* (Term.term * int) list ->  (int * (int * less) list) list         *)
  17.628 +(*                                                                   *)
  17.629 +(*                                                                   *)
  17.630 +(* Computes, from graph g, list of all its components and the list   *)
  17.631 +(* ntc (nodes, index of component) a graph whose nodes are the       *)
  17.632 +(* indices of the components of g.  Egdes of the new graph are       *)
  17.633 +(* only the edges of g linking two components.                       *)
  17.634 +(*                                                                   *)
  17.635 +(* ***************************************************************** *)
  17.636 +
  17.637 +fun evalcompgraph components g ntc = 
  17.638 +    let
  17.639 +    (* Liste (Index der Komponente, Komponente *)
  17.640 +    val IndexComp = indexComps components;
  17.641 +
  17.642 +    (* Compute new graph with the property that it only contains edges
  17.643 +       between components. *)
  17.644 +  
  17.645 +    (* k is index of current start component. *)   
  17.646 +       
  17.647 +    fun processComponent (k, comp) = 
  17.648 +     let
  17.649 +         (* all edges pointing away from the component *)
  17.650 +	   (* (Term.term * less) list *)
  17.651 +	       val allEdges = flat (map (adjacent_term g) comp);
  17.652 +
  17.653 +		(* choose those edges pointing to nodes outside
  17.654 +                   the current component *)
  17.655 +		
  17.656 +		fun selectEdges  [] = []
  17.657 +		|   selectEdges  ((v,l)::es) = let val k' = getIndex v ntc in 
  17.658 +		    if k' = k then selectEdges es else (k', l) :: (selectEdges  es) end;
  17.659 +
  17.660 +		 (* Insert edge into sorted list of edges, where edge is
  17.661 +                    only added if
  17.662 +                    - it is found for the first time
  17.663 +                    - it is a <= edge and no parallel < edge was found earlier
  17.664 +                    - it is a < edge
  17.665 +                 *)
  17.666 +		     
  17.667 +		 fun insert (h,l) [] = [(h,l)]
  17.668 +		 |   insert (h,l) ((k',l')::es) = if h = k' then (
  17.669 +		     case l of (Less (_, _, _)) => (h,l)::es
  17.670 +		     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
  17.671 +	                      | _ => (k',l)::es) )
  17.672 +		     else (k',l'):: insert (h,l) es;
  17.673 +
  17.674 +		 (* Reorganise list of edges such that
  17.675 +                    - duplicate edges are removed
  17.676 +                    - if a < edge and a <= edge exist at the same time,
  17.677 +                      remove <= edge *)
  17.678 +		     
  17.679 +		 fun sortEdges [] sorted = sorted: (int * less) list
  17.680 +		 |   sortEdges (e::es) sorted = sortEdges es (insert e sorted); 
  17.681 +		    
  17.682 +     in 
  17.683 +       (k, (sortEdges (selectEdges allEdges) []))
  17.684 +     end; 
  17.685 +     
  17.686 +	     			       
  17.687 +in map processComponent IndexComp end; 
  17.688 +
  17.689 +(* Remove ``less'' edge info from graph *)
  17.690 +(* type ('a * ('a * less) list) list *)
  17.691 +fun stripOffLess g = map (fn (v, desc) => (v,map (fn (u,l) => u) desc)) g;
  17.692 +
  17.693 +
  17.694 +
  17.695 +(* *********************************************************************** *)
  17.696 +(*                                                                         *)
  17.697 +(* dfs_term g u v:                                                         *)
  17.698 +(* (Term.term  *(Term.term * less) list) list ->                           *)
  17.699 +(* Term.term -> Term.term -> (bool * less list)                            *) 
  17.700 +(*                                                                         *)
  17.701 +(* Depth first search of v from u.                                         *)
  17.702 +(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
  17.703 +(*                                                                         *)
  17.704 +(* *********************************************************************** *)
  17.705 +
  17.706 +
  17.707 +fun dfs_term g u v = 
  17.708 + let 
  17.709 +(* TODO: this comment is unclear *)
  17.710 +    (* Liste der gegangenen Kanten, 
  17.711 +       die Kante e die zum Vorgaenger eines Knoten u gehoert ist jene 
  17.712 +       für die gilt (upper e) = u *)
  17.713 +    val pred :  less list ref = ref nil;
  17.714 +    val visited: term list ref = ref nil;
  17.715 +    
  17.716 +    fun been_visited v = exists (fn w => w aconv v) (!visited)
  17.717 +    
  17.718 +    fun dfs_visit u' = 
  17.719 +    let val _ = visited := u' :: (!visited)
  17.720 +    
  17.721 +    fun update l = let val _ = pred := l ::(!pred) in () end;
  17.722 +    
  17.723 +    in if been_visited v then () 
  17.724 +       else (app (fn (v',l) => if been_visited v' then () else (
  17.725 +        update l; 
  17.726 +        dfs_visit v'; ()) )) (adjacent_term g u')
  17.727 +    end
  17.728 +   
  17.729 +  in 
  17.730 +    dfs_visit u; 
  17.731 +    if (been_visited v) then (true, (!pred)) else (false , [])   
  17.732 +  end;
  17.733 +
  17.734 +  
  17.735 +(* *********************************************************************** *)
  17.736 +(*                                                                         *)
  17.737 +(* completeTermPath u v g:                                                 *)
  17.738 +(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *) 
  17.739 +(* -> less list                                                            *)
  17.740 +(*                                                                         *)
  17.741 +(* Complete the path from u to v in graph g.  Path search is performed     *)
  17.742 +(* with dfs_term g u v.  This yields for each node v' its predecessor u'   *)
  17.743 +(* and the edge u' -> v'.  Allows traversing graph backwards from v and    *)
  17.744 +(* finding the path u -> v.                                                *)
  17.745 +(*                                                                         *)
  17.746 +(* *********************************************************************** *)
  17.747 +
  17.748 +  
  17.749 +fun completeTermPath u v g = 
  17.750 +  let 
  17.751 +   
  17.752 +   val (found, pred) = dfs_term g u v;
  17.753 +
  17.754 +   fun path x y  =
  17.755 +      let
  17.756 + 
  17.757 +      (* find predecessor u of node v and the edge u -> v *)
  17.758 +
  17.759 +      fun lookup v [] = raise Cannot
  17.760 +      |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
  17.761 +
  17.762 +      (* traverse path backwards and return list of visited edges *)   
  17.763 +      fun rev_path v = 
  17.764 +       let val l = lookup v pred
  17.765 +           val u = lower l;
  17.766 +       in
  17.767 +        if u aconv x then [l]
  17.768 +        else (rev_path u) @ [l] 
  17.769 +       end
  17.770 +     in rev_path y end;
  17.771 +       
  17.772 +  in 
  17.773 +  if found then (if u aconv v then [(Le (u, v, (Thm ([], Less.le_refl))))]
  17.774 +  else path u v ) else raise Cannot
  17.775 +end;  
  17.776 +
  17.777 +
  17.778 +(* *********************************************************************** *)
  17.779 +(*                                                                         *)
  17.780 +(* dfs_int g u v:                                                          *)
  17.781 +(* (int  *(int * less) list) list -> int -> int                            *)
  17.782 +(* -> (bool *(int*  less) list)                                            *) 
  17.783 +(*                                                                         *)
  17.784 +(* Depth first search of v from u.                                         *)
  17.785 +(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
  17.786 +(*                                                                         *)
  17.787 +(* *********************************************************************** *)
  17.788 +
  17.789 +fun dfs_int g u v = 
  17.790 + let 
  17.791 +    val pred : (int * less ) list ref = ref nil;
  17.792 +    val visited: int list ref = ref nil;
  17.793 +    
  17.794 +    fun been_visited v = exists (fn w => w = v) (!visited)
  17.795 +    
  17.796 +    fun dfs_visit u' = 
  17.797 +    let val _ = visited := u' :: (!visited)
  17.798 +    
  17.799 +    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
  17.800 +    
  17.801 +    in if been_visited v then () 
  17.802 +    else (app (fn (v',l) => if been_visited v' then () else (
  17.803 +       update (v',l); 
  17.804 +       dfs_visit v'; ()) )) (adjacent g u')
  17.805 +    
  17.806 +    end
  17.807 +   
  17.808 +  in 
  17.809 +    dfs_visit u; 
  17.810 +    if (been_visited v) then (true, (!pred)) else (false , [])   
  17.811 +  end;
  17.812 +  
  17.813 +     
  17.814 +(* *********************************************************************** *)
  17.815 +(*                                                                         *)
  17.816 +(* findProof (g2,  cg2, neqEdges, components, ntc) subgoal:                *)
  17.817 +(* (Term.term * (Term.term * less) list) list *                            *)
  17.818 +(* (int * (int * less) list) list * less list *  Term.term list list       *)
  17.819 +(* * ( (Term.term * int) -> proof                                          *)
  17.820 +(*                                                                         *)
  17.821 +(* findProof constructs from graphs (g2, cg2) and neqEdges a proof for     *)
  17.822 +(* subgoal.  Raises exception Cannot if this is not possible.              *)
  17.823 +(*                                                                         *)
  17.824 +(* *********************************************************************** *)
  17.825 +     
  17.826 +fun findProof (g2, cg2, neqEdges, components, ntc ) subgoal =
  17.827 +let
  17.828 +   
  17.829 + (* complete path x y from component graph *)
  17.830 + fun completeComponentPath x y predlist = 
  17.831 +   let         
  17.832 +	  val xi = getIndex x ntc
  17.833 +	  val yi = getIndex y ntc 
  17.834 +	  
  17.835 +	  fun lookup k [] =  raise Cannot
  17.836 +	  |   lookup k ((h,l)::us) = if k = h then l else lookup k us;	  
  17.837 +	  
  17.838 +	  fun rev_completeComponentPath y' = 
  17.839 +	   let val edge = lookup (getIndex y' ntc) predlist
  17.840 +	       val u = lower edge
  17.841 +	       val v = upper edge
  17.842 +	   in
  17.843 +             if (getIndex u ntc) = xi then 
  17.844 +	       (completeTermPath x u g2)@[edge]@(completeTermPath v y' g2)
  17.845 +	     else (rev_completeComponentPath u)@[edge]@(completeTermPath v y' g2)
  17.846 +           end
  17.847 +   in  
  17.848 +      if x aconv y then 
  17.849 +        [(Le (x, y, (Thm ([], Less.le_refl))))]
  17.850 +      else ( if xi = yi then completeTermPath x y g2
  17.851 +             else rev_completeComponentPath y )  
  17.852 +   end;
  17.853 +
  17.854 +(* ******************************************************************* *) 
  17.855 +(* findLess e x y xi yi xreachable yreachable                          *)
  17.856 +(*                                                                     *)
  17.857 +(* Find a path from x through e to y, of weight <                      *)
  17.858 +(* ******************************************************************* *) 
  17.859 + 
  17.860 + fun findLess e x y xi yi Xreachable Yreachable = 
  17.861 +  let val u = lower e 
  17.862 +      val v = upper e
  17.863 +      val ui = getIndex u ntc
  17.864 +      val vi = getIndex v ntc
  17.865 +            
  17.866 +  in 
  17.867 +      if ui mem Xreachable andalso vi mem Xreachable andalso 
  17.868 +         ui mem Yreachable andalso vi mem Yreachable then (
  17.869 +       
  17.870 +  (case e of (Less (_, _, _)) =>  
  17.871 +       let
  17.872 +        val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc)
  17.873 +	    in 
  17.874 +	     if xufound then (
  17.875 +	      let 
  17.876 +	       val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi 
  17.877 +	      in 
  17.878 +	       if vyfound then (
  17.879 +	        let 
  17.880 +	         val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
  17.881 +	         val xyLesss = transPath (tl xypath, hd xypath)
  17.882 +	        in 
  17.883 +		 if xyLesss subsumes subgoal then Some (getprf xyLesss) 
  17.884 +                 else None
  17.885 +	       end)
  17.886 +	       else None
  17.887 +	      end)
  17.888 +	     else None
  17.889 +	    end
  17.890 +       |  _   => 
  17.891 +         let val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc)
  17.892 +             in 
  17.893 +	      if xufound then (
  17.894 +	       let 
  17.895 +	        val (uvfound, uvpred) = dfs_int cg2 (getIndex u ntc) (getIndex v ntc)
  17.896 +	       in
  17.897 +		if uvfound then (
  17.898 +		 let 
  17.899 +		  val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi
  17.900 +		 in 
  17.901 +		  if vyfound then (
  17.902 +		   let
  17.903 +		    val uvpath = completeComponentPath u v uvpred
  17.904 +		    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
  17.905 +		    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
  17.906 +		    val xyLesss = transPath (tl xypath, hd xypath)
  17.907 +		   in 
  17.908 +		    if xyLesss subsumes subgoal then Some (getprf xyLesss)
  17.909 +                    else None
  17.910 +		   end )
  17.911 +		  else None   
  17.912 +	         end)
  17.913 +		else None
  17.914 +	       end ) 
  17.915 +	      else None
  17.916 +	     end )
  17.917 +    ) else None
  17.918 +end;  
  17.919 +   
  17.920 +         
  17.921 +in
  17.922 +  (* looking for x <= y: any path from x to y is sufficient *)
  17.923 +  case subgoal of (Le (x, y, _)) => (
  17.924 +  
  17.925 +   let 
  17.926 +    val xi = getIndex x ntc
  17.927 +    val yi = getIndex y ntc
  17.928 +    (* sucht im Komponentengraphen einen Weg von der Komponente in der x liegt
  17.929 +       zu der in der y liegt *)
  17.930 +    val (found, pred) = dfs_int cg2 xi yi
  17.931 +   in 
  17.932 +    if found then (
  17.933 +       let val xypath = completeComponentPath x y pred 
  17.934 +           val xyLesss = transPath (tl xypath, hd xypath) 
  17.935 +       in  
  17.936 +	  (case xyLesss of
  17.937 +	    (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], Less.less_imp_le))  
  17.938 +				else raise Cannot
  17.939 +	     | _   => if xyLesss subsumes subgoal then (getprf xyLesss) 
  17.940 +	              else raise Cannot)
  17.941 +       end )
  17.942 +     else raise Cannot 
  17.943 +   end 
  17.944 +   
  17.945 +   )
  17.946 + (* looking for x < y: particular path required, which is not necessarily
  17.947 +    found by normal dfs *)
  17.948 + |   (Less (x, y, _)) => (
  17.949 +   let 
  17.950 +    val xi = getIndex x ntc
  17.951 +    val yi = getIndex y ntc
  17.952 +    val cg2' = stripOffLess cg2
  17.953 +    val cg2'_transpose = transpose cg2'
  17.954 +    (* alle von x aus erreichbaren Komponenten *)
  17.955 +    val xreachable = dfs_int_reachable cg2' xi
  17.956 +    (* all comonents reachable from y in the transposed graph cg2' *)
  17.957 +    val yreachable = dfs_int_reachable cg2'_transpose yi
  17.958 +    (* for all edges u ~= v or u < v check if they are part of path x < y *)
  17.959 +    fun processNeqEdges [] = raise Cannot 
  17.960 +    |   processNeqEdges (e::es) = 
  17.961 +      case  (findLess e x y xi yi xreachable yreachable) of (Some prf) => prf  
  17.962 +      | _ => processNeqEdges es
  17.963 +        
  17.964 +    in 
  17.965 +       processNeqEdges neqEdges 
  17.966 +    end
  17.967 + 
  17.968 + )
  17.969 +| (NotEq (x, y, _)) => (
  17.970 +  
  17.971 +  let val xi = getIndex x ntc 
  17.972 +        val yi = getIndex y ntc
  17.973 +	val cg2' = stripOffLess cg2
  17.974 +	val cg2'_transpose = transpose cg2'
  17.975 +        val xreachable = dfs_int_reachable cg2' xi
  17.976 +	val yreachable = dfs_int_reachable cg2'_transpose yi
  17.977 +	
  17.978 +	fun processNeqEdges [] = raise Cannot  
  17.979 +  	|   processNeqEdges (e::es) = (
  17.980 +	    let val u = lower e 
  17.981 +	        val v = upper e
  17.982 +		val ui = getIndex u ntc
  17.983 +		val vi = getIndex v ntc
  17.984 +		
  17.985 +	    in  
  17.986 +	        (* if x ~= y follows from edge e *)
  17.987 +	    	         if e subsumes subgoal then (
  17.988 +		     case e of (Less (u, v, q)) => (
  17.989 +		       if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq))
  17.990 +		       else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym"))
  17.991 +		     )
  17.992 +		     |    (NotEq (u,v, q)) => (
  17.993 +		       if u aconv x andalso v aconv y then q
  17.994 +		       else (Thm ([q],  thm "not_sym"))
  17.995 +		     )
  17.996 +		 )
  17.997 +                (* if SCC_x is linked to SCC_y via edge e *)
  17.998 +		 else if ui = xi andalso vi = yi then (
  17.999 +                   case e of (Less (_, _,_)) => (
 17.1000 +		        let val xypath = (completeTermPath x u g2) @ [e] @ (completeTermPath v y g2)
 17.1001 +			    val xyLesss = transPath (tl xypath, hd xypath)
 17.1002 +			in  (Thm ([getprf xyLesss], Less.less_imp_neq)) end)
 17.1003 +		   | _ => (   
 17.1004 +		        let val xupath = completeTermPath x u g2
 17.1005 +			    val uxpath = completeTermPath u x g2
 17.1006 +			    val vypath = completeTermPath v y g2
 17.1007 +			    val yvpath = completeTermPath y v g2
 17.1008 +			    val xuLesss = transPath (tl xupath, hd xupath)     
 17.1009 +			    val uxLesss = transPath (tl uxpath, hd uxpath)			    
 17.1010 +			    val vyLesss = transPath (tl vypath, hd vypath)			
 17.1011 +			    val yvLesss = transPath (tl yvpath, hd yvpath)
 17.1012 +			    val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], Less.eqI))
 17.1013 +			    val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], Less.eqI))
 17.1014 +			in 
 17.1015 +                           (Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq)) 
 17.1016 +			end
 17.1017 +			)       
 17.1018 +		  ) else if ui = yi andalso vi = xi then (
 17.1019 +		     case e of (Less (_, _,_)) => (
 17.1020 +		        let val xypath = (completeTermPath y u g2) @ [e] @ (completeTermPath v x g2)
 17.1021 +			    val xyLesss = transPath (tl xypath, hd xypath)
 17.1022 +			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) 
 17.1023 +		     | _ => (
 17.1024 +		        
 17.1025 +			let val yupath = completeTermPath y u g2
 17.1026 +			    val uypath = completeTermPath u y g2
 17.1027 +			    val vxpath = completeTermPath v x g2
 17.1028 +			    val xvpath = completeTermPath x v g2
 17.1029 +			    val yuLesss = transPath (tl yupath, hd yupath)     
 17.1030 +			    val uyLesss = transPath (tl uypath, hd uypath)			    
 17.1031 +			    val vxLesss = transPath (tl vxpath, hd vxpath)			
 17.1032 +			    val xvLesss = transPath (tl xvpath, hd xvpath)
 17.1033 +			    val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI))
 17.1034 +			    val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI))
 17.1035 +			in
 17.1036 +			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym"))
 17.1037 +		        end
 17.1038 +		       )
 17.1039 +		  ) else (
 17.1040 +                       (* there exists a path x < y or y < x such that
 17.1041 +                          x ~= y may be concluded *)
 17.1042 +	        	case  (findLess e x y xi yi xreachable yreachable) of 
 17.1043 +		              (Some prf) =>  (Thm ([prf], Less.less_imp_neq))  
 17.1044 +                             | None =>  (
 17.1045 +		               let 
 17.1046 +		                val yr = dfs_int_reachable cg2' yi
 17.1047 +	                        val xr = dfs_int_reachable cg2'_transpose xi
 17.1048 +		               in 
 17.1049 +		                case  (findLess e y x yi xi yr xr) of 
 17.1050 +		                      (Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) 
 17.1051 +                                      | _ => processNeqEdges es
 17.1052 +		               end)
 17.1053 +		 ) end) 
 17.1054 +     in processNeqEdges neqEdges end
 17.1055 +  )    
 17.1056 +end;
 17.1057 +
 17.1058 +
 17.1059 +(* *********************************************************************** *)
 17.1060 +(*                                                                         *)
 17.1061 +(* checkComponents g components ntc neqEdges:                              *)
 17.1062 +(* (Term.term * (Term.term * less) list) list -> Term.term list list  ->   *)
 17.1063 +(* (Term.term * int) -> less list -> bool                                  *)
 17.1064 +(*                                                                         *)
 17.1065 +(* For each edge in the list neqEdges check if it leads to a contradiction.*)
 17.1066 +(* We have a contradiction for edge u ~= v and u < v if:                   *)
 17.1067 +(* - u and v are in the same component,                                    *)
 17.1068 +(*   that is, a path u <= v and a path v <= u exist, hence u = v.          *)
 17.1069 +(* From irreflexivity of < follows u < u or v < v.  Ex false quodlibet.    *)
 17.1070 +(*                                                                         *)
 17.1071 +(*                                                                         *)
 17.1072 +(* *********************************************************************** *)
 17.1073 +
 17.1074 +
 17.1075 +fun checkComponents g components ntc neqEdges = 
 17.1076 + let
 17.1077 +    (* Construct proof by contradiction for edge *)
 17.1078 +    fun handleContr edge  = 
 17.1079 +       (case edge of 
 17.1080 +          (Less  (x, y, _)) => (
 17.1081 +	    let 
 17.1082 +	     val xxpath = edge :: (completeTermPath y x g)
 17.1083 +	     val xxLesss = transPath (tl xxpath, hd xxpath)
 17.1084 +	     val q = getprf xxLesss
 17.1085 +	    in 
 17.1086 +	     raise (Contr (Thm ([q], Less.less_reflE ))) 
 17.1087 +	    end 
 17.1088 +	  )
 17.1089 +        | (NotEq (x, y, _)) => (
 17.1090 +	    let 
 17.1091 +	     val xypath = (completeTermPath x y g)
 17.1092 +	     val yxpath = (completeTermPath y x g)
 17.1093 +	     val xyLesss = transPath (tl xypath, hd xypath)
 17.1094 +	     val yxLesss = transPath (tl yxpath, hd yxpath)
 17.1095 +             val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 
 17.1096 +	    in 
 17.1097 +	     raise (Contr (Thm ([q], Less.less_reflE )))
 17.1098 +	    end  
 17.1099 +	 )
 17.1100 +	| _ =>  error "trans_tac/checkCompoents/handleContr: invalid Contradiction");
 17.1101 +
 17.1102 +   (* Check each edge in neqEdges for contradiction.
 17.1103 +      If there is a contradiction, call handleContr, otherwise do nothing. *)
 17.1104 +    fun checkNeqEdges [] = () 
 17.1105 +    |   checkNeqEdges (e::es) = 
 17.1106 +        (case e of (Less (u, v, _)) => 
 17.1107 +	  if (getIndex u ntc) = (getIndex v ntc) then handleContr e g
 17.1108 +          else checkNeqEdges es
 17.1109 +        | (NotEq (u, v, _)) =>  
 17.1110 +	  if (getIndex u ntc) = (getIndex v ntc) then handleContr e g
 17.1111 +          else checkNeqEdges es
 17.1112 +        | _ => checkNeqEdges es)
 17.1113 +     
 17.1114 + in if g = [] then () else checkNeqEdges neqEdges end;
 17.1115 +
 17.1116 +(* *********************************************************************** *)
 17.1117 +(*                                                                         *)
 17.1118 +(* solvePartialOrder sign (asms,concl) :                                   *)
 17.1119 +(* Sign.sg -> less list * Term.term -> proof list                          *)
 17.1120 +(*                                                                         *)
 17.1121 +(* Find proof if possible for partial orders.                              *)
 17.1122 +(*                                                                         *)
 17.1123 +(* *********************************************************************** *)
 17.1124 +
 17.1125 +fun solvePartialOrder sign (asms, concl) =
 17.1126 + let 
 17.1127 +  val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[])
 17.1128 +  val components = scc_term g1
 17.1129 +  val ntc = indexNodes (indexComps components)
 17.1130 +  val cg2 = evalcompgraph components g2 ntc
 17.1131 + in
 17.1132 + (* Check for contradiction within assumptions  *)
 17.1133 +  checkComponents g2 components ntc neqEdges;
 17.1134 +  let 
 17.1135 +   val (subgoals, prf) = mkconcl_partial sign concl
 17.1136 +   fun solve facts less =
 17.1137 +       (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less
 17.1138 +       | Some prf => prf )
 17.1139 +  in
 17.1140 +   map (solve asms) subgoals
 17.1141 +  end
 17.1142 + end;
 17.1143 +
 17.1144 +(* *********************************************************************** *)
 17.1145 +(*                                                                         *)
 17.1146 +(* solveTotalOrder sign (asms,concl) :                                     *)
 17.1147 +(* Sign.sg -> less list * Term.term -> proof list                          *)
 17.1148 +(*                                                                         *)
 17.1149 +(* Find proof if possible for linear orders.                               *)
 17.1150 +(*                                                                         *)
 17.1151 +(* *********************************************************************** *)
 17.1152 +
 17.1153 +fun solveTotalOrder sign (asms, concl) =
 17.1154 + let 
 17.1155 +  val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[])
 17.1156 +  val components = scc_term g1   
 17.1157 +  val ntc = indexNodes (indexComps components)
 17.1158 +  val cg2 = evalcompgraph components g2 ntc
 17.1159 + in
 17.1160 +  checkComponents g2 components ntc neqEdges;
 17.1161 +  let 
 17.1162 +   val (subgoals, prf) = mkconcl_linear sign concl
 17.1163 +   fun solve facts less =
 17.1164 +      (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less
 17.1165 +      | Some prf => prf )
 17.1166 +  in
 17.1167 +   map (solve asms) subgoals
 17.1168 +  end
 17.1169 + end;
 17.1170 +
 17.1171 +  
 17.1172 +(* partial_tac - solves linear/total orders *)
 17.1173 +  
 17.1174 +val partial_tac = SUBGOAL (fn (A, n, sign) =>
 17.1175 + let
 17.1176 +  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
 17.1177 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
 17.1178 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
 17.1179 +  val lesss = flat (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs - 1)))
 17.1180 +  val prfs = solvePartialOrder sign (lesss, C);
 17.1181 +  val (subgoals, prf) = mkconcl_partial sign C;
 17.1182 + in
 17.1183 +  METAHYPS (fn asms =>
 17.1184 +    let val thms = map (prove asms) prfs
 17.1185 +    in rtac (prove thms prf) 1 end) n
 17.1186 + end
 17.1187 + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
 17.1188 +      | Cannot  => no_tac
 17.1189 +      );
 17.1190 +       
 17.1191 +(* linear_tac - solves linear/total orders *)
 17.1192 +  
 17.1193 +val linear_tac = SUBGOAL (fn (A, n, sign) =>
 17.1194 + let
 17.1195 +  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
 17.1196 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
 17.1197 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
 17.1198 +  val lesss = flat (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs - 1)))
 17.1199 +  val prfs = solveTotalOrder sign (lesss, C);
 17.1200 +  val (subgoals, prf) = mkconcl_linear sign C;
 17.1201 + in
 17.1202 +  METAHYPS (fn asms =>
 17.1203 +    let val thms = map (prove asms) prfs
 17.1204 +    in rtac (prove thms prf) 1 end) n
 17.1205 + end
 17.1206 + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
 17.1207 +      | Cannot  => no_tac);
 17.1208 +       
 17.1209 +end;
 17.1210 +