1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Oct 26 15:37:02 2007 +0200
1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Oct 26 15:42:23 2007 +0200
1.3 @@ -12,16 +12,6 @@
1.4 syntax
1.5 "_alpha" :: "type" ("\<alpha>")
1.6 "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
1.7 - "_beta" :: "type" ("\<beta>")
1.8 - "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
1.9 - "_gamma" :: "type" ("\<gamma>")
1.10 - "_gamma_ofsort" :: "sort \<Rightarrow> type" ("\<gamma>()\<Colon>_" [0] 1000)
1.11 - "_alpha_f" :: "type" ("\<alpha>\<^sub>f")
1.12 - "_alpha_f_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>\<^sub>f()\<Colon>_" [0] 1000)
1.13 - "_beta_f" :: "type" ("\<beta>\<^sub>f")
1.14 - "_beta_f_ofsort" :: "sort \<Rightarrow> type" ("\<beta>\<^sub>f()\<Colon>_" [0] 1000)
1.15 - "_gamma_f" :: "type" ("\<gamma>\<^sub>f")
1.16 - "_gamma_ofsort_f" :: "sort \<Rightarrow> type" ("\<gamma>\<^sub>f()\<Colon>_" [0] 1000)
1.17
1.18 parse_ast_translation {*
1.19 let
1.20 @@ -30,38 +20,8 @@
1.21 fun alpha_ofsort_ast_tr [ast] =
1.22 Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
1.23 | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
1.24 - fun beta_ast_tr [] = Syntax.Variable "'b"
1.25 - | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
1.26 - fun beta_ofsort_ast_tr [ast] =
1.27 - Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
1.28 - | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
1.29 - fun gamma_ast_tr [] = Syntax.Variable "'c"
1.30 - | gamma_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
1.31 - fun gamma_ofsort_ast_tr [ast] =
1.32 - Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c", ast]
1.33 - | gamma_ofsort_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
1.34 - fun alpha_f_ast_tr [] = Syntax.Variable "'a_f"
1.35 - | alpha_f_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
1.36 - fun alpha_f_ofsort_ast_tr [ast] =
1.37 - Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a_f", ast]
1.38 - | alpha_f_ofsort_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
1.39 - fun beta_f_ast_tr [] = Syntax.Variable "'b_f"
1.40 - | beta_f_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
1.41 - fun beta_f_ofsort_ast_tr [ast] =
1.42 - Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b_f", ast]
1.43 - | beta_f_ofsort_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
1.44 - fun gamma_f_ast_tr [] = Syntax.Variable "'c_f"
1.45 - | gamma_f_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
1.46 - fun gamma_f_ofsort_ast_tr [ast] =
1.47 - Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c_f", ast]
1.48 - | gamma_f_ofsort_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
1.49 in [
1.50 - ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
1.51 - ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr),
1.52 - ("_gamma", gamma_ast_tr), ("_gamma_ofsort", gamma_ofsort_ast_tr),
1.53 - ("_alpha_f", alpha_f_ast_tr), ("_alpha_f_ofsort", alpha_f_ofsort_ast_tr),
1.54 - ("_beta_f", beta_f_ast_tr), ("_beta_f_ofsort", beta_f_ofsort_ast_tr),
1.55 - ("_gamma_f", gamma_f_ast_tr), ("_gamma_f_ofsort", gamma_f_ofsort_ast_tr)
1.56 + ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr)
1.57 ] end
1.58 *}
1.59 (*>*)
1.60 @@ -164,8 +124,8 @@
1.61 *}
1.62
1.63 class semigroup = type +
1.64 - fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<^loc>\<otimes>" 70)
1.65 - assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
1.66 + fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
1.67 + assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.68
1.69 text {*
1.70 \noindent This @{text "\<CLASS>"} specification consists of two
1.71 @@ -242,8 +202,8 @@
1.72 *}
1.73
1.74 class monoidl = semigroup +
1.75 - fixes neutral :: "\<alpha>" ("\<^loc>\<one>")
1.76 - assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
1.77 + fixes neutral :: "\<alpha>" ("\<one>")
1.78 + assumes neutl: "\<one> \<otimes> x = x"
1.79
1.80 text {*
1.81 \noindent Again, we make some instances, by
1.82 @@ -283,7 +243,7 @@
1.83 *}
1.84
1.85 class monoid = monoidl +
1.86 - assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
1.87 + assumes neutr: "x \<otimes> \<one> = x"
1.88
1.89 text {*
1.90 \noindent Instantiations may also be given simultaneously for different
1.91 @@ -313,8 +273,8 @@
1.92 *}
1.93
1.94 class group = monoidl +
1.95 - fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<^loc>\<div>)" [1000] 999)
1.96 - assumes invl: "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>"
1.97 + fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
1.98 + assumes invl: "x\<div> \<otimes> x = \<one>"
1.99
1.100 instance int :: group
1.101 inverse_int_def: "i\<div> \<equiv> - i"
1.102 @@ -381,15 +341,15 @@
1.103 states that the function @{text "(x \<circ>)"} is injective:
1.104 *}
1.105
1.106 - lemma (in group) left_cancel: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z \<longleftrightarrow> y = z"
1.107 + lemma (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
1.108 proof
1.109 - assume "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
1.110 - then have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> y) = x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
1.111 - then have "(x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> y = (x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> z" using assoc by simp
1.112 + assume "x \<otimes> y = x \<otimes> z"
1.113 + then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
1.114 + then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
1.115 then show "y = z" using neutl and invl by simp
1.116 next
1.117 assume "y = z"
1.118 - then show "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
1.119 + then show "x \<otimes> y = x \<otimes> z" by simp
1.120 qed
1.121
1.122 text {*
1.123 @@ -412,8 +372,8 @@
1.124
1.125 fun (in monoid)
1.126 pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
1.127 - "pow_nat 0 x = \<^loc>\<one>"
1.128 - | "pow_nat (Suc n) x = x \<^loc>\<otimes> pow_nat n x"
1.129 + "pow_nat 0 x = \<one>"
1.130 + | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
1.131
1.132 text {*
1.133 \noindent If the locale @{text group} is also a class, this local
1.134 @@ -440,16 +400,16 @@
1.135 subclass (in group) monoid
1.136 proof unfold_locales
1.137 fix x
1.138 - from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
1.139 - with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
1.140 - with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
1.141 + from invl have "x\<div> \<otimes> x = \<one>" by simp
1.142 + with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
1.143 + with left_cancel show "x \<otimes> \<one> = x" by simp
1.144 qed
1.145
1.146 text {*
1.147 - The logical proof is carried out on the locale level
1.148 + \noindent The logical proof is carried out on the locale level
1.149 and thus conveniently is opened using the @{text unfold_locales}
1.150 method which only leaves the logical differences still
1.151 - open to proof to the user. After the proof it is propagated
1.152 + open to proof to the user. Afterwards it is propagated
1.153 to the type system, making @{text group} an instance of
1.154 @{text monoid}. For illustration, a derived definition
1.155 in @{text group} which uses @{text pow_nat}:
1.156 @@ -459,10 +419,10 @@
1.157 pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
1.158 "pow_int k x = (if k >= 0
1.159 then pow_nat (nat k) x
1.160 - else (pow_nat (nat (- k)) x)\<^loc>\<div>)"
1.161 + else (pow_nat (nat (- k)) x)\<div>)"
1.162
1.163 text {*
1.164 - yields the global definition of
1.165 + \noindent yields the global definition of
1.166 @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
1.167 with the corresponding theorem @{thm pow_int_def [no_vars]}.
1.168 *}
2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Fri Oct 26 15:37:02 2007 +0200
2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Fri Oct 26 15:42:23 2007 +0200
2.3 @@ -1,29 +1,28 @@
2.4 module Classes where {
2.5
2.6
2.7 -data Nat = Suc Classes.Nat | Zero_nat;
2.8 +data Nat = Suc Nat | Zero_nat;
2.9
2.10 data Bit = B1 | B0;
2.11
2.12 -nat_aux :: Integer -> Classes.Nat -> Classes.Nat;
2.13 -nat_aux i n =
2.14 - (if i <= 0 then n else Classes.nat_aux (i - 1) (Classes.Suc n));
2.15 +nat_aux :: Integer -> Nat -> Nat;
2.16 +nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
2.17
2.18 -nat :: Integer -> Classes.Nat;
2.19 -nat i = Classes.nat_aux i Classes.Zero_nat;
2.20 +nat :: Integer -> Nat;
2.21 +nat i = nat_aux i Zero_nat;
2.22
2.23 class Semigroup a where {
2.24 mult :: a -> a -> a;
2.25 };
2.26
2.27 -class (Classes.Semigroup a) => Monoidl a where {
2.28 +class (Semigroup a) => Monoidl a where {
2.29 neutral :: a;
2.30 };
2.31
2.32 -class (Classes.Monoidl a) => Monoid a where {
2.33 +class (Monoidl a) => Monoid a where {
2.34 };
2.35
2.36 -class (Classes.Monoid a) => Group a where {
2.37 +class (Monoid a) => Group a where {
2.38 inverse :: a -> a;
2.39 };
2.40
2.41 @@ -36,31 +35,31 @@
2.42 mult_int :: Integer -> Integer -> Integer;
2.43 mult_int i j = i + j;
2.44
2.45 -instance Classes.Semigroup Integer where {
2.46 - mult = Classes.mult_int;
2.47 +instance Semigroup Integer where {
2.48 + mult = mult_int;
2.49 };
2.50
2.51 -instance Classes.Monoidl Integer where {
2.52 - neutral = Classes.neutral_int;
2.53 +instance Monoidl Integer where {
2.54 + neutral = neutral_int;
2.55 };
2.56
2.57 -instance Classes.Monoid Integer where {
2.58 +instance Monoid Integer where {
2.59 };
2.60
2.61 -instance Classes.Group Integer where {
2.62 - inverse = Classes.inverse_int;
2.63 +instance Group Integer where {
2.64 + inverse = inverse_int;
2.65 };
2.66
2.67 -pow_nat :: (Classes.Monoid a) => Classes.Nat -> a -> a;
2.68 -pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x);
2.69 -pow_nat Classes.Zero_nat x = Classes.neutral;
2.70 +pow_nat :: (Monoid a) => Nat -> a -> a;
2.71 +pow_nat (Suc n) x = mult x (pow_nat n x);
2.72 +pow_nat Zero_nat x = neutral;
2.73
2.74 -pow_int :: (Classes.Group a) => Integer -> a -> a;
2.75 +pow_int :: (Group a) => Integer -> a -> a;
2.76 pow_int k x =
2.77 - (if 0 <= k then Classes.pow_nat (Classes.nat k) x
2.78 - else Classes.inverse (Classes.pow_nat (Classes.nat (negate k)) x));
2.79 + (if 0 <= k then pow_nat (nat k) x
2.80 + else inverse (pow_nat (nat (negate k)) x));
2.81
2.82 example :: Integer;
2.83 -example = Classes.pow_int 10 (-2);
2.84 +example = pow_int 10 (-2);
2.85
2.86 }
3.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Oct 26 15:37:02 2007 +0200
3.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Oct 26 15:42:23 2007 +0200
3.3 @@ -148,8 +148,8 @@
3.4 \isamarkuptrue%
3.5 \ \ \ \ \isacommand{class}\isamarkupfalse%
3.6 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
3.7 -\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
3.8 -\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
3.9 +\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
3.10 +\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
3.11 \begin{isamarkuptext}%
3.12 \noindent This \isa{{\isasymCLASS}} specification consists of two
3.13 parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
3.14 @@ -291,8 +291,8 @@
3.15 \isamarkuptrue%
3.16 \ \ \ \ \isacommand{class}\isamarkupfalse%
3.17 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
3.18 -\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
3.19 -\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
3.20 +\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
3.21 +\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
3.22 \begin{isamarkuptext}%
3.23 \noindent Again, we make some instances, by
3.24 providing suitable parameter definitions and proofs for the
3.25 @@ -401,7 +401,7 @@
3.26 \isamarkuptrue%
3.27 \ \ \ \ \isacommand{class}\isamarkupfalse%
3.28 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
3.29 -\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
3.30 +\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
3.31 \begin{isamarkuptext}%
3.32 \noindent Instantiations may also be given simultaneously for different
3.33 type constructors:%
3.34 @@ -470,8 +470,8 @@
3.35 \isamarkuptrue%
3.36 \ \ \ \ \isacommand{class}\isamarkupfalse%
3.37 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
3.38 -\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
3.39 -\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
3.40 +\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
3.41 +\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
3.42 \isanewline
3.43 \ \ \ \ \isacommand{instance}\isamarkupfalse%
3.44 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
3.45 @@ -612,7 +612,7 @@
3.46 \end{isamarkuptext}%
3.47 \isamarkuptrue%
3.48 \ \ \ \ \isacommand{lemma}\isamarkupfalse%
3.49 -\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
3.50 +\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
3.51 %
3.52 \isadelimproof
3.53 \ \ \ \ %
3.54 @@ -622,14 +622,14 @@
3.55 \isacommand{proof}\isamarkupfalse%
3.56 \isanewline
3.57 \ \ \ \ \isacommand{assume}\isamarkupfalse%
3.58 -\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
3.59 +\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
3.60 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
3.61 \ \isacommand{have}\isamarkupfalse%
3.62 -\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.63 +\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.64 \ simp\isanewline
3.65 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
3.66 \ \isacommand{have}\isamarkupfalse%
3.67 -\ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
3.68 +\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
3.69 \ assoc\ \isacommand{by}\isamarkupfalse%
3.70 \ simp\isanewline
3.71 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
3.72 @@ -643,7 +643,7 @@
3.73 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
3.74 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
3.75 \ \isacommand{show}\isamarkupfalse%
3.76 -\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.77 +\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.78 \ simp\isanewline
3.79 \ \ \ \ \isacommand{qed}\isamarkupfalse%
3.80 %
3.81 @@ -674,8 +674,8 @@
3.82 \ \ \ \ \isacommand{fun}\isamarkupfalse%
3.83 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
3.84 \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.85 -\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
3.86 -\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
3.87 +\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
3.88 +\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
3.89 \begin{isamarkuptext}%
3.90 \noindent If the locale \isa{group} is also a class, this local
3.91 definition is propagated onto a global definition of
3.92 @@ -715,15 +715,15 @@
3.93 \ x\isanewline
3.94 \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
3.95 \ invl\ \isacommand{have}\isamarkupfalse%
3.96 -\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.97 +\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.98 \ simp\isanewline
3.99 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
3.100 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
3.101 -\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.102 +\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.103 \ simp\isanewline
3.104 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
3.105 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
3.106 -\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.107 +\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.108 \ simp\isanewline
3.109 \ \ \ \ \isacommand{qed}\isamarkupfalse%
3.110 %
3.111 @@ -735,10 +735,10 @@
3.112 \endisadelimproof
3.113 %
3.114 \begin{isamarkuptext}%
3.115 -The logical proof is carried out on the locale level
3.116 +\noindent The logical proof is carried out on the locale level
3.117 and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales}
3.118 method which only leaves the logical differences still
3.119 - open to proof to the user. After the proof it is propagated
3.120 + open to proof to the user. Afterwards it is propagated
3.121 to the type system, making \isa{group} an instance of
3.122 \isa{monoid}. For illustration, a derived definition
3.123 in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
3.124 @@ -749,9 +749,9 @@
3.125 \ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.126 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
3.127 \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
3.128 -\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
3.129 +\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
3.130 \begin{isamarkuptext}%
3.131 -yields the global definition of
3.132 +\noindent yields the global definition of
3.133 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
3.134 with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
3.135 \end{isamarkuptext}%
4.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty Fri Oct 26 15:37:02 2007 +0200
4.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty Fri Oct 26 15:42:23 2007 +0200
4.3 @@ -25,10 +25,10 @@
4.4 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
4.5 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
4.6 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
4.7 -\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
4.8 -\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
4.9 -\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
4.10 -\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
4.11 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
4.12 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
4.13 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
4.14 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
4.15 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
4.16 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
4.17 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}