theory Ind_Prelims

imports Main LaTeXsugar"../Base" Simple_Inductive_Package

begin

section{* Preliminaries *}

text {*

  expects from the package to produce a convenient reasoning

  infrastructure. This infrastructure needs to be derived from the definition

  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{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}

*}

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 {*

  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 {*

  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),

*}

lemma %linenos trcl_induct:

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: 

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 {*

*}

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: 

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

  @{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: 

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 

  The method of defining inductive predicates by impredicative quantification

  also generalises to mutually inductive predicates. The next example defines

*}

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:

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

*}

lemma %linenos evenS: 

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 {*

  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.

  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 {*

*}

lemma %linenos accpartI: 

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 {*

  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(*>*)