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