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