isabelle-cookbook: comparison ProgTutorial/Package/Ind_General

equal deleted inserted replaced

-:db8e302f44c8
+:d5accbc67e1b
 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
 | fresh_lam1: "fresh a (Lam a t)"
 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 (*>*)
-section {* The Code in a Nutshell *}
+section {* The Code in a Nutshell\label{sec:nutshell} *}
 text {*
 (FIXME: perhaps move somewhere else)
 The point of these examples is to get a feeling what the automatic proofs
 The inductive package will generate the reasoning infrastructure
 for mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
 follows we will have the convention that various, possibly empty collections of
 ``things'' are indicated either by adding an @{text "s"} or by adding
 a superscript @{text [quotes] "\<^isup>*"}. The shorthand for the predicates
-will therefore be @{text "preds"} or @{text "pred\<^sup>*"}. In this case of the
+will therefore be @{text "preds"} or @{text "pred\<^sup>*"}. In the case of the
-predicates there must be at least a single one in order to obtain a meaningful
+predicates there must be, of course, at least a single one in order to obtain a
-definition.
+meaningful definition.
-The input for the inductive predicate will be some @{text "preds"} with possible
+The input for the inductive package will be some @{text "preds"} with possible
 typing and syntax annotations, and also some introduction rules. We call below the
 introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle
-notation, one such @{text "rule"} is of the form
+notation, one such @{text "rule"} is assumed to be of the form
 \begin{isabelle}
 @{text "rule ::=
 \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow>
 \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*\<^raw:}}_{\text{\rm recursive premises}}$>
 \<Longrightarrow> pred ts"}
 \end{isabelle}
-We actually assume the user will always state rules of this form and we omit
+For the purposes here, we will assume the @{text rules} have
-any code that test this format. So things can go horribly wrong if the
+this format and omit any code that actually tests this. Therefore ``things''
-@{text "rules"} are not of this form.\footnote{FIXME: Exercise to test this
+can go horribly wrong, if the @{text "rules"} are not of this
-format.} The @{text As} and @{text Bs} in a @{text "rule"} are formulae not
+form.\footnote{FIXME: Exercise to test this format.} The @{text As} and
-involving the inductive predicates @{text "preds"}; the instances @{text
+@{text Bs} in a @{text "rule"} are formulae not involving the inductive
-"pred ss"} and @{text "pred ts"} can stand for different predicates.
+predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred
-Everything left of @{text [quotes] "\<Longrightarrow> pred ts"} are called the premises of
+ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and
-the rule. The variables @{text "xs"} are usually omitted in the user's
+@{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the
-input. The variables @{text "ys"} are local with respect to on recursive
+arguments of the predicates. Every formula left of @{text [quotes]
-premise. Some examples of @{text "rule"}s the user might write are:
+"\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified
+variables @{text "xs"} are usually omitted in the user's input. The
+quantification for the variables @{text "ys"} is local with respect to
+one recursive premise and must be given. Some examples of @{text "rule"}s
+are
 @{thm [display] fresh_var[no_vars]}
 which has only a single non-recursive premise, whereas
 has a single recursive premise; the rule
 @{thm [display] accpartI[no_vars]}
-has a recursive premise which has a precondition. In the examples, all
+has a recursive premise that has a precondition. As usual all
 rules are stated without the leading meta-quantification @{text "\<And>xs"}.
-The code of the inductive package falls roughly in tree parts involving
+The code of the inductive package falls roughly in tree parts: the first
-the definitions, the induction principles and the introduction rules,
+deals with the definitions, the second with the induction principles and
-respectively. For the definitions we need to have the @{text rules}
+the third with the introduction rules.
-in a form where the meta-quantifiers and meta-implications are replaced
-by their object logic equivalent. Therefore an @{text "orule"} is of the
+For the definitions we need to have the @{text rules} in a form where
-form
+the meta-quantifiers and meta-implications are replaced by their object
+logic equivalents. Therefore an @{text "orule"} is of the form
 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
 A definition for the predicate @{text "pred"} has then the form
 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
-The induction principles for the predicate @{text "pred"} are of the
+The induction principles for every predicate @{text "pred"} are of the
 form
 @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
-where in the @{text "rules"} every @{text pred} is replaced by a new
+where in the @{text "rules"} every @{text pred} is replaced by a fresh
-(meta)variable @{text "?P"}.
+meta-variable @{text "?P"}.
-In order to derive an induction principle for the predicate @{text "pred"}
+In order to derive an induction principle for the predicate @{text "pred"},
-we first transform it into the object logic and fix the meta-variables. Hence
+we first transform @{text ind} into the object logic and fix the meta-variables.
-we have to prove a formula of the form
+Hence we have to prove a formula of the form
 @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}
 If we assume @{text "pred zs"} and unfold its definition, then we have
 and must prove
 @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
-This can be done by instantiating the @{text "\<forall>preds"} with the @{text "Ps"}.
+This can be done by instantiating the @{text "\<forall>preds"}-quantification
-Then we are done since we are left with a simple identity.
+with the @{text "Ps"}. Then we are done since we are left with a simple
+identity.
-The proofs for the introduction rules are more involved. Assuming we want to
-prove the introduction rule
+Although the user declares introduction rules @{text rules}, they must
+be derived from the @{text defs}. These derivations are a bit involved.
+Assuming we want to prove the introduction rule
 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 then we can assume
 @{text [display] "pred ts"}
 In the last step we removed some quantifiers and moved the precondition @{text "orules"}
 into the assumtion. The @{text "orules"} stand for all introduction rules that are given
-by the user. We apply the one which corresponds to introduction rule we are proving.
+by the user. We apply the @{text orule} that corresponds to introduction rule we are
-This introduction rule must be of the form
+proving. This introduction rule must necessarily be of the form
 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 When we apply this rule we end up in the goal state where we have to prove
 \begin{isabelle}
 (a)~@{text "As"}\\
 (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
 \end{isabelle}
-The goals @{text "As"} we can immediately discharge with the assumption in @{text "(i)"}.
+We can immediately discharge the goals @{text "As"} using the assumption in
-The goals in @{text "(b)"} we discharge as follows: we assume the @{text "(iv)"}
+@{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we
-@{text "Bs"} and prove @{text "(c)"} @{text "pred ss"}. We then resolve the
+assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the
-@{text "Bs"}  with the assumptions in @{text "(ii)"}. This gives us
+@{text "Bs"}  with the assumptions in @{text "(ii)"}. This gives us the
+assumptions
 @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}
 Instantiating the universal quantifiers and then resolving with the assumptions
 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after.
+This completes the proof for introduction rules.
-What remains is to implement the reasoning outlined above.
+What remains is to implement the reasoning outlined above. We do this in
-For building testcases, we use some shorthands for the definitions
+the next section. For building testcases, we use the shorthands for
-of @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}.
+@{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
+given in Figure~\ref{fig:shorthands}.
 *}
 text_raw{*
 \begin{figure}[p]
 (* accessible-part example *)
 val acc_rules =
 [@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}]
-val acc_pred = @{term "accpart:: ('a \<Rightarrow>'a\<Rightarrow>bool)\<Rightarrow>'a \<Rightarrow>bool"}*}
+val acc_pred = @{term "accpart::('a \<Rightarrow>'a\<Rightarrow>bool)\<Rightarrow>'a \<Rightarrow>bool"}*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
-\caption{Shorthands for the inductive predicates of @{text "even"}-@{text "odd"},
+\caption{Shorthands for the inductive predicates @{text "even"}-@{text "odd"},
-@{text "fresh"} and @{text "accpart"}. The follow the convention @{text "rules"},
+@{text "fresh"} and @{text "accpart"}. The names of these shorthands follow
-@{text "orules"}, @{text "preds"} and so on as used in Section ???. The purpose
+the convention @{text "rules"}, @{text "orules"}, @{text "preds"} and so on.
-of these shorthands is to simplify the construction of testcases.}
+The purpose of these shorthands is to simplify the construction of testcases
+in Section~\ref{sec:code}.\label{fig:shorthands}}
 \end{figure}
 *}

changeset 211	d5accbc67e1b
parent 210	db8e302f44c8
child 212	ac01ddb285f6