src/HOL/Tools/int_arith.ML
changeset 30496 7cdcc9dd95cb
parent 29269 5c25a2012975
child 30518 07b45c1aa788
--- a/src/HOL/Tools/int_arith.ML	Thu Mar 12 18:01:25 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML	Thu Mar 12 18:01:26 2009 +0100
@@ -1,59 +1,32 @@
-(*  Title:      HOL/Tools/int_arith1.ML
-    Authors:    Larry Paulson and Tobias Nipkow
-
-Simprocs and decision procedure for linear arithmetic.
-*)
-
-structure Int_Numeral_Base_Simprocs =
-  struct
-  fun prove_conv tacs ctxt (_: thm list) (t, u) =
-    if t aconv u then NONE
-    else
-      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
-      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
-
-  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
-
-  fun prep_simproc (name, pats, proc) =
-    Simplifier.simproc (the_context()) name pats proc;
-
-  fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
-    | is_numeral _ = false
-
-  fun simplify_meta_eq f_number_of_eq f_eq =
-      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
+(* Authors: Larry Paulson and Tobias Nipkow
 
-  (*reorientation simprules using ==, for the following simproc*)
-  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
-  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
-  val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
-
-  (*reorientation simplification procedure: reorients (polymorphic) 
-    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
-  fun reorient_proc sg _ (_ $ t $ u) =
-    case u of
-        Const(@{const_name HOL.zero}, _) => NONE
-      | Const(@{const_name HOL.one}, _) => NONE
-      | Const(@{const_name Int.number_of}, _) $ _ => NONE
-      | _ => SOME (case t of
-          Const(@{const_name HOL.zero}, _) => meta_zero_reorient
-        | Const(@{const_name HOL.one}, _) => meta_one_reorient
-        | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
-
-  val reorient_simproc = 
-      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
-
-  end;
-
-
-Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
-
+Simprocs and decision procedure for numerals and linear arithmetic.
+*)
 
 structure Int_Numeral_Simprocs =
 struct
 
-(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
-  isn't complicated by the abstract 0 and 1.*)
+(*reorientation simprules using ==, for the following simproc*)
+val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
+val meta_one_reorient = @{thm one_reorient} RS eq_reflection
+val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
+
+(*reorientation simplification procedure: reorients (polymorphic) 
+  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
+fun reorient_proc sg _ (_ $ t $ u) =
+  case u of
+      Const(@{const_name HOL.zero}, _) => NONE
+    | Const(@{const_name HOL.one}, _) => NONE
+    | Const(@{const_name Int.number_of}, _) $ _ => NONE
+    | _ => SOME (case t of
+        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
+      | Const(@{const_name HOL.one}, _) => meta_one_reorient
+      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
+
+val reorient_simproc = 
+  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
+
+(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
 
 (** New term ordering so that AC-rewriting brings numerals to the front **)
@@ -88,7 +61,7 @@
 
 fun numtermless tu = (numterm_ord tu = LESS);
 
-(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
+(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
 val num_ss = HOL_ss settermless numtermless;
 
 
@@ -213,7 +186,7 @@
 val divide_1s = [@{thm divide_numeral_1}];
 
 (*To perform binary arithmetic.  The "left" rewriting handles patterns
-  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
+  created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *)
 val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
                  @{thm add_number_of_left}, @{thm mult_number_of_left}] @
                 @{thms arith_simps} @ @{thms rel_simps};
@@ -279,7 +252,7 @@
 
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val bal_add1 = @{thm eq_add_iff1} RS trans
@@ -288,7 +261,7 @@
 
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   val bal_add1 = @{thm less_add_iff1} RS trans
@@ -297,7 +270,7 @@
 
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   val bal_add1 = @{thm le_add_iff1} RS trans
@@ -305,7 +278,7 @@
 );
 
 val cancel_numerals =
-  map Int_Numeral_Base_Simprocs.prep_simproc
+  map Arith_Data.prep_simproc
    [("inteq_cancel_numerals",
      ["(l::'a::number_ring) + m = n",
       "(l::'a::number_ring) = m + n",
@@ -342,7 +315,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
-  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+  val prove_conv        = Arith_Data.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
@@ -372,7 +345,7 @@
   val mk_coeff          = mk_fcoeff
   val dest_coeff        = dest_fcoeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
-  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+  val prove_conv        = Arith_Data.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
@@ -392,23 +365,42 @@
 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
 
 val combine_numerals =
-  Int_Numeral_Base_Simprocs.prep_simproc
+  Arith_Data.prep_simproc
     ("int_combine_numerals", 
      ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
      K CombineNumerals.proc);
 
 val field_combine_numerals =
-  Int_Numeral_Base_Simprocs.prep_simproc
+  Arith_Data.prep_simproc
     ("field_combine_numerals", 
      ["(i::'a::{number_ring,field,division_by_zero}) + j",
       "(i::'a::{number_ring,field,division_by_zero}) - j"], 
      K FieldCombineNumerals.proc);
 
+(** Constant folding for multiplication in semirings **)
+
+(*We do not need folding for addition: combine_numerals does the same thing*)
+
+structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
+  val eq_reflection = eq_reflection
 end;
 
+structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
+
+val assoc_fold_simproc =
+  Arith_Data.prep_simproc
+   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
+    K Semiring_Times_Assoc.proc);
+
+end;
+
+Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
 Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
+Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc];
 
 (*examples:
 print_depth 22;
@@ -447,29 +439,6 @@
 test "(i + j + -12 + (k::int)) - -15 = y";
 *)
 
-
-(** Constant folding for multiplication in semirings **)
-
-(*We do not need folding for addition: combine_numerals does the same thing*)
-
-structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
-struct
-  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
-  val eq_reflection = eq_reflection
-end;
-
-structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
-
-val assoc_fold_simproc =
-  Int_Numeral_Base_Simprocs.prep_simproc
-   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
-    K Semiring_Times_Assoc.proc);
-
-Addsimprocs [assoc_fold_simproc];
-
-
-
-
 (*** decision procedure for linear arithmetic ***)
 
 (*---------------------------------------------------------------------------*)
@@ -480,8 +449,10 @@
 Instantiation of the generic linear arithmetic package for int.
 *)
 
+structure Int_Arith =
+struct
+
 (* Update parameters of arithmetic prover *)
-local
 
 (* reduce contradictory =/</<= to False *)
 
@@ -489,25 +460,31 @@
    and m and n are ground terms over rings (roughly speaking).
    That is, m and n consist only of 1s combined with "+", "-" and "*".
 *)
-local
+
 val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
+
 val lhss0 = [@{cpat "0::?'a::ring"}];
+
 fun proc0 phi ss ct =
   let val T = ctyp_of_term ct
   in if typ_of T = @{typ int} then NONE else
      SOME (instantiate' [SOME T] [] zeroth)
   end;
+
 val zero_to_of_int_zero_simproc =
   make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   proc = proc0, identifier = []};
 
 val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
+
 val lhss1 = [@{cpat "1::?'a::ring_1"}];
+
 fun proc1 phi ss ct =
   let val T = ctyp_of_term ct
   in if typ_of T = @{typ int} then NONE else
      SOME (instantiate' [SOME T] [] oneth)
   end;
+
 val one_to_of_int_one_simproc =
   make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   proc = proc1, identifier = []};
@@ -533,15 +510,15 @@
      addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
 
 fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
+
 val lhss' =
   [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
    @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
    @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
-in
+
 val zero_one_idom_simproc =
   make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   proc = sproc, identifier = []}
-end;
 
 val add_rules =
     simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
@@ -556,13 +533,11 @@
 
 val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
 
-val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
+val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   :: Int_Numeral_Simprocs.combine_numerals
   :: Int_Numeral_Simprocs.cancel_numerals;
 
-in
-
-val int_arith_setup =
+val setup =
   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
@@ -570,13 +545,11 @@
     lessD = lessD @ [@{thm zless_imp_add1_zle}],
     neqE = neqE,
     simpset = simpset addsimps add_rules
-                      addsimprocs Int_Numeral_Base_Simprocs
+                      addsimprocs int_numeral_base_simprocs
                       addcongs [if_weak_cong]}) #>
   arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   arith_discrete @{type_name Int.int}
 
-end;
-
 val fast_int_arith_simproc =
   Simplifier.simproc (the_context ())
   "fast_int_arith" 
@@ -584,4 +557,6 @@
       "(m::'a::{ordered_idom,number_ring}) <= n",
       "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
 
-Addsimprocs [fast_int_arith_simproc];
+end;
+
+Addsimprocs [Int_Arith.fast_int_arith_simproc];