author | wenzelm |
Wed, 12 Mar 2014 17:25:28 +0100 | |
changeset 56066 | cce36efe32eb |
parent 55793 | 52c8f934ea6f |
child 58645 | 94bef115c08f |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Decision_Procs/commutative_ring_tac.ML |
2 |
Author: Amine Chaieb |
|
17516 | 3 |
|
4 |
Tactic for solving equalities over commutative rings. |
|
5 |
*) |
|
6 |
||
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
7 |
signature COMMUTATIVE_RING_TAC = |
17516 | 8 |
sig |
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
9 |
val tac: Proof.context -> int -> tactic |
17516 | 10 |
end |
11 |
||
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
12 |
structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC = |
17516 | 13 |
struct |
14 |
||
15 |
(* Zero and One of the commutative ring *) |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
16 |
fun cring_zero T = Const (@{const_name Groups.zero}, T); |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
17 |
fun cring_one T = Const (@{const_name Groups.one}, T); |
17516 | 18 |
|
19 |
(* reification functions *) |
|
20 |
(* add two polynom expressions *) |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
21 |
fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
22 |
fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]); |
17516 | 23 |
|
20623 | 24 |
(* pol *) |
55793 | 25 |
fun pol_Pc t = |
26 |
Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t); |
|
27 |
fun pol_Pinj t = |
|
28 |
Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t); |
|
29 |
fun pol_PX t = |
|
30 |
Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t); |
|
17516 | 31 |
|
32 |
(* polex *) |
|
55793 | 33 |
fun polex_add t = |
34 |
Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t); |
|
35 |
fun polex_sub t = |
|
36 |
Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t); |
|
37 |
fun polex_mul t = |
|
38 |
Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t); |
|
39 |
fun polex_neg t = |
|
40 |
Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t); |
|
41 |
fun polex_pol t = |
|
42 |
Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t); |
|
43 |
fun polex_pow t = |
|
44 |
Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t); |
|
17516 | 45 |
|
46 |
(* reification of polynoms : primitive cring expressions *) |
|
22950 | 47 |
fun reif_pol T vs (t as Free _) = |
48 |
let |
|
49 |
val one = @{term "1::nat"}; |
|
31986 | 50 |
val i = find_index (fn t' => t' = t) vs |
55793 | 51 |
in |
52 |
if i = 0 then |
|
53 |
pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T) |
|
54 |
else |
|
55 |
pol_Pinj T $ HOLogic.mk_nat i $ |
|
56 |
(pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)) |
|
17516 | 57 |
end |
55793 | 58 |
| reif_pol T _ t = pol_Pc T $ t; |
17516 | 59 |
|
60 |
(* reification of polynom expressions *) |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
61 |
fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) = |
22950 | 62 |
polex_add T $ reif_polex T vs a $ reif_polex T vs b |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
63 |
| reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) = |
22950 | 64 |
polex_sub T $ reif_polex T vs a $ reif_polex T vs b |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
65 |
| reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) = |
22950 | 66 |
polex_mul T $ reif_polex T vs a $ reif_polex T vs b |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
67 |
| reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) = |
22950 | 68 |
polex_neg T $ reif_polex T vs a |
24996 | 69 |
| reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) = |
22950 | 70 |
polex_pow T $ reif_polex T vs a $ n |
71 |
| reif_polex T vs t = polex_pol T $ reif_pol T vs t; |
|
17516 | 72 |
|
73 |
(* reification of the equation *) |
|
55793 | 74 |
val cr_sort = @{sort comm_ring_1}; |
22950 | 75 |
|
55793 | 76 |
fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) = |
77 |
if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then |
|
22950 | 78 |
let |
55793 | 79 |
val thy = Proof_Context.theory_of ctxt; |
44121 | 80 |
val fs = Misc_Legacy.term_frees eq; |
22950 | 81 |
val cvs = cterm_of thy (HOLogic.mk_list T fs); |
82 |
val clhs = cterm_of thy (reif_polex T fs lhs); |
|
83 |
val crhs = cterm_of thy (reif_polex T fs rhs); |
|
84 |
val ca = ctyp_of thy T; |
|
85 |
in (ca, cvs, clhs, crhs) end |
|
55793 | 86 |
else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort) |
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
87 |
| reif_eq _ _ = error "reif_eq: not an equation"; |
17516 | 88 |
|
22950 | 89 |
(* The cring tactic *) |
17516 | 90 |
(* Attention: You have to make sure that no t^0 is in the goal!! *) |
91 |
(* Use simply rewriting t^0 = 1 *) |
|
20623 | 92 |
val cring_simps = |
55793 | 93 |
@{thms mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]}; |
17516 | 94 |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
95 |
fun tac ctxt = SUBGOAL (fn (g, i) => |
20623 | 96 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
97 |
val cring_ctxt = ctxt addsimps cring_simps; (*FIXME really the full simpset!?*) |
55793 | 98 |
val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g); |
20623 | 99 |
val norm_eq_th = |
55793 | 100 |
simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq}); |
20623 | 101 |
in |
46708
b138dee7bed3
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents:
44121
diff
changeset
|
102 |
cut_tac norm_eq_th i |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
103 |
THEN (simp_tac cring_ctxt i) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
104 |
THEN (simp_tac cring_ctxt i) |
20623 | 105 |
end); |
106 |
||
17516 | 107 |
end; |