author  ballarin 
Tue, 16 Dec 2008 21:10:53 +0100  
changeset 29237  e90d9d51106b 
parent 24920  2a45e400fdad 
child 29269  5c25a2012975 
permissions  rwrr 
13854  1 
(* 
2 
Id: $Id$ 

3 
Author: Clemens Ballarin 

21505  4 

5 
Normalisation method for locales ring and cring. 

13854  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 
21505  10 
val print_structures: Proof.context > unit 
20547  11 
val setup: theory > theory 
20168
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 

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

22846  23 
structure Data = GenericDataFun 
24 
( 

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

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

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

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

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

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

30 
val extend = I; 
22634  31 
fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop)); 
22846  32 
); 
13854  33 

22846  34 
fun print_structures ctxt = 
35 
let 

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

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

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

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

13854  42 

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

43 

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

44 
(** Method **) 
13854  45 

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

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

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

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

49 
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

50 
 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

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

52 
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

53 

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

54 
fun algebra_tac ctxt = 
22846  55 
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

56 

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

57 

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

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

59 

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

60 
fun add_struct_thm s = 
22634  61 
Thm.declaration_attribute 
22846  62 
(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

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

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

67 
val attribute = Attrib.syntax 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

68 
(Scan.lift ((Args.add >> K true  Args.del >> K false)  Args.colon  
21505  69 
Scan.succeed true)  Scan.lift Args.name  
20168
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

70 
Scan.repeat Args.term 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

71 
>> (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

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 = 
21588  77 
Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac), 
78 
"normalisation of algebraic structure")] #> 

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

79 
Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")]; 
ed7bced29e1b
Reimplemented algebra method; now controlled by attribute.
ballarin
parents:
20129
diff
changeset

80 

21505  81 
end; 