--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Package/Ind_Prelims.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -0,0 +1,351 @@
+theory Ind_Prelims
+imports Main LaTeXsugar"../Base" Simple_Inductive_Package
+begin
+
+section{* Preliminaries *}
+  
+text {*
+  On the Isabelle level, the user will just give a specification of an
+  inductive predicate and 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. This will roughly 
+  mean that the package has three main parts, namely:
+
+
+  \begin{itemize}
+  \item parsing the specification and typing the parsed input,
+  \item making the definitions and deriving the reasoning infrastructure, and
+  \item storing the results in the theory. 
+  \end{itemize}
+
+  Before we start with explaining all parts,
+  let us first give three examples showing how to define inductive predicates
+  by hand and then also how to prove by hand important properties about
+  them. 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.
+
+  We first consider the transitive closure of a relation @{text R}. It is
+  an inductive predicate characterised by the two introduction rules:
+
+  \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}
+
+  In Isabelle 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 {*
+  As said above the package has to make an appropriate definition and provide
+  lemmas to reason about the predicate @{term trcl\<iota>}. 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
+  @{text P} closed under the rules above. This gives rise to the definition
+*}
+
+definition "trcl \<equiv> 
+     \<lambda>R x y. \<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}. 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 
+  should use the meta-connectives since they simplify the
+  reasoning for the user.
+
+  With this definition, the proof of the induction principle for @{term trcl}
+  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 @{term 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 rules are slightly more complicated. 
+  For the first one, we need to prove the following lemma:
+*}
+
+lemma %linenos trcl_base: 
+  shows "trcl R x x"
+apply(unfold trcl_def)
+apply(rule allI impI)+
+apply(drule spec)
+apply(assumption)
+done
+
+text {*
+  We again unfold first the definition and apply introduction rules 
+  for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible (Lines 3 and 4).
+  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. 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).
+*}
+
+text {*
+  Next we have to show that the second introduction rule also follows from the
+  definition.  Since this rule has premises, the proof is a bit more
+  involved. After unfolding the definitions and applying the introduction
+  rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
+*}
+
+lemma trcl_step: 
+  shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+apply (unfold trcl_def)
+apply (rule allI impI)+
+
+txt {* 
+  we obtain the goal state
+
+  @{subgoals [display]} 
+
+  To see better where we are, let us explicitly name the assumptions 
+  by starting a subproof.
+*}
+
+proof -
+  case (goal1 P)
+  have p1: "R x y" by fact
+  have p2: "\<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 r1: "\<forall>x. P x x" by fact
+  have r2: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
+  show "P x z"
+  
+txt {*
+  The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of
+  the second introduction rule; the assumptions @{text "r1"} and @{text "r2"}
+  correspond to the introduction rules. We apply @{text "r2"} 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. So we continue the proof with:
+
+*}
+
+    apply (rule r2[rule_format])
+
+txt {*
+  This gives us two new subgoals
+
+  @{subgoals [display]} 
+
+  which can be solved using assumptions @{text p1} and @{text p2}. The latter
+  involves a quantifier and implications that have to be eliminated before it
+  can be applied. To avoid potential problems with higher-order unification,
+  we explicitly instantiate the quantifier to @{text "P"} and also match
+  explicitly the implications with @{text "r1"} and @{text "r2"}. This gives
+  the proof:
+*}
+
+    apply(rule p1)
+    apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])
+    done
+qed
+
+text {*
+  Now we are done. 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: 
+  shows "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}\small
+  @{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}
+  
+  The user will state for this inductive definition the specification:
+*}
+
+simple_inductive
+  even\<iota> and odd\<iota>
+where
+  even0: "even\<iota> 0"
+| evenS: "odd\<iota> n \<Longrightarrow> even\<iota> (Suc n)"
+| oddS: "even\<iota> n \<Longrightarrow> odd\<iota> (Suc n)"
+
+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 \<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 \<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"
+
+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 {*
+  The only difference with the proof @{text "trcl_induct"} is that we have to
+  instantiate here two universal quantifiers.  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 %linenos evenS: 
+  shows "odd m \<Longrightarrow> even (Suc m)"
+apply (unfold odd_def even_def)
+apply (rule allI impI)+
+proof -
+  case (goal1 P)
+  have p1: "\<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 r1: "P 0" by fact
+  have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact
+  have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact
+  show "P (Suc m)"
+    apply(rule r2[rule_format])
+    apply(rule p1[THEN spec[where x=P], THEN spec[where x=Q],
+	           THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])
+    done
+qed
+
+text {*
+  In Line 13, we apply the assumption @{text "r2"} (since we prove the second
+  introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if
+  the second introduction rule had more premises we have to do that for all
+  of them). In order for this assumption to be applicable, the quantifiers
+  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} characterised 
+  by the introduction rule
+  
+  \begin{center}\small
+  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
+  \end{center}
+
+  whose premise involves a universal quantifier and an implication. 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"
+
+text {*
+  The proof of the induction principle is again straightforward.
+*}
+
+lemma accpart_induct:
+  assumes asm: "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 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. The proof is as follows.
+*}
+
+lemma %linenos accpartI: 
+  shows "(\<And>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 p1: "\<And>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 r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
+  show "P x"
+    apply(rule r1[rule_format])
+    proof -
+      case (goal1 y)
+      have r1_prem: "R y x" by fact
+      show "P y"
+	apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
+      done
+  qed
+qed
+
+text {*
+  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 above (Line 14). This local assumption will be used to solve
+  the goal @{term "P y"} using the 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.
+
+*}
+
+end