src/HOL/Library/comm_ring.ML

tuned proofs

(*  Author:     Amine Chaieb

Tactic for solving equalities over commutative rings.
*)

signature COMM_RING =
sig
  val comm_ring_tac : Proof.context -> int -> tactic
  val setup : theory -> theory
end

structure CommRing: COMM_RING =
struct

(* The Cring exception for erronous uses of cring_tac *)
exception CRing of string;

(* Zero and One of the commutative ring *)
fun cring_zero T = Const (@{const_name HOL.zero}, T);
fun cring_one T = Const (@{const_name HOL.one}, T);

(* reification functions *)
(* add two polynom expressions *)
fun polT t = Type ("Commutative_Ring.pol", [t]);
fun polexT t = Type ("Commutative_Ring.polex", [t]);

(* pol *)
fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);

(* polex *)
fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t);

(* reification of polynoms : primitive cring expressions *)
fun reif_pol T vs (t as Free _) =
      let
        val one = @{term "1::nat"};
        val i = find_index (fn t' => t' = t) vs
      in if i = 0
        then pol_PX T $ (pol_Pc T $ cring_one T)
          $ one $ (pol_Pc T $ cring_zero T)
        else pol_Pinj T $ HOLogic.mk_nat i
          $ (pol_PX T $ (pol_Pc T $ cring_one T)
            $ one $ (pol_Pc T $ cring_zero T))
        end
  | reif_pol T vs t = pol_Pc T $ t;

(* reification of polynom expressions *)
fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
      polex_add T $ reif_polex T vs a $ reif_polex T vs b
  | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
      polex_sub T $ reif_polex T vs a $ reif_polex T vs b
  | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
      polex_mul T $ reif_polex T vs a $ reif_polex T vs b
  | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
      polex_neg T $ reif_polex T vs a
  | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
      polex_pow T $ reif_polex T vs a $ n
  | reif_polex T vs t = polex_pol T $ reif_pol T vs t;

(* reification of the equation *)
val cr_sort = @{sort "comm_ring_1"};

fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
      if Sign.of_sort thy (T, cr_sort) then
        let
          val fs = OldTerm.term_frees eq;
          val cvs = cterm_of thy (HOLogic.mk_list T fs);
          val clhs = cterm_of thy (reif_polex T fs lhs);
          val crhs = cterm_of thy (reif_polex T fs rhs);
          val ca = ctyp_of thy T;
        in (ca, cvs, clhs, crhs) end
      else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
  | reif_eq _ _ = raise CRing "reif_eq: not an equation";

(* The cring tactic *)
(* Attention: You have to make sure that no t^0 is in the goal!! *)
(* Use simply rewriting t^0 = 1 *)
val cring_simps =
  [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
    @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];

fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
  let
    val thy = ProofContext.theory_of ctxt;
    val cring_ss = Simplifier.simpset_of ctxt  (*FIXME really the full simpset!?*)
      addsimps cring_simps;
    val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
    val norm_eq_th =
      simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
  in
    cut_rules_tac [norm_eq_th] i
    THEN (simp_tac cring_ss i)
    THEN (simp_tac cring_ss i)
  end);

val setup =
  Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
    "reflective decision procedure for equalities over commutative rings" #>
  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
    "method for proving algebraic properties (same as comm_ring)";

end;