src/HOL/ex/Classpackage.thy
changeset 21707 dfc7b21d0ee9
parent 21545 54cc492d80a9
child 21911 e29bcab0c81c
     1.1 --- a/src/HOL/ex/Classpackage.thy	Thu Dec 07 21:08:51 2006 +0100
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Thu Dec 07 21:44:13 2006 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Florian Haftmann, TU Muenchen
     1.5  *)
     1.6  
     1.7 -header {* Test and Examples for Pure/Tools/class_package.ML *}
     1.8 +header {* Test and examples for new class package *}
     1.9  
    1.10  theory Classpackage
    1.11  imports Main
    1.12 @@ -96,30 +96,33 @@
    1.13    from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp
    1.14  qed
    1.15  
    1.16 -definition (in monoid)
    1.17 +context monoid
    1.18 +begin
    1.19 +
    1.20 +definition
    1.21    units :: "'a set" where
    1.22 -  "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }"
    1.23 +  "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
    1.24  
    1.25 -lemma (in monoid) inv_obtain:
    1.26 -  assumes ass: "x \<in> units"
    1.27 +lemma inv_obtain:
    1.28 +  assumes "x \<in> units"
    1.29    obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
    1.30  proof -
    1.31 -  from ass units_def obtain y
    1.32 +  from assms units_def obtain y
    1.33      where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
    1.34    thus ?thesis ..
    1.35  qed
    1.36  
    1.37 -lemma (in monoid) inv_unique:
    1.38 -  assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
    1.39 +lemma inv_unique:
    1.40 +  assumes "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
    1.41    shows "y = y'"
    1.42  proof -
    1.43 -  from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
    1.44 +  from assms neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
    1.45    also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
    1.46 -  also with eq neutl have "... = y'" by simp
    1.47 +  also with assms neutl have "... = y'" by simp
    1.48    finally show ?thesis .
    1.49  qed
    1.50  
    1.51 -lemma (in monoid) units_inv_comm:
    1.52 +lemma units_inv_comm:
    1.53    assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
    1.54      and G: "x \<in> units"
    1.55    shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
    1.56 @@ -131,6 +134,8 @@
    1.57    with neutl z_choice show ?thesis by simp
    1.58  qed
    1.59  
    1.60 +end
    1.61 +
    1.62  consts
    1.63    reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.64  
    1.65 @@ -138,35 +143,38 @@
    1.66    "reduce f g 0 x = g"
    1.67    "reduce f g (Suc n) x = f x (reduce f g n x)"
    1.68  
    1.69 -definition (in monoid)
    1.70 +context monoid
    1.71 +begin
    1.72 +
    1.73 +definition
    1.74    npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.75    npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
    1.76  
    1.77 -abbreviation (in monoid)
    1.78 -  abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
    1.79 +abbreviation
    1.80 +  npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
    1.81    "x \<^loc>\<up> n \<equiv> npow n x"
    1.82  
    1.83 -lemma (in monoid) npow_def:
    1.84 +lemma npow_def:
    1.85    "x \<^loc>\<up> 0 = \<^loc>\<one>"
    1.86    "x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n"
    1.87  using npow_def_prim by simp_all
    1.88  
    1.89 -lemma (in monoid) nat_pow_one:
    1.90 +lemma nat_pow_one:
    1.91    "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
    1.92  using npow_def neutl by (induct n) simp_all
    1.93  
    1.94 -lemma (in monoid) nat_pow_mult:
    1.95 -  "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x"
    1.96 +lemma nat_pow_mult: "x \<^loc>\<up> n \<^loc>\<otimes> x \<^loc>\<up> m = x \<^loc>\<up> (n + m)"
    1.97  proof (induct n)
    1.98    case 0 with neutl npow_def show ?case by simp
    1.99  next
   1.100    case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
   1.101  qed
   1.102  
   1.103 -lemma (in monoid) nat_pow_pow:
   1.104 -  "npow n (npow m x) = npow (n * m) x"
   1.105 +lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)"
   1.106  using npow_def nat_pow_mult by (induct n) simp_all
   1.107  
   1.108 +end
   1.109 +
   1.110  class group = monoidl +
   1.111    fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
   1.112    assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
   1.113 @@ -277,7 +285,7 @@
   1.114      else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
   1.115  
   1.116  abbreviation (in group)
   1.117 -  abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
   1.118 +  pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
   1.119    "x \<^loc>\<up> k \<equiv> pow k x"
   1.120  
   1.121  lemma (in group) int_pow_zero: