author chaieb Wed, 31 Oct 2007 12:19:33 +0100 changeset 25249 76b9892020d5 parent 25248 cc5cf5f1178b child 25250 b3a485b98963
exported field_comp_conv: a numerical conversion over fields
 src/HOL/Arith_Tools.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Arith_Tools.thy	Wed Oct 31 10:37:14 2007 +0100
+++ b/src/HOL/Arith_Tools.thy	Wed Oct 31 12:19:33 2007 +0100
@@ -417,8 +417,9 @@
lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"

-declaration{*
-let
+
+ML{*
+local
val zr = @{cpat "0"}
val zT = ctyp_of_term zr
val geq = @{cpat "op ="}
@@ -427,9 +428,7 @@

- fun prove_nz ctxt =
-  let val ss = local_simpset_of ctxt
-  in fn T => fn t =>
+ fun prove_nz ss T t =
let
val z = instantiate_cterm ([(zT,T)],[]) zr
val eq = instantiate_cterm ([(eqT,T)],[]) geq
@@ -438,21 +437,20 @@
(Thm.capply (Thm.capply eq t) z)))
in equal_elim (symmetric th) TrueI
end
-  end

- fun proc ctxt phi ss ct =
+ fun proc phi ss ct =
let
val ((x,y),(w,z)) =
(Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
val T = ctyp_of_term x
-    val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
+    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
in SOME (implies_elim (implies_elim th y_nz) z_nz)
end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE

- fun proc2 ctxt phi ss ct =
+ fun proc2 phi ss ct =
let
val (l,r) = Thm.dest_binop ct
val T = ctyp_of_term l
@@ -460,13 +458,13 @@
(Const(@{const_name "HOL.divide"},_)\$_\$_, _) =>
let val (x,y) = Thm.dest_binop l val z = r
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
-            val ynz = prove_nz ctxt T y
+            val ynz = prove_nz ss T y
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
end
| (_, Const (@{const_name "HOL.divide"},_)\$_\$_) =>
let val (x,y) = Thm.dest_binop r val z = l
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
-            val ynz = prove_nz ctxt T y
+            val ynz = prove_nz ss T y
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
end
| _ => NONE)
@@ -525,15 +523,15 @@
| _ => NONE)
handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE

make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
-                     proc = proc ctxt, identifier = []}
+                     proc = proc, identifier = []}

make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
-                     proc = proc2 ctxt, identifier = []}
+                     proc = proc2, identifier = []}

val ord_frac_simproc =
make_simproc
@@ -566,11 +564,11 @@
local
open Conv
in
-fun comp_conv ctxt = (Simplifier.rewrite
+val comp_conv = (Simplifier.rewrite
ord_frac_simproc]
@@ -600,14 +598,17 @@
end

in
- NormalizerData.funs @{thm class_fieldgb.axioms}
+ val field_comp_conv = comp_conv;
+ val fieldgb_declaration =
+  NormalizerData.funs @{thm class_fieldgb.axioms}
{is_const = K numeral_is_const,
dest_const = K dest_const,
mk_const = mk_const,
-    conv = K comp_conv}
-end
+    conv = K (K comp_conv)}
+end;
+*}

-*}
+declaration{* fieldgb_declaration *}

subsection {* Ferrante and Rackoff algorithm over ordered fields *}