src/HOL/Decision_Procs/commutative_ring_tac.ML
changeset 33356 9157d0f9f00e
parent 32149 ef59550a55d3
child 33495 1464ddca182b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Fri Oct 30 13:59:49 2009 +0100
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Author:     Amine Chaieb
     1.5 +
     1.6 +Tactic for solving equalities over commutative rings.
     1.7 +*)
     1.8 +
     1.9 +signature COMMUTATIVE_RING_TAC =
    1.10 +sig
    1.11 +  val tac: Proof.context -> int -> tactic
    1.12 +  val setup: theory -> theory
    1.13 +end
    1.14 +
    1.15 +structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
    1.16 +struct
    1.17 +
    1.18 +(* Zero and One of the commutative ring *)
    1.19 +fun cring_zero T = Const (@{const_name HOL.zero}, T);
    1.20 +fun cring_one T = Const (@{const_name HOL.one}, T);
    1.21 +
    1.22 +(* reification functions *)
    1.23 +(* add two polynom expressions *)
    1.24 +fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]);
    1.25 +fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
    1.26 +
    1.27 +(* pol *)
    1.28 +fun pol_Pc t = Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
    1.29 +fun pol_Pinj t = Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
    1.30 +fun pol_PX t = Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
    1.31 +
    1.32 +(* polex *)
    1.33 +fun polex_add t = Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
    1.34 +fun polex_sub t = Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
    1.35 +fun polex_mul t = Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
    1.36 +fun polex_neg t = Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
    1.37 +fun polex_pol t = Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
    1.38 +fun polex_pow t = Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
    1.39 +
    1.40 +(* reification of polynoms : primitive cring expressions *)
    1.41 +fun reif_pol T vs (t as Free _) =
    1.42 +      let
    1.43 +        val one = @{term "1::nat"};
    1.44 +        val i = find_index (fn t' => t' = t) vs
    1.45 +      in if i = 0
    1.46 +        then pol_PX T $ (pol_Pc T $ cring_one T)
    1.47 +          $ one $ (pol_Pc T $ cring_zero T)
    1.48 +        else pol_Pinj T $ HOLogic.mk_nat i
    1.49 +          $ (pol_PX T $ (pol_Pc T $ cring_one T)
    1.50 +            $ one $ (pol_Pc T $ cring_zero T))
    1.51 +        end
    1.52 +  | reif_pol T vs t = pol_Pc T $ t;
    1.53 +
    1.54 +(* reification of polynom expressions *)
    1.55 +fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
    1.56 +      polex_add T $ reif_polex T vs a $ reif_polex T vs b
    1.57 +  | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
    1.58 +      polex_sub T $ reif_polex T vs a $ reif_polex T vs b
    1.59 +  | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
    1.60 +      polex_mul T $ reif_polex T vs a $ reif_polex T vs b
    1.61 +  | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
    1.62 +      polex_neg T $ reif_polex T vs a
    1.63 +  | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
    1.64 +      polex_pow T $ reif_polex T vs a $ n
    1.65 +  | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
    1.66 +
    1.67 +(* reification of the equation *)
    1.68 +val cr_sort = @{sort "comm_ring_1"};
    1.69 +
    1.70 +fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
    1.71 +      if Sign.of_sort thy (T, cr_sort) then
    1.72 +        let
    1.73 +          val fs = OldTerm.term_frees eq;
    1.74 +          val cvs = cterm_of thy (HOLogic.mk_list T fs);
    1.75 +          val clhs = cterm_of thy (reif_polex T fs lhs);
    1.76 +          val crhs = cterm_of thy (reif_polex T fs rhs);
    1.77 +          val ca = ctyp_of thy T;
    1.78 +        in (ca, cvs, clhs, crhs) end
    1.79 +      else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
    1.80 +  | reif_eq _ _ = error "reif_eq: not an equation";
    1.81 +
    1.82 +(* The cring tactic *)
    1.83 +(* Attention: You have to make sure that no t^0 is in the goal!! *)
    1.84 +(* Use simply rewriting t^0 = 1 *)
    1.85 +val cring_simps =
    1.86 +  [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
    1.87 +    @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
    1.88 +
    1.89 +fun tac ctxt = SUBGOAL (fn (g, i) =>
    1.90 +  let
    1.91 +    val thy = ProofContext.theory_of ctxt;
    1.92 +    val cring_ss = Simplifier.simpset_of ctxt  (*FIXME really the full simpset!?*)
    1.93 +      addsimps cring_simps;
    1.94 +    val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
    1.95 +    val norm_eq_th =
    1.96 +      simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
    1.97 +  in
    1.98 +    cut_rules_tac [norm_eq_th] i
    1.99 +    THEN (simp_tac cring_ss i)
   1.100 +    THEN (simp_tac cring_ss i)
   1.101 +  end);
   1.102 +
   1.103 +val setup =
   1.104 +  Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o tac))
   1.105 +    "reflective decision procedure for equalities over commutative rings";
   1.106 +
   1.107 +end;