author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 33520  b2cb4da715f7 
child 35408  b48ab741683b 
permissions  rwrr 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24920
diff
changeset

1 
(* Author: Clemens Ballarin 
21505  2 

3 
Normalisation method for locales ring and cring. 

13854  4 
*) 
5 

20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

6 
signature ALGEBRA = 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

7 
sig 
21505  8 
val print_structures: Proof.context > unit 
20547  9 
val setup: theory > theory 
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

10 
end; 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

11 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

12 
structure Algebra: ALGEBRA = 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

13 
struct 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

14 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

15 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

16 
(** Theory and context data **) 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

17 

20547  18 
fun struct_eq ((s1: string, ts1), (s2, ts2)) = 
20348  19 
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2); 
13854  20 

33519  21 
structure Data = Generic_Data 
22846  22 
( 
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

23 
type T = ((string * term list) * thm list) list; 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

24 
(* Algebraic structures: 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

25 
identifier of the structure, list of operations and simp rules, 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

26 
identifier and operations identify the structure uniquely. *) 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

27 
val empty = []; 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

28 
val extend = I; 
33520  29 
val merge = AList.join struct_eq (K Thm.merge_thms); 
22846  30 
); 
13854  31 

22846  32 
fun print_structures ctxt = 
33 
let 

34 
val structs = Data.get (Context.Proof ctxt); 

24920  35 
val pretty_term = Pretty.quote o Syntax.pretty_term ctxt; 
22846  36 
fun pretty_struct ((s, ts), _) = Pretty.block 
37 
[Pretty.str s, Pretty.str ":", Pretty.brk 1, 

38 
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))]; 

39 
in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end; 

13854  40 

20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

41 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

42 
(** Method **) 
13854  43 

20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

44 
fun struct_tac ((s, ts), simps) = 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

45 
let 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

46 
val ops = map (fst o Term.strip_comb) ts; 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

47 
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

48 
 ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b  _ => false) ops; 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24920
diff
changeset

49 
fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS); 
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

50 
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

51 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

52 
fun algebra_tac ctxt = 
22846  53 
EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt))); 
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

54 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

55 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

56 
(** Attribute **) 
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13936
diff
changeset

57 

20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

58 
fun add_struct_thm s = 
22634  59 
Thm.declaration_attribute 
22846  60 
(fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm))); 
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

61 
fun del_struct s = 
22634  62 
Thm.declaration_attribute 
22846  63 
(fn _ => Data.map (AList.delete struct_eq s)); 
13854  64 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

65 
val attrib_setup = 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

66 
Attrib.setup @{binding algebra} 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

67 
(Scan.lift ((Args.add >> K true  Args.del >> K false)  Args.colon  Scan.succeed true) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

68 
 Scan.lift Args.name  Scan.repeat Args.term 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

69 
>> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts))) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

70 
"theorems controlling algebra method"; 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

71 

20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

72 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

73 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

74 
(** Setup **) 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

75 

ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

76 
val setup = 
30515  77 
Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac)) 
78 
"normalisation of algebraic structure" #> 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

79 
attrib_setup; 
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

80 

21505  81 
end; 