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