# HG changeset patch # User wenzelm # Date 1194701480 -3600 # Node ID 8b1aa43573206f6d5b5f19bb0f4a87bbe1acf97d # Parent 5200374fda5d9e66075b1a0ee316b3e931f8cd8f updated; diff -r 5200374fda5d -r 8b1aa4357320 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sat Nov 10 14:31:18 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sat Nov 10 14:31:20 2007 +0100 @@ -583,25 +583,25 @@ \begin{description} - \item[\isa{Pretty{\isacharunderscore}Int}] represents \isa{HOL} integers by big + \item[\isa{Code{\isacharunderscore}Integer}] represents \isa{HOL} integers by big integer literals in target languages. - \item[\isa{Pretty{\isacharunderscore}Char}] represents \isa{HOL} characters by + \item[\isa{Code{\isacharunderscore}Char}] represents \isa{HOL} characters by character literals in target languages. - \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char}, + \item[\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Code{\isacharunderscore}Char}, but also offers treatment of character codes; includes - \isa{Pretty{\isacharunderscore}Int}. - \item[\isa{Executable{\isacharunderscore}Rat}] implements rational - numbers. - \item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers, - namly those representable by rational numbers. + \isa{Code{\isacharunderscore}Integer}. \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers, which in general will result in higher efficency; pattern matching with \isa{{\isadigit{0}}} / \isa{Suc} - is eliminated; includes \isa{Pretty{\isacharunderscore}Int}. - \item[\isa{ML{\isacharunderscore}String}] provides an additional datatype \isa{mlstring}; - in the \isa{HOL} default setup, strings in HOL are mapped to list - of \isa{HOL} characters in SML; values of type \isa{mlstring} are - mapped to strings in SML. + is eliminated; includes \isa{Code{\isacharunderscore}Integer}. + \item[\isa{Code{\isacharunderscore}Index}] 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. + \item[\isa{Code{\isacharunderscore}Message}] provides an additional datatype + \isa{message{\isacharunderscore}string} which is isomorphic to strings; + \isa{message{\isacharunderscore}string}s are mapped to target-language strings. + Useful for code setups which involve e.g. printing (error) messages. \end{description} @@ -1507,7 +1507,7 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexml{Code.add-func}\verb|Code.add_func: bool -> thm -> theory -> theory| \\ + \indexml{Code.add-func}\verb|Code.add_func: thm -> theory -> theory| \\ \indexml{Code.del-func}\verb|Code.del_func: thm -> theory -> theory| \\ \indexml{Code.add-funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\ \indexml{Code.add-inline}\verb|Code.add_inline: thm -> theory -> theory| \\ diff -r 5200374fda5d -r 8b1aa4357320 doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty --- a/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Sat Nov 10 14:31:18 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Sat Nov 10 14:31:20 2007 +0100 @@ -20,15 +20,15 @@ %symbol markup -- \emph achieves decent spacing via italic corrections \newcommand{\isamath}[1]{\emph{$#1$}} \newcommand{\isatext}[1]{\emph{#1}} -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} -\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} -\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} -\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} -\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript} +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript} +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} diff -r 5200374fda5d -r 8b1aa4357320 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Sat Nov 10 14:31:18 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Sat Nov 10 14:31:20 2007 +0100 @@ -9,7 +9,8 @@ structure List = struct -fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys +fun member A_ x (y :: ys) = + (if HOL.eqop A_ y x then true else member A_ x ys) | member A_ x [] = false; end; (*struct List*) diff -r 5200374fda5d -r 8b1aa4357320 doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Sat Nov 10 14:31:18 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Sat Nov 10 14:31:20 2007 +0100 @@ -12,7 +12,8 @@ fun foldr f (x :: xs) a = f x (foldr f xs a) | foldr f [] a = a; -fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys +fun member A_ x (y :: ys) = + (if HOL.eqop A_ y x then true else member A_ x ys) | member A_ x [] = false; end; (*struct List*) @@ -26,10 +27,10 @@ fun insert x (Set xs) = Set (x :: xs); -fun union xs (Set ys) = List.foldr insert ys xs; +fun uniona xs (Set ys) = List.foldr insert ys xs; fun member A_ x (Set xs) = List.member A_ x xs; -fun uniona (Set xs) = List.foldr union xs empty; +fun unionaa (Set xs) = List.foldr uniona xs empty; end; (*struct Set*) diff -r 5200374fda5d -r 8b1aa4357320 doc-src/TutorialI/Protocol/document/Message.tex --- a/doc-src/TutorialI/Protocol/document/Message.tex Sat Nov 10 14:31:18 2007 +0100 +++ b/doc-src/TutorialI/Protocol/document/Message.tex Sat Nov 10 14:31:20 2007 +0100 @@ -50,7 +50,7 @@ \isacommand{types}\isamarkupfalse% \ key\ {\isacharequal}\ nat\isanewline \isacommand{consts}\isamarkupfalse% -\ invKey\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}key{\isacharequal}{\isachargreater}key{\isachardoublequoteclose}% +\ invKey\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}key\ {\isasymRightarrow}\ key{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof diff -r 5200374fda5d -r 8b1aa4357320 doc-src/TutorialI/Protocol/document/Public.tex --- a/doc-src/TutorialI/Protocol/document/Public.tex Sat Nov 10 14:31:18 2007 +0100 +++ b/doc-src/TutorialI/Protocol/document/Public.tex Sat Nov 10 14:31:20 2007 +0100 @@ -18,18 +18,16 @@ \begin{isamarkuptext}% The function \isa{pubK} maps agents to their public keys. The function -\isa{priK} maps agents to their private keys. It is defined in terms of -\isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is -not a proper constant, so we declare it using \isacommand{syntax} -(cf.\ \S\ref{sec:syntax-translations}).% +\isa{priK} maps agents to their private keys. It is merely +an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of +\isa{invKey} and \isa{pubK}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isamarkupfalse% -\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline -\isacommand{syntax}\isamarkupfalse% -\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline -\isacommand{translations}\isamarkupfalse% -\ {\isachardoublequoteopen}priK\ x{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}% +\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline +\isacommand{abbreviation}\isamarkupfalse% +\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline +\isakeyword{where}\ {\isachardoublequoteopen}priK\ x\ \ {\isasymequiv}\ \ invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent The set \isa{bad} consists of those agents whose private keys are known to @@ -43,7 +41,7 @@ \isacommand{axioms}\isamarkupfalse% \isanewline \ \ inj{\isacharunderscore}pubK{\isacharcolon}\ \ \ \ \ \ \ \ {\isachardoublequoteopen}inj\ pubK{\isachardoublequoteclose}\isanewline -\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isachartilde}{\isacharequal}\ pubK\ B{\isachardoublequoteclose}% +\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isasymnoteq}\ pubK\ B{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof