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:
```