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