src/HOL/Algebra/ringsimp.ML
author wenzelm
Thu Mar 26 20:08:55 2009 +0100 (2009-03-26)
changeset 30729 461ee3e49ad3
parent 30722 623d4831c8cf
child 33519 e31a85f92ce9
permissions -rw-r--r--
interpretation/interpret: prefixes are mandatory by default;
wenzelm@29269
     1
(*  Author:    Clemens Ballarin
wenzelm@21505
     2
wenzelm@21505
     3
Normalisation method for locales ring and cring.
ballarin@13854
     4
*)
ballarin@13854
     5
ballarin@20168
     6
signature ALGEBRA =
ballarin@20168
     7
sig
wenzelm@21505
     8
  val print_structures: Proof.context -> unit
wenzelm@20547
     9
  val setup: theory -> theory
ballarin@20168
    10
end;
ballarin@20168
    11
ballarin@20168
    12
structure Algebra: ALGEBRA =
ballarin@20168
    13
struct
ballarin@20168
    14
ballarin@20168
    15
ballarin@20168
    16
(** Theory and context data **)
ballarin@20168
    17
wenzelm@20547
    18
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
haftmann@20348
    19
  (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
ballarin@13854
    20
wenzelm@22846
    21
structure Data = GenericDataFun
wenzelm@22846
    22
(
ballarin@20168
    23
  type T = ((string * term list) * thm list) list;
ballarin@20168
    24
    (* Algebraic structures:
ballarin@20168
    25
       identifier of the structure, list of operations and simp rules,
ballarin@20168
    26
       identifier and operations identify the structure uniquely. *)
ballarin@20168
    27
  val empty = [];
ballarin@20168
    28
  val extend = I;
haftmann@22634
    29
  fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
wenzelm@22846
    30
);
ballarin@13854
    31
wenzelm@22846
    32
fun print_structures ctxt =
wenzelm@22846
    33
  let
wenzelm@22846
    34
    val structs = Data.get (Context.Proof ctxt);
wenzelm@24920
    35
    val pretty_term = Pretty.quote o Syntax.pretty_term ctxt;
wenzelm@22846
    36
    fun pretty_struct ((s, ts), _) = Pretty.block
wenzelm@22846
    37
      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
wenzelm@22846
    38
       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
wenzelm@22846
    39
  in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
ballarin@13854
    40
ballarin@20168
    41
ballarin@20168
    42
(** Method **)
ballarin@13854
    43
ballarin@20168
    44
fun struct_tac ((s, ts), simps) =
ballarin@20168
    45
  let
ballarin@20168
    46
    val ops = map (fst o Term.strip_comb) ts;
ballarin@20168
    47
    fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
ballarin@20168
    48
      | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
wenzelm@29269
    49
    fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS);
ballarin@20168
    50
  in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
ballarin@20168
    51
ballarin@20168
    52
fun algebra_tac ctxt =
wenzelm@22846
    53
  EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));
ballarin@20168
    54
ballarin@20168
    55
ballarin@20168
    56
(** Attribute **)
ballarin@14399
    57
ballarin@20168
    58
fun add_struct_thm s =
haftmann@22634
    59
  Thm.declaration_attribute
wenzelm@22846
    60
    (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
ballarin@20168
    61
fun del_struct s =
haftmann@22634
    62
  Thm.declaration_attribute
wenzelm@22846
    63
    (fn _ => Data.map (AList.delete struct_eq s));
ballarin@13854
    64
wenzelm@30722
    65
val attrib_setup =
wenzelm@30722
    66
  Attrib.setup @{binding algebra}
wenzelm@30722
    67
    (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
wenzelm@30722
    68
      -- Scan.lift Args.name -- Scan.repeat Args.term
wenzelm@30722
    69
      >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
wenzelm@30722
    70
    "theorems controlling algebra method";
wenzelm@30722
    71
ballarin@20168
    72
ballarin@20168
    73
ballarin@20168
    74
(** Setup **)
ballarin@20168
    75
ballarin@20168
    76
val setup =
wenzelm@30515
    77
  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
wenzelm@30515
    78
    "normalisation of algebraic structure" #>
wenzelm@30722
    79
  attrib_setup;
ballarin@20168
    80
wenzelm@21505
    81
end;