src/HOL/ex/Classpackage.thy
author haftmann
Fri Dec 29 12:11:00 2006 +0100 (2006-12-29)
changeset 21924 fe474e69e603
parent 21911 e29bcab0c81c
child 22074 de3586cb0ebd
permissions -rw-r--r--
simplified class_package
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Test and examples for new 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 lemma inv_obtain:
   107   assumes "x \<in> units"
   108   obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
   109 proof -
   110   from assms units_def obtain y
   111     where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
   112   thus ?thesis ..
   113 qed
   114 
   115 lemma inv_unique:
   116   assumes "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
   117   shows "y = y'"
   118 proof -
   119   from assms neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
   120   also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
   121   also with assms neutl have "... = y'" by simp
   122   finally show ?thesis .
   123 qed
   124 
   125 lemma units_inv_comm:
   126   assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
   127     and G: "x \<in> units"
   128   shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
   129 proof -
   130   from G inv_obtain obtain z
   131     where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
   132   from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
   133   with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
   134   with neutl z_choice show ?thesis by simp
   135 qed
   136 
   137 end
   138 
   139 consts
   140   reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
   141 
   142 primrec
   143   "reduce f g 0 x = g"
   144   "reduce f g (Suc n) x = f x (reduce f g n x)"
   145 
   146 context monoid
   147 begin
   148 
   149 definition
   150   npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   151   npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
   152 
   153 abbreviation
   154   npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
   155   "x \<^loc>\<up> n \<equiv> npow n x"
   156 
   157 lemma npow_def:
   158   "x \<^loc>\<up> 0 = \<^loc>\<one>"
   159   "x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n"
   160 using npow_def_prim by simp_all
   161 
   162 lemma nat_pow_one:
   163   "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
   164 using npow_def neutl by (induct n) simp_all
   165 
   166 lemma nat_pow_mult: "x \<^loc>\<up> n \<^loc>\<otimes> x \<^loc>\<up> m = x \<^loc>\<up> (n + m)"
   167 proof (induct n)
   168   case 0 with neutl npow_def show ?case by simp
   169 next
   170   case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
   171 qed
   172 
   173 lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)"
   174 using npow_def nat_pow_mult by (induct n) simp_all
   175 
   176 end
   177 
   178 class group = monoidl +
   179   fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
   180   assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
   181 
   182 class group_comm = group + monoid_comm
   183 
   184 instance int :: group_comm
   185   "\<div> k \<equiv> - (k\<Colon>int)"
   186 proof
   187   fix k :: int
   188   from mult_int_def one_int_def inv_int_def show "\<div> k \<otimes> k = \<one>" by simp
   189 qed
   190 
   191 lemma (in group) cancel:
   192   "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
   193 proof
   194   fix x y z :: 'a
   195   assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
   196   hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
   197   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
   198   with neutl invl show "y = z" by simp
   199 next
   200   fix x y z :: 'a
   201   assume eq: "y = z"
   202   thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
   203 qed
   204 
   205 lemma (in group) neutr:
   206   "x \<^loc>\<otimes> \<^loc>\<one> = x"
   207 proof -
   208   from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
   209   with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
   210   with cancel show ?thesis by simp
   211 qed
   212 
   213 lemma (in group) invr:
   214   "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
   215 proof -
   216   from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
   217   with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
   218   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
   219   with cancel show ?thesis ..
   220 qed
   221 
   222 instance group < monoid
   223 proof -
   224   fix x
   225   from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
   226 qed
   227 
   228 lemma (in group) all_inv [intro]:
   229   "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
   230   unfolding units_def
   231 proof -
   232   fix x :: "'a"
   233   from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . 
   234   then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
   235   hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
   236   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
   237 qed
   238 
   239 lemma (in group) cancer:
   240   "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
   241 proof
   242   assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
   243   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)
   244   with invr neutr show "y = z" by simp
   245 next
   246   assume eq: "y = z"
   247   thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
   248 qed
   249 
   250 lemma (in group) inv_one:
   251   "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
   252 proof -
   253   from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
   254   moreover from invr have "... = \<^loc>\<one>" by simp
   255   finally show ?thesis .
   256 qed
   257 
   258 lemma (in group) inv_inv:
   259   "\<^loc>\<div> (\<^loc>\<div> x) = x"
   260 proof -
   261   from invl invr neutr
   262     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
   263   with assoc [symmetric]
   264     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
   265   with invl neutr show ?thesis by simp
   266 qed
   267 
   268 lemma (in group) inv_mult_group:
   269   "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
   270 proof -
   271   from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
   272   with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
   273   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
   274   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
   275   with invr neutr show ?thesis by simp
   276 qed
   277 
   278 lemma (in group) inv_comm:
   279   "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
   280 using invr invl by simp
   281 
   282 definition (in group)
   283   pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" where
   284   "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
   285     else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
   286 
   287 abbreviation (in group)
   288   pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
   289   "x \<^loc>\<up> k \<equiv> pow k x"
   290 
   291 lemma (in group) int_pow_zero:
   292   "x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>"
   293 using npow_def pow_def by simp
   294 
   295 lemma (in group) int_pow_one:
   296   "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
   297 using pow_def nat_pow_one inv_one by simp
   298 
   299 instance * :: (semigroup, semigroup) semigroup
   300   mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
   301               (x1 \<otimes> y1, x2 \<otimes> y2)"
   302 by default (simp_all add: split_paired_all mult_prod_def assoc)
   303 
   304 instance * :: (monoidl, monoidl) monoidl
   305   one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
   306 by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
   307 
   308 instance * :: (monoid, monoid) monoid
   309 by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr)
   310 
   311 instance * :: (monoid_comm, monoid_comm) monoid_comm
   312 by default (simp_all add: split_paired_all mult_prod_def comm)
   313 
   314 instance * :: (group, group) group
   315   inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
   316 by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
   317 
   318 instance * :: (group_comm, group_comm) group_comm
   319 by default (simp_all add: split_paired_all mult_prod_def comm)
   320 
   321 definition
   322   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
   323 definition
   324   "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
   325 
   326 definition "x1 = X (1::nat) 2 3"
   327 definition "x2 = X (1::int) 2 3"
   328 definition "y2 = Y (1::int) 2 3"
   329 
   330 code_gen "op \<otimes>" \<one> inv
   331 code_gen X Y (SML #) (Haskell -) (OCaml -)
   332 code_gen x1 x2 y2 (SML #) (Haskell -) (OCaml -)
   333 
   334 end