diff -r 13fd0a83d3c3 -r 039845fc96bd CookBook/Package/Ind_Examples.thy
--- a/CookBook/Package/Ind_Examples.thy	Fri Feb 13 09:57:08 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy	Fri Feb 13 14:15:28 2009 +0000
@@ -6,13 +6,14 @@
 
 text {*
   Let us first give three examples showing how to define inductive predicates
-  by hand and prove characteristic properties such as introduction rules and
-  an induction rule. From these examples, we will then figure out a general
-  method for defining inductive predicates.  The aim in this section is not to
-  write proofs that are as beautiful as possible, but as close as possible to
-  the ML-code producing the proofs that we will develop later.
+  by hand and then how to prove characteristic properties about them, such as 
+  introduction rules and an induction principle. From these examples, we will 
+  figure out a 
+  general method for defining inductive predicates.  The aim in this section is 
+  not to write proofs that are as beautiful as possible, but as close as 
+  possible to the ML-code producing the proofs that we will develop later.
 
-  As a first example, we consider the transitive closure of a relation @{text
+  As a first example, let us consider the transitive closure of a relation @{text
   R}. It is an inductive predicate characterized by the two introduction rules
 
   \begin{center}
@@ -38,15 +39,17 @@
 text {*
   where we quantify over the predicate @{text P}. Note that we have to use the
   object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating
-  this definition. 
+  this definition. The introduction rules and induction principles derived later
+  should use the corresponding meta-connectives since they simplify the reasoning for
+  the user.
 
-  With this definition of the transitive closure, the proof of the induction
-  theorem is almost immediate. It suffices to convert all the meta-level connectives
-  in the induction rule to object-level connectives using the @{text atomize} proof
-  method, expand the definition of @{text trcl}, eliminate the universal quantifier
-  contained in it, and then solve the goal by assumption.
+  With this definition, the proof of the induction theorem for the transitive
+  closure is almost immediate. It suffices to convert all the meta-level
+  connectives in the induction rule to object-level connectives using the
+  @{text atomize} proof method (Line 4), expand the definition of @{text trcl}
+  (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7),
+  and then solve the goal by assumption (Line 8).
 
-  (FIXME: add linenumbers to the proof below and the text above)
 *}
 
 lemma %linenos trcl_induct:
@@ -60,16 +63,17 @@
 done
 
 text {*
-  We now turn to the proofs of the introduction rules, which are slightly more complicated.
-  In order to prove the first introduction rule, we again unfold the definition and
+  The proofs for the introduction are slightly more complicated. We need to prove
+  the goals @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}.
+  In order to prove the first goal, we again unfold the definition and
   then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.
-  We then end up in a proof state of the following form:
+  We then end up in the goal state
 
 *}
 
 (*<*)lemma "trcl R x x"
-  apply (unfold trcl_def)
-  apply (rule allI impI)+(*>*)
+apply (unfold trcl_def)
+apply (rule allI impI)+(*>*)
 txt {* @{subgoals [display]} *}
 (*<*)oops(*>*)
 
@@ -77,10 +81,9 @@
   The two assumptions correspond to the introduction rules, where @{text "trcl
   R"} has been replaced by P. Thus, all we have to do is to eliminate the
   universal quantifier in front of the first assumption, and then solve the
-  goal by assumption:
+  goal by assumption. Thus the proof is:
 *}
 
-
 lemma trcl_base: "trcl R x x"
 apply(unfold trcl_def)
 apply(rule allI impI)+
@@ -89,54 +92,90 @@
 done
 
 text {*
-  Since the second introduction rule has premises, its proof is not as easy as the previous
-  one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"}
-  and @{text "\<longrightarrow>"}, we get the proof state
+  Since the second introduction rule has premises, its proof is not as easy. After unfolding 
+  the definitions and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we 
+  get the goal state
 *}
 
-
 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
-  apply (unfold trcl_def)
-  apply (rule allI impI)+(*>*)
+apply (unfold trcl_def)
+apply (rule allI impI)+(*>*)
 txt {*@{subgoals [display]} *}
 (*<*)oops(*>*)
 
 text {*
-  The third and fourth assumption corresponds to the first and second introduction rule,
-  respectively, whereas the first and second assumption corresponds to the premises of
-  the introduction rule. Since we want to prove the second introduction rule, we apply
-  the fourth assumption to the goal @{term "P x z"}. In order for the assumption to
-  be applicable, we have to eliminate the universal quantifiers and turn the object-level
-  implications into meta-level ones. This can be accomplished using the @{text rule_format}
-  attribute. Applying the assumption produces two new subgoals, which can be solved using
-  the first and second assumption. The second assumption again involves a quantifier and
-  implications that have to be eliminated before it can be applied. To avoid problems
-  with higher order unification, it is advisable to provide an instantiation for the
-  universally quantified predicate variable in the assumption.
+  The third and fourth assumption corresponds to the first and second
+  introduction rule, respectively, whereas the first and second assumption
+  corresponds to the pre\-mises of the introduction rule. Since we want to prove
+  the second introduction rule, we apply the fourth assumption to the goal
+  @{term "P x z"}. In order for the 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. Applying the assumption produces the two new subgoals
+*}
+
+(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+apply (unfold trcl_def)
+apply (rule allI impI)+
+proof -
+  case (goal1 P)
+  have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
+  show ?case
+    apply (rule a4[rule_format])(*>*)
+txt {*@{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {* 
+  which can be
+  solved using the first and second assumption. The second assumption again
+  involves a quantifier and an implications that have to be eliminated before it
+  can be applied. To avoid potential problems with higher-order unification, 
+  we should explcitly instantiate the universally quantified
+  predicate variable to @{text "P"} and also match explicitly the implications
+  with the the third and fourth assumption. This gives the proof:
 *}
 
 
 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
-  apply (unfold trcl_def)
-  apply (rule allI impI)+
-  proof -
-    case (goal1 P)
-    have g1: "R x y" by fact
-    have g2: "\<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact
-    have g3: "\<forall>x. P x x" by fact
-    have g4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
-    show ?case
-      apply (rule g4 [rule_format])
-      apply (rule g1)
-      apply (rule g2 [THEN spec [where x=P], THEN mp, THEN mp, OF g3, OF g4])
-      done
-  qed
+apply(unfold trcl_def)
+apply(rule allI impI)+
+proof -
+  case (goal1 P)
+  have a1: "R x y" by fact
+  have a2: "\<forall>P. (\<forall>x. P x x) 
+                  \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact
+  have a3: "\<forall>x. P x x" by fact
+  have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
+  show "P x z"
+    apply(rule a4[rule_format])
+    apply(rule a1)
+    apply(rule a2 [THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4])
+    done
+qed
 
 text {*
+  It might be surprising that we are not using the automatic tactics in
+  Isabelle in order to prove the lemmas we are after. After all @{text "blast"}
+  would easily dispense of the lemmas.
+*}
 
-  This method of defining inductive predicates easily generalizes to mutually inductive
-  predicates, like the predicates @{text even} and @{text odd} characterized by the
-  following introduction rules:
+lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+apply(unfold trcl_def)
+apply(blast)
+done
+
+text {*
+  Experience has shown that it is generally a bad idea to rely heavily on @{term blast}
+  and the like in automated proofs. The reason is that you do not have precise control 
+  over them (the user can, for example, declare new intro- or simplification rules that 
+  can throw automatic tactics off course) and also it is very hard to debug
+  proofs involving automatic tactics. Therefore whenever possible, automatic tactics
+  should be avoided or constrained. 
+  
+
+  This method of defining inductive predicates generalises also to mutually inductive
+  predicates. The next example defines the predicates @{text even} and @{text odd} 
+  characterised by the following rules:
  
   \begin{center}
   @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm}
@@ -144,8 +183,8 @@
   @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
   \end{center}
   
-  Since the predicates are mutually inductive, each of the definitions contain two
-  quantifiers over the predicates @{text P} and @{text Q}.
+  Since the predicates are mutually inductive, each definition 
+  quantifies over both predicates, below named @{text P} and @{text Q}.
 *}
 
 definition "even n \<equiv> 
@@ -162,60 +201,43 @@
 *}
 
 lemma even_induct:
-  assumes even: "even n"
+  assumes asm: "even n"
   shows "P 0 \<Longrightarrow> 
              (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
-  apply (atomize (full))
-  apply (cut_tac even)
-  apply (unfold even_def)
-  apply (drule spec [where x=P])
-  apply (drule spec [where x=Q])
-  apply assumption
-  done
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold even_def)
+apply(drule spec[where x=P])
+apply(drule spec[where x=Q])
+apply(assumption)
+done
 
 text {*
-  A similar induction rule having @{term "Q n"} as a conclusion can be proved for
-  the @{text odd} predicate.
+  We omit the other induction rule having @{term "Q n"} as conclusion.
   The proofs of the introduction rules are also very similar to the ones in the
-  previous example. We only show the proof of the second introduction rule,
-  since it is almost the same as the one for the third introduction rule,
-  and the proof of the first rule is trivial.
+  @{text "trcl"}-example. We only show the proof of the second introduction rule:
 *}
 
 lemma evenS: "odd m \<Longrightarrow> even (Suc m)"
-  apply (unfold odd_def even_def)
-  apply (rule allI impI)+
-  proof -
-    case goal1
-    show ?case
-      apply (rule goal1(3) [rule_format])
-      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
-	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
-      done
-  qed
-(*<*)
-lemma even0: "even 0"
-  apply (unfold even_def)
-  apply (rule allI impI)+
-  apply assumption
-  done
-
-lemma oddS: "even m \<Longrightarrow> odd (Suc m)"
-  apply (unfold odd_def even_def)
-  apply (rule allI impI)+
-  proof -
-    case goal1
-    show ?case
-      apply (rule goal1(4) [rule_format])
-      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
-	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
-      done
-  qed
-(*>*)
+apply (unfold odd_def even_def)
+apply (rule allI impI)+
+proof -
+  case (goal1 P)
+  have a1: "\<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 m" by fact
+  have a2: "P 0" by fact
+  have a3: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact
+  have a4: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact
+  show "P (Suc m)"
+    apply(rule a3[rule_format])
+    apply(rule a1[THEN spec[where x=P], THEN spec[where x=Q],
+	THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4])
+    done
+qed
 
 text {*
-  As a final example, we will consider the definition of the accessible
-  part of a relation @{text R} characterized by the introduction rule
+  As a final example, we definethe accessible part of a relation @{text R} characterised 
+  by the introduction rule
   
   \begin{center}
   @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
@@ -228,53 +250,63 @@
 definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
 
 text {*
-  The proof of the induction theorem is again straightforward:
+  The proof of the induction theorem is again straightforward.
 *}
 
 lemma accpart_induct:
-  assumes acc: "accpart R x"
-  shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
-  apply (atomize (full))
-  apply (cut_tac acc)
-  apply (unfold accpart_def)
-  apply (drule spec [where x=P])
-  apply assumption
-  done
-(*<*)
-lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
-  apply (unfold accpart_def)
-  apply (rule allI impI)+
-(*>*)
+  assumes asm: "accpart R x"
+  shows "(\<And>x. (\<forall>y. R y x \<longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold accpart_def)
+apply(drule spec[where x=P])
+apply(assumption)
+done
 
-txt {*
-
-  Proving the introduction rule is a little more complicated, due to the quantifier
+text {*
+  Proving the introduction rule is a little more complicated, because the quantifier
   and the implication in the premise. We first convert the meta-level universal quantifier
   and implication to their object-level counterparts. Unfolding the definition of
   @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
   yields the following proof state:
-  @{subgoals [display]}
+*}
+
+(*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+apply (unfold accpart_def)
+apply (rule allI impI)+(*>*)
+txt {* @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
   Applying the second assumption produces a proof state with the new local assumption
   @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the
   first assumption.
 *}
-(*<*)oops(*>*)
 
-lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
-  apply (unfold accpart_def)
-  apply (rule allI impI)+
-  proof -
-    case goal1
-    note goal1' = this
-    show ?case
-      apply (rule goal1'(2) [rule_format])
-      proof -
-        case goal1
-        show ?case
-	  apply (rule goal1'(1) [OF goal1, THEN spec [where x=P],
-            THEN mp, OF goal1'(2)])
-	  done
-      qed
-    qed
+lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+apply (unfold accpart_def)
+apply (rule allI impI)+
+proof -
+  case (goal1 P)
+  have a1: "\<forall>y. R y x \<longrightarrow> 
+                   (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
+  have a2: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
+  show "P x"
+    apply(rule a2[rule_format])
+    proof -
+      case (goal1 y)
+      have a3: "R y x" by fact
+      show "P y"
+      apply(rule a1[THEN spec[where x=y], THEN mp, OF a3, 
+            THEN spec[where x=P], THEN mp, OF a2])
+      done
+  qed
+qed
+
+text {*
+  Now the point is to figure out what the automatic proofs should do. For
+  this it might be instructive to look at the general construction principle
+  of inductive definitions, which we shall do next.
+*}
 
 end