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