# HG changeset patch
# User nipkow
# Date 1346999764 -7200
# Node ID d383fd5dbd3c5b89b534b5f91f510f46ca896520
# Parent  e1e1d427747d3738a20619d045a3885dbb50876a# Parent  3601bf546775afebe84b282d92e8f7eba3a124d3
merged

diff -r e1e1d427747d -r d383fd5dbd3c src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Fri Sep 07 08:20:18 2012 +0200
+++ b/src/HOL/IMP/AExp.thy	Fri Sep 07 08:36:04 2012 +0200
@@ -8,16 +8,16 @@
 type_synonym val = int
 type_synonym state = "vname \<Rightarrow> val"
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpaexpdef}{% *}
+text_raw{*\snip{AExpaexpdef}{2}{1}{% *}
 datatype aexp = N int | V vname | Plus aexp aexp
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpavaldef}{% *}
+text_raw{*\snip{AExpavaldef}{1}{2}{% *}
 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
 "aval (N n) s = n" |
 "aval (V x) s = s x" |
 "aval (Plus a1 a2) s = aval a1 s + aval a2 s"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 
 value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
@@ -34,7 +34,7 @@
 translations
   "_State ms" => "_Update <> ms"
 
-text {* 
+text {* \noindent
   We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
 *}
 lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)"
@@ -43,8 +43,7 @@
 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
 
 
-text {* Variables that are not mentioned in the state are 0 by default in 
-  the @{term "<a := b::int>"} syntax: 
+text {* In  the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default:
 *}
 value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
 
@@ -56,7 +55,7 @@
 
 text{* Evaluate constant subsexpressions: *}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpconstdef}{% *}
+text_raw{*\snip{AExpasimpconstdef}{0}{2}{% *}
 fun asimp_const :: "aexp \<Rightarrow> aexp" where
 "asimp_const (N n) = N n" |
 "asimp_const (V x) = V x" |
@@ -64,7 +63,7 @@
   (case (asimp_const a\<^isub>1, asimp_const a\<^isub>2) of
     (N n\<^isub>1, N n\<^isub>2) \<Rightarrow> N(n\<^isub>1+n\<^isub>2) |
     (b\<^isub>1,b\<^isub>2) \<Rightarrow> Plus b\<^isub>1 b\<^isub>2)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 theorem aval_asimp_const:
   "aval (asimp_const a) s = aval a s"
@@ -75,13 +74,13 @@
 text{* Now we also eliminate all occurrences 0 in additions. The standard
 method: optimized versions of the constructors: *}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpplusdef}{% *}
+text_raw{*\snip{AExpplusdef}{0}{2}{% *}
 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
 "plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)" |
 "plus (N i) a = (if i=0 then a else Plus (N i) a)" |
 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
 "plus a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 lemma aval_plus[simp]:
   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
@@ -89,12 +88,12 @@
 apply simp_all (* just for a change from auto *)
 done
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpdef}{% *}
+text_raw{*\snip{AExpasimpdef}{2}{0}{% *}
 fun asimp :: "aexp \<Rightarrow> aexp" where
 "asimp (N n) = N n" |
 "asimp (V x) = V x" |
 "asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 text{* Note that in @{const asimp_const} the optimized constructor was
 inlined. Making it a separate function @{const plus} improves modularity of
diff -r e1e1d427747d -r d383fd5dbd3c src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Fri Sep 07 08:20:18 2012 +0200
+++ b/src/HOL/IMP/ASM.thy	Fri Sep 07 08:36:04 2012 +0200
@@ -4,33 +4,33 @@
 
 subsection "Stack Machine"
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMinstrdef}{% *}
+text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
 datatype instr = LOADI val | LOAD vname | ADD
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMstackdef}{% *}
+text_raw{*\snip{ASMstackdef}{1}{2}{% *}
 type_synonym stack = "val list"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 abbreviation "hd2 xs == hd(tl xs)"
 abbreviation "tl2 xs == tl(tl xs)"
 
 text{* \noindent Abbreviations are transparent: they are unfolded after
 parsing and folded back again before printing. Internally, they do not
-exist. *}
+exist.*}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexeconedef}{% *}
+text_raw{*\snip{ASMexeconedef}{0}{1}{% *}
 fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
 "exec1 (LOADI n) _ stk  =  n # stk" |
 "exec1 (LOAD x) s stk  =  s(x) # stk" |
 "exec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexecdef}{% *}
+text_raw{*\snip{ASMexecdef}{1}{2}{% *}
 fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
 "exec [] _ stk = stk" |
 "exec (i#is) s stk = exec is s (exec1 i s stk)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 value "exec [LOADI 5, LOAD ''y'', ADD]
  <''x'' := 42, ''y'' := 43> [50]"
@@ -44,12 +44,12 @@
 
 subsection "Compilation"
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMcompdef}{% *}
+text_raw{*\snip{ASMcompdef}{0}{2}{% *}
 fun comp :: "aexp \<Rightarrow> instr list" where
 "comp (N n) = [LOADI n]" |
 "comp (V x) = [LOAD x]" |
 "comp (Plus e\<^isub>1 e\<^isub>2) = comp e\<^isub>1 @ comp e\<^isub>2 @ [ADD]"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
 
diff -r e1e1d427747d -r d383fd5dbd3c src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Fri Sep 07 08:20:18 2012 +0200
+++ b/src/HOL/IMP/BExp.thy	Fri Sep 07 08:36:04 2012 +0200
@@ -2,17 +2,17 @@
 
 subsection "Boolean Expressions"
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbexpdef}{% *}
+text_raw{*\snip{BExpbexpdef}{0}{1}{% *}
 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbvaldef}{% *}
+text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
 "bval (Bc v) s = v" |
 "bval (Not b) s = (\<not> bval b s)" |
 "bval (And b\<^isub>1 b\<^isub>2) s = (bval b\<^isub>1 s \<and> bval b\<^isub>2 s)" |
 "bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
             <''x'' := 3, ''y'' := 1>"
@@ -31,37 +31,37 @@
 
 text{* Optimizing constructors: *}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BExplessdef}{% *}
+text_raw{*\snip{BExplessdef}{0}{2}{% *}
 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
 "less (N n\<^isub>1) (N n\<^isub>2) = Bc(n\<^isub>1 < n\<^isub>2)" |
 "less a\<^isub>1 a\<^isub>2 = Less a\<^isub>1 a\<^isub>2"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
 apply(induction a1 a2 rule: less.induct)
 apply simp_all
 done
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpanddef}{% *}
+text_raw{*\snip{BExpanddef}{2}{2}{% *}
 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
 "and (Bc True) b = b" |
 "and b (Bc True) = b" |
 "and (Bc False) b = Bc False" |
 "and b (Bc False) = Bc False" |
 "and b\<^isub>1 b\<^isub>2 = And b\<^isub>1 b\<^isub>2"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
 apply(induction b1 b2 rule: and.induct)
 apply simp_all
 done
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpnotdef}{% *}
+text_raw{*\snip{BExpnotdef}{2}{2}{% *}
 fun not :: "bexp \<Rightarrow> bexp" where
 "not (Bc True) = Bc False" |
 "not (Bc False) = Bc True" |
 "not b = Not b"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 lemma bval_not[simp]: "bval (not b) s = (\<not> bval b s)"
 apply(induction b rule: not.induct)
@@ -70,13 +70,13 @@
 
 text{* Now the overall optimizer: *}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbsimpdef}{% *}
+text_raw{*\snip{BExpbsimpdef}{0}{2}{% *}
 fun bsimp :: "bexp \<Rightarrow> bexp" where
 "bsimp (Bc v) = Bc v" |
 "bsimp (Not b) = not(bsimp b)" |
 "bsimp (And b\<^isub>1 b\<^isub>2) = and (bsimp b\<^isub>1) (bsimp b\<^isub>2)" |
 "bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 value "bsimp (And (Less (N 0) (N 1)) b)"
 
diff -r e1e1d427747d -r d383fd5dbd3c src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Fri Sep 07 08:20:18 2012 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Fri Sep 07 08:36:04 2012 +0200
@@ -4,7 +4,7 @@
 
 subsection "Big-Step Semantics of Commands"
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepdef}{% *}
+text_raw{*\snip{BigStepdef}{0}{1}{% *}
 inductive
   big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
 where
@@ -21,16 +21,16 @@
 WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
 WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
              (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *}
+text_raw{*\snip{BigStepEx}{1}{2}{% *}
 schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
 apply(rule Seq)
 apply(rule Assign)
 apply simp
 apply(rule Assign)
 done
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 thm ex[simplified]
 
@@ -130,11 +130,11 @@
   in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   in the same @{text s'}}. Formally:
 *}
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEquiv}{% *}
+text_raw{*\snip{BigStepEquiv}{0}{1}{% *}
 abbreviation
   equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
   "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 text {*
 Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
@@ -220,17 +220,17 @@
 subsection "Execution is deterministic"
 
 text {* This proof is automatic. *}
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDeterministic}{% *}
+text_raw{*\snip{BigStepDeterministic}{0}{1}{% *}
 theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
   by (induction arbitrary: u rule: big_step.induct) blast+
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 
 text {*
   This is the proof as you might present it in a lecture. The remaining
   cases are simple enough to be proved automatically:
 *}
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDetLong}{% *}
+text_raw{*\snip{BigStepDetLong}{0}{2}{% *}
 theorem
   "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
 proof (induction arbitrary: t' rule: big_step.induct)
@@ -250,6 +250,6 @@
   from c IHc have "s1' = s1" by blast
   with w IHw show "t' = t" by blast
 qed blast+ -- "prove the rest automatically"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 end
diff -r e1e1d427747d -r d383fd5dbd3c src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Fri Sep 07 08:20:18 2012 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Fri Sep 07 08:36:04 2012 +0200
@@ -4,7 +4,7 @@
 
 subsection "The transition relation"
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\SmallStepDef}{% *}
+text_raw{*\snip{SmallStepDef}{0}{2}{% *}
 inductive
   small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
 where
@@ -17,7 +17,7 @@
 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
 
 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 
 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
diff -r e1e1d427747d -r d383fd5dbd3c src/HOL/IMP/document/isaverbatimwrite.sty
--- a/src/HOL/IMP/document/isaverbatimwrite.sty	Fri Sep 07 08:20:18 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-\@ifundefined{verbatim@processline}{\input verbatim.sty}{}
-
-\newwrite \isaverbatim@out
-\def\openisaverbatimout#1{\immediate\openout \isaverbatim@out #1}
-\def\closeisaverbatimout{\immediate\closeout \isaverbatim@out}
-\def\isaverbatimwrite{%
-  \@bsphack
-  \let\do\@makeother\dospecials
-  \catcode`\^^M\active \catcode`\^^I=12
-  \def\verbatim@processline{%
-    \immediate\write\isaverbatim@out
-      {\the\verbatim@line}}%
-  \verbatim@start}
-
-\def\endisaverbatimwrite{%
-  \@esphack}
diff -r e1e1d427747d -r d383fd5dbd3c src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Fri Sep 07 08:20:18 2012 +0200
+++ b/src/HOL/IMP/document/root.tex	Fri Sep 07 08:36:04 2012 +0200
@@ -1,23 +1,20 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
-
 \usepackage{latexsym}
-
 % this should be the last package used
 \usepackage{pdfsetup}
 
-\usepackage{isaverbatimwrite}
+% snip
+\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
+\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
 
-% urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 \renewcommand{\isastyle}{\isastyleminor}
 
-
 \begin{document}
-\openisaverbatimout fragments
 
 \title{Concrete Semantics}
 \author{TN \& GK}
@@ -32,7 +29,6 @@
 
 \nocite{Nipkow}
 
-% optional bibliography
 \bibliographystyle{abbrv}
 \bibliography{root}