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