src/HOL/Algebra/ringsimp.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21505 13d4dba99337
child 21588 cd0dc678a205
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
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;
ballarin@20168
    32
  fun merge _ (structs1, structs2) = gen_merge_lists
ballarin@20168
    33
    (fn ((s1, _), (s2, _)) => struct_eq (s1, s2)) structs1 structs2;
ballarin@20168
    34
  fun print generic structs =
ballarin@20168
    35
    let
ballarin@20168
    36
      val ctxt = Context.proof_of generic;
ballarin@20168
    37
      val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
ballarin@20168
    38
      fun pretty_struct ((s, ts), _) = Pretty.block
ballarin@20168
    39
        [Pretty.str s, Pretty.str ":", Pretty.brk 1,
ballarin@20168
    40
         Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
ballarin@20168
    41
    in
ballarin@20168
    42
      Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
ballarin@20168
    43
        Pretty.writeln
ballarin@20168
    44
    end
ballarin@20168
    45
end);
ballarin@13854
    46
wenzelm@21505
    47
val print_structures = AlgebraData.print o Context.Proof;
ballarin@13854
    48
ballarin@20168
    49
ballarin@20168
    50
(** Method **)
ballarin@13854
    51
ballarin@20168
    52
fun struct_tac ((s, ts), simps) =
ballarin@20168
    53
  let
ballarin@20168
    54
    val ops = map (fst o Term.strip_comb) ts;
ballarin@20168
    55
    fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
ballarin@20168
    56
      | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
ballarin@20168
    57
    fun less (a, b) = (Term.term_lpo ord (a, b) = LESS);
ballarin@20168
    58
  in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
ballarin@20168
    59
ballarin@20168
    60
fun algebra_tac ctxt =
wenzelm@21505
    61
  EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
ballarin@20168
    62
ballarin@20168
    63
val method =
ballarin@20168
    64
  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt))
ballarin@20168
    65
ballarin@20168
    66
ballarin@20168
    67
(** Attribute **)
ballarin@14399
    68
ballarin@20168
    69
fun add_struct_thm s =
ballarin@20168
    70
  Thm.declaration_attribute (fn thm => fn ctxt =>
wenzelm@21505
    71
    AlgebraData.map (fn structs =>
ballarin@20168
    72
      if AList.defined struct_eq structs s
ballarin@20168
    73
      then AList.map_entry struct_eq s (fn thms => thm :: thms) structs
ballarin@20168
    74
      else (s, [thm])::structs) ctxt);
ballarin@20168
    75
fun del_struct s =
ballarin@20168
    76
  Thm.declaration_attribute (fn _ => fn ctxt =>
ballarin@20168
    77
    AlgebraData.map (AList.delete struct_eq s) ctxt);
ballarin@13854
    78
ballarin@20168
    79
val attribute = Attrib.syntax
ballarin@20168
    80
     (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
wenzelm@21505
    81
        Scan.succeed true) -- Scan.lift Args.name --
ballarin@20168
    82
      Scan.repeat Args.term
ballarin@20168
    83
      >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
ballarin@20168
    84
ballarin@20168
    85
ballarin@20168
    86
(** Setup **)
ballarin@20168
    87
ballarin@20168
    88
val setup =
ballarin@20168
    89
  AlgebraData.init #>
ballarin@20168
    90
  Method.add_methods [("algebra", method, "normalisation of algebraic structure")] #>
ballarin@20168
    91
  Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
ballarin@20168
    92
ballarin@20168
    93
wenzelm@21505
    94
end;