src/HOL/ex/Classpackage.thy
author haftmann
Mon, 14 Aug 2006 13:46:17 +0200
changeset 20383 58f65fc90cf4
parent 20187 af47971ea304
child 20427 0b102b4182de
permissions -rw-r--r--
adaptions to improvements
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     1
(*  ID:         $Id$
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     3
*)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     4
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     5
header {* Test and Examples for Pure/Tools/class_package.ML *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     6
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     7
theory Classpackage
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     8
imports Main
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     9
begin
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    10
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    11
class semigroup =
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    12
  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    13
  assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    14
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    15
instance nat :: semigroup
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    16
  "m \<otimes> n \<equiv> m + n"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    17
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    18
  fix m n q :: nat 
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    19
  from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    20
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    21
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    22
instance int :: semigroup
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    23
  "k \<otimes> l \<equiv> k + l"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    24
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    25
  fix k l j :: int
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    26
  from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    27
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    28
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    29
instance (type) list :: semigroup
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    30
  "xs \<otimes> ys \<equiv> xs @ ys"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    31
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    32
  fix xs ys zs :: "'a list"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    33
  show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    34
  proof -
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    35
    from semigroup_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    36
    thus ?thesis by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    37
  qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    38
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    39
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    40
class monoidl = semigroup +
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    41
  fixes one :: 'a ("\<^loc>\<one>")
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    42
  assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    43
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    44
instance monoidl_num_def: nat :: monoidl and int :: monoidl
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    45
  "\<one> \<equiv> 0"
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    46
  "\<one> \<equiv> 0"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    47
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    48
  fix n :: nat
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    49
  from monoidl_num_def show "\<one> \<otimes> n = n" by simp
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    50
next
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    51
  fix k :: int
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    52
  from monoidl_num_def show "\<one> \<otimes> k = k" by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    53
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    54
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    55
instance (type) list :: monoidl
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    56
  "\<one> \<equiv> []"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    57
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    58
  fix xs :: "'a list"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    59
  show "\<one> \<otimes> xs = xs"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    60
  proof -
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    61
    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    62
    moreover from monoidl_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    63
    ultimately show ?thesis by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    64
  qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    65
qed  
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    66
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    67
class monoid = monoidl +
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    68
  assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    69
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    70
instance monoid_list_def: (type) list :: monoid
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    71
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    72
  fix xs :: "'a list"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    73
  show "xs \<otimes> \<one> = xs"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    74
  proof -
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    75
    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    76
    moreover from monoid_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    77
    ultimately show ?thesis by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    78
  qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    79
qed  
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    80
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    81
class monoid_comm = monoid +
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    82
  assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    83
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    84
instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    85
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    86
  fix n :: nat
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    87
  from monoid_comm_num_def show "n \<otimes> \<one> = n" by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    88
next
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    89
  fix n m :: nat
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    90
  from monoid_comm_num_def show "n \<otimes> m = m \<otimes> n" by simp
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    91
next
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    92
  fix k :: int
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    93
  from monoid_comm_num_def show "k \<otimes> \<one> = k" by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    94
next
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    95
  fix k l :: int
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
    96
  from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    97
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    98
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    99
definition (in monoid)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   100
  units :: "'a set"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   101
  units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   102
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   103
lemma (in monoid) inv_obtain:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   104
  assumes ass: "x \<in> units"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   105
  obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   106
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   107
  from ass units_def obtain y
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   108
    where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   109
  thus ?thesis ..
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   110
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   111
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   112
lemma (in monoid) inv_unique:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   113
  assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   114
  shows "y = y'"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   115
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   116
  from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   117
  also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   118
  also with eq neutl have "... = y'" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   119
  finally show ?thesis .
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   120
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   121
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   122
lemma (in monoid) units_inv_comm:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   123
  assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   124
    and G: "x \<in> units"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   125
  shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   126
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   127
  from G inv_obtain obtain z
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   128
    where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   129
  from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   130
  with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   131
  with neutl z_choice show ?thesis by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   132
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   133
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   134
consts
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   135
  reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   136
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   137
primrec
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   138
  "reduce f g 0 x = g"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   139
  "reduce f g (Suc n) x = f x (reduce f g n x)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   140
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   141
definition (in monoid)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   142
  npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   143
  npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   144
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   145
abbreviation (in monoid)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   146
  abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   147
  "x \<^loc>\<up> n \<equiv> npow n x"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   148
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   149
lemma (in monoid) npow_def:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   150
  "x \<^loc>\<up> 0 = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   151
  "x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   152
using npow_def_prim by simp_all
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   153
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   154
lemma (in monoid) nat_pow_one:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   155
  "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   156
using npow_def neutl by (induct n) simp_all
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   157
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   158
lemma (in monoid) nat_pow_mult:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   159
  "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   160
proof (induct n)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   161
  case 0 with neutl npow_def show ?case by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   162
next
19933
16a5037f2d25 hyps better than prems
haftmann
parents: 19928
diff changeset
   163
  case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   164
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   165
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   166
lemma (in monoid) nat_pow_pow:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   167
  "npow n (npow m x) = npow (n * m) x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   168
using npow_def nat_pow_mult by (induct n) simp_all
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   169
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   170
class group = monoidl +
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   171
  fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   172
  assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   173
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   174
class group_comm = group + monoid_comm
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   175
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   176
instance group_comm_int_def: int :: group_comm
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   177
  "\<div> k \<equiv> - (k\<Colon>int)"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   178
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   179
  fix k :: int
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   180
  from group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   181
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   182
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   183
lemma (in group) cancel:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   184
  "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   185
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   186
  fix x y z :: 'a
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   187
  assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   188
  hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   189
  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   190
  with neutl invl show "y = z" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   191
next
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   192
  fix x y z :: 'a
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   193
  assume eq: "y = z"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   194
  thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   195
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   196
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   197
lemma (in group) neutr:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   198
  "x \<^loc>\<otimes> \<^loc>\<one> = x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   199
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   200
  from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   201
  with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   202
  with cancel show ?thesis by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   203
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   204
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   205
lemma (in group) invr:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   206
  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   207
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   208
  from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   209
  with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   210
  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   211
  with cancel show ?thesis ..
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   212
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   213
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   214
instance group < monoid
19928
cb8472f4c5fd switched to open locales for classes
haftmann
parents: 19888
diff changeset
   215
proof -
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   216
  fix x
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   217
  from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   218
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   219
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   220
lemma (in group) all_inv [intro]:
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   221
  "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   222
  unfolding units_def
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   223
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   224
  fix x :: "'a"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   225
  from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . 
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   226
  then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   227
  hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   228
  thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   229
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   230
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   231
lemma (in group) cancer:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   232
  "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   233
proof
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   234
  assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   235
  with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   236
  with invr neutr show "y = z" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   237
next
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   238
  assume eq: "y = z"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   239
  thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   240
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   241
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   242
lemma (in group) inv_one:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   243
  "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   244
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   245
  from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   246
  moreover from invr have "... = \<^loc>\<one>" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   247
  finally show ?thesis .
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   248
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   249
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   250
lemma (in group) inv_inv:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   251
  "\<^loc>\<div> (\<^loc>\<div> x) = x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   252
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   253
  from invl invr neutr
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   254
    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   255
  with assoc [symmetric]
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   256
    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   257
  with invl neutr show ?thesis by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   258
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   259
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   260
lemma (in group) inv_mult_group:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   261
  "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   262
proof -
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   263
  from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   264
  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   265
  with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   266
  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   267
  with invr neutr show ?thesis by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   268
qed
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   269
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   270
lemma (in group) inv_comm:
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   271
  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   272
using invr invl by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   273
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   274
definition (in group)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   275
  pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   276
  pow_def: "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   277
    else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   278
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   279
abbreviation (in group)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   280
  abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
19928
cb8472f4c5fd switched to open locales for classes
haftmann
parents: 19888
diff changeset
   281
  "x \<^loc>\<up> k \<equiv> pow k x"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   282
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   283
lemma (in group) int_pow_zero:
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   284
  "x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   285
using npow_def pow_def by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   286
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   287
lemma (in group) int_pow_one:
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   288
  "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   289
using pow_def nat_pow_one inv_one by simp
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   290
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   291
instance group_prod_def: (group, group) * :: group
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   292
  mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
19958
fc4ac94f03e0 improvements in Classpackage
haftmann
parents: 19951
diff changeset
   293
              (x1 \<otimes> y1, x2 \<otimes> y2)"
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   294
  mult_one_def: "\<one> \<equiv> (\<one>, \<one>)"
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   295
  mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
19928
cb8472f4c5fd switched to open locales for classes
haftmann
parents: 19888
diff changeset
   296
by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   297
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   298
instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
19928
cb8472f4c5fd switched to open locales for classes
haftmann
parents: 19888
diff changeset
   299
by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   300
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   301
definition
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   302
  "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   303
  "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   304
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   305
definition
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   306
  "x1 = X (1::nat) 2 3"
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   307
  "x2 = X (1::int) 2 3"
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   308
  "y2 = Y (1::int) 2 3"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   309
20178
e56fa3c8b1f1 adaption to changes in class_package
haftmann
parents: 20106
diff changeset
   310
code_generate "op \<otimes>" \<one> inv
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   311
code_generate (ml, haskell) X Y
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20187
diff changeset
   312
code_generate (ml, haskell) x1 x2 y2
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   313
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   314
code_serialize ml (-)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   315
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   316
end