# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272142550 -7200
# Node ID 620a24bf954ae8e96a837ffa6de175f0a483716b
# Parent  0bcd598d2587e88f1bc2d56e15602a49ea0b1d75
added a section to the introduction; described @{make_string}

diff -r 0bcd598d2587 -r 620a24bf954a ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Apr 07 11:32:00 2010 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Apr 24 22:55:50 2010 +0200
@@ -10,7 +10,7 @@
 *}
 (*>*)
 
-chapter {* First Steps *}
+chapter {* First Steps\label{chp:firststeps} *}
 
 text {*
    \begin{flushright}
@@ -142,12 +142,12 @@
   will print out @{text [quotes] "any string"} inside the response buffer of
   Isabelle.  This function expects a string as argument. If you develop under
   PolyML, then there is a convenient, though again ``quick-and-dirty'', method
-  for converting values into strings, namely the function 
-  @{ML_ind makestring in PolyML}:
+  for converting values into strings, namely the antiquotation 
+  @{text "@{make_string}"}:
 
-  @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} 
+  @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
 
-  However, @{ML makestring in PolyML} only works if the type of what
+  However, @{text "@{makes_tring}"} only works if the type of what
   is converted is monomorphic and not a function.
 
   The function @{ML "writeln"} should only be used for testing purposes,
@@ -797,6 +797,11 @@
   \end{readmore}
 
   \footnote{\bf FIXME: find a good exercise for combinators}
+  \begin{exercise}
+  Find out what the combinator @{ML "K I"} does.
+  \end{exercise}
+
+
   \footnote{\bf FIXME: say something about calling conventions} 
 *}
 
diff -r 0bcd598d2587 -r 620a24bf954a ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Wed Apr 07 11:32:00 2010 +0200
+++ b/ProgTutorial/Intro.thy	Sat Apr 24 22:55:50 2010 +0200
@@ -145,6 +145,28 @@
   to solve the exercises on your own, and then look at the solutions.
 *}
 
+section {* How To Understand Code in Isabelle *}
+
+text {*
+  One of the more difficult aspects of programming is to understand somebody
+  else's code. This is aggravated in Isabelle by the fact that many parts of
+  the code contain only few comments. There is one strategy that might be
+  helpful to navigate your way: ML is an interactive programming environment,
+  which means you can evaluate code on the fly (for example inside an
+  \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy
+  self-contained chunks of existing code into a separate theory file and then
+  study it alongside with examples. You can also install probes inside the
+  copied code without having to recompile the whole Isabelle distributions. Such
+  probes might be messages or printouts of variables (see chapter
+  \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
+  probing the code with explicit print statements is the most efficient method
+  for understanding what some code is doing. However do not expect quick
+  results with this! Depending on the size of the code you are looking at, 
+  you will spend the better part of a quiet afternoon with it. But there 
+  seems to be no better way around it.
+*}
+
+
 section {* Aaaaargh! My Code Does not Work Anymore *}
 
 text {*
@@ -248,7 +270,10 @@
   Please let me know of any omissions. Responsibility for any remaining
   errors lies with me.\bigskip
 
-  \vspace{5cm}
+  \newpage
+  \mbox{}\\[5cm]
+  
+  
   {\Large\bf
   This tutorial is still in the process of being written! All of the
   text is still under construction. Sections and 
diff -r 0bcd598d2587 -r 620a24bf954a ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Wed Apr 07 11:32:00 2010 +0200
+++ b/ProgTutorial/Parsing.thy	Sat Apr 24 22:55:50 2010 +0200
@@ -15,6 +15,13 @@
 chapter {* Parsing\label{chp:parsing} *}
 
 text {*
+  \begin{flushright}
+  {\em An important principle underlying the success and popularity of Unix\\ is
+  the philosophy of building on the work of others.} \\[1ex]
+  Linus Torwalds in the email exchange\\ with Andrew S.~Tannenbaum
+  \end{flushright}
+
+
   Isabelle distinguishes between \emph{outer} and \emph{inner}
   syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}
   and so on, belong to the outer syntax, whereas terms, types and so on belong
@@ -1386,6 +1393,37 @@
   \end{minipage} *}
 (*<*)oops(*>*)
 
+method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
+
+lemma "True"
+apply(test)
+oops
+
+method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
+
+lemma "False"
+apply(joker)
+oops
+
+text {* if true is set then always works *}
+
+ML {* atac *} 
+
+method_setup first_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD (atac 1)))) *} {* bla *}
+
+ML {* HEADGOAL *}
+
+lemma "A \<Longrightarrow> A"
+apply(first_atac)
+oops
+
+method_setup my_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD' atac))) *} {* bla *}
+
+lemma "A \<Longrightarrow> A"
+apply(my_atac)
+oops
+
+
 
 
 
@@ -1398,7 +1436,23 @@
 ML {* Scan.succeed  *}
 *)
 
+ML {* resolve_tac *}
+
+method_setup myrule =
+  {* Scan.lift (Scan.succeed (K (METHOD (fn thms => resolve_tac thms 1)))) *}
+  {* bla *}
+
+lemma
+  assumes a: "A \<Longrightarrow> B \<Longrightarrow> C"
+  shows "C"
+using a
+apply(myrule)
+oops
+
+
+
 text {*
+  (********************************************************)
   (FIXME: explain a version of rule-tac)
 *}
 
diff -r 0bcd598d2587 -r 620a24bf954a progtutorial.pdf
Binary file progtutorial.pdf has changed