1(* Author: Tobias Nipkow
2
3A special simproc for the instantiation of the generic linear arithmetic package for int.
4*)
5
6signature INT_ARITH =
7sig
8  val zero_one_idom_simproc: simproc
9end
10
11structure Int_Arith : INT_ARITH =
12struct
13
14(* Update parameters of arithmetic prover *)
15
16(* reduce contradictory =/</<= to False *)
17
18(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
19   and m and n are ground terms over rings (roughly speaking).
20   That is, m and n consist only of 1s combined with "+", "-" and "*".
21*)
22
23val zeroth = Thm.symmetric (mk_meta_eq @{thm of_int_0});
24
25val zero_to_of_int_zero_simproc =
26  Simplifier.make_simproc \<^context> "zero_to_of_int_zero_simproc"
27   {lhss = [\<^term>\<open>0::'a::ring\<close>],
28    proc = fn _ => fn _ => fn ct =>
29      let val T = Thm.ctyp_of_cterm ct in
30        if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
31        else SOME (Thm.instantiate' [SOME T] [] zeroth)
32      end};
33
34val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
35
36val one_to_of_int_one_simproc =
37  Simplifier.make_simproc \<^context> "one_to_of_int_one_simproc"
38   {lhss = [\<^term>\<open>1::'a::ring_1\<close>],
39    proc = fn _ => fn _ => fn ct =>
40      let val T = Thm.ctyp_of_cterm ct in
41        if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
42        else SOME (Thm.instantiate' [SOME T] [] oneth)
43      end};
44
45fun check (Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>int\<close>)) = false
46  | check (Const (\<^const_name>\<open>Groups.one\<close>, _)) = true
47  | check (Const (s, _)) = member (op =) [\<^const_name>\<open>HOL.eq\<close>,
48      \<^const_name>\<open>Groups.times\<close>, \<^const_name>\<open>Groups.uminus\<close>,
49      \<^const_name>\<open>Groups.minus\<close>, \<^const_name>\<open>Groups.plus\<close>,
50      \<^const_name>\<open>Groups.zero\<close>,
51      \<^const_name>\<open>Orderings.less\<close>, \<^const_name>\<open>Orderings.less_eq\<close>] s
52  | check (a $ b) = check a andalso check b
53  | check _ = false;
54
55val conv_ss =
56  \<^context>
57  |> put_simpset HOL_basic_ss
58  |> fold (Simplifier.add_simp o (fn th => th RS sym))
59       @{thms of_int_add of_int_mult
60         of_int_diff of_int_minus of_int_less_iff
61         of_int_le_iff of_int_eq_iff}
62  |> (fn ss => ss addsimprocs [zero_to_of_int_zero_simproc, one_to_of_int_one_simproc])
63  |> simpset_of;
64
65val zero_one_idom_simproc =
66  Simplifier.make_simproc \<^context> "zero_one_idom_simproc"
67   {lhss =
68      [\<^term>\<open>(x::'a::ring_char_0) = y\<close>,
69       \<^term>\<open>(x::'a::linordered_idom) < y\<close>,
70       \<^term>\<open>(x::'a::linordered_idom) \<le> y\<close>],
71    proc = fn _ => fn ctxt => fn ct =>
72      if check (Thm.term_of ct)
73      then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
74      else NONE};
75
76end;
77