--- a/CookBook/Package/Ind_Examples.thy	Thu Feb 19 14:44:53 2009 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,317 +0,0 @@
-theory Ind_Examples
-imports Main LaTeXsugar
-begin
-
-section{* Examples of Inductive Definitions \label{sec:ind-examples} *}
-
-text {*
-  Let us first give three examples showing how to define inductive
-  predicates by hand and then also how to prove by hand characteristic properties
-  about them, such as introduction rules and induction principles. 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 later.
-
-
-  As a first example, let us consider the transitive closure of a relation @{text
-  R}. It is an inductive predicate characterised by the two introduction rules:
-
-  \begin{center}
-  @{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}
-
-  Note that the @{text trcl} predicate has two different kinds of parameters: the
-  first parameter @{text R} stays \emph{fixed} throughout the definition, whereas
-  the second and third parameter changes in the ``recursive call''. This will
-  become important later on when we deal with fixed parameters and locales. 
-
-  Since an inductively defined predicate is the least predicate closed under
-  a collection of introduction rules, we define the predicate @{text "trcl R x y"} in
-  such a way that it holds if and only if @{text "P x y"} holds for every predicate
-  @{text P} closed under the rules above. This gives rise to the definition 
-*}
-
-definition "trcl R x y \<equiv> 
-      \<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 x y"
-
-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 (there is no other way for definitions in
-  HOL). However, 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, the proof of the induction principle for the transitive
-  closure 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 @{text trcl}
-  (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7),
-  and then solve the goal by assumption (Line 8).
-
-*}
-
-lemma %linenos trcl_induct:
-  assumes asm: "trcl R x y"
-  shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
-apply(atomize (full))
-apply(cut_tac asm)
-apply(unfold trcl_def)
-apply(drule spec[where x=P])
-apply(assumption)
-done
-
-text {*
-  The proofs for the introduction are slightly more complicated. We need to prove
-  the facs @{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 fact, 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 the goal state:
-*}
-
-(*<*)lemma "trcl R x x"
-apply (unfold trcl_def)
-apply (rule allI impI)+(*>*)
-txt {* @{subgoals [display]} *}
-(*<*)oops(*>*)
-
-text {*
-  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. Thus the proof is:
-*}
-
-lemma trcl_base: "trcl R x x"
-apply(unfold trcl_def)
-apply(rule allI impI)+
-apply(drule spec)
-apply(assumption)
-done
-
-text {*
-  Since the second @{text trcl}-rule has premises, the proof of its
-  introduction rule 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)+(*>*)
-txt {*@{subgoals [display]} *}
-(*<*)oops(*>*)
-
-text {*
-  The third and fourth assumption correspond 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 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 available in
-  Isabelle for proving this lemmas. After all @{text "blast"} would easily 
-  dispense of it.
-*}
-
-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
-  @{text blast}, @{text auto} 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 whenever something goes wrong. Therefore if possible, automatic 
-  tactics should be avoided or sufficiently constrained.
-
-  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} characterised by the following
-  rules:
- 
-  \begin{center}
-  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
-  @{prop[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
-  @{prop[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
-  \end{center}
-  
-  Since the predicates are mutually inductive, each definition 
-  quantifies over both predicates, below named @{text P} and @{text Q}.
-*}
-
-definition "even n \<equiv> 
-  \<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 n \<equiv>
-  \<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"
-
-text {*
-  For proving the induction principles, we use exactly the same technique 
-  as in the transitive closure example, namely:
-*}
-
-lemma even_induct:
-  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 asm)
-apply(unfold even_def)
-apply(drule spec[where x=P])
-apply(drule spec[where x=Q])
-apply(assumption)
-done
-
-text {*
-  We omit the other induction principle that has @{term "Q n"} as conclusion.
-  The proofs of the introduction rules are also very similar to the ones in the
-  @{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 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 define the 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"}
-  \end{center}
-
-  whose premise involves a universal quantifier and an implication. The
-  definition of @{text accpart} is:
-*}
-
-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 principle is again straightforward.
-*}
-
-lemma accpart_induct:
-  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
-
-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 goal state:
-*}
-
-(*<*)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 goal 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.
-*}
-
-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 {*
-  (FIXME check that the code works like as indicated)
-
-  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. For this 
-  it is instructive to look at the general construction principle 
-  of inductive definitions, which we shall do in the next section.
-*}
-
-end