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