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