src/HOL/Decision_Procs/commutative_ring_tac.ML
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 55793 52c8f934ea6f
child 58645 94bef115c08f
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
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
wenzelm@17516
    10
end
wenzelm@17516
    11
haftmann@33356
    12
structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
wenzelm@17516
    13
struct
wenzelm@17516
    14
wenzelm@17516
    15
(* Zero and One of the commutative ring *)
haftmann@35267
    16
fun cring_zero T = Const (@{const_name Groups.zero}, T);
haftmann@35267
    17
fun cring_one T = Const (@{const_name Groups.one}, T);
wenzelm@17516
    18
wenzelm@17516
    19
(* reification functions *)
wenzelm@17516
    20
(* add two polynom expressions *)
haftmann@33356
    21
fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]);
haftmann@33356
    22
fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
wenzelm@17516
    23
wenzelm@20623
    24
(* pol *)
wenzelm@55793
    25
fun pol_Pc t =
wenzelm@55793
    26
  Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
wenzelm@55793
    27
fun pol_Pinj t =
wenzelm@55793
    28
  Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
wenzelm@55793
    29
fun pol_PX t =
wenzelm@55793
    30
  Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
wenzelm@17516
    31
wenzelm@17516
    32
(* polex *)
wenzelm@55793
    33
fun polex_add t =
wenzelm@55793
    34
  Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
wenzelm@55793
    35
fun polex_sub t =
wenzelm@55793
    36
  Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
wenzelm@55793
    37
fun polex_mul t =
wenzelm@55793
    38
  Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
wenzelm@55793
    39
fun polex_neg t =
wenzelm@55793
    40
  Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
wenzelm@55793
    41
fun polex_pol t =
wenzelm@55793
    42
  Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
wenzelm@55793
    43
fun polex_pow t =
wenzelm@55793
    44
  Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
wenzelm@17516
    45
wenzelm@17516
    46
(* reification of polynoms : primitive cring expressions *)
haftmann@22950
    47
fun reif_pol T vs (t as Free _) =
haftmann@22950
    48
      let
haftmann@22950
    49
        val one = @{term "1::nat"};
haftmann@31986
    50
        val i = find_index (fn t' => t' = t) vs
wenzelm@55793
    51
      in
wenzelm@55793
    52
        if i = 0 then
wenzelm@55793
    53
          pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)
wenzelm@55793
    54
        else
wenzelm@55793
    55
          pol_Pinj T $ HOLogic.mk_nat i $
wenzelm@55793
    56
            (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T))
wenzelm@17516
    57
        end
wenzelm@55793
    58
  | reif_pol T _ t = pol_Pc T $ t;
wenzelm@17516
    59
wenzelm@17516
    60
(* reification of polynom expressions *)
haftmann@35267
    61
fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
haftmann@22950
    62
      polex_add T $ reif_polex T vs a $ reif_polex T vs b
haftmann@35267
    63
  | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
haftmann@22950
    64
      polex_sub T $ reif_polex T vs a $ reif_polex T vs b
haftmann@35267
    65
  | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) =
haftmann@22950
    66
      polex_mul T $ reif_polex T vs a $ reif_polex T vs b
haftmann@35267
    67
  | reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) =
haftmann@22950
    68
      polex_neg T $ reif_polex T vs a
haftmann@24996
    69
  | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
haftmann@22950
    70
      polex_pow T $ reif_polex T vs a $ n
haftmann@22950
    71
  | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
wenzelm@17516
    72
wenzelm@17516
    73
(* reification of the equation *)
wenzelm@55793
    74
val cr_sort = @{sort comm_ring_1};
haftmann@22950
    75
wenzelm@55793
    76
fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
wenzelm@55793
    77
      if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
haftmann@22950
    78
        let
wenzelm@55793
    79
          val thy = Proof_Context.theory_of ctxt;
wenzelm@44121
    80
          val fs = Misc_Legacy.term_frees eq;
haftmann@22950
    81
          val cvs = cterm_of thy (HOLogic.mk_list T fs);
haftmann@22950
    82
          val clhs = cterm_of thy (reif_polex T fs lhs);
haftmann@22950
    83
          val crhs = cterm_of thy (reif_polex T fs rhs);
haftmann@22950
    84
          val ca = ctyp_of thy T;
haftmann@22950
    85
        in (ca, cvs, clhs, crhs) end
wenzelm@55793
    86
      else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
haftmann@33356
    87
  | reif_eq _ _ = error "reif_eq: not an equation";
wenzelm@17516
    88
haftmann@22950
    89
(* The cring tactic *)
wenzelm@17516
    90
(* Attention: You have to make sure that no t^0 is in the goal!! *)
wenzelm@17516
    91
(* Use simply rewriting t^0 = 1 *)
wenzelm@20623
    92
val cring_simps =
wenzelm@55793
    93
  @{thms mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]};
wenzelm@17516
    94
haftmann@33356
    95
fun tac ctxt = SUBGOAL (fn (g, i) =>
wenzelm@20623
    96
  let
wenzelm@51717
    97
    val cring_ctxt = ctxt addsimps cring_simps;  (*FIXME really the full simpset!?*)
wenzelm@55793
    98
    val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
wenzelm@20623
    99
    val norm_eq_th =
wenzelm@55793
   100
      simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
wenzelm@20623
   101
  in
wenzelm@46708
   102
    cut_tac norm_eq_th i
wenzelm@51717
   103
    THEN (simp_tac cring_ctxt i)
wenzelm@51717
   104
    THEN (simp_tac cring_ctxt i)
wenzelm@20623
   105
  end);
wenzelm@20623
   106
wenzelm@17516
   107
end;