Fixed splitting of div and mod on integers (split theorem differed from implementation).
authorwebertj
Tue Nov 17 10:17:53 2009 +0000 (2009-11-17)
changeset 33728cb4235333c30
parent 33719 474ebcc348e6
child 33729 3101453e0b1c
Fixed splitting of div and mod on integers (split theorem differed from implementation).
src/HOL/Divides.thy
src/HOL/Tools/lin_arith.ML
     1.1 --- a/src/HOL/Divides.thy	Mon Nov 16 18:33:12 2009 +0000
     1.2 +++ b/src/HOL/Divides.thy	Tue Nov 17 10:17:53 2009 +0000
     1.3 @@ -2030,9 +2030,11 @@
     1.4                        split_neg_lemma [of concl: "%x y. P y"])
     1.5  done
     1.6  
     1.7 -(* Enable arith to deal with div 2 and mod 2: *)
     1.8 -declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split]
     1.9 -declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
    1.10 +(* Enable arith to deal with @{term div} and @{term mod} when
    1.11 +   these are applied to some constant that is of the form
    1.12 +   @{term "number_of k"}: *)
    1.13 +declare split_zdiv [of _ _ "number_of k", standard, arith_split]
    1.14 +declare split_zmod [of _ _ "number_of k", standard, arith_split]
    1.15  
    1.16  
    1.17  subsubsection{*Speeding up the Division Algorithm with Shifting*}
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Nov 16 18:33:12 2009 +0000
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Tue Nov 17 10:17:53 2009 +0000
     2.3 @@ -438,7 +438,7 @@
     2.4        in
     2.5          SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
     2.6        end
     2.7 -    (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
     2.8 +    (* ?P (nat ?i) = ((ALL n. ?i = of_nat n --> ?P n) & (?i < 0 --> ?P 0)) *)
     2.9      | (Const ("Int.nat", _), [t1]) =>
    2.10        let
    2.11          val rev_terms   = rev terms
    2.12 @@ -449,12 +449,12 @@
    2.13                              (map (incr_boundvars 1) rev_terms)
    2.14          val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
    2.15          val t1'         = incr_boundvars 1 t1
    2.16 -        val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
    2.17 +        val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
    2.18                              (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
    2.19          val t1_lt_zero  = Const (@{const_name HOL.less},
    2.20                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
    2.21          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
    2.22 -        val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
    2.23 +        val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
    2.24          val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
    2.25        in
    2.26          SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
    2.27 @@ -524,13 +524,15 @@
    2.28          SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
    2.29        end
    2.30      (* ?P ((?n::int) mod (number_of ?k)) =
    2.31 -         ((iszero (number_of ?k) --> ?P ?n) &
    2.32 -          (neg (number_of (uminus ?k)) -->
    2.33 -            (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
    2.34 -          (neg (number_of ?k) -->
    2.35 -            (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
    2.36 +         ((number_of ?k = 0 --> ?P ?n) &
    2.37 +          (0 < number_of ?k -->
    2.38 +            (ALL i j.
    2.39 +              0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
    2.40 +          (number_of ?k < 0 -->
    2.41 +            (ALL i j.
    2.42 +              number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
    2.43      | (Const ("Divides.div_class.mod",
    2.44 -        Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
    2.45 +        Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
    2.46        let
    2.47          val rev_terms               = rev terms
    2.48          val zero                    = Const (@{const_name HOL.zero}, split_type)
    2.49 @@ -540,33 +542,33 @@
    2.50          val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)])
    2.51                                          (map (incr_boundvars 2) rev_terms)
    2.52          val t1'                     = incr_boundvars 2 t1
    2.53 -        val (t2' as (_ $ k'))       = incr_boundvars 2 t2
    2.54 -        val iszero_t2               = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
    2.55 -        val neg_minus_k             = Const ("Int.neg", split_type --> HOLogic.boolT) $
    2.56 -                                        (number_of $
    2.57 -                                          (Const (@{const_name HOL.uminus},
    2.58 -                                            HOLogic.intT --> HOLogic.intT) $ k'))
    2.59 +        val t2'                     = incr_boundvars 2 t2
    2.60 +        val t2_eq_zero              = Const ("op =",
    2.61 +                                        split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
    2.62 +        val zero_lt_t2              = Const (@{const_name HOL.less},
    2.63 +                                        split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
    2.64 +        val t2_lt_zero              = Const (@{const_name HOL.less},
    2.65 +                                        split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
    2.66          val zero_leq_j              = Const (@{const_name HOL.less_eq},
    2.67                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
    2.68 +        val j_leq_zero              = Const (@{const_name HOL.less_eq},
    2.69 +                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
    2.70          val j_lt_t2                 = Const (@{const_name HOL.less},
    2.71                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
    2.72 +        val t2_lt_j                 = Const (@{const_name HOL.less},
    2.73 +                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
    2.74          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
    2.75                                         (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
    2.76                                           (Const (@{const_name HOL.times},
    2.77                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
    2.78 -        val neg_t2                  = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
    2.79 -        val t2_lt_j                 = Const (@{const_name HOL.less},
    2.80 -                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
    2.81 -        val j_leq_zero              = Const (@{const_name HOL.less_eq},
    2.82 -                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
    2.83          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
    2.84 -        val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
    2.85 -        val subgoal2                = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
    2.86 +        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
    2.87 +        val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
    2.88                                          @ hd terms2_3
    2.89                                          :: (if tl terms2_3 = [] then [not_false] else [])
    2.90                                          @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
    2.91                                          @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
    2.92 -        val subgoal3                = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
    2.93 +        val subgoal3                = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
    2.94                                          @ hd terms2_3
    2.95                                          :: (if tl terms2_3 = [] then [not_false] else [])
    2.96                                          @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
    2.97 @@ -576,13 +578,15 @@
    2.98          SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
    2.99        end
   2.100      (* ?P ((?n::int) div (number_of ?k)) =
   2.101 -         ((iszero (number_of ?k) --> ?P 0) &
   2.102 -          (neg (number_of (uminus ?k)) -->
   2.103 -            (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
   2.104 -          (neg (number_of ?k) -->
   2.105 -            (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
   2.106 +         ((number_of ?k = 0 --> ?P 0) &
   2.107 +          (0 < number_of ?k -->
   2.108 +            (ALL i j.
   2.109 +              0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P i)) &
   2.110 +          (number_of ?k < 0 -->
   2.111 +            (ALL i j.
   2.112 +              number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P i))) *)
   2.113      | (Const ("Divides.div_class.div",
   2.114 -        Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
   2.115 +        Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
   2.116        let
   2.117          val rev_terms               = rev terms
   2.118          val zero                    = Const (@{const_name HOL.zero}, split_type)
   2.119 @@ -592,38 +596,37 @@
   2.120          val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)])
   2.121                                          (map (incr_boundvars 2) rev_terms)
   2.122          val t1'                     = incr_boundvars 2 t1
   2.123 -        val (t2' as (_ $ k'))       = incr_boundvars 2 t2
   2.124 -        val iszero_t2               = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
   2.125 -        val neg_minus_k             = Const ("Int.neg", split_type --> HOLogic.boolT) $
   2.126 -                                        (number_of $
   2.127 -                                          (Const (@{const_name HOL.uminus},
   2.128 -                                            HOLogic.intT --> HOLogic.intT) $ k'))
   2.129 +        val t2'                     = incr_boundvars 2 t2
   2.130 +        val t2_eq_zero              = Const ("op =",
   2.131 +                                        split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   2.132 +        val zero_lt_t2              = Const (@{const_name HOL.less},
   2.133 +                                        split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
   2.134 +        val t2_lt_zero              = Const (@{const_name HOL.less},
   2.135 +                                        split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
   2.136          val zero_leq_j              = Const (@{const_name HOL.less_eq},
   2.137                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
   2.138 +        val j_leq_zero              = Const (@{const_name HOL.less_eq},
   2.139 +                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
   2.140          val j_lt_t2                 = Const (@{const_name HOL.less},
   2.141                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   2.142 -        val t1_eq_t2_times_i_plus_j = Const ("op =",
   2.143 -                                        split_type --> split_type --> HOLogic.boolT) $ t1' $
   2.144 +        val t2_lt_j                 = Const (@{const_name HOL.less},
   2.145 +                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   2.146 +        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   2.147                                         (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
   2.148                                           (Const (@{const_name HOL.times},
   2.149                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   2.150 -        val neg_t2                  = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
   2.151 -        val t2_lt_j                 = Const (@{const_name HOL.less},
   2.152 -                                        split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   2.153 -        val j_leq_zero              = Const (@{const_name HOL.less_eq},
   2.154 -                                        split_type --> split_type --> HOLogic.boolT) $ j $ zero
   2.155          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   2.156 -        val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
   2.157 -        val subgoal2                = (HOLogic.mk_Trueprop neg_minus_k)
   2.158 -                                        :: terms2_3
   2.159 -                                        @ not_false
   2.160 -                                        :: (map HOLogic.mk_Trueprop
   2.161 -                                             [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
   2.162 -        val subgoal3                = (HOLogic.mk_Trueprop neg_t2)
   2.163 -                                        :: terms2_3
   2.164 -                                        @ not_false
   2.165 -                                        :: (map HOLogic.mk_Trueprop
   2.166 -                                             [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
   2.167 +        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   2.168 +        val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
   2.169 +                                        @ hd terms2_3
   2.170 +                                        :: (if tl terms2_3 = [] then [not_false] else [])
   2.171 +                                        @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
   2.172 +                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   2.173 +        val subgoal3                = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
   2.174 +                                        @ hd terms2_3
   2.175 +                                        :: (if tl terms2_3 = [] then [not_false] else [])
   2.176 +                                        @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
   2.177 +                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   2.178          val Ts'                     = split_type :: split_type :: Ts
   2.179        in
   2.180          SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
   2.181 @@ -886,12 +889,12 @@
   2.182       (l <= min m n + k) = (l <= m+k & l <= n+k)
   2.183    *)
   2.184    refute_tac (K true)
   2.185 -    (* Splitting is also done inside simple_tac, but not completely --   *)
   2.186 -    (* split_tac may use split theorems that have not been implemented in    *)
   2.187 -    (* simple_tac (cf. pre_decomp and split_once_items above), and       *)
   2.188 -    (* split_limit may trigger.                                   *)
   2.189 -    (* Therefore splitting outside of simple_tac may allow us to prove   *)
   2.190 -    (* some goals that simple_tac alone would fail on.                   *)
   2.191 +    (* Splitting is also done inside simple_tac, but not completely --    *)
   2.192 +    (* split_tac may use split theorems that have not been implemented in *)
   2.193 +    (* simple_tac (cf. pre_decomp and split_once_items above), and        *)
   2.194 +    (* split_limit may trigger.                                           *)
   2.195 +    (* Therefore splitting outside of simple_tac may allow us to prove    *)
   2.196 +    (* some goals that simple_tac alone would fail on.                    *)
   2.197      (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
   2.198      (lin_arith_tac ctxt ex);
   2.199