1 (* |
1 (* |
2 Title: Normalisation method for locales ring and cring |
|
3 Id: $Id$ |
2 Id: $Id$ |
4 Author: Clemens Ballarin |
3 Author: Clemens Ballarin |
5 Copyright: TU Muenchen |
4 |
|
5 Normalisation method for locales ring and cring. |
6 *) |
6 *) |
7 |
7 |
8 signature ALGEBRA = |
8 signature ALGEBRA = |
9 sig |
9 sig |
10 val print_structures: Context.generic -> unit |
10 val print_structures: Proof.context -> unit |
11 val setup: theory -> theory |
11 val setup: theory -> theory |
12 end; |
12 end; |
13 |
13 |
14 structure Algebra: ALGEBRA = |
14 structure Algebra: ALGEBRA = |
15 struct |
15 struct |
56 | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; |
56 | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; |
57 fun less (a, b) = (Term.term_lpo ord (a, b) = LESS); |
57 fun less (a, b) = (Term.term_lpo ord (a, b) = LESS); |
58 in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end; |
58 in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end; |
59 |
59 |
60 fun algebra_tac ctxt = |
60 fun algebra_tac ctxt = |
61 let val _ = print_structures (Context.Proof ctxt) |
61 EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))); |
62 in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end; |
|
63 |
62 |
64 val method = |
63 val method = |
65 Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt)) |
64 Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt)) |
66 |
65 |
67 |
66 |
68 (** Attribute **) |
67 (** Attribute **) |
69 |
68 |
70 fun add_struct_thm s = |
69 fun add_struct_thm s = |
71 Thm.declaration_attribute (fn thm => fn ctxt => |
70 Thm.declaration_attribute (fn thm => fn ctxt => |
72 AlgebraData.map (fn structs => |
71 AlgebraData.map (fn structs => |
73 if AList.defined struct_eq structs s |
72 if AList.defined struct_eq structs s |
74 then AList.map_entry struct_eq s (fn thms => thm :: thms) structs |
73 then AList.map_entry struct_eq s (fn thms => thm :: thms) structs |
75 else (s, [thm])::structs) ctxt); |
74 else (s, [thm])::structs) ctxt); |
76 fun del_struct s = |
75 fun del_struct s = |
77 Thm.declaration_attribute (fn _ => fn ctxt => |
76 Thm.declaration_attribute (fn _ => fn ctxt => |
78 AlgebraData.map (AList.delete struct_eq s) ctxt); |
77 AlgebraData.map (AList.delete struct_eq s) ctxt); |
79 |
78 |
80 val attribute = Attrib.syntax |
79 val attribute = Attrib.syntax |
81 (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || |
80 (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || |
82 Scan.succeed true) -- Scan.lift Args.name -- |
81 Scan.succeed true) -- Scan.lift Args.name -- |
83 Scan.repeat Args.term |
82 Scan.repeat Args.term |
84 >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts))); |
83 >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts))); |
85 |
84 |
86 |
85 |
87 (** Setup **) |
86 (** Setup **) |