src/HOL/Algebra/ringsimp.ML
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 67561 f0b11413f1c9
permissions -rw-r--r--
More on Algebra by Paulo and Martin
wenzelm@35849
     1
(*  Author:     Clemens Ballarin
wenzelm@21505
     2
wenzelm@21505
     3
Normalisation method for locales ring and cring.
ballarin@13854
     4
*)
ballarin@13854
     5
wenzelm@58811
     6
signature RINGSIMP =
ballarin@20168
     7
sig
wenzelm@21505
     8
  val print_structures: Proof.context -> unit
wenzelm@58811
     9
  val add_struct: string * term list -> attribute
wenzelm@58811
    10
  val del_struct: string * term list -> attribute
wenzelm@47701
    11
  val algebra_tac: Proof.context -> int -> tactic
ballarin@20168
    12
end;
ballarin@20168
    13
wenzelm@58811
    14
structure Ringsimp: RINGSIMP =
ballarin@20168
    15
struct
ballarin@20168
    16
ballarin@20168
    17
(** Theory and context data **)
ballarin@20168
    18
wenzelm@20547
    19
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
haftmann@20348
    20
  (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
ballarin@13854
    21
wenzelm@33519
    22
structure Data = Generic_Data
wenzelm@22846
    23
(
ballarin@20168
    24
  type T = ((string * term list) * thm list) list;
ballarin@20168
    25
    (* Algebraic structures:
ballarin@20168
    26
       identifier of the structure, list of operations and simp rules,
ballarin@20168
    27
       identifier and operations identify the structure uniquely. *)
ballarin@20168
    28
  val empty = [];
ballarin@20168
    29
  val extend = I;
wenzelm@33520
    30
  val merge = AList.join struct_eq (K Thm.merge_thms);
wenzelm@22846
    31
);
ballarin@13854
    32
wenzelm@22846
    33
fun print_structures ctxt =
wenzelm@22846
    34
  let
wenzelm@22846
    35
    val structs = Data.get (Context.Proof ctxt);
wenzelm@24920
    36
    val pretty_term = Pretty.quote o Syntax.pretty_term ctxt;
wenzelm@22846
    37
    fun pretty_struct ((s, ts), _) = Pretty.block
wenzelm@22846
    38
      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
wenzelm@22846
    39
       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
wenzelm@22846
    40
  in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
ballarin@13854
    41
ballarin@20168
    42
ballarin@20168
    43
(** Method **)
ballarin@13854
    44
wenzelm@51717
    45
fun struct_tac ctxt ((s, ts), simps) =
ballarin@20168
    46
  let
ballarin@20168
    47
    val ops = map (fst o Term.strip_comb) ts;
ballarin@20168
    48
    fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
ballarin@20168
    49
      | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
wenzelm@67561
    50
  in
wenzelm@67561
    51
    asm_full_simp_tac
wenzelm@67561
    52
      (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_term_ord (Term_Ord.term_lpo ord))
wenzelm@67561
    53
  end;
ballarin@20168
    54
ballarin@20168
    55
fun algebra_tac ctxt =
wenzelm@51717
    56
  EVERY' (map (fn s => TRY o struct_tac ctxt s) (Data.get (Context.Proof ctxt)));
ballarin@20168
    57
ballarin@20168
    58
ballarin@20168
    59
(** Attribute **)
ballarin@14399
    60
wenzelm@58811
    61
fun add_struct s =
haftmann@22634
    62
  Thm.declaration_attribute
wenzelm@22846
    63
    (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
wenzelm@47701
    64
ballarin@20168
    65
fun del_struct s =
haftmann@22634
    66
  Thm.declaration_attribute
wenzelm@22846
    67
    (fn _ => Data.map (AList.delete struct_eq s));
ballarin@13854
    68
wenzelm@21505
    69
end;