|
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 : int -> tactic |
|
10 val comm_ring_method: int -> Proof.method |
|
11 val algebra_method: int -> Proof.method |
|
12 val setup : (theory -> theory) list |
|
13 end |
|
14 |
|
15 structure CommRing: COMM_RING = |
|
16 struct |
|
17 |
|
18 (* The Cring exception for erronous uses of cring_tac *) |
|
19 exception CRing of string; |
|
20 |
|
21 (* Zero and One of the commutative ring *) |
|
22 fun cring_zero T = Const("0",T); |
|
23 fun cring_one T = Const("1",T); |
|
24 |
|
25 (* reification functions *) |
|
26 (* add two polynom expressions *) |
|
27 fun polT t = Type ("Commutative_Ring.pol",[t]); |
|
28 fun polexT t = Type("Commutative_Ring.polex",[t]); |
|
29 val nT = HOLogic.natT; |
|
30 fun listT T = Type ("List.list",[T]); |
|
31 |
|
32 (* Reification of the constructors *) |
|
33 (* Nat*) |
|
34 val succ = Const("Suc",nT --> nT); |
|
35 val zero = Const("0",nT); |
|
36 val one = Const("1",nT); |
|
37 |
|
38 (* Lists *) |
|
39 fun reif_list T [] = Const("List.list.Nil",listT T) |
|
40 | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T) |
|
41 $x$(reif_list T xs); |
|
42 |
|
43 (* pol*) |
|
44 fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t); |
|
45 fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t); |
|
46 fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t); |
|
47 |
|
48 (* polex *) |
|
49 fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t); |
|
50 fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t); |
|
51 fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t); |
|
52 fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t); |
|
53 fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t); |
|
54 fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t); |
|
55 (* reification of natural numbers *) |
|
56 fun reif_nat n = |
|
57 if n>0 then succ$(reif_nat (n-1)) |
|
58 else if n=0 then zero |
|
59 else raise CRing "ring_tac: reif_nat negative n"; |
|
60 |
|
61 (* reification of polynoms : primitive cring expressions *) |
|
62 fun reif_pol T vs t = |
|
63 case t of |
|
64 Free(_,_) => |
|
65 let val i = find_index_eq t vs |
|
66 in if i = 0 |
|
67 then (pol_PX T)$((pol_Pc T)$ (cring_one T)) |
|
68 $one$((pol_Pc T)$(cring_zero T)) |
|
69 else (pol_Pinj T)$(reif_nat i)$ |
|
70 ((pol_PX T)$((pol_Pc T)$ (cring_one T)) |
|
71 $one$ |
|
72 ((pol_Pc T)$(cring_zero T))) |
|
73 end |
|
74 | _ => (pol_Pc T)$ t; |
|
75 |
|
76 |
|
77 (* reification of polynom expressions *) |
|
78 fun reif_polex T vs t = |
|
79 case t of |
|
80 Const("op +",_)$a$b => (polex_add T) |
|
81 $ (reif_polex T vs a)$(reif_polex T vs b) |
|
82 | Const("op -",_)$a$b => (polex_sub T) |
|
83 $ (reif_polex T vs a)$(reif_polex T vs b) |
|
84 | Const("op *",_)$a$b => (polex_mul T) |
|
85 $ (reif_polex T vs a)$ (reif_polex T vs b) |
|
86 | Const("uminus",_)$a => (polex_neg T) |
|
87 $ (reif_polex T vs a) |
|
88 | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n |
|
89 |
|
90 | _ => (polex_pol T) $ (reif_pol T vs t); |
|
91 |
|
92 (* reification of the equation *) |
|
93 val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}"; |
|
94 fun reif_eq sg (eq as Const("op =",Type("fun",a::_))$lhs$rhs) = |
|
95 if Sign.of_sort (the_context()) (a,cr_sort) |
|
96 then |
|
97 let val fs = term_frees eq |
|
98 val cvs = cterm_of sg (reif_list a fs) |
|
99 val clhs = cterm_of sg (reif_polex a fs lhs) |
|
100 val crhs = cterm_of sg (reif_polex a fs rhs) |
|
101 val ca = ctyp_of sg a |
|
102 in (ca,cvs,clhs, crhs) |
|
103 end |
|
104 else raise CRing "reif_eq: not an equation over comm_ring + recpower" |
|
105 | reif_eq sg _ = raise CRing "reif_eq: not an equation"; |
|
106 |
|
107 (*The cring tactic *) |
|
108 (* Attention: You have to make sure that no t^0 is in the goal!! *) |
|
109 (* Use simply rewriting t^0 = 1 *) |
|
110 fun cring_ss sg = simpset_of sg |
|
111 addsimps |
|
112 (map thm ["mkPX_def", "mkPinj_def","sub_def", |
|
113 "power_add","even_def","pow_if"]) |
|
114 addsimps [sym OF [thm "power_add"]]; |
|
115 |
|
116 val norm_eq = thm "norm_eq" |
|
117 fun comm_ring_tac i =(fn st => |
|
118 let |
|
119 val g = List.nth (prems_of st, i - 1) |
|
120 val sg = sign_of_thm st |
|
121 val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g) |
|
122 val norm_eq_th = simplify (cring_ss sg) |
|
123 (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] |
|
124 norm_eq) |
|
125 in ((cut_rules_tac [norm_eq_th] i) |
|
126 THEN (simp_tac (cring_ss sg) i) |
|
127 THEN (simp_tac (cring_ss sg) i)) st |
|
128 end); |
|
129 |
|
130 fun comm_ring_method i = Method.METHOD (fn facts => |
|
131 Method.insert_tac facts 1 THEN comm_ring_tac i); |
|
132 val algebra_method = comm_ring_method; |
|
133 |
|
134 val setup = |
|
135 [Method.add_method ("comm_ring", |
|
136 Method.no_args (comm_ring_method 1), |
|
137 "reflective decision procedure for equalities over commutative rings"), |
|
138 Method.add_method ("algebra", |
|
139 Method.no_args (algebra_method 1), |
|
140 "Method for proving algebraic properties: for now only comm_ring")]; |
|
141 |
|
142 end; |