# HG changeset patch # User wenzelm # Date 939909759 -7200 # Node ID c007f801cd598daa4bdc559c2d37af295db2a008 # Parent 0cb6508f190c9605ef6c9696b73995aa6231428e improved presentation; diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/Cantor.thy --- a/src/HOL/Isar_examples/Cantor.thy Thu Oct 14 15:14:14 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Thu Oct 14 16:02:39 1999 +0200 @@ -5,7 +5,7 @@ header {* Cantor's Theorem *}; -theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of +theory Cantor = Main:;text_raw {* \footnote{This is an Isar version of the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.} *}; diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/ExprCompiler.thy --- a/src/HOL/Isar_examples/ExprCompiler.thy Thu Oct 14 15:14:14 1999 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Thu Oct 14 16:02:39 1999 +0200 @@ -9,17 +9,52 @@ theory ExprCompiler = Main:; -subsection {* Basics *}; +text {* + This is a (quite trivial) example of program verification. We model + a compiler translating expressions to stack machine instructions, and + prove its correctness wrt.\ evaluation semantics. +*}; + + +subsection {* Binary operations *}; text {* - First we define a type abbreviation for binary operations over some - type of values. + Binary operations are just functions over some type of values. This + is both for syntax and semantics, i.e.\ we use a ``shallow + embedding''. *}; types 'val binop = "'val => 'val => 'val"; +subsection {* Expressions *}; + +text {* + The language of expressions is defined as an inductive type, + consisting of variables, constants, and binary operations on + expressions. +*}; + +datatype ('adr, 'val) expr = + Variable 'adr | + Constant 'val | + Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"; + +text {* + Evaluation (wrt.\ an environment) is defined by primitive recursion + over the structure of expressions. +*}; + +consts + eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"; + +primrec + "eval (Variable x) env = env x" + "eval (Constant c) env = c" + "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"; + + subsection {* Machine *}; text {* @@ -32,8 +67,8 @@ Apply "'val binop"; text {* - Execution of a list of stack machine instructions is - straight-forward. + Execution of a list of stack machine instructions is easily defined + as follows. *}; consts @@ -54,35 +89,10 @@ "execute instrs env == hd (exec instrs [] env)"; -subsection {* Expressions *}; - -text {* - We introduce a simple language of expressions: variables, constants, - binary operations. -*}; - -datatype ('adr, 'val) expr = - Variable 'adr | - Constant 'val | - Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"; - -text {* - Evaluation of expressions does not do any unexpected things. -*}; - -consts - eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"; - -primrec - "eval (Variable x) env = env x" - "eval (Constant c) env = c" - "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"; - - subsection {* Compiler *}; text {* - So we are ready to define the compilation function of expressions to + We are ready to define the compilation function of expressions to lists of stack machine instructions. *}; diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/Peirce.thy --- a/src/HOL/Isar_examples/Peirce.thy Thu Oct 14 15:14:14 1999 +0200 +++ b/src/HOL/Isar_examples/Peirce.thy Thu Oct 14 16:02:39 1999 +0200 @@ -77,13 +77,13 @@ Nevertheless, the ``strong'' mode of plain assumptions is quite important in practice to achieve robustness of proof document interpretation. By forcing both the conclusion \emph{and} the - assumptions to unify with any pending goal to be solved, goal - selection becomes quite deterministic. For example, typical - ``case-analysis'' rules give rise to several goals that only differ - in there local contexts. With strong assumptions these may be still - solved in any order in a predictable way, while weak ones would - quickly lead to great confusion, eventually demanding even some - backtracking. + assumptions to unify with the pending goal to be solved, goal + selection becomes quite deterministic. For example, decomposition + with ``case-analysis'' type rules usually give rise to several goals + that only differ in there local contexts. With strong assumptions + these may be still solved in any order in a predictable way, while + weak ones would quickly lead to great confusion, eventually demanding + even some backtracking. *}; end; diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/Summation.thy --- a/src/HOL/Isar_examples/Summation.thy Thu Oct 14 15:14:14 1999 +0200 +++ b/src/HOL/Isar_examples/Summation.thy Thu Oct 14 16:02:39 1999 +0200 @@ -30,7 +30,7 @@ subsection {* Summation laws *}; -verbatim {* \begin{comment} *}; +text_raw {* \begin{comment} *}; (* FIXME binary arithmetic does not yet work here *) @@ -46,7 +46,7 @@ theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; -verbatim {* \end{comment} *}; +text_raw {* \end{comment} *}; theorem sum_of_naturals: diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/document/root.tex --- a/src/HOL/Isar_examples/document/root.tex Thu Oct 14 15:14:14 1999 +0200 +++ b/src/HOL/Isar_examples/document/root.tex Thu Oct 14 16:02:39 1999 +0200 @@ -17,6 +17,8 @@ \end{abstract} \tableofcontents + +\parindent 0pt \parskip 0.5ex \input{session} \nocite{isabelle-isar-ref,Wenzel:1999:TPHOL} diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/document/style.tex --- a/src/HOL/Isar_examples/document/style.tex Thu Oct 14 15:14:14 1999 +0200 +++ b/src/HOL/Isar_examples/document/style.tex Thu Oct 14 16:02:39 1999 +0200 @@ -5,7 +5,6 @@ \usepackage{comment,proof,isabelle,pdfsetup} \renewcommand{\isamarkupheader}[1]{\section{#1}} -\parindent 0pt \parskip 0.5ex \newcommand{\name}[1]{\textsl{#1}} @@ -24,7 +23,6 @@ \newcommand{\conj}{\land} \newcommand{\disj}{\lor} - %%% Local Variables: %%% mode: latex %%% TeX-master: "root"