author | schirmer |
Fri, 17 Mar 2006 17:38:38 +0100 (2006-03-17) | |
changeset 19284 | 4c86109423d5 |
parent 16568 | e02fe7ae212b |
child 19931 | fb32b43e7f80 |
permissions | -rw-r--r-- |
13854 | 1 |
(* |
2 |
Title: Normalisation method for locale cring |
|
3 |
Id: $Id$ |
|
4 |
Author: Clemens Ballarin |
|
5 |
Copyright: TU Muenchen |
|
6 |
*) |
|
7 |
||
8 |
(*** Term order for commutative rings ***) |
|
9 |
||
10 |
fun ring_ord a = |
|
13936 | 11 |
find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv", |
14963 | 12 |
"CRing.minus", "Group.monoid.one", "Group.monoid.mult"]; |
13854 | 13 |
|
16568 | 14 |
fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); |
13854 | 15 |
|
16 |
val cring_ss = HOL_ss settermless termless_ring; |
|
17 |
||
18 |
fun cring_normalise ctxt = let |
|
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
19 |
fun ring_filter t = (case HOLogic.dest_Trueprop t of |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
20 |
Const ("CRing.ring_axioms", _) $ Free (s, _) => [s] |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
21 |
| _ => []) |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
22 |
handle TERM _ => []; |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
23 |
fun comm_filter t = (case HOLogic.dest_Trueprop t of |
14963 | 24 |
Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s] |
13864 | 25 |
| _ => []) |
13854 | 26 |
handle TERM _ => []; |
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
27 |
|
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
28 |
val prems = ProofContext.prems_of ctxt; |
15570 | 29 |
val rings = List.concat (map (ring_filter o #prop o rep_thm) prems); |
30 |
val comms = List.concat (map (comm_filter o #prop o rep_thm) prems); |
|
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
31 |
val non_comm_rings = rings \\ comms; |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
32 |
val comm_rings = rings inter_string comms; |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
33 |
val _ = tracing |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
34 |
("Non-commutative rings in proof context: " ^ commas non_comm_rings ^ |
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
35 |
"\nCommutative rings in proof context: " ^ commas comm_rings); |
13854 | 36 |
val simps = |
16486 | 37 |
List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".ring_simprules"))) |
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
38 |
non_comm_rings) @ |
16486 | 39 |
List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".cring_simprules"))) |
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
40 |
comm_rings); |
13854 | 41 |
in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps)) |
42 |
end; |
|
43 |
||
44 |
(* |
|
45 |
val ring_ss = HOL_basic_ss settermless termless_ring addsimps |
|
46 |
[a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def, |
|
47 |
r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0, |
|
48 |
a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus]; |
|
49 |
*) |