# HG changeset patch # User chaieb # Date 1193829573 -3600 # Node ID 76b9892020d52479052099206dd3f079a22b991a # Parent cc5cf5f1178bd52cfe2814858517fa9f8defd329 exported field_comp_conv: a numerical conversion over fields diff -r cc5cf5f1178b -r 76b9892020d5 src/HOL/Arith_Tools.thy --- 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\ 0 \ z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y" by (simp add: add_divide_distrib) -declaration{* -let + +ML{* +local val zr = @{cpat "0"} val zT = ctyp_of_term zr val geq = @{cpat "op ="} @@ -427,9 +428,7 @@ val add_frac_num = mk_meta_eq @{thm "add_frac_num"} val add_num_frac = mk_meta_eq @{thm "add_num_frac"} - 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 -fun add_frac_frac_simproc ctxt = +val add_frac_frac_simproc = make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], name = "add_frac_frac_simproc", - proc = proc ctxt, identifier = []} + proc = proc, identifier = []} -fun add_frac_num_simproc ctxt = +val add_frac_num_simproc = make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], name = "add_frac_num_simproc", - 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 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} addsimps ths addsimps comp_arith addsimps simp_thms addsimprocs field_cancel_numeral_factors - addsimprocs [add_frac_frac_simproc ctxt, add_frac_num_simproc ctxt, + addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] addcongs [@{thm "if_weak_cong"}])) then_conv (Simplifier.rewrite (HOL_basic_ss addsimps @@ -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 *}