1 theory Ind_Prelims

     2 imports Main LaTeXsugar"../Base" Simple_Inductive_Package

     3 begin

     4 

     5 section{* Preliminaries *}

     6   

     7 text {*

     8   The user will just give a specification of an inductive predicate and

     9   expects from the package to produce a convenient reasoning

    10   infrastructure. This infrastructure needs to be derived from the definition

    11   that correspond to the specified predicate. This will roughly mean that the

    12   package has three main parts, namely:

    13 

    14 

    15   \begin{itemize}

    16   \item parsing the specification and typing the parsed input,

    17   \item making the definitions and deriving the reasoning infrastructure, and

    18   \item storing the results in the theory. 

    19   \end{itemize}

    20 

    21   Before we start with explaining all parts, let us first give three examples

    22   showing how to define inductive predicates by hand and then also how to

    23   prove by hand important properties about them. From these examples, we will

    24   figure out a general method for defining inductive predicates.  The aim in

    25   this section is \emph{not} to write proofs that are as beautiful as

    26   possible, but as close as possible to the ML-code we will develop in later

    27   sections.

    28 

    29 

    30   We first consider the transitive closure of a relation @{text R}. It is

    31   an inductive predicate characterised by the two introduction rules:

    32 

    33   \begin{center}\small

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

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

    36   \end{center}

    37 

    38   In Isabelle, the user will state for @{term trcl\<iota>} the specification:

    39 *}

    40 

    41 simple_inductive

    42   trcl\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

    43 where

    44   base: "trcl\<iota> R x x"

    45 | step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"

    46 

    47 text {*

    48   As said above the package has to make an appropriate definition and provide

    49   lemmas to reason about the predicate @{term trcl\<iota>}. Since an inductively

    50   defined predicate is the least predicate closed under a collection of

    51   introduction rules, the predicate @{text "trcl R x y"} can be defined so

    52   that it holds if and only if @{text "P x y"} holds for every predicate

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

    54 *}

    55 

    56 definition "trcl \<equiv> 

    57      \<lambda>R x y. \<forall>P. (\<forall>x. P x x) 

    58                   \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"

    59 

    60 text {*

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

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

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

    64   HOL). However, the introduction rules and induction principles 

    65   should use the meta-connectives since they simplify the

    66   reasoning for the user.

    67 

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

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

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

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

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

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

    74 

    75 *}

    76 

    77 lemma %linenos trcl_induct:

    78   assumes "trcl R x y"

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

    80 apply(atomize (full))

    81 apply(cut_tac prems)

    82 apply(unfold trcl_def)

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

    84 apply(assumption)

    85 done

    86 

    87 text {*

    88   The proofs for the introduction rules are slightly more complicated. 

    89   For the first one, we need to prove the following lemma:

    90 *}

    91 

    92 lemma %linenos trcl_base: 

    93   shows "trcl R x x"

    94 apply(unfold trcl_def)

    95 apply(rule allI impI)+

    96 apply(drule spec)

    97 apply(assumption)

    98 done

    99 

   100 text {*

   101   We again unfold first the definition and apply introduction rules 

   102   for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible (Lines 3 and 4).

   103   We then end up in the goal state:

   104 *}

   105 

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

   107 apply (unfold trcl_def)

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

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

   110 (*<*)oops(*>*)

   111 

   112 text {*

   113   The two assumptions correspond to the introduction rules. Thus, all we have

   114   to do is to eliminate the universal quantifier in front of the first

   115   assumption (Line 5), and then solve the goal by assumption (Line 6).

   116 *}

   117 

   118 text {*

   119   Next we have to show that the second introduction rule also follows from the

   120   definition.  Since this rule has premises, the proof is a bit more

   121   involved. After unfolding the definitions and applying the introduction

   122   rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}

   123 *}

   124 

   125 lemma trcl_step: 

   126   shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   127 apply (unfold trcl_def)

   128 apply (rule allI impI)+

   129 

   130 txt {* 

   131   we obtain the goal state

   132 

   133   @{subgoals [display]} 

   134 

   135   To see better where we are, let us explicitly name the assumptions 

   136   by starting a subproof.

   137 *}

   138 

   139 proof -

   140   case (goal1 P)

   141   have p1: "R x y" by fact

   142   have p2: "\<forall>P. (\<forall>x. P x x) 

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

   144   have r1: "\<forall>x. P x x" by fact

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

   146   show "P x z"

   147   

   148 txt {*

   149   The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of

   150   the second introduction rule; the assumptions @{text "r1"} and @{text "r2"}

   151   correspond to the introduction rules. We apply @{text "r2"} to the goal

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

   153   have to eliminate the universal quantifier and turn the object-level

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

   155   rule_format} attribute. So we continue the proof with:

   156 

   157 *}

   158 

   159     apply (rule r2[rule_format])

   160 

   161 txt {*

   162   This gives us two new subgoals

   163 

   164   @{subgoals [display]} 

   165 

   166   which can be solved using assumptions @{text p1} and @{text p2}. The latter

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

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

   169   we explicitly instantiate the quantifier to @{text "P"} and also match

   170   explicitly the implications with @{text "r1"} and @{text "r2"}. This gives

   171   the proof:

   172 *}

   173 

   174     apply(rule p1)

   175     apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])

   176     done

   177 qed

   178 

   179 text {*

   180   Now we are done. It might be surprising that we are not using the automatic

   181   tactics available in Isabelle for proving this lemmas. After all @{text

   182   "blast"} would easily dispense of it.

   183 *}

   184 

   185 lemma trcl_step_blast: 

   186   shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   187 apply(unfold trcl_def)

   188 apply(blast)

   189 done

   190 

   191 text {*

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

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

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

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

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

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

   198   tactics should be avoided or sufficiently constrained.

   199 

   200   The method of defining inductive predicates by impredicative quantification

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

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

   203   rules:

   204  

   205   \begin{center}\small

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

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

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

   209   \end{center}

   210   

   211   The user will state for this inductive definition the specification:

   212 *}

   213 

   214 simple_inductive

   215   even and odd

   216 where

   217   even0: "even 0"

   218 | evenS: "odd n \<Longrightarrow> even (Suc n)"

   219 | oddS: "even n \<Longrightarrow> odd (Suc n)"

   220 

   221 text {*

   222   Since the predicates @{term even} and @{term odd} are mutually inductive, each 

   223   corresponding definition must quantify over both predicates (we name them 

   224   below @{text "P"} and @{text "Q"}).

   225 *}

   226 

   227 definition "even\<iota> \<equiv> 

   228   \<lambda>n. \<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> P n"

   230 

   231 definition "odd\<iota> \<equiv>

   232   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

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

   234 

   235 text {*

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

   237   as in the transitive closure example, namely:

   238 *}

   239 

   240 lemma even_induct:

   241   assumes "even n"

   242   shows "P 0 \<Longrightarrow> 

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

   244 apply(atomize (full))

   245 apply(cut_tac prems)

   246 apply(unfold even_def)

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

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

   249 apply(assumption)

   250 done

   251 

   252 text {*

   253   The only difference with the proof @{text "trcl_induct"} is that we have to

   254   instantiate here two universal quantifiers.  We omit the other induction

   255   principle that has @{term "Q n"} as conclusion.  The proofs of the

   256   introduction rules are also very similar to the ones in the @{text

   257   "trcl"}-example. We only show the proof of the second introduction rule.

   258 

   259 *}

   260 

   261 lemma %linenos evenS: 

   262   shows "odd m \<Longrightarrow> even (Suc m)"

   263 apply (unfold odd_def even_def)

   264 apply (rule allI impI)+

   265 proof -

   266   case (goal1 P Q)

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

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

   269   have r1: "P 0" by fact

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

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

   272   show "P (Suc m)"

   273     apply(rule r2[rule_format])

   274     apply(rule p1[THEN spec[where x=P], THEN spec[where x=Q],

   275 	           THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])

   276     done

   277 qed

   278 

   279 text {*

   280   In Line 13, we apply the assumption @{text "r2"} (since we prove the second

   281   introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if

   282   the second introduction rule had more premises we have to do that for all

   283   of them). In order for this assumption to be applicable, the quantifiers

   284   need to be instantiated and then also the implications need to be resolved

   285   with the other rules.

   286 

   287 

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

   289   by the introduction rule

   290   

   291   \begin{center}\small

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

   293   \end{center}

   294 

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

   296   definition of @{text accpart} is:

   297 *}

   298 

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

   300 

   301 text {*

   302   The proof of the induction principle is again straightforward.

   303 *}

   304 

   305 lemma accpart_induct:

   306   assumes "accpart R x"

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

   308 apply(atomize (full))

   309 apply(cut_tac prems)

   310 apply(unfold accpart_def)

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

   312 apply(assumption)

   313 done

   314 

   315 text {*

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

   317   and the implication in the premise. The proof is as follows.

   318 *}

   319 

   320 lemma %linenos accpartI: 

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

   322 apply (unfold accpart_def)

   323 apply (rule allI impI)+

   324 proof -

   325   case (goal1 P)

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

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

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

   329   show "P x"

   330     apply(rule r1[rule_format])

   331     proof -

   332       case (goal1 y)

   333       have r1_prem: "R y x" by fact

   334       show "P y"

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

   336       done

   337   qed

   338 qed

   339 

   340 text {*

   341   In Line 11, applying the assumption @{text "r1"} generates a goal state with

   342   the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the 

   343   proof above (Line 14). This local assumption is used to solve

   344   the goal @{term "P y"} with the help of assumption @{text "p1"}.

   345 

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

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

   348   This is usually the first step in writing a package. We next explain

   349   the parsing and typing part of the package.

   350 

   351 *}

   352 (*<*)end(*>*)