extended linear arith capabilities with code by Amine
authornipkow
Tue Aug 14 19:23:27 2007 +0200 (2007-08-14)
changeset 24266bdb48fd8fbdd
parent 24265 4d5917cc60c4
child 24267 867efa1dc4f8
extended linear arith capabilities with code by Amine
src/HOL/int_arith1.ML
     1.1 --- a/src/HOL/int_arith1.ML	Tue Aug 14 15:09:33 2007 +0200
     1.2 +++ b/src/HOL/int_arith1.ML	Tue Aug 14 19:23:27 2007 +0200
     1.3 @@ -570,7 +570,66 @@
     1.4  (* Update parameters of arithmetic prover *)
     1.5  local
     1.6  
     1.7 -(* reduce contradictory <= to False *)
     1.8 +(* reduce contradictory =/</<= to False *)
     1.9 +
    1.10 +(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
    1.11 +   and m and n are ground terms over rings (roughly speaking).
    1.12 +   That is, m and n consist only of 1s combined with "+", "-" and "*".
    1.13 +*)
    1.14 +local
    1.15 +val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
    1.16 +val lhss0 = [@{cpat "0::?'a::ring"}];
    1.17 +fun proc0 phi ss ct =
    1.18 +  let val T = ctyp_of_term ct
    1.19 +  in if typ_of T = @{typ int} then NONE else
    1.20 +     SOME (instantiate' [SOME T] [] zeroth)
    1.21 +  end;
    1.22 +val zero_to_of_int_zero_simproc =
    1.23 +  make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
    1.24 +  proc = proc0, identifier = []};
    1.25 +
    1.26 +val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
    1.27 +val lhss1 = [@{cpat "1::?'a::ring_1"}];
    1.28 +fun proc1 phi ss ct =
    1.29 +  let val T = ctyp_of_term ct
    1.30 +  in if typ_of T = @{typ int} then NONE else
    1.31 +     SOME (instantiate' [SOME T] [] oneth)
    1.32 +  end;
    1.33 +val one_to_of_int_one_simproc =
    1.34 +  make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
    1.35 +  proc = proc1, identifier = []};
    1.36 +
    1.37 +val allowed_consts =
    1.38 +  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
    1.39 +   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
    1.40 +   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
    1.41 +   @{const_name "HOL.less_eq"}];
    1.42 +
    1.43 +fun check t = case t of
    1.44 +   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
    1.45 +                else s mem_string allowed_consts
    1.46 + | a$b => check a andalso check b
    1.47 + | _ => false;
    1.48 +
    1.49 +val conv =
    1.50 +  Simplifier.rewrite
    1.51 +   (HOL_basic_ss addsimps
    1.52 +     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
    1.53 +             @{thm of_int_diff},  @{thm of_int_minus}])@
    1.54 +      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
    1.55 +     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
    1.56 +
    1.57 +fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
    1.58 +val lhss' =
    1.59 +  [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
    1.60 +   @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
    1.61 +   @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
    1.62 +in
    1.63 +val zero_one_idom_simproc =
    1.64 +  make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    1.65 +  proc = sproc, identifier = []}
    1.66 +end;
    1.67 +
    1.68  val add_rules =
    1.69      simp_thms @ arith_simps @ rel_simps @ arith_special @
    1.70      [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
    1.71 @@ -584,7 +643,7 @@
    1.72  
    1.73  val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    1.74  
    1.75 -val Int_Numeral_Base_Simprocs = assoc_fold_simproc
    1.76 +val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
    1.77    :: Int_Numeral_Simprocs.combine_numerals
    1.78    :: Int_Numeral_Simprocs.cancel_numerals;
    1.79