# HG changeset patch # User krauss # Date 1329600684 -3600 # Node ID 274bb026da6c7239af85ba964b5fcfffea48a57a # Parent c4cf9d03c352eb5073a42b6ce9265b5ad8e554af# Parent af3df09590f9be49170787b254d72ef044a7fc67 merged diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Adaptation.thy --- 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\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 + diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Evaluation.thy --- 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 + diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Foundations.thy --- 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\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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Further.thy --- 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 + diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Inductive_Predicate.thy --- 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 \ lexord r (xs, ys)" -(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*) + "append xs (a # v) ys \ lexordp r xs ys" +(*<*)unfolding lexordp_def by (auto simp add: append)(*>*) lemma %quote [code_pred_intro]: - "append u (a # v) xs \ append u (b # w) ys \ r (a, b) - \ lexord r (xs, ys)" -(*<*)unfolding lexord_def Collect_def append mem_def apply simp + "append u (a # v) xs \ append u (b # w) ys \ r a b + \ 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: "\ r' xs' ys' a v. r = r' \ (xs, ys) = (xs', ys') \ append xs' (a # v) ys' \ thesis" - assume 2: "\ r' xs' ys' u a v b w. r = r' \ (xs, ys) = (xs', ys') \ append u (a # v) xs' \ append u (b # w) ys' \ r' (a, b) \ thesis" + assume lexord: "lexordp r xs ys" + assume 1: "\r' xs' ys' a v. r = r' \ xs = xs' \ ys = ys' + \ append xs' (a # v) ys' \ thesis" + assume 2: "\r' xs' ys' u a v b w. r = r' \ xs = xs' \ ys = ys' + \ append u (a # v) xs' \ append u (b # w) ys' \ r' a b \ thesis" { assume "\a v. ys = xs @ a # v" from this 1 have thesis - by (fastsimp simp add: append) + by (fastforce simp add: append) } moreover { - assume "\u a b v w. (a, b) \ r \ xs = u @ a # v \ ys = u @ b # w" - from this 2 have thesis by (fastsimp simp add: append mem_def) + assume "\u a b v w. r a b \ xs = u @ a # v \ 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 + diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Introduction.thy --- 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 + diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Refinement.thy --- 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 + diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/Setup.thy --- 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 + diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/document/Adaptation.tex --- 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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/document/Evaluation.tex --- 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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/document/Foundations.tex --- 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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/document/Further.tex --- 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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/document/Inductive_Predicate.tex --- 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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/document/Introduction.tex --- 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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/Codegen/Thy/document/Refinement.tex --- 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 diff -r c4cf9d03c352 -r 274bb026da6c doc-src/IsarImplementation/Thy/document/Proof.tex --- 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% diff -r c4cf9d03c352 -r 274bb026da6c doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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% diff -r c4cf9d03c352 -r 274bb026da6c doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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}% diff -r c4cf9d03c352 -r 274bb026da6c doc-src/TutorialI/Types/document/Axioms.tex --- 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% diff -r c4cf9d03c352 -r 274bb026da6c doc-src/antiquote_setup.ML --- 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; diff -r c4cf9d03c352 -r 274bb026da6c src/Pure/Isar/code.ML --- 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;