--- a/doc-src/Codegen/Thy/Adaptation.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Adaptation.thy Sat Feb 18 22:31:24 2012 +0100
@@ -125,36 +125,38 @@
\begin{description}
- \item[@{theory "Code_Integer"}] represents @{text HOL} integers by
+ \item[@{text "Code_Integer"}] represents @{text HOL} integers by
big integer literals in target languages.
- \item[@{theory "Code_Char"}] represents @{text HOL} characters by
+ \item[@{text "Code_Char"}] represents @{text HOL} characters by
character literals in target languages.
- \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"}, but
- also offers treatment of character codes; includes @{theory
+ \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but
+ also offers treatment of character codes; includes @{text
"Code_Char"}.
- \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements
+ \item[@{text "Efficient_Nat"}] \label{eff_nat} implements
natural numbers by integers, which in general will result in
higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
- @{const "Suc"} is eliminated; includes @{theory "Code_Integer"}
- and @{theory "Code_Numeral"}.
+ @{const "Suc"} is eliminated; includes @{text "Code_Integer"}
+ and @{text "Code_Numeral"}.
\item[@{theory "Code_Numeral"}] provides an additional datatype
@{typ index} which is mapped to target-language built-in
integers. Useful for code setups which involve e.g.~indexing
- of target-language arrays.
+ of target-language arrays. Part of @{text "HOL-Main"}.
\item[@{theory "String"}] provides an additional datatype @{typ
String.literal} which is isomorphic to strings; @{typ
String.literal}s are mapped to target-language strings. Useful
for code setups which involve e.g.~printing (error) messages.
+ Part of @{text "HOL-Main"}.
\end{description}
\begin{warn}
- When importing any of these theories, they should form the last
+ When importing any of those theories which are not part of
+ @{text "HOL-Main"}, they should form the last
items in an import list. Since these theories adapt the code
generator setup in a non-conservative fashion, strange effects may
occur otherwise.
@@ -342,3 +344,4 @@
*}
end
+
--- a/doc-src/Codegen/Thy/Evaluation.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Evaluation.thy Sat Feb 18 22:31:24 2012 +0100
@@ -284,3 +284,4 @@
*}
end
+
--- a/doc-src/Codegen/Thy/Foundations.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Foundations.thy Sat Feb 18 22:31:24 2012 +0100
@@ -117,7 +117,7 @@
interface, transforming a list of function theorems to another list
of function theorems, provided that neither the heading constant nor
its type change. The @{term "0\<Colon>nat"} / @{const Suc} pattern
- elimination implemented in theory @{theory Efficient_Nat} (see
+ elimination implemented in theory @{text Efficient_Nat} (see
\secref{eff_nat}) uses this interface.
\noindent The current setup of the preprocessor may be inspected
--- a/doc-src/Codegen/Thy/Further.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Sat Feb 18 22:31:24 2012 +0100
@@ -18,7 +18,7 @@
\item @{text Scala} sacrifices Hindely-Milner type inference for a
much more rich type system with subtyping etc. For this reason
type arguments sometimes have to be given explicitly in square
- brackets (mimicing System F syntax).
+ brackets (mimicking System F syntax).
\item In contrast to @{text Haskell} where most specialities of
the type system are implemented using \emph{type classes},
@@ -348,3 +348,4 @@
*}
end
+
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Sat Feb 18 22:31:24 2012 +0100
@@ -11,6 +11,9 @@
lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
+
+lemmas lexordp_def =
+ lexordp_def [unfolded lexord_def mem_Collect_eq split]
(*>*)
section {* Inductive Predicates \label{sec:inductive} *}
@@ -152,7 +155,7 @@
*}
text %quote {*
- @{thm [display] lexord_def [of r]}
+ @{thm [display] lexordp_def [of r]}
*}
text {*
@@ -161,34 +164,36 @@
*}
lemma %quote [code_pred_intro]:
- "append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
-(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
+ "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys"
+(*<*)unfolding lexordp_def by (auto simp add: append)(*>*)
lemma %quote [code_pred_intro]:
- "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
- \<Longrightarrow> lexord r (xs, ys)"
-(*<*)unfolding lexord_def Collect_def append mem_def apply simp
+ "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b
+ \<Longrightarrow> lexordp r xs ys"
+(*<*)unfolding lexordp_def append apply simp
apply (rule disjI2) by auto(*>*)
-code_pred %quote lexord
+code_pred %quote lexordp
(*<*)proof -
fix r xs ys
- assume lexord: "lexord r (xs, ys)"
- assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
- assume 2: "\<And> r' xs' ys' u a v b w. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' (a, b) \<Longrightarrow> thesis"
+ assume lexord: "lexordp r xs ys"
+ assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
+ \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
+ assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
+ \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis"
{
assume "\<exists>a v. ys = xs @ a # v"
from this 1 have thesis
- by (fastsimp simp add: append)
+ by (fastforce simp add: append)
} moreover
{
- assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
- from this 2 have thesis by (fastsimp simp add: append mem_def)
+ assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w"
+ from this 2 have thesis by (fastforce simp add: append)
} moreover
note lexord
ultimately show thesis
- unfolding lexord_def
- by (fastsimp simp add: Collect_def)
+ unfolding lexordp_def
+ by fastforce
qed(*>*)
@@ -267,3 +272,4 @@
*}
end
+
--- a/doc-src/Codegen/Thy/Introduction.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Introduction.thy Sat Feb 18 22:31:24 2012 +0100
@@ -239,3 +239,4 @@
*}
end
+
--- a/doc-src/Codegen/Thy/Refinement.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Refinement.thy Sat Feb 18 22:31:24 2012 +0100
@@ -265,12 +265,10 @@
text {*
Typical data structures implemented by representations involving
- invariants are available in the library, e.g.~theories @{theory
- Cset} and @{theory Mapping} specify sets (type @{typ "'a Cset.set"}) and
- key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively;
- these can be implemented by distinct lists as presented here as
- example (theory @{theory Dlist}) and red-black-trees respectively
- (theory @{theory RBT}).
+ invariants are available in the library, theory @{theory Mapping}
+ specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
+ these can be implemented by red-black-trees (theory @{theory RBT}).
*}
end
+
--- a/doc-src/Codegen/Thy/Setup.thy Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/Setup.thy Sat Feb 18 22:31:24 2012 +0100
@@ -1,7 +1,9 @@
theory Setup
imports
Complex_Main
- More_List RBT Dlist List_Cset Mapping
+ "~~/src/HOL/Library/Dlist"
+ "~~/src/HOL/Library/RBT"
+ "~~/src/HOL/Library/Mapping"
uses
"../../antiquote_setup.ML"
"../../more_antiquote.ML"
@@ -27,3 +29,4 @@
declare [[names_unique = false]]
end
+
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Sat Feb 18 22:31:24 2012 +0100
@@ -158,33 +158,35 @@
\begin{description}
- \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}}}] represents \isa{HOL} integers by
+ \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}] represents \isa{HOL} integers by
big integer literals in target languages.
- \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}}}] represents \isa{HOL} characters by
+ \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}] represents \isa{HOL} characters by
character literals in target languages.
- \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char{\isaliteral{5F}{\isacharunderscore}}chr}}}] like \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}, but
- also offers treatment of character codes; includes \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}}}.
+ \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char{\isaliteral{5F}{\isacharunderscore}}chr}] like \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}, but
+ also offers treatment of character codes; includes \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}.
- \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}}}] \label{eff_nat} implements
+ \item[\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}] \label{eff_nat} implements
natural numbers by integers, which in general will result in
higher efficiency; pattern matching with \isa{{\isadigit{0}}} /
- \isa{Suc} is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}}}
- and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}}}.
+ \isa{Suc} is eliminated; includes \isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}
+ and \isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}.
\item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}}}] provides an additional datatype
\isa{index} which is mapped to target-language built-in
integers. Useful for code setups which involve e.g.~indexing
- of target-language arrays.
+ of target-language arrays. Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.
\item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings. Useful
for code setups which involve e.g.~printing (error) messages.
+ Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.
\end{description}
\begin{warn}
- When importing any of these theories, they should form the last
+ When importing any of those theories which are not part of
+ \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}, they should form the last
items in an import list. Since these theories adapt the code
generator setup in a non-conservative fashion, strange effects may
occur otherwise.
@@ -641,6 +643,7 @@
%
\endisadelimtheory
\isanewline
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Sat Feb 18 22:31:24 2012 +0100
@@ -427,6 +427,7 @@
%
\endisadelimtheory
\isanewline
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/Codegen/Thy/document/Foundations.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Sat Feb 18 22:31:24 2012 +0100
@@ -178,7 +178,7 @@
interface, transforming a list of function theorems to another list
of function theorems, provided that neither the heading constant nor
its type change. The \isa{{\isadigit{0}}} / \isa{Suc} pattern
- elimination implemented in theory \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}}} (see
+ elimination implemented in theory \isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat} (see
\secref{eff_nat}) uses this interface.
\noindent The current setup of the preprocessor may be inspected
--- a/doc-src/Codegen/Thy/document/Further.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Sat Feb 18 22:31:24 2012 +0100
@@ -38,7 +38,7 @@
\item \isa{Scala} sacrifices Hindely-Milner type inference for a
much more rich type system with subtyping etc. For this reason
type arguments sometimes have to be given explicitly in square
- brackets (mimicing System F syntax).
+ brackets (mimicking System F syntax).
\item In contrast to \isa{Haskell} where most specialities of
the type system are implemented using \emph{type classes},
@@ -616,6 +616,7 @@
%
\endisadelimtheory
\isanewline
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Sat Feb 18 22:31:24 2012 +0100
@@ -332,10 +332,9 @@
%
\begin{isamarkuptext}%
\begin{isabelle}%
-lexord\ r\ {\isaliteral{3D}{\isacharequal}}\isanewline
-{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\isanewline
-\isaindent{\ }{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C6F723E}{\isasymor}}\isanewline
-\isaindent{\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}u\ a\ b\ v\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}%
+lexordp\ r\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\isanewline
+{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C6F723E}{\isasymor}}\isanewline
+\isaindent{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}u\ a\ b\ v\ w{\isaliteral{2E}{\isachardot}}\ r\ a\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -360,13 +359,13 @@
\isatagquote
\isacommand{lemma}\isamarkupfalse%
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ xs\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexord\ r\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ xs\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexordp\ r\ xs\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ u\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ append\ u\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexord\ r\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ u\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ append\ u\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ a\ b\isanewline
+\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexordp\ r\ xs\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
-\ lexord%
+\ lexordp%
\endisatagquote
{\isafoldquote}%
%
@@ -492,6 +491,7 @@
%
\endisadelimtheory
\isanewline
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/Codegen/Thy/document/Introduction.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Sat Feb 18 22:31:24 2012 +0100
@@ -578,6 +578,7 @@
%
\endisadelimtheory
\isanewline
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/Codegen/Thy/document/Refinement.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Sat Feb 18 22:31:24 2012 +0100
@@ -628,11 +628,9 @@
%
\begin{isamarkuptext}%
Typical data structures implemented by representations involving
- invariants are available in the library, e.g.~theories \hyperlink{theory.Cset}{\mbox{\isa{Cset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isaliteral{27}{\isacharprime}}a\ Cset{\isaliteral{2E}{\isachardot}}set}) and
- key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping}) respectively;
- these can be implemented by distinct lists as presented here as
- example (theory \hyperlink{theory.Dlist}{\mbox{\isa{Dlist}}}) and red-black-trees respectively
- (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
+ invariants are available in the library, theory \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}}
+ specifies key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping});
+ these can be implemented by red-black-trees (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -650,6 +648,7 @@
%
\endisadelimtheory
\isanewline
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Feb 18 22:31:24 2012 +0100
@@ -485,7 +485,7 @@
\begin{isamarkuptext}%
The following example demonstrates how rules can be
derived by building up a context of assumptions first, and exporting
- some local fact afterwards. We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality
+ some local fact afterwards. We refer to \isa{Pure} equality
here for testing purposes.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Feb 18 22:31:24 2012 +0100
@@ -1115,7 +1115,7 @@
%
\begin{isamarkuptext}%
We define a type of finite sequences, with slightly different
- names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \hyperlink{theory.Main}{\mbox{\isa{Main}}}:%
+ names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \isa{Main}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 18 22:31:24 2012 +0100
@@ -1363,12 +1363,12 @@
\item Iterated replacement via recursive \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}.
For example, consider list enumeration \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{2C}{\isacharcomma}}\ d{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as
- defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
+ defined in theory \isa{List} in Isabelle/HOL.
\item Change of binding status of variables: anything beyond the
built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} mixfix annotation requires explicit
syntax translations. For example, consider list filter
- comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
+ comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \isa{List} in Isabelle/HOL.
\end{itemize}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Axioms.tex Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Sat Feb 18 22:31:24 2012 +0100
@@ -463,7 +463,7 @@
\emph{with} axioms.
Further note that classes may contain axioms but \emph{no} operations.
-An example is class \isa{finite} from theory \hyperlink{theory.Finite-Set}{\mbox{\isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set}}}
+An example is class \isa{finite} from theory \isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set}
which specifies a type to be finite: \isa{{\isaliteral{22}{\isachardoublequote}}finite\ {\isaliteral{28}{\isacharparenleft}}UNIV\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}finite\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/antiquote_setup.ML Sat Feb 18 09:46:58 2012 +0100
+++ b/doc-src/antiquote_setup.ML Sat Feb 18 22:31:24 2012 +0100
@@ -207,7 +207,6 @@
entity_antiqs no_check "" "inference" #>
entity_antiqs no_check "isatt" "executable" #>
entity_antiqs (K check_tool) "isatt" "tool" #>
- entity_antiqs (K (can Thy_Info.get_theory)) "" "theory" #>
entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
"" Isabelle_Markup.ML_antiquotationN;
--- a/src/Pure/Isar/code.ML Sat Feb 18 09:46:58 2012 +0100
+++ b/src/Pure/Isar/code.ML Sat Feb 18 22:31:24 2012 +0100
@@ -49,6 +49,7 @@
-> theory -> theory) -> theory -> theory
val add_eqn: thm -> theory -> theory
val add_nbe_eqn: thm -> theory -> theory
+ val add_abs_eqn: thm -> theory -> theory
val add_default_eqn: thm -> theory -> theory
val add_default_eqn_attribute: attribute
val add_default_eqn_attrib: Attrib.src
@@ -114,8 +115,6 @@
(* constants *)
-fun typ_equiv tys = Type.raw_instance tys andalso Type.raw_instance (swap tys);
-
fun check_bare_const thy t = case try dest_Const t
of SOME c_ty => c_ty
| NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
@@ -517,7 +516,8 @@
| THM _ => bad "Not a proper equation";
val (rep, lhs) = dest_comb full_lhs
handle TERM _ => bad "Not an abstract equation";
- val (rep_const, ty) = dest_Const rep;
+ val (rep_const, ty) = dest_Const rep
+ handle TERM _ => bad "Not an abstract equation";
val (tyco, Ts) = (dest_Type o domain_type) ty
handle TERM _ => bad "Not an abstract equation"
| TYPE _ => bad "Not an abstract equation";
@@ -697,8 +697,7 @@
val add_consts = fold_aterms add_const
in add_consts rhs o fold add_consts args end;
-fun dest_eqn thy =
- apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
+val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
abstype cert = Equations of thm * bool list
| Projection of term * string
@@ -809,21 +808,21 @@
|> Thm.varifyT_global
|> Conjunction.elim_balanced (length propers);
fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
- in (tyscm, map (abstractions o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
+ in (tyscm, map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
| equations_of_cert thy (Projection (t, tyco)) =
let
val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
val tyscm = typscheme_projection thy t;
val t' = Logic.varify_types_global t;
fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
- in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
+ in (tyscm, [((abstractions o dest_eqn) t', (NONE, true))]) end
| equations_of_cert thy (Abstract (abs_thm, tyco)) =
let
val tyscm = typscheme_abs thy abs_thm;
val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
in
- (tyscm, [((abstractions o dest_eqn thy o Thm.prop_of) concrete_thm,
+ (tyscm, [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
(SOME (Thm.varifyT_global abs_thm), true))])
end;