--- a/CONTRIBUTORS Tue Jul 14 20:58:53 2009 -0400
+++ b/CONTRIBUTORS Tue Jul 14 21:19:34 2009 -0400
@@ -7,6 +7,12 @@
Contributions to this Isabelle version
--------------------------------------
+* July 2009: Florian Haftmann, TUM
+ New quickcheck implementation using new code generator
+
+* July 2009: Florian Haftmann, TUM
+ HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation
+
* June 2009: Andreas Lochbihler, Uni Karlsruhe
HOL/Library/Fin_Fun: almost everywhere constant functions
--- a/NEWS Tue Jul 14 20:58:53 2009 -0400
+++ b/NEWS Tue Jul 14 21:19:34 2009 -0400
@@ -18,6 +18,16 @@
*** HOL ***
+* Code generator attributes follow the usual underscore convention:
+ code_unfold replaces code unfold
+ code_post replaces code post
+ etc.
+ INCOMPATIBILITY.
+
+* New quickcheck implementation using new code generator.
+
+* New type class boolean_algebra.
+
* Class semiring_div requires superclass no_zero_divisors and proof of
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
--- a/doc-src/Codegen/Thy/ML.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/ML.thy Tue Jul 14 21:19:34 2009 -0400
@@ -78,8 +78,7 @@
text %mlref {*
\begin{mldecls}
- @{index_ML Code.read_const: "theory -> string -> string"} \\
- @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
+ @{index_ML Code.read_const: "theory -> string -> string"}
\end{mldecls}
\begin{description}
@@ -87,11 +86,6 @@
\item @{ML Code.read_const}~@{text thy}~@{text s}
reads a constant as a concrete term expression @{text s}.
- \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}
- rewrites a code equation @{text thm} with a simpset @{text ss};
- only arguments and right hand side are rewritten,
- not the head of the code equation.
-
\end{description}
*}
--- a/doc-src/Codegen/Thy/Program.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/Program.thy Tue Jul 14 21:19:34 2009 -0400
@@ -153,14 +153,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the Isabelle
- simplifier. Due to the interpretation of theorems
- as code equations, rewrites are applied to the right
- hand side and the arguments of the left hand side of an
- equation, but never to the constant heading the left hand side.
- An important special case are \emph{inline theorems} which may be
- declared and undeclared using the
- \emph{code inline} or \emph{code inline del} attribute respectively.
+ The \emph{simpset} allows to employ the full generality of the
+ Isabelle simplifier. Due to the interpretation of theorems as code
+ equations, rewrites are applied to the right hand side and the
+ arguments of the left hand side of an equation, but never to the
+ constant heading the left hand side. An important special case are
+ \emph{unfold theorems} which may be declared and undeclared using
+ the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
+ attribute respectively.
Some common applications:
*}
@@ -173,21 +173,21 @@
\item replacing non-executable constructs by executable ones:
*}
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
"x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
text {*
\item eliminating superfluous constants:
*}
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
"1 = Suc 0" by simp
text {*
\item replacing executable but inconvenient constructs:
*}
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
"xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
text_raw {*
@@ -210,10 +210,10 @@
on code equations.
\begin{warn}
- The attribute \emph{code unfold}
- associated with the @{text "SML code generator"} also applies to
- the @{text "generic code generator"}:
- \emph{code unfold} implies \emph{code inline}.
+
+ Attribute @{attribute code_unfold} also applies to the
+ preprocessor of the ancient @{text "SML code generator"}; in case
+ this is not what you intend, use @{attribute code_inline} instead.
\end{warn}
*}
--- a/doc-src/Codegen/Thy/document/ML.tex Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/document/ML.tex Tue Jul 14 21:19:34 2009 -0400
@@ -124,8 +124,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
- \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
+ \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
\end{mldecls}
\begin{description}
@@ -133,11 +132,6 @@
\item \verb|Code.read_const|~\isa{thy}~\isa{s}
reads a constant as a concrete term expression \isa{s}.
- \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
- rewrites a code equation \isa{thm} with a simpset \isa{ss};
- only arguments and right hand side are rewritten,
- not the head of the code equation.
-
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Program.tex Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/document/Program.tex Tue Jul 14 21:19:34 2009 -0400
@@ -395,14 +395,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the Isabelle
- simplifier. Due to the interpretation of theorems
- as code equations, rewrites are applied to the right
- hand side and the arguments of the left hand side of an
- equation, but never to the constant heading the left hand side.
- An important special case are \emph{inline theorems} which may be
- declared and undeclared using the
- \emph{code inline} or \emph{code inline del} attribute respectively.
+ The \emph{simpset} allows to employ the full generality of the
+ Isabelle simplifier. Due to the interpretation of theorems as code
+ equations, rewrites are applied to the right hand side and the
+ arguments of the left hand side of an equation, but never to the
+ constant heading the left hand side. An important special case are
+ \emph{unfold theorems} which may be declared and undeclared using
+ the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
+ attribute respectively.
Some common applications:%
\end{isamarkuptext}%
@@ -421,7 +421,7 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagquote
@@ -442,7 +442,7 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisatagquote
@@ -463,7 +463,7 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagquote
@@ -491,10 +491,10 @@
on code equations.
\begin{warn}
- The attribute \emph{code unfold}
- associated with the \isa{SML\ code\ generator} also applies to
- the \isa{generic\ code\ generator}:
- \emph{code unfold} implies \emph{code inline}.
+
+ Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
+ preprocessor of the ancient \isa{SML\ code\ generator}; in case
+ this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jul 14 21:19:34 2009 -0400
@@ -1190,7 +1190,13 @@
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
- 'code' ( 'inline' ) ? ( 'del' ) ?
+ 'code' ( 'del' ) ?
+ ;
+
+ 'code_unfold' ( 'del' ) ?
+ ;
+
+ 'code_post' ( 'del' ) ?
;
\end{rail}
@@ -1280,11 +1286,15 @@
generation. Usually packages introducing code equations provide
a reasonable default setup for selection.
- \item @{attribute (HOL) code}~@{text inline} declares (or with
+ \item @{attribute (HOL) code_inline} declares (or with
option ``@{text "del"}'' removes) inlining theorems which are
applied as rewrite rules to any code equation during
preprocessing.
+ \item @{attribute (HOL) code_post} declares (or with
+ option ``@{text "del"}'' removes) theorems which are
+ applied as rewrite rules to any result of an evaluation.
+
\item @{command (HOL) "print_codesetup"} gives an overview on
selected code equations and code generator datatypes.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jul 14 21:19:34 2009 -0400
@@ -1201,7 +1201,13 @@
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
- 'code' ( 'inline' ) ? ( 'del' ) ?
+ 'code' ( 'del' ) ?
+ ;
+
+ 'code_unfold' ( 'del' ) ?
+ ;
+
+ 'code_post' ( 'del' ) ?
;
\end{rail}
@@ -1288,11 +1294,15 @@
generation. Usually packages introducing code equations provide
a reasonable default setup for selection.
- \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
+ \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
applied as rewrite rules to any code equation during
preprocessing.
+ \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
+ option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
+ applied as rewrite rules to any result of an evaluation.
+
\item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
selected code equations and code generator datatypes.
--- a/src/HOL/Code_Eval.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Code_Eval.thy Tue Jul 14 21:19:34 2009 -0400
@@ -32,7 +32,7 @@
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
-lemma valapp_code [code, code inline]:
+lemma valapp_code [code, code_inline]:
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
by (simp only: valapp_def fst_conv snd_conv)
--- a/src/HOL/Code_Numeral.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Code_Numeral.thy Tue Jul 14 21:19:34 2009 -0400
@@ -176,16 +176,16 @@
end
-lemma zero_code_numeral_code [code inline, code]:
+lemma zero_code_numeral_code [code_inline, code]:
"(0\<Colon>code_numeral) = Numeral0"
by (simp add: number_of_code_numeral_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
+lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
using zero_code_numeral_code ..
-lemma one_code_numeral_code [code inline, code]:
+lemma one_code_numeral_code [code_inline, code]:
"(1\<Colon>code_numeral) = Numeral1"
by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
+lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
using one_code_numeral_code ..
lemma plus_code_numeral_code [code nbe]:
--- a/src/HOL/Divides.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Divides.thy Tue Jul 14 21:19:34 2009 -0400
@@ -131,7 +131,7 @@
note that ultimately show thesis by blast
qed
-lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code_unfold]: "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
--- a/src/HOL/Fact.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Fact.thy Tue Jul 14 21:19:34 2009 -0400
@@ -261,7 +261,7 @@
by (cases m) auto
-subsection {* fact and of_nat *}
+subsection {* @{term fact} and @{term of_nat} *}
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
by auto
--- a/src/HOL/Finite_Set.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Finite_Set.thy Tue Jul 14 21:19:34 2009 -0400
@@ -218,6 +218,12 @@
"\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
by (induct rule:finite_induct) simp_all
+lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)"
+by (blast intro: Inter_lower finite_subset)
+
+lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)"
+by (blast intro: INT_lower finite_subset)
+
lemma finite_empty_induct:
assumes "finite A"
and "P A"
@@ -784,6 +790,62 @@
end
+context ab_semigroup_idem_mult
+begin
+
+lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
+apply unfold_locales
+ apply (simp add: mult_ac)
+apply (simp add: mult_idem mult_assoc[symmetric])
+done
+
+end
+
+context lower_semilattice
+begin
+
+lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+proof qed (rule inf_assoc inf_commute inf_idem)+
+
+lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
+by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
+
+lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
+by (induct pred:finite) auto
+
+lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
+proof(induct arbitrary: a pred:finite)
+ case empty thus ?case by simp
+next
+ case (insert x A)
+ show ?case
+ proof cases
+ assume "A = {}" thus ?thesis using insert by simp
+ next
+ assume "A \<noteq> {}" thus ?thesis using insert by auto
+ qed
+qed
+
+end
+
+context upper_semilattice
+begin
+
+lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
+
+lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
+by(rule lower_semilattice.fold_inf_insert)(rule dual_semilattice)
+
+lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
+by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice)
+
+lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
+by(rule lower_semilattice.fold_inf_le_inf)(rule dual_semilattice)
+
+end
+
+
subsubsection{* The derived combinator @{text fold_image} *}
definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
@@ -801,7 +863,7 @@
proof -
interpret I: fun_left_comm "%x y. (g x) * y"
by unfold_locales (simp add: mult_ac)
- show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
+ show ?thesis using assms by(simp add:fold_image_def)
qed
(*
@@ -829,10 +891,7 @@
lemma fold_image_reindex:
assumes fin: "finite A"
shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
-using fin apply induct
- apply simp
-apply simp
-done
+using fin by induct auto
(*
text{*
@@ -2351,14 +2410,15 @@
shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
by(fastsimp simp:surj_def dest!: endo_inj_surj)
-corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
+corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
proof
assume "finite(UNIV::nat set)"
with finite_UNIV_inj_surj[of Suc]
show False by simp (blast dest: Suc_neq_Zero surjD)
qed
-lemma infinite_UNIV_char_0:
+(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
+lemma infinite_UNIV_char_0[noatp]:
"\<not> finite (UNIV::'a::semiring_char_0 set)"
proof
assume "finite (UNIV::'a set)"
@@ -2499,13 +2559,6 @@
context ab_semigroup_idem_mult
begin
-lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
-apply unfold_locales
- apply (simp add: mult_ac)
-apply (simp add: mult_idem mult_assoc[symmetric])
-done
-
-
lemma fold1_insert_idem [simp]:
assumes nonempty: "A \<noteq> {}" and A: "finite A"
shows "fold1 times (insert x A) = x * fold1 times A"
@@ -2667,10 +2720,6 @@
context lower_semilattice
begin
-lemma ab_semigroup_idem_mult_inf:
- "ab_semigroup_idem_mult inf"
- proof qed (rule inf_assoc inf_commute inf_idem)+
-
lemma below_fold1_iff:
assumes "finite A" "A \<noteq> {}"
shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
@@ -2716,11 +2765,6 @@
end
-lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
- "ab_semigroup_idem_mult sup"
- by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
- (rule dual_lattice)
-
context lattice
begin
@@ -2741,7 +2785,7 @@
apply(erule exE)
apply(rule order_trans)
apply(erule (1) fold1_belowI)
-apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
+apply(erule (1) lower_semilattice.fold1_belowI [OF dual_semilattice])
done
lemma sup_Inf_absorb [simp]:
@@ -2753,7 +2797,7 @@
lemma inf_Sup_absorb [simp]:
"finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
by (simp add: Sup_fin_def inf_absorb1
- lower_semilattice.fold1_belowI [OF dual_lattice])
+ lower_semilattice.fold1_belowI [OF dual_semilattice])
end
--- a/src/HOL/GCD.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/GCD.thy Tue Jul 14 21:19:34 2009 -0400
@@ -37,7 +37,7 @@
subsection {* gcd *}
-class gcd = one +
+class gcd = zero + one + dvd +
fixes
gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
@@ -540,15 +540,15 @@
(* to do: add the three variations of these, and for ints? *)
-lemma finite_divisors_nat:
- assumes "(m::nat)~= 0" shows "finite{d. d dvd m}"
+lemma finite_divisors_nat[simp]:
+ assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
proof-
have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
from finite_subset[OF _ this] show ?thesis using assms
by(bestsimp intro!:dvd_imp_le)
qed
-lemma finite_divisors_int:
+lemma finite_divisors_int[simp]:
assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
proof-
have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
@@ -557,10 +557,25 @@
by(bestsimp intro!:dvd_imp_le_int)
qed
+lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
+apply(rule antisym)
+ apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
+apply simp
+done
+
+lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
+apply(rule antisym)
+ apply(rule Max_le_iff[THEN iffD2])
+ apply simp
+ apply fastsimp
+ apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
+apply simp
+done
+
lemma gcd_is_Max_divisors_nat:
"m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
apply(rule Max_eqI[THEN sym])
- apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
+ apply (metis finite_Collect_conjI finite_divisors_nat)
apply simp
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
apply simp
@@ -569,7 +584,7 @@
lemma gcd_is_Max_divisors_int:
"m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
apply(rule Max_eqI[THEN sym])
- apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
+ apply (metis finite_Collect_conjI finite_divisors_int)
apply simp
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
apply simp
@@ -1442,31 +1457,61 @@
lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
+lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
+by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
+
+lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
+by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
+
+lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
+by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
+
+lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
+by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
-apply(rule lcm_unique_nat[THEN iffD1])
-apply (metis dvd.order_trans lcm_unique_nat)
-done
+by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
-apply(rule lcm_unique_int[THEN iffD1])
-apply (metis dvd_trans lcm_unique_int)
-done
+by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
-lemmas lcm_left_commute_nat =
- mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
-
-lemmas lcm_left_commute_int =
- mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
+lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
+lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
+lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
+proof qed (auto simp add: gcd_ac_nat)
+
+lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
+proof qed (auto simp add: gcd_ac_int)
+
+lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
+proof qed (auto simp add: lcm_ac_nat)
+
+lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
+proof qed (auto simp add: lcm_ac_int)
+
+
+(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
+
+lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
+
+lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
+
+lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
+by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
+
+lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
+by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
+
subsection {* Primes *}
-(* Is there a better way to handle these, rather than making them
- elim rules? *)
+(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
by (unfold prime_nat_def, auto)
@@ -1490,7 +1535,7 @@
by (unfold prime_nat_def, auto)
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
- by (unfold prime_int_def prime_nat_def, auto)
+ by (unfold prime_int_def prime_nat_def) auto
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
by (unfold prime_int_def prime_nat_def, auto)
@@ -1504,8 +1549,6 @@
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
by (unfold prime_int_def prime_nat_def, auto)
-thm prime_nat_def;
-thm prime_nat_def [transferred];
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
m = 1 \<or> m = p))"
@@ -1566,35 +1609,13 @@
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_nat_def dvd_def apply auto
- apply (subgoal_tac "k > 1")
- apply force
- apply (subgoal_tac "k ~= 0")
- apply force
- apply (rule notI)
- apply force
-done
+ by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
-(* there's a lot of messing around with signs of products here --
- could this be made more automatic? *)
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_int_altdef dvd_def
apply auto
- apply (rule_tac x = m in exI)
- apply (rule_tac x = k in exI)
- apply (auto simp add: mult_compare_simps)
- apply (subgoal_tac "k > 0")
- apply arith
- apply (case_tac "k <= 0")
- apply (subgoal_tac "m * k <= 0")
- apply force
- apply (subst zero_compare_simps(8))
- apply auto
- apply (subgoal_tac "m * k <= 0")
- apply force
- apply (subst zero_compare_simps(8))
- apply auto
-done
+ by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
n > 0 --> (p dvd x^n --> p dvd x)"
--- a/src/HOL/HOL.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/HOL.thy Tue Jul 14 21:19:34 2009 -0400
@@ -1787,7 +1787,7 @@
assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
begin
-lemma eq [code unfold, code inline del]: "eq = (op =)"
+lemma eq [code_unfold, code_inline del]: "eq = (op =)"
by (rule ext eq_equals)+
lemma eq_refl: "eq x x \<longleftrightarrow> True"
@@ -1796,7 +1796,7 @@
lemma equals_eq: "(op =) \<equiv> eq"
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
-declare equals_eq [symmetric, code post]
+declare equals_eq [symmetric, code_post]
end
@@ -1847,7 +1847,7 @@
lemmas [code] = Let_def if_True if_False
-lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
+lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
instantiation itself :: (type) eq
begin
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 21:19:34 2009 -0400
@@ -283,7 +283,7 @@
where
[code del]: "raise_exc e = raise []"
-lemma raise_raise_exc [code, 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/Int.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Int.thy Tue Jul 14 21:19:34 2009 -0400
@@ -650,11 +650,11 @@
text {* Removal of leading zeroes *}
-lemma Bit0_Pls [simp, code post]:
+lemma Bit0_Pls [simp, code_post]:
"Bit0 Pls = Pls"
unfolding numeral_simps by simp
-lemma Bit1_Min [simp, code post]:
+lemma Bit1_Min [simp, code_post]:
"Bit1 Min = Min"
unfolding numeral_simps by simp
@@ -2126,11 +2126,11 @@
hide (open) const nat_aux
-lemma zero_is_num_zero [code, 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, 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 Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/IntDiv.thy Tue Jul 14 21:19:34 2009 -0400
@@ -36,7 +36,7 @@
text{*algorithm for the general case @{term "b\<noteq>0"}*}
definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
- [code inline]: "negateSnd = apsnd uminus"
+ [code_inline]: "negateSnd = apsnd uminus"
definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--{*The full division algorithm considers all possible signs for a, b
--- a/src/HOL/Lattices.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Lattices.thy Tue Jul 14 21:19:34 2009 -0400
@@ -29,7 +29,7 @@
text {* Dual lattice *}
-lemma dual_lattice:
+lemma dual_semilattice:
"lower_semilattice (op \<ge>) (op >) sup"
by (rule lower_semilattice.intro, rule dual_order)
(unfold_locales, simp_all add: sup_least)
@@ -180,6 +180,11 @@
context lattice
begin
+lemma dual_lattice:
+ "lattice (op \<ge>) (op >) sup inf"
+ by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order)
+ (unfold_locales, auto)
+
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
@@ -252,12 +257,148 @@
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
by(simp add:ACI inf_sup_distrib1)
+lemma dual_distrib_lattice:
+ "distrib_lattice (op \<ge>) (op >) sup inf"
+ by (rule distrib_lattice.intro, rule dual_lattice)
+ (unfold_locales, fact inf_sup_distrib1)
+
lemmas distrib =
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
end
+subsection {* Boolean algebras *}
+
+class boolean_algebra = distrib_lattice + top + bot + minus + uminus +
+ assumes inf_compl_bot: "x \<sqinter> - x = bot"
+ and sup_compl_top: "x \<squnion> - x = top"
+ assumes diff_eq: "x - y = x \<sqinter> - y"
+begin
+
+lemma dual_boolean_algebra:
+ "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot"
+ by (rule boolean_algebra.intro, rule dual_distrib_lattice)
+ (unfold_locales,
+ auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le)
+
+lemma compl_inf_bot:
+ "- x \<sqinter> x = bot"
+ by (simp add: inf_commute inf_compl_bot)
+
+lemma compl_sup_top:
+ "- x \<squnion> x = top"
+ by (simp add: sup_commute sup_compl_top)
+
+lemma inf_bot_left [simp]:
+ "bot \<sqinter> x = bot"
+ by (rule inf_absorb1) simp
+
+lemma inf_bot_right [simp]:
+ "x \<sqinter> bot = bot"
+ by (rule inf_absorb2) simp
+
+lemma sup_top_left [simp]:
+ "top \<squnion> x = top"
+ by (rule sup_absorb1) simp
+
+lemma sup_top_right [simp]:
+ "x \<squnion> top = top"
+ by (rule sup_absorb2) simp
+
+lemma inf_top_left [simp]:
+ "top \<sqinter> x = x"
+ by (rule inf_absorb2) simp
+
+lemma inf_top_right [simp]:
+ "x \<sqinter> top = x"
+ by (rule inf_absorb1) simp
+
+lemma sup_bot_left [simp]:
+ "bot \<squnion> x = x"
+ by (rule sup_absorb2) simp
+
+lemma sup_bot_right [simp]:
+ "x \<squnion> bot = x"
+ by (rule sup_absorb1) simp
+
+lemma compl_unique:
+ assumes "x \<sqinter> y = bot"
+ and "x \<squnion> y = top"
+ shows "- x = y"
+proof -
+ have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
+ using inf_compl_bot assms(1) by simp
+ then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
+ by (simp add: inf_commute)
+ then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
+ by (simp add: inf_sup_distrib1)
+ then have "- x \<sqinter> top = y \<sqinter> top"
+ using sup_compl_top assms(2) by simp
+ then show "- x = y" by (simp add: inf_top_right)
+qed
+
+lemma double_compl [simp]:
+ "- (- x) = x"
+ using compl_inf_bot compl_sup_top by (rule compl_unique)
+
+lemma compl_eq_compl_iff [simp]:
+ "- x = - y \<longleftrightarrow> x = y"
+proof
+ assume "- x = - y"
+ then have "- x \<sqinter> y = bot"
+ and "- x \<squnion> y = top"
+ by (simp_all add: compl_inf_bot compl_sup_top)
+ then have "- (- x) = y" by (rule compl_unique)
+ then show "x = y" by simp
+next
+ assume "x = y"
+ then show "- x = - y" by simp
+qed
+
+lemma compl_bot_eq [simp]:
+ "- bot = top"
+proof -
+ from sup_compl_top have "bot \<squnion> - bot = top" .
+ then show ?thesis by simp
+qed
+
+lemma compl_top_eq [simp]:
+ "- top = bot"
+proof -
+ from inf_compl_bot have "top \<sqinter> - top = bot" .
+ then show ?thesis by simp
+qed
+
+lemma compl_inf [simp]:
+ "- (x \<sqinter> y) = - x \<squnion> - y"
+proof (rule compl_unique)
+ have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)"
+ by (rule inf_sup_distrib1)
+ also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
+ by (simp only: inf_commute inf_assoc inf_left_commute)
+ finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = bot"
+ by (simp add: inf_compl_bot)
+next
+ have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
+ by (rule sup_inf_distrib2)
+ also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
+ by (simp only: sup_commute sup_assoc sup_left_commute)
+ finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = top"
+ by (simp add: sup_compl_top)
+qed
+
+lemma compl_sup [simp]:
+ "- (x \<squnion> y) = - x \<sqinter> - y"
+proof -
+ interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
+ by (rule dual_boolean_algebra)
+ then show ?thesis by simp
+qed
+
+end
+
+
subsection {* Uniqueness of inf and sup *}
lemma (in lower_semilattice) inf_unique:
@@ -330,17 +471,24 @@
subsection {* Bool as lattice *}
-instantiation bool :: distrib_lattice
+instantiation bool :: boolean_algebra
begin
definition
+ bool_Compl_def: "uminus = Not"
+
+definition
+ bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
+
+definition
inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
definition
sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
-instance
- by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
+instance proof
+qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def
+ bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto)
end
@@ -369,7 +517,33 @@
end
instance "fun" :: (type, distrib_lattice) distrib_lattice
- by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
+proof
+qed (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
+
+instantiation "fun" :: (type, uminus) uminus
+begin
+
+definition
+ fun_Compl_def: "- A = (\<lambda>x. - A x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, minus) minus
+begin
+
+definition
+ fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
+
+instance ..
+
+end
+
+instance "fun" :: (type, boolean_algebra) boolean_algebra
+proof
+qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def
+ inf_compl_bot sup_compl_top diff_eq)
text {* redundant bindings *}
--- a/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 21:19:34 2009 -0400
@@ -24,11 +24,11 @@
lemmas [code del] = char.recs char.cases char.size
-lemma [code, 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, 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)
--- a/src/HOL/Library/Countable.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Countable.thy Tue Jul 14 21:19:34 2009 -0400
@@ -58,7 +58,7 @@
subclass (in finite) countable
proof
have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
- with finite_conv_nat_seg_image [of UNIV]
+ with finite_conv_nat_seg_image [of "UNIV::'a set"]
obtain n and f :: "nat \<Rightarrow> 'a"
where "UNIV = f ` {i. i < n}" by auto
then have "surj f" unfolding surj_def by auto
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 21:19:34 2009 -0400
@@ -26,15 +26,15 @@
code_datatype number_nat_inst.number_of_nat
-lemma zero_nat_code [code, code inline]:
+lemma zero_nat_code [code, code_inline]:
"0 = (Numeral0 :: nat)"
by simp
-lemmas [code post] = zero_nat_code [symmetric]
+lemmas [code_post] = zero_nat_code [symmetric]
-lemma one_nat_code [code, code inline]:
+lemma one_nat_code [code, code_inline]:
"1 = (Numeral1 :: nat)"
by simp
-lemmas [code post] = one_nat_code [symmetric]
+lemmas [code_post] = one_nat_code [symmetric]
lemma Suc_code [code]:
"Suc n = n + 1"
@@ -89,7 +89,7 @@
expression:
*}
-lemma [code, code unfold]:
+lemma [code, code_unfold]:
"nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
@@ -302,7 +302,7 @@
Natural numerals.
*}
-lemma [code inline, symmetric, code post]:
+lemma [code_inline, symmetric, code_post]:
"nat (number_of i) = number_nat_inst.number_of_nat i"
-- {* this interacts as desired with @{thm nat_number_of_def} *}
by (simp add: number_nat_inst.number_of_nat)
@@ -335,9 +335,9 @@
"nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
unfolding nat_number_of_def number_of_is_id neg_def by simp
-lemma of_nat_int [code unfold]:
+lemma of_nat_int [code_unfold]:
"of_nat = int" by (simp add: int_def)
-declare of_nat_int [symmetric, code post]
+declare of_nat_int [symmetric, code_post]
code_const int
(SML "_")
--- a/src/HOL/Library/Executable_Set.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Executable_Set.thy Tue Jul 14 21:19:34 2009 -0400
@@ -15,7 +15,7 @@
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
"subset = op \<le>"
-declare subset_def [symmetric, code unfold]
+declare subset_def [symmetric, code_unfold]
lemma [code]:
"subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
@@ -25,7 +25,7 @@
[code del]: "eq_set = op ="
(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code unfold]
+declare set_eq_subset[code_unfold]
*)
lemma [code]:
@@ -40,7 +40,7 @@
subsection {* Rewrites for primitive operations *}
-declare List_Set.project_def [symmetric, code unfold]
+declare List_Set.project_def [symmetric, code_unfold]
subsection {* code generator setup *}
--- a/src/HOL/Library/Float.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Float.thy Tue Jul 14 21:19:34 2009 -0400
@@ -19,7 +19,7 @@
"of_float (Float a b) = real a * pow2 b"
defs (overloaded)
- real_of_float_def [code unfold]: "real == of_float"
+ real_of_float_def [code_unfold]: "real == of_float"
primrec mantissa :: "float \<Rightarrow> int" where
"mantissa (Float a b) = a"
@@ -42,7 +42,7 @@
instance ..
end
-lemma number_of_float_Float [code inline, symmetric, code post]:
+lemma number_of_float_Float [code_inline, symmetric, code_post]:
"number_of k = Float (number_of k) 0"
by (simp add: number_of_float_def number_of_is_id)
--- a/src/HOL/Library/Fraction_Field.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Fraction_Field.thy Tue Jul 14 21:19:34 2009 -0400
@@ -93,10 +93,10 @@
begin
definition
- Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
+ Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
definition
- One_fract_def [code, code unfold]: "1 = Fract 1 1"
+ One_fract_def [code, code_unfold]: "1 = Fract 1 1"
definition
add_fract_def [code del]:
@@ -196,14 +196,14 @@
lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
by (rule of_nat_fract [symmetric])
-lemma fract_collapse [code post]:
+lemma fract_collapse [code_post]:
"Fract 0 k = 0"
"Fract 1 1 = 1"
"Fract k 0 = 0"
by (cases "k = 0")
(simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
-lemma fract_expand [code unfold]:
+lemma fract_expand [code_unfold]:
"0 = Fract 0 1"
"1 = Fract 1 1"
by (simp_all add: fract_collapse)
--- a/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 21:19:34 2009 -0400
@@ -40,10 +40,10 @@
"0 = Fin 0"
definition
- [code inline]: "1 = Fin 1"
+ [code_inline]: "1 = Fin 1"
definition
- [code inline, code del]: "number_of k = Fin (number_of k)"
+ [code_inline, code del]: "number_of k = Fin (number_of k)"
instance ..
--- a/src/HOL/Library/Polynomial.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Polynomial.thy Tue Jul 14 21:19:34 2009 -0400
@@ -1505,7 +1505,7 @@
code_datatype "0::'a::zero poly" pCons
-declare pCons_0_0 [code post]
+declare pCons_0_0 [code_post]
instantiation poly :: ("{zero,eq}") eq
begin
--- a/src/HOL/List.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/List.thy Tue Jul 14 21:19:34 2009 -0400
@@ -2076,7 +2076,7 @@
by(induct xs) simp_all
text{* For efficient code generation: avoid intermediate list. *}
-lemma foldl_map[code unfold]:
+lemma foldl_map[code_unfold]:
"foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
by(induct xs arbitrary:a) simp_all
@@ -2198,7 +2198,7 @@
text{* For efficient code generation ---
@{const listsum} is not tail recursive but @{const foldl} is. *}
-lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
+lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
by(simp add:listsum_foldr foldl_foldr1)
lemma distinct_listsum_conv_Setsum:
@@ -3746,32 +3746,32 @@
show ?case by (induct xs) (auto simp add: Cons aux)
qed
-lemma mem_iff [code post]:
+lemma mem_iff [code_post]:
"x mem xs \<longleftrightarrow> x \<in> set xs"
by (induct xs) auto
-lemmas in_set_code [code unfold] = mem_iff [symmetric]
+lemmas in_set_code [code_unfold] = mem_iff [symmetric]
lemma empty_null:
"xs = [] \<longleftrightarrow> null xs"
by (cases xs) simp_all
-lemma [code inline]:
+lemma [code_inline]:
"eq_class.eq xs [] \<longleftrightarrow> null xs"
by (simp add: eq empty_null)
-lemmas null_empty [code post] =
+lemmas null_empty [code_post] =
empty_null [symmetric]
lemma list_inter_conv:
"set (list_inter xs ys) = set xs \<inter> set ys"
by (induct xs) auto
-lemma list_all_iff [code post]:
+lemma list_all_iff [code_post]:
"list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
by (induct xs) auto
-lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
+lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
lemma list_all_append [simp]:
"list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
@@ -3785,11 +3785,11 @@
"list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
-lemma list_ex_iff [code post]:
+lemma list_ex_iff [code_post]:
"list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
by (induct xs) simp_all
-lemmas list_bex_code [code unfold] =
+lemmas list_bex_code [code_unfold] =
list_ex_iff [symmetric]
lemma list_ex_length:
@@ -3804,7 +3804,7 @@
"map_filter f P xs = map f (filter P xs)"
by (induct xs) auto
-lemma length_remdups_length_unique [code inline]:
+lemma length_remdups_length_unique [code_inline]:
"length (remdups xs) = length_unique xs"
by (induct xs) simp_all
@@ -3813,43 +3813,43 @@
text {* Code for bounded quantification and summation over nats. *}
-lemma atMost_upto [code unfold]:
+lemma atMost_upto [code_unfold]:
"{..n} = set [0..<Suc n]"
by auto
-lemma atLeast_upt [code unfold]:
+lemma atLeast_upt [code_unfold]:
"{..<n} = set [0..<n]"
by auto
-lemma greaterThanLessThan_upt [code unfold]:
+lemma greaterThanLessThan_upt [code_unfold]:
"{n<..<m} = set [Suc n..<m]"
by auto
-lemma atLeastLessThan_upt [code unfold]:
+lemma atLeastLessThan_upt [code_unfold]:
"{n..<m} = set [n..<m]"
by auto
-lemma greaterThanAtMost_upt [code unfold]:
+lemma greaterThanAtMost_upt [code_unfold]:
"{n<..m} = set [Suc n..<Suc m]"
by auto
-lemma atLeastAtMost_upt [code unfold]:
+lemma atLeastAtMost_upt [code_unfold]:
"{n..m} = set [n..<Suc m]"
by auto
-lemma all_nat_less_eq [code unfold]:
+lemma all_nat_less_eq [code_unfold]:
"(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
by auto
-lemma ex_nat_less_eq [code unfold]:
+lemma ex_nat_less_eq [code_unfold]:
"(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
by auto
-lemma all_nat_less [code unfold]:
+lemma all_nat_less [code_unfold]:
"(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
by auto
-lemma ex_nat_less [code unfold]:
+lemma ex_nat_less [code_unfold]:
"(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
by auto
@@ -3857,30 +3857,30 @@
"distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
by (induct xs) simp_all
-lemma setsum_set_upt_conv_listsum [code unfold]:
+lemma setsum_set_upt_conv_listsum [code_unfold]:
"setsum f (set [m..<n]) = listsum (map f [m..<n])"
by (rule setsum_set_distinct_conv_listsum) simp
text {* Code for summation over ints. *}
-lemma greaterThanLessThan_upto [code unfold]:
+lemma greaterThanLessThan_upto [code_unfold]:
"{i<..<j::int} = set [i+1..j - 1]"
by auto
-lemma atLeastLessThan_upto [code unfold]:
+lemma atLeastLessThan_upto [code_unfold]:
"{i..<j::int} = set [i..j - 1]"
by auto
-lemma greaterThanAtMost_upto [code unfold]:
+lemma greaterThanAtMost_upto [code_unfold]:
"{i<..j::int} = set [i+1..j]"
by auto
-lemma atLeastAtMost_upto [code unfold]:
+lemma atLeastAtMost_upto [code_unfold]:
"{i..j::int} = set [i..j]"
by auto
-lemma setsum_set_upto_conv_listsum [code unfold]:
+lemma setsum_set_upto_conv_listsum [code_unfold]:
"setsum f (set [i..j::int]) = listsum (map f [i..j])"
by (rule setsum_set_distinct_conv_listsum) simp
--- a/src/HOL/MicroJava/BV/BVExample.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Jul 14 21:19:34 2009 -0400
@@ -467,7 +467,7 @@
lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
-lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
+lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
code_module BV
contains
--- a/src/HOL/Nat.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Nat.thy Tue Jul 14 21:19:34 2009 -0400
@@ -1200,9 +1200,9 @@
text {* for code generation *}
definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
- funpow_code_def [code post]: "funpow = compow"
+ funpow_code_def [code_post]: "funpow = compow"
-lemmas [code unfold] = funpow_code_def [symmetric]
+lemmas [code_unfold] = funpow_code_def [symmetric]
lemma [code]:
"funpow 0 f = id"
@@ -1265,7 +1265,7 @@
end
-declare of_nat_code [code, code unfold, code inline del]
+declare of_nat_code [code, code_unfold, code_inline del]
text{*Class for unital semirings with characteristic zero.
Includes non-ordered rings like the complex numbers.*}
--- a/src/HOL/Nat_Numeral.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Nat_Numeral.thy Tue Jul 14 21:19:34 2009 -0400
@@ -20,13 +20,13 @@
begin
definition
- nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
+ nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
instance ..
end
-lemma [code post]:
+lemma [code_post]:
"nat (number_of v) = number_of v"
unfolding nat_number_of_def ..
@@ -316,13 +316,13 @@
lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
by (simp add: nat_number_of_def)
-lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
+lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
by (simp add: nat_number_of_def)
lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
by (simp add: nat_1 nat_number_of_def)
-lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
+lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
by (simp add: nat_numeral_1_eq_1)
--- a/src/HOL/Option.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Option.thy Tue Jul 14 21:19:34 2009 -0400
@@ -94,7 +94,7 @@
subsubsection {* Code generator setup *}
definition is_none :: "'a option \<Rightarrow> bool" where
- [code post]: "is_none x \<longleftrightarrow> x = None"
+ [code_post]: "is_none x \<longleftrightarrow> x = None"
lemma is_none_code [code]:
shows "is_none None \<longleftrightarrow> True"
@@ -105,7 +105,7 @@
"is_none x \<longleftrightarrow> x = None"
by (simp add: is_none_def)
-lemma [code inline]:
+lemma [code_inline]:
"eq_class.eq x None \<longleftrightarrow> is_none x"
by (simp add: eq is_none_none)
--- a/src/HOL/Orderings.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Orderings.thy Tue Jul 14 21:19:34 2009 -0400
@@ -268,13 +268,13 @@
text {* Explicit dictionaries for code generation *}
-lemma min_ord_min [code, code unfold, code inline del]:
+lemma min_ord_min [code, code_unfold, code_inline del]:
"min = ord.min (op \<le>)"
by (rule ext)+ (simp add: min_def ord.min_def)
declare ord.min_def [code]
-lemma max_ord_max [code, code unfold, code inline del]:
+lemma max_ord_max [code, code_unfold, code_inline del]:
"max = ord.max (op \<le>)"
by (rule ext)+ (simp add: max_def ord.max_def)
--- a/src/HOL/Power.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Power.thy Tue Jul 14 21:19:34 2009 -0400
@@ -455,7 +455,7 @@
subsection {* Code generator tweak *}
-lemma power_power_power [code, code unfold, code inline del]:
+lemma power_power_power [code, code_unfold, code_inline del]:
"power = power.power (1::'a::{power}) (op *)"
unfolding power_def power.power_def ..
--- a/src/HOL/Rational.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Rational.thy Tue Jul 14 21:19:34 2009 -0400
@@ -93,10 +93,10 @@
begin
definition
- Zero_rat_def [code, code unfold]: "0 = Fract 0 1"
+ Zero_rat_def [code, code_unfold]: "0 = Fract 0 1"
definition
- One_rat_def [code, code unfold]: "1 = Fract 1 1"
+ One_rat_def [code, code_unfold]: "1 = Fract 1 1"
definition
add_rat_def [code del]:
@@ -211,7 +211,7 @@
end
-lemma rat_number_collapse [code post]:
+lemma rat_number_collapse [code_post]:
"Fract 0 k = 0"
"Fract 1 1 = 1"
"Fract (number_of k) 1 = number_of k"
@@ -219,7 +219,7 @@
by (cases "k = 0")
(simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
-lemma rat_number_expand [code unfold]:
+lemma rat_number_expand [code_unfold]:
"0 = Fract 0 1"
"1 = Fract 1 1"
"number_of k = Fract (number_of k) 1"
@@ -291,11 +291,11 @@
lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
by (simp add: Fract_of_int_eq [symmetric])
-lemma Fract_number_of_quotient [code post]:
+lemma Fract_number_of_quotient [code_post]:
"Fract (number_of k) (number_of l) = number_of k / number_of l"
unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
-lemma Fract_1_number_of [code post]:
+lemma Fract_1_number_of [code_post]:
"Fract 1 (number_of k) = 1 / number_of k"
unfolding Fract_of_int_quotient number_of_eq by simp
@@ -1003,7 +1003,7 @@
definition (in term_syntax)
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+ [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/RealDef.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/RealDef.thy Tue Jul 14 21:19:34 2009 -0400
@@ -559,8 +559,8 @@
real :: "'a => real"
defs (overloaded)
- real_of_nat_def [code unfold]: "real == real_of_nat"
- real_of_int_def [code unfold]: "real == real_of_int"
+ real_of_nat_def [code_unfold]: "real == real_of_nat"
+ real_of_int_def [code_unfold]: "real == real_of_int"
lemma real_eq_of_nat: "real = of_nat"
unfolding real_of_nat_def ..
@@ -946,7 +946,7 @@
end
-lemma [code unfold, symmetric, code post]:
+lemma [code_unfold, symmetric, code_post]:
"number_of k = real_of_int (number_of k)"
unfolding number_of_is_id real_number_of_def ..
@@ -1061,29 +1061,29 @@
code_datatype Ratreal
-lemma Ratreal_number_collapse [code post]:
+lemma Ratreal_number_collapse [code_post]:
"Ratreal 0 = 0"
"Ratreal 1 = 1"
"Ratreal (number_of k) = number_of k"
by simp_all
-lemma zero_real_code [code, code unfold]:
+lemma zero_real_code [code, code_unfold]:
"0 = Ratreal 0"
by simp
-lemma one_real_code [code, code unfold]:
+lemma one_real_code [code, code_unfold]:
"1 = Ratreal 1"
by simp
-lemma number_of_real_code [code unfold]:
+lemma number_of_real_code [code_unfold]:
"number_of k = Ratreal (number_of k)"
by simp
-lemma Ratreal_number_of_quotient [code post]:
+lemma Ratreal_number_of_quotient [code_post]:
"Ratreal (number_of r) / Ratreal (number_of s) = number_of r / number_of s"
by simp
-lemma Ratreal_number_of_quotient2 [code post]:
+lemma Ratreal_number_of_quotient2 [code_post]:
"Ratreal (number_of r / number_of s) = number_of r / number_of s"
unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
@@ -1129,7 +1129,7 @@
definition (in term_syntax)
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+ [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Set.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Set.thy Tue Jul 14 21:19:34 2009 -0400
@@ -10,7 +10,6 @@
text {* A set in HOL is simply a predicate. *}
-
subsection {* Basic syntax *}
global
@@ -363,46 +362,6 @@
Bex_def: "Bex A P == EX x. x:A & P(x)"
Bex1_def: "Bex1 A P == EX! x. x:A & P(x)"
-instantiation "fun" :: (type, minus) minus
-begin
-
-definition
- fun_diff_def: "A - B = (%x. A x - B x)"
-
-instance ..
-
-end
-
-instantiation bool :: minus
-begin
-
-definition
- bool_diff_def: "A - B = (A & ~ B)"
-
-instance ..
-
-end
-
-instantiation "fun" :: (type, uminus) uminus
-begin
-
-definition
- fun_Compl_def: "- A = (%x. - A x)"
-
-instance ..
-
-end
-
-instantiation bool :: uminus
-begin
-
-definition
- bool_Compl_def: "- A = (~ A)"
-
-instance ..
-
-end
-
definition Pow :: "'a set => 'a set set" where
Pow_def: "Pow A = {B. B \<le> A}"
--- a/src/HOL/SetInterval.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/SetInterval.thy Tue Jul 14 21:19:34 2009 -0400
@@ -284,8 +284,8 @@
lemma atLeast0AtMost: "{0..n::nat} = {..n}"
by(simp add:atMost_def atLeastAtMost_def)
-declare atLeast0LessThan[symmetric, code unfold]
- atLeast0AtMost[symmetric, code unfold]
+declare atLeast0LessThan[symmetric, code_unfold]
+ atLeast0AtMost[symmetric, code_unfold]
lemma atLeastLessThan0: "{m..<0::nat} = {}"
by (simp add: atLeastLessThan_def)
--- a/src/HOL/String.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/String.thy Tue Jul 14 21:19:34 2009 -0400
@@ -58,11 +58,11 @@
end
*}
-lemma char_case_nibble_pair [code, 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, 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/Tools/inductive_codegen.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Jul 14 21:19:34 2009 -0400
@@ -697,7 +697,8 @@
val setup =
add_codegen "inductive" inductive_codegen #>
- Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
- Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
+ Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+ "introduction rules for executable predicates";
end;
--- a/src/HOL/Tools/inductive_set.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Tools/inductive_set.ML Tue Jul 14 21:19:34 2009 -0400
@@ -541,8 +541,9 @@
"declare rules for converting between predicate and set notation" #>
Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
- Code.add_attribute ("ind_set",
- Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
+ Attrib.setup @{binding code_ind_set}
+ (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
+ "introduction rules for executable predicates" #>
Codegen.add_preprocessor codegen_preproc #>
Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
"declaration of monotonicity rule for set operators" #>
--- a/src/HOL/Tools/recfun_codegen.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Jul 14 21:19:34 2009 -0400
@@ -23,15 +23,13 @@
fun merge _ = Symtab.merge (K true);
);
-fun add_thm NONE thm thy = Code.add_eqn thm thy
- | add_thm (SOME module_name) thm thy =
- let
- val (thm', _) = Code.mk_eqn thy (thm, true)
- in
- thy
- |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
- |> Code.add_eqn thm'
- end;
+fun add_thm_target module_name thm thy =
+ let
+ val (thm', _) = Code.mk_eqn thy (thm, true)
+ in
+ thy
+ |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
+ end;
fun expand_eta thy [] = []
| expand_eta thy (thms as thm :: _) =
@@ -163,15 +161,8 @@
end)
| _ => NONE);
-val setup = let
- fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
- (add_thm opt_module thm) I);
- val del = Thm.declaration_attribute (fn thm => Context.mapping
- (Code.del_eqn thm) I);
-in
+val setup =
add_codegen "recfun" recfun_codegen
- #> Code.add_attribute ("", Args.del |-- Scan.succeed del
- || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
-end;
+ #> Code.set_code_target_attr add_thm_target;
end;
--- a/src/HOL/ex/Numeral.thy Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/ex/Numeral.thy Tue Jul 14 21:19:34 2009 -0400
@@ -751,14 +751,14 @@
subsection {* Code generator setup for @{typ int} *}
definition Pls :: "num \<Rightarrow> int" where
- [simp, code post]: "Pls n = of_num n"
+ [simp, code_post]: "Pls n = of_num n"
definition Mns :: "num \<Rightarrow> int" where
- [simp, code post]: "Mns n = - of_num n"
+ [simp, code_post]: "Mns n = - of_num n"
code_datatype "0::int" Pls Mns
-lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
+lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
[simp, code del]: "sub m n = (of_num m - of_num n)"
@@ -874,10 +874,10 @@
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
by (simp_all add: of_num_less_iff)
-lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
-lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
-declare zero_is_num_zero [code inline del]
-declare one_is_num_one [code inline del]
+lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
+lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
+declare zero_is_num_zero [code_inline del]
+declare one_is_num_one [code_inline del]
hide (open) const sub dup
--- a/src/Pure/Isar/code.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/Isar/code.ML Tue Jul 14 21:19:34 2009 -0400
@@ -62,7 +62,7 @@
val print_codesetup: theory -> unit
(*infrastructure*)
- val add_attribute: string * attribute parser -> theory -> theory
+ val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
val purge_data: theory -> theory
end;
@@ -235,31 +235,6 @@
end;
-(** code attributes **)
-
-structure Code_Attr = TheoryDataFun (
- type T = (string * attribute parser) list;
- val empty = [];
- val copy = I;
- val extend = I;
- fun merge _ = AList.merge (op = : string * string -> bool) (K true);
-);
-
-fun add_attribute (attr as (name, _)) =
- let
- fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
- | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
- in Code_Attr.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 _ = Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "code")
- (Scan.peek (fn context =>
- List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
- "declare theorems for code generation"));
-
-
(** data store **)
(* code equations *)
@@ -543,7 +518,7 @@
in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
let
- val _ = if tyco' <> tyco
+ val _ = if (tyco' : string) <> tyco
then error "Different type constructors in constructor set"
else ();
val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
@@ -911,18 +886,32 @@
of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
| NONE => thy;
+structure Code_Attr = TheoryDataFun (
+ type T = (string -> thm -> theory -> theory) option;
+ val empty = NONE;
+ val copy = I;
+ val extend = I;
+ fun merge _ (NONE, f2) = f2
+ | merge _ (f1, _) = f1;
+);
+
+fun set_code_target_attr f = Code_Attr.map (K (SOME f));
+
val _ = Context.>> (Context.map_theory
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
- fun add_simple_attribute (name, f) =
- add_attribute (name, Scan.succeed (mk_attribute f));
- fun add_del_attribute (name, (add, del)) =
- add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
- || Scan.succeed (mk_attribute add))
+ val code_attribute_parser =
+ Args.del |-- Scan.succeed (mk_attribute del_eqn)
+ || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
+ || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
+ (fn prefix => mk_attribute (fn thm => fn thy => thy
+ |> add_warning_eqn thm
+ |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
+ || Scan.succeed (mk_attribute add_warning_eqn);
in
Type_Interpretation.init
- #> add_del_attribute ("", (add_warning_eqn, del_eqn))
- #> add_simple_attribute ("nbe", add_nbe_eqn)
+ #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
+ "declare theorems for code generation"
end));
--- a/src/Pure/Isar/proof_context.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/Isar/proof_context.ML Tue Jul 14 21:19:34 2009 -0400
@@ -523,16 +523,17 @@
(* patterns *)
-fun prepare_patternT ctxt =
- let val Mode {pattern, schematic, ...} = get_mode ctxt in
- if pattern orelse schematic then I
- else Term.map_atyps
- (fn T as TVar (xi, _) =>
- if not (TypeInfer.is_param xi)
- then error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
- else T
- | T => T)
- end;
+fun prepare_patternT ctxt T =
+ let
+ val Mode {pattern, schematic, ...} = get_mode ctxt;
+ val _ =
+ pattern orelse schematic orelse
+ T |> Term.exists_subtype
+ (fn TVar (xi, _) =>
+ not (TypeInfer.is_param xi) andalso
+ error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
+ | _ => false)
+ in T end;
local
--- a/src/Pure/logic.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/logic.ML Tue Jul 14 21:19:34 2009 -0400
@@ -71,9 +71,7 @@
val varify: term -> term
val unvarify: term -> term
val legacy_varifyT: typ -> typ
- val legacy_unvarifyT: typ -> typ
val legacy_varify: term -> term
- val legacy_unvarify: term -> term
val get_goal: term -> int -> term
val goal_params: term -> int -> term * term list
val prems_of_goal: term -> int -> term list
@@ -508,16 +506,11 @@
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
-val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
val legacy_varify =
Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
Term.map_types legacy_varifyT;
-val legacy_unvarify =
- Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
- Term.map_types legacy_unvarifyT;
-
(* goal states *)
--- a/src/Pure/type_infer.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/type_infer.ML Tue Jul 14 21:19:34 2009 -0400
@@ -39,7 +39,8 @@
fun is_param (x, _: int) = String.isPrefix "?" x;
fun param i (x, S) = TVar (("?" ^ x, i), S);
-val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T);
+val paramify_vars =
+ perhaps (Term_Subst.map_atypsT_option (fn TVar ((x, i), S) => SOME (param i (x, S)) | _ => NONE));
val paramify_dummies =
let
--- a/src/Tools/Code/code_preproc.ML Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Tools/Code/code_preproc.ML Tue Jul 14 21:19:34 2009 -0400
@@ -526,14 +526,16 @@
val setup =
let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
- fun add_del_attribute (name, (add, del)) =
- Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
- || Scan.succeed (mk_attribute add))
+ fun add_del_attribute_parser (add, del) =
+ Attrib.add_del (mk_attribute add) (mk_attribute del);
in
- add_del_attribute ("inline", (add_inline, del_inline))
- #> add_del_attribute ("post", (add_post, del_post))
- #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
- (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
+ Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
+ "preprocessing equations for code generator"
+ #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
+ "postprocessing equations for code generator"
+ #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
+ (fn thm => Codegen.add_unfold thm #> add_inline thm)))
+ "preprocessing equations for code generators"
end;
val _ =