--- a/ProgTutorial/General.thy	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/General.thy	Sun Oct 25 15:26:03 2009 +0100
@@ -11,7 +11,7 @@
 (*>*)
 
 
-chapter {* Isabelle in More Detail *}
+chapter {* Isabelle Essentials *}
 
 text {*
   Isabelle is build around a few central ideas. One central idea is the
@@ -886,14 +886,13 @@
 
   Recall that Isabelle does not let you call @{ML note in LocalTheory} twice
   with the same theorem name. In effect, once a theorem is stored under a name, 
-  this association will be fixed. While this is a ``safety-net'' to make sure a
+  this association is fixed. While this is a ``safety-net'' to make sure a
   theorem name refers to a particular theorem or collection of theorems, it is 
   also a bit too restrictive in cases where a theorem name should refer to a 
   dynamically expanding list of theorems (like a simpset). Therefore Isabelle 
   also implements a mechanism where a theorem name can refer to a custom theorem 
   list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. 
-  To see how it works let us assume we defined our own theorem list maintained 
-  in the data storage @{text MyThmList}.
+  To see how it works let us assume we defined our own theorem list @{text MyThmList}.
 *}
 
 ML{*structure MyThmList = GenericDataFun
@@ -945,8 +944,8 @@
   @{text "> True"}
   \end{isabelle}
 
-  There is a multitude of functions that manage or manipulate theorems in the 
-  structures @{ML_struct Thm} and @{ML_struct Drule}. For example 
+  There is a multitude of functions in the structures @{ML_struct Thm} and @{ML_struct Drule} 
+  for managing or manipulating theorems. For example 
   we can test theorems for alpha equality. Suppose you proved the following three 
   theorems.
 *}
@@ -1008,8 +1007,7 @@
   Note that in the second case, there is no premise.
 
   \begin{readmore}
-  For the functions @{text "assume"}, @{text "forall_elim"} etc 
-  see \isccite{sec:thms}. The basic functions for theorems are defined in
+  The basic functions for theorems are defined in
   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   \end{readmore}
 
@@ -1191,10 +1189,10 @@
   term stands for the theorem to be presented; the output can be constructed to
   ones wishes.  Let us, for example, assume we want to quote theorems without
   leading @{text \<forall>}-quantifiers. For this we can implement the following function 
-  that strips off meta-quantifiers.
+  that strips off @{text "\<forall>"}s.
 *}
 
-ML %linenosgray {*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
+ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
       Term.dest_abs body |> snd |> strip_allq
   | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = 
       strip_allq t
@@ -1243,7 +1241,7 @@
   and uses them as name in the outermost abstractions.
 *}
 
-ML {*fun rename_allq [] t = t
+ML{*fun rename_allq [] t = t
   | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
       Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
   | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
@@ -1506,6 +1504,49 @@
   \end{readmore}
 *}
 
+section {* Theories\label{sec:theories} (TBD) *}
+
+
+text {*
+  Theories are the most fundamental building blocks in Isabelle. They 
+  contain definitions, syntax declarations, axioms, proofs etc. If a definition
+  is stated, it must be stored in a theory in order to be usable later
+  on. Similar with proofs: once a proof is finished, the proved theorem
+  needs to be stored in the theorem database of the theory in order to
+  be usable. All relevant data of a theort can be querried as follows.
+
+  \begin{isabelle}
+  \isacommand{print\_theory}\\
+  @{text "> names: Pure Code_Generator HOL \<dots>"}\\
+  @{text "> classes: Inf < type \<dots>"}\\
+  @{text "> default sort: type"}\\
+  @{text "> syntactic types: #prop \<dots>"}\\
+  @{text "> logical types: 'a \<times> 'b \<dots>"}\\
+  @{text "> type arities: * :: (random, random) random \<dots>"}\\
+  @{text "> logical constants: == :: 'a \<Rightarrow> 'a \<Rightarrow> prop \<dots>"}\\
+  @{text "> abbreviations: \<dots>"}\\
+  @{text "> axioms: \<dots>"}\\
+  @{text "> oracles: \<dots>"}\\
+  @{text "> definitions: \<dots>"}\\
+  @{text "> theorems: \<dots>"}
+  \end{isabelle}
+
+  \begin{center}
+  \begin{tikzpicture}
+  \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A};
+  \end{tikzpicture}
+  \end{center}
+
+
+  In contrast to an ordinary theory, which simply consists of a type
+  signature, as well as tables for constants, axioms and theorems, a local
+  theory contains additional context information, such as locally fixed
+  variables and local assumptions that may be used by the package. The type
+  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
+  @{ML_type "Proof.context"}, although not every proof context constitutes a
+  valid local theory.
+*}
+
 section {* Setups (TBD) *}
 
 text {*
@@ -1559,21 +1600,6 @@
   the current simpset.
 *}
 
-section {* Theories\label{sec:theories} (TBD) *}
-
-text {*
-  There are theories, proof contexts and local theories (in this order, if you
-  want to order them). 
-
-  In contrast to an ordinary theory, which simply consists of a type
-  signature, as well as tables for constants, axioms and theorems, a local
-  theory contains additional context information, such as locally fixed
-  variables and local assumptions that may be used by the package. The type
-  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
-  @{ML_type "Proof.context"}, although not every proof context constitutes a
-  valid local theory.
-*}
-
 section {* Contexts (TBD) *}
 
 section {* Local Theories (TBD) *}

--- a/ProgTutorial/Intro.thy	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/Intro.thy	Sun Oct 25 15:26:03 2009 +0100
@@ -27,7 +27,7 @@
   then this tutorial is for you. It will guide you through the first steps of
   Isabelle programming, and also explain tricks of the trade. We also hope
   the tutorial will encourage researchers to play with Isabelle and implement
-  new ideas. The sources of Isabelle can look intimidating, but beginners 
+  new ideas. The source code of Isabelle can look intimidating, but beginners 
   can get by with knowledge of only a small number functions and a few basic
   coding conventions.
 

--- a/ProgTutorial/Package/Ind_Code.thy	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Oct 25 15:26:03 2009 +0100
@@ -135,8 +135,8 @@
 
 local_setup %gray {* fn lthy =>
 let
-  val def = defn_aux lthy fresh_orules 
-                             [fresh_pred] (fresh_pred, fresh_arg_tys)
+  val arg = (fresh_pred, fresh_arg_tys)
+  val def = defn_aux lthy fresh_orules [fresh_pred] arg
 in
   tracing (string_of_term lthy def); lthy
 end *}
@@ -239,9 +239,12 @@
   quantifiers. 
 *}
 
-ML{*fun inst_spec ctrm = 
-  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] 
-    @{thm spec}*}
+ML{*fun inst_spec ctrm =
+let
+  val cty = ctyp_of_term ctrm
+in 
+  Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} 
+end*}
 
 text {*
   This helper function uses the function @{ML_ind instantiate' in Drule}
@@ -613,10 +616,10 @@
 *}
 ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
 let 
-  val s = ["Params1 from the rule:", string_of_cterms ctxt params1] 
-        @ ["Params2 from the predicate:", string_of_cterms ctxt params2] 
-        @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) 
-        @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) 
+ val s = ["Params1 from the rule:", string_of_cterms ctxt params1] 
+       @ ["Params2 from the predicate:", string_of_cterms ctxt params2] 
+       @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) 
+       @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) 
 in 
   s |> cat_lines
     |> tracing

--- a/ProgTutorial/Tactical.thy	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun Oct 25 15:26:03 2009 +0100
@@ -331,8 +331,30 @@
   misinterpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   @{term C} intact, with the exception of possibly instantiating schematic
-  variables. If you use the predefined tactics, which we describe in the next
-  section, this will always be the case.
+  variables. The instantiations of schematic variables can even be observed 
+  on the user level. For this consider the following definition and proof.
+*}
+
+definition 
+  EQ_TRUE 
+where
+  "EQ_TRUE X \<equiv> (X = True)"
+
+lemma test: 
+  shows "EQ_TRUE ?X"
+  unfolding EQ_TRUE_def
+  by (rule refl)
+
+text {*
+  Although Isabelle issues a warning message when stating goals involving 
+  meta-variables, it is possible to prove this theorem. The reason for the warning 
+  message is that the proved theorem is not @{text "EQ_TRUE ?X"}, as one might 
+  expect, but @{thm test}:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{thm [source] test}\\
+  @{text ">"}~@{thm test}
+  \end{isabelle}
  
   \begin{readmore}
   For more information about the internals of goals see \isccite{sec:tactical-goals}.

--- a/ProgTutorial/document/root.tex	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/document/root.tex	Sun Oct 25 15:26:03 2009 +0100
@@ -17,6 +17,8 @@
 \usepackage{makeidx}
 \usepackage{index}
 \usepackage{tocbibind}
+\usepackage{tikz}
+\usetikzlibrary{shadows}
 \usepackage{pdfsetup}
 
 

Binary file progtutorial.pdf has changed