--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Fri Oct 10 06:45:53 2008 +0200
@@ -25,7 +25,7 @@
explicitly:
*}
-lemma %quoteme [code func]:
+lemma %quoteme [code]:
"dequeue (Queue xs []) =
(if xs = [] then (None, Queue [] [])
else dequeue (Queue [] (rev xs)))"
@@ -34,7 +34,7 @@
by (cases xs, simp_all) (cases "rev xs", simp_all)
text {*
- \noindent The annotation @{text "[code func]"} is an @{text Isar}
+ \noindent The annotation @{text "[code]"} is an @{text Isar}
@{text attribute} which states that the given theorems should be
considered as defining equations for a @{text fun} statement --
the corresponding constant is determined syntactically. The resulting code:
@@ -255,7 +255,7 @@
the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
*}
-lemma %quoteme plus_Dig [code func]:
+lemma %quoteme plus_Dig [code]:
"0 + n = n"
"m + 0 = m"
"1 + Dig0 n = Dig1 n"
@@ -282,12 +282,12 @@
which are an obstacle here:
*}
-lemma %quoteme Suc_Dig [code func]:
+lemma %quoteme Suc_Dig [code]:
"Suc n = n + 1"
by simp
declare %quoteme One_nat_def [code inline del]
-declare %quoteme add_Suc_shift [code func del]
+declare %quoteme add_Suc_shift [code del]
text {*
\noindent This yields the following code:
@@ -316,10 +316,10 @@
*}
code_datatype %invisible "0::nat" Suc
-declare %invisible plus_Dig [code func del]
+declare %invisible plus_Dig [code del]
declare %invisible One_nat_def [code inline]
-declare %invisible add_Suc_shift [code func]
-lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
+declare %invisible add_Suc_shift [code]
+lemma %invisible [code]: "0 + n = (n \<Colon> nat)" by simp
subsection {* Equality and wellsortedness *}
@@ -367,10 +367,10 @@
instantiation %quoteme "*" :: (order, order) order
begin
-definition %quoteme [code func del]:
+definition %quoteme [code del]:
"x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
-definition %quoteme [code func del]:
+definition %quoteme [code del]:
"x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
instance %quoteme proof
@@ -378,7 +378,7 @@
end %quoteme
-lemma %quoteme order_prod [code func]:
+lemma %quoteme order_prod [code]:
"(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
"(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
@@ -396,7 +396,7 @@
code theorems:
*}
-lemma %quoteme order_prod_code [code func]:
+lemma %quoteme order_prod_code [code]:
"(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
"(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
@@ -438,7 +438,7 @@
@{const [show_types] list_all2} can do the job:
*}
-lemma %quoteme monotype_eq_list_all2 [code func]:
+lemma %quoteme monotype_eq_list_all2 [code]:
"eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
by (simp add: eq list_all2_eq [symmetric])
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Fri Oct 10 06:45:53 2008 +0200
@@ -55,7 +55,7 @@
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
@@ -71,7 +71,7 @@
\endisadelimquoteme
%
\begin{isamarkuptext}%
-\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar}
+\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
\isa{attribute} which states that the given theorems should be
considered as defining equations for a \isa{fun} statement --
the corresponding constant is determined syntactically. The resulting code:%
@@ -287,8 +287,8 @@
\verb|};|\newline%
\newline%
\verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
+\verb|pow Zero_nat a = neutral;|\newline%
\verb|pow (Suc n) a = mult a (pow n a);|\newline%
-\verb|pow Zero_nat a = neutral;|\newline%
\newline%
\verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
\verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
@@ -298,8 +298,8 @@
\verb|neutral_nat = Suc Zero_nat;|\newline%
\newline%
\verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
+\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
\verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
-\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
\newline%
\verb|instance Semigroup Nat where {|\newline%
\verb| mult = mult_nat;|\newline%
@@ -350,16 +350,16 @@
\verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
\verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
\newline%
-\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline%
-\verb| |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline%
+\verb|fun pow A_ Zero_nat a = neutral A_|\newline%
+\verb| |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline%
\newline%
\verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
\verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
\newline%
\verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
\newline%
-\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline%
-\verb| |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline%
+\verb|fun mult_nat Zero_nat n = Zero_nat|\newline%
+\verb| |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
\newline%
\verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
\newline%
@@ -575,7 +575,7 @@
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
@@ -629,7 +629,7 @@
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
-\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
@@ -637,7 +637,7 @@
\isacommand{declare}\isamarkupfalse%
\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
\isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
\endisatagquoteme
{\isafoldquoteme}%
%
@@ -715,13 +715,13 @@
\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
\isacommand{declare}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
\isacommand{declare}\isamarkupfalse%
\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
\isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisataginvisible
{\isafoldinvisible}%
@@ -784,15 +784,15 @@
\newline%
\verb|fun eqop A_ a b = eq A_ a b;|\newline%
\newline%
-\verb|fun member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys|\newline%
-\verb| |\verb,|,\verb| member A_ x [] = false;|\newline%
+\verb|fun member A_ x [] = false|\newline%
+\verb| |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline%
\newline%
-\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
-\verb| (if member A_ z xs|\newline%
-\verb| then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
-\verb| else collect_duplicates A_ xs (z :: ys) zs)|\newline%
-\verb| else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline%
-\verb| |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline%
+\verb|fun collect_duplicates A_ xs ys [] = xs|\newline%
+\verb| |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline%
+\verb| (if member A_ z xs|\newline%
+\verb| then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
+\verb| else collect_duplicates A_ xs (z :: ys) zs)|\newline%
+\verb| else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline%
\newline%
\verb|end; (*struct Example*)|%
\end{isamarkuptext}%
@@ -835,11 +835,11 @@
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
@@ -852,7 +852,7 @@
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\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
\ \ \ \ \ 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
\ \ {\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
@@ -884,7 +884,7 @@
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\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
\ \ \ \ \ 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
\ \ {\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
@@ -1007,7 +1007,7 @@
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
-\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\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
\ \ \ \ \ 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
\ \ \isacommand{by}\isamarkupfalse%
@@ -1038,8 +1038,8 @@
\newline%
\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
\newline%
-\verb|fun null (x :: xs) = false|\newline%
-\verb| |\verb,|,\verb| null [] = true;|\newline%
+\verb|fun null [] = true|\newline%
+\verb| |\verb,|,\verb| null (x :: xs) = false;|\newline%
\newline%
\verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
\verb| |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 10 06:45:53 2008 +0200
@@ -993,7 +993,7 @@
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
- 'code' ('func' | 'inline') ( 'del' )?
+ 'code' ( 'inline' ) ? ( 'del' ) ?
;
\end{rail}
@@ -1080,13 +1080,13 @@
are not required to have a definition by means of defining equations;
if needed these are implemented by program abort instead.
- \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
- with option ``@{text "del:"}'' deselects) a defining equation for
+ \item [@{attribute (HOL) code}] explicitly selects (or
+ with option ``@{text "del"}'' deselects) a defining equation for
code generation. Usually packages introducing defining equations
provide a reasonable default setup for selection.
\item [@{attribute (HOL) code}@{text inline}] declares (or with
- option ``@{text "del:"}'' removes) inlining theorems which are
+ option ``@{text "del"}'' removes) inlining theorems which are
applied as rewrite rules to any defining equation during
preprocessing.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 10 06:45:53 2008 +0200
@@ -997,7 +997,7 @@
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
- 'code' ('func' | 'inline') ( 'del' )?
+ 'code' ( 'inline' ) ? ( 'del' ) ?
;
\end{rail}
@@ -1081,13 +1081,13 @@
are not required to have a definition by means of defining equations;
if needed these are implemented by program abort instead.
- \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
- with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
+ \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or
+ with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for
code generation. Usually packages introducing defining equations
provide a reasonable default setup for selection.
\item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
- option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
+ option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
applied as rewrite rules to any defining equation during
preprocessing.
--- a/src/HOL/Code_Eval.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Code_Eval.thy Fri Oct 10 06:45:53 2008 +0200
@@ -133,14 +133,14 @@
subsubsection {* Code generator setup *}
-lemmas [code func del] = term.recs term.cases term.size
-lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
+lemmas [code del] = term.recs term.cases term.size
+lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
-lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
-lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
-lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code func]: "Code_Eval.term_of c =
+lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
(let (n, m) = nibble_pair_of_char c
in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
(Code_Eval.term_of n)) (Code_Eval.term_of m))"
--- a/src/HOL/Code_Setup.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Code_Setup.thy Fri Oct 10 06:45:53 2008 +0200
@@ -21,32 +21,32 @@
text {* Code equations *}
-lemma [code func]:
+lemma [code]:
shows "False \<and> x \<longleftrightarrow> False"
and "True \<and> x \<longleftrightarrow> x"
and "x \<and> False \<longleftrightarrow> False"
and "x \<and> True \<longleftrightarrow> x" by simp_all
-lemma [code func]:
+lemma [code]:
shows "False \<or> x \<longleftrightarrow> x"
and "True \<or> x \<longleftrightarrow> True"
and "x \<or> False \<longleftrightarrow> x"
and "x \<or> True \<longleftrightarrow> True" by simp_all
-lemma [code func]:
+lemma [code]:
shows "\<not> True \<longleftrightarrow> False"
and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
-lemmas [code func] = Let_def if_True if_False
+lemmas [code] = Let_def if_True if_False
-lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
+lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
text {* Equality *}
context eq
begin
-lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
+lemma equals_eq [code inline, code]: "op = \<equiv> eq"
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
declare eq [code unfold, code inline del]
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Oct 10 06:45:53 2008 +0200
@@ -481,7 +481,7 @@
"numgcdh (C i) = (\<lambda>g. zgcd i g)"
"numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
"numgcdh t = (\<lambda>g. 1)"
-defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
+defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
recdef reducecoeffh "measure size"
"reducecoeffh (C i) = (\<lambda> g. C (i div g))"
--- a/src/HOL/Datatype.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Datatype.thy Fri Oct 10 06:45:53 2008 +0200
@@ -635,7 +635,7 @@
definition
option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
where
- [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
+ [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
lemma option_map_None [simp, code]: "option_map f None = None"
by (simp add: option_map_def)
--- a/src/HOL/Divides.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Divides.thy Fri Oct 10 06:45:53 2008 +0200
@@ -127,7 +127,7 @@
note that ultimately show thesis by blast
qed
-lemma dvd_eq_mod_eq_0 [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
proof
assume "b mod a = 0"
with mod_div_equality [of b a] have "b div a * a = b" by simp
@@ -230,7 +230,7 @@
begin
definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- [code func del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
+ [code del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
definition div_nat where
"m div n = fst (divmod m n)"
--- a/src/HOL/Equiv_Relations.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Equiv_Relations.thy Fri Oct 10 06:45:53 2008 +0200
@@ -94,7 +94,7 @@
subsection {* Quotients *}
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where
- [code func del]: "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
+ [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
by (unfold quotient_def) blast
--- a/src/HOL/Fun.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Fun.thy Fri Oct 10 06:45:53 2008 +0200
@@ -117,7 +117,7 @@
definition
bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
- [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
+ [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
constdefs
surj :: "('a => 'b) => bool" (*surjective*)
--- a/src/HOL/HOL.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/HOL.thy Fri Oct 10 06:45:53 2008 +0200
@@ -1227,7 +1227,7 @@
constdefs
simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1)
- [code func del]: "simp_implies \<equiv> op ==>"
+ [code del]: "simp_implies \<equiv> op ==>"
lemma simp_impliesI:
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
--- a/src/HOL/Hyperreal/Integration.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Fri Oct 10 06:45:53 2008 +0200
@@ -16,29 +16,29 @@
--{*Partitions and tagged partitions etc.*}
partition :: "[(real*real),nat => real] => bool" where
- [code func del]: "partition = (%(a,b) D. D 0 = a &
+ [code del]: "partition = (%(a,b) D. D 0 = a &
(\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
(\<forall>n \<ge> N. D(n) = b)))"
definition
psize :: "(nat => real) => nat" where
- [code func del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+ [code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
(\<forall>n \<ge> N. D(n) = D(N)))"
definition
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
- [code func del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
+ [code del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
(\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
--{*Gauges and gauge-fine divisions*}
definition
gauge :: "[real => bool, real => real] => bool" where
- [code func del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
+ [code del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
definition
fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
- [code func del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
+ [code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
--{*Riemann sum*}
@@ -50,7 +50,7 @@
definition
Integral :: "[(real*real),real=>real,real] => bool" where
- [code func del]: "Integral = (%(a,b) f k. \<forall>e > 0.
+ [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
(\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
\<bar>rsum(D,p) f - k\<bar> < e)))"
--- a/src/HOL/Hyperreal/Lim.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
definition
LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
- [code func del]: "f -- a --> L =
+ [code del]: "f -- a --> L =
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
--> norm (f x - L) < r)"
@@ -26,7 +26,7 @@
definition
isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- [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)"
+ [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
subsection {* Limits of Functions *}
--- a/src/HOL/Hyperreal/SEQ.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Fri Oct 10 06:45:53 2008 +0200
@@ -15,13 +15,13 @@
definition
Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
--{*Standard definition of sequence converging to zero*}
- [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
+ [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
definition
LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----> (_))" [60, 60] 60) where
--{*Standard definition of convergence of sequence*}
- [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
+ [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
definition
lim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -36,22 +36,22 @@
definition
Bseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Standard definition for bounded sequence*}
- [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+ [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
definition
monoseq :: "(nat=>real)=>bool" where
--{*Definition for monotonicity*}
- [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))"
+ [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))"
definition
subseq :: "(nat => nat) => bool" where
--{*Definition of subsequence*}
- [code func del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
+ [code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
definition
Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
--{*Standard definition of the Cauchy condition*}
- [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
+ [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
subsection {* Bounded Sequences *}
--- a/src/HOL/Int.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Int.thy Fri Oct 10 06:45:53 2008 +0200
@@ -24,7 +24,7 @@
definition
intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
where
- [code func del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
+ [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
typedef (Integ)
int = "UNIV//intrel"
@@ -34,34 +34,34 @@
begin
definition
- Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
+ Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
definition
- One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
+ One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
definition
- add_int_def [code func del]: "z + w = Abs_Integ
+ add_int_def [code del]: "z + w = Abs_Integ
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
intrel `` {(x + u, y + v)})"
definition
- minus_int_def [code func del]:
+ minus_int_def [code del]:
"- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
definition
- diff_int_def [code func del]: "z - w = z + (-w \<Colon> int)"
+ diff_int_def [code del]: "z - w = z + (-w \<Colon> int)"
definition
- mult_int_def [code func del]: "z * w = Abs_Integ
+ mult_int_def [code del]: "z * w = Abs_Integ
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
intrel `` {(x*u + y*v, x*v + y*u)})"
definition
- le_int_def [code func del]:
+ le_int_def [code del]:
"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)"
definition
- less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+ less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
definition
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
@@ -298,7 +298,7 @@
definition
of_int :: "int \<Rightarrow> 'a"
where
- [code func del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+ [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
proof -
@@ -390,7 +390,7 @@
definition
nat :: "int \<Rightarrow> nat"
where
- [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+ [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
@@ -585,19 +585,19 @@
definition
Pls :: int where
- [code func del]: "Pls = 0"
+ [code del]: "Pls = 0"
definition
Min :: int where
- [code func del]: "Min = - 1"
+ [code del]: "Min = - 1"
definition
Bit0 :: "int \<Rightarrow> int" where
- [code func del]: "Bit0 k = k + k"
+ [code del]: "Bit0 k = k + k"
definition
Bit1 :: "int \<Rightarrow> int" where
- [code func del]: "Bit1 k = 1 + k + k"
+ [code del]: "Bit1 k = 1 + k + k"
class number = type + -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
@@ -622,11 +622,11 @@
definition
succ :: "int \<Rightarrow> int" where
- [code func del]: "succ k = k + 1"
+ [code del]: "succ k = k + 1"
definition
pred :: "int \<Rightarrow> int" where
- [code func del]: "pred k = k - 1"
+ [code del]: "pred k = k - 1"
lemmas
max_number_of [simp] = max_def
@@ -785,7 +785,7 @@
begin
definition
- int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
+ int_number_of_def [code del]: "number_of w = (of_int w \<Colon> int)"
instance
by intro_classes (simp only: int_number_of_def)
@@ -1167,7 +1167,7 @@
definition
Ints :: "'a set"
where
- [code func del]: "Ints = range of_int"
+ [code del]: "Ints = range of_int"
end
@@ -1799,36 +1799,36 @@
code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
-lemmas pred_succ_numeral_code [code func] =
+lemmas pred_succ_numeral_code [code] =
pred_bin_simps succ_bin_simps
-lemmas plus_numeral_code [code func] =
+lemmas plus_numeral_code [code] =
add_bin_simps
arith_extra_simps(1) [where 'a = int]
-lemmas minus_numeral_code [code func] =
+lemmas minus_numeral_code [code] =
minus_bin_simps
arith_extra_simps(2) [where 'a = int]
arith_extra_simps(5) [where 'a = int]
-lemmas times_numeral_code [code func] =
+lemmas times_numeral_code [code] =
mult_bin_simps
arith_extra_simps(4) [where 'a = int]
instantiation int :: eq
begin
-definition [code func del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
instance by default (simp add: eq_int_def)
end
-lemma eq_number_of_int_code [code func]:
+lemma eq_number_of_int_code [code]:
"eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
unfolding eq_int_def number_of_is_id ..
-lemma eq_int_code [code func]:
+lemma eq_int_code [code]:
"eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
"eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
"eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
@@ -1859,11 +1859,11 @@
"eq_class.eq (k::int) k \<longleftrightarrow> True"
by (rule HOL.eq_refl)
-lemma less_eq_number_of_int_code [code func]:
+lemma less_eq_number_of_int_code [code]:
"(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
unfolding number_of_is_id ..
-lemma less_eq_int_code [code func]:
+lemma less_eq_int_code [code]:
"Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
"Int.Pls \<le> Int.Min \<longleftrightarrow> False"
"Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
@@ -1890,11 +1890,11 @@
(auto simp add: neg_def linorder_not_less group_simps
zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
-lemma less_number_of_int_code [code func]:
+lemma less_number_of_int_code [code]:
"(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
unfolding number_of_is_id ..
-lemma less_int_code [code func]:
+lemma less_int_code [code]:
"Int.Pls < Int.Pls \<longleftrightarrow> False"
"Int.Pls < Int.Min \<longleftrightarrow> False"
"Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
@@ -1935,11 +1935,11 @@
hide (open) const nat_aux
-lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
+lemma zero_is_num_zero [code, code inline, symmetric, code post]:
"(0\<Colon>int) = Numeral0"
by simp
-lemma one_is_num_one [code func, code inline, symmetric, code post]:
+lemma one_is_num_one [code, code inline, symmetric, code post]:
"(1\<Colon>int) = Numeral1"
by simp
--- a/src/HOL/IntDiv.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/IntDiv.thy Fri Oct 10 06:45:53 2008 +0200
@@ -14,13 +14,13 @@
constdefs
quorem :: "(int*int) * (int*int) => bool"
--{*definition of quotient and remainder*}
- [code func]: "quorem == %((a,b), (q,r)).
+ [code]: "quorem == %((a,b), (q,r)).
a = b*q + r &
(if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
adjust :: "[int, int*int] => int*int"
--{*for the division algorithm*}
- [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
+ [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
else (2*q, r)"
text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
@@ -46,7 +46,7 @@
text{*algorithm for the general case @{term "b\<noteq>0"}*}
constdefs
negateSnd :: "int*int => int*int"
- [code func]: "negateSnd == %(q,r). (q,-r)"
+ [code]: "negateSnd == %(q,r). (q,-r)"
definition
divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
@@ -1477,7 +1477,7 @@
context ring_1
begin
-lemma of_int_num [code func]:
+lemma of_int_num [code]:
"of_int k = (if k = 0 then 0 else if k < 0 then
- of_int (- k) else let
(l, m) = divAlg (k, 2);
--- a/src/HOL/Lattices.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Lattices.thy Fri Oct 10 06:45:53 2008 +0200
@@ -9,7 +9,7 @@
imports Fun
begin
-subsection{* Lattices *}
+subsection {* Lattices *}
notation
less_eq (infix "\<sqsubseteq>" 50) and
@@ -40,7 +40,7 @@
class lattice = lower_semilattice + upper_semilattice
-subsubsection{* Intro and elim rules*}
+subsubsection {* Intro and elim rules*}
context lower_semilattice
begin
@@ -512,10 +512,10 @@
begin
definition
- inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+ inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
definition
- sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+ sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
instance
apply intro_classes
@@ -536,10 +536,10 @@
begin
definition
- Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+ Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
definition
- Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+ Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
instance
by intro_classes
--- a/src/HOL/Library/Array.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Array.thy Fri Oct 10 06:45:53 2008 +0200
@@ -107,14 +107,14 @@
subsection {* Properties *}
-lemma array_make [code func]:
+lemma array_make [code]:
"Array.new n x = make n (\<lambda>_. x)"
by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
monad_simp array_of_list_replicate [symmetric]
map_replicate_trivial replicate_append_same
of_list_def)
-lemma array_of_list_make [code func]:
+lemma array_of_list_make [code]:
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
unfolding make_def map_nth ..
@@ -126,28 +126,28 @@
definition new' where
[code del]: "new' = Array.new o nat_of_index"
hide (open) const new'
-lemma [code func]:
+lemma [code]:
"Array.new = Array.new' o index_of_nat"
by (simp add: new'_def o_def)
definition of_list' where
[code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
hide (open) const of_list'
-lemma [code func]:
+lemma [code]:
"Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
by (simp add: of_list'_def)
definition make' where
[code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
hide (open) const make'
-lemma [code func]:
+lemma [code]:
"Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
by (simp add: make'_def o_def)
definition length' where
[code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
hide (open) const length'
-lemma [code func]:
+lemma [code]:
"Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
by (simp add: length'_def monad_simp',
simp add: liftM_def comp_def monad_simp,
@@ -156,14 +156,14 @@
definition nth' where
[code del]: "nth' a = Array.nth a o nat_of_index"
hide (open) const nth'
-lemma [code func]:
+lemma [code]:
"Array.nth a n = Array.nth' a (index_of_nat n)"
by (simp add: nth'_def)
definition upd' where
[code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
hide (open) const upd'
-lemma [code func]:
+lemma [code]:
"Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def monad_simp upd_return)
--- a/src/HOL/Library/Char_nat.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Char_nat.thy Fri Oct 10 06:45:53 2008 +0200
@@ -54,7 +54,7 @@
"nibble_of_nat (n mod 16) = nibble_of_nat n"
unfolding nibble_of_nat_def Let_def by auto
-lemmas [code func] = nibble_of_nat_norm [symmetric]
+lemmas [code] = nibble_of_nat_norm [symmetric]
lemma nibble_of_nat_simps [simp]:
"nibble_of_nat 0 = Nibble0"
@@ -75,7 +75,7 @@
"nibble_of_nat 15 = NibbleF"
unfolding nibble_of_nat_def Let_def by auto
-lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
+lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
[simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
@@ -115,7 +115,7 @@
nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
"nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
-lemma nibble_of_pair [code func]:
+lemma nibble_of_pair [code]:
"nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
--- a/src/HOL/Library/Char_ord.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Char_ord.thy Fri Oct 10 06:45:53 2008 +0200
@@ -64,11 +64,11 @@
begin
definition
- 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>
+ char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
definition
- char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+ char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
instance
@@ -90,7 +90,7 @@
end
-lemma [simp, code func]:
+lemma [simp, code]:
shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
and char_less_simp: "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
unfolding char_less_eq_def char_less_def by simp_all
--- a/src/HOL/Library/Code_Char_chr.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Fri Oct 10 06:45:53 2008 +0200
@@ -12,28 +12,28 @@
definition
"int_of_char = int o nat_of_char"
-lemma [code func]:
+lemma [code]:
"nat_of_char = nat o int_of_char"
unfolding int_of_char_def by (simp add: expand_fun_eq)
definition
"char_of_int = char_of_nat o nat"
-lemma [code func]:
+lemma [code]:
"char_of_nat = char_of_int o int"
unfolding char_of_int_def by (simp add: expand_fun_eq)
-lemmas [code func del] = char.recs char.cases char.size
+lemmas [code del] = char.recs char.cases char.size
-lemma [code func, code inline]:
+lemma [code, code inline]:
"char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
-lemma [code func, code inline]:
+lemma [code, code inline]:
"char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
-lemma [code func]:
+lemma [code]:
"size (c\<Colon>char) = 0"
by (cases c) auto
--- a/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:53 2008 +0200
@@ -64,7 +64,7 @@
instantiation index :: zero
begin
-definition [simp, code func del]:
+definition [simp, code del]:
"0 = index_of_nat 0"
instance ..
@@ -87,12 +87,12 @@
then show "P k" by simp
qed simp_all
-lemmas [code func del] = index.recs index.cases
+lemmas [code del] = index.recs index.cases
declare index_case [case_names nat, cases type: index]
declare index.induct [case_names nat, induct type: index]
-lemma [code func]:
+lemma [code]:
"index_size = nat_of_index"
proof (rule ext)
fix k
@@ -102,7 +102,7 @@
finally show "index_size k = nat_of_index k" .
qed
-lemma [code func]:
+lemma [code]:
"size = nat_of_index"
proof (rule ext)
fix k
@@ -110,7 +110,7 @@
by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
qed
-lemma [code func]:
+lemma [code]:
"eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
by (cases k, cases l) (simp add: eq)
@@ -143,63 +143,63 @@
instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
begin
-lemma zero_index_code [code inline, code func]:
+lemma zero_index_code [code inline, code]:
"(0\<Colon>index) = Numeral0"
by (simp add: number_of_index_def Pls_def)
lemma [code post]: "Numeral0 = (0\<Colon>index)"
using zero_index_code ..
-definition [simp, code func del]:
+definition [simp, code del]:
"(1\<Colon>index) = index_of_nat 1"
-lemma one_index_code [code inline, code func]:
+lemma one_index_code [code inline, code]:
"(1\<Colon>index) = Numeral1"
by (simp add: number_of_index_def Pls_def Bit1_def)
lemma [code post]: "Numeral1 = (1\<Colon>index)"
using one_index_code ..
-definition [simp, code func del]:
+definition [simp, code del]:
"n + m = index_of_nat (nat_of_index n + nat_of_index m)"
-lemma plus_index_code [code func]:
+lemma plus_index_code [code]:
"index_of_nat n + index_of_nat m = index_of_nat (n + m)"
by simp
-definition [simp, code func del]:
+definition [simp, code del]:
"n - m = index_of_nat (nat_of_index n - nat_of_index m)"
-definition [simp, code func del]:
+definition [simp, code del]:
"n * m = index_of_nat (nat_of_index n * nat_of_index m)"
-lemma times_index_code [code func]:
+lemma times_index_code [code]:
"index_of_nat n * index_of_nat m = index_of_nat (n * m)"
by simp
-definition [simp, code func del]:
+definition [simp, code del]:
"n div m = index_of_nat (nat_of_index n div nat_of_index m)"
-definition [simp, code func del]:
+definition [simp, code del]:
"n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
-lemma div_index_code [code func]:
+lemma div_index_code [code]:
"index_of_nat n div index_of_nat m = index_of_nat (n div m)"
by simp
-lemma mod_index_code [code func]:
+lemma mod_index_code [code]:
"index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
by simp
-definition [simp, code func del]:
+definition [simp, code del]:
"n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
-definition [simp, code func del]:
+definition [simp, code del]:
"n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
-lemma less_eq_index_code [code func]:
+lemma less_eq_index_code [code]:
"index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
by simp
-lemma less_index_code [code func]:
+lemma less_index_code [code]:
"index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
by simp
@@ -260,25 +260,25 @@
definition
minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
where
- [code func del]: "minus_index_aux = op -"
+ [code del]: "minus_index_aux = op -"
-lemma [code func]: "op - = minus_index_aux"
+lemma [code]: "op - = minus_index_aux"
using minus_index_aux_def ..
definition
div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index"
where
- [code func del]: "div_mod_index n m = (n div m, n mod m)"
+ [code del]: "div_mod_index n m = (n div m, n mod m)"
-lemma [code func]:
+lemma [code]:
"div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
unfolding div_mod_index_def by auto
-lemma [code func]:
+lemma [code]:
"n div m = fst (div_mod_index n m)"
unfolding div_mod_index_def by simp
-lemma [code func]:
+lemma [code]:
"n mod m = snd (div_mod_index n m)"
unfolding div_mod_index_def by simp
@@ -340,7 +340,7 @@
text {* Evaluation *}
-lemma [code func, code func del]:
+lemma [code, code del]:
"(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
--- a/src/HOL/Library/Code_Integer.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Integer.thy Fri Oct 10 06:45:53 2008 +0200
@@ -92,7 +92,7 @@
text {* Evaluation *}
-lemma [code func, code func del]:
+lemma [code, code del]:
"(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" ..
code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
--- a/src/HOL/Library/Code_Message.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Message.thy Fri Oct 10 06:45:53 2008 +0200
@@ -12,12 +12,12 @@
datatype message_string = STR string
-lemmas [code func del] = message_string.recs message_string.cases
+lemmas [code del] = message_string.recs message_string.cases
-lemma [code func]: "size (s\<Colon>message_string) = 0"
+lemma [code]: "size (s\<Colon>message_string) = 0"
by (cases s) simp_all
-lemma [code func]: "message_string_size (s\<Colon>message_string) = 0"
+lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
by (cases s) simp_all
subsection {* ML interface *}
--- a/src/HOL/Library/Efficient_Nat.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Oct 10 06:45:53 2008 +0200
@@ -232,7 +232,6 @@
of NONE => NONE
| SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
- (*FIXME*)
end
in
@@ -344,13 +343,13 @@
definition
int :: "nat \<Rightarrow> int"
where
- [code func del]: "int = of_nat"
+ [code del]: "int = of_nat"
-lemma int_code' [code func]:
+lemma int_code' [code]:
"int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
unfolding int_nat_number_of [folded int_def] ..
-lemma nat_code' [code func]:
+lemma nat_code' [code]:
"nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
by auto
@@ -434,7 +433,7 @@
text {* Evaluation *}
-lemma [code func, code func del]:
+lemma [code, code del]:
"(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
--- a/src/HOL/Library/Enum.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Enum.thy Fri Oct 10 06:45:53 2008 +0200
@@ -13,7 +13,7 @@
class enum = itself +
fixes enum :: "'a list"
- assumes UNIV_enum [code func]: "UNIV = set enum"
+ assumes UNIV_enum [code]: "UNIV = set enum"
and enum_distinct: "distinct enum"
begin
@@ -49,7 +49,7 @@
end
-lemma order_fun [code func]:
+lemma order_fun [code]:
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
@@ -58,10 +58,10 @@
subsection {* Quantifiers *}
-lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
+lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
by (simp add: list_all_iff enum_all)
-lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
by (simp add: list_all_iff enum_all)
@@ -157,7 +157,7 @@
begin
definition
- [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)"
+ [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)"
instance proof
show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
@@ -177,7 +177,7 @@
end
-lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
+lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
by (simp add: enum_fun_def Let_def)
@@ -286,9 +286,9 @@
begin
definition
- [code func del]: "enum = map (split Char) (product enum enum)"
+ [code del]: "enum = map (split Char) (product enum enum)"
-lemma enum_char [code func]:
+lemma enum_char [code]:
"enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
--- a/src/HOL/Library/GCD.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/GCD.thy Fri Oct 10 06:45:53 2008 +0200
@@ -18,7 +18,7 @@
definition
is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
- [code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+ [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
(\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
text {* Uniqueness *}
@@ -776,7 +776,7 @@
thus ?thesis by (simp add: zlcm_def)
qed
-lemma zgcd_code [code func]:
+lemma zgcd_code [code]:
"zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
--- a/src/HOL/Library/Heap_Monad.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy Fri Oct 10 06:45:53 2008 +0200
@@ -266,14 +266,14 @@
definition
Fail :: "message_string \<Rightarrow> exception"
where
- [code func del]: "Fail s = Exn"
+ [code del]: "Fail s = Exn"
definition
raise_exc :: "exception \<Rightarrow> 'a Heap"
where
- [code func del]: "raise_exc e = raise []"
+ [code del]: "raise_exc e = raise []"
-lemma raise_raise_exc [code func, code inline]:
+lemma raise_raise_exc [code, code inline]:
"raise s = raise_exc (Fail (STR s))"
unfolding Fail_def raise_exc_def raise_def ..
--- a/src/HOL/Library/List_Prefix.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/List_Prefix.thy Fri Oct 10 06:45:53 2008 +0200
@@ -15,10 +15,10 @@
begin
definition
- prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
+ prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
definition
- strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
+ strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
instance
by intro_classes (auto simp add: prefix_def strict_prefix_def)
@@ -374,18 +374,18 @@
subsection {* Executable code *}
-lemma less_eq_code [code func]:
+lemma less_eq_code [code]:
"([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
by simp_all
-lemma less_code [code func]:
+lemma less_code [code]:
"xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
"[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
"(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
unfolding strict_prefix_def by auto
-lemmas [code func] = postfix_to_prefix
+lemmas [code] = postfix_to_prefix
end
--- a/src/HOL/Library/List_lexord.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/List_lexord.thy Fri Oct 10 06:45:53 2008 +0200
@@ -13,10 +13,10 @@
begin
definition
- list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
+ list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
definition
- list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
+ list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
instance ..
@@ -63,10 +63,10 @@
begin
definition
- [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+ [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
definition
- [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
+ [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
instance
by intro_classes
@@ -92,13 +92,13 @@
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
by (unfold list_le_def) auto
-lemma less_code [code func]:
+lemma less_code [code]:
"xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
"[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
"(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
by simp_all
-lemma less_eq_code [code func]:
+lemma less_eq_code [code]:
"x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
"[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
"(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
--- a/src/HOL/Library/Multiset.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Oct 10 06:45:53 2008 +0200
@@ -29,7 +29,7 @@
"single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
declare
- Mempty_def[code func del] single_def[code func del]
+ Mempty_def[code del] single_def[code del]
definition
count :: "'a multiset => 'a => nat" where
@@ -59,7 +59,7 @@
begin
definition
- union_def[code func del]:
+ union_def[code del]:
"M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
definition
@@ -69,7 +69,7 @@
Zero_multiset_def [simp]: "0 = {#}"
definition
- size_def[code func del]: "size M = setsum (count M) (set_of M)"
+ size_def[code del]: "size M = setsum (count M) (set_of M)"
instance ..
@@ -207,10 +207,10 @@
subsubsection {* Size *}
-lemma size_empty [simp,code func]: "size {#} = 0"
+lemma size_empty [simp,code]: "size {#} = 0"
by (simp add: size_def)
-lemma size_single [simp,code func]: "size {#b#} = 1"
+lemma size_single [simp,code]: "size {#b#} = 1"
by (simp add: size_def)
lemma finite_set_of [iff]: "finite (set_of M)"
@@ -223,7 +223,7 @@
apply (simp add: Int_insert_left set_of_def)
done
-lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N"
+lemma size_union[simp,code]: "size (M + N::'a multiset) = size M + size N"
apply (unfold size_def)
apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
prefer 2
@@ -376,16 +376,16 @@
subsubsection {* Comprehension (filter) *}
-lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
+lemma MCollect_empty[simp, code]: "MCollect {#} P = {#}"
by (simp add: MCollect_def Mempty_def Abs_multiset_inject
in_multiset expand_fun_eq)
-lemma MCollect_single[simp, code func]:
+lemma MCollect_single[simp, code]:
"MCollect {#x#} P = (if P x then {#x#} else {#})"
by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
in_multiset expand_fun_eq)
-lemma MCollect_union[simp, code func]:
+lemma MCollect_union[simp, code]:
"MCollect (M+N) f = MCollect M f + MCollect N f"
by (simp add: MCollect_def union_def Abs_multiset_inject
in_multiset expand_fun_eq)
@@ -500,7 +500,7 @@
definition
mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
- [code func del]:"mult1 r =
+ [code del]:"mult1 r =
{(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
(\<forall>b. b :# K --> (b, a) \<in> r)}"
@@ -716,10 +716,10 @@
begin
definition
- less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+ less_multiset_def [code del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
definition
- le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
+ le_multiset_def [code del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
unfolding trans_def by (blast intro: order_less_trans)
@@ -983,11 +983,11 @@
definition
mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
- [code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
+ [code del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
definition
mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
- [code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
+ [code del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
notation mset_le (infix "\<subseteq>#" 50)
notation mset_less (infix "\<subset>#" 50)
@@ -1448,22 +1448,22 @@
subsection {* Image *}
-definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
+definition [code del]: "image_mset f == fold_mset (op + o single o f) {#}"
interpretation image_left_comm: left_commutative ["op + o single o f"]
by (unfold_locales) (simp add:union_ac)
-lemma image_mset_empty [simp, code func]: "image_mset f {#} = {#}"
+lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
by (simp add: image_mset_def)
-lemma image_mset_single [simp, code func]: "image_mset f {#x#} = {#f x#}"
+lemma image_mset_single [simp, code]: "image_mset f {#x#} = {#f x#}"
by (simp add: image_mset_def)
lemma image_mset_insert:
"image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
by (simp add: image_mset_def add_ac)
-lemma image_mset_union[simp, code func]:
+lemma image_mset_union[simp, code]:
"image_mset f (M+N) = image_mset f M + image_mset f N"
apply (induct N)
apply simp
--- a/src/HOL/Library/Nat_Infinity.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Fri Oct 10 06:45:53 2008 +0200
@@ -37,7 +37,7 @@
[code inline]: "1 = Fin 1"
definition
- [code inline, code func del]: "number_of k = Fin (number_of k)"
+ [code inline, code del]: "number_of k = Fin (number_of k)"
instance ..
--- a/src/HOL/Library/Nested_Environment.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Fri Oct 10 06:45:53 2008 +0200
@@ -525,11 +525,11 @@
text {* Environments and code generation *}
-lemma [code func, code func del]:
+lemma [code, code del]:
fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
-lemma eq_env_code [code func]:
+lemma eq_env_code [code]:
fixes x y :: "'a\<Colon>eq"
and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
@@ -567,7 +567,7 @@
of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
qed simp_all
-lemma [code func, code func del]:
+lemma [code, code del]:
"(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
end
--- a/src/HOL/Library/Option_ord.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Option_ord.thy Fri Oct 10 06:45:53 2008 +0200
@@ -13,10 +13,10 @@
begin
definition less_eq_option where
- [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))"
+ [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))"
definition less_option where
- [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))"
+ [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))"
lemma less_eq_option_None [simp]: "None \<le> x"
by (simp add: less_eq_option_def)
--- a/src/HOL/Library/Primes.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Primes.thy Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
definition
prime :: "nat \<Rightarrow> bool" where
- [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+ [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
lemma two_is_prime: "prime 2"
--- a/src/HOL/Library/Product_ord.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Product_ord.thy Fri Oct 10 06:45:53 2008 +0200
@@ -13,16 +13,16 @@
begin
definition
- 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"
+ prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
definition
- prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+ prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
instance ..
end
-lemma [code func]:
+lemma [code]:
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
unfolding prod_le_def prod_less_def by simp_all
--- a/src/HOL/Library/RType.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/RType.thy Fri Oct 10 06:45:53 2008 +0200
@@ -89,7 +89,7 @@
#> TypedefPackage.interpretation Typerep.perhaps_add_def
*}
-lemma [code func]:
+lemma [code]:
"eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
\<and> list_all2 eq_class.eq tys1 tys2"
by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
--- a/src/HOL/Library/Ref.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Ref.thy Fri Oct 10 06:45:53 2008 +0200
@@ -51,7 +51,7 @@
by (cases f)
(auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
-lemma update_change [code func]:
+lemma update_change [code]:
"r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
by (auto simp add: monad_simp change_def lookup_chain)
--- a/src/HOL/Library/Sublist_Order.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Sublist_Order.thy Fri Oct 10 06:45:53 2008 +0200
@@ -47,7 +47,7 @@
using assms by (induct rule: less_eq_list.induct) blast+
definition
- [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+ [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
by (induct rule: ileq_induct) auto
--- a/src/HOL/Library/Univ_Poly.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Fri Oct 10 06:45:53 2008 +0200
@@ -72,7 +72,7 @@
definition (in semiring_0)
divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where
- [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+ [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
--{*order of a polynomial*}
definition (in ring_1) order :: "'a => 'a list => nat" where
--- a/src/HOL/Library/Word.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Word.thy Fri Oct 10 06:45:53 2008 +0200
@@ -2042,7 +2042,7 @@
definition
length_nat :: "nat => nat" where
- [code func del]: "length_nat x = (LEAST n. x < 2 ^ n)"
+ [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
lemma length_nat: "length (nat_to_bv n) = length_nat n"
apply (simp add: length_nat_def)
@@ -2267,7 +2267,7 @@
fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
-declare fast_bv_to_nat_helper.simps [code func del]
+declare fast_bv_to_nat_helper.simps [code del]
lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
fast_bv_to_nat_helper bs (Int.Bit0 bin)"
--- a/src/HOL/List.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/List.thy Fri Oct 10 06:45:53 2008 +0200
@@ -204,7 +204,7 @@
definition
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
- [code func del]: "list_all2 P xs ys =
+ [code del]: "list_all2 P xs ys =
(length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
definition
@@ -2872,7 +2872,7 @@
definition
sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
- [code func del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
+ [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
set(sorted_list_of_set A) = A &
@@ -3057,7 +3057,7 @@
constdefs
set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
"set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
-declare set_Cons_def [code func del]
+declare set_Cons_def [code del]
lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
by (auto simp add: set_Cons_def)
@@ -3095,7 +3095,7 @@
"lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
--{*Compares lists by their length and then lexicographically*}
-declare lex_def [code func del]
+declare lex_def [code del]
lemma wf_lexn: "wf r ==> wf (lexn r n)"
@@ -3171,7 +3171,7 @@
lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
"lexord r == {(x,y). \<exists> a v. y = x @ a # v \<or>
(\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
-declare lexord_def [code func del]
+declare lexord_def [code del]
lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
by (unfold lexord_def, induct_tac y, auto)
@@ -3379,7 +3379,7 @@
primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
"nibble_pair_of_char (Char n m) = (n, m)"
-declare nibble_pair_of_char.simps [code func del]
+declare nibble_pair_of_char.simps [code del]
setup {*
let
@@ -3393,11 +3393,11 @@
end
*}
-lemma char_case_nibble_pair [code func, code inline]:
+lemma char_case_nibble_pair [code, code inline]:
"char_case f = split f o nibble_pair_of_char"
by (simp add: expand_fun_eq split: char.split)
-lemma char_rec_nibble_pair [code func, code inline]:
+lemma char_rec_nibble_pair [code, code inline]:
"char_rec f = split f o nibble_pair_of_char"
unfolding char_case_nibble_pair [symmetric]
by (simp add: expand_fun_eq split: char.split)
--- a/src/HOL/Map.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Map.thy Fri Oct 10 06:45:53 2008 +0200
@@ -91,7 +91,7 @@
by simp_all
defs
- map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
+ map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
subsection {* @{term [source] empty} *}
--- a/src/HOL/Matrix/Matrix.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Matrix/Matrix.thy Fri Oct 10 06:45:53 2008 +0200
@@ -768,7 +768,7 @@
instantiation matrix :: (zero) zero
begin
-definition zero_matrix_def [code func del]: "0 = Abs_matrix (\<lambda>j i. 0)"
+definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
instance ..
@@ -1440,9 +1440,9 @@
instantiation matrix :: ("{lattice, zero}") lattice
begin
-definition [code func del]: "inf = combine_matrix inf"
+definition [code del]: "inf = combine_matrix inf"
-definition [code func del]: "sup = combine_matrix sup"
+definition [code del]: "sup = combine_matrix sup"
instance
by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
@@ -1453,7 +1453,7 @@
begin
definition
- plus_matrix_def [code func del]: "A + B = combine_matrix (op +) A B"
+ plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
instance ..
@@ -1463,7 +1463,7 @@
begin
definition
- minus_matrix_def [code func del]: "- A = apply_matrix uminus A"
+ minus_matrix_def [code del]: "- A = apply_matrix uminus A"
instance ..
@@ -1473,7 +1473,7 @@
begin
definition
- diff_matrix_def [code func del]: "A - B = combine_matrix (op -) A B"
+ diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
instance ..
@@ -1483,7 +1483,7 @@
begin
definition
- times_matrix_def [code func del]: "A * B = mult_matrix (op *) (op +) A B"
+ times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
instance ..
@@ -1493,7 +1493,7 @@
begin
definition
- abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
+ abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
instance ..
--- a/src/HOL/Matrix/SparseMatrix.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Fri Oct 10 06:45:53 2008 +0200
@@ -25,7 +25,7 @@
lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
by (simp add: sparse_row_matrix_def)
-lemmas [code func] = sparse_row_vector_empty [symmetric]
+lemmas [code] = sparse_row_vector_empty [symmetric]
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))"
by (induct l, auto)
@@ -417,8 +417,8 @@
apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
done
-lemmas [code func] = sparse_row_add_spmat [symmetric]
-lemmas [code func] = sparse_row_vector_add [symmetric]
+lemmas [code] = sparse_row_add_spmat [symmetric]
+lemmas [code] = sparse_row_vector_add [symmetric]
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)))"
proof -
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 10 06:45:53 2008 +0200
@@ -68,7 +68,7 @@
definition
"wf_class G = wfP ((subcls1 G)^--1)"
-lemma class_rec_func (*[code func]*):
+lemma class_rec_func (*[code]*):
"class_rec G C t f = (if wf_class G then
(case class G C
of None \<Rightarrow> undefined
--- a/src/HOL/NSA/HDeriv.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HDeriv.thy Fri Oct 10 06:45:53 2008 +0200
@@ -27,7 +27,7 @@
definition
increment :: "[real=>real,real,hypreal] => hypreal" where
- [code func del]: "increment f x h = (@inc. f NSdifferentiable x &
+ [code del]: "increment f x h = (@inc. f NSdifferentiable x &
inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
--- a/src/HOL/NSA/HLim.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HLim.thy Fri Oct 10 06:45:53 2008 +0200
@@ -16,18 +16,18 @@
definition
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
- [code func del]: "f -- a --NS> L =
+ [code del]: "f -- a --NS> L =
(\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
definition
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
--{*NS definition dispenses with limit notions*}
- [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
+ [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
( *f* f) y @= star_of (f a))"
definition
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+ [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
subsection {* Limits of Functions *}
--- a/src/HOL/NSA/HLog.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HLog.thy Fri Oct 10 06:45:53 2008 +0200
@@ -20,11 +20,11 @@
definition
powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
- [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
+ [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
definition
hlog :: "[hypreal,hypreal] => hypreal" where
- [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
+ [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
by (simp add: powhr_def starfun2_star_n)
--- a/src/HOL/NSA/HSEQ.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HSEQ.thy Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----NS> (_))" [60, 60] 60) where
--{*Nonstandard definition of convergence of sequence*}
- [code func del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+ [code del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
definition
nslim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -31,12 +31,12 @@
definition
NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition for bounded sequence*}
- [code func del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+ [code del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
definition
NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition*}
- [code func del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+ [code del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
subsection {* Limits of Sequences *}
--- a/src/HOL/NSA/HSeries.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HSeries.thy Fri Oct 10 06:45:53 2008 +0200
@@ -13,7 +13,7 @@
definition
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
- [code func del]: "sumhr =
+ [code del]: "sumhr =
(%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
definition
@@ -22,7 +22,7 @@
definition
NSsummable :: "(nat=>real) => bool" where
- [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
+ [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
definition
NSsuminf :: "(nat=>real) => real" where
--- a/src/HOL/NSA/HyperDef.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HyperDef.thy Fri Oct 10 06:45:53 2008 +0200
@@ -47,7 +47,7 @@
begin
definition
- star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)"
+ star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
instance ..
@@ -113,7 +113,7 @@
definition
of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
- [transfer_unfold, code func del]: "of_hypreal = *f* of_real"
+ [transfer_unfold, code del]: "of_hypreal = *f* of_real"
lemma Standard_of_hypreal [simp]:
"r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
@@ -428,7 +428,7 @@
subsection{*Powers with Hypernatural Exponents*}
definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
- hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N"
+ hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
(* hypernatural powers of hyperreals *)
lemma Standard_hyperpow [simp]:
--- a/src/HOL/NSA/HyperNat.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HyperNat.thy Fri Oct 10 06:45:53 2008 +0200
@@ -19,7 +19,7 @@
definition
hSuc :: "hypnat => hypnat" where
- hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
+ hSuc_def [transfer_unfold, code del]: "hSuc = *f* Suc"
subsection{*Properties Transferred from Naturals*}
@@ -367,7 +367,7 @@
definition
of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
- of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
+ of_hypnat_def [transfer_unfold, code del]: "of_hypnat = *f* of_nat"
lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
by transfer (rule of_nat_0)
--- a/src/HOL/NSA/NSA.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/NSA.thy Fri Oct 10 06:45:53 2008 +0200
@@ -17,15 +17,15 @@
definition
Infinitesimal :: "('a::real_normed_vector) star set" where
- [code func del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
+ [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
definition
HFinite :: "('a::real_normed_vector) star set" where
- [code func del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
+ [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
definition
HInfinite :: "('a::real_normed_vector) star set" where
- [code func del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
+ [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
definition
approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
@@ -58,7 +58,7 @@
definition
scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
- [transfer_unfold, code func del]: "scaleHR = starfun2 scaleR"
+ [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
by (simp add: hnorm_def)
--- a/src/HOL/NSA/NSCA.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/NSCA.thy Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
definition --{* standard part map*}
stc :: "hcomplex => hcomplex" where
- [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+ [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
--- a/src/HOL/NSA/NSComplex.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/NSComplex.thy Fri Oct 10 06:45:53 2008 +0200
@@ -26,11 +26,11 @@
definition
hRe :: "hcomplex => hypreal" where
- [code func del]: "hRe = *f* Re"
+ [code del]: "hRe = *f* Re"
definition
hIm :: "hcomplex => hypreal" where
- [code func del]: "hIm = *f* Im"
+ [code del]: "hIm = *f* Im"
(*------ imaginary unit ----------*)
@@ -43,22 +43,22 @@
definition
hcnj :: "hcomplex => hcomplex" where
- [code func del]: "hcnj = *f* cnj"
+ [code del]: "hcnj = *f* cnj"
(*------------ Argand -------------*)
definition
hsgn :: "hcomplex => hcomplex" where
- [code func del]: "hsgn = *f* sgn"
+ [code del]: "hsgn = *f* sgn"
definition
harg :: "hcomplex => hypreal" where
- [code func del]: "harg = *f* arg"
+ [code del]: "harg = *f* arg"
definition
(* abbreviation for (cos a + i sin a) *)
hcis :: "hypreal => hcomplex" where
- [code func del]:"hcis = *f* cis"
+ [code del]:"hcis = *f* cis"
(*----- injection from hyperreals -----*)
@@ -69,16 +69,16 @@
definition
(* abbreviation for r*(cos a + i sin a) *)
hrcis :: "[hypreal, hypreal] => hcomplex" where
- [code func del]: "hrcis = *f2* rcis"
+ [code del]: "hrcis = *f2* rcis"
(*------------ e ^ (x + iy) ------------*)
definition
hexpi :: "hcomplex => hcomplex" where
- [code func del]: "hexpi = *f* expi"
+ [code del]: "hexpi = *f* expi"
definition
HComplex :: "[hypreal,hypreal] => hcomplex" where
- [code func del]: "HComplex = *f2* Complex"
+ [code del]: "HComplex = *f2* Complex"
lemmas hcomplex_defs [transfer_unfold] =
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
--- a/src/HOL/NSA/Star.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/Star.thy Fri Oct 10 06:45:53 2008 +0200
@@ -17,12 +17,12 @@
definition
InternalSets :: "'a star set set" where
- [code func del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
+ [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
definition
(* nonstandard extension of function *)
is_starext :: "['a star => 'a star, 'a => 'a] => bool" where
- [code func del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+ [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
definition
@@ -32,7 +32,7 @@
definition
InternalFuns :: "('a star => 'b star) set" where
- [code func del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
+ [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
(*--------------------------------------------------------
--- a/src/HOL/NSA/StarDef.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Oct 10 06:45:53 2008 +0200
@@ -291,7 +291,7 @@
subsection {* Internal predicates *}
definition unstar :: "bool star \<Rightarrow> bool" where
- [code func del]: "unstar b \<longleftrightarrow> b = star_of True"
+ [code del]: "unstar b \<longleftrightarrow> b = star_of True"
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -432,7 +432,7 @@
begin
definition
- star_zero_def [code func del]: "0 \<equiv> star_of 0"
+ star_zero_def [code del]: "0 \<equiv> star_of 0"
instance ..
@@ -442,7 +442,7 @@
begin
definition
- star_one_def [code func del]: "1 \<equiv> star_of 1"
+ star_one_def [code del]: "1 \<equiv> star_of 1"
instance ..
@@ -452,7 +452,7 @@
begin
definition
- star_add_def [code func del]: "(op +) \<equiv> *f2* (op +)"
+ star_add_def [code del]: "(op +) \<equiv> *f2* (op +)"
instance ..
@@ -462,7 +462,7 @@
begin
definition
- star_mult_def [code func del]: "(op *) \<equiv> *f2* (op *)"
+ star_mult_def [code del]: "(op *) \<equiv> *f2* (op *)"
instance ..
@@ -472,7 +472,7 @@
begin
definition
- star_minus_def [code func del]: "uminus \<equiv> *f* uminus"
+ star_minus_def [code del]: "uminus \<equiv> *f* uminus"
instance ..
@@ -482,7 +482,7 @@
begin
definition
- star_diff_def [code func del]: "(op -) \<equiv> *f2* (op -)"
+ star_diff_def [code del]: "(op -) \<equiv> *f2* (op -)"
instance ..
--- a/src/HOL/Nat.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Nat.thy Fri Oct 10 06:45:53 2008 +0200
@@ -55,7 +55,7 @@
instantiation nat :: zero
begin
-definition Zero_nat_def [code func del]:
+definition Zero_nat_def [code del]:
"0 = Abs_Nat Zero_Rep"
instance ..
@@ -1281,7 +1281,7 @@
definition
Nats :: "'a set" where
- [code func del]: "Nats = range of_nat"
+ [code del]: "Nats = range of_nat"
notation (xsymbols)
Nats ("\<nat>")
--- a/src/HOL/NatBin.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NatBin.thy Fri Oct 10 06:45:53 2008 +0200
@@ -18,7 +18,7 @@
begin
definition
- nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)"
+ nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
instance ..
--- a/src/HOL/Orderings.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 10 06:45:53 2008 +0200
@@ -968,10 +968,10 @@
begin
definition
- le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+ le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
definition
- less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
+ less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
instance
by intro_classes (auto simp add: le_bool_def less_bool_def)
@@ -990,7 +990,7 @@
lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
by (simp add: le_bool_def)
-lemma [code func]:
+lemma [code]:
"False \<le> b \<longleftrightarrow> True"
"True \<le> b \<longleftrightarrow> b"
"False < b \<longleftrightarrow> b"
@@ -1004,10 +1004,10 @@
begin
definition
- le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
+ le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
definition
- less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
+ less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
instance ..
--- a/src/HOL/Product_Type.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Product_Type.thy Fri Oct 10 06:45:53 2008 +0200
@@ -23,10 +23,10 @@
-- "prefer plain propositional version"
lemma
- shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
- and [code func]: "eq_class.eq True P \<longleftrightarrow> P"
- and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
- and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
+ shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
+ and [code]: "eq_class.eq True P \<longleftrightarrow> P"
+ and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
+ and [code]: "eq_class.eq P True \<longleftrightarrow> P"
and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
by (simp_all add: eq)
@@ -89,7 +89,7 @@
instance unit :: eq ..
-lemma [code func]:
+lemma [code]:
"eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
code_type unit
@@ -359,10 +359,10 @@
subsubsection {* @{text split} and @{text curry} *}
-lemma split_conv [simp, code func]: "split f (a, b) = f a b"
+lemma split_conv [simp, code]: "split f (a, b) = f a b"
by (simp add: split_def)
-lemma curry_conv [simp, code func]: "curry f a b = f (a, b)"
+lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
by (simp add: curry_def)
lemmas split = split_conv -- {* for backwards compatibility *}
@@ -728,9 +728,9 @@
*}
definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
- [code func del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
+ [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
-lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
+lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
by (simp add: prod_fun_def)
lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
@@ -758,12 +758,12 @@
definition
apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
where
- [code func del]: "apfst f = prod_fun f id"
+ [code del]: "apfst f = prod_fun f id"
definition
apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
where
- [code func del]: "apsnd f = prod_fun id f"
+ [code del]: "apsnd f = prod_fun id f"
lemma apfst_conv [simp, code]:
"apfst f (x, y) = (f x, y)"
@@ -917,7 +917,7 @@
instance * :: (eq, eq) eq ..
-lemma [code func]:
+lemma [code]:
"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)
lemma split_case_cert:
--- a/src/HOL/Real/ContNotDenum.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/ContNotDenum.thy Fri Oct 10 06:45:53 2008 +0200
@@ -403,7 +403,7 @@
(f (Suc n)) \<notin> e)
)"
-declare newInt.simps [code func del]
+declare newInt.simps [code del]
subsubsection {* Properties *}
--- a/src/HOL/Real/PReal.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/PReal.thy Fri Oct 10 06:45:53 2008 +0200
@@ -19,7 +19,7 @@
definition
cut :: "rat set => bool" where
- [code func del]: "cut A = ({} \<subset> A &
+ [code del]: "cut A = ({} \<subset> A &
A < {r. 0 < r} &
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
@@ -56,7 +56,7 @@
definition
diff_set :: "[rat set,rat set] => rat set" where
- [code func del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+ [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
definition
mult_set :: "[rat set,rat set] => rat set" where
@@ -64,17 +64,17 @@
definition
inverse_set :: "rat set => rat set" where
- [code func del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+ [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
instantiation preal :: "{ord, plus, minus, times, inverse, one}"
begin
definition
- preal_less_def [code func del]:
+ preal_less_def [code del]:
"R < S == Rep_preal R < Rep_preal S"
definition
- preal_le_def [code func del]:
+ preal_le_def [code del]:
"R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
definition
--- a/src/HOL/Real/RComplete.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/RComplete.thy Fri Oct 10 06:45:53 2008 +0200
@@ -488,7 +488,7 @@
definition
floor :: "real => int" where
- [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
+ [code del]: "floor r = (LEAST n::int. r < real (n+1))"
definition
ceiling :: "real => int" where
--- a/src/HOL/Real/Rational.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/Rational.thy Fri Oct 10 06:45:53 2008 +0200
@@ -71,7 +71,7 @@
definition
Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
- [code func del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
+ [code del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
code_datatype Fract
@@ -101,7 +101,7 @@
One_rat_def [code, code unfold]: "1 = Fract 1 1"
definition
- add_rat_def [code func del]:
+ add_rat_def [code del]:
"q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
@@ -116,7 +116,7 @@
qed
definition
- minus_rat_def [code func del]:
+ minus_rat_def [code del]:
"- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})"
lemma minus_rat [simp, code]: "- Fract a b = Fract (- a) b"
@@ -130,7 +130,7 @@
by (cases "b = 0") (simp_all add: eq_rat)
definition
- diff_rat_def [code func del]: "q - r = q + - (r::rat)"
+ diff_rat_def [code del]: "q - r = q + - (r::rat)"
lemma diff_rat [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -138,7 +138,7 @@
using assms by (simp add: diff_rat_def)
definition
- mult_rat_def [code func del]:
+ mult_rat_def [code del]:
"q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
ratrel``{(fst x * fst y, snd x * snd y)})"
@@ -219,7 +219,7 @@
begin
definition
- rat_number_of_def [code func del]: "number_of w = Fract w 1"
+ rat_number_of_def [code del]: "number_of w = Fract w 1"
instance by intro_classes (simp add: rat_number_of_def of_int_rat)
@@ -265,7 +265,7 @@
begin
definition
- inverse_rat_def [code func del]:
+ inverse_rat_def [code del]:
"inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.
ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
@@ -277,7 +277,7 @@
qed
definition
- divide_rat_def [code func del]: "q / r = q * inverse (r::rat)"
+ divide_rat_def [code del]: "q / r = q * inverse (r::rat)"
lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
by (simp add: divide_rat_def)
@@ -320,7 +320,7 @@
begin
definition
- le_rat_def [code func del]:
+ le_rat_def [code del]:
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
@@ -370,7 +370,7 @@
qed
definition
- less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+ less_rat_def [code del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
lemma less_rat [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -450,13 +450,13 @@
begin
definition
- abs_rat_def [code func del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
+ abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
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)
definition
- sgn_rat_def [code func del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
+ sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)"
unfolding Fract_of_int_eq
@@ -553,7 +553,7 @@
begin
definition of_rat :: "rat \<Rightarrow> 'a" where
- [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
+ [code del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
end
@@ -680,7 +680,7 @@
definition
Rats :: "'a set" where
- [code func del]: "Rats = range of_rat"
+ [code del]: "Rats = range of_rat"
notation (xsymbols)
Rats ("\<rat>")
@@ -850,9 +850,9 @@
qed
definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
- [simp, code func del]: "Fract_norm a b = Fract a b"
+ [simp, code del]: "Fract_norm a b = Fract a b"
-lemma [code func]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
+lemma [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
@@ -863,7 +863,7 @@
instantiation rat :: eq
begin
-definition [code func del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
+definition [code del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
instance by default (simp add: eq_rat_def)
--- a/src/HOL/Real/RealDef.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/RealDef.thy Fri Oct 10 06:45:53 2008 +0200
@@ -15,7 +15,7 @@
definition
realrel :: "((preal * preal) * (preal * preal)) set" where
- [code func del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Real) real = "UNIV//realrel"
by (auto simp add: quotient_def)
@@ -23,46 +23,46 @@
definition
(** these don't use the overloaded "real" function: users don't see them **)
real_of_preal :: "preal => real" where
- [code func del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
+ [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
begin
definition
- real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
+ real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
definition
- real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
+ real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
definition
- real_add_def [code func del]: "z + w =
+ real_add_def [code del]: "z + w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x+u, y+v)}) })"
definition
- real_minus_def [code func del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+ real_minus_def [code del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
definition
- real_diff_def [code func del]: "r - (s::real) = r + - s"
+ real_diff_def [code del]: "r - (s::real) = r + - s"
definition
- real_mult_def [code func del]:
+ real_mult_def [code del]:
"z * w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
definition
- real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
+ real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
definition
- real_divide_def [code func del]: "R / (S::real) = R * inverse S"
+ real_divide_def [code del]: "R / (S::real) = R * inverse S"
definition
- real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
+ real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
(\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
definition
- real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+ real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
definition
real_abs_def: "abs (r::real) = (if r < 0 then - r else r)"
@@ -939,7 +939,7 @@
begin
definition
- real_number_of_def [code func del]: "number_of w = real_of_int w"
+ real_number_of_def [code del]: "number_of w = real_of_int w"
instance
by intro_classes (simp add: real_number_of_def)
--- a/src/HOL/Real/RealVector.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/RealVector.thy Fri Oct 10 06:45:53 2008 +0200
@@ -308,7 +308,7 @@
definition
Reals :: "'a::real_algebra_1 set" where
- [code func del]: "Reals \<equiv> range of_real"
+ [code del]: "Reals \<equiv> range of_real"
notation (xsymbols)
Reals ("\<real>")
--- a/src/HOL/Set.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Set.thy Fri Oct 10 06:45:53 2008 +0200
@@ -324,8 +324,8 @@
text {* Isomorphisms between predicates and sets. *}
defs
- mem_def [code func]: "x : S == S x"
- Collect_def [code func]: "Collect P == P"
+ mem_def [code]: "x : S == S x"
+ Collect_def [code]: "Collect P == P"
defs
Ball_def: "Ball A P == ALL x. x:A --> P(x)"
@@ -2061,7 +2061,7 @@
constdefs
vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90)
- [code func del]: "f -` B == {x. f x : B}"
+ [code del]: "f -` B == {x. f x : B}"
subsubsection {* Basic rules *}
@@ -2156,7 +2156,7 @@
definition
contents :: "'a set \<Rightarrow> 'a"
where
- [code func del]: "contents X = (THE x. X = {x})"
+ [code del]: "contents X = (THE x. X = {x})"
lemma contents_eq [simp]: "contents {x} = x"
by (simp add: contents_def)
@@ -2189,22 +2189,22 @@
subsection {* Rudimentary code generation *}
-lemma empty_code [code func]: "{} x \<longleftrightarrow> False"
+lemma empty_code [code]: "{} x \<longleftrightarrow> False"
unfolding empty_def Collect_def ..
-lemma UNIV_code [code func]: "UNIV x \<longleftrightarrow> True"
+lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
unfolding UNIV_def Collect_def ..
-lemma insert_code [code func]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
+lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
unfolding insert_def Collect_def mem_def Un_def by auto
-lemma inter_code [code func]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
+lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
unfolding Int_def Collect_def mem_def ..
-lemma union_code [code func]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
+lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
unfolding Un_def Collect_def mem_def ..
-lemma vimage_code [code func]: "(f -` A) x = A (f x)"
+lemma vimage_code [code]: "(f -` A) x = A (f x)"
unfolding vimage_def Collect_def mem_def ..
--- a/src/HOL/SizeChange/Graphs.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/SizeChange/Graphs.thy Fri Oct 10 06:45:53 2008 +0200
@@ -67,7 +67,7 @@
graph_zero_def: "0 = Graph {}"
definition
- graph_plus_def [code func del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
+ graph_plus_def [code del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
instance proof
fix x y z :: "('a,'b) graph"
@@ -83,22 +83,22 @@
begin
definition
- graph_leq_def [code func del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
+ graph_leq_def [code del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
definition
- graph_less_def [code func del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
+ graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
definition
- [code func del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
+ [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
definition
- [code func del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
+ [code del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
definition
- Inf_graph_def [code func del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
+ Inf_graph_def [code del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
definition
- Sup_graph_def [code func del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
+ Sup_graph_def [code del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
instance proof
fix x y z :: "('a,'b) graph"
@@ -165,7 +165,7 @@
begin
definition
- graph_mult_def [code func del]: "G * H = grcomp G H"
+ graph_mult_def [code del]: "G * H = grcomp G H"
instance proof
fix a :: "('a, 'b) graph"
--- a/src/HOL/SizeChange/Implementation.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/SizeChange/Implementation.thy Fri Oct 10 06:45:53 2008 +0200
@@ -122,16 +122,16 @@
code_modulename SML
Implementation Graphs
-lemma [code func]:
+lemma [code]:
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
unfolding graph_leq_def graph_less_def by rule+
-lemma [code func]:
+lemma [code]:
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
unfolding graph_plus_def ..
-lemma [code func]:
+lemma [code]:
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
unfolding graph_mult_def ..
--- a/src/HOL/Tools/ComputeHOL.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Tools/ComputeHOL.thy Fri Oct 10 06:45:53 2008 +0200
@@ -1,5 +1,5 @@
theory ComputeHOL
-imports Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
+imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
begin
lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
--- a/src/HOL/Wellfounded.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Wellfounded.thy Fri Oct 10 06:45:53 2008 +0200
@@ -40,7 +40,7 @@
(ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
- [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+ [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
abbreviation acyclicP :: "('a => 'a => bool) => bool" where
"acyclicP r == acyclic {(x, y). r x y}"
@@ -840,10 +840,10 @@
setup Size.setup
-lemma size_bool [code func]:
+lemma size_bool [code]:
"size (b\<Colon>bool) = 0" by (cases b) auto
-lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
+lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
by (induct n) simp_all
declare "prod.size" [noatp]
--- a/src/HOL/Word/BinGeneral.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Word/BinGeneral.thy Fri Oct 10 06:45:53 2008 +0200
@@ -129,7 +129,7 @@
subsection {* Destructors for binary integers *}
definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
- [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
+ [code del]: "bin_rl w = (THE (r, l). w = r BIT l)"
lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
apply (unfold bin_rl_def)
@@ -139,10 +139,10 @@
done
definition
- bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
+ bin_rest_def [code del]: "bin_rest w = fst (bin_rl w)"
definition
- bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
+ bin_last_def [code del] : "bin_last w = snd (bin_rl w)"
primrec bin_nth where
Z: "bin_nth w 0 = (bin_last w = bit.B1)"
@@ -159,7 +159,7 @@
"bin_rl (r BIT b) = (r, b)"
unfolding bin_rl_char by simp_all
-declare bin_rl_simps(1-4) [code func]
+declare bin_rl_simps(1-4) [code]
lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
@@ -212,7 +212,7 @@
"bin_rest (w BIT b) = w"
unfolding bin_rest_def by auto
-declare bin_rest_simps(1-4) [code func]
+declare bin_rest_simps(1-4) [code]
lemma bin_last_simps [simp]:
"bin_last Int.Pls = bit.B0"
@@ -222,7 +222,7 @@
"bin_last (w BIT b) = b"
unfolding bin_last_def by auto
-declare bin_last_simps(1-4) [code func]
+declare bin_last_simps(1-4) [code]
lemma bin_r_l_extras [simp]:
"bin_last 0 = bit.B0"
@@ -403,7 +403,7 @@
subsection {* Truncating binary integers *}
definition
- bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
+ bin_sign_def [code del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
lemma bin_sign_simps [simp]:
"bin_sign Int.Pls = Int.Pls"
@@ -413,7 +413,7 @@
"bin_sign (w BIT b) = bin_sign w"
unfolding bin_sign_def by (auto simp: bin_rec_simps)
-declare bin_sign_simps(1-4) [code func]
+declare bin_sign_simps(1-4) [code]
lemma bin_sign_rest [simp]:
"bin_sign (bin_rest w) = (bin_sign w)"
--- a/src/HOL/Word/BinOperations.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Word/BinOperations.thy Fri Oct 10 06:45:53 2008 +0200
@@ -21,19 +21,19 @@
begin
definition
- int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls
+ int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls
(\<lambda>w b s. s BIT (NOT b))"
definition
- int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
+ int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
(\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
definition
- int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
+ int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
(\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
definition
- int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
+ int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
(\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
instance ..
@@ -48,13 +48,13 @@
"NOT (w BIT b) = (NOT w) BIT (NOT b)"
unfolding int_not_def by (simp_all add: bin_rec_simps)
-declare int_not_simps(1-4) [code func]
+declare int_not_simps(1-4) [code]
-lemma int_xor_Pls [simp, code func]:
+lemma int_xor_Pls [simp, code]:
"Int.Pls XOR x = x"
unfolding int_xor_def by (simp add: bin_rec_PM)
-lemma int_xor_Min [simp, code func]:
+lemma int_xor_Min [simp, code]:
"Int.Min XOR x = NOT x"
unfolding int_xor_def by (simp add: bin_rec_PM)
@@ -69,7 +69,7 @@
apply (simp add: int_not_simps [symmetric])
done
-lemma int_xor_Bits2 [simp, code func]:
+lemma int_xor_Bits2 [simp, code]:
"(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
"(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
"(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
@@ -85,16 +85,16 @@
apply clarsimp+
done
-lemma int_xor_extra_simps [simp, code func]:
+lemma int_xor_extra_simps [simp, code]:
"w XOR Int.Pls = w"
"w XOR Int.Min = NOT w"
using int_xor_x_simps' by simp_all
-lemma int_or_Pls [simp, code func]:
+lemma int_or_Pls [simp, code]:
"Int.Pls OR x = x"
by (unfold int_or_def) (simp add: bin_rec_PM)
-lemma int_or_Min [simp, code func]:
+lemma int_or_Min [simp, code]:
"Int.Min OR x = Int.Min"
by (unfold int_or_def) (simp add: bin_rec_PM)
@@ -102,7 +102,7 @@
"(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
unfolding int_or_def by (simp add: bin_rec_simps)
-lemma int_or_Bits2 [simp, code func]:
+lemma int_or_Bits2 [simp, code]:
"(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
"(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
"(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
@@ -118,16 +118,16 @@
apply clarsimp+
done
-lemma int_or_extra_simps [simp, code func]:
+lemma int_or_extra_simps [simp, code]:
"w OR Int.Pls = w"
"w OR Int.Min = Int.Min"
using int_or_x_simps' by simp_all
-lemma int_and_Pls [simp, code func]:
+lemma int_and_Pls [simp, code]:
"Int.Pls AND x = Int.Pls"
unfolding int_and_def by (simp add: bin_rec_PM)
-lemma int_and_Min [simp, code func]:
+lemma int_and_Min [simp, code]:
"Int.Min AND x = x"
unfolding int_and_def by (simp add: bin_rec_PM)
@@ -135,7 +135,7 @@
"(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
unfolding int_and_def by (simp add: bin_rec_simps)
-lemma int_and_Bits2 [simp, code func]:
+lemma int_and_Bits2 [simp, code]:
"(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
"(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
"(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
@@ -151,7 +151,7 @@
apply clarsimp+
done
-lemma int_and_extra_simps [simp, code func]:
+lemma int_and_extra_simps [simp, code]:
"w AND Int.Pls = Int.Pls"
"w AND Int.Min = w"
using int_and_x_simps' by simp_all
--- a/src/HOL/Word/WordDefinition.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy Fri Oct 10 06:45:53 2008 +0200
@@ -30,7 +30,7 @@
only difference in these is the type class *}
word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
where
- [code func del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
+ [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
code_datatype word_of_int
@@ -96,9 +96,9 @@
subsection "Arithmetic operations"
-declare uint_def [code func del]
+declare uint_def [code del]
-lemma [code func]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
+lemma [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse)
(insert range_bintrunc, auto)
--- a/src/HOL/ex/Codegenerator_Pretty.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy Fri Oct 10 06:45:53 2008 +0200
@@ -9,7 +9,7 @@
imports ExecutableContent Code_Char Efficient_Nat
begin
-declare isnorm.simps [code func del]
+declare isnorm.simps [code del]
ML {* (*FIXME get rid of this*)
nonfix union;
--- a/src/HOL/ex/NormalForm.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy Fri Oct 10 06:45:53 2008 +0200
@@ -12,7 +12,7 @@
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code nbe]
lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-declare disj_assoc [code func del]
+declare disj_assoc [code del]
lemma "0 + (n::nat) = n" by normalization
lemma "0 + Suc n = Suc n" by normalization
lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
--- a/src/HOL/ex/Numeral.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/Numeral.thy Fri Oct 10 06:45:53 2008 +0200
@@ -74,19 +74,19 @@
begin
definition one_num :: num where
- [code func del]: "1 = num_of_nat 1"
+ [code del]: "1 = num_of_nat 1"
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
- [code func del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
+ [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
- [code func del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
+ [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
definition Dig0 :: "num \<Rightarrow> num" where
- [code func del]: "Dig0 n = n + n"
+ [code del]: "Dig0 n = n + n"
definition Dig1 :: "num \<Rightarrow> num" where
- [code func del]: "Dig1 n = n + n + 1"
+ [code del]: "Dig1 n = n + n + 1"
instance proof
qed (simp_all add: one_num_def plus_num_def times_num_def
@@ -503,10 +503,10 @@
begin
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code func del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
+ [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code func del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
+ [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
instance proof
qed (auto simp add: less_eq_num_def less_num_def
@@ -768,10 +768,10 @@
lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
- [simp, code func del]: "sub m n = (of_num m - of_num n)"
+ [simp, code del]: "sub m n = (of_num m - of_num n)"
definition dup :: "int \<Rightarrow> int" where
- [code func del]: "dup k = 2 * k"
+ [code del]: "dup k = 2 * k"
lemma Dig_sub [code]:
"sub 1 1 = 0"
@@ -794,7 +794,7 @@
"dup (Mns n) = Mns (Dig0 n)"
by (simp_all add: dup_def of_num.simps)
-lemma [code func, code func del]:
+lemma [code, code del]:
"(1 :: int) = 1"
"(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
"(uminus :: int \<Rightarrow> int) = uminus"
--- a/src/HOL/ex/Random.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/Random.thy Fri Oct 10 06:45:53 2008 +0200
@@ -124,7 +124,7 @@
definition
select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
where
- [code func del]: "select_default k x y = (do
+ [code del]: "select_default k x y = (do
l \<leftarrow> range k;
return (if l + 1 < k then x else y)
done)"
--- a/src/Pure/Isar/code.ML Fri Oct 10 06:45:50 2008 +0200
+++ b/src/Pure/Isar/code.ML Fri Oct 10 06:45:53 2008 +0200
@@ -96,12 +96,10 @@
fun add_attribute (attr as (name, _)) =
let
- fun add_parser ("", parser) attrs = attrs @ [("", parser)]
+ fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
| add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
- fun error "" = error ("Code attribute already declared")
- | error name = error ("Code attribute " ^ name ^ " already declared")
- in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
- then error name else add_parser attr attrs)
+ in CodeAttr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
+ then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
end;
val _ =
@@ -637,7 +635,7 @@
|| Scan.succeed (mk_attribute add))
in
TypeInterpretation.init
- #> add_del_attribute ("func", (add_eqn, del_eqn))
+ #> add_del_attribute ("", (add_eqn, del_eqn))
#> add_simple_attribute ("nbe", add_nonlinear_eqn)
#> add_del_attribute ("inline", (add_inline, del_inline))
#> add_del_attribute ("post", (add_post, del_post))