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