src/HOL/ex/Classpackage.thy
 author haftmann Fri Mar 09 08:45:55 2007 +0100 (2007-03-09) changeset 22424 8a5412121687 parent 22384 33a46e6c7f04 child 22473 753123c89d72 permissions -rw-r--r--
*** empty log message ***
```     1 (*  ID:         \$Id\$
```
```     2     Author:     Florian Haftmann, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Test and examples for Isar class package *}
```
```     6
```
```     7 theory Classpackage
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 class semigroup =
```
```    12   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
```
```    13   assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
```
```    14
```
```    15 instance nat :: semigroup
```
```    16   "m \<otimes> n \<equiv> m + n"
```
```    17 proof
```
```    18   fix m n q :: nat
```
```    19   from mult_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
```
```    20 qed
```
```    21
```
```    22 instance int :: semigroup
```
```    23   "k \<otimes> l \<equiv> k + l"
```
```    24 proof
```
```    25   fix k l j :: int
```
```    26   from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
```
```    27 qed
```
```    28
```
```    29 instance list :: (type) semigroup
```
```    30   "xs \<otimes> ys \<equiv> xs @ ys"
```
```    31 proof
```
```    32   fix xs ys zs :: "'a list"
```
```    33   show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
```
```    34   proof -
```
```    35     from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
```
```    36     thus ?thesis by simp
```
```    37   qed
```
```    38 qed
```
```    39
```
```    40 class monoidl = semigroup +
```
```    41   fixes one :: 'a ("\<^loc>\<one>")
```
```    42   assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
```
```    43
```
```    44 instance nat :: monoidl and int :: monoidl
```
```    45   "\<one> \<equiv> 0"
```
```    46   "\<one> \<equiv> 0"
```
```    47 proof
```
```    48   fix n :: nat
```
```    49   from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp
```
```    50 next
```
```    51   fix k :: int
```
```    52   from mult_int_def one_int_def show "\<one> \<otimes> k = k" by simp
```
```    53 qed
```
```    54
```
```    55 instance list :: (type) monoidl
```
```    56   "\<one> \<equiv> []"
```
```    57 proof
```
```    58   fix xs :: "'a list"
```
```    59   show "\<one> \<otimes> xs = xs"
```
```    60   proof -
```
```    61     from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
```
```    62     moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
```
```    63     ultimately show ?thesis by simp
```
```    64   qed
```
```    65 qed
```
```    66
```
```    67 class monoid = monoidl +
```
```    68   assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
```
```    69
```
```    70 instance list :: (type) monoid
```
```    71 proof
```
```    72   fix xs :: "'a list"
```
```    73   show "xs \<otimes> \<one> = xs"
```
```    74   proof -
```
```    75     from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
```
```    76     moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
```
```    77     ultimately show ?thesis by simp
```
```    78   qed
```
```    79 qed
```
```    80
```
```    81 class monoid_comm = monoid +
```
```    82   assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
```
```    83
```
```    84 instance nat :: monoid_comm and int :: monoid_comm
```
```    85 proof
```
```    86   fix n :: nat
```
```    87   from mult_nat_def one_nat_def show "n \<otimes> \<one> = n" by simp
```
```    88 next
```
```    89   fix n m :: nat
```
```    90   from mult_nat_def show "n \<otimes> m = m \<otimes> n" by simp
```
```    91 next
```
```    92   fix k :: int
```
```    93   from mult_int_def one_int_def show "k \<otimes> \<one> = k" by simp
```
```    94 next
```
```    95   fix k l :: int
```
```    96   from mult_int_def show "k \<otimes> l = l \<otimes> k" by simp
```
```    97 qed
```
```    98
```
```    99 context monoid
```
```   100 begin
```
```   101
```
```   102 definition
```
```   103   units :: "'a set" where
```
```   104   "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
```
```   105
```
```   106 end
```
```   107
```
```   108 context monoid
```
```   109 begin
```
```   110
```
```   111 lemma inv_obtain:
```
```   112   assumes "x \<in> units"
```
```   113   obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
```
```   114 proof -
```
```   115   from assms units_def obtain y
```
```   116     where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
```
```   117   thus ?thesis ..
```
```   118 qed
```
```   119
```
```   120 lemma inv_unique:
```
```   121   assumes "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
```
```   122   shows "y = y'"
```
```   123 proof -
```
```   124   from assms neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
```
```   125   also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
```
```   126   also with assms neutl have "... = y'" by simp
```
```   127   finally show ?thesis .
```
```   128 qed
```
```   129
```
```   130 lemma units_inv_comm:
```
```   131   assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
```
```   132     and G: "x \<in> units"
```
```   133   shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
```
```   134 proof -
```
```   135   from G inv_obtain obtain z
```
```   136     where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
```
```   137   from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
```
```   138   with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
```
```   139   with neutl z_choice show ?thesis by simp
```
```   140 qed
```
```   141
```
```   142 end
```
```   143
```
```   144 consts
```
```   145   reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
```
```   146
```
```   147 primrec
```
```   148   "reduce f g 0 x = g"
```
```   149   "reduce f g (Suc n) x = f x (reduce f g n x)"
```
```   150
```
```   151 context monoid
```
```   152 begin
```
```   153
```
```   154 definition
```
```   155   npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```   156   npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
```
```   157
```
```   158 end
```
```   159
```
```   160 context monoid
```
```   161 begin
```
```   162
```
```   163 abbreviation
```
```   164   npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
```
```   165   "x \<^loc>\<up> n \<equiv> npow n x"
```
```   166
```
```   167 lemma npow_def:
```
```   168   "x \<^loc>\<up> 0 = \<^loc>\<one>"
```
```   169   "x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n"
```
```   170 using npow_def_prim by simp_all
```
```   171
```
```   172 lemma nat_pow_one:
```
```   173   "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
```
```   174 using npow_def neutl by (induct n) simp_all
```
```   175
```
```   176 lemma nat_pow_mult: "x \<^loc>\<up> n \<^loc>\<otimes> x \<^loc>\<up> m = x \<^loc>\<up> (n + m)"
```
```   177 proof (induct n)
```
```   178   case 0 with neutl npow_def show ?case by simp
```
```   179 next
```
```   180   case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
```
```   181 qed
```
```   182
```
```   183 lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)"
```
```   184 using npow_def nat_pow_mult by (induct n) simp_all
```
```   185
```
```   186 end
```
```   187
```
```   188 class group = monoidl +
```
```   189   fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
```
```   190   assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
```
```   191
```
```   192 class group_comm = group + monoid_comm
```
```   193
```
```   194 instance int :: group_comm
```
```   195   "\<div> k \<equiv> - (k\<Colon>int)"
```
```   196 proof
```
```   197   fix k :: int
```
```   198   from mult_int_def one_int_def inv_int_def show "\<div> k \<otimes> k = \<one>" by simp
```
```   199 qed
```
```   200
```
```   201 lemma (in group) cancel:
```
```   202   "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
```
```   203 proof
```
```   204   fix x y z :: 'a
```
```   205   assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
```
```   206   hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
```
```   207   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
```
```   208   with neutl invl show "y = z" by simp
```
```   209 next
```
```   210   fix x y z :: 'a
```
```   211   assume eq: "y = z"
```
```   212   thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
```
```   213 qed
```
```   214
```
```   215 lemma (in group) neutr:
```
```   216   "x \<^loc>\<otimes> \<^loc>\<one> = x"
```
```   217 proof -
```
```   218   from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
```
```   219   with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
```
```   220   with cancel show ?thesis by simp
```
```   221 qed
```
```   222
```
```   223 lemma (in group) invr:
```
```   224   "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
```
```   225 proof -
```
```   226   from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
```
```   227   with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
```
```   228   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
```
```   229   with cancel show ?thesis ..
```
```   230 qed
```
```   231
```
```   232 instance advanced group < monoid
```
```   233 proof unfold_locales
```
```   234   fix x
```
```   235   from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
```
```   236 qed
```
```   237
```
```   238 lemma (in group) all_inv [intro]:
```
```   239   "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
```
```   240   unfolding units_def
```
```   241 proof -
```
```   242   fix x :: "'a"
```
```   243   from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" .
```
```   244   then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
```
```   245   hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
```
```   246   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
```
```   247 qed
```
```   248
```
```   249 lemma (in group) cancer:
```
```   250   "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
```
```   251 proof
```
```   252   assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
```
```   253   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)
```
```   254   with invr neutr show "y = z" by simp
```
```   255 next
```
```   256   assume eq: "y = z"
```
```   257   thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
```
```   258 qed
```
```   259
```
```   260 lemma (in group) inv_one:
```
```   261   "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
```
```   262 proof -
```
```   263   from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
```
```   264   moreover from invr have "... = \<^loc>\<one>" by simp
```
```   265   finally show ?thesis .
```
```   266 qed
```
```   267
```
```   268 lemma (in group) inv_inv:
```
```   269   "\<^loc>\<div> (\<^loc>\<div> x) = x"
```
```   270 proof -
```
```   271   from invl invr neutr
```
```   272     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
```
```   273   with assoc [symmetric]
```
```   274     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
```
```   275   with invl neutr show ?thesis by simp
```
```   276 qed
```
```   277
```
```   278 lemma (in group) inv_mult_group:
```
```   279   "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
```
```   280 proof -
```
```   281   from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
```
```   282   with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
```
```   283   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
```
```   284   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
```
```   285   with invr neutr show ?thesis by simp
```
```   286 qed
```
```   287
```
```   288 lemma (in group) inv_comm:
```
```   289   "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
```
```   290 using invr invl by simp
```
```   291
```
```   292 definition (in group)
```
```   293   pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```   294   "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
```
```   295     else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
```
```   296
```
```   297 abbreviation (in group)
```
```   298   pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
```
```   299   "x \<^loc>\<up> k \<equiv> pow k x"
```
```   300
```
```   301 lemma (in group) int_pow_zero:
```
```   302   "x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>"
```
```   303 using npow_def pow_def by simp
```
```   304
```
```   305 lemma (in group) int_pow_one:
```
```   306   "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
```
```   307 using pow_def nat_pow_one inv_one by simp
```
```   308
```
```   309 instance * :: (semigroup, semigroup) semigroup
```
```   310   mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
```
```   311               (x1 \<otimes> y1, x2 \<otimes> y2)"
```
```   312 by default (simp_all add: split_paired_all mult_prod_def assoc)
```
```   313
```
```   314 instance * :: (monoidl, monoidl) monoidl
```
```   315   one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
```
```   316 by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
```
```   317
```
```   318 instance * :: (monoid, monoid) monoid
```
```   319 by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr)
```
```   320
```
```   321 instance * :: (monoid_comm, monoid_comm) monoid_comm
```
```   322 by default (simp_all add: split_paired_all mult_prod_def comm)
```
```   323
```
```   324 instance * :: (group, group) group
```
```   325   inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
```
```   326 by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
```
```   327
```
```   328 instance * :: (group_comm, group_comm) group_comm
```
```   329 by default (simp_all add: split_paired_all mult_prod_def comm)
```
```   330
```
```   331
```
```   332 definition
```
```   333   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
```
```   334 definition
```
```   335   "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
```
```   336
```
```   337 definition "x1 = X (1::nat) 2 3"
```
```   338 definition "x2 = X (1::int) 2 3"
```
```   339 definition "y2 = Y (1::int) 2 3"
```
```   340
```
```   341 code_gen "op \<otimes>" \<one> inv X Y
```
```   342 code_gen x1 x2 y2 (SML #) (OCaml -) (Haskell -)
```
```   343
```
```   344 end
```