# HG changeset patch
# User webertj
# Date 1258453131 0
# Node ID 3101453e0b1c10b3126557f6385e732f125b8e7b
# Parent  e588744f14dabc1bb5944513cc344df7949e7840# Parent  cb4235333c302b23012759d546b74d2b54eb252a
merged

diff -r e588744f14da -r 3101453e0b1c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Nov 16 21:57:16 2009 +0100
+++ b/src/HOL/Divides.thy	Tue Nov 17 10:18:51 2009 +0000
@@ -2030,9 +2030,11 @@
                       split_neg_lemma [of concl: "%x y. P y"])
 done
 
-(* Enable arith to deal with div 2 and mod 2: *)
-declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split]
-declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
+(* Enable arith to deal with @{term div} and @{term mod} when
+   these are applied to some constant that is of the form
+   @{term "number_of k"}: *)
+declare split_zdiv [of _ _ "number_of k", standard, arith_split]
+declare split_zmod [of _ _ "number_of k", standard, arith_split]
 
 
 subsubsection{*Speeding up the Division Algorithm with Shifting*}
diff -r e588744f14da -r 3101453e0b1c src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Nov 16 21:57:16 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Tue Nov 17 10:18:51 2009 +0000
@@ -438,7 +438,7 @@
       in
         SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
       end
-    (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
+    (* ?P (nat ?i) = ((ALL n. ?i = of_nat n --> ?P n) & (?i < 0 --> ?P 0)) *)
     | (Const ("Int.nat", _), [t1]) =>
       let
         val rev_terms   = rev terms
@@ -449,12 +449,12 @@
                             (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' $
+        val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
                             (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
         val t1_lt_zero  = Const (@{const_name HOL.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 subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
       in
         SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
@@ -524,13 +524,15 @@
         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 (uminus ?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))) *)
+         ((number_of ?k = 0 --> ?P ?n) &
+          (0 < number_of ?k -->
+            (ALL i j.
+              0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
+          (number_of ?k < 0 -->
+            (ALL i j.
+              number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
     | (Const ("Divides.div_class.mod",
-        Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+        Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const (@{const_name HOL.zero}, split_type)
@@ -540,33 +542,33 @@
         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 ("Int.iszero", split_type --> HOLogic.boolT) $ t2
-        val neg_minus_k             = Const ("Int.neg", split_type --> HOLogic.boolT) $
-                                        (number_of $
-                                          (Const (@{const_name HOL.uminus},
-                                            HOLogic.intT --> HOLogic.intT) $ k'))
+        val t2'                     = incr_boundvars 2 t2
+        val t2_eq_zero              = Const ("op =",
+                                        split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+        val zero_lt_t2              = Const (@{const_name HOL.less},
+                                        split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
+        val t2_lt_zero              = Const (@{const_name HOL.less},
+                                        split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
         val zero_leq_j              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
+        val j_leq_zero              = Const (@{const_name HOL.less_eq},
+                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val j_lt_t2                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t2_lt_j                 = Const (@{const_name HOL.less},
+                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val neg_t2                  = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const (@{const_name HOL.less},
-                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const (@{const_name HOL.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])
+        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+        val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
                                         @ hd terms2_3
                                         :: (if tl terms2_3 = [] then [not_false] else [])
                                         @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
                                         @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
-        val subgoal3                = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
+        val subgoal3                = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
                                         @ hd terms2_3
                                         :: (if tl terms2_3 = [] then [not_false] else [])
                                         @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
@@ -576,13 +578,15 @@
         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
       end
     (* ?P ((?n::int) div (number_of ?k)) =
-         ((iszero (number_of ?k) --> ?P 0) &
-          (neg (number_of (uminus ?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))) *)
+         ((number_of ?k = 0 --> ?P 0) &
+          (0 < number_of ?k -->
+            (ALL i j.
+              0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P i)) &
+          (number_of ?k < 0 -->
+            (ALL i j.
+              number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P i))) *)
     | (Const ("Divides.div_class.div",
-        Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+        Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const (@{const_name HOL.zero}, split_type)
@@ -592,38 +596,37 @@
         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 ("Int.iszero", split_type --> HOLogic.boolT) $ t2
-        val neg_minus_k             = Const ("Int.neg", split_type --> HOLogic.boolT) $
-                                        (number_of $
-                                          (Const (@{const_name HOL.uminus},
-                                            HOLogic.intT --> HOLogic.intT) $ k'))
+        val t2'                     = incr_boundvars 2 t2
+        val t2_eq_zero              = Const ("op =",
+                                        split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+        val zero_lt_t2              = Const (@{const_name HOL.less},
+                                        split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
+        val t2_lt_zero              = Const (@{const_name HOL.less},
+                                        split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
         val zero_leq_j              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
+        val j_leq_zero              = Const (@{const_name HOL.less_eq},
+                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val j_lt_t2                 = Const (@{const_name HOL.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' $
+        val t2_lt_j                 = Const (@{const_name HOL.less},
+                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val neg_t2                  = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const (@{const_name HOL.less},
-                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const (@{const_name HOL.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])
-        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])
+        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+        val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
+                                        @ hd terms2_3
+                                        :: (if tl terms2_3 = [] then [not_false] else [])
+                                        @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
+                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
+        val subgoal3                = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
+                                        @ hd terms2_3
+                                        :: (if tl terms2_3 = [] then [not_false] else [])
+                                        @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
+                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
         val Ts'                     = split_type :: split_type :: Ts
       in
         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
@@ -886,12 +889,12 @@
      (l <= min m n + k) = (l <= m+k & l <= n+k)
   *)
   refute_tac (K true)
-    (* Splitting is also done inside simple_tac, but not completely --   *)
-    (* split_tac may use split theorems that have not been implemented in    *)
-    (* simple_tac (cf. pre_decomp and split_once_items above), and       *)
-    (* split_limit may trigger.                                   *)
-    (* Therefore splitting outside of simple_tac may allow us to prove   *)
-    (* some goals that simple_tac alone would fail on.                   *)
+    (* Splitting is also done inside simple_tac, but not completely --    *)
+    (* split_tac may use split theorems that have not been implemented in *)
+    (* simple_tac (cf. pre_decomp and split_once_items above), and        *)
+    (* split_limit may trigger.                                           *)
+    (* Therefore splitting outside of simple_tac may allow us to prove    *)
+    (* some goals that simple_tac alone would fail on.                    *)
     (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
     (lin_arith_tac ctxt ex);