1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Fri Oct 10 06:45:50 2008 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Fri Oct 10 06:45:53 2008 +0200
1.3 @@ -25,7 +25,7 @@
1.4 explicitly:
1.5 *}
1.6
1.7 -lemma %quoteme [code func]:
1.8 +lemma %quoteme [code]:
1.9 "dequeue (Queue xs []) =
1.10 (if xs = [] then (None, Queue [] [])
1.11 else dequeue (Queue [] (rev xs)))"
1.12 @@ -34,7 +34,7 @@
1.13 by (cases xs, simp_all) (cases "rev xs", simp_all)
1.14
1.15 text {*
1.16 - \noindent The annotation @{text "[code func]"} is an @{text Isar}
1.17 + \noindent The annotation @{text "[code]"} is an @{text Isar}
1.18 @{text attribute} which states that the given theorems should be
1.19 considered as defining equations for a @{text fun} statement --
1.20 the corresponding constant is determined syntactically. The resulting code:
1.21 @@ -255,7 +255,7 @@
1.22 the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
1.23 *}
1.24
1.25 -lemma %quoteme plus_Dig [code func]:
1.26 +lemma %quoteme plus_Dig [code]:
1.27 "0 + n = n"
1.28 "m + 0 = m"
1.29 "1 + Dig0 n = Dig1 n"
1.30 @@ -282,12 +282,12 @@
1.31 which are an obstacle here:
1.32 *}
1.33
1.34 -lemma %quoteme Suc_Dig [code func]:
1.35 +lemma %quoteme Suc_Dig [code]:
1.36 "Suc n = n + 1"
1.37 by simp
1.38
1.39 declare %quoteme One_nat_def [code inline del]
1.40 -declare %quoteme add_Suc_shift [code func del]
1.41 +declare %quoteme add_Suc_shift [code del]
1.42
1.43 text {*
1.44 \noindent This yields the following code:
1.45 @@ -316,10 +316,10 @@
1.46 *}
1.47
1.48 code_datatype %invisible "0::nat" Suc
1.49 -declare %invisible plus_Dig [code func del]
1.50 +declare %invisible plus_Dig [code del]
1.51 declare %invisible One_nat_def [code inline]
1.52 -declare %invisible add_Suc_shift [code func]
1.53 -lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
1.54 +declare %invisible add_Suc_shift [code]
1.55 +lemma %invisible [code]: "0 + n = (n \<Colon> nat)" by simp
1.56
1.57
1.58 subsection {* Equality and wellsortedness *}
1.59 @@ -367,10 +367,10 @@
1.60 instantiation %quoteme "*" :: (order, order) order
1.61 begin
1.62
1.63 -definition %quoteme [code func del]:
1.64 +definition %quoteme [code del]:
1.65 "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
1.66
1.67 -definition %quoteme [code func del]:
1.68 +definition %quoteme [code del]:
1.69 "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
1.70
1.71 instance %quoteme proof
1.72 @@ -378,7 +378,7 @@
1.73
1.74 end %quoteme
1.75
1.76 -lemma %quoteme order_prod [code func]:
1.77 +lemma %quoteme order_prod [code]:
1.78 "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
1.79 x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
1.80 "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
1.81 @@ -396,7 +396,7 @@
1.82 code theorems:
1.83 *}
1.84
1.85 -lemma %quoteme order_prod_code [code func]:
1.86 +lemma %quoteme order_prod_code [code]:
1.87 "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
1.88 x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
1.89 "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
1.90 @@ -438,7 +438,7 @@
1.91 @{const [show_types] list_all2} can do the job:
1.92 *}
1.93
1.94 -lemma %quoteme monotype_eq_list_all2 [code func]:
1.95 +lemma %quoteme monotype_eq_list_all2 [code]:
1.96 "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
1.97 eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
1.98 by (simp add: eq list_all2_eq [symmetric])
2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Fri Oct 10 06:45:50 2008 +0200
2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Fri Oct 10 06:45:53 2008 +0200
2.3 @@ -55,7 +55,7 @@
2.4 %
2.5 \isatagquoteme
2.6 \isacommand{lemma}\isamarkupfalse%
2.7 -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.8 +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
2.9 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
2.10 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
2.11 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.12 @@ -71,7 +71,7 @@
2.13 \endisadelimquoteme
2.14 %
2.15 \begin{isamarkuptext}%
2.16 -\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar}
2.17 +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
2.18 \isa{attribute} which states that the given theorems should be
2.19 considered as defining equations for a \isa{fun} statement --
2.20 the corresponding constant is determined syntactically. The resulting code:%
2.21 @@ -287,8 +287,8 @@
2.22 \verb|};|\newline%
2.23 \newline%
2.24 \verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
2.25 +\verb|pow Zero_nat a = neutral;|\newline%
2.26 \verb|pow (Suc n) a = mult a (pow n a);|\newline%
2.27 -\verb|pow Zero_nat a = neutral;|\newline%
2.28 \newline%
2.29 \verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
2.30 \verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
2.31 @@ -298,8 +298,8 @@
2.32 \verb|neutral_nat = Suc Zero_nat;|\newline%
2.33 \newline%
2.34 \verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
2.35 +\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
2.36 \verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
2.37 -\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
2.38 \newline%
2.39 \verb|instance Semigroup Nat where {|\newline%
2.40 \verb| mult = mult_nat;|\newline%
2.41 @@ -350,16 +350,16 @@
2.42 \verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
2.43 \verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
2.44 \newline%
2.45 -\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline%
2.46 -\verb| |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline%
2.47 +\verb|fun pow A_ Zero_nat a = neutral A_|\newline%
2.48 +\verb| |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline%
2.49 \newline%
2.50 \verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
2.51 \verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
2.52 \newline%
2.53 \verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
2.54 \newline%
2.55 -\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline%
2.56 -\verb| |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline%
2.57 +\verb|fun mult_nat Zero_nat n = Zero_nat|\newline%
2.58 +\verb| |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
2.59 \newline%
2.60 \verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
2.61 \newline%
2.62 @@ -575,7 +575,7 @@
2.63 %
2.64 \isatagquoteme
2.65 \isacommand{lemma}\isamarkupfalse%
2.66 -\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.67 +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
2.68 \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
2.69 \ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
2.70 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
2.71 @@ -629,7 +629,7 @@
2.72 %
2.73 \isatagquoteme
2.74 \isacommand{lemma}\isamarkupfalse%
2.75 -\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.76 +\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
2.77 \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
2.78 \ \ \isacommand{by}\isamarkupfalse%
2.79 \ simp\isanewline
2.80 @@ -637,7 +637,7 @@
2.81 \isacommand{declare}\isamarkupfalse%
2.82 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
2.83 \isacommand{declare}\isamarkupfalse%
2.84 -\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
2.85 +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
2.86 \endisatagquoteme
2.87 {\isafoldquoteme}%
2.88 %
2.89 @@ -715,13 +715,13 @@
2.90 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
2.91 \ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
2.92 \isacommand{declare}\isamarkupfalse%
2.93 -\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
2.94 +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
2.95 \isacommand{declare}\isamarkupfalse%
2.96 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
2.97 \isacommand{declare}\isamarkupfalse%
2.98 -\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
2.99 +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
2.100 \isacommand{lemma}\isamarkupfalse%
2.101 -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
2.102 +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
2.103 \ simp%
2.104 \endisataginvisible
2.105 {\isafoldinvisible}%
2.106 @@ -784,15 +784,15 @@
2.107 \newline%
2.108 \verb|fun eqop A_ a b = eq A_ a b;|\newline%
2.109 \newline%
2.110 -\verb|fun member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys|\newline%
2.111 -\verb| |\verb,|,\verb| member A_ x [] = false;|\newline%
2.112 +\verb|fun member A_ x [] = false|\newline%
2.113 +\verb| |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline%
2.114 \newline%
2.115 -\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
2.116 -\verb| (if member A_ z xs|\newline%
2.117 -\verb| then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
2.118 -\verb| else collect_duplicates A_ xs (z :: ys) zs)|\newline%
2.119 -\verb| else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline%
2.120 -\verb| |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline%
2.121 +\verb|fun collect_duplicates A_ xs ys [] = xs|\newline%
2.122 +\verb| |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline%
2.123 +\verb| (if member A_ z xs|\newline%
2.124 +\verb| then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
2.125 +\verb| else collect_duplicates A_ xs (z :: ys) zs)|\newline%
2.126 +\verb| else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline%
2.127 \newline%
2.128 \verb|end; (*struct Example*)|%
2.129 \end{isamarkuptext}%
2.130 @@ -835,11 +835,11 @@
2.131 \isakeyword{begin}\isanewline
2.132 \isanewline
2.133 \isacommand{definition}\isamarkupfalse%
2.134 -\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
2.135 +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
2.136 \ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
2.137 \isanewline
2.138 \isacommand{definition}\isamarkupfalse%
2.139 -\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
2.140 +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
2.141 \ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
2.142 \isanewline
2.143 \isacommand{instance}\isamarkupfalse%
2.144 @@ -852,7 +852,7 @@
2.145 \isanewline
2.146 \isanewline
2.147 \isacommand{lemma}\isamarkupfalse%
2.148 -\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.149 +\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
2.150 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
2.151 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
2.152 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
2.153 @@ -884,7 +884,7 @@
2.154 %
2.155 \isatagquoteme
2.156 \isacommand{lemma}\isamarkupfalse%
2.157 -\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.158 +\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
2.159 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
2.160 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
2.161 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
2.162 @@ -1007,7 +1007,7 @@
2.163 %
2.164 \isatagquoteme
2.165 \isacommand{lemma}\isamarkupfalse%
2.166 -\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.167 +\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
2.168 \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
2.169 \ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
2.170 \ \ \isacommand{by}\isamarkupfalse%
2.171 @@ -1038,8 +1038,8 @@
2.172 \newline%
2.173 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
2.174 \newline%
2.175 -\verb|fun null (x :: xs) = false|\newline%
2.176 -\verb| |\verb,|,\verb| null [] = true;|\newline%
2.177 +\verb|fun null [] = true|\newline%
2.178 +\verb| |\verb,|,\verb| null (x :: xs) = false;|\newline%
2.179 \newline%
2.180 \verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
2.181 \verb| |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 10 06:45:50 2008 +0200
3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 10 06:45:53 2008 +0200
3.3 @@ -993,7 +993,7 @@
3.4 syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
3.5 ;
3.6
3.7 - 'code' ('func' | 'inline') ( 'del' )?
3.8 + 'code' ( 'inline' ) ? ( 'del' ) ?
3.9 ;
3.10 \end{rail}
3.11
3.12 @@ -1080,13 +1080,13 @@
3.13 are not required to have a definition by means of defining equations;
3.14 if needed these are implemented by program abort instead.
3.15
3.16 - \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
3.17 - with option ``@{text "del:"}'' deselects) a defining equation for
3.18 + \item [@{attribute (HOL) code}] explicitly selects (or
3.19 + with option ``@{text "del"}'' deselects) a defining equation for
3.20 code generation. Usually packages introducing defining equations
3.21 provide a reasonable default setup for selection.
3.22
3.23 \item [@{attribute (HOL) code}@{text inline}] declares (or with
3.24 - option ``@{text "del:"}'' removes) inlining theorems which are
3.25 + option ``@{text "del"}'' removes) inlining theorems which are
3.26 applied as rewrite rules to any defining equation during
3.27 preprocessing.
3.28
4.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 10 06:45:50 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 10 06:45:53 2008 +0200
4.3 @@ -997,7 +997,7 @@
4.4 syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
4.5 ;
4.6
4.7 - 'code' ('func' | 'inline') ( 'del' )?
4.8 + 'code' ( 'inline' ) ? ( 'del' ) ?
4.9 ;
4.10 \end{rail}
4.11
4.12 @@ -1081,13 +1081,13 @@
4.13 are not required to have a definition by means of defining equations;
4.14 if needed these are implemented by program abort instead.
4.15
4.16 - \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
4.17 - with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
4.18 + \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or
4.19 + with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for
4.20 code generation. Usually packages introducing defining equations
4.21 provide a reasonable default setup for selection.
4.22
4.23 \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
4.24 - option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
4.25 + option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
4.26 applied as rewrite rules to any defining equation during
4.27 preprocessing.
4.28
5.1 --- a/src/HOL/Code_Eval.thy Fri Oct 10 06:45:50 2008 +0200
5.2 +++ b/src/HOL/Code_Eval.thy Fri Oct 10 06:45:53 2008 +0200
5.3 @@ -133,14 +133,14 @@
5.4
5.5 subsubsection {* Code generator setup *}
5.6
5.7 -lemmas [code func del] = term.recs term.cases term.size
5.8 -lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
5.9 +lemmas [code del] = term.recs term.cases term.size
5.10 +lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
5.11
5.12 -lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
5.13 -lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
5.14 -lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
5.15 +lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
5.16 +lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
5.17 +lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
5.18
5.19 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code func]: "Code_Eval.term_of c =
5.20 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
5.21 (let (n, m) = nibble_pair_of_char c
5.22 in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
5.23 (Code_Eval.term_of n)) (Code_Eval.term_of m))"
6.1 --- a/src/HOL/Code_Setup.thy Fri Oct 10 06:45:50 2008 +0200
6.2 +++ b/src/HOL/Code_Setup.thy Fri Oct 10 06:45:53 2008 +0200
6.3 @@ -21,32 +21,32 @@
6.4
6.5 text {* Code equations *}
6.6
6.7 -lemma [code func]:
6.8 +lemma [code]:
6.9 shows "False \<and> x \<longleftrightarrow> False"
6.10 and "True \<and> x \<longleftrightarrow> x"
6.11 and "x \<and> False \<longleftrightarrow> False"
6.12 and "x \<and> True \<longleftrightarrow> x" by simp_all
6.13
6.14 -lemma [code func]:
6.15 +lemma [code]:
6.16 shows "False \<or> x \<longleftrightarrow> x"
6.17 and "True \<or> x \<longleftrightarrow> True"
6.18 and "x \<or> False \<longleftrightarrow> x"
6.19 and "x \<or> True \<longleftrightarrow> True" by simp_all
6.20
6.21 -lemma [code func]:
6.22 +lemma [code]:
6.23 shows "\<not> True \<longleftrightarrow> False"
6.24 and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
6.25
6.26 -lemmas [code func] = Let_def if_True if_False
6.27 +lemmas [code] = Let_def if_True if_False
6.28
6.29 -lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
6.30 +lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
6.31
6.32 text {* Equality *}
6.33
6.34 context eq
6.35 begin
6.36
6.37 -lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
6.38 +lemma equals_eq [code inline, code]: "op = \<equiv> eq"
6.39 by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
6.40
6.41 declare eq [code unfold, code inline del]
7.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Oct 10 06:45:50 2008 +0200
7.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Oct 10 06:45:53 2008 +0200
7.3 @@ -481,7 +481,7 @@
7.4 "numgcdh (C i) = (\<lambda>g. zgcd i g)"
7.5 "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
7.6 "numgcdh t = (\<lambda>g. 1)"
7.7 -defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
7.8 +defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
7.9
7.10 recdef reducecoeffh "measure size"
7.11 "reducecoeffh (C i) = (\<lambda> g. C (i div g))"
8.1 --- a/src/HOL/Datatype.thy Fri Oct 10 06:45:50 2008 +0200
8.2 +++ b/src/HOL/Datatype.thy Fri Oct 10 06:45:53 2008 +0200
8.3 @@ -635,7 +635,7 @@
8.4 definition
8.5 option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
8.6 where
8.7 - [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
8.8 + [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
8.9
8.10 lemma option_map_None [simp, code]: "option_map f None = None"
8.11 by (simp add: option_map_def)
9.1 --- a/src/HOL/Divides.thy Fri Oct 10 06:45:50 2008 +0200
9.2 +++ b/src/HOL/Divides.thy Fri Oct 10 06:45:53 2008 +0200
9.3 @@ -127,7 +127,7 @@
9.4 note that ultimately show thesis by blast
9.5 qed
9.6
9.7 -lemma dvd_eq_mod_eq_0 [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
9.8 +lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
9.9 proof
9.10 assume "b mod a = 0"
9.11 with mod_div_equality [of b a] have "b div a * a = b" by simp
9.12 @@ -230,7 +230,7 @@
9.13 begin
9.14
9.15 definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
9.16 - [code func del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
9.17 + [code del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
9.18
9.19 definition div_nat where
9.20 "m div n = fst (divmod m n)"
10.1 --- a/src/HOL/Equiv_Relations.thy Fri Oct 10 06:45:50 2008 +0200
10.2 +++ b/src/HOL/Equiv_Relations.thy Fri Oct 10 06:45:53 2008 +0200
10.3 @@ -94,7 +94,7 @@
10.4 subsection {* Quotients *}
10.5
10.6 definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where
10.7 - [code func del]: "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
10.8 + [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
10.9
10.10 lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
10.11 by (unfold quotient_def) blast
11.1 --- a/src/HOL/Fun.thy Fri Oct 10 06:45:50 2008 +0200
11.2 +++ b/src/HOL/Fun.thy Fri Oct 10 06:45:53 2008 +0200
11.3 @@ -117,7 +117,7 @@
11.4
11.5 definition
11.6 bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
11.7 - [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
11.8 + [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
11.9
11.10 constdefs
11.11 surj :: "('a => 'b) => bool" (*surjective*)
12.1 --- a/src/HOL/HOL.thy Fri Oct 10 06:45:50 2008 +0200
12.2 +++ b/src/HOL/HOL.thy Fri Oct 10 06:45:53 2008 +0200
12.3 @@ -1227,7 +1227,7 @@
12.4
12.5 constdefs
12.6 simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1)
12.7 - [code func del]: "simp_implies \<equiv> op ==>"
12.8 + [code del]: "simp_implies \<equiv> op ==>"
12.9
12.10 lemma simp_impliesI:
12.11 assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
13.1 --- a/src/HOL/Hyperreal/Integration.thy Fri Oct 10 06:45:50 2008 +0200
13.2 +++ b/src/HOL/Hyperreal/Integration.thy Fri Oct 10 06:45:53 2008 +0200
13.3 @@ -16,29 +16,29 @@
13.4 --{*Partitions and tagged partitions etc.*}
13.5
13.6 partition :: "[(real*real),nat => real] => bool" where
13.7 - [code func del]: "partition = (%(a,b) D. D 0 = a &
13.8 + [code del]: "partition = (%(a,b) D. D 0 = a &
13.9 (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
13.10 (\<forall>n \<ge> N. D(n) = b)))"
13.11
13.12 definition
13.13 psize :: "(nat => real) => nat" where
13.14 - [code func del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
13.15 + [code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
13.16 (\<forall>n \<ge> N. D(n) = D(N)))"
13.17
13.18 definition
13.19 tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
13.20 - [code func del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
13.21 + [code del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
13.22 (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
13.23
13.24 --{*Gauges and gauge-fine divisions*}
13.25
13.26 definition
13.27 gauge :: "[real => bool, real => real] => bool" where
13.28 - [code func del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
13.29 + [code del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
13.30
13.31 definition
13.32 fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
13.33 - [code func del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
13.34 + [code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
13.35
13.36 --{*Riemann sum*}
13.37
13.38 @@ -50,7 +50,7 @@
13.39
13.40 definition
13.41 Integral :: "[(real*real),real=>real,real] => bool" where
13.42 - [code func del]: "Integral = (%(a,b) f k. \<forall>e > 0.
13.43 + [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
13.44 (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
13.45 (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
13.46 \<bar>rsum(D,p) f - k\<bar> < e)))"
14.1 --- a/src/HOL/Hyperreal/Lim.thy Fri Oct 10 06:45:50 2008 +0200
14.2 +++ b/src/HOL/Hyperreal/Lim.thy Fri Oct 10 06:45:53 2008 +0200
14.3 @@ -16,7 +16,7 @@
14.4 definition
14.5 LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
14.6 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
14.7 - [code func del]: "f -- a --> L =
14.8 + [code del]: "f -- a --> L =
14.9 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
14.10 --> norm (f x - L) < r)"
14.11
14.12 @@ -26,7 +26,7 @@
14.13
14.14 definition
14.15 isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
14.16 - [code func del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
14.17 + [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
14.18
14.19
14.20 subsection {* Limits of Functions *}
15.1 --- a/src/HOL/Hyperreal/SEQ.thy Fri Oct 10 06:45:50 2008 +0200
15.2 +++ b/src/HOL/Hyperreal/SEQ.thy Fri Oct 10 06:45:53 2008 +0200
15.3 @@ -15,13 +15,13 @@
15.4 definition
15.5 Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
15.6 --{*Standard definition of sequence converging to zero*}
15.7 - [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
15.8 + [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
15.9
15.10 definition
15.11 LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
15.12 ("((_)/ ----> (_))" [60, 60] 60) where
15.13 --{*Standard definition of convergence of sequence*}
15.14 - [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
15.15 + [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
15.16
15.17 definition
15.18 lim :: "(nat => 'a::real_normed_vector) => 'a" where
15.19 @@ -36,22 +36,22 @@
15.20 definition
15.21 Bseq :: "(nat => 'a::real_normed_vector) => bool" where
15.22 --{*Standard definition for bounded sequence*}
15.23 - [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
15.24 + [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
15.25
15.26 definition
15.27 monoseq :: "(nat=>real)=>bool" where
15.28 --{*Definition for monotonicity*}
15.29 - [code func del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
15.30 + [code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
15.31
15.32 definition
15.33 subseq :: "(nat => nat) => bool" where
15.34 --{*Definition of subsequence*}
15.35 - [code func del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
15.36 + [code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
15.37
15.38 definition
15.39 Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
15.40 --{*Standard definition of the Cauchy condition*}
15.41 - [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
15.42 + [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
15.43
15.44
15.45 subsection {* Bounded Sequences *}
16.1 --- a/src/HOL/Int.thy Fri Oct 10 06:45:50 2008 +0200
16.2 +++ b/src/HOL/Int.thy Fri Oct 10 06:45:53 2008 +0200
16.3 @@ -24,7 +24,7 @@
16.4 definition
16.5 intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
16.6 where
16.7 - [code func del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
16.8 + [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
16.9
16.10 typedef (Integ)
16.11 int = "UNIV//intrel"
16.12 @@ -34,34 +34,34 @@
16.13 begin
16.14
16.15 definition
16.16 - Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
16.17 + Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
16.18
16.19 definition
16.20 - One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
16.21 + One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
16.22
16.23 definition
16.24 - add_int_def [code func del]: "z + w = Abs_Integ
16.25 + add_int_def [code del]: "z + w = Abs_Integ
16.26 (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
16.27 intrel `` {(x + u, y + v)})"
16.28
16.29 definition
16.30 - minus_int_def [code func del]:
16.31 + minus_int_def [code del]:
16.32 "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
16.33
16.34 definition
16.35 - diff_int_def [code func del]: "z - w = z + (-w \<Colon> int)"
16.36 + diff_int_def [code del]: "z - w = z + (-w \<Colon> int)"
16.37
16.38 definition
16.39 - mult_int_def [code func del]: "z * w = Abs_Integ
16.40 + mult_int_def [code del]: "z * w = Abs_Integ
16.41 (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
16.42 intrel `` {(x*u + y*v, x*v + y*u)})"
16.43
16.44 definition
16.45 - le_int_def [code func del]:
16.46 + le_int_def [code del]:
16.47 "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
16.48
16.49 definition
16.50 - less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
16.51 + less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
16.52
16.53 definition
16.54 zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
16.55 @@ -298,7 +298,7 @@
16.56 definition
16.57 of_int :: "int \<Rightarrow> 'a"
16.58 where
16.59 - [code func del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
16.60 + [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
16.61
16.62 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
16.63 proof -
16.64 @@ -390,7 +390,7 @@
16.65 definition
16.66 nat :: "int \<Rightarrow> nat"
16.67 where
16.68 - [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
16.69 + [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
16.70
16.71 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
16.72 proof -
16.73 @@ -585,19 +585,19 @@
16.74
16.75 definition
16.76 Pls :: int where
16.77 - [code func del]: "Pls = 0"
16.78 + [code del]: "Pls = 0"
16.79
16.80 definition
16.81 Min :: int where
16.82 - [code func del]: "Min = - 1"
16.83 + [code del]: "Min = - 1"
16.84
16.85 definition
16.86 Bit0 :: "int \<Rightarrow> int" where
16.87 - [code func del]: "Bit0 k = k + k"
16.88 + [code del]: "Bit0 k = k + k"
16.89
16.90 definition
16.91 Bit1 :: "int \<Rightarrow> int" where
16.92 - [code func del]: "Bit1 k = 1 + k + k"
16.93 + [code del]: "Bit1 k = 1 + k + k"
16.94
16.95 class number = type + -- {* for numeric types: nat, int, real, \dots *}
16.96 fixes number_of :: "int \<Rightarrow> 'a"
16.97 @@ -622,11 +622,11 @@
16.98
16.99 definition
16.100 succ :: "int \<Rightarrow> int" where
16.101 - [code func del]: "succ k = k + 1"
16.102 + [code del]: "succ k = k + 1"
16.103
16.104 definition
16.105 pred :: "int \<Rightarrow> int" where
16.106 - [code func del]: "pred k = k - 1"
16.107 + [code del]: "pred k = k - 1"
16.108
16.109 lemmas
16.110 max_number_of [simp] = max_def
16.111 @@ -785,7 +785,7 @@
16.112 begin
16.113
16.114 definition
16.115 - int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
16.116 + int_number_of_def [code del]: "number_of w = (of_int w \<Colon> int)"
16.117
16.118 instance
16.119 by intro_classes (simp only: int_number_of_def)
16.120 @@ -1167,7 +1167,7 @@
16.121 definition
16.122 Ints :: "'a set"
16.123 where
16.124 - [code func del]: "Ints = range of_int"
16.125 + [code del]: "Ints = range of_int"
16.126
16.127 end
16.128
16.129 @@ -1799,36 +1799,36 @@
16.130
16.131 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
16.132
16.133 -lemmas pred_succ_numeral_code [code func] =
16.134 +lemmas pred_succ_numeral_code [code] =
16.135 pred_bin_simps succ_bin_simps
16.136
16.137 -lemmas plus_numeral_code [code func] =
16.138 +lemmas plus_numeral_code [code] =
16.139 add_bin_simps
16.140 arith_extra_simps(1) [where 'a = int]
16.141
16.142 -lemmas minus_numeral_code [code func] =
16.143 +lemmas minus_numeral_code [code] =
16.144 minus_bin_simps
16.145 arith_extra_simps(2) [where 'a = int]
16.146 arith_extra_simps(5) [where 'a = int]
16.147
16.148 -lemmas times_numeral_code [code func] =
16.149 +lemmas times_numeral_code [code] =
16.150 mult_bin_simps
16.151 arith_extra_simps(4) [where 'a = int]
16.152
16.153 instantiation int :: eq
16.154 begin
16.155
16.156 -definition [code func del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
16.157 +definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
16.158
16.159 instance by default (simp add: eq_int_def)
16.160
16.161 end
16.162
16.163 -lemma eq_number_of_int_code [code func]:
16.164 +lemma eq_number_of_int_code [code]:
16.165 "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
16.166 unfolding eq_int_def number_of_is_id ..
16.167
16.168 -lemma eq_int_code [code func]:
16.169 +lemma eq_int_code [code]:
16.170 "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
16.171 "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
16.172 "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
16.173 @@ -1859,11 +1859,11 @@
16.174 "eq_class.eq (k::int) k \<longleftrightarrow> True"
16.175 by (rule HOL.eq_refl)
16.176
16.177 -lemma less_eq_number_of_int_code [code func]:
16.178 +lemma less_eq_number_of_int_code [code]:
16.179 "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
16.180 unfolding number_of_is_id ..
16.181
16.182 -lemma less_eq_int_code [code func]:
16.183 +lemma less_eq_int_code [code]:
16.184 "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
16.185 "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
16.186 "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
16.187 @@ -1890,11 +1890,11 @@
16.188 (auto simp add: neg_def linorder_not_less group_simps
16.189 zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
16.190
16.191 -lemma less_number_of_int_code [code func]:
16.192 +lemma less_number_of_int_code [code]:
16.193 "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
16.194 unfolding number_of_is_id ..
16.195
16.196 -lemma less_int_code [code func]:
16.197 +lemma less_int_code [code]:
16.198 "Int.Pls < Int.Pls \<longleftrightarrow> False"
16.199 "Int.Pls < Int.Min \<longleftrightarrow> False"
16.200 "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
16.201 @@ -1935,11 +1935,11 @@
16.202
16.203 hide (open) const nat_aux
16.204
16.205 -lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
16.206 +lemma zero_is_num_zero [code, code inline, symmetric, code post]:
16.207 "(0\<Colon>int) = Numeral0"
16.208 by simp
16.209
16.210 -lemma one_is_num_one [code func, code inline, symmetric, code post]:
16.211 +lemma one_is_num_one [code, code inline, symmetric, code post]:
16.212 "(1\<Colon>int) = Numeral1"
16.213 by simp
16.214
17.1 --- a/src/HOL/IntDiv.thy Fri Oct 10 06:45:50 2008 +0200
17.2 +++ b/src/HOL/IntDiv.thy Fri Oct 10 06:45:53 2008 +0200
17.3 @@ -14,13 +14,13 @@
17.4 constdefs
17.5 quorem :: "(int*int) * (int*int) => bool"
17.6 --{*definition of quotient and remainder*}
17.7 - [code func]: "quorem == %((a,b), (q,r)).
17.8 + [code]: "quorem == %((a,b), (q,r)).
17.9 a = b*q + r &
17.10 (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
17.11
17.12 adjust :: "[int, int*int] => int*int"
17.13 --{*for the division algorithm*}
17.14 - [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
17.15 + [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
17.16 else (2*q, r)"
17.17
17.18 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
17.19 @@ -46,7 +46,7 @@
17.20 text{*algorithm for the general case @{term "b\<noteq>0"}*}
17.21 constdefs
17.22 negateSnd :: "int*int => int*int"
17.23 - [code func]: "negateSnd == %(q,r). (q,-r)"
17.24 + [code]: "negateSnd == %(q,r). (q,-r)"
17.25
17.26 definition
17.27 divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
17.28 @@ -1477,7 +1477,7 @@
17.29 context ring_1
17.30 begin
17.31
17.32 -lemma of_int_num [code func]:
17.33 +lemma of_int_num [code]:
17.34 "of_int k = (if k = 0 then 0 else if k < 0 then
17.35 - of_int (- k) else let
17.36 (l, m) = divAlg (k, 2);
18.1 --- a/src/HOL/Lattices.thy Fri Oct 10 06:45:50 2008 +0200
18.2 +++ b/src/HOL/Lattices.thy Fri Oct 10 06:45:53 2008 +0200
18.3 @@ -9,7 +9,7 @@
18.4 imports Fun
18.5 begin
18.6
18.7 -subsection{* Lattices *}
18.8 +subsection {* Lattices *}
18.9
18.10 notation
18.11 less_eq (infix "\<sqsubseteq>" 50) and
18.12 @@ -40,7 +40,7 @@
18.13 class lattice = lower_semilattice + upper_semilattice
18.14
18.15
18.16 -subsubsection{* Intro and elim rules*}
18.17 +subsubsection {* Intro and elim rules*}
18.18
18.19 context lower_semilattice
18.20 begin
18.21 @@ -512,10 +512,10 @@
18.22 begin
18.23
18.24 definition
18.25 - inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
18.26 + inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
18.27
18.28 definition
18.29 - sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
18.30 + sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
18.31
18.32 instance
18.33 apply intro_classes
18.34 @@ -536,10 +536,10 @@
18.35 begin
18.36
18.37 definition
18.38 - Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
18.39 + Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
18.40
18.41 definition
18.42 - Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
18.43 + Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
18.44
18.45 instance
18.46 by intro_classes
19.1 --- a/src/HOL/Library/Array.thy Fri Oct 10 06:45:50 2008 +0200
19.2 +++ b/src/HOL/Library/Array.thy Fri Oct 10 06:45:53 2008 +0200
19.3 @@ -107,14 +107,14 @@
19.4
19.5 subsection {* Properties *}
19.6
19.7 -lemma array_make [code func]:
19.8 +lemma array_make [code]:
19.9 "Array.new n x = make n (\<lambda>_. x)"
19.10 by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
19.11 monad_simp array_of_list_replicate [symmetric]
19.12 map_replicate_trivial replicate_append_same
19.13 of_list_def)
19.14
19.15 -lemma array_of_list_make [code func]:
19.16 +lemma array_of_list_make [code]:
19.17 "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
19.18 unfolding make_def map_nth ..
19.19
19.20 @@ -126,28 +126,28 @@
19.21 definition new' where
19.22 [code del]: "new' = Array.new o nat_of_index"
19.23 hide (open) const new'
19.24 -lemma [code func]:
19.25 +lemma [code]:
19.26 "Array.new = Array.new' o index_of_nat"
19.27 by (simp add: new'_def o_def)
19.28
19.29 definition of_list' where
19.30 [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
19.31 hide (open) const of_list'
19.32 -lemma [code func]:
19.33 +lemma [code]:
19.34 "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
19.35 by (simp add: of_list'_def)
19.36
19.37 definition make' where
19.38 [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
19.39 hide (open) const make'
19.40 -lemma [code func]:
19.41 +lemma [code]:
19.42 "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
19.43 by (simp add: make'_def o_def)
19.44
19.45 definition length' where
19.46 [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
19.47 hide (open) const length'
19.48 -lemma [code func]:
19.49 +lemma [code]:
19.50 "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
19.51 by (simp add: length'_def monad_simp',
19.52 simp add: liftM_def comp_def monad_simp,
19.53 @@ -156,14 +156,14 @@
19.54 definition nth' where
19.55 [code del]: "nth' a = Array.nth a o nat_of_index"
19.56 hide (open) const nth'
19.57 -lemma [code func]:
19.58 +lemma [code]:
19.59 "Array.nth a n = Array.nth' a (index_of_nat n)"
19.60 by (simp add: nth'_def)
19.61
19.62 definition upd' where
19.63 [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
19.64 hide (open) const upd'
19.65 -lemma [code func]:
19.66 +lemma [code]:
19.67 "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
19.68 by (simp add: upd'_def monad_simp upd_return)
19.69
20.1 --- a/src/HOL/Library/Char_nat.thy Fri Oct 10 06:45:50 2008 +0200
20.2 +++ b/src/HOL/Library/Char_nat.thy Fri Oct 10 06:45:53 2008 +0200
20.3 @@ -54,7 +54,7 @@
20.4 "nibble_of_nat (n mod 16) = nibble_of_nat n"
20.5 unfolding nibble_of_nat_def Let_def by auto
20.6
20.7 -lemmas [code func] = nibble_of_nat_norm [symmetric]
20.8 +lemmas [code] = nibble_of_nat_norm [symmetric]
20.9
20.10 lemma nibble_of_nat_simps [simp]:
20.11 "nibble_of_nat 0 = Nibble0"
20.12 @@ -75,7 +75,7 @@
20.13 "nibble_of_nat 15 = NibbleF"
20.14 unfolding nibble_of_nat_def Let_def by auto
20.15
20.16 -lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
20.17 +lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
20.18 [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
20.19
20.20 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
20.21 @@ -115,7 +115,7 @@
20.22 nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
20.23 "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
20.24
20.25 -lemma nibble_of_pair [code func]:
20.26 +lemma nibble_of_pair [code]:
20.27 "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
20.28 unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
20.29
21.1 --- a/src/HOL/Library/Char_ord.thy Fri Oct 10 06:45:50 2008 +0200
21.2 +++ b/src/HOL/Library/Char_ord.thy Fri Oct 10 06:45:53 2008 +0200
21.3 @@ -64,11 +64,11 @@
21.4 begin
21.5
21.6 definition
21.7 - char_less_eq_def [code func del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
21.8 + char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
21.9 n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
21.10
21.11 definition
21.12 - char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
21.13 + char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
21.14 n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
21.15
21.16 instance
21.17 @@ -90,7 +90,7 @@
21.18
21.19 end
21.20
21.21 -lemma [simp, code func]:
21.22 +lemma [simp, code]:
21.23 shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
21.24 and char_less_simp: "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
21.25 unfolding char_less_eq_def char_less_def by simp_all
22.1 --- a/src/HOL/Library/Code_Char_chr.thy Fri Oct 10 06:45:50 2008 +0200
22.2 +++ b/src/HOL/Library/Code_Char_chr.thy Fri Oct 10 06:45:53 2008 +0200
22.3 @@ -12,28 +12,28 @@
22.4 definition
22.5 "int_of_char = int o nat_of_char"
22.6
22.7 -lemma [code func]:
22.8 +lemma [code]:
22.9 "nat_of_char = nat o int_of_char"
22.10 unfolding int_of_char_def by (simp add: expand_fun_eq)
22.11
22.12 definition
22.13 "char_of_int = char_of_nat o nat"
22.14
22.15 -lemma [code func]:
22.16 +lemma [code]:
22.17 "char_of_nat = char_of_int o int"
22.18 unfolding char_of_int_def by (simp add: expand_fun_eq)
22.19
22.20 -lemmas [code func del] = char.recs char.cases char.size
22.21 +lemmas [code del] = char.recs char.cases char.size
22.22
22.23 -lemma [code func, code inline]:
22.24 +lemma [code, code inline]:
22.25 "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
22.26 by (cases c) (auto simp add: nibble_pair_of_nat_char)
22.27
22.28 -lemma [code func, code inline]:
22.29 +lemma [code, code inline]:
22.30 "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
22.31 by (cases c) (auto simp add: nibble_pair_of_nat_char)
22.32
22.33 -lemma [code func]:
22.34 +lemma [code]:
22.35 "size (c\<Colon>char) = 0"
22.36 by (cases c) auto
22.37
23.1 --- a/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:50 2008 +0200
23.2 +++ b/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:53 2008 +0200
23.3 @@ -64,7 +64,7 @@
23.4 instantiation index :: zero
23.5 begin
23.6
23.7 -definition [simp, code func del]:
23.8 +definition [simp, code del]:
23.9 "0 = index_of_nat 0"
23.10
23.11 instance ..
23.12 @@ -87,12 +87,12 @@
23.13 then show "P k" by simp
23.14 qed simp_all
23.15
23.16 -lemmas [code func del] = index.recs index.cases
23.17 +lemmas [code del] = index.recs index.cases
23.18
23.19 declare index_case [case_names nat, cases type: index]
23.20 declare index.induct [case_names nat, induct type: index]
23.21
23.22 -lemma [code func]:
23.23 +lemma [code]:
23.24 "index_size = nat_of_index"
23.25 proof (rule ext)
23.26 fix k
23.27 @@ -102,7 +102,7 @@
23.28 finally show "index_size k = nat_of_index k" .
23.29 qed
23.30
23.31 -lemma [code func]:
23.32 +lemma [code]:
23.33 "size = nat_of_index"
23.34 proof (rule ext)
23.35 fix k
23.36 @@ -110,7 +110,7 @@
23.37 by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
23.38 qed
23.39
23.40 -lemma [code func]:
23.41 +lemma [code]:
23.42 "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
23.43 by (cases k, cases l) (simp add: eq)
23.44
23.45 @@ -143,63 +143,63 @@
23.46 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
23.47 begin
23.48
23.49 -lemma zero_index_code [code inline, code func]:
23.50 +lemma zero_index_code [code inline, code]:
23.51 "(0\<Colon>index) = Numeral0"
23.52 by (simp add: number_of_index_def Pls_def)
23.53 lemma [code post]: "Numeral0 = (0\<Colon>index)"
23.54 using zero_index_code ..
23.55
23.56 -definition [simp, code func del]:
23.57 +definition [simp, code del]:
23.58 "(1\<Colon>index) = index_of_nat 1"
23.59
23.60 -lemma one_index_code [code inline, code func]:
23.61 +lemma one_index_code [code inline, code]:
23.62 "(1\<Colon>index) = Numeral1"
23.63 by (simp add: number_of_index_def Pls_def Bit1_def)
23.64 lemma [code post]: "Numeral1 = (1\<Colon>index)"
23.65 using one_index_code ..
23.66
23.67 -definition [simp, code func del]:
23.68 +definition [simp, code del]:
23.69 "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
23.70
23.71 -lemma plus_index_code [code func]:
23.72 +lemma plus_index_code [code]:
23.73 "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
23.74 by simp
23.75
23.76 -definition [simp, code func del]:
23.77 +definition [simp, code del]:
23.78 "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
23.79
23.80 -definition [simp, code func del]:
23.81 +definition [simp, code del]:
23.82 "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
23.83
23.84 -lemma times_index_code [code func]:
23.85 +lemma times_index_code [code]:
23.86 "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
23.87 by simp
23.88
23.89 -definition [simp, code func del]:
23.90 +definition [simp, code del]:
23.91 "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
23.92
23.93 -definition [simp, code func del]:
23.94 +definition [simp, code del]:
23.95 "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
23.96
23.97 -lemma div_index_code [code func]:
23.98 +lemma div_index_code [code]:
23.99 "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
23.100 by simp
23.101
23.102 -lemma mod_index_code [code func]:
23.103 +lemma mod_index_code [code]:
23.104 "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
23.105 by simp
23.106
23.107 -definition [simp, code func del]:
23.108 +definition [simp, code del]:
23.109 "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
23.110
23.111 -definition [simp, code func del]:
23.112 +definition [simp, code del]:
23.113 "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
23.114
23.115 -lemma less_eq_index_code [code func]:
23.116 +lemma less_eq_index_code [code]:
23.117 "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
23.118 by simp
23.119
23.120 -lemma less_index_code [code func]:
23.121 +lemma less_index_code [code]:
23.122 "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
23.123 by simp
23.124
23.125 @@ -260,25 +260,25 @@
23.126 definition
23.127 minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
23.128 where
23.129 - [code func del]: "minus_index_aux = op -"
23.130 + [code del]: "minus_index_aux = op -"
23.131
23.132 -lemma [code func]: "op - = minus_index_aux"
23.133 +lemma [code]: "op - = minus_index_aux"
23.134 using minus_index_aux_def ..
23.135
23.136 definition
23.137 div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index"
23.138 where
23.139 - [code func del]: "div_mod_index n m = (n div m, n mod m)"
23.140 + [code del]: "div_mod_index n m = (n div m, n mod m)"
23.141
23.142 -lemma [code func]:
23.143 +lemma [code]:
23.144 "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
23.145 unfolding div_mod_index_def by auto
23.146
23.147 -lemma [code func]:
23.148 +lemma [code]:
23.149 "n div m = fst (div_mod_index n m)"
23.150 unfolding div_mod_index_def by simp
23.151
23.152 -lemma [code func]:
23.153 +lemma [code]:
23.154 "n mod m = snd (div_mod_index n m)"
23.155 unfolding div_mod_index_def by simp
23.156
23.157 @@ -340,7 +340,7 @@
23.158
23.159 text {* Evaluation *}
23.160
23.161 -lemma [code func, code func del]:
23.162 +lemma [code, code del]:
23.163 "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
23.164
23.165 code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
24.1 --- a/src/HOL/Library/Code_Integer.thy Fri Oct 10 06:45:50 2008 +0200
24.2 +++ b/src/HOL/Library/Code_Integer.thy Fri Oct 10 06:45:53 2008 +0200
24.3 @@ -92,7 +92,7 @@
24.4
24.5 text {* Evaluation *}
24.6
24.7 -lemma [code func, code func del]:
24.8 +lemma [code, code del]:
24.9 "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" ..
24.10
24.11 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
25.1 --- a/src/HOL/Library/Code_Message.thy Fri Oct 10 06:45:50 2008 +0200
25.2 +++ b/src/HOL/Library/Code_Message.thy Fri Oct 10 06:45:53 2008 +0200
25.3 @@ -12,12 +12,12 @@
25.4
25.5 datatype message_string = STR string
25.6
25.7 -lemmas [code func del] = message_string.recs message_string.cases
25.8 +lemmas [code del] = message_string.recs message_string.cases
25.9
25.10 -lemma [code func]: "size (s\<Colon>message_string) = 0"
25.11 +lemma [code]: "size (s\<Colon>message_string) = 0"
25.12 by (cases s) simp_all
25.13
25.14 -lemma [code func]: "message_string_size (s\<Colon>message_string) = 0"
25.15 +lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
25.16 by (cases s) simp_all
25.17
25.18 subsection {* ML interface *}
26.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Oct 10 06:45:50 2008 +0200
26.2 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Oct 10 06:45:53 2008 +0200
26.3 @@ -232,7 +232,6 @@
26.4 of NONE => NONE
26.5 | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
26.6 then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
26.7 - (*FIXME*)
26.8 end
26.9
26.10 in
26.11 @@ -344,13 +343,13 @@
26.12 definition
26.13 int :: "nat \<Rightarrow> int"
26.14 where
26.15 - [code func del]: "int = of_nat"
26.16 + [code del]: "int = of_nat"
26.17
26.18 -lemma int_code' [code func]:
26.19 +lemma int_code' [code]:
26.20 "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
26.21 unfolding int_nat_number_of [folded int_def] ..
26.22
26.23 -lemma nat_code' [code func]:
26.24 +lemma nat_code' [code]:
26.25 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
26.26 by auto
26.27
26.28 @@ -434,7 +433,7 @@
26.29
26.30 text {* Evaluation *}
26.31
26.32 -lemma [code func, code func del]:
26.33 +lemma [code, code del]:
26.34 "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
26.35
26.36 code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
27.1 --- a/src/HOL/Library/Enum.thy Fri Oct 10 06:45:50 2008 +0200
27.2 +++ b/src/HOL/Library/Enum.thy Fri Oct 10 06:45:53 2008 +0200
27.3 @@ -13,7 +13,7 @@
27.4
27.5 class enum = itself +
27.6 fixes enum :: "'a list"
27.7 - assumes UNIV_enum [code func]: "UNIV = set enum"
27.8 + assumes UNIV_enum [code]: "UNIV = set enum"
27.9 and enum_distinct: "distinct enum"
27.10 begin
27.11
27.12 @@ -49,7 +49,7 @@
27.13
27.14 end
27.15
27.16 -lemma order_fun [code func]:
27.17 +lemma order_fun [code]:
27.18 fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
27.19 shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
27.20 and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
27.21 @@ -58,10 +58,10 @@
27.22
27.23 subsection {* Quantifiers *}
27.24
27.25 -lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
27.26 +lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
27.27 by (simp add: list_all_iff enum_all)
27.28
27.29 -lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
27.30 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
27.31 by (simp add: list_all_iff enum_all)
27.32
27.33
27.34 @@ -157,7 +157,7 @@
27.35 begin
27.36
27.37 definition
27.38 - [code func del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
27.39 + [code del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
27.40
27.41 instance proof
27.42 show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
27.43 @@ -177,7 +177,7 @@
27.44
27.45 end
27.46
27.47 -lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
27.48 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
27.49 in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
27.50 by (simp add: enum_fun_def Let_def)
27.51
27.52 @@ -286,9 +286,9 @@
27.53 begin
27.54
27.55 definition
27.56 - [code func del]: "enum = map (split Char) (product enum enum)"
27.57 + [code del]: "enum = map (split Char) (product enum enum)"
27.58
27.59 -lemma enum_char [code func]:
27.60 +lemma enum_char [code]:
27.61 "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
27.62 Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
27.63 Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
28.1 --- a/src/HOL/Library/GCD.thy Fri Oct 10 06:45:50 2008 +0200
28.2 +++ b/src/HOL/Library/GCD.thy Fri Oct 10 06:45:53 2008 +0200
28.3 @@ -18,7 +18,7 @@
28.4
28.5 definition
28.6 is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
28.7 - [code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
28.8 + [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
28.9 (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
28.10
28.11 text {* Uniqueness *}
28.12 @@ -776,7 +776,7 @@
28.13 thus ?thesis by (simp add: zlcm_def)
28.14 qed
28.15
28.16 -lemma zgcd_code [code func]:
28.17 +lemma zgcd_code [code]:
28.18 "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
28.19 by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
28.20
29.1 --- a/src/HOL/Library/Heap_Monad.thy Fri Oct 10 06:45:50 2008 +0200
29.2 +++ b/src/HOL/Library/Heap_Monad.thy Fri Oct 10 06:45:53 2008 +0200
29.3 @@ -266,14 +266,14 @@
29.4 definition
29.5 Fail :: "message_string \<Rightarrow> exception"
29.6 where
29.7 - [code func del]: "Fail s = Exn"
29.8 + [code del]: "Fail s = Exn"
29.9
29.10 definition
29.11 raise_exc :: "exception \<Rightarrow> 'a Heap"
29.12 where
29.13 - [code func del]: "raise_exc e = raise []"
29.14 + [code del]: "raise_exc e = raise []"
29.15
29.16 -lemma raise_raise_exc [code func, code inline]:
29.17 +lemma raise_raise_exc [code, code inline]:
29.18 "raise s = raise_exc (Fail (STR s))"
29.19 unfolding Fail_def raise_exc_def raise_def ..
29.20
30.1 --- a/src/HOL/Library/List_Prefix.thy Fri Oct 10 06:45:50 2008 +0200
30.2 +++ b/src/HOL/Library/List_Prefix.thy Fri Oct 10 06:45:53 2008 +0200
30.3 @@ -15,10 +15,10 @@
30.4 begin
30.5
30.6 definition
30.7 - prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
30.8 + prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
30.9
30.10 definition
30.11 - strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
30.12 + strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
30.13
30.14 instance
30.15 by intro_classes (auto simp add: prefix_def strict_prefix_def)
30.16 @@ -374,18 +374,18 @@
30.17
30.18 subsection {* Executable code *}
30.19
30.20 -lemma less_eq_code [code func]:
30.21 +lemma less_eq_code [code]:
30.22 "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
30.23 "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
30.24 "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
30.25 by simp_all
30.26
30.27 -lemma less_code [code func]:
30.28 +lemma less_code [code]:
30.29 "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
30.30 "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
30.31 "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
30.32 unfolding strict_prefix_def by auto
30.33
30.34 -lemmas [code func] = postfix_to_prefix
30.35 +lemmas [code] = postfix_to_prefix
30.36
30.37 end
31.1 --- a/src/HOL/Library/List_lexord.thy Fri Oct 10 06:45:50 2008 +0200
31.2 +++ b/src/HOL/Library/List_lexord.thy Fri Oct 10 06:45:53 2008 +0200
31.3 @@ -13,10 +13,10 @@
31.4 begin
31.5
31.6 definition
31.7 - list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
31.8 + list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
31.9
31.10 definition
31.11 - list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
31.12 + list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
31.13
31.14 instance ..
31.15
31.16 @@ -63,10 +63,10 @@
31.17 begin
31.18
31.19 definition
31.20 - [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
31.21 + [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
31.22
31.23 definition
31.24 - [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
31.25 + [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
31.26
31.27 instance
31.28 by intro_classes
31.29 @@ -92,13 +92,13 @@
31.30 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
31.31 by (unfold list_le_def) auto
31.32
31.33 -lemma less_code [code func]:
31.34 +lemma less_code [code]:
31.35 "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
31.36 "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
31.37 "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
31.38 by simp_all
31.39
31.40 -lemma less_eq_code [code func]:
31.41 +lemma less_eq_code [code]:
31.42 "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
31.43 "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
31.44 "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
32.1 --- a/src/HOL/Library/Multiset.thy Fri Oct 10 06:45:50 2008 +0200
32.2 +++ b/src/HOL/Library/Multiset.thy Fri Oct 10 06:45:53 2008 +0200
32.3 @@ -29,7 +29,7 @@
32.4 "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
32.5
32.6 declare
32.7 - Mempty_def[code func del] single_def[code func del]
32.8 + Mempty_def[code del] single_def[code del]
32.9
32.10 definition
32.11 count :: "'a multiset => 'a => nat" where
32.12 @@ -59,7 +59,7 @@
32.13 begin
32.14
32.15 definition
32.16 - union_def[code func del]:
32.17 + union_def[code del]:
32.18 "M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
32.19
32.20 definition
32.21 @@ -69,7 +69,7 @@
32.22 Zero_multiset_def [simp]: "0 = {#}"
32.23
32.24 definition
32.25 - size_def[code func del]: "size M = setsum (count M) (set_of M)"
32.26 + size_def[code del]: "size M = setsum (count M) (set_of M)"
32.27
32.28 instance ..
32.29
32.30 @@ -207,10 +207,10 @@
32.31
32.32 subsubsection {* Size *}
32.33
32.34 -lemma size_empty [simp,code func]: "size {#} = 0"
32.35 +lemma size_empty [simp,code]: "size {#} = 0"
32.36 by (simp add: size_def)
32.37
32.38 -lemma size_single [simp,code func]: "size {#b#} = 1"
32.39 +lemma size_single [simp,code]: "size {#b#} = 1"
32.40 by (simp add: size_def)
32.41
32.42 lemma finite_set_of [iff]: "finite (set_of M)"
32.43 @@ -223,7 +223,7 @@
32.44 apply (simp add: Int_insert_left set_of_def)
32.45 done
32.46
32.47 -lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N"
32.48 +lemma size_union[simp,code]: "size (M + N::'a multiset) = size M + size N"
32.49 apply (unfold size_def)
32.50 apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
32.51 prefer 2
32.52 @@ -376,16 +376,16 @@
32.53
32.54 subsubsection {* Comprehension (filter) *}
32.55
32.56 -lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
32.57 +lemma MCollect_empty[simp, code]: "MCollect {#} P = {#}"
32.58 by (simp add: MCollect_def Mempty_def Abs_multiset_inject
32.59 in_multiset expand_fun_eq)
32.60
32.61 -lemma MCollect_single[simp, code func]:
32.62 +lemma MCollect_single[simp, code]:
32.63 "MCollect {#x#} P = (if P x then {#x#} else {#})"
32.64 by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
32.65 in_multiset expand_fun_eq)
32.66
32.67 -lemma MCollect_union[simp, code func]:
32.68 +lemma MCollect_union[simp, code]:
32.69 "MCollect (M+N) f = MCollect M f + MCollect N f"
32.70 by (simp add: MCollect_def union_def Abs_multiset_inject
32.71 in_multiset expand_fun_eq)
32.72 @@ -500,7 +500,7 @@
32.73
32.74 definition
32.75 mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
32.76 - [code func del]:"mult1 r =
32.77 + [code del]:"mult1 r =
32.78 {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
32.79 (\<forall>b. b :# K --> (b, a) \<in> r)}"
32.80
32.81 @@ -716,10 +716,10 @@
32.82 begin
32.83
32.84 definition
32.85 - less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
32.86 + less_multiset_def [code del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
32.87
32.88 definition
32.89 - le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
32.90 + le_multiset_def [code del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
32.91
32.92 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
32.93 unfolding trans_def by (blast intro: order_less_trans)
32.94 @@ -983,11 +983,11 @@
32.95
32.96 definition
32.97 mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
32.98 - [code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
32.99 + [code del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
32.100
32.101 definition
32.102 mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
32.103 - [code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
32.104 + [code del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
32.105
32.106 notation mset_le (infix "\<subseteq>#" 50)
32.107 notation mset_less (infix "\<subset>#" 50)
32.108 @@ -1448,22 +1448,22 @@
32.109
32.110 subsection {* Image *}
32.111
32.112 -definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
32.113 +definition [code del]: "image_mset f == fold_mset (op + o single o f) {#}"
32.114
32.115 interpretation image_left_comm: left_commutative ["op + o single o f"]
32.116 by (unfold_locales) (simp add:union_ac)
32.117
32.118 -lemma image_mset_empty [simp, code func]: "image_mset f {#} = {#}"
32.119 +lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
32.120 by (simp add: image_mset_def)
32.121
32.122 -lemma image_mset_single [simp, code func]: "image_mset f {#x#} = {#f x#}"
32.123 +lemma image_mset_single [simp, code]: "image_mset f {#x#} = {#f x#}"
32.124 by (simp add: image_mset_def)
32.125
32.126 lemma image_mset_insert:
32.127 "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
32.128 by (simp add: image_mset_def add_ac)
32.129
32.130 -lemma image_mset_union[simp, code func]:
32.131 +lemma image_mset_union[simp, code]:
32.132 "image_mset f (M+N) = image_mset f M + image_mset f N"
32.133 apply (induct N)
32.134 apply simp
33.1 --- a/src/HOL/Library/Nat_Infinity.thy Fri Oct 10 06:45:50 2008 +0200
33.2 +++ b/src/HOL/Library/Nat_Infinity.thy Fri Oct 10 06:45:53 2008 +0200
33.3 @@ -37,7 +37,7 @@
33.4 [code inline]: "1 = Fin 1"
33.5
33.6 definition
33.7 - [code inline, code func del]: "number_of k = Fin (number_of k)"
33.8 + [code inline, code del]: "number_of k = Fin (number_of k)"
33.9
33.10 instance ..
33.11
34.1 --- a/src/HOL/Library/Nested_Environment.thy Fri Oct 10 06:45:50 2008 +0200
34.2 +++ b/src/HOL/Library/Nested_Environment.thy Fri Oct 10 06:45:53 2008 +0200
34.3 @@ -525,11 +525,11 @@
34.4
34.5 text {* Environments and code generation *}
34.6
34.7 -lemma [code func, code func del]:
34.8 +lemma [code, code del]:
34.9 fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
34.10 shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
34.11
34.12 -lemma eq_env_code [code func]:
34.13 +lemma eq_env_code [code]:
34.14 fixes x y :: "'a\<Colon>eq"
34.15 and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
34.16 shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
34.17 @@ -567,7 +567,7 @@
34.18 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
34.19 qed simp_all
34.20
34.21 -lemma [code func, code func del]:
34.22 +lemma [code, code del]:
34.23 "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
34.24
34.25 end
35.1 --- a/src/HOL/Library/Option_ord.thy Fri Oct 10 06:45:50 2008 +0200
35.2 +++ b/src/HOL/Library/Option_ord.thy Fri Oct 10 06:45:53 2008 +0200
35.3 @@ -13,10 +13,10 @@
35.4 begin
35.5
35.6 definition less_eq_option where
35.7 - [code func del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
35.8 + [code del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
35.9
35.10 definition less_option where
35.11 - [code func del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
35.12 + [code del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
35.13
35.14 lemma less_eq_option_None [simp]: "None \<le> x"
35.15 by (simp add: less_eq_option_def)
36.1 --- a/src/HOL/Library/Primes.thy Fri Oct 10 06:45:50 2008 +0200
36.2 +++ b/src/HOL/Library/Primes.thy Fri Oct 10 06:45:53 2008 +0200
36.3 @@ -16,7 +16,7 @@
36.4
36.5 definition
36.6 prime :: "nat \<Rightarrow> bool" where
36.7 - [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
36.8 + [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
36.9
36.10
36.11 lemma two_is_prime: "prime 2"
37.1 --- a/src/HOL/Library/Product_ord.thy Fri Oct 10 06:45:50 2008 +0200
37.2 +++ b/src/HOL/Library/Product_ord.thy Fri Oct 10 06:45:53 2008 +0200
37.3 @@ -13,16 +13,16 @@
37.4 begin
37.5
37.6 definition
37.7 - prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
37.8 + prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
37.9
37.10 definition
37.11 - prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
37.12 + prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
37.13
37.14 instance ..
37.15
37.16 end
37.17
37.18 -lemma [code func]:
37.19 +lemma [code]:
37.20 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
37.21 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
37.22 unfolding prod_le_def prod_less_def by simp_all
38.1 --- a/src/HOL/Library/RType.thy Fri Oct 10 06:45:50 2008 +0200
38.2 +++ b/src/HOL/Library/RType.thy Fri Oct 10 06:45:53 2008 +0200
38.3 @@ -89,7 +89,7 @@
38.4 #> TypedefPackage.interpretation Typerep.perhaps_add_def
38.5 *}
38.6
38.7 -lemma [code func]:
38.8 +lemma [code]:
38.9 "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
38.10 \<and> list_all2 eq_class.eq tys1 tys2"
38.11 by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
39.1 --- a/src/HOL/Library/Ref.thy Fri Oct 10 06:45:50 2008 +0200
39.2 +++ b/src/HOL/Library/Ref.thy Fri Oct 10 06:45:53 2008 +0200
39.3 @@ -51,7 +51,7 @@
39.4 by (cases f)
39.5 (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
39.6
39.7 -lemma update_change [code func]:
39.8 +lemma update_change [code]:
39.9 "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
39.10 by (auto simp add: monad_simp change_def lookup_chain)
39.11
40.1 --- a/src/HOL/Library/Sublist_Order.thy Fri Oct 10 06:45:50 2008 +0200
40.2 +++ b/src/HOL/Library/Sublist_Order.thy Fri Oct 10 06:45:53 2008 +0200
40.3 @@ -47,7 +47,7 @@
40.4 using assms by (induct rule: less_eq_list.induct) blast+
40.5
40.6 definition
40.7 - [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
40.8 + [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
40.9
40.10 lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
40.11 by (induct rule: ileq_induct) auto
41.1 --- a/src/HOL/Library/Univ_Poly.thy Fri Oct 10 06:45:50 2008 +0200
41.2 +++ b/src/HOL/Library/Univ_Poly.thy Fri Oct 10 06:45:53 2008 +0200
41.3 @@ -72,7 +72,7 @@
41.4
41.5 definition (in semiring_0)
41.6 divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where
41.7 - [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
41.8 + [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
41.9
41.10 --{*order of a polynomial*}
41.11 definition (in ring_1) order :: "'a => 'a list => nat" where
42.1 --- a/src/HOL/Library/Word.thy Fri Oct 10 06:45:50 2008 +0200
42.2 +++ b/src/HOL/Library/Word.thy Fri Oct 10 06:45:53 2008 +0200
42.3 @@ -2042,7 +2042,7 @@
42.4
42.5 definition
42.6 length_nat :: "nat => nat" where
42.7 - [code func del]: "length_nat x = (LEAST n. x < 2 ^ n)"
42.8 + [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
42.9
42.10 lemma length_nat: "length (nat_to_bv n) = length_nat n"
42.11 apply (simp add: length_nat_def)
42.12 @@ -2267,7 +2267,7 @@
42.13 fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
42.14 fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
42.15
42.16 -declare fast_bv_to_nat_helper.simps [code func del]
42.17 +declare fast_bv_to_nat_helper.simps [code del]
42.18
42.19 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
42.20 fast_bv_to_nat_helper bs (Int.Bit0 bin)"
43.1 --- a/src/HOL/List.thy Fri Oct 10 06:45:50 2008 +0200
43.2 +++ b/src/HOL/List.thy Fri Oct 10 06:45:53 2008 +0200
43.3 @@ -204,7 +204,7 @@
43.4
43.5 definition
43.6 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
43.7 - [code func del]: "list_all2 P xs ys =
43.8 + [code del]: "list_all2 P xs ys =
43.9 (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
43.10
43.11 definition
43.12 @@ -2872,7 +2872,7 @@
43.13
43.14 definition
43.15 sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
43.16 - [code func del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
43.17 + [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
43.18
43.19 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
43.20 set(sorted_list_of_set A) = A &
43.21 @@ -3057,7 +3057,7 @@
43.22 constdefs
43.23 set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
43.24 "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
43.25 -declare set_Cons_def [code func del]
43.26 +declare set_Cons_def [code del]
43.27
43.28 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
43.29 by (auto simp add: set_Cons_def)
43.30 @@ -3095,7 +3095,7 @@
43.31 "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
43.32 --{*Compares lists by their length and then lexicographically*}
43.33
43.34 -declare lex_def [code func del]
43.35 +declare lex_def [code del]
43.36
43.37
43.38 lemma wf_lexn: "wf r ==> wf (lexn r n)"
43.39 @@ -3171,7 +3171,7 @@
43.40 lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
43.41 "lexord r == {(x,y). \<exists> a v. y = x @ a # v \<or>
43.42 (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
43.43 -declare lexord_def [code func del]
43.44 +declare lexord_def [code del]
43.45
43.46 lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
43.47 by (unfold lexord_def, induct_tac y, auto)
43.48 @@ -3379,7 +3379,7 @@
43.49 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
43.50 "nibble_pair_of_char (Char n m) = (n, m)"
43.51
43.52 -declare nibble_pair_of_char.simps [code func del]
43.53 +declare nibble_pair_of_char.simps [code del]
43.54
43.55 setup {*
43.56 let
43.57 @@ -3393,11 +3393,11 @@
43.58 end
43.59 *}
43.60
43.61 -lemma char_case_nibble_pair [code func, code inline]:
43.62 +lemma char_case_nibble_pair [code, code inline]:
43.63 "char_case f = split f o nibble_pair_of_char"
43.64 by (simp add: expand_fun_eq split: char.split)
43.65
43.66 -lemma char_rec_nibble_pair [code func, code inline]:
43.67 +lemma char_rec_nibble_pair [code, code inline]:
43.68 "char_rec f = split f o nibble_pair_of_char"
43.69 unfolding char_case_nibble_pair [symmetric]
43.70 by (simp add: expand_fun_eq split: char.split)
44.1 --- a/src/HOL/Map.thy Fri Oct 10 06:45:50 2008 +0200
44.2 +++ b/src/HOL/Map.thy Fri Oct 10 06:45:53 2008 +0200
44.3 @@ -91,7 +91,7 @@
44.4 by simp_all
44.5
44.6 defs
44.7 - map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
44.8 + map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
44.9
44.10
44.11 subsection {* @{term [source] empty} *}
45.1 --- a/src/HOL/Matrix/Matrix.thy Fri Oct 10 06:45:50 2008 +0200
45.2 +++ b/src/HOL/Matrix/Matrix.thy Fri Oct 10 06:45:53 2008 +0200
45.3 @@ -768,7 +768,7 @@
45.4 instantiation matrix :: (zero) zero
45.5 begin
45.6
45.7 -definition zero_matrix_def [code func del]: "0 = Abs_matrix (\<lambda>j i. 0)"
45.8 +definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
45.9
45.10 instance ..
45.11
45.12 @@ -1440,9 +1440,9 @@
45.13 instantiation matrix :: ("{lattice, zero}") lattice
45.14 begin
45.15
45.16 -definition [code func del]: "inf = combine_matrix inf"
45.17 +definition [code del]: "inf = combine_matrix inf"
45.18
45.19 -definition [code func del]: "sup = combine_matrix sup"
45.20 +definition [code del]: "sup = combine_matrix sup"
45.21
45.22 instance
45.23 by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
45.24 @@ -1453,7 +1453,7 @@
45.25 begin
45.26
45.27 definition
45.28 - plus_matrix_def [code func del]: "A + B = combine_matrix (op +) A B"
45.29 + plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
45.30
45.31 instance ..
45.32
45.33 @@ -1463,7 +1463,7 @@
45.34 begin
45.35
45.36 definition
45.37 - minus_matrix_def [code func del]: "- A = apply_matrix uminus A"
45.38 + minus_matrix_def [code del]: "- A = apply_matrix uminus A"
45.39
45.40 instance ..
45.41
45.42 @@ -1473,7 +1473,7 @@
45.43 begin
45.44
45.45 definition
45.46 - diff_matrix_def [code func del]: "A - B = combine_matrix (op -) A B"
45.47 + diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
45.48
45.49 instance ..
45.50
45.51 @@ -1483,7 +1483,7 @@
45.52 begin
45.53
45.54 definition
45.55 - times_matrix_def [code func del]: "A * B = mult_matrix (op *) (op +) A B"
45.56 + times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
45.57
45.58 instance ..
45.59
45.60 @@ -1493,7 +1493,7 @@
45.61 begin
45.62
45.63 definition
45.64 - abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
45.65 + abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
45.66
45.67 instance ..
45.68
46.1 --- a/src/HOL/Matrix/SparseMatrix.thy Fri Oct 10 06:45:50 2008 +0200
46.2 +++ b/src/HOL/Matrix/SparseMatrix.thy Fri Oct 10 06:45:53 2008 +0200
46.3 @@ -25,7 +25,7 @@
46.4 lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
46.5 by (simp add: sparse_row_matrix_def)
46.6
46.7 -lemmas [code func] = sparse_row_vector_empty [symmetric]
46.8 +lemmas [code] = sparse_row_vector_empty [symmetric]
46.9
46.10 lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
46.11 by (induct l, auto)
46.12 @@ -417,8 +417,8 @@
46.13 apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
46.14 done
46.15
46.16 -lemmas [code func] = sparse_row_add_spmat [symmetric]
46.17 -lemmas [code func] = sparse_row_vector_add [symmetric]
46.18 +lemmas [code] = sparse_row_add_spmat [symmetric]
46.19 +lemmas [code] = sparse_row_vector_add [symmetric]
46.20
46.21 lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
46.22 proof -
47.1 --- a/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 10 06:45:50 2008 +0200
47.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 10 06:45:53 2008 +0200
47.3 @@ -68,7 +68,7 @@
47.4 definition
47.5 "wf_class G = wfP ((subcls1 G)^--1)"
47.6
47.7 -lemma class_rec_func (*[code func]*):
47.8 +lemma class_rec_func (*[code]*):
47.9 "class_rec G C t f = (if wf_class G then
47.10 (case class G C
47.11 of None \<Rightarrow> undefined
48.1 --- a/src/HOL/NSA/HDeriv.thy Fri Oct 10 06:45:50 2008 +0200
48.2 +++ b/src/HOL/NSA/HDeriv.thy Fri Oct 10 06:45:53 2008 +0200
48.3 @@ -27,7 +27,7 @@
48.4
48.5 definition
48.6 increment :: "[real=>real,real,hypreal] => hypreal" where
48.7 - [code func del]: "increment f x h = (@inc. f NSdifferentiable x &
48.8 + [code del]: "increment f x h = (@inc. f NSdifferentiable x &
48.9 inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
48.10
48.11
49.1 --- a/src/HOL/NSA/HLim.thy Fri Oct 10 06:45:50 2008 +0200
49.2 +++ b/src/HOL/NSA/HLim.thy Fri Oct 10 06:45:53 2008 +0200
49.3 @@ -16,18 +16,18 @@
49.4 definition
49.5 NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
49.6 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
49.7 - [code func del]: "f -- a --NS> L =
49.8 + [code del]: "f -- a --NS> L =
49.9 (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
49.10
49.11 definition
49.12 isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
49.13 --{*NS definition dispenses with limit notions*}
49.14 - [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
49.15 + [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
49.16 ( *f* f) y @= star_of (f a))"
49.17
49.18 definition
49.19 isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
49.20 - [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
49.21 + [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
49.22
49.23
49.24 subsection {* Limits of Functions *}
50.1 --- a/src/HOL/NSA/HLog.thy Fri Oct 10 06:45:50 2008 +0200
50.2 +++ b/src/HOL/NSA/HLog.thy Fri Oct 10 06:45:53 2008 +0200
50.3 @@ -20,11 +20,11 @@
50.4
50.5 definition
50.6 powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
50.7 - [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
50.8 + [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
50.9
50.10 definition
50.11 hlog :: "[hypreal,hypreal] => hypreal" where
50.12 - [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
50.13 + [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
50.14
50.15 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
50.16 by (simp add: powhr_def starfun2_star_n)
51.1 --- a/src/HOL/NSA/HSEQ.thy Fri Oct 10 06:45:50 2008 +0200
51.2 +++ b/src/HOL/NSA/HSEQ.thy Fri Oct 10 06:45:53 2008 +0200
51.3 @@ -16,7 +16,7 @@
51.4 NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
51.5 ("((_)/ ----NS> (_))" [60, 60] 60) where
51.6 --{*Nonstandard definition of convergence of sequence*}
51.7 - [code func del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
51.8 + [code del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
51.9
51.10 definition
51.11 nslim :: "(nat => 'a::real_normed_vector) => 'a" where
51.12 @@ -31,12 +31,12 @@
51.13 definition
51.14 NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
51.15 --{*Nonstandard definition for bounded sequence*}
51.16 - [code func del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
51.17 + [code del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
51.18
51.19 definition
51.20 NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
51.21 --{*Nonstandard definition*}
51.22 - [code func del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
51.23 + [code del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
51.24
51.25 subsection {* Limits of Sequences *}
51.26
52.1 --- a/src/HOL/NSA/HSeries.thy Fri Oct 10 06:45:50 2008 +0200
52.2 +++ b/src/HOL/NSA/HSeries.thy Fri Oct 10 06:45:53 2008 +0200
52.3 @@ -13,7 +13,7 @@
52.4
52.5 definition
52.6 sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
52.7 - [code func del]: "sumhr =
52.8 + [code del]: "sumhr =
52.9 (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
52.10
52.11 definition
52.12 @@ -22,7 +22,7 @@
52.13
52.14 definition
52.15 NSsummable :: "(nat=>real) => bool" where
52.16 - [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
52.17 + [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
52.18
52.19 definition
52.20 NSsuminf :: "(nat=>real) => real" where
53.1 --- a/src/HOL/NSA/HyperDef.thy Fri Oct 10 06:45:50 2008 +0200
53.2 +++ b/src/HOL/NSA/HyperDef.thy Fri Oct 10 06:45:53 2008 +0200
53.3 @@ -47,7 +47,7 @@
53.4 begin
53.5
53.6 definition
53.7 - star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)"
53.8 + star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
53.9
53.10 instance ..
53.11
53.12 @@ -113,7 +113,7 @@
53.13
53.14 definition
53.15 of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
53.16 - [transfer_unfold, code func del]: "of_hypreal = *f* of_real"
53.17 + [transfer_unfold, code del]: "of_hypreal = *f* of_real"
53.18
53.19 lemma Standard_of_hypreal [simp]:
53.20 "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
53.21 @@ -428,7 +428,7 @@
53.22 subsection{*Powers with Hypernatural Exponents*}
53.23
53.24 definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
53.25 - hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N"
53.26 + hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
53.27 (* hypernatural powers of hyperreals *)
53.28
53.29 lemma Standard_hyperpow [simp]:
54.1 --- a/src/HOL/NSA/HyperNat.thy Fri Oct 10 06:45:50 2008 +0200
54.2 +++ b/src/HOL/NSA/HyperNat.thy Fri Oct 10 06:45:53 2008 +0200
54.3 @@ -19,7 +19,7 @@
54.4
54.5 definition
54.6 hSuc :: "hypnat => hypnat" where
54.7 - hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
54.8 + hSuc_def [transfer_unfold, code del]: "hSuc = *f* Suc"
54.9
54.10 subsection{*Properties Transferred from Naturals*}
54.11
54.12 @@ -367,7 +367,7 @@
54.13
54.14 definition
54.15 of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
54.16 - of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
54.17 + of_hypnat_def [transfer_unfold, code del]: "of_hypnat = *f* of_nat"
54.18
54.19 lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
54.20 by transfer (rule of_nat_0)
55.1 --- a/src/HOL/NSA/NSA.thy Fri Oct 10 06:45:50 2008 +0200
55.2 +++ b/src/HOL/NSA/NSA.thy Fri Oct 10 06:45:53 2008 +0200
55.3 @@ -17,15 +17,15 @@
55.4
55.5 definition
55.6 Infinitesimal :: "('a::real_normed_vector) star set" where
55.7 - [code func del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
55.8 + [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
55.9
55.10 definition
55.11 HFinite :: "('a::real_normed_vector) star set" where
55.12 - [code func del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
55.13 + [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
55.14
55.15 definition
55.16 HInfinite :: "('a::real_normed_vector) star set" where
55.17 - [code func del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
55.18 + [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
55.19
55.20 definition
55.21 approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
55.22 @@ -58,7 +58,7 @@
55.23
55.24 definition
55.25 scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
55.26 - [transfer_unfold, code func del]: "scaleHR = starfun2 scaleR"
55.27 + [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
55.28
55.29 lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
55.30 by (simp add: hnorm_def)
56.1 --- a/src/HOL/NSA/NSCA.thy Fri Oct 10 06:45:50 2008 +0200
56.2 +++ b/src/HOL/NSA/NSCA.thy Fri Oct 10 06:45:53 2008 +0200
56.3 @@ -16,7 +16,7 @@
56.4
56.5 definition --{* standard part map*}
56.6 stc :: "hcomplex => hcomplex" where
56.7 - [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
56.8 + [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
56.9
56.10
56.11 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
57.1 --- a/src/HOL/NSA/NSComplex.thy Fri Oct 10 06:45:50 2008 +0200
57.2 +++ b/src/HOL/NSA/NSComplex.thy Fri Oct 10 06:45:53 2008 +0200
57.3 @@ -26,11 +26,11 @@
57.4
57.5 definition
57.6 hRe :: "hcomplex => hypreal" where
57.7 - [code func del]: "hRe = *f* Re"
57.8 + [code del]: "hRe = *f* Re"
57.9
57.10 definition
57.11 hIm :: "hcomplex => hypreal" where
57.12 - [code func del]: "hIm = *f* Im"
57.13 + [code del]: "hIm = *f* Im"
57.14
57.15
57.16 (*------ imaginary unit ----------*)
57.17 @@ -43,22 +43,22 @@
57.18
57.19 definition
57.20 hcnj :: "hcomplex => hcomplex" where
57.21 - [code func del]: "hcnj = *f* cnj"
57.22 + [code del]: "hcnj = *f* cnj"
57.23
57.24 (*------------ Argand -------------*)
57.25
57.26 definition
57.27 hsgn :: "hcomplex => hcomplex" where
57.28 - [code func del]: "hsgn = *f* sgn"
57.29 + [code del]: "hsgn = *f* sgn"
57.30
57.31 definition
57.32 harg :: "hcomplex => hypreal" where
57.33 - [code func del]: "harg = *f* arg"
57.34 + [code del]: "harg = *f* arg"
57.35
57.36 definition
57.37 (* abbreviation for (cos a + i sin a) *)
57.38 hcis :: "hypreal => hcomplex" where
57.39 - [code func del]:"hcis = *f* cis"
57.40 + [code del]:"hcis = *f* cis"
57.41
57.42 (*----- injection from hyperreals -----*)
57.43
57.44 @@ -69,16 +69,16 @@
57.45 definition
57.46 (* abbreviation for r*(cos a + i sin a) *)
57.47 hrcis :: "[hypreal, hypreal] => hcomplex" where
57.48 - [code func del]: "hrcis = *f2* rcis"
57.49 + [code del]: "hrcis = *f2* rcis"
57.50
57.51 (*------------ e ^ (x + iy) ------------*)
57.52 definition
57.53 hexpi :: "hcomplex => hcomplex" where
57.54 - [code func del]: "hexpi = *f* expi"
57.55 + [code del]: "hexpi = *f* expi"
57.56
57.57 definition
57.58 HComplex :: "[hypreal,hypreal] => hcomplex" where
57.59 - [code func del]: "HComplex = *f2* Complex"
57.60 + [code del]: "HComplex = *f2* Complex"
57.61
57.62 lemmas hcomplex_defs [transfer_unfold] =
57.63 hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
58.1 --- a/src/HOL/NSA/Star.thy Fri Oct 10 06:45:50 2008 +0200
58.2 +++ b/src/HOL/NSA/Star.thy Fri Oct 10 06:45:53 2008 +0200
58.3 @@ -17,12 +17,12 @@
58.4
58.5 definition
58.6 InternalSets :: "'a star set set" where
58.7 - [code func del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
58.8 + [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
58.9
58.10 definition
58.11 (* nonstandard extension of function *)
58.12 is_starext :: "['a star => 'a star, 'a => 'a] => bool" where
58.13 - [code func del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
58.14 + [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
58.15 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
58.16
58.17 definition
58.18 @@ -32,7 +32,7 @@
58.19
58.20 definition
58.21 InternalFuns :: "('a star => 'b star) set" where
58.22 - [code func del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
58.23 + [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
58.24
58.25
58.26 (*--------------------------------------------------------
59.1 --- a/src/HOL/NSA/StarDef.thy Fri Oct 10 06:45:50 2008 +0200
59.2 +++ b/src/HOL/NSA/StarDef.thy Fri Oct 10 06:45:53 2008 +0200
59.3 @@ -291,7 +291,7 @@
59.4 subsection {* Internal predicates *}
59.5
59.6 definition unstar :: "bool star \<Rightarrow> bool" where
59.7 - [code func del]: "unstar b \<longleftrightarrow> b = star_of True"
59.8 + [code del]: "unstar b \<longleftrightarrow> b = star_of True"
59.9
59.10 lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
59.11 by (simp add: unstar_def star_of_def star_n_eq_iff)
59.12 @@ -432,7 +432,7 @@
59.13 begin
59.14
59.15 definition
59.16 - star_zero_def [code func del]: "0 \<equiv> star_of 0"
59.17 + star_zero_def [code del]: "0 \<equiv> star_of 0"
59.18
59.19 instance ..
59.20
59.21 @@ -442,7 +442,7 @@
59.22 begin
59.23
59.24 definition
59.25 - star_one_def [code func del]: "1 \<equiv> star_of 1"
59.26 + star_one_def [code del]: "1 \<equiv> star_of 1"
59.27
59.28 instance ..
59.29
59.30 @@ -452,7 +452,7 @@
59.31 begin
59.32
59.33 definition
59.34 - star_add_def [code func del]: "(op +) \<equiv> *f2* (op +)"
59.35 + star_add_def [code del]: "(op +) \<equiv> *f2* (op +)"
59.36
59.37 instance ..
59.38
59.39 @@ -462,7 +462,7 @@
59.40 begin
59.41
59.42 definition
59.43 - star_mult_def [code func del]: "(op *) \<equiv> *f2* (op *)"
59.44 + star_mult_def [code del]: "(op *) \<equiv> *f2* (op *)"
59.45
59.46 instance ..
59.47
59.48 @@ -472,7 +472,7 @@
59.49 begin
59.50
59.51 definition
59.52 - star_minus_def [code func del]: "uminus \<equiv> *f* uminus"
59.53 + star_minus_def [code del]: "uminus \<equiv> *f* uminus"
59.54
59.55 instance ..
59.56
59.57 @@ -482,7 +482,7 @@
59.58 begin
59.59
59.60 definition
59.61 - star_diff_def [code func del]: "(op -) \<equiv> *f2* (op -)"
59.62 + star_diff_def [code del]: "(op -) \<equiv> *f2* (op -)"
59.63
59.64 instance ..
59.65
60.1 --- a/src/HOL/Nat.thy Fri Oct 10 06:45:50 2008 +0200
60.2 +++ b/src/HOL/Nat.thy Fri Oct 10 06:45:53 2008 +0200
60.3 @@ -55,7 +55,7 @@
60.4 instantiation nat :: zero
60.5 begin
60.6
60.7 -definition Zero_nat_def [code func del]:
60.8 +definition Zero_nat_def [code del]:
60.9 "0 = Abs_Nat Zero_Rep"
60.10
60.11 instance ..
60.12 @@ -1281,7 +1281,7 @@
60.13
60.14 definition
60.15 Nats :: "'a set" where
60.16 - [code func del]: "Nats = range of_nat"
60.17 + [code del]: "Nats = range of_nat"
60.18
60.19 notation (xsymbols)
60.20 Nats ("\<nat>")
61.1 --- a/src/HOL/NatBin.thy Fri Oct 10 06:45:50 2008 +0200
61.2 +++ b/src/HOL/NatBin.thy Fri Oct 10 06:45:53 2008 +0200
61.3 @@ -18,7 +18,7 @@
61.4 begin
61.5
61.6 definition
61.7 - nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)"
61.8 + nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
61.9
61.10 instance ..
61.11
62.1 --- a/src/HOL/Orderings.thy Fri Oct 10 06:45:50 2008 +0200
62.2 +++ b/src/HOL/Orderings.thy Fri Oct 10 06:45:53 2008 +0200
62.3 @@ -968,10 +968,10 @@
62.4 begin
62.5
62.6 definition
62.7 - le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
62.8 + le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
62.9
62.10 definition
62.11 - less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
62.12 + less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
62.13
62.14 instance
62.15 by intro_classes (auto simp add: le_bool_def less_bool_def)
62.16 @@ -990,7 +990,7 @@
62.17 lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
62.18 by (simp add: le_bool_def)
62.19
62.20 -lemma [code func]:
62.21 +lemma [code]:
62.22 "False \<le> b \<longleftrightarrow> True"
62.23 "True \<le> b \<longleftrightarrow> b"
62.24 "False < b \<longleftrightarrow> b"
62.25 @@ -1004,10 +1004,10 @@
62.26 begin
62.27
62.28 definition
62.29 - le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
62.30 + le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
62.31
62.32 definition
62.33 - less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
62.34 + less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
62.35
62.36 instance ..
62.37
63.1 --- a/src/HOL/Product_Type.thy Fri Oct 10 06:45:50 2008 +0200
63.2 +++ b/src/HOL/Product_Type.thy Fri Oct 10 06:45:53 2008 +0200
63.3 @@ -23,10 +23,10 @@
63.4 -- "prefer plain propositional version"
63.5
63.6 lemma
63.7 - shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
63.8 - and [code func]: "eq_class.eq True P \<longleftrightarrow> P"
63.9 - and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
63.10 - and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
63.11 + shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
63.12 + and [code]: "eq_class.eq True P \<longleftrightarrow> P"
63.13 + and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
63.14 + and [code]: "eq_class.eq P True \<longleftrightarrow> P"
63.15 and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
63.16 by (simp_all add: eq)
63.17
63.18 @@ -89,7 +89,7 @@
63.19
63.20 instance unit :: eq ..
63.21
63.22 -lemma [code func]:
63.23 +lemma [code]:
63.24 "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
63.25
63.26 code_type unit
63.27 @@ -359,10 +359,10 @@
63.28
63.29 subsubsection {* @{text split} and @{text curry} *}
63.30
63.31 -lemma split_conv [simp, code func]: "split f (a, b) = f a b"
63.32 +lemma split_conv [simp, code]: "split f (a, b) = f a b"
63.33 by (simp add: split_def)
63.34
63.35 -lemma curry_conv [simp, code func]: "curry f a b = f (a, b)"
63.36 +lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
63.37 by (simp add: curry_def)
63.38
63.39 lemmas split = split_conv -- {* for backwards compatibility *}
63.40 @@ -728,9 +728,9 @@
63.41 *}
63.42
63.43 definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
63.44 - [code func del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
63.45 + [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
63.46
63.47 -lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
63.48 +lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
63.49 by (simp add: prod_fun_def)
63.50
63.51 lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
63.52 @@ -758,12 +758,12 @@
63.53 definition
63.54 apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
63.55 where
63.56 - [code func del]: "apfst f = prod_fun f id"
63.57 + [code del]: "apfst f = prod_fun f id"
63.58
63.59 definition
63.60 apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
63.61 where
63.62 - [code func del]: "apsnd f = prod_fun id f"
63.63 + [code del]: "apsnd f = prod_fun id f"
63.64
63.65 lemma apfst_conv [simp, code]:
63.66 "apfst f (x, y) = (f x, y)"
63.67 @@ -917,7 +917,7 @@
63.68
63.69 instance * :: (eq, eq) eq ..
63.70
63.71 -lemma [code func]:
63.72 +lemma [code]:
63.73 "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
63.74
63.75 lemma split_case_cert:
64.1 --- a/src/HOL/Real/ContNotDenum.thy Fri Oct 10 06:45:50 2008 +0200
64.2 +++ b/src/HOL/Real/ContNotDenum.thy Fri Oct 10 06:45:53 2008 +0200
64.3 @@ -403,7 +403,7 @@
64.4 (f (Suc n)) \<notin> e)
64.5 )"
64.6
64.7 -declare newInt.simps [code func del]
64.8 +declare newInt.simps [code del]
64.9
64.10 subsubsection {* Properties *}
64.11
65.1 --- a/src/HOL/Real/PReal.thy Fri Oct 10 06:45:50 2008 +0200
65.2 +++ b/src/HOL/Real/PReal.thy Fri Oct 10 06:45:53 2008 +0200
65.3 @@ -19,7 +19,7 @@
65.4
65.5 definition
65.6 cut :: "rat set => bool" where
65.7 - [code func del]: "cut A = ({} \<subset> A &
65.8 + [code del]: "cut A = ({} \<subset> A &
65.9 A < {r. 0 < r} &
65.10 (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
65.11
65.12 @@ -56,7 +56,7 @@
65.13
65.14 definition
65.15 diff_set :: "[rat set,rat set] => rat set" where
65.16 - [code func del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
65.17 + [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
65.18
65.19 definition
65.20 mult_set :: "[rat set,rat set] => rat set" where
65.21 @@ -64,17 +64,17 @@
65.22
65.23 definition
65.24 inverse_set :: "rat set => rat set" where
65.25 - [code func del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
65.26 + [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
65.27
65.28 instantiation preal :: "{ord, plus, minus, times, inverse, one}"
65.29 begin
65.30
65.31 definition
65.32 - preal_less_def [code func del]:
65.33 + preal_less_def [code del]:
65.34 "R < S == Rep_preal R < Rep_preal S"
65.35
65.36 definition
65.37 - preal_le_def [code func del]:
65.38 + preal_le_def [code del]:
65.39 "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
65.40
65.41 definition
66.1 --- a/src/HOL/Real/RComplete.thy Fri Oct 10 06:45:50 2008 +0200
66.2 +++ b/src/HOL/Real/RComplete.thy Fri Oct 10 06:45:53 2008 +0200
66.3 @@ -488,7 +488,7 @@
66.4
66.5 definition
66.6 floor :: "real => int" where
66.7 - [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
66.8 + [code del]: "floor r = (LEAST n::int. r < real (n+1))"
66.9
66.10 definition
66.11 ceiling :: "real => int" where
67.1 --- a/src/HOL/Real/Rational.thy Fri Oct 10 06:45:50 2008 +0200
67.2 +++ b/src/HOL/Real/Rational.thy Fri Oct 10 06:45:53 2008 +0200
67.3 @@ -71,7 +71,7 @@
67.4
67.5 definition
67.6 Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
67.7 - [code func del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
67.8 + [code del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
67.9
67.10 code_datatype Fract
67.11
67.12 @@ -101,7 +101,7 @@
67.13 One_rat_def [code, code unfold]: "1 = Fract 1 1"
67.14
67.15 definition
67.16 - add_rat_def [code func del]:
67.17 + add_rat_def [code del]:
67.18 "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
67.19 ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
67.20
67.21 @@ -116,7 +116,7 @@
67.22 qed
67.23
67.24 definition
67.25 - minus_rat_def [code func del]:
67.26 + minus_rat_def [code del]:
67.27 "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})"
67.28
67.29 lemma minus_rat [simp, code]: "- Fract a b = Fract (- a) b"
67.30 @@ -130,7 +130,7 @@
67.31 by (cases "b = 0") (simp_all add: eq_rat)
67.32
67.33 definition
67.34 - diff_rat_def [code func del]: "q - r = q + - (r::rat)"
67.35 + diff_rat_def [code del]: "q - r = q + - (r::rat)"
67.36
67.37 lemma diff_rat [simp]:
67.38 assumes "b \<noteq> 0" and "d \<noteq> 0"
67.39 @@ -138,7 +138,7 @@
67.40 using assms by (simp add: diff_rat_def)
67.41
67.42 definition
67.43 - mult_rat_def [code func del]:
67.44 + mult_rat_def [code del]:
67.45 "q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
67.46 ratrel``{(fst x * fst y, snd x * snd y)})"
67.47
67.48 @@ -219,7 +219,7 @@
67.49 begin
67.50
67.51 definition
67.52 - rat_number_of_def [code func del]: "number_of w = Fract w 1"
67.53 + rat_number_of_def [code del]: "number_of w = Fract w 1"
67.54
67.55 instance by intro_classes (simp add: rat_number_of_def of_int_rat)
67.56
67.57 @@ -265,7 +265,7 @@
67.58 begin
67.59
67.60 definition
67.61 - inverse_rat_def [code func del]:
67.62 + inverse_rat_def [code del]:
67.63 "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.
67.64 ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
67.65
67.66 @@ -277,7 +277,7 @@
67.67 qed
67.68
67.69 definition
67.70 - divide_rat_def [code func del]: "q / r = q * inverse (r::rat)"
67.71 + divide_rat_def [code del]: "q / r = q * inverse (r::rat)"
67.72
67.73 lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
67.74 by (simp add: divide_rat_def)
67.75 @@ -320,7 +320,7 @@
67.76 begin
67.77
67.78 definition
67.79 - le_rat_def [code func del]:
67.80 + le_rat_def [code del]:
67.81 "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
67.82 {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
67.83
67.84 @@ -370,7 +370,7 @@
67.85 qed
67.86
67.87 definition
67.88 - less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
67.89 + less_rat_def [code del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
67.90
67.91 lemma less_rat [simp]:
67.92 assumes "b \<noteq> 0" and "d \<noteq> 0"
67.93 @@ -450,13 +450,13 @@
67.94 begin
67.95
67.96 definition
67.97 - abs_rat_def [code func del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
67.98 + abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
67.99
67.100 lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
67.101 by (auto simp add: abs_rat_def zabs_def Zero_rat_def less_rat not_less le_less minus_rat eq_rat zero_compare_simps)
67.102
67.103 definition
67.104 - sgn_rat_def [code func del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
67.105 + sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
67.106
67.107 lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)"
67.108 unfolding Fract_of_int_eq
67.109 @@ -553,7 +553,7 @@
67.110 begin
67.111
67.112 definition of_rat :: "rat \<Rightarrow> 'a" where
67.113 - [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
67.114 + [code del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
67.115
67.116 end
67.117
67.118 @@ -680,7 +680,7 @@
67.119
67.120 definition
67.121 Rats :: "'a set" where
67.122 - [code func del]: "Rats = range of_rat"
67.123 + [code del]: "Rats = range of_rat"
67.124
67.125 notation (xsymbols)
67.126 Rats ("\<rat>")
67.127 @@ -850,9 +850,9 @@
67.128 qed
67.129
67.130 definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
67.131 - [simp, code func del]: "Fract_norm a b = Fract a b"
67.132 + [simp, code del]: "Fract_norm a b = Fract a b"
67.133
67.134 -lemma [code func]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
67.135 +lemma [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
67.136 if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
67.137 by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
67.138
67.139 @@ -863,7 +863,7 @@
67.140 instantiation rat :: eq
67.141 begin
67.142
67.143 -definition [code func del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
67.144 +definition [code del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
67.145
67.146 instance by default (simp add: eq_rat_def)
67.147
68.1 --- a/src/HOL/Real/RealDef.thy Fri Oct 10 06:45:50 2008 +0200
68.2 +++ b/src/HOL/Real/RealDef.thy Fri Oct 10 06:45:53 2008 +0200
68.3 @@ -15,7 +15,7 @@
68.4
68.5 definition
68.6 realrel :: "((preal * preal) * (preal * preal)) set" where
68.7 - [code func del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
68.8 + [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
68.9
68.10 typedef (Real) real = "UNIV//realrel"
68.11 by (auto simp add: quotient_def)
68.12 @@ -23,46 +23,46 @@
68.13 definition
68.14 (** these don't use the overloaded "real" function: users don't see them **)
68.15 real_of_preal :: "preal => real" where
68.16 - [code func del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
68.17 + [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
68.18
68.19 instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
68.20 begin
68.21
68.22 definition
68.23 - real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
68.24 + real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
68.25
68.26 definition
68.27 - real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
68.28 + real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
68.29
68.30 definition
68.31 - real_add_def [code func del]: "z + w =
68.32 + real_add_def [code del]: "z + w =
68.33 contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
68.34 { Abs_Real(realrel``{(x+u, y+v)}) })"
68.35
68.36 definition
68.37 - real_minus_def [code func del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
68.38 + real_minus_def [code del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
68.39
68.40 definition
68.41 - real_diff_def [code func del]: "r - (s::real) = r + - s"
68.42 + real_diff_def [code del]: "r - (s::real) = r + - s"
68.43
68.44 definition
68.45 - real_mult_def [code func del]:
68.46 + real_mult_def [code del]:
68.47 "z * w =
68.48 contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
68.49 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
68.50
68.51 definition
68.52 - real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
68.53 + real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
68.54
68.55 definition
68.56 - real_divide_def [code func del]: "R / (S::real) = R * inverse S"
68.57 + real_divide_def [code del]: "R / (S::real) = R * inverse S"
68.58
68.59 definition
68.60 - real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
68.61 + real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
68.62 (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
68.63
68.64 definition
68.65 - real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
68.66 + real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
68.67
68.68 definition
68.69 real_abs_def: "abs (r::real) = (if r < 0 then - r else r)"
68.70 @@ -939,7 +939,7 @@
68.71 begin
68.72
68.73 definition
68.74 - real_number_of_def [code func del]: "number_of w = real_of_int w"
68.75 + real_number_of_def [code del]: "number_of w = real_of_int w"
68.76
68.77 instance
68.78 by intro_classes (simp add: real_number_of_def)
69.1 --- a/src/HOL/Real/RealVector.thy Fri Oct 10 06:45:50 2008 +0200
69.2 +++ b/src/HOL/Real/RealVector.thy Fri Oct 10 06:45:53 2008 +0200
69.3 @@ -308,7 +308,7 @@
69.4
69.5 definition
69.6 Reals :: "'a::real_algebra_1 set" where
69.7 - [code func del]: "Reals \<equiv> range of_real"
69.8 + [code del]: "Reals \<equiv> range of_real"
69.9
69.10 notation (xsymbols)
69.11 Reals ("\<real>")
70.1 --- a/src/HOL/Set.thy Fri Oct 10 06:45:50 2008 +0200
70.2 +++ b/src/HOL/Set.thy Fri Oct 10 06:45:53 2008 +0200
70.3 @@ -324,8 +324,8 @@
70.4 text {* Isomorphisms between predicates and sets. *}
70.5
70.6 defs
70.7 - mem_def [code func]: "x : S == S x"
70.8 - Collect_def [code func]: "Collect P == P"
70.9 + mem_def [code]: "x : S == S x"
70.10 + Collect_def [code]: "Collect P == P"
70.11
70.12 defs
70.13 Ball_def: "Ball A P == ALL x. x:A --> P(x)"
70.14 @@ -2061,7 +2061,7 @@
70.15
70.16 constdefs
70.17 vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90)
70.18 - [code func del]: "f -` B == {x. f x : B}"
70.19 + [code del]: "f -` B == {x. f x : B}"
70.20
70.21
70.22 subsubsection {* Basic rules *}
70.23 @@ -2156,7 +2156,7 @@
70.24 definition
70.25 contents :: "'a set \<Rightarrow> 'a"
70.26 where
70.27 - [code func del]: "contents X = (THE x. X = {x})"
70.28 + [code del]: "contents X = (THE x. X = {x})"
70.29
70.30 lemma contents_eq [simp]: "contents {x} = x"
70.31 by (simp add: contents_def)
70.32 @@ -2189,22 +2189,22 @@
70.33
70.34 subsection {* Rudimentary code generation *}
70.35
70.36 -lemma empty_code [code func]: "{} x \<longleftrightarrow> False"
70.37 +lemma empty_code [code]: "{} x \<longleftrightarrow> False"
70.38 unfolding empty_def Collect_def ..
70.39
70.40 -lemma UNIV_code [code func]: "UNIV x \<longleftrightarrow> True"
70.41 +lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
70.42 unfolding UNIV_def Collect_def ..
70.43
70.44 -lemma insert_code [code func]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
70.45 +lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
70.46 unfolding insert_def Collect_def mem_def Un_def by auto
70.47
70.48 -lemma inter_code [code func]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
70.49 +lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
70.50 unfolding Int_def Collect_def mem_def ..
70.51
70.52 -lemma union_code [code func]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
70.53 +lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
70.54 unfolding Un_def Collect_def mem_def ..
70.55
70.56 -lemma vimage_code [code func]: "(f -` A) x = A (f x)"
70.57 +lemma vimage_code [code]: "(f -` A) x = A (f x)"
70.58 unfolding vimage_def Collect_def mem_def ..
70.59
70.60
71.1 --- a/src/HOL/SizeChange/Graphs.thy Fri Oct 10 06:45:50 2008 +0200
71.2 +++ b/src/HOL/SizeChange/Graphs.thy Fri Oct 10 06:45:53 2008 +0200
71.3 @@ -67,7 +67,7 @@
71.4 graph_zero_def: "0 = Graph {}"
71.5
71.6 definition
71.7 - graph_plus_def [code func del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
71.8 + graph_plus_def [code del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
71.9
71.10 instance proof
71.11 fix x y z :: "('a,'b) graph"
71.12 @@ -83,22 +83,22 @@
71.13 begin
71.14
71.15 definition
71.16 - graph_leq_def [code func del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
71.17 + graph_leq_def [code del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
71.18
71.19 definition
71.20 - graph_less_def [code func del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
71.21 + graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
71.22
71.23 definition
71.24 - [code func del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
71.25 + [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
71.26
71.27 definition
71.28 - [code func del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
71.29 + [code del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
71.30
71.31 definition
71.32 - Inf_graph_def [code func del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
71.33 + Inf_graph_def [code del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
71.34
71.35 definition
71.36 - Sup_graph_def [code func del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
71.37 + Sup_graph_def [code del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
71.38
71.39 instance proof
71.40 fix x y z :: "('a,'b) graph"
71.41 @@ -165,7 +165,7 @@
71.42 begin
71.43
71.44 definition
71.45 - graph_mult_def [code func del]: "G * H = grcomp G H"
71.46 + graph_mult_def [code del]: "G * H = grcomp G H"
71.47
71.48 instance proof
71.49 fix a :: "('a, 'b) graph"
72.1 --- a/src/HOL/SizeChange/Implementation.thy Fri Oct 10 06:45:50 2008 +0200
72.2 +++ b/src/HOL/SizeChange/Implementation.thy Fri Oct 10 06:45:53 2008 +0200
72.3 @@ -122,16 +122,16 @@
72.4 code_modulename SML
72.5 Implementation Graphs
72.6
72.7 -lemma [code func]:
72.8 +lemma [code]:
72.9 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
72.10 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
72.11 unfolding graph_leq_def graph_less_def by rule+
72.12
72.13 -lemma [code func]:
72.14 +lemma [code]:
72.15 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
72.16 unfolding graph_plus_def ..
72.17
72.18 -lemma [code func]:
72.19 +lemma [code]:
72.20 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
72.21 unfolding graph_mult_def ..
72.22
73.1 --- a/src/HOL/Tools/ComputeHOL.thy Fri Oct 10 06:45:50 2008 +0200
73.2 +++ b/src/HOL/Tools/ComputeHOL.thy Fri Oct 10 06:45:53 2008 +0200
73.3 @@ -1,5 +1,5 @@
73.4 theory ComputeHOL
73.5 -imports Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
73.6 +imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
73.7 begin
73.8
73.9 lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
74.1 --- a/src/HOL/Wellfounded.thy Fri Oct 10 06:45:50 2008 +0200
74.2 +++ b/src/HOL/Wellfounded.thy Fri Oct 10 06:45:53 2008 +0200
74.3 @@ -40,7 +40,7 @@
74.4 (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
74.5
74.6 wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
74.7 - [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
74.8 + [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
74.9
74.10 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
74.11 "acyclicP r == acyclic {(x, y). r x y}"
74.12 @@ -840,10 +840,10 @@
74.13
74.14 setup Size.setup
74.15
74.16 -lemma size_bool [code func]:
74.17 +lemma size_bool [code]:
74.18 "size (b\<Colon>bool) = 0" by (cases b) auto
74.19
74.20 -lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
74.21 +lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
74.22 by (induct n) simp_all
74.23
74.24 declare "prod.size" [noatp]
75.1 --- a/src/HOL/Word/BinGeneral.thy Fri Oct 10 06:45:50 2008 +0200
75.2 +++ b/src/HOL/Word/BinGeneral.thy Fri Oct 10 06:45:53 2008 +0200
75.3 @@ -129,7 +129,7 @@
75.4 subsection {* Destructors for binary integers *}
75.5
75.6 definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
75.7 - [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
75.8 + [code del]: "bin_rl w = (THE (r, l). w = r BIT l)"
75.9
75.10 lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
75.11 apply (unfold bin_rl_def)
75.12 @@ -139,10 +139,10 @@
75.13 done
75.14
75.15 definition
75.16 - bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
75.17 + bin_rest_def [code del]: "bin_rest w = fst (bin_rl w)"
75.18
75.19 definition
75.20 - bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
75.21 + bin_last_def [code del] : "bin_last w = snd (bin_rl w)"
75.22
75.23 primrec bin_nth where
75.24 Z: "bin_nth w 0 = (bin_last w = bit.B1)"
75.25 @@ -159,7 +159,7 @@
75.26 "bin_rl (r BIT b) = (r, b)"
75.27 unfolding bin_rl_char by simp_all
75.28
75.29 -declare bin_rl_simps(1-4) [code func]
75.30 +declare bin_rl_simps(1-4) [code]
75.31
75.32 lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
75.33
75.34 @@ -212,7 +212,7 @@
75.35 "bin_rest (w BIT b) = w"
75.36 unfolding bin_rest_def by auto
75.37
75.38 -declare bin_rest_simps(1-4) [code func]
75.39 +declare bin_rest_simps(1-4) [code]
75.40
75.41 lemma bin_last_simps [simp]:
75.42 "bin_last Int.Pls = bit.B0"
75.43 @@ -222,7 +222,7 @@
75.44 "bin_last (w BIT b) = b"
75.45 unfolding bin_last_def by auto
75.46
75.47 -declare bin_last_simps(1-4) [code func]
75.48 +declare bin_last_simps(1-4) [code]
75.49
75.50 lemma bin_r_l_extras [simp]:
75.51 "bin_last 0 = bit.B0"
75.52 @@ -403,7 +403,7 @@
75.53 subsection {* Truncating binary integers *}
75.54
75.55 definition
75.56 - bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
75.57 + bin_sign_def [code del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
75.58
75.59 lemma bin_sign_simps [simp]:
75.60 "bin_sign Int.Pls = Int.Pls"
75.61 @@ -413,7 +413,7 @@
75.62 "bin_sign (w BIT b) = bin_sign w"
75.63 unfolding bin_sign_def by (auto simp: bin_rec_simps)
75.64
75.65 -declare bin_sign_simps(1-4) [code func]
75.66 +declare bin_sign_simps(1-4) [code]
75.67
75.68 lemma bin_sign_rest [simp]:
75.69 "bin_sign (bin_rest w) = (bin_sign w)"
76.1 --- a/src/HOL/Word/BinOperations.thy Fri Oct 10 06:45:50 2008 +0200
76.2 +++ b/src/HOL/Word/BinOperations.thy Fri Oct 10 06:45:53 2008 +0200
76.3 @@ -21,19 +21,19 @@
76.4 begin
76.5
76.6 definition
76.7 - int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls
76.8 + int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls
76.9 (\<lambda>w b s. s BIT (NOT b))"
76.10
76.11 definition
76.12 - int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
76.13 + int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
76.14 (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
76.15
76.16 definition
76.17 - int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
76.18 + int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
76.19 (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
76.20
76.21 definition
76.22 - int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
76.23 + int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
76.24 (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
76.25
76.26 instance ..
76.27 @@ -48,13 +48,13 @@
76.28 "NOT (w BIT b) = (NOT w) BIT (NOT b)"
76.29 unfolding int_not_def by (simp_all add: bin_rec_simps)
76.30
76.31 -declare int_not_simps(1-4) [code func]
76.32 +declare int_not_simps(1-4) [code]
76.33
76.34 -lemma int_xor_Pls [simp, code func]:
76.35 +lemma int_xor_Pls [simp, code]:
76.36 "Int.Pls XOR x = x"
76.37 unfolding int_xor_def by (simp add: bin_rec_PM)
76.38
76.39 -lemma int_xor_Min [simp, code func]:
76.40 +lemma int_xor_Min [simp, code]:
76.41 "Int.Min XOR x = NOT x"
76.42 unfolding int_xor_def by (simp add: bin_rec_PM)
76.43
76.44 @@ -69,7 +69,7 @@
76.45 apply (simp add: int_not_simps [symmetric])
76.46 done
76.47
76.48 -lemma int_xor_Bits2 [simp, code func]:
76.49 +lemma int_xor_Bits2 [simp, code]:
76.50 "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
76.51 "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
76.52 "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
76.53 @@ -85,16 +85,16 @@
76.54 apply clarsimp+
76.55 done
76.56
76.57 -lemma int_xor_extra_simps [simp, code func]:
76.58 +lemma int_xor_extra_simps [simp, code]:
76.59 "w XOR Int.Pls = w"
76.60 "w XOR Int.Min = NOT w"
76.61 using int_xor_x_simps' by simp_all
76.62
76.63 -lemma int_or_Pls [simp, code func]:
76.64 +lemma int_or_Pls [simp, code]:
76.65 "Int.Pls OR x = x"
76.66 by (unfold int_or_def) (simp add: bin_rec_PM)
76.67
76.68 -lemma int_or_Min [simp, code func]:
76.69 +lemma int_or_Min [simp, code]:
76.70 "Int.Min OR x = Int.Min"
76.71 by (unfold int_or_def) (simp add: bin_rec_PM)
76.72
76.73 @@ -102,7 +102,7 @@
76.74 "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
76.75 unfolding int_or_def by (simp add: bin_rec_simps)
76.76
76.77 -lemma int_or_Bits2 [simp, code func]:
76.78 +lemma int_or_Bits2 [simp, code]:
76.79 "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
76.80 "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
76.81 "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
76.82 @@ -118,16 +118,16 @@
76.83 apply clarsimp+
76.84 done
76.85
76.86 -lemma int_or_extra_simps [simp, code func]:
76.87 +lemma int_or_extra_simps [simp, code]:
76.88 "w OR Int.Pls = w"
76.89 "w OR Int.Min = Int.Min"
76.90 using int_or_x_simps' by simp_all
76.91
76.92 -lemma int_and_Pls [simp, code func]:
76.93 +lemma int_and_Pls [simp, code]:
76.94 "Int.Pls AND x = Int.Pls"
76.95 unfolding int_and_def by (simp add: bin_rec_PM)
76.96
76.97 -lemma int_and_Min [simp, code func]:
76.98 +lemma int_and_Min [simp, code]:
76.99 "Int.Min AND x = x"
76.100 unfolding int_and_def by (simp add: bin_rec_PM)
76.101
76.102 @@ -135,7 +135,7 @@
76.103 "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
76.104 unfolding int_and_def by (simp add: bin_rec_simps)
76.105
76.106 -lemma int_and_Bits2 [simp, code func]:
76.107 +lemma int_and_Bits2 [simp, code]:
76.108 "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
76.109 "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
76.110 "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
76.111 @@ -151,7 +151,7 @@
76.112 apply clarsimp+
76.113 done
76.114
76.115 -lemma int_and_extra_simps [simp, code func]:
76.116 +lemma int_and_extra_simps [simp, code]:
76.117 "w AND Int.Pls = Int.Pls"
76.118 "w AND Int.Min = w"
76.119 using int_and_x_simps' by simp_all
77.1 --- a/src/HOL/Word/WordDefinition.thy Fri Oct 10 06:45:50 2008 +0200
77.2 +++ b/src/HOL/Word/WordDefinition.thy Fri Oct 10 06:45:53 2008 +0200
77.3 @@ -30,7 +30,7 @@
77.4 only difference in these is the type class *}
77.5 word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
77.6 where
77.7 - [code func del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
77.8 + [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
77.9
77.10 code_datatype word_of_int
77.11
77.12 @@ -96,9 +96,9 @@
77.13
77.14 subsection "Arithmetic operations"
77.15
77.16 -declare uint_def [code func del]
77.17 +declare uint_def [code del]
77.18
77.19 -lemma [code func]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
77.20 +lemma [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
77.21 by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse)
77.22 (insert range_bintrunc, auto)
77.23
78.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy Fri Oct 10 06:45:50 2008 +0200
78.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Fri Oct 10 06:45:53 2008 +0200
78.3 @@ -9,7 +9,7 @@
78.4 imports ExecutableContent Code_Char Efficient_Nat
78.5 begin
78.6
78.7 -declare isnorm.simps [code func del]
78.8 +declare isnorm.simps [code del]
78.9
78.10 ML {* (*FIXME get rid of this*)
78.11 nonfix union;
79.1 --- a/src/HOL/ex/NormalForm.thy Fri Oct 10 06:45:50 2008 +0200
79.2 +++ b/src/HOL/ex/NormalForm.thy Fri Oct 10 06:45:53 2008 +0200
79.3 @@ -12,7 +12,7 @@
79.4 lemma "p \<longrightarrow> True" by normalization
79.5 declare disj_assoc [code nbe]
79.6 lemma "((P | Q) | R) = (P | (Q | R))" by normalization
79.7 -declare disj_assoc [code func del]
79.8 +declare disj_assoc [code del]
79.9 lemma "0 + (n::nat) = n" by normalization
79.10 lemma "0 + Suc n = Suc n" by normalization
79.11 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
80.1 --- a/src/HOL/ex/Numeral.thy Fri Oct 10 06:45:50 2008 +0200
80.2 +++ b/src/HOL/ex/Numeral.thy Fri Oct 10 06:45:53 2008 +0200
80.3 @@ -74,19 +74,19 @@
80.4 begin
80.5
80.6 definition one_num :: num where
80.7 - [code func del]: "1 = num_of_nat 1"
80.8 + [code del]: "1 = num_of_nat 1"
80.9
80.10 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
80.11 - [code func del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
80.12 + [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
80.13
80.14 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
80.15 - [code func del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
80.16 + [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
80.17
80.18 definition Dig0 :: "num \<Rightarrow> num" where
80.19 - [code func del]: "Dig0 n = n + n"
80.20 + [code del]: "Dig0 n = n + n"
80.21
80.22 definition Dig1 :: "num \<Rightarrow> num" where
80.23 - [code func del]: "Dig1 n = n + n + 1"
80.24 + [code del]: "Dig1 n = n + n + 1"
80.25
80.26 instance proof
80.27 qed (simp_all add: one_num_def plus_num_def times_num_def
80.28 @@ -503,10 +503,10 @@
80.29 begin
80.30
80.31 definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
80.32 - [code func del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
80.33 + [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
80.34
80.35 definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
80.36 - [code func del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
80.37 + [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
80.38
80.39 instance proof
80.40 qed (auto simp add: less_eq_num_def less_num_def
80.41 @@ -768,10 +768,10 @@
80.42 lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
80.43
80.44 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
80.45 - [simp, code func del]: "sub m n = (of_num m - of_num n)"
80.46 + [simp, code del]: "sub m n = (of_num m - of_num n)"
80.47
80.48 definition dup :: "int \<Rightarrow> int" where
80.49 - [code func del]: "dup k = 2 * k"
80.50 + [code del]: "dup k = 2 * k"
80.51
80.52 lemma Dig_sub [code]:
80.53 "sub 1 1 = 0"
80.54 @@ -794,7 +794,7 @@
80.55 "dup (Mns n) = Mns (Dig0 n)"
80.56 by (simp_all add: dup_def of_num.simps)
80.57
80.58 -lemma [code func, code func del]:
80.59 +lemma [code, code del]:
80.60 "(1 :: int) = 1"
80.61 "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
80.62 "(uminus :: int \<Rightarrow> int) = uminus"
81.1 --- a/src/HOL/ex/Random.thy Fri Oct 10 06:45:50 2008 +0200
81.2 +++ b/src/HOL/ex/Random.thy Fri Oct 10 06:45:53 2008 +0200
81.3 @@ -124,7 +124,7 @@
81.4 definition
81.5 select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
81.6 where
81.7 - [code func del]: "select_default k x y = (do
81.8 + [code del]: "select_default k x y = (do
81.9 l \<leftarrow> range k;
81.10 return (if l + 1 < k then x else y)
81.11 done)"
82.1 --- a/src/Pure/Isar/code.ML Fri Oct 10 06:45:50 2008 +0200
82.2 +++ b/src/Pure/Isar/code.ML Fri Oct 10 06:45:53 2008 +0200
82.3 @@ -96,12 +96,10 @@
82.4
82.5 fun add_attribute (attr as (name, _)) =
82.6 let
82.7 - fun add_parser ("", parser) attrs = attrs @ [("", parser)]
82.8 + fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
82.9 | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
82.10 - fun error "" = error ("Code attribute already declared")
82.11 - | error name = error ("Code attribute " ^ name ^ " already declared")
82.12 - in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
82.13 - then error name else add_parser attr attrs)
82.14 + in CodeAttr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
82.15 + then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
82.16 end;
82.17
82.18 val _ =
82.19 @@ -637,7 +635,7 @@
82.20 || Scan.succeed (mk_attribute add))
82.21 in
82.22 TypeInterpretation.init
82.23 - #> add_del_attribute ("func", (add_eqn, del_eqn))
82.24 + #> add_del_attribute ("", (add_eqn, del_eqn))
82.25 #> add_simple_attribute ("nbe", add_nonlinear_eqn)
82.26 #> add_del_attribute ("inline", (add_inline, del_inline))
82.27 #> add_del_attribute ("post", (add_post, del_post))