1.1 --- a/src/HOL/NatSimprocs.thy Thu Jun 21 15:42:12 2007 +0200
1.2 +++ b/src/HOL/NatSimprocs.thy Thu Jun 21 15:42:13 2007 +0200
1.3 @@ -1,12 +1,13 @@
1.4 (* Title: HOL/NatSimprocs.thy
1.5 ID: $Id$
1.6 - Copyright 2003 TU Muenchen
1.7 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.8 + Author: Amine Chaieb, TU Muenchen
1.9 *)
1.10
1.11 header {*Simprocs for the Naturals*}
1.12
1.13 theory NatSimprocs
1.14 -imports Groebner_Basis
1.15 +imports Groebner_Basis Dense_Linear_Order
1.16 uses
1.17 "~~/src/Provers/Arith/cancel_numeral_factor.ML"
1.18 "~~/src/Provers/Arith/extract_common_term.ML"
1.19 @@ -36,12 +37,12 @@
1.20 text{*No longer required as a simprule because of the @{text inverse_fold}
1.21 simproc*}
1.22 lemma Suc_diff_number_of:
1.23 - "neg (number_of (uminus v)::int) ==>
1.24 + "neg (number_of (uminus v)::int) ==>
1.25 Suc m - (number_of v) = m - (number_of (Numeral.pred v))"
1.26 apply (subst Suc_diff_eq_diff_pred)
1.27 apply simp
1.28 apply (simp del: nat_numeral_1_eq_1)
1.29 -apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
1.30 +apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
1.31 neg_number_of_pred_iff_0)
1.32 done
1.33
1.34 @@ -52,25 +53,25 @@
1.35 subsection{*For @{term nat_case} and @{term nat_rec}*}
1.36
1.37 lemma nat_case_number_of [simp]:
1.38 - "nat_case a f (number_of v) =
1.39 - (let pv = number_of (Numeral.pred v) in
1.40 + "nat_case a f (number_of v) =
1.41 + (let pv = number_of (Numeral.pred v) in
1.42 if neg pv then a else f (nat pv))"
1.43 by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
1.44
1.45 lemma nat_case_add_eq_if [simp]:
1.46 - "nat_case a f ((number_of v) + n) =
1.47 - (let pv = number_of (Numeral.pred v) in
1.48 + "nat_case a f ((number_of v) + n) =
1.49 + (let pv = number_of (Numeral.pred v) in
1.50 if neg pv then nat_case a f n else f (nat pv + n))"
1.51 apply (subst add_eq_if)
1.52 apply (simp split add: nat.split
1.53 del: nat_numeral_1_eq_1
1.54 - add: numeral_1_eq_Suc_0 [symmetric] Let_def
1.55 + add: numeral_1_eq_Suc_0 [symmetric] Let_def
1.56 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
1.57 done
1.58
1.59 lemma nat_rec_number_of [simp]:
1.60 - "nat_rec a f (number_of v) =
1.61 - (let pv = number_of (Numeral.pred v) in
1.62 + "nat_rec a f (number_of v) =
1.63 + (let pv = number_of (Numeral.pred v) in
1.64 if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
1.65 apply (case_tac " (number_of v) ::nat")
1.66 apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
1.67 @@ -78,9 +79,9 @@
1.68 done
1.69
1.70 lemma nat_rec_add_eq_if [simp]:
1.71 - "nat_rec a f (number_of v + n) =
1.72 - (let pv = number_of (Numeral.pred v) in
1.73 - if neg pv then nat_rec a f n
1.74 + "nat_rec a f (number_of v + n) =
1.75 + (let pv = number_of (Numeral.pred v) in
1.76 + if neg pv then nat_rec a f n
1.77 else f (nat pv + n) (nat_rec a f (nat pv + n)))"
1.78 apply (subst add_eq_if)
1.79 apply (simp split add: nat.split
1.80 @@ -123,7 +124,7 @@
1.81
1.82 lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
1.83 apply (subgoal_tac "m mod 2 < 2")
1.84 -apply (force simp del: mod_less_divisor, simp)
1.85 +apply (force simp del: mod_less_divisor, simp)
1.86 done
1.87
1.88 subsubsection{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
1.89 @@ -273,35 +274,35 @@
1.90
1.91 subsubsection{*To Simplify Inequalities Where One Side is the Constant 1*}
1.92
1.93 -lemma less_minus_iff_1 [simp]:
1.94 - fixes b::"'b::{ordered_idom,number_ring}"
1.95 +lemma less_minus_iff_1 [simp]:
1.96 + fixes b::"'b::{ordered_idom,number_ring}"
1.97 shows "(1 < - b) = (b < -1)"
1.98 by auto
1.99
1.100 -lemma le_minus_iff_1 [simp]:
1.101 - fixes b::"'b::{ordered_idom,number_ring}"
1.102 +lemma le_minus_iff_1 [simp]:
1.103 + fixes b::"'b::{ordered_idom,number_ring}"
1.104 shows "(1 \<le> - b) = (b \<le> -1)"
1.105 by auto
1.106
1.107 -lemma equation_minus_iff_1 [simp]:
1.108 - fixes b::"'b::number_ring"
1.109 +lemma equation_minus_iff_1 [simp]:
1.110 + fixes b::"'b::number_ring"
1.111 shows "(1 = - b) = (b = -1)"
1.112 -by (subst equation_minus_iff, auto)
1.113 +by (subst equation_minus_iff, auto)
1.114
1.115 -lemma minus_less_iff_1 [simp]:
1.116 - fixes a::"'b::{ordered_idom,number_ring}"
1.117 +lemma minus_less_iff_1 [simp]:
1.118 + fixes a::"'b::{ordered_idom,number_ring}"
1.119 shows "(- a < 1) = (-1 < a)"
1.120 by auto
1.121
1.122 -lemma minus_le_iff_1 [simp]:
1.123 - fixes a::"'b::{ordered_idom,number_ring}"
1.124 +lemma minus_le_iff_1 [simp]:
1.125 + fixes a::"'b::{ordered_idom,number_ring}"
1.126 shows "(- a \<le> 1) = (-1 \<le> a)"
1.127 by auto
1.128
1.129 -lemma minus_equation_iff_1 [simp]:
1.130 - fixes a::"'b::number_ring"
1.131 +lemma minus_equation_iff_1 [simp]:
1.132 + fixes a::"'b::number_ring"
1.133 shows "(- a = 1) = (a = -1)"
1.134 -by (subst minus_equation_iff, auto)
1.135 +by (subst minus_equation_iff, auto)
1.136
1.137
1.138 subsubsection {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
1.139 @@ -366,7 +367,7 @@
1.140 subsubsection{*Division By @{text "-1"}*}
1.141
1.142 lemma divide_minus1 [simp]:
1.143 - "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
1.144 + "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
1.145 by simp
1.146
1.147 lemma minus1_divide [simp]:
1.148 @@ -392,27 +393,27 @@
1.149 val minus1_divide = @{thm minus1_divide};
1.150 *}
1.151
1.152 +
1.153 section{* Installing Groebner Bases for Fields *}
1.154
1.155 -
1.156 -interpretation class_fieldgb:
1.157 +interpretation class_fieldgb:
1.158 fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
1.159
1.160 lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
1.161 -lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
1.162 +lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
1.163 by simp
1.164 -lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
1.165 +lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
1.166 by simp
1.167 -lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y"
1.168 +lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y"
1.169 by simp
1.170 -lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y"
1.171 +lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y"
1.172 by simp
1.173
1.174 lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
1.175
1.176 -lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
1.177 +lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
1.178 by (simp add: add_divide_distrib)
1.179 -lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
1.180 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
1.181 by (simp add: add_divide_distrib)
1.182
1.183 declaration{*
1.184 @@ -421,28 +422,28 @@
1.185 val zT = ctyp_of_term zr
1.186 val geq = @{cpat "op ="}
1.187 val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
1.188 - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
1.189 + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
1.190 val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
1.191 val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
1.192
1.193 fun prove_nz ctxt =
1.194 - let val ss = local_simpset_of ctxt
1.195 - in fn T => fn t =>
1.196 - let
1.197 - val z = instantiate_cterm ([(zT,T)],[]) zr
1.198 + let val ss = local_simpset_of ctxt
1.199 + in fn T => fn t =>
1.200 + let
1.201 + val z = instantiate_cterm ([(zT,T)],[]) zr
1.202 val eq = instantiate_cterm ([(eqT,T)],[]) geq
1.203 - val th = Simplifier.rewrite (ss addsimps simp_thms)
1.204 - (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
1.205 + val th = Simplifier.rewrite (ss addsimps simp_thms)
1.206 + (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
1.207 (Thm.capply (Thm.capply eq t) z)))
1.208 in equal_elim (symmetric th) TrueI
1.209 end
1.210 end
1.211
1.212 - fun proc ctxt phi ss ct =
1.213 - let
1.214 - val ((x,y),(w,z)) =
1.215 + fun proc ctxt phi ss ct =
1.216 + let
1.217 + val ((x,y),(w,z)) =
1.218 (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
1.219 - val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
1.220 + val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
1.221 val T = ctyp_of_term x
1.222 val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
1.223 val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
1.224 @@ -450,18 +451,18 @@
1.225 end
1.226 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
1.227
1.228 - fun proc2 ctxt phi ss ct =
1.229 - let
1.230 + fun proc2 ctxt phi ss ct =
1.231 + let
1.232 val (l,r) = Thm.dest_binop ct
1.233 val T = ctyp_of_term l
1.234 in (case (term_of l, term_of r) of
1.235 - (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
1.236 + (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
1.237 let val (x,y) = Thm.dest_binop l val z = r
1.238 val _ = map (HOLogic.dest_number o term_of) [x,y,z]
1.239 val ynz = prove_nz ctxt T y
1.240 in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
1.241 end
1.242 - | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
1.243 + | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
1.244 let val (x,y) = Thm.dest_binop r val z = l
1.245 val _ = map (HOLogic.dest_number o term_of) [x,y,z]
1.246 val ynz = prove_nz ctxt T y
1.247 @@ -478,43 +479,43 @@
1.248
1.249 fun proc3 phi ss ct =
1.250 (case term_of ct of
1.251 - Const(@{const_name "Orderings.less"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
1.252 - let
1.253 + Const(@{const_name "Orderings.less"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
1.254 + let
1.255 val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
1.256 val _ = map is_number [a,b,c]
1.257 val T = ctyp_of_term c
1.258 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
1.259 in SOME (mk_meta_eq th) end
1.260 - | Const(@{const_name "Orderings.less_eq"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
1.261 - let
1.262 + | Const(@{const_name "Orderings.less_eq"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
1.263 + let
1.264 val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
1.265 val _ = map is_number [a,b,c]
1.266 val T = ctyp_of_term c
1.267 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
1.268 in SOME (mk_meta_eq th) end
1.269 - | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
1.270 - let
1.271 + | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
1.272 + let
1.273 val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
1.274 val _ = map is_number [a,b,c]
1.275 val T = ctyp_of_term c
1.276 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
1.277 in SOME (mk_meta_eq th) end
1.278 - | Const(@{const_name "Orderings.less"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
1.279 - let
1.280 + | Const(@{const_name "Orderings.less"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
1.281 + let
1.282 val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
1.283 val _ = map is_number [a,b,c]
1.284 val T = ctyp_of_term c
1.285 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
1.286 in SOME (mk_meta_eq th) end
1.287 - | Const(@{const_name "Orderings.less_eq"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
1.288 - let
1.289 + | Const(@{const_name "Orderings.less_eq"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
1.290 + let
1.291 val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
1.292 val _ = map is_number [a,b,c]
1.293 val T = ctyp_of_term c
1.294 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
1.295 in SOME (mk_meta_eq th) end
1.296 - | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
1.297 - let
1.298 + | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
1.299 + let
1.300 val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
1.301 val _ = map is_number [a,b,c]
1.302 val T = ctyp_of_term c
1.303 @@ -523,49 +524,49 @@
1.304 | _ => NONE)
1.305 handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
1.306
1.307 -fun add_frac_frac_simproc ctxt =
1.308 - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
1.309 +fun add_frac_frac_simproc ctxt =
1.310 + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
1.311 name = "add_frac_frac_simproc",
1.312 proc = proc ctxt, identifier = []}
1.313
1.314 -fun add_frac_num_simproc ctxt =
1.315 - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
1.316 +fun add_frac_num_simproc ctxt =
1.317 + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
1.318 name = "add_frac_num_simproc",
1.319 proc = proc2 ctxt, identifier = []}
1.320
1.321 -val ord_frac_simproc =
1.322 - make_simproc
1.323 - {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
1.324 - @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
1.325 - @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
1.326 +val ord_frac_simproc =
1.327 + make_simproc
1.328 + {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
1.329 + @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
1.330 + @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
1.331 @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
1.332 @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
1.333 @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
1.334 name = "ord_frac_simproc", proc = proc3, identifier = []}
1.335
1.336 -val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
1.337 +val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
1.338 "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
1.339
1.340 -val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
1.341 - "add_Suc", "add_number_of_left", "mult_number_of_left",
1.342 +val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
1.343 + "add_Suc", "add_number_of_left", "mult_number_of_left",
1.344 "Suc_eq_add_numeral_1"])@
1.345 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
1.346 - @ arith_simps@ nat_arith @ rel_simps
1.347 -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
1.348 - @{thm "divide_Numeral1"},
1.349 + @ arith_simps@ nat_arith @ rel_simps
1.350 +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
1.351 + @{thm "divide_Numeral1"},
1.352 @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
1.353 @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
1.354 - @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
1.355 - @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
1.356 + @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
1.357 + @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
1.358 @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
1.359 - @{thm "diff_def"}, @{thm "minus_divide_left"},
1.360 + @{thm "diff_def"}, @{thm "minus_divide_left"},
1.361 @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
1.362
1.363 local
1.364 open Conv
1.365 in
1.366 -fun comp_conv ctxt = (Simplifier.rewrite
1.367 -(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
1.368 +fun comp_conv ctxt = (Simplifier.rewrite
1.369 +(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
1.370 addsimps ths addsimps comp_arith addsimps simp_thms
1.371 addsimprocs field_cancel_numeral_factors
1.372 addsimprocs [add_frac_frac_simproc ctxt, add_frac_num_simproc ctxt,
1.373 @@ -575,9 +576,9 @@
1.374 [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
1.375 end
1.376
1.377 -fun numeral_is_const ct =
1.378 - case term_of ct of
1.379 - Const (@{const_name "HOL.divide"},_) $ a $ b =>
1.380 +fun numeral_is_const ct =
1.381 + case term_of ct of
1.382 + Const (@{const_name "HOL.divide"},_) $ a $ b =>
1.383 numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
1.384 | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
1.385 | t => can HOLogic.dest_number t
1.386 @@ -587,16 +588,16 @@
1.387 Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
1.388 | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
1.389
1.390 -fun mk_const phi cT x =
1.391 +fun mk_const phi cT x =
1.392 let val (a, b) = Rat.quotient_of_rat x
1.393 in if b = 1 then Normalizer.mk_cnumber cT a
1.394 - else Thm.capply
1.395 - (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
1.396 + else Thm.capply
1.397 + (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
1.398 (Normalizer.mk_cnumber cT a))
1.399 (Normalizer.mk_cnumber cT b)
1.400 end
1.401
1.402 -in
1.403 +in
1.404 NormalizerData.funs @{thm class_fieldgb.axioms}
1.405 {is_const = K numeral_is_const,
1.406 dest_const = K dest_const,
1.407 @@ -606,4 +607,334 @@
1.408
1.409 *}
1.410
1.411 +
1.412 +subsection {* Instantiation of quantifier elimination in dense linear order
1.413 + (Ferrante and Rackoff algorithm) to linear arithmetic over ordered fields.*}
1.414 +
1.415 +lemma neg_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))"
1.416 +proof-
1.417 + assume H: "c < 0"
1.418 + have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_eq_simps)
1.419 + also have "\<dots> = (0 < x)" by simp
1.420 + finally show "(c*x < 0) == (x > 0)" by simp
1.421 +qed
1.422 +
1.423 +lemma pos_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))"
1.424 +proof-
1.425 + assume H: "c > 0"
1.426 + hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_eq_simps)
1.427 + also have "\<dots> = (0 > x)" by simp
1.428 + finally show "(c*x < 0) == (x < 0)" by simp
1.429 +qed
1.430 +
1.431 +lemma neg_prod_sum_lt: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t< 0) == (x > (- 1/c)*t))"
1.432 +proof-
1.433 + assume H: "c < 0"
1.434 + have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
1.435 + also have "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_eq_simps)
1.436 + also have "\<dots> = ((- 1/c)*t < x)" by simp
1.437 + finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp
1.438 +qed
1.439 +
1.440 +lemma pos_prod_sum_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t < 0) == (x < (- 1/c)*t))"
1.441 +proof-
1.442 + assume H: "c > 0"
1.443 + have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
1.444 + also have "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_eq_simps)
1.445 + also have "\<dots> = ((- 1/c)*t > x)" by simp
1.446 + finally show "(c*x + t < 0) == (x < (- 1/c)*t)" by simp
1.447 +qed
1.448 +
1.449 +lemma sum_lt:"((x::'a::pordered_ab_group_add) + t < 0) == (x < - t)"
1.450 + using less_diff_eq[where a= x and b=t and c=0] by simp
1.451 +
1.452 +lemma neg_prod_le:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))"
1.453 +proof-
1.454 + assume H: "c < 0"
1.455 + have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_eq_simps)
1.456 + also have "\<dots> = (0 <= x)" by simp
1.457 + finally show "(c*x <= 0) == (x >= 0)" by simp
1.458 +qed
1.459 +
1.460 +lemma pos_prod_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))"
1.461 +proof-
1.462 + assume H: "c > 0"
1.463 + hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_eq_simps)
1.464 + also have "\<dots> = (0 >= x)" by simp
1.465 + finally show "(c*x <= 0) == (x <= 0)" by simp
1.466 +qed
1.467 +
1.468 +lemma neg_prod_sum_le: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t <= 0) == (x >= (- 1/c)*t))"
1.469 +proof-
1.470 + assume H: "c < 0"
1.471 + have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
1.472 + also have "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_eq_simps)
1.473 + also have "\<dots> = ((- 1/c)*t <= x)" by simp
1.474 + finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp
1.475 +qed
1.476 +
1.477 +lemma pos_prod_sum_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t <= 0) == (x <= (- 1/c)*t))"
1.478 +proof-
1.479 + assume H: "c > 0"
1.480 + have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
1.481 + also have "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_eq_simps)
1.482 + also have "\<dots> = ((- 1/c)*t >= x)" by simp
1.483 + finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp
1.484 +qed
1.485 +
1.486 +lemma sum_le:"((x::'a::pordered_ab_group_add) + t <= 0) == (x <= - t)"
1.487 + using le_diff_eq[where a= x and b=t and c=0] by simp
1.488 +
1.489 +lemma nz_prod_eq:"(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x = 0) == (x = 0))" by simp
1.490 +lemma nz_prod_sum_eq: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x + t = 0) == (x = (- 1/c)*t))"
1.491 +proof-
1.492 + assume H: "c \<noteq> 0"
1.493 + have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp)
1.494 + also have "\<dots> = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_eq_simps)
1.495 + finally show "(c*x + t = 0) == (x = (- 1/c)*t)" by simp
1.496 +qed
1.497 +lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)"
1.498 + using eq_diff_eq[where a= x and b=t and c=0] by simp
1.499 +
1.500 +
1.501 +interpretation class_ordered_field_dense_linear_order: dense_linear_order
1.502 + ["op <=" "op <"
1.503 + "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
1.504 +proof (unfold_locales,
1.505 + simp_all only: ordered_field_no_ub ordered_field_no_lb,
1.506 + auto simp add: linorder_not_le)
1.507 + fix x y::'a assume lt: "x < y"
1.508 + from less_half_sum[OF lt] show "x < (x + y) /2" by simp
1.509 +next
1.510 + fix x y::'a assume lt: "x < y"
1.511 + from gt_half_sum[OF lt] show "(x + y) /2 < y" by simp
1.512 +qed
1.513 +
1.514 +declaration{*
1.515 +let
1.516 +fun earlier [] x y = false
1.517 + | earlier (h::t) x y =
1.518 + if h aconvc y then false else if h aconvc x then true else earlier t x y;
1.519 +
1.520 +fun dest_frac ct = case term_of ct of
1.521 + Const (@{const_name "HOL.divide"},_) $ a $ b=>
1.522 + Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
1.523 + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
1.524 +
1.525 +fun mk_frac phi cT x =
1.526 + let val (a, b) = Rat.quotient_of_rat x
1.527 + in if b = 1 then Normalizer.mk_cnumber cT a
1.528 + else Thm.capply
1.529 + (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
1.530 + (Normalizer.mk_cnumber cT a))
1.531 + (Normalizer.mk_cnumber cT b)
1.532 + end
1.533 +
1.534 +fun whatis x ct = case term_of ct of
1.535 + Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ =>
1.536 + if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
1.537 + else ("Nox",[])
1.538 +| Const(@{const_name "HOL.plus"}, _)$y$_ =>
1.539 + if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
1.540 + else ("Nox",[])
1.541 +| Const(@{const_name "HOL.times"}, _)$_$y =>
1.542 + if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct])
1.543 + else ("Nox",[])
1.544 +| t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
1.545 +
1.546 +fun xnormalize_conv ctxt [] ct = reflexive ct
1.547 +| xnormalize_conv ctxt (vs as (x::_)) ct =
1.548 + case term_of ct of
1.549 + Const(@{const_name "Orderings.less"},_)$_$Const(@{const_name "HOL.zero"},_) =>
1.550 + (case whatis x (Thm.dest_arg1 ct) of
1.551 + ("c*x+t",[c,t]) =>
1.552 + let
1.553 + val cr = dest_frac c
1.554 + val clt = Thm.dest_fun2 ct
1.555 + val cz = Thm.dest_arg ct
1.556 + val neg = cr </ Rat.zero
1.557 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.558 + (Thm.capply @{cterm "Trueprop"}
1.559 + (if neg then Thm.capply (Thm.capply clt c) cz
1.560 + else Thm.capply (Thm.capply clt cz) c))
1.561 + val cth = equal_elim (symmetric cthp) TrueI
1.562 + val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
1.563 + (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
1.564 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.565 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.566 + in rth end
1.567 + | ("x+t",[t]) =>
1.568 + let
1.569 + val T = ctyp_of_term x
1.570 + val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
1.571 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.572 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.573 + in rth end
1.574 + | ("c*x",[c]) =>
1.575 + let
1.576 + val cr = dest_frac c
1.577 + val clt = Thm.dest_fun2 ct
1.578 + val cz = Thm.dest_arg ct
1.579 + val neg = cr </ Rat.zero
1.580 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.581 + (Thm.capply @{cterm "Trueprop"}
1.582 + (if neg then Thm.capply (Thm.capply clt c) cz
1.583 + else Thm.capply (Thm.capply clt cz) c))
1.584 + val cth = equal_elim (symmetric cthp) TrueI
1.585 + val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
1.586 + (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
1.587 + val rth = th
1.588 + in rth end
1.589 + | _ => reflexive ct)
1.590 +
1.591 +
1.592 +| Const(@{const_name "Orderings.less_eq"},_)$_$Const(@{const_name "HOL.zero"},_) =>
1.593 + (case whatis x (Thm.dest_arg1 ct) of
1.594 + ("c*x+t",[c,t]) =>
1.595 + let
1.596 + val T = ctyp_of_term x
1.597 + val cr = dest_frac c
1.598 + val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
1.599 + val cz = Thm.dest_arg ct
1.600 + val neg = cr </ Rat.zero
1.601 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.602 + (Thm.capply @{cterm "Trueprop"}
1.603 + (if neg then Thm.capply (Thm.capply clt c) cz
1.604 + else Thm.capply (Thm.capply clt cz) c))
1.605 + val cth = equal_elim (symmetric cthp) TrueI
1.606 + val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
1.607 + (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
1.608 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.609 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.610 + in rth end
1.611 + | ("x+t",[t]) =>
1.612 + let
1.613 + val T = ctyp_of_term x
1.614 + val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
1.615 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.616 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.617 + in rth end
1.618 + | ("c*x",[c]) =>
1.619 + let
1.620 + val T = ctyp_of_term x
1.621 + val cr = dest_frac c
1.622 + val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
1.623 + val cz = Thm.dest_arg ct
1.624 + val neg = cr </ Rat.zero
1.625 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.626 + (Thm.capply @{cterm "Trueprop"}
1.627 + (if neg then Thm.capply (Thm.capply clt c) cz
1.628 + else Thm.capply (Thm.capply clt cz) c))
1.629 + val cth = equal_elim (symmetric cthp) TrueI
1.630 + val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
1.631 + (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
1.632 + val rth = th
1.633 + in rth end
1.634 + | _ => reflexive ct)
1.635 +
1.636 +| Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) =>
1.637 + (case whatis x (Thm.dest_arg1 ct) of
1.638 + ("c*x+t",[c,t]) =>
1.639 + let
1.640 + val T = ctyp_of_term x
1.641 + val cr = dest_frac c
1.642 + val ceq = Thm.dest_fun2 ct
1.643 + val cz = Thm.dest_arg ct
1.644 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.645 + (Thm.capply @{cterm "Trueprop"}
1.646 + (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
1.647 + val cth = equal_elim (symmetric cthp) TrueI
1.648 + val th = implies_elim
1.649 + (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
1.650 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.651 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.652 + in rth end
1.653 + | ("x+t",[t]) =>
1.654 + let
1.655 + val T = ctyp_of_term x
1.656 + val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
1.657 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.658 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.659 + in rth end
1.660 + | ("c*x",[c]) =>
1.661 + let
1.662 + val T = ctyp_of_term x
1.663 + val cr = dest_frac c
1.664 + val ceq = Thm.dest_fun2 ct
1.665 + val cz = Thm.dest_arg ct
1.666 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.667 + (Thm.capply @{cterm "Trueprop"}
1.668 + (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
1.669 + val cth = equal_elim (symmetric cthp) TrueI
1.670 + val rth = implies_elim
1.671 + (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
1.672 + in rth end
1.673 + | _ => reflexive ct);
1.674 +
1.675 +local
1.676 + val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
1.677 + val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
1.678 + val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
1.679 +in
1.680 +fun field_isolate_conv phi ctxt vs ct = case term_of ct of
1.681 + Const(@{const_name "Orderings.less"},_)$a$b =>
1.682 + let val (ca,cb) = Thm.dest_binop ct
1.683 + val T = ctyp_of_term ca
1.684 + val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
1.685 + val nth = Conv.fconv_rule
1.686 + (Conv.arg_conv (Conv.arg1_conv
1.687 + (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.688 + val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.689 + in rth end
1.690 +| Const(@{const_name "Orderings.less_eq"},_)$a$b =>
1.691 + let val (ca,cb) = Thm.dest_binop ct
1.692 + val T = ctyp_of_term ca
1.693 + val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
1.694 + val nth = Conv.fconv_rule
1.695 + (Conv.arg_conv (Conv.arg1_conv
1.696 + (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.697 + val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.698 + in rth end
1.699 +
1.700 +| Const("op =",_)$a$b =>
1.701 + let val (ca,cb) = Thm.dest_binop ct
1.702 + val T = ctyp_of_term ca
1.703 + val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
1.704 + val nth = Conv.fconv_rule
1.705 + (Conv.arg_conv (Conv.arg1_conv
1.706 + (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.707 + val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.708 + in rth end
1.709 +| @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
1.710 +| _ => reflexive ct
1.711 +end;
1.712 +
1.713 +fun classfield_whatis phi =
1.714 + let
1.715 + fun h x t =
1.716 + case term_of t of
1.717 + Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
1.718 + else Ferrante_Rackoff_Data.Nox
1.719 + | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
1.720 + else Ferrante_Rackoff_Data.Nox
1.721 + | Const(@{const_name "Orderings.less"},_)$y$z =>
1.722 + if term_of x aconv y then Ferrante_Rackoff_Data.Lt
1.723 + else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
1.724 + else Ferrante_Rackoff_Data.Nox
1.725 + | Const (@{const_name "Orderings.less_eq"},_)$y$z =>
1.726 + if term_of x aconv y then Ferrante_Rackoff_Data.Le
1.727 + else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
1.728 + else Ferrante_Rackoff_Data.Nox
1.729 + | _ => Ferrante_Rackoff_Data.Nox
1.730 + in h end;
1.731 +fun class_field_ss phi =
1.732 + HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
1.733 + addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}]
1.734 +
1.735 +in
1.736 +Ferrante_Rackoff_Data.funs @{thm "class_ordered_field_dense_linear_order.ferrack_axiom"}
1.737 + {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
1.738 end
1.739 +*}
1.740 +
1.741 +end