--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Mon Mar 30 17:40:20 2009 +0200
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Wed Apr 01 12:28:14 2009 +0100
@@ -1,23 +1,10 @@
 theory Ind_General_Scheme 
-imports Simple_Inductive_Package Ind_Prelims
+imports Ind_Interface
 begin
 
-(*<*)
-datatype trm =
-  Var "string"
-| App "trm" "trm"
-| Lam "string" "trm"
+section {* The Code in a Nutshell\label{sec:nutshell} *}
 
-simple_inductive 
-  fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" 
-where
-  fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"
-| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
-| fresh_lam1: "fresh a (Lam a t)"
-| fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
-(*>*)
 
-section {* The Code in a Nutshell\label{sec:nutshell} *}
 
 text {*
   The inductive package will generate the reasoning infrastructure for
@@ -70,13 +57,11 @@
   has a single recursive premise that has a precondition. As usual all 
   rules are stated without the leading meta-quantification @{text "\<And>xs"}.
 
-  The code of the inductive package falls roughly in tree parts: the first
-  deals with the definitions, the second with the induction principles and 
-  the third with the introduction rules. 
-  
-  For the definitions we need to have the @{text rules} in a form where 
-  the meta-quantifiers and meta-implications are replaced by their object 
-  logic equivalents. Therefore an @{text "orule"} is of the form 
+  The output of the inductive package will be definitions for the predicates, 
+  induction principles and introduction rules.  For the definitions we need to have the
+  @{text rules} in a form where the meta-quantifiers and meta-implications are
+  replaced by their object logic equivalents. Therefore an @{text "orule"} is
+  of the form
 
   @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
 
@@ -111,13 +96,13 @@
   with the @{text "Ps"}. Then we are done since we are left with a simple 
   identity.
   
-  Although the user declares introduction rules @{text rules}, they must 
+  Although the user declares the introduction rules @{text rules}, they must 
   also be derived from the @{text defs}. These derivations are a bit involved. 
   Assuming we want to prove the introduction rule 
 
   @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
-  then we can have assumptions of the form
+  then we have assumptions of the form
 
   \begin{isabelle}
   (i)~~@{text "As"}\\
@@ -143,7 +128,8 @@
   In the last step we removed some quantifiers and moved the precondition @{text "orules"}  
   into the assumtion. The @{text "orules"} stand for all introduction rules that are given 
   by the user. We apply the @{text orule} that corresponds to introduction rule we are 
-  proving. This introduction rule must necessarily be of the form 
+  proving. After lifting to the meta-connectives, this introduction rule must necessarily 
+  be of the form 
 
   @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
@@ -167,10 +153,10 @@
   in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after.
   This completes the proof for introduction rules.
 
-  What remains is to implement the reasoning outlined in this section. We do this  
-  next. For building testcases, we use the shorthands for 
+  What remains is to implement in Isabelle the reasoning outlined in this section. 
+  We will describe the code in the next section. For building testcases, we use the shorthands for 
   @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
-  given in Figure~\ref{fig:shorthands}.
+  defined in Figure~\ref{fig:shorthands}.
 *}