src/HOL/OrderedGroup.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 20713 823967ef47f1
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
obua@14755
     1
(*  Title:      HOL/OrderedGroup.ML
obua@14755
     2
    ID:         $Id$
ballarin@20129
     3
    Author:     Steven Obua, Tobias Nipkow, Technische Universitaet Muenchen
obua@14755
     4
*)
obua@14755
     5
obua@14755
     6
structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
obua@14755
     7
struct
nipkow@16568
     8
nipkow@16568
     9
(*** Term order for abelian groups ***)
nipkow@16568
    10
haftmann@20713
    11
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
ballarin@20129
    12
  | agrp_ord _ = ~1;
nipkow@16568
    13
nipkow@16568
    14
fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
nipkow@16568
    15
huffman@18925
    16
local
huffman@18925
    17
  val ac1 = mk_meta_eq (thm "add_assoc");
huffman@18925
    18
  val ac2 = mk_meta_eq (thm "add_commute");
huffman@18925
    19
  val ac3 = mk_meta_eq (thm "add_left_commute");
haftmann@19233
    20
  fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
huffman@18925
    21
        SOME ac1
haftmann@19233
    22
    | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
huffman@18925
    23
        if termless_agrp (y, x) then SOME ac3 else NONE
huffman@18925
    24
    | solve_add_ac thy _ (_ $ x $ y) =
huffman@18925
    25
        if termless_agrp (y, x) then SOME ac2 else NONE
huffman@18925
    26
    | solve_add_ac thy _ _ = NONE
huffman@18925
    27
in
huffman@18925
    28
  val add_ac_proc = Simplifier.simproc (the_context ())
huffman@18925
    29
    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
huffman@18925
    30
end;
huffman@18925
    31
huffman@18925
    32
val cancel_ss = HOL_basic_ss settermless termless_agrp
huffman@18925
    33
  addsimprocs [add_ac_proc] addsimps
huffman@18925
    34
  [thm "add_0", thm "add_0_right",
nipkow@16568
    35
   thm "diff_def", thm "minus_add_distrib",
nipkow@16568
    36
   thm "minus_minus", thm "minus_zero",
nipkow@16568
    37
   thm "right_minus", thm "left_minus",
nipkow@16568
    38
   thm "add_minus_cancel", thm "minus_add_cancel"];
nipkow@16568
    39
  
obua@14755
    40
  val eq_reflection = thm "eq_reflection"
obua@14755
    41
  
wenzelm@16423
    42
  val thy_ref = Theory.self_ref (theory "OrderedGroup")
obua@14755
    43
obua@14755
    44
  val T = TFree("'a", ["OrderedGroup.ab_group_add"])
nipkow@16568
    45
obua@14755
    46
  val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
obua@14755
    47
  fun dest_eqI th = 
obua@14755
    48
      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
obua@14755
    49
	      (HOLogic.dest_Trueprop (concl_of th)))  
obua@14755
    50
end;
obua@14755
    51
obua@14755
    52
structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
obua@14755
    53
obua@14755
    54
Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];