src/HOL/Algebras.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35092 cfe605c54e50
child 35267 8dfd816713c6
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
haftmann@34974
     1
(*  Title:      HOL/Algebras.thy
haftmann@34974
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@34974
     3
*)
haftmann@34974
     4
haftmann@34974
     5
header {* Generic algebraic structures and operations *}
haftmann@34974
     6
haftmann@34974
     7
theory Algebras
haftmann@34974
     8
imports HOL
haftmann@34974
     9
begin
haftmann@34974
    10
haftmann@34974
    11
subsection {* Generic algebraic structures *}
haftmann@34974
    12
haftmann@35026
    13
text {*
haftmann@35026
    14
  These locales provide basic structures for interpretation into
haftmann@35026
    15
  bigger structures;  extensions require careful thinking, otherwise
haftmann@35026
    16
  undesired effects may occur due to interpretation.
haftmann@35026
    17
*}
haftmann@35026
    18
haftmann@35026
    19
ML {*
haftmann@35026
    20
structure Ac_Simps = Named_Thms(
haftmann@35026
    21
  val name = "ac_simps"
haftmann@35026
    22
  val description = "associativity and commutativity simplification rules"
haftmann@35026
    23
)
haftmann@35026
    24
*}
haftmann@35026
    25
haftmann@35026
    26
setup Ac_Simps.setup
haftmann@35026
    27
haftmann@34974
    28
locale semigroup =
haftmann@34974
    29
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
haftmann@35026
    30
  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
haftmann@34974
    31
haftmann@34974
    32
locale abel_semigroup = semigroup +
haftmann@35026
    33
  assumes commute [ac_simps]: "a * b = b * a"
haftmann@34974
    34
begin
haftmann@34974
    35
haftmann@35026
    36
lemma left_commute [ac_simps]:
haftmann@34974
    37
  "b * (a * c) = a * (b * c)"
haftmann@34974
    38
proof -
haftmann@34974
    39
  have "(b * a) * c = (a * b) * c"
haftmann@34974
    40
    by (simp only: commute)
haftmann@34974
    41
  then show ?thesis
haftmann@34974
    42
    by (simp only: assoc)
haftmann@34974
    43
qed
haftmann@34974
    44
haftmann@34974
    45
end
haftmann@34974
    46
haftmann@34974
    47
locale semilattice = abel_semigroup +
haftmann@34974
    48
  assumes idem [simp]: "a * a = a"
haftmann@34974
    49
begin
haftmann@34974
    50
haftmann@34974
    51
lemma left_idem [simp]:
haftmann@34974
    52
  "a * (a * b) = a * b"
haftmann@34974
    53
  by (simp add: assoc [symmetric])
haftmann@34974
    54
haftmann@34974
    55
end
haftmann@34974
    56
haftmann@34974
    57
haftmann@35092
    58
subsection {* Generic syntactic operations *}
haftmann@34974
    59
haftmann@34974
    60
class zero = 
haftmann@34974
    61
  fixes zero :: 'a  ("0")
haftmann@34974
    62
haftmann@34974
    63
class one =
haftmann@34974
    64
  fixes one  :: 'a  ("1")
haftmann@34974
    65
haftmann@35092
    66
hide (open) const zero one
haftmann@35092
    67
haftmann@35092
    68
syntax
haftmann@35092
    69
  "_index1"  :: index    ("\<^sub>1")
haftmann@35092
    70
translations
haftmann@35092
    71
  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
haftmann@35092
    72
haftmann@34974
    73
lemma Let_0 [simp]: "Let 0 f = f 0"
haftmann@34974
    74
  unfolding Let_def ..
haftmann@34974
    75
haftmann@34974
    76
lemma Let_1 [simp]: "Let 1 f = f 1"
haftmann@34974
    77
  unfolding Let_def ..
haftmann@34974
    78
haftmann@34974
    79
setup {*
haftmann@34974
    80
  Reorient_Proc.add
haftmann@34974
    81
    (fn Const(@{const_name Algebras.zero}, _) => true
haftmann@34974
    82
      | Const(@{const_name Algebras.one}, _) => true
haftmann@34974
    83
      | _ => false)
haftmann@34974
    84
*}
haftmann@34974
    85
haftmann@34974
    86
simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
haftmann@34974
    87
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
haftmann@34974
    88
haftmann@34974
    89
typed_print_translation {*
haftmann@34974
    90
let
haftmann@34974
    91
  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
haftmann@34974
    92
    if (not o null) ts orelse T = dummyT
haftmann@34974
    93
      orelse not (! show_types) andalso can Term.dest_Type T
haftmann@34974
    94
    then raise Match
haftmann@34974
    95
    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
haftmann@34974
    96
in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
haftmann@34974
    97
*} -- {* show types that are presumably too general *}
haftmann@34974
    98
haftmann@34974
    99
class plus =
haftmann@34974
   100
  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
haftmann@34974
   101
haftmann@34974
   102
class minus =
haftmann@34974
   103
  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
haftmann@34974
   104
haftmann@34974
   105
class uminus =
haftmann@34974
   106
  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
haftmann@34974
   107
haftmann@34974
   108
class times =
haftmann@34974
   109
  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
haftmann@34974
   110
haftmann@34974
   111
end