# HG changeset patch
# User webertj
# Date 1154352576 -7200
# Node ID 1fe9aed8fcaca07f92dd3335673cf8647d44e5f9
# Parent  1154363129be7d2f9b55683a1f4b954297aaec9d
code reformatted

diff -r 1154363129be -r 1fe9aed8fcac src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Jul 31 14:08:42 2006 +0200
+++ b/src/HOL/arith_data.ML	Mon Jul 31 15:29:36 2006 +0200
@@ -141,15 +141,19 @@
 
 val nat_cancel_sums_add = map prep_simproc
   [("nateq_cancel_sums",
-     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], K EqCancelSums.proc),
+     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
+     K EqCancelSums.proc),
    ("natless_cancel_sums",
-     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], K LessCancelSums.proc),
+     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
+     K LessCancelSums.proc),
    ("natle_cancel_sums",
-     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], K LeCancelSums.proc)];
+     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
+     K LeCancelSums.proc)];
 
 val nat_cancel_sums = nat_cancel_sums_add @
   [prep_simproc ("natdiff_cancel_sums",
-    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], K DiffCancelSums.proc)];
+    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
+    K DiffCancelSums.proc)];
 
 end;  (* ArithData *)
 
@@ -202,8 +206,10 @@
 structure ArithTheoryData = TheoryDataFun
 (struct
   val name = "HOL/arith";
-  type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string  list, presburger: (int -> tactic) option};
-
+  type T = {splits: thm list,
+            inj_consts: (string * typ) list,
+            discrete: string list,
+            presburger: (int -> tactic) option};
   val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE};
   val copy = I;
   val extend = I;
@@ -241,8 +247,6 @@
 
 (* Decomposition of terms *)
 
-(* typ -> bool *)
-
 fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT)
   | nT _                      = false;
 
@@ -274,9 +278,7 @@
    their coefficients
 *)
 
-(* (string * Term.typ) list -> ... *)
-
-fun demult inj_consts =
+fun demult (inj_consts : (string * Term.typ) list) =
 let
   fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
       (case s of
@@ -292,29 +294,34 @@
           let
             val den = HOLogic.dest_binum dent
           in
-            if den = 0 then  raise Zero  else  demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
+            if den = 0 then
+              raise Zero
+            else
+              demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
           end
       | _ =>
           atomult (mC, s, t, m)
       ) handle TERM _ => atomult (mC, s, t, m)
     )
-    | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) = (
-      let
+    | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
+      (let
         val den = HOLogic.dest_binum dent
       in
-        if den = 0 then  raise Zero  else  demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
+        if den = 0 then
+          raise Zero
+        else
+          demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
       end
-        handle TERM _ => (SOME atom, m)
-    )
-    | demult(Const("0",_),m) = (NONE, Rat.rat_of_int 0)
-    | demult(Const("1",_),m) = (NONE, m)
-    | demult(t as Const("Numeral.number_of",_)$n,m) =
-        ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
-         handle TERM _ => (SOME t,m))
-    | demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
-    | demult(t as Const f $ x, m) =
-        (if f mem inj_consts then SOME x else SOME t,m)
-    | demult(atom,m) = (SOME atom,m)
+        handle TERM _ => (SOME atom, m))
+    | demult (Const ("0", _), m) = (NONE, Rat.rat_of_int 0)
+    | demult (Const ("1", _), m) = (NONE, m)
+    | demult (t as Const ("Numeral.number_of", _) $ n, m) =
+        ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
+          handle TERM _ => (SOME t,m))
+    | demult (Const ("HOL.uminus", _) $ t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
+    | demult (t as Const f $ x, m) =
+        (if f mem inj_consts then SOME x else SOME t, m)
+    | demult (atom, m) = (SOME atom, m)
 and
   atomult (mC, atom, t, m) = (
     case demult (t, m) of (NONE, m')    => (SOME atom, m')
@@ -412,24 +419,31 @@
 
 val fast_arith_split_limit = ref 9;
 
-(* checks whether splitting with 'thm' is implemented                        *)
-
-(* Thm.thm -> bool *)
+(* checks if splitting with 'thm' is implemented                             *)
 
-fun is_split_thm thm =
-  case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) =>  (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
-    (case head_of lhs of
-      Const (a, _) => a mem_string ["Orderings.max", "Orderings.min", "HOL.abs", "HOL.minus", "IntDef.nat", "Divides.op mod", "Divides.op div"]
-    | _            => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false))
-  | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false);
+fun is_split_thm (thm : thm) : bool =
+  case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
+    (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
+    case head_of lhs of
+      Const (a, _) => a mem_string ["Orderings.max",
+                                    "Orderings.min",
+                                    "HOL.abs",
+                                    "HOL.minus",
+                                    "IntDef.nat",
+                                    "Divides.op mod",
+                                    "Divides.op div"]
+    | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
+                                 Display.string_of_thm thm);
+                       false))
+  | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
+                   Display.string_of_thm thm);
+          false);
 
 (* substitute new for occurrences of old in a term, incrementing bound       *)
 (* variables as needed when substituting inside an abstraction               *)
 
-(* (term * term) list -> term -> term *)
-
-fun subst_term []    t = t
-  | subst_term pairs t =
+fun subst_term ([] : (term * term) list) (t : term) = t
+  | subst_term pairs                     t          =
       (case AList.lookup (op aconv) pairs t of
         SOME new =>
           new
@@ -447,14 +461,17 @@
 (* variables and a term list for premises), or NONE if split_tac would fail  *)
 (* on the subgoal                                                            *)
 
-(* theory -> typ list * term list -> (typ list * term list) list option *)
-
 (* FIXME: currently only the effect of certain split theorems is reproduced  *)
 (*        (which is why we need 'is_split_thm').  A more canonical           *)
 (*        implementation should analyze the right-hand side of the split     *)
 (*        theorem that can be applied, and modify the subgoal accordingly.   *)
+(*        Or even better, the splitter should be extended to provide         *)
+(*        splitting on terms as well as splitting on theorems (where the     *)
+(*        former can have a faster implementation as it does not need to be  *)
+(*        proof-producing).                                                  *)
 
-fun split_once_items sg (Ts, terms) =
+fun split_once_items (sg : theory) (Ts : typ list, terms : term list) :
+                     (typ list * term list) list option =
 let
   (* takes a list  [t1, ..., tn]  to the term                                *)
   (*   tn' --> ... --> t1' --> False  ,                                      *)
@@ -467,12 +484,15 @@
   val splits     = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
 in
   if length splits > !fast_arith_split_limit then (
-    tracing ("fast_arith_split_limit exceeded (current value is " ^ string_of_int (!fast_arith_split_limit) ^ ")");
+    tracing ("fast_arith_split_limit exceeded (current value is " ^
+              string_of_int (!fast_arith_split_limit) ^ ")");
     NONE
   ) else (
   case splits of [] =>
-    NONE  (* split_tac would fail: no possible split *)
-  | ((_, _, _, split_type, split_term) :: _) => (  (* ignore all but the first possible split *)
+    (* split_tac would fail: no possible split *)
+    NONE
+  | ((_, _, _, split_type, split_term) :: _) => (
+    (* ignore all but the first possible split *)
     case strip_comb split_term of
     (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
       (Const ("Orderings.max", _), [t1, t2]) =>
@@ -480,7 +500,8 @@
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+        val t1_leq_t2     = Const ("Orderings.less_eq",
+                                    split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
@@ -494,7 +515,8 @@
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+        val t1_leq_t2     = Const ("Orderings.less_eq",
+                                    split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
@@ -505,15 +527,18 @@
     (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
     | (Const ("HOL.abs", _), [t1]) =>
       let
-        val rev_terms     = rev terms
-        val terms1        = map (subst_term [(split_term, t1)]) rev_terms
-        val terms2        = map (subst_term [(split_term, Const ("HOL.uminus", split_type --> split_type) $ t1)]) rev_terms
-        val zero          = Const ("0", split_type)
-        val zero_leq_t1   = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ t1
-        val t1_lt_zero    = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
-        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
-        val subgoal1      = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
-        val subgoal2      = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
+        val rev_terms   = rev terms
+        val terms1      = map (subst_term [(split_term, t1)]) rev_terms
+        val terms2      = map (subst_term [(split_term, Const ("HOL.uminus",
+                            split_type --> split_type) $ t1)]) rev_terms
+        val zero        = Const ("0", split_type)
+        val zero_leq_t1 = Const ("Orderings.less_eq",
+                            split_type --> split_type --> HOLogic.boolT) $ zero $ t1
+        val t1_lt_zero  = Const ("Orderings.less",
+                            split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
+        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
+        val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
       in
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
@@ -526,11 +551,15 @@
         val zero            = Const ("0", split_type)
         val d               = Bound 0
         val terms1          = map (subst_term [(split_term, zero)]) rev_terms
-        val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms)
+        val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
+                                (map (incr_boundvars 1) rev_terms)
         val t1'             = incr_boundvars 1 t1
         val t2'             = incr_boundvars 1 t2
-        val t1_lt_t2        = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
-        val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const ("HOL.plus", split_type --> split_type --> split_type) $ t2' $ d)
+        val t1_lt_t2        = Const ("Orderings.less",
+                                split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+        val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+                                (Const ("HOL.plus",
+                                  split_type --> split_type --> split_type) $ t2' $ d)
         val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
         val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
@@ -544,18 +573,23 @@
         val zero_int    = Const ("0", HOLogic.intT)
         val zero_nat    = Const ("0", HOLogic.natT)
         val n           = Bound 0
-        val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms)
+        val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
+                            (map (incr_boundvars 1) rev_terms)
         val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
         val t1'         = incr_boundvars 1 t1
-        val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
-        val t1_lt_zero  = Const ("Orderings.less", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
+        val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+                            (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
+        val t1_lt_zero  = Const ("Orderings.less",
+                            HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
       in
         SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
       end
-    (* "?P ((?n::nat) mod (number_of ?k)) = ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
+    (* "?P ((?n::nat) mod (number_of ?k)) =
+         ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
+           (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
     | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
@@ -563,22 +597,31 @@
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
-        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, j)])
+                                        (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
-        val t2_eq_zero              = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val t2_neq_zero             = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t2_eq_zero              = Const ("op =",
+                                        split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+        val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
+                                        split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+        val j_lt_t2                 = Const ("Orderings.less",
+                                        split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+                                         (Const ("HOL.times",
+                                           split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
-        val subgoal2                = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+        val subgoal2                = (map HOLogic.mk_Trueprop
+                                        [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
+                                          @ terms2 @ [not_false]
       in
         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
       end
-    (* "?P ((?n::nat) div (number_of ?k)) = ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
+    (* "?P ((?n::nat) div (number_of ?k)) =
+         ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
+           (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
     | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
@@ -586,45 +629,64 @@
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
-        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, i)])
+                                        (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
-        val t2_eq_zero              = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val t2_neq_zero             = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t2_eq_zero              = Const ("op =",
+                                        split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+        val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
+                                        split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+        val j_lt_t2                 = Const ("Orderings.less",
+                                        split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+                                         (Const ("HOL.times",
+                                           split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
-        val subgoal2                = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+        val subgoal2                = (map HOLogic.mk_Trueprop
+                                        [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
+                                          @ terms2 @ [not_false]
       in
         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
       end
-    (* "?P ((?n::int) mod (number_of ?k)) = ((iszero (number_of ?k) --> ?P ?n) &
-                                              (neg (number_of (bin_minus ?k)) --> (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
-                                              (neg (number_of ?k) --> (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
-    | (Const ("Divides.op mod", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+    (* "?P ((?n::int) mod (number_of ?k)) =
+         ((iszero (number_of ?k) --> ?P ?n) &
+          (neg (number_of (bin_minus ?k)) -->
+            (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
+          (neg (number_of ?k) -->
+            (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
+    | (Const ("Divides.op mod",
+        Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const ("0", split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
-        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)])
+                                        (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val (t2' as (_ $ k'))       = incr_boundvars 2 t2
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
-                                        (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
-        val zero_leq_j              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+                                        (number_of $
+                                          (Const ("Numeral.bin_minus",
+                                            HOLogic.binT --> HOLogic.binT) $ k'))
+        val zero_leq_j              = Const ("Orderings.less_eq",
+                                        split_type --> split_type --> HOLogic.boolT) $ zero $ j
+        val j_lt_t2                 = Const ("Orderings.less",
+                                        split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+                                         (Const ("HOL.times",
+                                           split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+        val t2_lt_j                 = Const ("Orderings.less",
+                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+        val j_leq_zero              = Const ("Orderings.less_eq",
+                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
@@ -641,61 +703,76 @@
       in
         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
       end
-    (* "?P ((?n::int) div (number_of ?k)) = ((iszero (number_of ?k) --> ?P 0) &
-                                              (neg (number_of (bin_minus ?k)) --> (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
-                                              (neg (number_of ?k) --> (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
-    | (Const ("Divides.op div", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+    (* "?P ((?n::int) div (number_of ?k)) =
+         ((iszero (number_of ?k) --> ?P 0) &
+          (neg (number_of (bin_minus ?k)) -->
+            (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
+          (neg (number_of ?k) -->
+            (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
+    | (Const ("Divides.op div",
+        Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const ("0", split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
-        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)])
+                                        (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val (t2' as (_ $ k'))       = incr_boundvars 2 t2
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
-                                        (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
-        val zero_leq_j              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
-        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+                                        (number_of $
+                                          (Const ("Numeral.bin_minus",
+                                            HOLogic.binT --> HOLogic.binT) $ k'))
+        val zero_leq_j              = Const ("Orderings.less_eq",
+                                        split_type --> split_type --> HOLogic.boolT) $ zero $ j
+        val j_lt_t2                 = Const ("Orderings.less",
+                                        split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t1_eq_t2_times_i_plus_j = Const ("op =",
+                                        split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+                                         (Const ("HOL.times",
+                                           split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+        val t2_lt_j                 = Const ("Orderings.less",
+                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+        val j_leq_zero              = Const ("Orderings.less_eq",
+                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
         val subgoal2                = (HOLogic.mk_Trueprop neg_minus_k)
                                         :: terms2_3
                                         @ not_false
-                                        :: (map HOLogic.mk_Trueprop [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
+                                        :: (map HOLogic.mk_Trueprop
+                                             [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
         val subgoal3                = (HOLogic.mk_Trueprop neg_t2)
                                         :: terms2_3
                                         @ not_false
-                                        :: (map HOLogic.mk_Trueprop [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
+                                        :: (map HOLogic.mk_Trueprop
+                                             [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
         val Ts'                     = split_type :: split_type :: Ts
       in
         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
       end
-    (* this will only happen if a split theorem can be applied for which no code exists above -- *)
-    (* in which case either the split theorem should be implemented above, or 'is_split_thm'     *)
-    (* should be modified to filter it out                                                       *)
+    (* this will only happen if a split theorem can be applied for which no  *)
+    (* code exists above -- in which case either the split theorem should be *)
+    (* implemented above, or 'is_split_thm' should be modified to filter it  *)
+    (* out                                                                   *)
     | (t, ts) => (
-      warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ " (with " ^ Int.toString (length ts) ^
+      warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^
+               " (with " ^ Int.toString (length ts) ^
                " argument(s)) not implemented; proof reconstruction is likely to fail");
       NONE
     ))
   )
 end;
 
-(* remove terms that do not satisfy p; change the order of the remaining     *)
+(* remove terms that do not satisfy 'p'; change the order of the remaining   *)
 (* terms in the same way as filter_prems_tac does                            *)
 
-(* (term -> bool) -> term list -> term list *)
-
-fun filter_prems_tac_items p terms =
+fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
 let
   fun filter_prems (t, (left, right)) =
     if  p t  then  (left, right @ [t])  else  (left @ right, [])
@@ -707,29 +784,31 @@
 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)
 (* subgoal that has 'terms' as premises                                      *)
 
-(* term list -> bool *)
+fun negated_term_occurs_positively (terms : term list) : bool =
+  List.exists
+    (fn (Trueprop $ (Const ("Not", _) $ t)) => member (op aconv) terms (Trueprop $ t)
+      | _                                   => false)
+    terms;
 
-fun negated_term_occurs_positively terms =
-  List.exists (fn (TP $ (Const ("Not", _) $ t)) => member (op aconv) terms (TP $ t) | _ => false) terms;
-
-(* theory -> typ list * term list -> (typ list * term list) list *)
-
-fun pre_decomp sg (Ts, terms) =
+fun pre_decomp sg (Ts : typ list, terms : term list) : (typ list * term list) list =
 let
   (* repeatedly split (including newly emerging subgoals) until no further   *)
   (* splitting is possible                                                   *)
-  (* (typ list * term list) list -> (typ list * term list) list *)
-  fun split_loop [] = []
-    | split_loop (subgoal::subgoals) = (
+  fun split_loop ([] : (typ list * term list) list) = []
+    | split_loop (subgoal::subgoals)                = (
         case split_once_items sg subgoal of
           SOME new_subgoals => split_loop (new_subgoals @ subgoals)
         | NONE              => subgoal :: split_loop subgoals
       )
   fun is_relevant t  = isSome (decomp sg t)
-  val relevant_terms = filter_prems_tac_items is_relevant terms                                (* filter_prems_tac is_relevant *)
-  val split_goals    = split_loop [(Ts, relevant_terms)]                                       (* split_tac, NNF normalization *)
-  val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals    (* necessary because split_once_tac may normalize terms *)
-  val result         = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm  (* TRY (etac notE) THEN eq_assume_tac *)
+  (* filter_prems_tac is_relevant: *)
+  val relevant_terms = filter_prems_tac_items is_relevant terms
+  (* split_tac, NNF normalization: *)
+  val split_goals    = split_loop [(Ts, relevant_terms)]
+  (* necessary because split_once_tac may normalize terms: *)
+  val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals
+  (* TRY (etac notE) THEN eq_assume_tac: *)
+  val result         = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm
 in
   result
 end;
@@ -743,9 +822,7 @@
 (* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
 (* !fast_arith_split_limit splits are possible.                              *)
 
-(* Thm.thm list -> int -> Tactical.tactic *)
-
-fun split_once_tac split_thms i =
+fun split_once_tac (split_thms : thm list) (i : int) : tactic =
 let
   val nnf_simpset =
     empty_ss setmkeqTrue mk_eq_True
@@ -782,8 +859,6 @@
 (* subgoals and finally attempt to solve them by finding an immediate        *)
 (* contradiction (i.e. a term and its negation) in their premises.           *)
 
-(* int -> Tactical.tactic *)
-
 fun pre_tac i st =
 let
   val sg            = theory_of_thm st
@@ -795,7 +870,9 @@
       THEN (
         (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
           THEN_ALL_NEW
-            ((fn j => PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
+            ((fn j => PRIMITIVE
+                        (Drule.fconv_rule
+                          (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
               THEN'
             (TRY o (etac notE THEN' eq_assume_tac)))
       ) i
@@ -893,7 +970,8 @@
   refute_tac (K true)
     (* Splitting is also done inside fast_arith_tac, but not completely --   *)
     (* split_tac may use split theorems that have not been implemented in    *)
-    (* fast_arith_tac (cf. pre_decomp and split_once_items above).           *)
+    (* fast_arith_tac (cf. pre_decomp and split_once_items above), and       *)
+    (* fast_arith_split_limit may trigger.                                   *)
     (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
     (* some goals that fast_arith_tac alone would fail on.                   *)
     (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
diff -r 1154363129be -r 1fe9aed8fcac src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Jul 31 14:08:42 2006 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Jul 31 15:29:36 2006 +0200
@@ -52,10 +52,13 @@
 
 signature LIN_ARITH_DATA =
 sig
-  type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool  (* internal representation of linear (in-)equations *)
+  (* internal representation of linear (in-)equations: *)
+  type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool
   val decomp: theory -> term -> decompT option
-  val pre_decomp: theory -> typ list * term list -> (typ list * term list) list  (* preprocessing, performed on a representation of subgoals as list of premises *)
-  val pre_tac   : int -> Tactical.tactic                                         (* preprocessing, performed on the goal -- must do the same as 'pre_decomp' *)
+  (* preprocessing, performed on a representation of subgoals as list of premises: *)
+  val pre_decomp: theory -> typ list * term list -> (typ list * term list) list
+  (* preprocessing, performed on the goal -- must do the same as 'pre_decomp': *)
+  val pre_tac   : int -> Tactical.tactic
   val number_of: IntInf.int * typ -> term
 end;
 (*
@@ -400,12 +403,10 @@
 (* Translate back a proof.                                                   *)
 (* ------------------------------------------------------------------------- *)
 
-(* string -> Thm.thm -> Thm.thm *)
-fun trace_thm msg th =
+fun trace_thm (msg : string) (th : thm) : thm =
     (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
 
-(* string -> unit *)
-fun trace_msg msg =
+fun trace_msg (msg : string) : unit =
     if !trace then tracing msg else ();
 
 (* FIXME OPTIMIZE!!!! (partly done already)
@@ -420,8 +421,7 @@
 local
  exception FalseE of thm
 in
-(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> injust -> Thm.thm *)
-fun mkthm (sg, ss) asms just =
+fun mkthm (sg:theory, ss:simpset) (asms:thm list) (just:injust) : thm =
   let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
           Data.get sg;
       val simpset' = Simplifier.inherit_context ss simpset;
@@ -495,8 +495,7 @@
 fun coeff poly atom : IntInf.int =
   AList.lookup (op =) poly atom |> the_default 0;
 
-(* int list -> int *)
-fun lcms is = Library.foldl lcm (1, is);
+fun lcms (is:int list) : int = Library.foldl lcm (1, is);
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
@@ -563,9 +562,7 @@
 
 (* ------------------------------------------------------------------------- *)
 
-(* Term.typ list -> int list -> Term.term * int -> lineq option *)
-
-fun mknat pTs ixs (atom, i) =
+fun mknat (pTs : typ list) (ixs : int list) (atom : term, i : int) : lineq option =
   if LA_Logic.is_nat (pTs, atom)
   then let val l = map (fn j => if j=i then 1 else 0) ixs
        in SOME (Lineq (0, Le, l, Nat i)) end
@@ -590,9 +587,7 @@
 (*        failure as soon as a case could not be refuted; i.e. delay further *)
 (*        splitting until after a refutation for other cases has been found. *)
 
-(* Theory.theory -> typ list * term list -> (typ list * (decompT * int) list) list *)
-
-fun split_items sg (Ts, terms) =
+fun split_items sg (Ts : typ list, terms : term list) : (typ list * (LA_Data.decompT * int) list) list =
   let
 (*
       val _ = trace_msg ("split_items: Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
@@ -601,71 +596,61 @@
       (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
       (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic    *)
       (* level                                                          *)
-      (* decompT option list -> decompT option list list *)
       fun elim_neq []              = [[]]
         | elim_neq (NONE :: ineqs) = map (cons NONE) (elim_neq ineqs)
         | elim_neq (SOME(ineq as (l,i,rel,r,j,d)) :: ineqs) =
           if rel = "~=" then elim_neq (ineqs @ [SOME (l, i, "<", r, j, d)]) @
                              elim_neq (ineqs @ [SOME (r, j, "<", l, i, d)])
           else map (cons (SOME ineq)) (elim_neq ineqs)
-      (* int -> decompT option list -> (decompT * int) list *)
+
       fun number_hyps _ []             = []
         | number_hyps n (NONE::xs)     = number_hyps (n+1) xs
         | number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs
 
       val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *)
-                                  (* (typ list * term list) list *)
                                   LA_Data.pre_decomp sg
                                |> (* compute the internal encoding of (in-)equalities *)
-                                  (* (typ list * decompT option list) list *)
                                   map (apsnd (map (LA_Data.decomp sg)))
                                |> (* splitting of inequalities *)
-                                  (* (typ list * decompT option list) list list *)
                                   map (fn (Ts, items) => map (pair Ts) (elim_neq items))
                                |> (* combine the list of lists of subgoals into a single list *)
-                                  (* (typ list * decompT option list) list *)
                                   List.concat
                                |> (* numbering of hypotheses, ignoring irrelevant ones *)
-                                  (* (typ list * (decompT * int) list) list *)
                                   map (apsnd (number_hyps 0))
 (*
-      val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^ " subgoal(s)"
-                ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
-                        ("  " ^ Int.toString n ^ ". Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
-                         "    items = " ^ string_of_list
-                                            (string_of_pair
-                                              (fn (l, i, rel, r, j, d) =>
-                                                enclose "(" ")" (commas
-                                                  [string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
-                                                   Rat.string_of_rat i,
-                                                   rel,
-                                                   string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
-                                                   Rat.string_of_rat j,
-                                                   Bool.toString d]))
-                                              Int.toString) items, n+1)) result 1))
+      val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^
+                " subgoal(s)" ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
+                        ("  " ^ Int.toString n ^ ". Ts    = " ^
+                           string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
+                         "    items = " ^ string_of_list (string_of_pair 
+                           (fn (l, i, rel, r, j, d) => enclose "(" ")" (commas
+                             [string_of_list
+                                (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
+                              Rat.string_of_rat i,
+                              rel,
+                              string_of_list
+                                (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
+                              Rat.string_of_rat j,
+                              Bool.toString d]))
+                           Int.toString) items, n+1)) result 1))
 *)
   in result end;
 
-(* term list * (decompT * int) -> term list *)
-
-fun add_atoms (ats, ((lhs,_,_,rhs,_,_),_)) =
+fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
     (map fst lhs) union ((map fst rhs) union ats);
 
-(* (bool * term) list * (decompT * int) -> (bool * term) list *)
-
-fun add_datoms (dats, ((lhs,_,_,rhs,_,d),_)) =
-    (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
-
-(* (decompT * int) list -> bool list *)
+fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decompT, _)) :
+  (bool * term) list =
+  (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
 
-fun discr initems = map fst (Library.foldl add_datoms ([],initems));
-
-(* Theory.theory -> (string * typ) list -> bool -> (typ list * (decompT * int) list) list -> injust list -> injust list option *)
+fun discr (initems : (LA_Data.decompT * int) list) : bool list =
+  map fst (Library.foldl add_datoms ([],initems));
 
-fun refutes sg params show_ex =
+fun refutes (sg : theory) (params : (string * typ) list) (show_ex : bool) :
+  (typ list * (LA_Data.decompT * int) list) list -> injust list -> injust list option =
 let
-  (* (typ list * (decompT * int) list) list -> injust list -> injust list option *)
-  fun refute ((Ts, initems)::initemss) js =
+  fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss)
+             (js : injust list) : injust list option =
     let val atoms = Library.foldl add_atoms ([], initems)
         val n = length atoms
         val mkleq = mklineq n atoms
@@ -675,7 +660,8 @@
         val ineqs = map mkleq initems @ natlineqs
     in case elim (ineqs, []) of
          Success j =>
-           (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); refute initemss (js@[j]))
+           (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")");
+            refute initemss (js@[j]))
        | Failure hist =>
            (if not show_ex then
               ()
@@ -692,62 +678,63 @@
     | refute [] js = SOME js
 in refute end;
 
-(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> term list -> injust list option *)
-
-fun refute sg params show_ex terms =
+fun refute (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) (terms : term list) :
+  injust list option =
   refutes sg params show_ex (split_items sg (map snd params, terms)) [];
 
-(* ('a -> bool) -> 'a list -> int *)
-
-fun count P xs = length (List.filter P xs);
+fun count (P : 'a -> bool) (xs : 'a list) : int = length (List.filter P xs);
 
 (* The limit on the number of ~= allowed.
    Because each ~= is split into two cases, this can lead to an explosion.
 *)
 val fast_arith_neq_limit = ref 9;
 
-(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *)
-
-fun prove sg params show_ex Hs concl =
+fun prove (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) (Hs : term list)
+          (concl : term) : injust list option =
   let
     (* append the negated conclusion to 'Hs' -- this corresponds to     *)
     (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
     (* theorem/tactic level                                             *)
     val Hs' = Hs @ [LA_Logic.neg_prop concl]
-    (* decompT option -> bool *)
     fun is_neq NONE                 = false
       | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
   in
     trace_msg "prove";
     if count is_neq (map (LA_Data.decomp sg) Hs')
       > !fast_arith_neq_limit then (
-      trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")");
+      trace_msg ("fast_arith_neq_limit exceeded (current value is " ^
+                   string_of_int (!fast_arith_neq_limit) ^ ")");
       NONE
     ) else
       refute sg params show_ex Hs'
   end;
 
-(* MetaSimplifier.simpset -> int * injust list -> Tactical.tactic *)
-
-fun refute_tac ss (i, justs) =
+fun refute_tac (ss : simpset) (i : int, justs : injust list) : tactic =
   fn state =>
-    let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ Int.toString (length justs) ^ " justification(s)):") state
+    let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^
+                             Int.toString (length justs) ^ " justification(s)):") state
         val sg          = theory_of_thm state
         val {neqE, ...} = Data.get sg
         fun just1 j =
-          REPEAT_DETERM (eresolve_tac neqE i) THEN                  (* eliminate inequalities *)
-            METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i  (* use theorems generated from the actual justifications *)
-    in DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN  (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
-       DETERM (LA_Data.pre_tac i) THEN                               (* user-defined preprocessing of the subgoal *)
+          (* eliminate inequalities *)
+          REPEAT_DETERM (eresolve_tac neqE i) THEN
+            (* use theorems generated from the actual justifications *)
+            METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
+    in (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
+       DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
+       (* user-defined preprocessing of the subgoal *)
+       DETERM (LA_Data.pre_tac i) THEN
        PRIMITIVE (trace_thm "State after pre_tac:") THEN
-       EVERY (map just1 justs)                                       (* prove every resulting subgoal, using its justification *)
+       (* prove every resulting subgoal, using its justification *)
+       EVERY (map just1 justs)
     end  state;
 
 (*
 Fast but very incomplete decider. Only premises and conclusions
 that are already (negated) (in)equations are taken into account.
 *)
-fun simpset_lin_arith_tac ss show_ex i st = SUBGOAL (fn (A,_) =>
+fun simpset_lin_arith_tac (ss : simpset) (show_ex : bool) (i : int) (st : thm) =
+  SUBGOAL (fn (A,_) =>
   let val params = rev (Logic.strip_params A)
       val Hs     = Logic.strip_assums_hyp A
       val concl  = Logic.strip_assums_concl A
@@ -757,19 +744,17 @@
      | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
   end) i st;
 
-fun lin_arith_tac show_ex i st =
+fun lin_arith_tac (show_ex : bool) (i : int) (st : thm) =
   simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
     show_ex i st;
 
-fun cut_lin_arith_tac ss i =
+fun cut_lin_arith_tac (ss : simpset) (i : int) =
   cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
   simpset_lin_arith_tac ss false i;
 
 (** Forward proof from theorems **)
 
-(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> Term.term -> injust list -> bool -> Thm.thm option *)
-
-fun prover (ctxt as (sg, ss)) thms Tconcl js pos =
+fun prover (ctxt as (sg, ss)) thms (Tconcl : term) (js : injust list) (pos : bool) : thm option =
 let
     (* There is no "forward version" of 'pre_tac'.  Therefore we combine the     *)
     (* available theorems into a single proof state and perform "backward proof" *)
@@ -794,9 +779,7 @@
       dives into terms and will thus try the non-negated concl anyway.
 *)
 
-(* Theory.theory -> MetaSimplifier.simpset -> Term.term -> Thm.thm option *)
-
-fun lin_arith_prover sg ss concl =
+fun lin_arith_prover sg ss (concl : term) : thm option =
 let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss));
     val Hs = map prop_of thms
     val Tconcl = LA_Logic.mk_Trueprop concl