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