src/HOL/Library/comm_ring.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17516 45164074dad4
child 19233 77ca20b0ed77
permissions -rw-r--r--
setup: theory -> theory;
     1 (*  ID:         $Id$
     2     Author:     Amine Chaieb
     3 
     4 Tactic for solving equalities over commutative rings.
     5 *)
     6 
     7 signature COMM_RING =
     8 sig
     9   val comm_ring_tac : int -> tactic
    10   val comm_ring_method: int -> Proof.method
    11   val algebra_method: int -> Proof.method
    12   val setup : theory -> theory
    13 end
    14 
    15 structure CommRing: COMM_RING =
    16 struct
    17 
    18 (* The Cring exception for erronous uses of cring_tac *)
    19 exception CRing of string;
    20 
    21 (* Zero and One of the commutative ring *)
    22 fun cring_zero T = Const("0",T);
    23 fun cring_one T = Const("1",T);
    24 
    25 (* reification functions *)
    26 (* add two polynom expressions *)
    27 fun polT t = Type ("Commutative_Ring.pol",[t]);
    28 fun  polexT t = Type("Commutative_Ring.polex",[t]);
    29 val nT = HOLogic.natT;
    30 fun listT T = Type ("List.list",[T]);
    31 
    32 (* Reification of the constructors *)
    33 (* Nat*)
    34 val succ = Const("Suc",nT --> nT);
    35 val zero = Const("0",nT);
    36 val one = Const("1",nT);
    37 
    38 (* Lists *)
    39 fun reif_list T [] = Const("List.list.Nil",listT T)
    40   | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T)
    41                              $x$(reif_list T xs);
    42 
    43 (* pol*)
    44 fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t);
    45 fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t);
    46 fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t);
    47 
    48 (* polex *)
    49 fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t);
    50 fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t);
    51 fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t);
    52 fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t);
    53 fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t);
    54 fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t);
    55 (* reification of natural numbers *)
    56 fun reif_nat n =
    57     if n>0 then succ$(reif_nat (n-1))
    58     else if n=0 then zero
    59     else raise CRing "ring_tac: reif_nat negative n";
    60 
    61 (* reification of polynoms : primitive cring expressions *)
    62 fun reif_pol T vs t =
    63     case t of
    64        Free(_,_) =>
    65         let val i = find_index_eq t vs
    66         in if i = 0
    67            then (pol_PX T)$((pol_Pc T)$ (cring_one T))
    68                           $one$((pol_Pc T)$(cring_zero T))
    69            else (pol_Pinj T)$(reif_nat i)$
    70                             ((pol_PX T)$((pol_Pc T)$ (cring_one T))
    71                                        $one$
    72                                        ((pol_Pc T)$(cring_zero T)))
    73         end
    74       | _ => (pol_Pc T)$ t;
    75 
    76 
    77 (* reification of polynom expressions *)
    78 fun reif_polex T vs t =
    79     case t of
    80         Const("op +",_)$a$b => (polex_add T)
    81                                    $ (reif_polex T vs a)$(reif_polex T vs b)
    82       | Const("op -",_)$a$b => (polex_sub T)
    83                                    $ (reif_polex T vs a)$(reif_polex T vs b)
    84       | Const("op *",_)$a$b =>  (polex_mul T)
    85                                     $ (reif_polex T vs a)$ (reif_polex T vs b)
    86       | Const("uminus",_)$a => (polex_neg T)
    87                                    $ (reif_polex T vs a)
    88       | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
    89 
    90       | _ => (polex_pol T) $ (reif_pol T vs t);
    91 
    92 (* reification of the equation *)
    93 val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}";
    94 fun reif_eq sg (eq as Const("op =",Type("fun",a::_))$lhs$rhs) =
    95     if Sign.of_sort (the_context()) (a,cr_sort)
    96     then
    97         let val fs = term_frees eq
    98             val cvs = cterm_of sg (reif_list a fs)
    99             val clhs = cterm_of sg (reif_polex a fs lhs)
   100             val crhs = cterm_of sg (reif_polex a fs rhs)
   101             val ca = ctyp_of sg a
   102         in (ca,cvs,clhs, crhs)
   103         end
   104     else raise CRing "reif_eq: not an equation over comm_ring + recpower"
   105   | reif_eq sg _ = raise CRing "reif_eq: not an equation";
   106 
   107 (*The cring tactic  *)
   108 (* Attention: You have to make sure that no t^0 is in the goal!! *)
   109 (* Use simply rewriting t^0 = 1 *)
   110 fun cring_ss sg = simpset_of sg
   111                            addsimps
   112                            (map thm ["mkPX_def", "mkPinj_def","sub_def",
   113                                      "power_add","even_def","pow_if"])
   114                            addsimps [sym OF [thm "power_add"]];
   115 
   116 val norm_eq = thm "norm_eq"
   117 fun comm_ring_tac i =(fn st =>
   118     let
   119         val g = List.nth (prems_of st, i - 1)
   120         val sg = sign_of_thm st
   121         val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g)
   122         val norm_eq_th = simplify (cring_ss sg)
   123                         (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs]
   124                                                 norm_eq)
   125     in ((cut_rules_tac [norm_eq_th] i)
   126             THEN (simp_tac (cring_ss sg) i)
   127             THEN (simp_tac (cring_ss sg) i)) st
   128     end);
   129 
   130 fun comm_ring_method i = Method.METHOD (fn facts =>
   131   Method.insert_tac facts 1 THEN comm_ring_tac i);
   132 val algebra_method = comm_ring_method;
   133 
   134 val setup =
   135   Method.add_method ("comm_ring",
   136      Method.no_args (comm_ring_method 1),
   137      "reflective decision procedure for equalities over commutative rings") #>
   138   Method.add_method ("algebra",
   139      Method.no_args (algebra_method 1),
   140      "Method for proving algebraic properties: for now only comm_ring");
   141 
   142 end;