src/HOL/Tools/Qelim/cooper.ML
changeset 47108 2a1953f0d20d
parent 46497 89ccf66aa73d
child 47142 d64fa2ca54b8
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -41,9 +41,9 @@
     1.4     @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
     1.5     @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
     1.6     @{term "nat"}, @{term "int"},
     1.7 -   @{term "Int.Bit0"}, @{term "Int.Bit1"},
     1.8 -   @{term "Int.Pls"}, @{term "Int.Min"},
     1.9 -   @{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
    1.10 +   @{term "Num.One"}, @{term "Num.Bit0"}, @{term "Num.Bit1"},
    1.11 +   @{term "Num.numeral :: num => int"}, @{term "Num.numeral :: num => nat"},
    1.12 +   @{term "Num.neg_numeral :: num => int"},
    1.13     @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    1.14     @{term "True"}, @{term "False"}];
    1.15  
    1.16 @@ -595,8 +595,10 @@
    1.17    | num_of_term vs (Term.Bound i) = Proc.Bound i
    1.18    | num_of_term vs @{term "0::int"} = Proc.C 0
    1.19    | num_of_term vs @{term "1::int"} = Proc.C 1
    1.20 -  | num_of_term vs (t as Const (@{const_name number_of}, _) $ _) =
    1.21 +  | num_of_term vs (t as Const (@{const_name numeral}, _) $ _) =
    1.22        Proc.C (dest_number t)
    1.23 +  | num_of_term vs (t as Const (@{const_name neg_numeral}, _) $ _) =
    1.24 +      Proc.Neg (Proc.C (dest_number t))
    1.25    | num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
    1.26        Proc.Neg (num_of_term vs t')
    1.27    | num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
    1.28 @@ -784,16 +786,16 @@
    1.29  
    1.30  local
    1.31  val ss1 = comp_ss
    1.32 -  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}]
    1.33 -      @ map (fn r => r RS sym)
    1.34 +  addsimps @{thms simp_thms} @ [@{thm "nat_numeral"} RS sym, @{thm "zdvd_int"}] 
    1.35 +      @ map (fn r => r RS sym) 
    1.36          [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
    1.37           @{thm "zmult_int"}]
    1.38    |> Splitter.add_split @{thm "zdiff_int_split"}
    1.39  
    1.40  val ss2 = HOL_basic_ss
    1.41 -  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
    1.42 -            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
    1.43 -            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
    1.44 +  addsimps [@{thm "nat_0_le"}, @{thm "int_numeral"},
    1.45 +            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"}, 
    1.46 +            @{thm "le_numeral_extra"(3)}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
    1.47    |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    1.48  val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
    1.49    @ map (Thm.symmetric o mk_meta_eq)