src/HOL/Library/comm_ring.ML
changeset 17516 45164074dad4
child 18708 4b3dadb4fe33
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/comm_ring.ML	Tue Sep 20 14:10:29 2005 +0200
     1.3 @@ -0,0 +1,142 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Amine Chaieb
     1.6 +
     1.7 +Tactic for solving equalities over commutative rings.
     1.8 +*)
     1.9 +
    1.10 +signature COMM_RING =
    1.11 +sig
    1.12 +  val comm_ring_tac : int -> tactic
    1.13 +  val comm_ring_method: int -> Proof.method
    1.14 +  val algebra_method: int -> Proof.method
    1.15 +  val setup : (theory -> theory) list
    1.16 +end
    1.17 +
    1.18 +structure CommRing: COMM_RING =
    1.19 +struct
    1.20 +
    1.21 +(* The Cring exception for erronous uses of cring_tac *)
    1.22 +exception CRing of string;
    1.23 +
    1.24 +(* Zero and One of the commutative ring *)
    1.25 +fun cring_zero T = Const("0",T);
    1.26 +fun cring_one T = Const("1",T);
    1.27 +
    1.28 +(* reification functions *)
    1.29 +(* add two polynom expressions *)
    1.30 +fun polT t = Type ("Commutative_Ring.pol",[t]);
    1.31 +fun  polexT t = Type("Commutative_Ring.polex",[t]);
    1.32 +val nT = HOLogic.natT;
    1.33 +fun listT T = Type ("List.list",[T]);
    1.34 +
    1.35 +(* Reification of the constructors *)
    1.36 +(* Nat*)
    1.37 +val succ = Const("Suc",nT --> nT);
    1.38 +val zero = Const("0",nT);
    1.39 +val one = Const("1",nT);
    1.40 +
    1.41 +(* Lists *)
    1.42 +fun reif_list T [] = Const("List.list.Nil",listT T)
    1.43 +  | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T)
    1.44 +                             $x$(reif_list T xs);
    1.45 +
    1.46 +(* pol*)
    1.47 +fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t);
    1.48 +fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t);
    1.49 +fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t);
    1.50 +
    1.51 +(* polex *)
    1.52 +fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t);
    1.53 +fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t);
    1.54 +fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t);
    1.55 +fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t);
    1.56 +fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t);
    1.57 +fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t);
    1.58 +(* reification of natural numbers *)
    1.59 +fun reif_nat n =
    1.60 +    if n>0 then succ$(reif_nat (n-1))
    1.61 +    else if n=0 then zero
    1.62 +    else raise CRing "ring_tac: reif_nat negative n";
    1.63 +
    1.64 +(* reification of polynoms : primitive cring expressions *)
    1.65 +fun reif_pol T vs t =
    1.66 +    case t of
    1.67 +       Free(_,_) =>
    1.68 +        let val i = find_index_eq t vs
    1.69 +        in if i = 0
    1.70 +           then (pol_PX T)$((pol_Pc T)$ (cring_one T))
    1.71 +                          $one$((pol_Pc T)$(cring_zero T))
    1.72 +           else (pol_Pinj T)$(reif_nat i)$
    1.73 +                            ((pol_PX T)$((pol_Pc T)$ (cring_one T))
    1.74 +                                       $one$
    1.75 +                                       ((pol_Pc T)$(cring_zero T)))
    1.76 +        end
    1.77 +      | _ => (pol_Pc T)$ t;
    1.78 +
    1.79 +
    1.80 +(* reification of polynom expressions *)
    1.81 +fun reif_polex T vs t =
    1.82 +    case t of
    1.83 +        Const("op +",_)$a$b => (polex_add T)
    1.84 +                                   $ (reif_polex T vs a)$(reif_polex T vs b)
    1.85 +      | Const("op -",_)$a$b => (polex_sub T)
    1.86 +                                   $ (reif_polex T vs a)$(reif_polex T vs b)
    1.87 +      | Const("op *",_)$a$b =>  (polex_mul T)
    1.88 +                                    $ (reif_polex T vs a)$ (reif_polex T vs b)
    1.89 +      | Const("uminus",_)$a => (polex_neg T)
    1.90 +                                   $ (reif_polex T vs a)
    1.91 +      | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
    1.92 +
    1.93 +      | _ => (polex_pol T) $ (reif_pol T vs t);
    1.94 +
    1.95 +(* reification of the equation *)
    1.96 +val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}";
    1.97 +fun reif_eq sg (eq as Const("op =",Type("fun",a::_))$lhs$rhs) =
    1.98 +    if Sign.of_sort (the_context()) (a,cr_sort)
    1.99 +    then
   1.100 +        let val fs = term_frees eq
   1.101 +            val cvs = cterm_of sg (reif_list a fs)
   1.102 +            val clhs = cterm_of sg (reif_polex a fs lhs)
   1.103 +            val crhs = cterm_of sg (reif_polex a fs rhs)
   1.104 +            val ca = ctyp_of sg a
   1.105 +        in (ca,cvs,clhs, crhs)
   1.106 +        end
   1.107 +    else raise CRing "reif_eq: not an equation over comm_ring + recpower"
   1.108 +  | reif_eq sg _ = raise CRing "reif_eq: not an equation";
   1.109 +
   1.110 +(*The cring tactic  *)
   1.111 +(* Attention: You have to make sure that no t^0 is in the goal!! *)
   1.112 +(* Use simply rewriting t^0 = 1 *)
   1.113 +fun cring_ss sg = simpset_of sg
   1.114 +                           addsimps
   1.115 +                           (map thm ["mkPX_def", "mkPinj_def","sub_def",
   1.116 +                                     "power_add","even_def","pow_if"])
   1.117 +                           addsimps [sym OF [thm "power_add"]];
   1.118 +
   1.119 +val norm_eq = thm "norm_eq"
   1.120 +fun comm_ring_tac i =(fn st =>
   1.121 +    let
   1.122 +        val g = List.nth (prems_of st, i - 1)
   1.123 +        val sg = sign_of_thm st
   1.124 +        val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g)
   1.125 +        val norm_eq_th = simplify (cring_ss sg)
   1.126 +                        (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs]
   1.127 +                                                norm_eq)
   1.128 +    in ((cut_rules_tac [norm_eq_th] i)
   1.129 +            THEN (simp_tac (cring_ss sg) i)
   1.130 +            THEN (simp_tac (cring_ss sg) i)) st
   1.131 +    end);
   1.132 +
   1.133 +fun comm_ring_method i = Method.METHOD (fn facts =>
   1.134 +  Method.insert_tac facts 1 THEN comm_ring_tac i);
   1.135 +val algebra_method = comm_ring_method;
   1.136 +
   1.137 +val setup =
   1.138 +  [Method.add_method ("comm_ring",
   1.139 +     Method.no_args (comm_ring_method 1),
   1.140 +     "reflective decision procedure for equalities over commutative rings"),
   1.141 +   Method.add_method ("algebra",
   1.142 +     Method.no_args (algebra_method 1),
   1.143 +     "Method for proving algebraic properties: for now only comm_ring")];
   1.144 +
   1.145 +end;