src/HOL/Library/comm_ring.ML
 author chaieb Mon Jun 11 11:06:04 2007 +0200 (2007-06-11) changeset 23315 df3a7e9ebadb parent 23261 85f27f79232f child 24630 351a308ab58d permissions -rw-r--r--
tuned Proof
```     1 (*  ID:         \$Id\$
```
```     2     Author:     Amine Chaieb
```
```     3
```
```     4 Tactic for solving equalities over commutative rings.
```
```     5 *)
```
```     6
```
```     7 signature COMM_RING =
```
```     8 sig
```
```     9   val comm_ring_tac : Proof.context -> int -> tactic
```
```    10   val setup : theory -> theory
```
```    11 end
```
```    12
```
```    13 structure CommRing: COMM_RING =
```
```    14 struct
```
```    15
```
```    16 (* The Cring exception for erronous uses of cring_tac *)
```
```    17 exception CRing of string;
```
```    18
```
```    19 (* Zero and One of the commutative ring *)
```
```    20 fun cring_zero T = Const (@{const_name HOL.zero}, T);
```
```    21 fun cring_one T = Const (@{const_name HOL.one}, T);
```
```    22
```
```    23 (* reification functions *)
```
```    24 (* add two polynom expressions *)
```
```    25 fun polT t = Type ("Commutative_Ring.pol", [t]);
```
```    26 fun polexT t = Type ("Commutative_Ring.polex", [t]);
```
```    27
```
```    28 (* pol *)
```
```    29 fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
```
```    30 fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
```
```    31 fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);
```
```    32
```
```    33 (* polex *)
```
```    34 fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
```
```    35 fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
```
```    36 fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
```
```    37 fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
```
```    38 fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
```
```    39 fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t);
```
```    40
```
```    41 (* reification of polynoms : primitive cring expressions *)
```
```    42 fun reif_pol T vs (t as Free _) =
```
```    43       let
```
```    44         val one = @{term "1::nat"};
```
```    45         val i = find_index_eq t vs
```
```    46       in if i = 0
```
```    47         then pol_PX T \$ (pol_Pc T \$ cring_one T)
```
```    48           \$ one \$ (pol_Pc T \$ cring_zero T)
```
```    49         else pol_Pinj T \$ HOLogic.mk_nat (Integer.int i)
```
```    50           \$ (pol_PX T \$ (pol_Pc T \$ cring_one T)
```
```    51             \$ one \$ (pol_Pc T \$ cring_zero T))
```
```    52         end
```
```    53   | reif_pol T vs t = pol_Pc T \$ t;
```
```    54
```
```    55 (* reification of polynom expressions *)
```
```    56 fun reif_polex T vs (Const (@{const_name HOL.plus}, _) \$ a \$ b) =
```
```    57       polex_add T \$ reif_polex T vs a \$ reif_polex T vs b
```
```    58   | reif_polex T vs (Const (@{const_name HOL.minus}, _) \$ a \$ b) =
```
```    59       polex_sub T \$ reif_polex T vs a \$ reif_polex T vs b
```
```    60   | reif_polex T vs (Const (@{const_name HOL.times}, _) \$ a \$ b) =
```
```    61       polex_mul T \$ reif_polex T vs a \$ reif_polex T vs b
```
```    62   | reif_polex T vs (Const (@{const_name HOL.uminus}, _) \$ a) =
```
```    63       polex_neg T \$ reif_polex T vs a
```
```    64   | reif_polex T vs (Const (@{const_name Nat.power}, _) \$ a \$ n) =
```
```    65       polex_pow T \$ reif_polex T vs a \$ n
```
```    66   | reif_polex T vs t = polex_pol T \$ reif_pol T vs t;
```
```    67
```
```    68 (* reification of the equation *)
```
```    69 val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
```
```    70
```
```    71 fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) \$ lhs \$ rhs) =
```
```    72       if Sign.of_sort thy (T, cr_sort) then
```
```    73         let
```
```    74           val fs = term_frees eq;
```
```    75           val cvs = cterm_of thy (HOLogic.mk_list T fs);
```
```    76           val clhs = cterm_of thy (reif_polex T fs lhs);
```
```    77           val crhs = cterm_of thy (reif_polex T fs rhs);
```
```    78           val ca = ctyp_of thy T;
```
```    79         in (ca, cvs, clhs, crhs) end
```
```    80       else raise CRing ("reif_eq: not an equation over " ^ Sign.string_of_sort thy cr_sort)
```
```    81   | reif_eq _ _ = raise CRing "reif_eq: not an equation";
```
```    82
```
```    83 (* The cring tactic *)
```
```    84 (* Attention: You have to make sure that no t^0 is in the goal!! *)
```
```    85 (* Use simply rewriting t^0 = 1 *)
```
```    86 val cring_simps =
```
```    87   [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
```
```    88     @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
```
```    89
```
```    90 fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
```
```    91   let
```
```    92     val thy = ProofContext.theory_of ctxt;
```
```    93     val cring_ss = Simplifier.local_simpset_of ctxt  (*FIXME really the full simpset!?*)
```
```    94       addsimps cring_simps;
```
```    95     val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
```
```    96     val norm_eq_th =
```
```    97       simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
```
```    98   in
```
```    99     cut_rules_tac [norm_eq_th] i
```
```   100     THEN (simp_tac cring_ss i)
```
```   101     THEN (simp_tac cring_ss i)
```
```   102   end);
```
```   103
```
```   104 val comm_ring_meth =
```
```   105   Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac);
```
```   106
```
```   107 val setup =
```
```   108   Method.add_method ("comm_ring", comm_ring_meth,
```
```   109     "reflective decision procedure for equalities over commutative rings") #>
```
```   110   Method.add_method ("algebra", comm_ring_meth,
```
```   111     "method for proving algebraic properties (same as comm_ring)");
```
```   112
```
```   113 end;
```