diff -r d5accbc67e1b -r ac01ddb285f6 ProgTutorial/Package/Ind_General_Scheme.thy --- a/ProgTutorial/Package/Ind_General_Scheme.thy Fri Mar 27 12:49:28 2009 +0000 +++ b/ProgTutorial/Package/Ind_General_Scheme.thy Fri Mar 27 18:19:42 2009 +0000 @@ -20,23 +20,15 @@ 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 - should do in order to solve all inductive definitions we throw at them. For this - it is instructive to look at the general construction principle - of inductive definitions, which we shall do in the next section. -*} - -text {* - The inductive package will generate the reasoning infrastructure - for mutually recursive predicates @{text "pred\<^isub>1\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 the case of the - predicates there must be, of course, at least a single one in order to obtain a - meaningful definition. + The inductive package will generate the reasoning infrastructure for + mutually recursive predicates @{text "pred\<^isub>1\pred\<^isub>n"}. In what + follows we will have the convention that various, possibly empty collections + of ``things'' (lists, nested implications and so on) are indicated either by + adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes] + "\<^isup>*"}. The shorthand for the predicates will therefore be @{text + "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must + be, of course, at least a single one in order to obtain a meaningful + definition. 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 @@ -54,11 +46,11 @@ this format and omit any code that actually tests this. Therefore ``things'' can go horribly wrong, if the @{text "rules"} are not of this form.\footnote{FIXME: Exercise to test this format.} The @{text As} and - @{text Bs} in a @{text "rule"} are formulae not involving the inductive + @{text Bs} in a @{text "rule"} stand for formulae not involving the inductive predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and @{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the - arguments of the predicates. Every formula left of @{text [quotes] + arguments of these predicates. Every formula left of @{text [quotes] "\ 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 @@ -75,7 +67,7 @@ @{thm [display] accpartI[no_vars]} - has a recursive premise that has a precondition. As usual all + has a single recursive premise that has a precondition. As usual all rules are stated without the leading meta-quantification @{text "\xs"}. The code of the inductive package falls roughly in tree parts: the first @@ -106,11 +98,12 @@ @{text [display] "pred zs \ orules[preds := Ps] \ P zs"} - If we assume @{text "pred zs"} and unfold its definition, then we have + If we assume @{text "pred zs"} and unfold its definition, then we have an + assumption @{text [display] "\preds. orules \ pred zs"} - and must prove + and must prove the goal @{text [display] "orules[preds := Ps] \ P zs"} @@ -119,23 +112,23 @@ identity. Although the user declares introduction rules @{text rules}, they must - be derived from the @{text defs}. These derivations are a bit involved. + also be derived from the @{text defs}. These derivations are a bit involved. Assuming we want to prove the introduction rule @{text [display] "\xs. As \ (\ys. Bs \ pred ss)\<^isup>* \ pred ts"} - then we can assume + then we can have assumptions of the form \begin{isabelle} (i)~~@{text "As"}\\ (ii)~@{text "(\ys. Bs \ pred ss)\<^isup>*"} \end{isabelle} - and must show + and must show the goal @{text [display] "pred ts"} - If we now unfold the definitions for the @{text preds}, we have + If we now unfold the definitions for the @{text preds}, we have assumptions \begin{isabelle} (i)~~~@{text "As"}\\ @@ -155,13 +148,14 @@ @{text [display] "As \ (\ys. Bs \ pred ss)\<^isup>* \ pred ts"} When we apply this rule we end up in the goal state where we have to prove + goals of the form \begin{isabelle} (a)~@{text "As"}\\ (b)~@{text "(\ys. Bs \ pred ss)\<^isup>*"} \end{isabelle} - We can immediately discharge the goals @{text "As"} using the assumption in + We can immediately discharge the goals @{text "As"} using the assumptions in @{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we 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 the @@ -173,8 +167,8 @@ 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. We do this in - the next section. For building testcases, we use the shorthands for + What remains is to implement the reasoning outlined in this section. We do this + next. For building testcases, we use the shorthands for @{text "even/odd"}, @{term "fresh"} and @{term "accpart"} given in Figure~\ref{fig:shorthands}. *}