
diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Package/Ind_Prelims.thy
--- a/ProgTutorial/Package/Ind_Prelims.thy	Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Wed Apr 01 12:26:56 2009 +0100
@@ -1,5 +1,5 @@
 theory Ind_Prelims
-imports Main LaTeXsugar"../Base" Simple_Inductive_Package
+imports Main LaTeXsugar "../Base" 
 begin
 
 section{* Preliminaries *}
@@ -9,55 +9,25 @@
   expects from the package to produce a convenient reasoning
   infrastructure. This infrastructure needs to be derived from the definition
   that correspond to the specified predicate(s). Before we start with
-  explaining all parts of the package, let us first give four examples showing
-  how to define inductive predicates by hand and then also how to prove by
-  hand properties about them. See Figure \ref{fig:paperpreds} for their usual
-  ``pencil-and-paper'' definitions. From these examples, we will
-  figure out a general method for defining inductive predicates.  The aim in
-  this section is \emph{not} to write proofs that are as beautiful as
-  possible, but as close as possible to the ML-code we will develop in later
-  sections.
+  explaining all parts of the package, let us first give some examples 
+  showing how to define inductive predicates and then also how
+  to generate a reasoning infrastructure for them. From the examples 
+  we will figure out a general method for
+  defining inductive predicates.  The aim in this section is \emph{not} to
+  write proofs that are as beautiful as possible, but as close as possible to
+  the ML-code we will develop in later sections.
 
-  \begin{figure}[t]
-  \begin{boxedminipage}{\textwidth}
+
+
+  We first consider the transitive closure of a relation @{text R}. The 
+  ``pencil-and-paper'' specification for the transitive closure is:
+
   \begin{center}\small
   @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}
   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
   \end{center}
-  \begin{center}\small
-  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
-  @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}
-  @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}
-  \end{center}
-  \begin{center}\small
-  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
-  \end{center}
-  \begin{center}\small
-  @{prop[mode=Rule] "a\<noteq>b \<Longrightarrow> fresh a (Var b)"}\hspace{5mm}
-  @{prop[mode=Rule] "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"}\\[2mm]
-  @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm}
-  @{prop[mode=Rule] "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
-  \end{center}
-  \end{boxedminipage}
-  \caption{Examples of four ``Pencil-and-paper'' definitions of inductively defined
-  predicates. In formal reasoning with Isabelle, the user just wants to give such 
-  definitions and expects that the reasoning structure is derived automatically. 
-  For this definitional packages need to be implemented.\label{fig:paperpreds}}
-  \end{figure}
 
-  We first consider the transitive closure of a relation @{text R}. The user will 
-  state for @{term trcl\<iota>} the specification:
-*}
-
-simple_inductive
-  trcl\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl\<iota> R x x"
-| step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"
-
-text {*
-  The package has to make an appropriate definition and provide
-  lemmas to reason about the predicate @{term trcl\<iota>}. Since an inductively
+  The package has to make an appropriate definition. Since an inductively
   defined predicate is the least predicate closed under a collection of
   introduction rules, the predicate @{text "trcl R x y"} can be defined so
   that it holds if and only if @{text "P x y"} holds for every predicate
@@ -79,7 +49,7 @@
   With this definition, the proof of the induction principle for @{term trcl}
   is almost immediate. It suffices to convert all the meta-level
   connectives in the lemma to object-level connectives using the
-  proof method @{text atomize} (Line 4), expand the definition of @{term trcl}
+  proof method @{text atomize} (Line 4 below), expand the definition of @{term trcl}
   (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),
   and then solve the goal by @{text assumption} (Line 8).
 
@@ -124,7 +94,7 @@
   The two assumptions come from the definition of @{term trcl} and correspond
   to the introduction rules. Thus, all we have to do is to eliminate the
   universal quantifier in front of the first assumption (Line 5), and then
-  solve the goal by assumption (Line 6).
+  solve the goal by @{text assumption} (Line 6).
 *}
 
 text {*
@@ -160,8 +130,8 @@
 txt {*
   The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of
   the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"}
-  come from the definition of @{term trcl} . We apply @{text "r2"} to the goal
-  @{term "P x z"}. In order for the assumption to be applicable as a rule, we
+  come from the definition of @{term trcl}. We apply @{text "r2"} to the goal
+  @{term "P x z"}. In order for this assumption to be applicable as a rule, we
   have to eliminate the universal quantifier and turn the object-level
   implications into meta-level ones. This can be accomplished using the @{text
   rule_format} attribute. So we continue the proof with:
@@ -211,28 +181,24 @@
 
   The method of defining inductive predicates by impredicative quantification
   also generalises to mutually inductive predicates. The next example defines
-  the predicates @{text even} and @{text odd}. The user will state for this 
-  inductive definition the specification:
-*}
+  the predicates @{text even} and @{text odd} given by
 
-simple_inductive
-  even and odd
-where
-  even0: "even 0"
-| evenS: "odd n \<Longrightarrow> even (Suc n)"
-| oddS: "even n \<Longrightarrow> odd (Suc n)"
+  \begin{center}\small
+  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
+  @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}
+  @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}
+  \end{center}
 
-text {*
   Since the predicates @{term even} and @{term odd} are mutually inductive, each 
   corresponding definition must quantify over both predicates (we name them 
   below @{text "P"} and @{text "Q"}).
 *}
 
-definition "even\<iota> \<equiv> 
+definition "even \<equiv> 
   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                  \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
 
-definition "odd\<iota> \<equiv>
+definition "odd \<equiv>
   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                  \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
 
@@ -280,7 +246,7 @@
 qed
 
 text {*
-  The interesting lines are 7 to 15. The assumptions fall into to categories:
+  The interesting lines are 7 to 15. The assumptions fall into two categories:
   @{text p1} corresponds to the premise of the introduction rule; @{text "r1"}
   to @{text "r3"} come from the definition of @{text "even"}.
   In Line 13, we apply the assumption @{text "r2"} (since we prove the second
@@ -290,10 +256,14 @@
   need to be instantiated and then also the implications need to be resolved
   with the other rules.
 
-  As a final example, we define the accessible part of a relation @{text R}
-  (see Figure~\ref{fig:paperpreds}). There the premsise of the introduction 
-  rule involves a universal quantifier and an implication. The
-  definition of @{text accpart} is:
+  Next we define the accessible part of a relation @{text R} given by
+  the single rule:
+
+  \begin{center}\small
+  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
+  \end{center}
+
+  The definition of @{text "accpart"} is:
 *}
 
 definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
@@ -325,15 +295,32 @@
 qed
 
 text {*
-  There are now two subproofs. The assumptions fall again into two categories (Lines
-  7 to 9). In Line 11, applying the assumption @{text "r1"} generates a goal state 
-  with the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the 
-  proof (Line 14). This local assumption is used to solve
-  the goal @{term "P y"} with the help of assumption @{text "p1"}.
+  As you can see, there are now two subproofs. The assumptions fall again into
+  two categories (Lines 7 to 9). In Line 11, applying the assumption @{text
+  "r1"} generates a goal state with the new local assumption @{term "R y x"},
+  named @{text "r1_prem"} in the second subproof (Line 14). This local assumption is
+  used to solve the goal @{term "P y"} with the help of assumption @{text
+  "p1"}.
+
 
-  The point of these examples is to get a feeling what the automatic proofs 
-  should do in order to solve all inductive definitions we throw at them.
-  This is usually the first step in writing a package. We next explain
+  \begin{exercise}
+  Give the definition for the freshness predicate for lambda-terms. The rules
+  for this predicate are:
+  
+  \begin{center}\small
+  @{prop[mode=Rule] "a\<noteq>b \<Longrightarrow> fresh a (Var b)"}\hspace{5mm}
+  @{prop[mode=Rule] "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"}\\[2mm]
+  @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm}
+  @{prop[mode=Rule] "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
+  \end{center}
+
+  From the definition derive the induction principle and the introduction 
+  rules. 
+  \end{exercise}
+
+  The point of all these examples is to get a feeling what the automatic
+  proofs should do in order to solve all inductive definitions we throw at
+  them.  This is usually the first step in writing a package. We next explain
   the parsing and typing part of the package.
 
 *}




