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