Restructured lin.arith.package.

--- a/src/HOL/Arith.ML	Wed Sep 22 21:49:37 1999 +0200
+++ b/src/HOL/Arith.ML	Thu Sep 23 09:04:36 1999 +0200
@@ -890,29 +890,18 @@
 
 end;
 
-structure Nat_LA_Data (* : LIN_ARITH_DATA *) =
-struct
-
-val lessD = [Suc_leI];
-
-(* reduce contradictory <= to False.
-   Most of the work is done by the cancel tactics.
-*)
-val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
+signature LIN_ARITH_DATA2 =
+sig
+  include LIN_ARITH_DATA
+  val discrete: (string * bool)list ref
+end;
 
-val cancel_sums_ss = HOL_basic_ss addsimps add_rules
-                                  addsimprocs nat_cancel_sums_add;
-
-val simp = simplify cancel_sums_ss;
-
-val add_mono_thms = map (fn s => prove_goal Arith.thy s
- (fn prems => [cut_facts_tac prems 1,
-               blast_tac (claset() addIs [add_le_mono]) 1]))
-["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
- "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
- "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
- "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
-];
+structure LA_Data_Ref: LIN_ARITH_DATA2 =
+struct
+  val add_mono_thms = ref ([]:thm list);
+  val lessD = ref ([]:thm list);
+  val ss_ref = ref HOL_basic_ss;
+  val discrete = ref ([]:(string*bool)list);
 
 (* Decomposition of terms *)
 
@@ -953,31 +942,44 @@
 fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
   | negate None = None;
 
-fun decomp1 tab (T,xxx) =
+fun decomp1 (T,xxx) =
   (case T of
      Type("fun",[Type(D,[]),_]) =>
-       (case assoc(!tab,D) of
+       (case assoc(!discrete,D) of
           None => None
         | Some d => (case decomp2 xxx of
                        None => None
                      | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
    | _ => None);
 
-(* tab: (string * bool)list ref  contains the discreteneness flag *)
-fun decomp tab (_$(Const(rel,T)$lhs$rhs)) = decomp1 tab (T,(rel,lhs,rhs))
-  | decomp tab (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
-      negate(decomp1 tab (T,(rel,lhs,rhs)))
-  | decomp _ _ = None
-
+fun decomp (_$(Const(rel,T)$lhs$rhs)) = decomp1 (T,(rel,lhs,rhs))
+  | decomp (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
+      negate(decomp1 (T,(rel,lhs,rhs)))
+  | decomp _ = None
 end;
 
-structure LA_Data_Ref =
-struct
-  val add_mono_thms = ref Nat_LA_Data.add_mono_thms
-  val lessD = ref Nat_LA_Data.lessD
-  val simp = ref Nat_LA_Data.simp
-  val discrete = ref [("nat",true)]
-  val decomp = Nat_LA_Data.decomp discrete
+let
+
+(* reduce contradictory <= to False.
+   Most of the work is done by the cancel tactics.
+*)
+val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
+
+val add_mono_thms = map (fn s => prove_goal Arith.thy s
+ (fn prems => [cut_facts_tac prems 1,
+               blast_tac (claset() addIs [add_le_mono]) 1]))
+["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
+ "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
+ "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
+ "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
+];
+
+in
+LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
+LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [Suc_leI];
+LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
+                      addsimprocs nat_cancel_sums_add;
+LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("nat",true)]
 end;
 
 structure Fast_Arith =
@@ -985,14 +987,16 @@
 
 val fast_arith_tac = Fast_Arith.lin_arith_tac;
 
+let
 val nat_arith_simproc_pats =
   map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT))
       ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
 
-val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
-                                        Fast_Arith.lin_arith_prover;
-
-Addsimprocs [fast_nat_arith_simproc];
+val fast_nat_arith_simproc = mk_simproc
+  "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
+in
+Addsimprocs [fast_nat_arith_simproc]
+end;
 
 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
 useful to detect inconsistencies among the premises for subgoals which are
@@ -1017,9 +1021,10 @@
    (max m n + k <= r) = (m+k <= r & n+k <= r)
    (l <= min m n + k) = (l <= m+k & l <= n+k)
 *)
-val arith_tac =
-  refute_tac (K true) (REPEAT o split_tac[nat_diff_split,split_min,split_max])
-             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
+val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max];
+fun arith_tac i =
+  refute_tac (K true) (REPEAT o split_tac (!arith_tac_split_thms))
+             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i;
 
 
 (* proof method setup *)

--- a/src/HOL/Integ/Bin.ML	Wed Sep 22 21:49:37 1999 +0200
+++ b/src/HOL/Integ/Bin.ML	Thu Sep 23 09:04:36 1999 +0200
@@ -480,22 +480,17 @@
 (The latter option is very inefficient!)
 *)
 
-structure Int_LA_Data(*: LIN_ARITH_DATA*) =
-struct
-
-val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
+(* Update parameters of arithmetic prover *)
+let
 
 (* reduce contradictory <= to False *)
 val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
                 [int_0,zmult_0,zmult_0_right];
 
-val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
-          addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv,
-                       Int_CC.sum_conv, Int_CC.rel_conv];
+val simprocs = [Int_Cancel.sum_conv, Int_Cancel.rel_conv,
+                Int_CC.sum_conv, Int_CC.rel_conv];
 
-val simp = simplify cancel_sums_ss;
-
-val add_mono_thms = Nat_LA_Data.add_mono_thms @
+val add_mono_thms =
   map (fn s => prove_goal Int.thy s
                  (fn prems => [cut_facts_tac prems 1,
                       asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
@@ -505,31 +500,24 @@
      "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
     ];
 
+in
+LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
+LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
+LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
+                      addsimprocs simprocs;
+LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
 end;
 
-(* Update parameters of arithmetic prover *)
-LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms;
-LA_Data_Ref.lessD :=         Int_LA_Data.lessD;
-LA_Data_Ref.simp :=          Int_LA_Data.simp;
-LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)];
-
-
+let
 val int_arith_simproc_pats =
   map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
       ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
 
-val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
-                                        Fast_Arith.lin_arith_prover;
-
-Addsimprocs [fast_int_arith_simproc];
-
-(* FIXME: K true should be replaced by a sensible test to speed things up
-   in case there are lots of irrelevant terms involved.
-
-val arith_tac =
-  refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
-             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
-*)
+val fast_int_arith_simproc = mk_simproc
+  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
+in
+Addsimprocs [fast_int_arith_simproc]
+end;
 
 (* Some test data
 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";

--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Sep 22 21:49:37 1999 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Sep 23 09:04:36 1999 +0200
@@ -17,6 +17,8 @@
 (in)equations. lin_arith_prover tries to prove or disprove the term.
 *)
 
+(* Debugging: (*? -> (*?*), !*) -> (*!*) *)
+
 (*** Data needed for setting up the linear arithmetic package ***)
 
 signature LIN_ARITH_LOGIC =
@@ -54,9 +56,8 @@
                             (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *)
   val lessD:            thm list ref (* m < n ==> m+1 <= n *)
   val decomp:
-    term ->
-      ((term * int)list * int * string * (term * int)list * int * bool)option
-  val simp: (thm -> thm) ref
+    term -> ((term*int)list * int * string * (term*int)list * int * bool)option
+  val ss_ref: simpset ref
 end;
 (*
 decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
@@ -65,7 +66,7 @@
          of summand * multiplicity pairs and a constant summand and
          d indicates if the domain is discrete.
 
-simp must reduce contradictory <= to False.
+ss_ref must reduce contradictory <= to False.
    It should also cancel common summands to keep <= reduced;
    otherwise <= can grow to massive proportions.
 *)
@@ -202,7 +203,7 @@
 
 
 fun elim ineqs =
-  let (*val dummy = print_ineqs ineqs;*)
+  let (*?val dummy = print_ineqs ineqs;!*)
       val (triv,nontriv) = partition is_trivial ineqs in
   if not(null triv)
   then case find_first is_answer triv of
@@ -268,19 +269,20 @@
         in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
 
       fun simp thm =
-        let val thm' = !LA_Data.simp thm
+        let val thm' = simplify (!LA_Data.ss_ref) thm
         in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
 
-      fun mk(Asm i) = ((*writeln"Asm";prth*)(nth_elem(i,asms)))
-        | mk(Nat(i)) = ((*writeln"N";*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
-        | mk(LessD(j)) = ((*writeln"L";prth*)(hd([mk j] RL !LA_Data.lessD)))
-        | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD))
-        | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
-        | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD))
-        | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp((*prth*)(addthms (mk j1) (mk j2)))))
-        | mk(Multiplied(n,j)) = ((*writeln"*";*)multn(n,mk j))
+      fun mk(Asm i) = ((*?writeln"Asm";prth!*)(nth_elem(i,asms)))
+        | mk(Nat(i)) = ((*?writeln"Nat";!*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
+        | mk(LessD(j)) = ((*?writeln"L";prth!*)(hd([mk j] RL !LA_Data.lessD)))
+        | mk(NotLeD(j)) = ((*?writeln"NLe";prth!*)(mk j RS LA_Logic.not_leD))
+        | mk(NotLeDD(j)) = ((*?writeln"NLeD";prth!*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
+        | mk(NotLessD(j)) = ((*?writeln"NL";prth!*)(mk j RS LA_Logic.not_lessD))
+        | mk(Added(j1,j2)) = ((*?writeln"+";prth!*)(simp((*?prth!*)(addthms (mk j1) (mk j2)))))
+        | mk(Multiplied(n,j)) = ((*?writeln"*";!*)multn(n,mk j))
 
-  in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end
+  in (*?writeln"mkthm";!*)
+     simplify (!LA_Data.ss_ref) (mk just) handle FalseE thm => thm end
 end;
 
 fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i;