src/HOL/Library/comm_ring.ML
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 23261 85f27f79232f
child 24630 351a308ab58d
permissions -rw-r--r--
tuned Proof
     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 : Proof.context -> int -> tactic
    10   val setup : theory -> theory
    11 end
    12 
    13 structure CommRing: COMM_RING =
    14 struct
    15 
    16 (* The Cring exception for erronous uses of cring_tac *)
    17 exception CRing of string;
    18 
    19 (* Zero and One of the commutative ring *)
    20 fun cring_zero T = Const (@{const_name HOL.zero}, T);
    21 fun cring_one T = Const (@{const_name HOL.one}, T);
    22 
    23 (* reification functions *)
    24 (* add two polynom expressions *)
    25 fun polT t = Type ("Commutative_Ring.pol", [t]);
    26 fun polexT t = Type ("Commutative_Ring.polex", [t]);
    27 
    28 (* pol *)
    29 fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
    30 fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
    31 fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);
    32 
    33 (* polex *)
    34 fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
    35 fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
    36 fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
    37 fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
    38 fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
    39 fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t);
    40 
    41 (* reification of polynoms : primitive cring expressions *)
    42 fun reif_pol T vs (t as Free _) =
    43       let
    44         val one = @{term "1::nat"};
    45         val i = find_index_eq t vs
    46       in if i = 0
    47         then pol_PX T $ (pol_Pc T $ cring_one T)
    48           $ one $ (pol_Pc T $ cring_zero T)
    49         else pol_Pinj T $ HOLogic.mk_nat (Integer.int i)
    50           $ (pol_PX T $ (pol_Pc T $ cring_one T)
    51             $ one $ (pol_Pc T $ cring_zero T))
    52         end
    53   | reif_pol T vs t = pol_Pc T $ t;
    54 
    55 (* reification of polynom expressions *)
    56 fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
    57       polex_add T $ reif_polex T vs a $ reif_polex T vs b
    58   | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
    59       polex_sub T $ reif_polex T vs a $ reif_polex T vs b
    60   | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
    61       polex_mul T $ reif_polex T vs a $ reif_polex T vs b
    62   | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
    63       polex_neg T $ reif_polex T vs a
    64   | reif_polex T vs (Const (@{const_name Nat.power}, _) $ a $ n) =
    65       polex_pow T $ reif_polex T vs a $ n
    66   | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
    67 
    68 (* reification of the equation *)
    69 val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
    70 
    71 fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
    72       if Sign.of_sort thy (T, cr_sort) then
    73         let
    74           val fs = term_frees eq;
    75           val cvs = cterm_of thy (HOLogic.mk_list T fs);
    76           val clhs = cterm_of thy (reif_polex T fs lhs);
    77           val crhs = cterm_of thy (reif_polex T fs rhs);
    78           val ca = ctyp_of thy T;
    79         in (ca, cvs, clhs, crhs) end
    80       else raise CRing ("reif_eq: not an equation over " ^ Sign.string_of_sort thy cr_sort)
    81   | reif_eq _ _ = raise CRing "reif_eq: not an equation";
    82 
    83 (* The cring tactic *)
    84 (* Attention: You have to make sure that no t^0 is in the goal!! *)
    85 (* Use simply rewriting t^0 = 1 *)
    86 val cring_simps =
    87   [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
    88     @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
    89 
    90 fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
    91   let
    92     val thy = ProofContext.theory_of ctxt;
    93     val cring_ss = Simplifier.local_simpset_of ctxt  (*FIXME really the full simpset!?*)
    94       addsimps cring_simps;
    95     val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
    96     val norm_eq_th =
    97       simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
    98   in
    99     cut_rules_tac [norm_eq_th] i
   100     THEN (simp_tac cring_ss i)
   101     THEN (simp_tac cring_ss i)
   102   end);
   103 
   104 val comm_ring_meth =
   105   Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac);
   106 
   107 val setup =
   108   Method.add_method ("comm_ring", comm_ring_meth,
   109     "reflective decision procedure for equalities over commutative rings") #>
   110   Method.add_method ("algebra", comm_ring_meth,
   111     "method for proving algebraic properties (same as comm_ring)");
   112 
   113 end;