# File comm_ring.ML

    (*  ID:         $Id: comm_ring.ML,v 1.1 2005/09/20 12:10:29 wenzelm Exp $
        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;