src/HOL/Library/comm_ring.ML
author nipkow
Thu Oct 29 16:23:57 2009 +0100 (2009-10-29)
changeset 33494 2b5b0f9e271c
parent 32149 ef59550a55d3
permissions -rw-r--r--
Replaced exception CRing by error because it is meant for the user.
     1 (*  Author:     Amine Chaieb
     2 
     3 Tactic for solving equalities over commutative rings.
     4 *)
     5 
     6 signature COMM_RING =
     7 sig
     8   val comm_ring_tac : Proof.context -> int -> tactic
     9   val setup : theory -> theory
    10 end
    11 
    12 structure CommRing: COMM_RING =
    13 struct
    14 
    15 (* Zero and One of the commutative ring *)
    16 fun cring_zero T = Const (@{const_name HOL.zero}, T);
    17 fun cring_one T = Const (@{const_name HOL.one}, T);
    18 
    19 (* reification functions *)
    20 (* add two polynom expressions *)
    21 fun polT t = Type ("Commutative_Ring.pol", [t]);
    22 fun polexT t = Type ("Commutative_Ring.polex", [t]);
    23 
    24 (* pol *)
    25 fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
    26 fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
    27 fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);
    28 
    29 (* polex *)
    30 fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
    31 fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
    32 fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
    33 fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
    34 fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
    35 fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t);
    36 
    37 (* reification of polynoms : primitive cring expressions *)
    38 fun reif_pol T vs (t as Free _) =
    39       let
    40         val one = @{term "1::nat"};
    41         val i = find_index (fn t' => t' = t) vs
    42       in if i = 0
    43         then pol_PX T $ (pol_Pc T $ cring_one T)
    44           $ one $ (pol_Pc T $ cring_zero T)
    45         else pol_Pinj T $ HOLogic.mk_nat i
    46           $ (pol_PX T $ (pol_Pc T $ cring_one T)
    47             $ one $ (pol_Pc T $ cring_zero T))
    48         end
    49   | reif_pol T vs t = pol_Pc T $ t;
    50 
    51 (* reification of polynom expressions *)
    52 fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
    53       polex_add T $ reif_polex T vs a $ reif_polex T vs b
    54   | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
    55       polex_sub T $ reif_polex T vs a $ reif_polex T vs b
    56   | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
    57       polex_mul T $ reif_polex T vs a $ reif_polex T vs b
    58   | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
    59       polex_neg T $ reif_polex T vs a
    60   | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
    61       polex_pow T $ reif_polex T vs a $ n
    62   | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
    63 
    64 (* reification of the equation *)
    65 val cr_sort = @{sort "comm_ring_1"};
    66 
    67 fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
    68       if Sign.of_sort thy (T, cr_sort) then
    69         let
    70           val fs = OldTerm.term_frees eq;
    71           val cvs = cterm_of thy (HOLogic.mk_list T fs);
    72           val clhs = cterm_of thy (reif_polex T fs lhs);
    73           val crhs = cterm_of thy (reif_polex T fs rhs);
    74           val ca = ctyp_of thy T;
    75         in (ca, cvs, clhs, crhs) end
    76       else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
    77   | reif_eq _ _ = error "reif_eq: not an equation";
    78 
    79 (* The cring tactic *)
    80 (* Attention: You have to make sure that no t^0 is in the goal!! *)
    81 (* Use simply rewriting t^0 = 1 *)
    82 val cring_simps =
    83   [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
    84     @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
    85 
    86 fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
    87   let
    88     val thy = ProofContext.theory_of ctxt;
    89     val cring_ss = Simplifier.simpset_of ctxt  (*FIXME really the full simpset!?*)
    90       addsimps cring_simps;
    91     val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
    92     val norm_eq_th =
    93       simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
    94   in
    95     cut_rules_tac [norm_eq_th] i
    96     THEN (simp_tac cring_ss i)
    97     THEN (simp_tac cring_ss i)
    98   end);
    99 
   100 val setup =
   101   Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
   102     "reflective decision procedure for equalities over commutative rings" #>
   103   Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
   104     "method for proving algebraic properties (same as comm_ring)";
   105 
   106 end;