src/HOL/Algebra/ringsimp.ML
author haftmann
Wed Apr 11 08:28:15 2007 +0200 (2007-04-11)
changeset 22634 399e4b4835da
parent 21588 cd0dc678a205
child 22846 fb79144af9a3
permissions -rw-r--r--
canonical merge operations
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
ballarin@20168
    23
structure AlgebraData = GenericDataFun
ballarin@20168
    24
(struct
ballarin@20168
    25
  val name = "Algebra/algebra";
ballarin@20168
    26
  type T = ((string * term list) * thm list) list;
ballarin@20168
    27
    (* Algebraic structures:
ballarin@20168
    28
       identifier of the structure, list of operations and simp rules,
ballarin@20168
    29
       identifier and operations identify the structure uniquely. *)
ballarin@20168
    30
  val empty = [];
ballarin@20168
    31
  val extend = I;
haftmann@22634
    32
  fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
ballarin@20168
    33
  fun print generic structs =
ballarin@20168
    34
    let
ballarin@20168
    35
      val ctxt = Context.proof_of generic;
ballarin@20168
    36
      val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
ballarin@20168
    37
      fun pretty_struct ((s, ts), _) = Pretty.block
ballarin@20168
    38
        [Pretty.str s, Pretty.str ":", Pretty.brk 1,
ballarin@20168
    39
         Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
ballarin@20168
    40
    in
ballarin@20168
    41
      Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
ballarin@20168
    42
        Pretty.writeln
ballarin@20168
    43
    end
ballarin@20168
    44
end);
ballarin@13854
    45
wenzelm@21505
    46
val print_structures = AlgebraData.print o Context.Proof;
ballarin@13854
    47
ballarin@20168
    48
ballarin@20168
    49
(** Method **)
ballarin@13854
    50
ballarin@20168
    51
fun struct_tac ((s, ts), simps) =
ballarin@20168
    52
  let
ballarin@20168
    53
    val ops = map (fst o Term.strip_comb) ts;
ballarin@20168
    54
    fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
ballarin@20168
    55
      | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
ballarin@20168
    56
    fun less (a, b) = (Term.term_lpo ord (a, b) = LESS);
ballarin@20168
    57
  in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
ballarin@20168
    58
ballarin@20168
    59
fun algebra_tac ctxt =
wenzelm@21505
    60
  EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
ballarin@20168
    61
ballarin@20168
    62
ballarin@20168
    63
(** Attribute **)
ballarin@14399
    64
ballarin@20168
    65
fun add_struct_thm s =
haftmann@22634
    66
  Thm.declaration_attribute
haftmann@22634
    67
    (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
ballarin@20168
    68
fun del_struct s =
haftmann@22634
    69
  Thm.declaration_attribute
haftmann@22634
    70
    (fn _ => AlgebraData.map (AList.delete struct_eq s));
ballarin@13854
    71
ballarin@20168
    72
val attribute = Attrib.syntax
ballarin@20168
    73
     (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
wenzelm@21505
    74
        Scan.succeed true) -- Scan.lift Args.name --
ballarin@20168
    75
      Scan.repeat Args.term
ballarin@20168
    76
      >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
ballarin@20168
    77
ballarin@20168
    78
ballarin@20168
    79
(** Setup **)
ballarin@20168
    80
ballarin@20168
    81
val setup =
ballarin@20168
    82
  AlgebraData.init #>
wenzelm@21588
    83
  Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
wenzelm@21588
    84
    "normalisation of algebraic structure")] #>
ballarin@20168
    85
  Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
ballarin@20168
    86
wenzelm@21505
    87
end;