theory Ind_Prelims

imports Main LaTeXsugar"../Base" Simple_Inductive_Package

section{* Preliminaries *}

  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

  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"

  where we quantify over the predicate @{text P}. We have to use the

  HOL). However, the introduction rules and induction principles 

  should use the meta-connectives since they simplify the

  With this definition, the proof of the induction principle for @{term trcl}

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

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

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

  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 (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.

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

  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"

  \begin{center}\small

  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"

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

  have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

  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

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

  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.

  \begin{center}\small

  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}

definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"

  shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"

  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"

  have p1: "\<And>y. R y x \<Longrightarrow> 

  have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact

    apply(rule r1[rule_format])

      have r1_prem: "R y x" by fact

	apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])

  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"}.

  should do in order to solve all inductive definitions we throw at them.

  This is usually the first step in writing a package.