src/HOL/Decision_Procs/commutative_ring_tac.ML
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51474 1e9e68247ad1 parent 47432 e1576d13e933 child 51717 9e7d1c139569 permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
```     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 = Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
```
```    26 fun pol_Pinj t = Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
```
```    27 fun pol_PX t = Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
```
```    28
```
```    29 (* polex *)
```
```    30 fun polex_add t = Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
```
```    31 fun polex_sub t = Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
```
```    32 fun polex_mul t = Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
```
```    33 fun polex_neg t = Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
```
```    34 fun polex_pol t = Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
```
```    35 fun polex_pow t = Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
```
```    36
```
```    37 (* reification of polynoms : primitive cring expressions *)
```
```    38 fun reif_pol T vs (t as Free _) =
```
```    39       let
```
```    40         val one = @{term "1::nat"};
```
```    41         val i = find_index (fn t' => t' = t) vs
```
```    42       in if i = 0
```
```    43         then pol_PX T \$ (pol_Pc T \$ cring_one T)
```
```    44           \$ one \$ (pol_Pc T \$ cring_zero T)
```
```    45         else pol_Pinj T \$ HOLogic.mk_nat i
```
```    46           \$ (pol_PX T \$ (pol_Pc T \$ cring_one T)
```
```    47             \$ one \$ (pol_Pc T \$ cring_zero T))
```
```    48         end
```
```    49   | reif_pol T vs t = pol_Pc T \$ t;
```
```    50
```
```    51 (* reification of polynom expressions *)
```
```    52 fun reif_polex T vs (Const (@{const_name Groups.plus}, _) \$ a \$ b) =
```
```    53       polex_add T \$ reif_polex T vs a \$ reif_polex T vs b
```
```    54   | reif_polex T vs (Const (@{const_name Groups.minus}, _) \$ a \$ b) =
```
```    55       polex_sub T \$ reif_polex T vs a \$ reif_polex T vs b
```
```    56   | reif_polex T vs (Const (@{const_name Groups.times}, _) \$ a \$ b) =
```
```    57       polex_mul T \$ reif_polex T vs a \$ reif_polex T vs b
```
```    58   | reif_polex T vs (Const (@{const_name Groups.uminus}, _) \$ a) =
```
```    59       polex_neg T \$ reif_polex T vs a
```
```    60   | reif_polex T vs (Const (@{const_name Power.power}, _) \$ a \$ n) =
```
```    61       polex_pow T \$ reif_polex T vs a \$ n
```
```    62   | reif_polex T vs t = polex_pol T \$ reif_pol T vs t;
```
```    63
```
```    64 (* reification of the equation *)
```
```    65 val cr_sort = @{sort "comm_ring_1"};
```
```    66
```
```    67 fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) \$ lhs \$ rhs) =
```
```    68       if Sign.of_sort thy (T, cr_sort) then
```
```    69         let
```
```    70           val fs = Misc_Legacy.term_frees eq;
```
```    71           val cvs = cterm_of thy (HOLogic.mk_list T fs);
```
```    72           val clhs = cterm_of thy (reif_polex T fs lhs);
```
```    73           val crhs = cterm_of thy (reif_polex T fs rhs);
```
```    74           val ca = ctyp_of thy T;
```
```    75         in (ca, cvs, clhs, crhs) end
```
```    76       else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
```
```    77   | reif_eq _ _ = error "reif_eq: not an equation";
```
```    78
```
```    79 (* The cring tactic *)
```
```    80 (* Attention: You have to make sure that no t^0 is in the goal!! *)
```
```    81 (* Use simply rewriting t^0 = 1 *)
```
```    82 val cring_simps =
```
```    83   [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
```
```    84     @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
```
```    85
```
```    86 fun tac ctxt = SUBGOAL (fn (g, i) =>
```
```    87   let
```
```    88     val thy = Proof_Context.theory_of ctxt;
```
```    89     val cring_ss = Simplifier.simpset_of ctxt  (*FIXME really the full simpset!?*)
```
```    90       addsimps cring_simps;
```
```    91     val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
```
```    92     val norm_eq_th =
```
```    93       simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
```
```    94   in
```
```    95     cut_tac norm_eq_th i
```
```    96     THEN (simp_tac cring_ss i)
```
```    97     THEN (simp_tac cring_ss i)
```
```    98   end);
```
```    99
```
```   100 end;
```