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