moved Tools/comm_ring.ML to Library;
authorwenzelm
Tue Sep 20 14:13:20 2005 +0200 (2005-09-20)
changeset 175179dc9d3005ed2
parent 17516 45164074dad4
child 17518 87b49367ee9b
moved Tools/comm_ring.ML to Library;
src/HOL/IsaMakefile
src/HOL/Tools/comm_ring.ML
     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;