theory Ind_Prelims
imports Main LaTeXsugar"../Base" Simple_Inductive_Package
begin

section{* Preliminaries *}
  
text {*
  The user will just give a specification of inductive predicate(s) 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(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.

  \begin{figure}[t]
  \begin{boxedminipage}{\textwidth}
  \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
  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 {*
  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 associated with the transitive closure 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}
  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 @{text assumption} (Line 8).

*}

lemma %linenos trcl_induct:
assumes "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 prems)
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 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).
*}

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 (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
  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 be constrained sufficiently.

  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:
*}

simple_inductive
  even and odd
where
  even0: "even 0"
| evenS: "odd n \<Longrightarrow> even (Suc n)"
| oddS: "even n \<Longrightarrow> odd (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\<iota> \<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>
  \<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 "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 prems)
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 @{prop "even n"} as premise and @{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 Q)
  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 {*
  The interesting lines are 7 to 15. The assumptions fall into to 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
  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}
  (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:
*}

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 and omitted.
  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 {*
  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"}.

  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
  the parsing and typing part of the package.

*}
(*<*)end(*>*)