--- a/src/HOL/IsaMakefile Tue Sep 20 14:10:29 2005 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 20 14:13:20 2005 +0200
@@ -97,7 +97,7 @@
Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \
Tools/ATP/recon_transfer_proof.ML \
Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \
- Tools/ATP/watcher.ML Tools/comm_ring.ML \
+ Tools/ATP/watcher.ML \
Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
Tools/datatype_codegen.ML Tools/datatype_package.ML \
Tools/datatype_prop.ML Tools/datatype_realizer.ML \
@@ -188,7 +188,7 @@
Library/Library/ROOT.ML Library/Library/document/root.tex \
Library/Library/document/root.bib Library/While_Combinator.thy \
Library/Product_ord.thy Library/Char_ord.thy \
- Library/List_lexord.thy
+ Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML
@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
--- a/src/HOL/Tools/comm_ring.ML Tue Sep 20 14:10:29 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-(* ID: $Id$
- Author: Amine Chaieb
-
-Tactic for solving equalities over commutative rings.
-*)
-
-signature COMM_RING =
-sig
- val comm_ring_tac : int -> tactic
- val comm_ring_method: int -> Proof.method
- val algebra_method: int -> Proof.method
- val setup : (theory -> theory) list
-end
-
-structure CommRing: COMM_RING =
-struct
-
-(* The Cring exception for erronous uses of cring_tac *)
-exception CRing of string;
-
-(* Zero and One of the commutative ring *)
-fun cring_zero T = Const("0",T);
-fun cring_one T = Const("1",T);
-
-(* reification functions *)
-(* add two polynom expressions *)
-fun polT t = Type ("Commutative_Ring.pol",[t]);
-fun polexT t = Type("Commutative_Ring.polex",[t]);
-val nT = HOLogic.natT;
-fun listT T = Type ("List.list",[T]);
-
-(* Reification of the constructors *)
-(* Nat*)
-val succ = Const("Suc",nT --> nT);
-val zero = Const("0",nT);
-val one = Const("1",nT);
-
-(* 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);
-
-(* pol*)
-fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t);
-fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t);
-fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t);
-
-(* polex *)
-fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t);
-fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t);
-fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t);
-fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t);
-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 =
- if n>0 then succ$(reif_nat (n-1))
- else if n=0 then zero
- else raise CRing "ring_tac: reif_nat negative n";
-
-(* reification of polynoms : primitive cring expressions *)
-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
- | _ => (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("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) =
- 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
- else raise CRing "reif_eq: not an equation over comm_ring + recpower"
- | reif_eq sg _ = raise CRing "reif_eq: not an equation";
-
-(*The cring tactic *)
-(* Attention: You have to make sure that no t^0 is in the goal!! *)
-(* Use simply rewriting t^0 = 1 *)
-fun cring_ss sg = simpset_of sg
- 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 =>
- let
- val g = 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 sg)
- (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs]
- norm_eq)
- in ((cut_rules_tac [norm_eq_th] i)
- THEN (simp_tac (cring_ss sg) i)
- THEN (simp_tac (cring_ss sg) i)) st
- end);
-
-fun comm_ring_method i = Method.METHOD (fn facts =>
- Method.insert_tac facts 1 THEN comm_ring_tac i);
-val algebra_method = comm_ring_method;
-
-val setup =
- [Method.add_method ("comm_ring",
- Method.no_args (comm_ring_method 1),
- "reflective decision procedure for equalities over commutative rings"),
- Method.add_method ("algebra",
- Method.no_args (algebra_method 1),
- "Method for proving algebraic properties: for now only comm_ring")];
-
-end;