author | haftmann |
Tue, 08 Aug 2006 08:18:59 +0200 | |
changeset 20348 | d59364649bcc |
parent 20168 | ed7bced29e1b |
child 20547 | 796ae7fa1049 |
permissions | -rw-r--r-- |
13854 | 1 |
(* |
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
2 |
Title: Normalisation method for locales ring and cring |
13854 | 3 |
Id: $Id$ |
4 |
Author: Clemens Ballarin |
|
5 |
Copyright: TU Muenchen |
|
6 |
*) |
|
7 |
||
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
8 |
signature ALGEBRA = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
9 |
sig |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
10 |
val print_structures: Context.generic -> unit |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
11 |
val setup: Theory.theory -> Theory.theory |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
12 |
end; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
13 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
14 |
structure Algebra: ALGEBRA = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
15 |
struct |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
16 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
17 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
18 |
(** Theory and context data **) |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
19 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
20 |
fun struct_eq ((s1, ts1), (s2, ts2)) = |
20348 | 21 |
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2); |
13854 | 22 |
|
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
23 |
structure AlgebraData = GenericDataFun |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
24 |
(struct |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
25 |
val name = "Algebra/algebra"; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
26 |
type T = ((string * term list) * thm list) list; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
27 |
(* Algebraic structures: |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
28 |
identifier of the structure, list of operations and simp rules, |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
29 |
identifier and operations identify the structure uniquely. *) |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
30 |
val empty = []; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
31 |
val extend = I; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
32 |
fun merge _ (structs1, structs2) = gen_merge_lists |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
33 |
(fn ((s1, _), (s2, _)) => struct_eq (s1, s2)) structs1 structs2; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
34 |
fun print generic structs = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
35 |
let |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
36 |
val ctxt = Context.proof_of generic; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
37 |
val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
38 |
fun pretty_struct ((s, ts), _) = Pretty.block |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
39 |
[Pretty.str s, Pretty.str ":", Pretty.brk 1, |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
40 |
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))]; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
41 |
in |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
42 |
Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |> |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
43 |
Pretty.writeln |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
44 |
end |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
45 |
end); |
13854 | 46 |
|
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
47 |
val print_structures = AlgebraData.print; |
13854 | 48 |
|
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
49 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
50 |
(** Method **) |
13854 | 51 |
|
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
52 |
fun struct_tac ((s, ts), simps) = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
53 |
let |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
54 |
val ops = map (fst o Term.strip_comb) ts; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
55 |
fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
56 |
| ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
57 |
fun less (a, b) = (Term.term_lpo ord (a, b) = LESS); |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
58 |
in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
59 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
60 |
fun algebra_tac ctxt = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
61 |
let val _ = print_structures (Context.Proof ctxt) |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
62 |
in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
63 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
64 |
val method = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
65 |
Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt)) |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
66 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
67 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
68 |
(** Attribute **) |
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset
|
69 |
|
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
70 |
fun add_struct_thm s = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
71 |
Thm.declaration_attribute (fn thm => fn ctxt => |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
72 |
AlgebraData.map (fn structs => |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
73 |
if AList.defined struct_eq structs s |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
74 |
then AList.map_entry struct_eq s (fn thms => thm :: thms) structs |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
75 |
else (s, [thm])::structs) ctxt); |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
76 |
fun del_struct s = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
77 |
Thm.declaration_attribute (fn _ => fn ctxt => |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
78 |
AlgebraData.map (AList.delete struct_eq s) ctxt); |
13854 | 79 |
|
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
80 |
val attribute = Attrib.syntax |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
81 |
(Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
82 |
Scan.succeed true) -- Scan.lift Args.name -- |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
83 |
Scan.repeat Args.term |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
84 |
>> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts))); |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
85 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
86 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
87 |
(** Setup **) |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
88 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
89 |
val setup = |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
90 |
AlgebraData.init #> |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
91 |
Method.add_methods [("algebra", method, "normalisation of algebraic structure")] #> |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
92 |
Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")]; |
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
93 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
94 |
|
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset
|
95 |
end; (* struct *) |