# HG changeset patch # User Christian Urban # Date 1238177982 0 # Node ID ac01ddb285f6b7f33a56ccf2e52710f145cc2cf5 # Parent d5accbc67e1be8b82e87bd0bb8cf98cd7c43c257 polishing diff -r d5accbc67e1b -r ac01ddb285f6 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Fri Mar 27 12:49:28 2009 +0000 +++ b/ProgTutorial/Package/Ind_Code.thy Fri Mar 27 18:19:42 2009 +0000 @@ -5,9 +5,9 @@ section {* The Gory Details\label{sec:code} *} text {* - As mentioned before the code falls roughly into three parts: the definitions, - the induction principles and the introduction rules. In addition there is an - administrative function that strings everything together. + As mentioned before the code falls roughly into three parts: code that deals + with the definitions, the induction principles and the introduction rules, respectively. + In addition there are some administrative functions that string everything together. *} subsection {* Definitions *} @@ -236,22 +236,22 @@ text {* This helper function instantiates the @{text "?x"} in the theorem @{thm spec} with a given @{ML_type cterm}. We call this helper function - in the next tactic, called @{text inst_spec_tac}. + in the following tactic, called @{text inst_spec_tac}. *} ML{*fun inst_spec_tac ctrms = EVERY' (map (dtac o inst_spec) ctrms)*} text {* - This tactic expects a list of @{ML_type cterm}s. It allows us in the following - proof to instantiate the three quantifiers in the assumption. + This tactic expects a list of @{ML_type cterm}s. It allows us in the + proof below to instantiate the three quantifiers in the assumption. *} lemma fixes P::"nat \ nat \ nat \ bool" shows "\x y z. P x y z \ True" apply (tactic {* - inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *}) + inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *}) txt {* We obtain the goal state @@ -311,8 +311,8 @@ The variables @{text "z"}, @{text "P"} and @{text "Q"} are schematic variables (since they are not quantified in the lemma). These schematic variables are needed so that they can be instantiated by the user. - We have to take care to also generate these schematic variables when - generating the goals for the induction principles. In general we have + It will take a bit of work to generate these schematic variables when + constructing the goals for the induction principles. In general we have to construct for each predicate @{text "pred"} a goal of the form @{text [display] @@ -321,9 +321,9 @@ where the predicates @{text preds} are replaced in @{text rules} by new distinct variables @{text "?Ps"}. We also need to generate fresh arguments @{text "?zs"} for the predicate @{text "pred"} and the @{text "?P"} in - the conclusion. The crucial point is that the @{text "?Ps"} and - @{text "?zs"} need to be schematic variables that can be instantiated - by the user. + the conclusion. As just mentioned, the crucial point is that the + @{text "?Ps"} and @{text "?zs"} need to be schematic variables that can + be instantiated by the user. We generate these goals in two steps. The first function, named @{text prove_ind}, expects that the introduction rules are already appropriately substituted. The argument @@ -352,16 +352,17 @@ text {* In Line 3 we produce names @{text "zs"} for each type in the argument type list. Line 4 makes these names unique and declares them as - \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. - That means they are not (yet) schematic variables. + \emph{free but fixed} variables in the local theory @{text "lthy'"}. + That means they are not schematic variables (yet). In Line 5 we construct the terms corresponding to these variables. The variables are applied to the predicate in Line 7 (this corresponds to the first premise @{text "pred zs"} of the induction principle). In Line 8 and 9, we first construct the term @{text "P zs"} - and then add the (substituted) introduction rules as premises. In case that - no introduction rules are given, the conclusion of this implication needs - to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal - mechanism will fail. + and then add the (substituted) introduction rules as preconditions. In + case that no introduction rules are given, the conclusion of this + implication needs to be wrapped inside a @{term Trueprop}, otherwise + the Isabelle's goal mechanism will fail.\footnote{FIXME: check with + Stefan...is this so?} In Line 11 we set up the goal to be proved; in the next line we call the tactic for proving the induction principle. As mentioned before, this tactic @@ -467,18 +468,25 @@ subsection {* Introduction Rules *} text {* - The proofs of the introduction rules are quite a bit - more involved than the ones for the induction principles. - To ease somewhat our work here, we use the following two helper - functions. + Constructing the goals for the introduction rules is easy: they + are just the rules given by the user. However, their proofs are + quite a bit more involved than the ones for the induction principles. + To explain the general method, our running example will be + the introduction rule + \begin{isabelle} + @{prop "\a b t. \a \ b; fresh a t\ \ fresh a (Lam b t)"} + \end{isabelle} + + about freshness for lambdas. In order to ease somewhat + our work here, we use the following two helper functions. *} ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} text {* - To see what these functions do, let us suppose whe have the following three + To see what these functions do, let us suppose we have the following three theorems. *} @@ -515,14 +523,7 @@ (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" "C"} - To explain the proof for the introduction rule, our running example will be - the rule: - - \begin{isabelle} - @{prop "\a b t. \a \ b; fresh a t\ \ fresh a (Lam b t)"} - \end{isabelle} - - for freshness of applications. We set up the proof as follows: + Now we set up the proof for the introduction rule as follows: *} lemma fresh_Lam: @@ -530,19 +531,19 @@ (*<*)oops(*>*) text {* - The first step will be to expand the definitions of freshness + The first step in the proof will be to expand the definitions of freshness and then introduce quantifiers and implications. For this we will use the tactic *} -ML{*fun expand_tac defs = +ML %linenosgray{*fun expand_tac defs = ObjectLogic.rulify_tac 1 THEN rewrite_goals_tac defs THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *} text {* - The first step of ``rulifying'' the lemma will turn out to be important - later on. Applying this tactic + The function in Line 2 ``rulifies'' the lemma. This will turn out to + be important later on. Applying this tactic *} (*<*) @@ -562,20 +563,20 @@ and @{text "t"}) which come from the introduction rule and parameters (in the case above only @{text "fresh"}) which come from the universal quantification in the definition @{term "fresh a (App t s)"}. - Similarly, there are preconditions - that come from the premises of the rule and premises from the - definition. We need to treat these - parameters and preconditions differently. In the code below + Similarly, there are assumptions + that come from the premises of the rule and assumptions from the + definition of the predicate. We need to treat these + parameters and assumptions differently. In the code below we will therefore separate them into @{text "params1"} and @{text params2}, respectively @{text "prems1"} and @{text "prems2"}. To do this separation, it is best to open a subproof with the tactic @{ML SUBPROOF}, since this tactic provides us - with the parameters (as list of @{ML_type cterm}s) and the premises - (as list of @{ML_type thm}s). The problem we have to overcome - with @{ML SUBPROOF} is, however, that this tactic always expects us to completely - discharge the goal (see Section~\ref{sec:simpletacs}). This is inconvenient for - our gradual explanation of the proof here. To circumvent this inconvenience - we use the following modified tactic: + with the parameters (as list of @{ML_type cterm}s) and the assumptions + (as list of @{ML_type thm}s called @{text prems}). The problem we have + to overcome with @{ML SUBPROOF} is, however, that this tactic always + expects us to completely discharge the goal (see Section~\ref{sec:simpletacs}). + This is inconvenient for our gradual explanation of the proof here. To + circumvent this inconvenience we use the following modified tactic: *} (*<*)oops(*>*) ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*} @@ -583,7 +584,8 @@ text {* If the tactic inside @{ML SUBPROOF} fails, then the overall tactic will still succeed. With this testing tactic, we can gradually implement - all necessary proof steps inside a subproof. + all necessary proof steps inside a subproof. Once we are finished, we + just have to replace it with @{ML SUBPROOF}. *} text_raw {* @@ -612,8 +614,8 @@ text {* First we calculate the values for @{text "params1/2"} and @{text "prems1/2"} - from @{text "params"} and @{text "prems"}, respectively. To see what is - going in our example, we will print out the values using the printing + from @{text "params"} and @{text "prems"}, respectively. To better see what is + going in our example, we will print out these values using the printing function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will supply us the @{text "params"} and @{text "prems"} as lists, we can separate them using the function @{ML chop}. @@ -629,9 +631,10 @@ end) *} text {* - For the separation we can rely on that Isabelle deterministically - produces parameter and premises in a goal state. The last parameters - that were introduced come from the quantifications in the definitions. + For the separation we can rely on the fact that Isabelle deterministically + produces parameters and premises in a goal state. The last parameters + that were introduced come from the quantifications in the definitions + (see the tactic @{ML expand_tac}). Therefore we only have to subtract the number of predicates (in this case only @{text "1"}) from the lenghts of all parameters. Similarly with the @{text "prems"}: the last premises in the goal state come from @@ -675,7 +678,7 @@ We now have to select from @{text prems2} the premise that corresponds to the introduction rule we prove, namely: - @{term [display] "\a t s. fresh a t \ fresh a s \ fresh a (App t s)"} + @{term [display] "\a b t. a \ b \ fresh a t \ fresh a (Lam a t)"} To use this premise with @{ML rtac}, we need to instantiate its quantifiers (with @{text params1}) and transform it into rule @@ -683,7 +686,7 @@ subproof as follows: *} -ML{*fun apply_prem_tac i preds rules = +ML %linenosgray{*fun apply_prem_tac i preds rules = SUBPROOF_test (fn {params, prems, context, ...} => let val (params1, params2) = chop (length params - length preds) params @@ -696,9 +699,9 @@ text {* The argument @{text i} corresponds to the number of the - introduction we want to analyse. We will later on lat it range - from @{text 0} to the number of introduction rules. - Below we applying this function with @{text 3}, since + introduction we want to prove. We will later on lat it range + from @{text 0} to the number of @{text "rules - 1"}. + Below we apply this function with @{text 3}, since we are proving the fourth introduction rule. *} @@ -712,19 +715,19 @@ text {* Since we print out the goal state just after the application of - @{ML rtac}, we can see the goal state we obtain: as expected it has - the two subgoals + @{ML rtac} (Line 8), we can see the goal state we obtain: \begin{isabelle} @{text "1."}~@{prop "a \ b"}\\ @{text "2."}~@{prop "fresh a t"} \end{isabelle} - where the first comes from a non-recursive premise of the rule - and the second comes from a recursive premise. The first goal - can be solved immediately by @{text "prems1"}. The second - needs more work. It can be solved with the other premise - in @{text "prems1"}, namely + As expected there are two subgoals, where the first comes from a + non-recursive premise of the introduction rule and the second comes + from a recursive premise. The first goal can be solved immediately + by @{text "prems1"}. The second needs more work. It can be solved + with the other premise in @{text "prems1"}, namely + @{term [break,display] "\fresh. @@ -737,8 +740,8 @@ come from @{text "params1"} and @{text "prems2"}. We can determine whether we are in the simple or complicated case by checking whether the topmost connective is an @{text "\"}. The premises in the simple - case cannot have such a quantification, since in the first step - of @{ML "expand_tac"} was the ``rulification'' of the lemma. + case cannot have such a quantification, since the first step + of @{ML "expand_tac"} was to ``rulify'' the lemma. The premise of the complicated case must have at least one @{text "\"} coming from the quantification over the @{text preds}. So we can implement the following function @@ -769,6 +772,7 @@ end) *} text {* + Note that the tactic is now @{ML SUBPROOF}, not @{ML SUBPROOF_test}. The full proof of the introduction rule now as follows: *} @@ -779,10 +783,10 @@ done text {* - Unfortunately, not everything is done yet. If you look closely - at the general principle outlined in Section~\ref{sec:nutshell}, - we have not yet dealt with the case when recursive premises - in a rule have preconditions @{text Bs}. The introduction rule + Phew! Unfortunately, not everything is done yet. If you look closely + at the general principle outlined for the introduction rules in + Section~\ref{sec:nutshell}, we have not yet dealt with the case where + recursive premises have preconditions. The introduction rule of the accessible part is such a rule. *} @@ -818,10 +822,10 @@ *}(*<*)oops(*>*) text {* - In order to make progress as before, we have to use the precondition + In order to make progress, we have to use the precondition @{text "R y x"} (in general there can be many of them). The best way to get a handle on these preconditions is to open up another subproof, - since the preconditions will be bound to @{text prems}. Therfore we + since the preconditions will then be bound to @{text prems}. Therfore we modify the function @{ML prepare_prem} as follows *} @@ -839,13 +843,17 @@ text {* In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve - them with @{text prem}. In the simple case, that is where the @{text prem} + them with @{text prem}. In the simple cases, that is where the @{text prem} comes from a non-recursive premise of the rule, @{text prems} will be - just the empty list and the @{ML MRS} does nothing. Similarly, in the + just the empty list and the function @{ML MRS} does nothing. Similarly, in the cases where the recursive premises of the rule do not have preconditions. + In case there are preconditions, then Line 4 discharges them. After + that we can proceed as before, i.e., check whether the outermost + connective is @{text "\"}. - The function @{ML prove_intro_tac} only needs to give the context to - @{ML prepare_prem} (Line 8) and is as follows. + The function @{ML prove_intro_tac} only needs to be changed so that it + gives the context to @{ML prepare_prem} (Line 8). The modified version + is below. *} ML %linenosgray{*fun prove_intro_tac i preds rules = @@ -859,7 +867,7 @@ end) *} text {* - With these extended function we can also prove the introduction + With these two functions we can now also prove the introduction rule for the accessible part. *} @@ -882,14 +890,13 @@ text {* Lines 2 to 4 correspond to the function @{ML expand_tac}. Some testcases - dor this tactic are: + for this tactic are: *} lemma even0_intro: shows "even 0" by (tactic {* intro_tac eo_defs eo_rules eo_preds 0 @{context} *}) - lemma evenS_intro: shows "\m. odd m \ even (Suc m)" by (tactic {* intro_tac eo_defs eo_rules eo_preds 1 @{context} *}) @@ -900,9 +907,10 @@ intro_tac @{thms fresh_def} fresh_rules [fresh_pred] 1 @{context} *}) text {* - The second function sets up in Line 4 the goals (in this case this is easy - since they are exactly the introduction rules the user gives) - and iterates @{ML intro_tac} over all introduction rules. + The second function sets up in Line 4 the goals (this is easy + for the introduction rules since they are exactly the rules + given by the user) and iterates @{ML intro_tac} over all + introduction rules. *} ML %linenosgray{*fun intros rules preds defs lthy = @@ -914,6 +922,14 @@ map_index intros_aux rules end*} +text {* + The iteration is done with the function @{ML map_index} since we + need the introduction rule together with its number (counted from + @{text 0}). This completes the code for the functions deriving the + reasoning infrastructure. It remains to implement some administrative + code that strings everything together. +*} + subsection {* Main Function *} text {* main internal function *} 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}. *} diff -r d5accbc67e1b -r ac01ddb285f6 ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Fri Mar 27 12:49:28 2009 +0000 +++ b/ProgTutorial/Package/Ind_Interface.thy Fri Mar 27 18:19:42 2009 +0000 @@ -442,10 +442,12 @@ *} text {* - From a high-level perspective the package consists of 6 subtasks: + (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. *} diff -r d5accbc67e1b -r ac01ddb285f6 ProgTutorial/Package/Ind_Intro.thy --- a/ProgTutorial/Package/Ind_Intro.thy Fri Mar 27 12:49:28 2009 +0000 +++ b/ProgTutorial/Package/Ind_Intro.thy Fri Mar 27 18:19:42 2009 +0000 @@ -33,12 +33,12 @@ inductive predicates. To keep things really simple, we will not use the general Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis of Isabelle's standard inductive definition package. Instead, we - will use a simpler \emph{impredicative} (i.e.\ involving quantification on + will describe a simpler \emph{impredicative} (i.e.\ involving quantification on predicate variables) encoding of inductive predicates. Due to its simplicity, this package will necessarily have a reduced functionality. It does neither support introduction rules involving arbitrary monotone - operators, nor does it prove case analysis (or inversion) rules. Moreover, - it only proves a weaker form of the induction principle for inductive + operators, nor does it prove case analysis rules (also called inversion rules). + Moreover, it only proves a weaker form of the induction principle for inductive predicates. *} diff -r d5accbc67e1b -r ac01ddb285f6 progtutorial.pdf Binary file progtutorial.pdf has changed