1 theory Ind_Prelims

     2 imports Main LaTeXsugar"../Base" Simple_Inductive_Package

     3 begin

     4 

     5 section{* Preliminaries *}

     6   

     7 text {*

     8   On the Isabelle level, the user will just give a specification of an

     9   inductive predicate and expects from the package to produce a convenient

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

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

    12   mean that the 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,

    22   let us first give three examples showing how to define inductive predicates

    23   by hand and then also how to prove by hand important properties about

    24   them. From these examples, we will figure out a general method for defining

    25   inductive predicates.  The aim in this section is \emph{not} to write proofs

    26   that are as beautiful as possible, but as close as possible to the ML-code

    27   we will develop in later sections.

    28 

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

    30   an inductive predicate characterised by the two introduction rules:

    31 

    32   \begin{center}\small

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

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

    35   \end{center}

    36 

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

    38 *}

    39 

    40 simple_inductive

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

    42 where

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

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

    45 

    46 text {*

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

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

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

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

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

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

    53 *}

    54 

    55 definition "trcl \<equiv> 

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

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

    58 

    59 text {*

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

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

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

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

    64   should use the meta-connectives since they simplify the

    65   reasoning for the user.

    66 

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

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

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

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

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

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

    73 

    74 *}

    75 

    76 lemma %linenos trcl_induct:

    77   assumes asm: "trcl R x y"

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

    79 apply(atomize (full))

    80 apply(cut_tac asm)

    81 apply(unfold trcl_def)

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

    83 apply(assumption)

    84 done

    85 

    86 text {*

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

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

    89 *}

    90 

    91 lemma %linenos trcl_base: 

    92   shows "trcl R x x"

    93 apply(unfold trcl_def)

    94 apply(rule allI impI)+

    95 apply(drule spec)

    96 apply(assumption)

    97 done

    98 

    99 text {*

   100   We again unfold first the definition and apply introduction rules 

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

   102   We then end up in the goal state:

   103 *}

   104 

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

   106 apply (unfold trcl_def)

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

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

   109 (*<*)oops(*>*)

   110 

   111 text {*

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

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

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

   115 *}

   116 

   117 text {*

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

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

   120   involved. After unfolding the definitions and applying the introduction

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

   122 *}

   123 

   124 lemma trcl_step: 

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

   126 apply (unfold trcl_def)

   127 apply (rule allI impI)+

   128 

   129 txt {* 

   130   we obtain the goal state

   131 

   132   @{subgoals [display]} 

   133 

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

   135   by starting a subproof.

   136 *}

   137 

   138 proof -

   139   case (goal1 P)

   140   have p1: "R x y" by fact

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

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

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

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

   145   show "P x z"

   146   

   147 txt {*

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

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

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

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

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

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

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

   155 

   156 *}

   157 

   158     apply (rule r2[rule_format])

   159 

   160 txt {*

   161   This gives us two new subgoals

   162 

   163   @{subgoals [display]} 

   164 

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

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

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

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

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

   170   the proof:

   171 *}

   172 

   173     apply(rule p1)

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

   175     done

   176 qed

   177 

   178 text {*

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

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

   181   "blast"} would easily dispense of it.

   182 *}

   183 

   184 lemma trcl_step_blast: 

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

   186 apply(unfold trcl_def)

   187 apply(blast)

   188 done

   189 

   190 text {*

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

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

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

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

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

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

   197   tactics should be avoided or sufficiently constrained.

   198 

   199   The method of defining inductive predicates by impredicative quantification

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

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

   202   rules:

   203  

   204   \begin{center}\small

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

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

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

   208   \end{center}

   209   

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

   211 *}

   212 

   213 simple_inductive

   214   even\<iota> and odd\<iota>

   215 where

   216   even0: "even\<iota> 0"

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

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

   219 

   220 text {*

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

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

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

   224 *}

   225 

   226 definition "even \<equiv> 

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

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

   229 

   230 definition "odd \<equiv>

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

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

   233 

   234 text {*

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

   236   as in the transitive closure example, namely:

   237 *}

   238 

   239 lemma even_induct:

   240   assumes asm: "even n"

   241   shows "P 0 \<Longrightarrow> 

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

   243 apply(atomize (full))

   244 apply(cut_tac asm)

   245 apply(unfold even_def)

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

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

   248 apply(assumption)

   249 done

   250 

   251 text {*

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

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

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

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

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

   257 

   258 *}

   259 

   260 lemma %linenos evenS: 

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

   262 apply (unfold odd_def even_def)

   263 apply (rule allI impI)+

   264 proof -

   265   case (goal1 P)

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

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

   268   have r1: "P 0" by fact

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

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

   271   show "P (Suc m)"

   272     apply(rule r2[rule_format])

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

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

   275     done

   276 qed

   277 

   278 text {*

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

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

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

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

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

   284   with the other rules.

   285 

   286 

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

   288   by the introduction rule

   289   

   290   \begin{center}\small

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

   292   \end{center}

   293 

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

   295   definition of @{text accpart} is:

   296 *}

   297 

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

   299 

   300 text {*

   301   The proof of the induction principle is again straightforward.

   302 *}

   303 

   304 lemma accpart_induct:

   305   assumes asm: "accpart R x"

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

   307 apply(atomize (full))

   308 apply(cut_tac asm)

   309 apply(unfold accpart_def)

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

   311 apply(assumption)

   312 done

   313 

   314 text {*

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

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

   317 *}

   318 

   319 lemma %linenos accpartI: 

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

   321 apply (unfold accpart_def)

   322 apply (rule allI impI)+

   323 proof -

   324   case (goal1 P)

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

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

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

   328   show "P x"

   329     apply(rule r1[rule_format])

   330     proof -

   331       case (goal1 y)

   332       have r1_prem: "R y x" by fact

   333       show "P y"

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

   335       done

   336   qed

   337 qed

   338 

   339 text {*

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

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

   342   proof above (Line 14). This local assumption will be used to solve

   343   the goal @{term "P y"} using the assumption @{text "p1"}.

   344 

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

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

   347   This is usually the first step in writing a package.

   348 

   349 *}

   350 

   351 end