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