author | wenzelm |
Wed, 27 Mar 2013 21:25:33 +0100 | |
changeset 51564 | bfdc3f720bd6 |
parent 47432 | e1576d13e933 |
child 51717 | 9e7d1c139569 |
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 *) |
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
25 |
fun pol_Pc t = Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
26 |
fun pol_Pinj t = Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
27 |
fun pol_PX t = Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t); |
17516 | 28 |
|
29 |
(* polex *) |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
30 |
fun polex_add t = Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
31 |
fun polex_sub t = Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
32 |
fun polex_mul t = Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
33 |
fun polex_neg t = Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
34 |
fun polex_pol t = Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t); |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
35 |
fun polex_pow t = Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t); |
17516 | 36 |
|
37 |
(* reification of polynoms : primitive cring expressions *) |
|
22950 | 38 |
fun reif_pol T vs (t as Free _) = |
39 |
let |
|
40 |
val one = @{term "1::nat"}; |
|
31986 | 41 |
val i = find_index (fn t' => t' = t) vs |
22950 | 42 |
in if i = 0 |
43 |
then pol_PX T $ (pol_Pc T $ cring_one T) |
|
44 |
$ one $ (pol_Pc T $ cring_zero T) |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23261
diff
changeset
|
45 |
else pol_Pinj T $ HOLogic.mk_nat i |
22950 | 46 |
$ (pol_PX T $ (pol_Pc T $ cring_one T) |
47 |
$ one $ (pol_Pc T $ cring_zero T)) |
|
17516 | 48 |
end |
22950 | 49 |
| reif_pol T vs t = pol_Pc T $ t; |
17516 | 50 |
|
51 |
(* reification of polynom expressions *) |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
52 |
fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) = |
22950 | 53 |
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
|
54 |
| reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) = |
22950 | 55 |
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
|
56 |
| reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) = |
22950 | 57 |
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
|
58 |
| reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) = |
22950 | 59 |
polex_neg T $ reif_polex T vs a |
24996 | 60 |
| reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) = |
22950 | 61 |
polex_pow T $ reif_polex T vs a $ n |
62 |
| reif_polex T vs t = polex_pol T $ reif_pol T vs t; |
|
17516 | 63 |
|
64 |
(* reification of the equation *) |
|
31021 | 65 |
val cr_sort = @{sort "comm_ring_1"}; |
22950 | 66 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
37744
diff
changeset
|
67 |
fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) = |
22950 | 68 |
if Sign.of_sort thy (T, cr_sort) then |
69 |
let |
|
44121 | 70 |
val fs = Misc_Legacy.term_frees eq; |
22950 | 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 |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
76 |
else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort) |
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
77 |
| reif_eq _ _ = error "reif_eq: not an equation"; |
17516 | 78 |
|
22950 | 79 |
(* The cring tactic *) |
17516 | 80 |
(* Attention: You have to make sure that no t^0 is in the goal!! *) |
81 |
(* Use simply rewriting t^0 = 1 *) |
|
20623 | 82 |
val cring_simps = |
22950 | 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}]]; |
|
17516 | 85 |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
32149
diff
changeset
|
86 |
fun tac ctxt = SUBGOAL (fn (g, i) => |
20623 | 87 |
let |
42361 | 88 |
val thy = Proof_Context.theory_of ctxt; |
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents:
31986
diff
changeset
|
89 |
val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*) |
22950 | 90 |
addsimps cring_simps; |
20623 | 91 |
val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g) |
92 |
val norm_eq_th = |
|
22950 | 93 |
simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq}) |
20623 | 94 |
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
|
95 |
cut_tac norm_eq_th i |
20623 | 96 |
THEN (simp_tac cring_ss i) |
97 |
THEN (simp_tac cring_ss i) |
|
98 |
end); |
|
99 |
||
17516 | 100 |
end; |