1.1 --- a/src/HOL/IsaMakefile Tue Sep 20 14:10:29 2005 +0200
1.2 +++ b/src/HOL/IsaMakefile Tue Sep 20 14:13:20 2005 +0200
1.3 @@ -97,7 +97,7 @@
1.4 Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \
1.5 Tools/ATP/recon_transfer_proof.ML \
1.6 Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \
1.7 - Tools/ATP/watcher.ML Tools/comm_ring.ML \
1.8 + Tools/ATP/watcher.ML \
1.9 Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
1.10 Tools/datatype_codegen.ML Tools/datatype_package.ML \
1.11 Tools/datatype_prop.ML Tools/datatype_realizer.ML \
1.12 @@ -188,7 +188,7 @@
1.13 Library/Library/ROOT.ML Library/Library/document/root.tex \
1.14 Library/Library/document/root.bib Library/While_Combinator.thy \
1.15 Library/Product_ord.thy Library/Char_ord.thy \
1.16 - Library/List_lexord.thy
1.17 + Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML
1.18 @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
1.19
1.20
2.1 --- a/src/HOL/Tools/comm_ring.ML Tue Sep 20 14:10:29 2005 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,142 +0,0 @@
2.4 -(* ID: $Id$
2.5 - Author: Amine Chaieb
2.6 -
2.7 -Tactic for solving equalities over commutative rings.
2.8 -*)
2.9 -
2.10 -signature COMM_RING =
2.11 -sig
2.12 - val comm_ring_tac : int -> tactic
2.13 - val comm_ring_method: int -> Proof.method
2.14 - val algebra_method: int -> Proof.method
2.15 - val setup : (theory -> theory) list
2.16 -end
2.17 -
2.18 -structure CommRing: COMM_RING =
2.19 -struct
2.20 -
2.21 -(* The Cring exception for erronous uses of cring_tac *)
2.22 -exception CRing of string;
2.23 -
2.24 -(* Zero and One of the commutative ring *)
2.25 -fun cring_zero T = Const("0",T);
2.26 -fun cring_one T = Const("1",T);
2.27 -
2.28 -(* reification functions *)
2.29 -(* add two polynom expressions *)
2.30 -fun polT t = Type ("Commutative_Ring.pol",[t]);
2.31 -fun polexT t = Type("Commutative_Ring.polex",[t]);
2.32 -val nT = HOLogic.natT;
2.33 -fun listT T = Type ("List.list",[T]);
2.34 -
2.35 -(* Reification of the constructors *)
2.36 -(* Nat*)
2.37 -val succ = Const("Suc",nT --> nT);
2.38 -val zero = Const("0",nT);
2.39 -val one = Const("1",nT);
2.40 -
2.41 -(* Lists *)
2.42 -fun reif_list T [] = Const("List.list.Nil",listT T)
2.43 - | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T)
2.44 - $x$(reif_list T xs);
2.45 -
2.46 -(* pol*)
2.47 -fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t);
2.48 -fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t);
2.49 -fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t);
2.50 -
2.51 -(* polex *)
2.52 -fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t);
2.53 -fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t);
2.54 -fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t);
2.55 -fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t);
2.56 -fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t);
2.57 -fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t);
2.58 -(* reification of natural numbers *)
2.59 -fun reif_nat n =
2.60 - if n>0 then succ$(reif_nat (n-1))
2.61 - else if n=0 then zero
2.62 - else raise CRing "ring_tac: reif_nat negative n";
2.63 -
2.64 -(* reification of polynoms : primitive cring expressions *)
2.65 -fun reif_pol T vs t =
2.66 - case t of
2.67 - Free(_,_) =>
2.68 - let val i = find_index_eq t vs
2.69 - in if i = 0
2.70 - then (pol_PX T)$((pol_Pc T)$ (cring_one T))
2.71 - $one$((pol_Pc T)$(cring_zero T))
2.72 - else (pol_Pinj T)$(reif_nat i)$
2.73 - ((pol_PX T)$((pol_Pc T)$ (cring_one T))
2.74 - $one$
2.75 - ((pol_Pc T)$(cring_zero T)))
2.76 - end
2.77 - | _ => (pol_Pc T)$ t;
2.78 -
2.79 -
2.80 -(* reification of polynom expressions *)
2.81 -fun reif_polex T vs t =
2.82 - case t of
2.83 - Const("op +",_)$a$b => (polex_add T)
2.84 - $ (reif_polex T vs a)$(reif_polex T vs b)
2.85 - | Const("op -",_)$a$b => (polex_sub T)
2.86 - $ (reif_polex T vs a)$(reif_polex T vs b)
2.87 - | Const("op *",_)$a$b => (polex_mul T)
2.88 - $ (reif_polex T vs a)$ (reif_polex T vs b)
2.89 - | Const("uminus",_)$a => (polex_neg T)
2.90 - $ (reif_polex T vs a)
2.91 - | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
2.92 -
2.93 - | _ => (polex_pol T) $ (reif_pol T vs t);
2.94 -
2.95 -(* reification of the equation *)
2.96 -val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}";
2.97 -fun reif_eq sg (eq as Const("op =",Type("fun",a::_))$lhs$rhs) =
2.98 - if Sign.of_sort (the_context()) (a,cr_sort)
2.99 - then
2.100 - let val fs = term_frees eq
2.101 - val cvs = cterm_of sg (reif_list a fs)
2.102 - val clhs = cterm_of sg (reif_polex a fs lhs)
2.103 - val crhs = cterm_of sg (reif_polex a fs rhs)
2.104 - val ca = ctyp_of sg a
2.105 - in (ca,cvs,clhs, crhs)
2.106 - end
2.107 - else raise CRing "reif_eq: not an equation over comm_ring + recpower"
2.108 - | reif_eq sg _ = raise CRing "reif_eq: not an equation";
2.109 -
2.110 -(*The cring tactic *)
2.111 -(* Attention: You have to make sure that no t^0 is in the goal!! *)
2.112 -(* Use simply rewriting t^0 = 1 *)
2.113 -fun cring_ss sg = simpset_of sg
2.114 - addsimps
2.115 - (map thm ["mkPX_def", "mkPinj_def","sub_def",
2.116 - "power_add","even_def","pow_if"])
2.117 - addsimps [sym OF [thm "power_add"]];
2.118 -
2.119 -val norm_eq = thm "norm_eq"
2.120 -fun comm_ring_tac i =(fn st =>
2.121 - let
2.122 - val g = List.nth (prems_of st, i - 1)
2.123 - val sg = sign_of_thm st
2.124 - val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g)
2.125 - val norm_eq_th = simplify (cring_ss sg)
2.126 - (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs]
2.127 - norm_eq)
2.128 - in ((cut_rules_tac [norm_eq_th] i)
2.129 - THEN (simp_tac (cring_ss sg) i)
2.130 - THEN (simp_tac (cring_ss sg) i)) st
2.131 - end);
2.132 -
2.133 -fun comm_ring_method i = Method.METHOD (fn facts =>
2.134 - Method.insert_tac facts 1 THEN comm_ring_tac i);
2.135 -val algebra_method = comm_ring_method;
2.136 -
2.137 -val setup =
2.138 - [Method.add_method ("comm_ring",
2.139 - Method.no_args (comm_ring_method 1),
2.140 - "reflective decision procedure for equalities over commutative rings"),
2.141 - Method.add_method ("algebra",
2.142 - Method.no_args (algebra_method 1),
2.143 - "Method for proving algebraic properties: for now only comm_ring")];
2.144 -
2.145 -end;