src/HOL/Algebra/ringsimp.ML
author ballarin
Wed Jul 19 19:25:58 2006 +0200 (2006-07-19)
changeset 20168 ed7bced29e1b
parent 20129 95e84d2c9f2c
child 20348 d59364649bcc
permissions -rw-r--r--
Reimplemented algebra method; now controlled by attribute.
     1 (*
     2   Title:     Normalisation method for locales ring and cring
     3   Id:        $Id$
     4   Author:    Clemens Ballarin
     5   Copyright: TU Muenchen
     6 *)
     7 
     8 signature ALGEBRA =
     9 sig
    10   val print_structures: Context.generic -> unit
    11   val setup: Theory.theory -> Theory.theory
    12 end;
    13 
    14 structure Algebra: ALGEBRA =
    15 struct
    16 
    17 
    18 (** Theory and context data **)
    19 
    20 fun struct_eq ((s1, ts1), (s2, ts2)) =
    21   (s1 = s2) andalso equal_lists (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 _ (structs1, structs2) = gen_merge_lists
    33     (fn ((s1, _), (s2, _)) => struct_eq (s1, s2)) structs1 structs2;
    34   fun print generic structs =
    35     let
    36       val ctxt = Context.proof_of generic;
    37       val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
    38       fun pretty_struct ((s, ts), _) = Pretty.block
    39         [Pretty.str s, Pretty.str ":", Pretty.brk 1,
    40          Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
    41     in
    42       Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
    43         Pretty.writeln
    44     end
    45 end);
    46 
    47 val print_structures = AlgebraData.print;
    48 
    49 
    50 (** Method **)
    51 
    52 fun struct_tac ((s, ts), simps) =
    53   let
    54     val ops = map (fst o Term.strip_comb) ts;
    55     fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
    56       | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
    57     fun less (a, b) = (Term.term_lpo ord (a, b) = LESS);
    58   in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
    59 
    60 fun algebra_tac ctxt =
    61   let val _ = print_structures (Context.Proof ctxt)
    62   in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end;
    63 
    64 val method =
    65   Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt))
    66 
    67 
    68 (** Attribute **)
    69 
    70 fun add_struct_thm s =
    71   Thm.declaration_attribute (fn thm => fn ctxt =>
    72     AlgebraData.map (fn structs => 
    73       if AList.defined struct_eq structs s
    74       then AList.map_entry struct_eq s (fn thms => thm :: thms) structs
    75       else (s, [thm])::structs) ctxt);
    76 fun del_struct s =
    77   Thm.declaration_attribute (fn _ => fn ctxt =>
    78     AlgebraData.map (AList.delete struct_eq s) ctxt);
    79 
    80 val attribute = Attrib.syntax
    81      (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
    82         Scan.succeed true) -- Scan.lift Args.name -- 
    83       Scan.repeat Args.term
    84       >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
    85 
    86 
    87 (** Setup **)
    88 
    89 val setup =
    90   AlgebraData.init #>
    91   Method.add_methods [("algebra", method, "normalisation of algebraic structure")] #>
    92   Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
    93 
    94 
    95 end;  (* struct *)