author | wenzelm |
Tue, 18 Sep 2007 16:08:00 +0200 | |
changeset 24630 | 351a308ab58d |
parent 23261 | 85f27f79232f |
child 24996 | ebd5f4cc7118 |
permissions | -rw-r--r-- |
17516 | 1 |
(* ID: $Id$ |
2 |
Author: Amine Chaieb |
|
3 |
||
4 |
Tactic for solving equalities over commutative rings. |
|
5 |
*) |
|
6 |
||
7 |
signature COMM_RING = |
|
8 |
sig |
|
20623 | 9 |
val comm_ring_tac : Proof.context -> int -> tactic |
18708 | 10 |
val setup : theory -> theory |
17516 | 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 *) |
|
22997 | 20 |
fun cring_zero T = Const (@{const_name HOL.zero}, T); |
21 |
fun cring_one T = Const (@{const_name HOL.one}, T); |
|
17516 | 22 |
|
23 |
(* reification functions *) |
|
24 |
(* add two polynom expressions *) |
|
22950 | 25 |
fun polT t = Type ("Commutative_Ring.pol", [t]); |
26 |
fun polexT t = Type ("Commutative_Ring.polex", [t]); |
|
17516 | 27 |
|
20623 | 28 |
(* pol *) |
22950 | 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); |
|
17516 | 32 |
|
33 |
(* polex *) |
|
22950 | 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); |
|
17516 | 40 |
|
41 |
(* reification of polynoms : primitive cring expressions *) |
|
22950 | 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) |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23261
diff
changeset
|
49 |
else pol_Pinj T $ HOLogic.mk_nat i |
22950 | 50 |
$ (pol_PX T $ (pol_Pc T $ cring_one T) |
51 |
$ one $ (pol_Pc T $ cring_zero T)) |
|
17516 | 52 |
end |
22950 | 53 |
| reif_pol T vs t = pol_Pc T $ t; |
17516 | 54 |
|
55 |
(* reification of polynom expressions *) |
|
22997 | 56 |
fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) = |
22950 | 57 |
polex_add T $ reif_polex T vs a $ reif_polex T vs b |
22997 | 58 |
| reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) = |
22950 | 59 |
polex_sub T $ reif_polex T vs a $ reif_polex T vs b |
22997 | 60 |
| reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) = |
22950 | 61 |
polex_mul T $ reif_polex T vs a $ reif_polex T vs b |
22997 | 62 |
| reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) = |
22950 | 63 |
polex_neg T $ reif_polex T vs a |
22997 | 64 |
| reif_polex T vs (Const (@{const_name Nat.power}, _) $ a $ n) = |
22950 | 65 |
polex_pow T $ reif_polex T vs a $ n |
66 |
| reif_polex T vs t = polex_pol T $ reif_pol T vs t; |
|
17516 | 67 |
|
68 |
(* reification of the equation *) |
|
22950 | 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) |
|
20623 | 81 |
| reif_eq _ _ = raise CRing "reif_eq: not an equation"; |
17516 | 82 |
|
22950 | 83 |
(* The cring tactic *) |
17516 | 84 |
(* Attention: You have to make sure that no t^0 is in the goal!! *) |
85 |
(* Use simply rewriting t^0 = 1 *) |
|
20623 | 86 |
val cring_simps = |
22950 | 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}]]; |
|
17516 | 89 |
|
20623 | 90 |
fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) => |
91 |
let |
|
22950 | 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; |
|
20623 | 95 |
val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g) |
96 |
val norm_eq_th = |
|
22950 | 97 |
simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq}) |
20623 | 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 = |
|
21588 | 105 |
Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac); |
17516 | 106 |
|
107 |
val setup = |
|
20623 | 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)"); |
|
17516 | 112 |
|
113 |
end; |