# HG changeset patch # User wenzelm # Date 1126728278 -7200 # Node ID 40ce48cc45f74b22995ea170f77b98d4b3d02a73 # Parent b110730a24fdb582306c2a28f84a997ef24a31b5 fixed some ML names; diff -r b110730a24fd -r 40ce48cc45f7 src/HOL/Tools/comm_ring.ML --- a/src/HOL/Tools/comm_ring.ML Wed Sep 14 22:04:37 2005 +0200 +++ b/src/HOL/Tools/comm_ring.ML Wed Sep 14 22:04:38 2005 +0200 @@ -1,14 +1,16 @@ (* ID: $Id$ Author: Amine Chaieb - Tactic for solving equalities over commutative rings *) -signature CRING = +Tactic for solving equalities over commutative rings *) + +signature COMM_RING = sig - val cring_tac : int -> tactic - val cring_method: int -> Proof.method - val setup : (theory -> theory) list + val comm_ring_tac : int -> tactic + val comm_ring_method: int -> Proof.method + val setup : (theory -> theory) list end -structure CommRing :CRING = + +structure CommRing: COMM_RING = struct (* The Cring exception for erronous uses of cring_tac *) @@ -34,7 +36,7 @@ (* Lists *) fun reif_list T [] = Const("List.list.Nil",listT T) | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T) - $x$(reif_list T xs); + $x$(reif_list T xs); (* pol*) fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t); @@ -49,7 +51,7 @@ fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t); fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t); (* reification of natural numbers *) -fun reif_nat n = +fun reif_nat n = if n>0 then succ$(reif_nat (n-1)) else if n=0 then zero else raise CRing "ring_tac: reif_nat negative n"; @@ -58,45 +60,45 @@ fun reif_pol T vs t = case t of Free(_,_) => - let val i = find_index_eq t vs - in if i = 0 - then (pol_PX T)$((pol_Pc T)$ (cring_one T)) - $one$((pol_Pc T)$(cring_zero T)) - else (pol_Pinj T)$(reif_nat i)$ - ((pol_PX T)$((pol_Pc T)$ (cring_one T)) - $one$ - ((pol_Pc T)$(cring_zero T))) - end + let val i = find_index_eq t vs + in if i = 0 + then (pol_PX T)$((pol_Pc T)$ (cring_one T)) + $one$((pol_Pc T)$(cring_zero T)) + else (pol_Pinj T)$(reif_nat i)$ + ((pol_PX T)$((pol_Pc T)$ (cring_one T)) + $one$ + ((pol_Pc T)$(cring_zero T))) + end | _ => (pol_Pc T)$ t; (* reification of polynom expressions *) fun reif_polex T vs t = case t of - Const("op +",_)$a$b => (polex_add T) - $ (reif_polex T vs a)$(reif_polex T vs b) - | Const("op -",_)$a$b => (polex_sub T) - $ (reif_polex T vs a)$(reif_polex T vs b) - | Const("op *",_)$a$b => (polex_mul T) - $ (reif_polex T vs a)$ (reif_polex T vs b) - | Const("uminus",_)$a => (polex_neg T) - $ (reif_polex T vs a) + Const("op +",_)$a$b => (polex_add T) + $ (reif_polex T vs a)$(reif_polex T vs b) + | Const("op -",_)$a$b => (polex_sub T) + $ (reif_polex T vs a)$(reif_polex T vs b) + | Const("op *",_)$a$b => (polex_mul T) + $ (reif_polex T vs a)$ (reif_polex T vs b) + | Const("uminus",_)$a => (polex_neg T) + $ (reif_polex T vs a) | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n | _ => (polex_pol T) $ (reif_pol T vs t); (* reification of the equation *) val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}"; -fun reif_eq sg (eq as Const("op =",Type("fun",a::_))$lhs$rhs) = +fun reif_eq sg (eq as Const("op =",Type("fun",a::_))$lhs$rhs) = if Sign.of_sort (the_context()) (a,cr_sort) - then - let val fs = term_frees eq - val cvs = cterm_of sg (reif_list a fs) - val clhs = cterm_of sg (reif_polex a fs lhs) - val crhs = cterm_of sg (reif_polex a fs rhs) - val ca = ctyp_of sg a - in (ca,cvs,clhs, crhs) - end + then + let val fs = term_frees eq + val cvs = cterm_of sg (reif_list a fs) + val clhs = cterm_of sg (reif_polex a fs lhs) + val crhs = cterm_of sg (reif_polex a fs rhs) + val ca = ctyp_of sg a + in (ca,cvs,clhs, crhs) + end else raise CRing "reif_eq: not an equation over comm_ring + recpower" | reif_eq sg _ = raise CRing "reif_eq: not an equation"; @@ -104,31 +106,31 @@ (* Attention: You have to make sure that no t^0 is in the goal!! *) (* Use simply rewriting t^0 = 1 *) val cring_ss = simpset_of (the_context()) - addsimps - (map thm ["mkPX_def", "mkPinj_def","sub_def", - "power_add","even_def","pow_if"]) - addsimps [sym OF [thm "power_add"]]; + addsimps + (map thm ["mkPX_def", "mkPinj_def","sub_def", + "power_add","even_def","pow_if"]) + addsimps [sym OF [thm "power_add"]]; val norm_eq = thm "norm_eq" -fun comm_ring_tac i =(fn st => +fun comm_ring_tac i =(fn st => let - val g = BasisLibrary.List.nth (prems_of st, i - 1) - val sg = sign_of_thm st - val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g) - val norm_eq_th = simplify cring_ss - (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] - norm_eq) - in ((cut_rules_tac [norm_eq_th] i) - THEN (simp_tac cring_ss i) - THEN (simp_tac cring_ss i)) st + val g = BasisLibrary.List.nth (prems_of st, i - 1) + val sg = sign_of_thm st + val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g) + val norm_eq_th = simplify cring_ss + (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] + norm_eq) + in ((cut_rules_tac [norm_eq_th] i) + THEN (simp_tac cring_ss i) + THEN (simp_tac cring_ss i)) st end); -fun cring_method i = Method.METHOD (fn facts => +fun comm_ring_method i = Method.METHOD (fn facts => Method.insert_tac facts 1 THEN comm_ring_tac i); val setup = [Method.add_method ("comm_ring", - Method.no_args (cring_method 1), + Method.no_args (comm_ring_method 1), "reflective decision procedure for equalities over commutative rings")]; -end; \ No newline at end of file +end;