1 theory Ind_Examples

     2 imports Main LaTeXsugar

     3 begin

     4 

     5 section{* Examples of Inductive Definitions \label{sec:ind-examples} *}

     6 

     7 text {*

     8   Let us first give three examples showing how to define inductive

     9   predicates by hand and then also how to prove by hand characteristic properties

    10   about them, such as introduction rules and induction principles. From

    11   these examples, we will figure out a general method for defining inductive

    12   predicates.  The aim in this section is \emph{not} to write proofs that are as

    13   beautiful as possible, but as close as possible to the ML-code we will 

    14   develop later.

    15 

    16 

    17   As a first example, let us consider the transitive closure of a relation @{text

    18   R}. It is an inductive predicate characterised by the two introduction rules:

    19 

    20   \begin{center}

    21   @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}

    22   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}

    23   \end{center}

    24 

    25   Note that the @{text trcl} predicate has two different kinds of parameters: the

    26   first parameter @{text R} stays \emph{fixed} throughout the definition, whereas

    27   the second and third parameter changes in the ``recursive call''. This will

    28   become important later on when we deal with fixed parameters and locales. 

    29 

    30   Since an inductively defined predicate is the least predicate closed under

    31   a collection of introduction rules, we define the predicate @{text "trcl R x y"} in

    32   such a way that it holds if and only if @{text "P x y"} holds for every predicate

    33   @{text P} closed under the rules above. This gives rise to the definition 

    34 *}

    35 

    36 definition "trcl R x y \<equiv> 

    37       \<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"

    38 

    39 text {*

    40   where we quantify over the predicate @{text P}. Note that we have to use the

    41   object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for

    42   stating this definition (there is no other way for definitions in

    43   HOL). However, the introduction rules and induction principles derived later

    44   should use the corresponding meta-connectives since they simplify the

    45   reasoning for the user.

    46 

    47   With this definition, the proof of the induction principle for the transitive

    48   closure is almost immediate. It suffices to convert all the meta-level

    49   connectives in the lemma to object-level connectives using the

    50   proof method @{text atomize} (Line 4), expand the definition of @{text trcl}

    51   (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7),

    52   and then solve the goal by assumption (Line 8).

    53 

    54 *}

    55 

    56 lemma %linenos trcl_induct:

    57   assumes asm: "trcl R x y"

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

    59 apply(atomize (full))

    60 apply(cut_tac asm)

    61 apply(unfold trcl_def)

    62 apply(drule spec[where x=P])

    63 apply(assumption)

    64 done

    65 

    66 text {*

    67   The proofs for the introduction are slightly more complicated. We need to prove

    68   the facs @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}.

    69   In order to prove the first fact, we again unfold the definition and

    70   then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.

    71   We then end up in the goal state:

    72 *}

    73 

    74 (*<*)lemma "trcl R x x"

    75 apply (unfold trcl_def)

    76 apply (rule allI impI)+(*>*)

    77 txt {* @{subgoals [display]} *}

    78 (*<*)oops(*>*)

    79 

    80 text {*

    81   The two assumptions correspond to the introduction rules, where @{text "trcl

    82   R"} has been replaced by P. Thus, all we have to do is to eliminate the

    83   universal quantifier in front of the first assumption, and then solve the

    84   goal by assumption. Thus the proof is:

    85 *}

    86 

    87 lemma trcl_base: "trcl R x x"

    88 apply(unfold trcl_def)

    89 apply(rule allI impI)+

    90 apply(drule spec)

    91 apply(assumption)

    92 done

    93 

    94 text {*

    95   Since the second @{text trcl}-rule has premises, the proof of its

    96   introduction rule is not as easy. After unfolding the definitions and

    97   applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we get the

    98   goal state:

    99 *}

   100 

   101 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   102 apply (unfold trcl_def)

   103 apply (rule allI impI)+(*>*)

   104 txt {*@{subgoals [display]} *}

   105 (*<*)oops(*>*)

   106 

   107 text {*

   108   The third and fourth assumption correspond to the first and second

   109   introduction rule, respectively, whereas the first and second assumption

   110   corresponds to the pre\-mises of the introduction rule. Since we want to prove

   111   the second introduction rule, we apply the fourth assumption to the goal

   112   @{term "P x z"}. In order for the assumption to be applicable as a rule, we have to

   113   eliminate the universal quantifier and turn the object-level implications

   114   into meta-level ones. This can be accomplished using the @{text rule_format}

   115   attribute. Applying the assumption produces the two new subgoals

   116 *}

   117 

   118 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   119 apply (unfold trcl_def)

   120 apply (rule allI impI)+

   121 proof -

   122   case (goal1 P)

   123   have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact

   124   show ?case

   125     apply (rule a4[rule_format])(*>*)

   126 txt {*@{subgoals [display]} *}

   127 (*<*)oops(*>*)

   128 

   129 text {* 

   130   which can be

   131   solved using the first and second assumption. The second assumption again

   132   involves a quantifier and an implications that have to be eliminated before it

   133   can be applied. To avoid potential problems with higher-order unification, 

   134   we should explcitly instantiate the universally quantified

   135   predicate variable to @{text "P"} and also match explicitly the implications

   136   with the the third and fourth assumption. This gives the proof:

   137 *}

   138 

   139 

   140 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   141 apply(unfold trcl_def)

   142 apply(rule allI impI)+

   143 proof -

   144   case (goal1 P)

   145   have a1: "R x y" by fact

   146   have a2: "\<forall>P. (\<forall>x. P x x) 

   147                   \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact

   148   have a3: "\<forall>x. P x x" by fact

   149   have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact

   150   show "P x z"

   151     apply(rule a4[rule_format])

   152     apply(rule a1)

   153     apply(rule a2[THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4])

   154     done

   155 qed

   156 

   157 text {*

   158   It might be surprising that we are not using the automatic tactics available in

   159   Isabelle for proving this lemmas. After all @{text "blast"} would easily 

   160   dispense of it.

   161 *}

   162 

   163 lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   164 apply(unfold trcl_def)

   165 apply(blast)

   166 done

   167 

   168 text {*

   169   Experience has shown that it is generally a bad idea to rely heavily on

   170   @{text blast}, @{text auto} and the like in automated proofs. The reason is

   171   that you do not have precise control over them (the user can, for example,

   172   declare new intro- or simplification rules that can throw automatic tactics

   173   off course) and also it is very hard to debug proofs involving automatic

   174   tactics whenever something goes wrong. Therefore if possible, automatic 

   175   tactics should be avoided or sufficiently constrained.

   176 

   177   The method of defining inductive predicates by impredicative quantification

   178   also generalises to mutually inductive predicates. The next example defines

   179   the predicates @{text even} and @{text odd} characterised by the following

   180   rules:

   181  

   182   \begin{center}

   183   @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}

   184   @{prop[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}

   185   @{prop[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}

   186   \end{center}

   187   

   188   Since the predicates are mutually inductive, each definition 

   189   quantifies over both predicates, below named @{text P} and @{text Q}.

   190 *}

   191 

   192 definition "even n \<equiv> 

   193   \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

   194              \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"

   195 

   196 definition "odd n \<equiv>

   197   \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

   198              \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"

   199 

   200 text {*

   201   For proving the induction principles, we use exactly the same technique 

   202   as in the transitive closure example, namely:

   203 *}

   204 

   205 lemma even_induct:

   206   assumes asm: "even n"

   207   shows "P 0 \<Longrightarrow> 

   208              (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   209 apply(atomize (full))

   210 apply(cut_tac asm)

   211 apply(unfold even_def)

   212 apply(drule spec[where x=P])

   213 apply(drule spec[where x=Q])

   214 apply(assumption)

   215 done

   216 

   217 text {*

   218   We omit the other induction principle that has @{term "Q n"} as conclusion.

   219   The proofs of the introduction rules are also very similar to the ones in the

   220   @{text "trcl"}-example. We only show the proof of the second introduction rule.

   221 *}

   222 

   223 lemma evenS: "odd m \<Longrightarrow> even (Suc m)"

   224 apply (unfold odd_def even_def)

   225 apply (rule allI impI)+

   226 proof -

   227   case (goal1 P)

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

   229                              \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact

   230   have a2: "P 0" by fact

   231   have a3: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact

   232   have a4: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact

   233   show "P (Suc m)"

   234     apply(rule a3[rule_format])

   235     apply(rule a1[THEN spec[where x=P], THEN spec[where x=Q],

   236 	THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4])

   237     done

   238 qed

   239 

   240 text {*

   241   As a final example, we define the accessible part of a relation @{text R} characterised 

   242   by the introduction rule

   243   

   244   \begin{center}

   245   @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}

   246   \end{center}

   247 

   248   whose premise involves a universal quantifier and an implication. The

   249   definition of @{text accpart} is:

   250 *}

   251 

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

   253 

   254 text {*

   255   The proof of the induction principle is again straightforward.

   256 *}

   257 

   258 lemma accpart_induct:

   259   assumes asm: "accpart R x"

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

   261 apply(atomize (full))

   262 apply(cut_tac asm)

   263 apply(unfold accpart_def)

   264 apply(drule spec[where x=P])

   265 apply(assumption)

   266 done

   267 

   268 text {*

   269   Proving the introduction rule is a little more complicated, because the quantifier

   270   and the implication in the premise. We first convert the meta-level universal quantifier

   271   and implication to their object-level counterparts. Unfolding the definition of

   272   @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}

   273   yields the following goal state:

   274 *}

   275 

   276 (*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   277 apply (unfold accpart_def)

   278 apply (rule allI impI)+(*>*)

   279 txt {* @{subgoals [display]} *}

   280 (*<*)oops(*>*)

   281 

   282 text {*

   283   Applying the second assumption produces a goal state with the new local assumption

   284   @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the

   285   first assumption.

   286 *}

   287 

   288 lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   289 apply (unfold accpart_def)

   290 apply (rule allI impI)+

   291 proof -

   292   case (goal1 P)

   293   have a1: "\<forall>y. R y x \<longrightarrow> 

   294                    (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact

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

   296   show "P x"

   297     apply(rule a2[rule_format])

   298     proof -

   299       case (goal1 y)

   300       have a3: "R y x" by fact

   301       show "P y"

   302       apply(rule a1[THEN spec[where x=y], THEN mp, OF a3, 

   303             THEN spec[where x=P], THEN mp, OF a2])

   304       done

   305   qed

   306 qed

   307 

   308 text {*

   309   (FIXME check that the code works like as indicated)

   310 

   311   The point of these examples is to get a feeling what the automatic proofs 

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

   313   it is instructive to look at the general construction principle 

   314   of inductive definitions, which we shall do in the next section.

   315 *}

   316 

   317 end