src/HOL/Algebra/ringsimp.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 58811 19382bbfa93a
child 67560 0fa87bd86566
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Author:     Clemens Ballarin
     2 
     3 Normalisation method for locales ring and cring.
     4 *)
     5 
     6 signature RINGSIMP =
     7 sig
     8   val print_structures: Proof.context -> unit
     9   val add_struct: string * term list -> attribute
    10   val del_struct: string * term list -> attribute
    11   val algebra_tac: Proof.context -> int -> tactic
    12 end;
    13 
    14 structure Ringsimp: RINGSIMP =
    15 struct
    16 
    17 (** Theory and context data **)
    18 
    19 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
    20   (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
    21 
    22 structure Data = Generic_Data
    23 (
    24   type T = ((string * term list) * thm list) list;
    25     (* Algebraic structures:
    26        identifier of the structure, list of operations and simp rules,
    27        identifier and operations identify the structure uniquely. *)
    28   val empty = [];
    29   val extend = I;
    30   val merge = AList.join struct_eq (K Thm.merge_thms);
    31 );
    32 
    33 fun print_structures ctxt =
    34   let
    35     val structs = Data.get (Context.Proof ctxt);
    36     val pretty_term = Pretty.quote o Syntax.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 Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
    41 
    42 
    43 (** Method **)
    44 
    45 fun struct_tac ctxt ((s, ts), simps) =
    46   let
    47     val ops = map (fst o Term.strip_comb) ts;
    48     fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
    49       | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
    50     fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
    51   in asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_termless less) end;
    52 
    53 fun algebra_tac ctxt =
    54   EVERY' (map (fn s => TRY o struct_tac ctxt s) (Data.get (Context.Proof ctxt)));
    55 
    56 
    57 (** Attribute **)
    58 
    59 fun add_struct s =
    60   Thm.declaration_attribute
    61     (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
    62 
    63 fun del_struct s =
    64   Thm.declaration_attribute
    65     (fn _ => Data.map (AList.delete struct_eq s));
    66 
    67 end;