src/HOL/Algebra/ringsimp.ML
author nipkow
Fri, 13 Nov 2009 14:14:04 +0100
changeset 33657 a4179bf442d1
parent 33520 b2cb4da715f7
child 35408 b48ab741683b
permissions -rw-r--r--
renamed lemmas "anti_sym" -> "antisym"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 24920
diff changeset
     1
(*  Author:    Clemens Ballarin
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 20547
diff changeset
     2
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 20547
diff changeset
     3
Normalisation method for locales ring and cring.
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents:
diff changeset
     4
*)
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents:
diff changeset
     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
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 20547
diff changeset
     8
  val print_structures: Proof.context -> unit
20547
wenzelm
parents: 20348
diff changeset
     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
wenzelm
parents: 20348
diff changeset
    18
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
20348
d59364649bcc abandoned equal_list in favor for eq_list
haftmann
parents: 20168
diff changeset
    19
  (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents:
diff changeset
    20
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 30722
diff changeset
    21
structure Data = Generic_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    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
wenzelm
parents: 33519
diff changeset
    29
  val merge = AList.join struct_eq (K Thm.merge_thms);
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    30
);
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents:
diff changeset
    31
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    32
fun print_structures ctxt =
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    33
  let
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    34
    val structs = Data.get (Context.Proof ctxt);
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 22846
diff changeset
    35
    val pretty_term = Pretty.quote o Syntax.pretty_term ctxt;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    36
    fun pretty_struct ((s, ts), _) = Pretty.block
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    37
      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    38
       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    39
  in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents:
diff changeset
    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
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents:
diff changeset
    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
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    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
399e4b4835da canonical merge operations
haftmann
parents: 21588
diff changeset
    59
  Thm.declaration_attribute
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    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
399e4b4835da canonical merge operations
haftmann
parents: 21588
diff changeset
    62
  Thm.declaration_attribute
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22634
diff changeset
    63
    (fn _ => Data.map (AList.delete struct_eq s));
13854
91c9ab25fece First distributed version of Group and Ring theory.
ballarin
parents:
diff changeset
    64
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up 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 bottom-up 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 bottom-up 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 bottom-up 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 bottom-up 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 bottom-up 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 bottom-up 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
bca05b17b618 simplified method setup;
wenzelm
parents: 30510
diff changeset
    77
  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
bca05b17b618 simplified method setup;
wenzelm
parents: 30510
diff changeset
    78
    "normalisation of algebraic structure" #>
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up 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
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 20547
diff changeset
    81
end;