1 theory Ind_Examples

     2 imports Main

     3 begin

     4 

     5 section{* Examples of inductive definitions *}

     6 

     7 text {*

     8 \label{sec:ind-examples}

     9 In this section, we will give three examples showing how to define inductive

    10 predicates by hand and prove characteristic properties such as introduction

    11 rules and an induction rule. From these examples, we will then figure out a

    12 general method for defining inductive predicates, which will be described in

    13 \S\ref{sec:ind-general-method}. This description will serve as a basis for the

    14 actual implementation to be developed in \S\ref{sec:ind-interface} -- \S\ref{sec:ind-proofs}.

    15 It should be noted that our aim in this section is not to write proofs that

    16 are as beautiful as possible, but as close as possible to the ML code producing

    17 the proofs that we will develop later.

    18 As a first example, we consider the \emph{transitive closure} @{text "trcl R"}

    19 of a relation @{text R}. It is characterized by the following

    20 two introduction rules

    21 \[

    22 \begin{array}{l}

    23 @{term "trcl R x x"} \\

    24 @{term [mode=no_brackets] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}

    25 \end{array}

    26 \]

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

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

    29 the second and third parameter changes in the ``recursive call''.

    30 Since an inductively defined predicate is the \emph{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 above rules. This gives rise to a definition containing

    34 a universal quantifier over the predicate @{text P}:

    35 *}

    36 

    37 definition "trcl \<equiv> \<lambda>R x y.

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

    39 

    40 text {*

    41 \noindent

    42 Since the predicate @{term "trcl R x y"} yields an element of the type of object

    43 level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the

    44 above introduction rules have to be converted to object-level implications

    45 @{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"}

    46 rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over

    47 the variable parameters of the introduction rules. Isabelle already offers some

    48 infrastructure for converting between meta-level and object-level connectives,

    49 which we will use later on.

    50 

    51 With this definition of the transitive closure, the proof of the (weak) induction

    52 theorem is almost immediate. It suffices to convert all the meta-level connectives

    53 in the induction rule to object-level connectives using the @{text atomize} proof

    54 method, expand the definition of @{text trcl}, eliminate the universal quantifier

    55 contained in it, and then solve the goal by assumption.

    56 *}

    57 

    58 lemma trcl_induct:

    59   assumes trcl: "trcl R x y"

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

    61   apply (atomize (full))

    62   apply (cut_tac trcl)

    63   apply (unfold trcl_def)

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

    65   apply assumption

    66   done

    67 (*<*)

    68 lemma "trcl R x x"

    69   apply (unfold trcl_def)

    70   apply (rule allI impI)+

    71 (*>*)

    72 txt {*

    73 \noindent

    74 The above induction rule is \emph{weak} in the sense that the induction step may

    75 only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not

    76 using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule

    77 containing this additional assumption can be derived from the weaker one with the

    78 help of the introduction rules for @{text trcl}.

    79 

    80 We now turn to the proofs of the introduction rules, which are slightly more complicated.

    81 In order to prove the first introduction rule, we again unfold the definition and

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

    83 We then end up in a proof state of the following form:

    84 @{subgoals [display]}

    85 The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been

    86 replaced by @{term "P"}. Thus, all we have to do is to eliminate the universal quantifier

    87 in front of the first assumption, and then solve the goal by assumption:

    88 *}

    89 (*<*)oops(*>*)

    90 lemma trcl_base: "trcl R x x"

    91   apply (unfold trcl_def)

    92   apply (rule allI impI)+

    93   apply (drule spec)

    94   apply assumption

    95   done

    96 (*<*)

    97 lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

    98   apply (unfold trcl_def)

    99   apply (rule allI impI)+

   100 (*>*)

   101 txt {*

   102 \noindent

   103 Since the second introduction rule has premises, its proof is not as easy as the previous

   104 one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"}

   105 and @{text "\<longrightarrow>"}, we get the proof state

   106 @{subgoals [display]}

   107 The third and fourth assumption corresponds to the first and second introduction rule,

   108 respectively, whereas the first and second assumption corresponds to the premises of

   109 the introduction rule. Since we want to prove the second introduction rule, we apply

   110 the fourth assumption to the goal @{term "P x z"}. In order for the assumption to

   111 be applicable, we have to eliminate the universal quantifiers and turn the object-level

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

   113 attribute. Applying the assumption produces two new subgoals, which can be solved using

   114 the first and second assumption. The second assumption again involves a quantifier and

   115 implications that have to be eliminated before it can be applied. To avoid problems

   116 with higher order unification, it is advisable to provide an instantiation for the

   117 universally quantified predicate variable in the assumption.

   118 *}

   119 (*<*)oops(*>*)

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

   121   apply (unfold trcl_def)

   122   apply (rule allI impI)+

   123   proof -

   124     case goal1

   125     show ?case

   126       apply (rule goal1(4) [rule_format])

   127       apply (rule goal1(1))

   128       apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp,

   129 	OF goal1(3-4)])

   130       done

   131   qed

   132 

   133 text {*

   134 \noindent

   135 This method of defining inductive predicates easily generalizes to mutually inductive

   136 predicates, like the predicates @{text even} and @{text odd} characterized by the

   137 following introduction rules:

   138 \[

   139 \begin{array}{l}

   140 @{term "even (0::nat)"} \\

   141 @{term "odd m \<Longrightarrow> even (Suc m)"} \\

   142 @{term "even m \<Longrightarrow> odd (Suc m)"}

   143 \end{array}

   144 \]

   145 Since the predicates are mutually inductive, each of the definitions contain two

   146 quantifiers over the predicates @{text P} and @{text Q}.

   147 *}

   148 

   149 definition "even \<equiv> \<lambda>n.

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

   151 

   152 definition "odd \<equiv> \<lambda>n.

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

   154 

   155 text {*

   156 \noindent

   157 For proving the induction rule, we use exactly the same technique as in the transitive

   158 closure example:

   159 *}

   160 

   161 lemma even_induct:

   162   assumes even: "even n"

   163   shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   164   apply (atomize (full))

   165   apply (cut_tac even)

   166   apply (unfold even_def)

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

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

   169   apply assumption

   170   done

   171 

   172 text {*

   173 \noindent

   174 A similar induction rule having @{term "Q n"} as a conclusion can be proved for

   175 the @{text odd} predicate.

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

   177 previous example. We only show the proof of the second introduction rule,

   178 since it is almost the same as the one for the third introduction rule,

   179 and the proof of the first rule is trivial.

   180 *}

   181 

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

   183   apply (unfold odd_def even_def)

   184   apply (rule allI impI)+

   185   proof -

   186     case goal1

   187     show ?case

   188       apply (rule goal1(3) [rule_format])

   189       apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],

   190 	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])

   191       done

   192   qed

   193 (*<*)

   194 lemma even0: "even 0"

   195   apply (unfold even_def)

   196   apply (rule allI impI)+

   197   apply assumption

   198   done

   199 

   200 lemma oddS: "even m \<Longrightarrow> odd (Suc m)"

   201   apply (unfold odd_def even_def)

   202   apply (rule allI impI)+

   203   proof -

   204     case goal1

   205     show ?case

   206       apply (rule goal1(4) [rule_format])

   207       apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],

   208 	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])

   209       done

   210   qed

   211 (*>*)

   212 text {*

   213 \noindent

   214 As a final example, we will consider the definition of the accessible

   215 part of a relation @{text R} characterized by the introduction rule

   216 \[

   217 @{term "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}

   218 \]

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

   220 definition of @{text accpart} is as follows:

   221 *}

   222 

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

   224 

   225 text {*

   226 \noindent

   227 The proof of the induction theorem is again straightforward:

   228 *}

   229 

   230 lemma accpart_induct:

   231   assumes acc: "accpart R x"

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

   233   apply (atomize (full))

   234   apply (cut_tac acc)

   235   apply (unfold accpart_def)

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

   237   apply assumption

   238   done

   239 (*<*)

   240 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   241   apply (unfold accpart_def)

   242   apply (rule allI impI)+

   243 (*>*)

   244 txt {*

   245 \noindent

   246 Proving the introduction rule is a little more complicated, due to the quantifier

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

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

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

   250 yields the following proof state:

   251 @{subgoals [display]}

   252 Applying the second assumption produces a proof state with the new local assumption

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

   254 first assumption.

   255 *}

   256 (*<*)oops(*>*)

   257 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   258   apply (unfold accpart_def)

   259   apply (rule allI impI)+

   260   proof -

   261     case goal1

   262     note goal1' = this

   263     show ?case

   264       apply (rule goal1'(2) [rule_format])

   265       proof -

   266         case goal1

   267         show ?case

   268 	  apply (rule goal1'(1) [OF goal1, THEN spec [where x=P],

   269             THEN mp, OF goal1'(2)])

   270 	  done

   271       qed

   272     qed

   273 

   274 end