diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Tue Mar 17 17:32:12 2009 +0100 +++ b/CookBook/Package/Ind_Code.thy Wed Mar 18 03:03:51 2009 +0100 @@ -55,7 +55,7 @@ text {* It returns the definition (as a theorem) and the local theory in which this definition has - been made. In Line 4 @{ML internalK in Thm} is just a flag attached to the + been made. In Line 4, @{ML internalK in Thm} is a flag attached to the theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). These flags just classify theorems and have no significant meaning, except for tools that, for example, find theorems in the theorem database. We also @@ -72,7 +72,7 @@ end *} text {* - which makes the difinition @{prop "MyTrue \ True"} and then prints it out. + which makes the definition @{prop "MyTrue \ True"} and then prints it out. Since we are testing the function inside \isacommand{local\_setup}, i.e.~make changes to the ambient theory, we can query the definition using the usual command \isacommand{thm}: @@ -82,17 +82,20 @@ @{text "> MyTrue \ True"} \end{isabelle} - The next two functions construct the terms we need for the definitions, namely - terms of the form + The next two functions construct the terms we need for the definitions for + our \isacommand{simple\_inductive} command. These + terms are of the form @{text [display] "\\<^raw:$zs$>. \preds. orules \ pred \<^raw:$zs$>"} The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur - in the @{text orules} and also be distinct from @{text "preds"}. + in the @{text orules} and also be distinct from the @{text "preds"}. - The first function constructs the term for one particular predicate @{text - "pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is - determined by the number of argument types of @{text "arg_tys"}. + The first function constructs the term for one particular predicate, say + @{text "pred"}; the number of arguments of this predicate is + determined by the number of argument types of @{text "arg_tys"}. + So it takes these two parameters as arguments. The other arguments are + all the @{text "preds"} and the @{text "orules"}. *} ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) = @@ -112,11 +115,13 @@ end*} text {* - The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"}. For this - it pairs every argument type with the string @{text [quotes] "z"} (Line 7); - then generates variants for all these strings so that they are unique - w.r.t.~to the @{text "orules"} and the predicates; in Line 9 it generates the - corresponding variable terms for the unique strings. + The function in Line 3 is just a helper function for constructing universal + quantifications. The code in Lines 5 to 9 produces the fresh @{text + "\<^raw:$zs$>"}. For this it pairs every argument type with the string + @{text [quotes] "z"} (Line 7); then generates variants for all these strings + so that they are unique w.r.t.~to the @{text "orules"} and the predicates; + in Line 9 it generates the corresponding variable terms for the unique + strings. The unique free variables are applied to the predicate (Line 11) using the function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in @@ -132,7 +137,7 @@ val orules = [@{prop "even 0"}, @{prop "\n::nat. odd n \ even (Suc n)"}, @{prop "\n::nat. even n \ odd (Suc n)"}] - val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] + val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}, @{term "z::nat"}] val pred = @{term "even::nat\bool"} val arg_tys = [@{typ "nat"}] val def = defs_aux lthy orules preds (pred, arg_tys) @@ -141,15 +146,18 @@ end *} text {* - It constructs the left-hand side for the definition of @{term "even"}. So we obtain + It constructs the left-hand side for the definition of @{text "even"}. So we obtain as printout the term @{text [display] "\z. \even odd. (even 0) \ (\n. odd n \ even (Suc n)) \ (\n. even n \ odd (Suc n)) \ even z"} - The main function for the definitions now has to just iterate - the function @{ML defs_aux} over all predicates. + The main function for the definitions now has to just iterate the function + @{ML defs_aux} over all predicates. The argument @{text "preds"} is again + the the list of predicates as @{ML_type term}s; the argument @{text + "prednames"} is the list of names of the predicates; @{text "arg_tyss"} is + the list of argument-type-lists for each predicate. *} ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = @@ -162,19 +170,16 @@ end*} text {* - The argument @{text "preds"} is again the the list of predicates as - @{ML_type term}s; - the argument @{text "prednames"} is the list of names of the predicates; - @{text "arg_tyss"} is the list of argument-type-lists for each predicate. - - The user give the introduction rules using meta-implications and meta-quantifications. - In line 4 we transform the introduction rules into the object logic (definitions - cannot use them). To do the transformation we have to - obtain the theory behind the local theory (Line 3); with this theory - we can use the function @{ML ObjectLogic.atomize_term} to make the - transformation (Line 4). The call to @{ML defs_aux} in Line 5 produces all - left-hand sides of the definitions. The actual definitions are then made in Line 7. - As the result we obtain a list of theorems and a local theory. + The user will state the introduction rules using meta-implications and + meta-quanti\-fications. In Line 4, we transform these introduction rules into + the object logic (since definitions cannot be stated with + meta-connectives). To do this transformation we have to obtain the theory + behind the local theory (Line 3); with this theory we can use the function + @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call + to @{ML defs_aux} in Line 5 produces all left-hand sides of the + definitions. The actual definitions are then made in Line 7. The result + of the function is a list of theorems and a local theory. + A testcase for this function is *} @@ -194,6 +199,9 @@ end *} text {* + where we feed into the functions all parameters corresponding to + the @{text even}-@{text odd} example. The definitions we obtain + are: \begin{isabelle} \isacommand{thm}~@{text "even_def odd_def"}\\ @@ -201,18 +209,16 @@ "> even \ \z. \even odd. (even 0) \ (\n. odd n \ even (Suc n)) > \ (\n. even n \ odd (Suc n)) \ even z, > odd \ \z. \even odd. (even 0) \ (\n. odd n \ even (Suc n)) -> \ (\n. even n \ odd (Suc n)) \ odd z"} +> \ (\n. even n \ odd (Suc n)) \ odd z"} \end{isabelle} - This completes the code concerning the definitions. Next comes the code for - the induction principles. - - Let us now turn to the induction principles. Recall that the proof of the - induction principle for @{term "even"} was: + This completes the code for making the definitions. Next we deal with + the induction principles. Recall that the proof of the induction principle + for @{text "even"} was: *} -lemma +lemma man_ind_principle: assumes prems: "even n" shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" apply(atomize (full)) @@ -224,32 +230,35 @@ done text {* - We have to implement code that constructs the induction principle and then - a tactic that automatically proves it. + The code for such induction principles has to accomplish two tasks: + constructing the induction principles from the given introduction + rules and then automatically generating a proof of them using a tactic. The tactic will use the following helper function for instantiating universal - quantifiers. This function instantiates the @{text "?x"} in the theorem - @{thm spec} with a given @{ML_type cterm}. + quantifiers. *} ML{*fun inst_spec ctrm = Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*} text {* - For example we can use it in the following proof to instantiate the - three quantifiers in the assumption. We use the tactic + This helper function instantiates the @{text "?x"} in the theorem + @{thm spec} with a given @{ML_type cterm}. Together with the tactic *} ML{*fun inst_spec_tac ctrms = EVERY' (map (dtac o inst_spec) ctrms)*} text {* - and then apply use it with the @{ML_type cterm}s @{text "y1\y3"}. - *} + we can use @{ML inst_spec} in the following proof to instantiate the + three quantifiers in the assumption. +*} -lemma "\(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \ True" +lemma + fixes P::"nat \ nat \ nat \ bool" + shows "\x y z. P x y z \ True" apply (tactic {* - inst_spec_tac [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *}) + inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *}) txt {* We obtain the goal state @@ -271,8 +280,11 @@ assume_tac]*} text {* - We only have to give it as arguments the premises and the instantiations. - A testcase for the tactic is + We only have to give it as arguments the definitions, the premise + (like @{text "even n"}) + and the instantiations. Compare this with the manual proof given for the + lemma @{thm [source] man_ind_principle}. + A testcase for this tactic is the function *} ML{*fun test_tac prems = @@ -284,7 +296,7 @@ end*} text {* - which indeed proves the induction principle. + which indeed proves the induction principle: *} lemma @@ -294,22 +306,23 @@ done text {* - While the generic proof for the induction principle is relatively simple, - it is a bit harder to construct the goals from just the introduction - rules the user states. In general we have to construct for each predicate + While the tactic for the induction principle is relatively simple, + it is a bit harder to construct the goals from the introduction + rules the user provides. In general we have to construct for each predicate @{text "pred"} a goal of the form @{text [display] - "\\<^raw:$zs$>. pred \<^raw:$zs$> \ rules[preds := \<^raw:$Ps$>] \ \<^raw:$P$>\<^raw:$zs$>"} + "\\<^raw:$zs$>. pred \<^raw:$zs$> \ rules[preds := \<^raw:$Ps$>] \ \<^raw:$P$> \<^raw:$zs$>"} where the given predicates @{text preds} are replaced in the introduction - rule @{text "rules"} by new distinct variables written as @{text "\<^raw:$Ps$>"}. - We also need to generate fresh arguments for the predicate @{text "pred"} and - the @{text "\<^raw:$P$>"} in the conclusion of the induction principle. + rules by new distinct variables written @{text "\<^raw:$Ps$>"}. + We also need to generate fresh arguments for the predicate @{text "pred"} in + the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve + that in two steps. - The function below expects that the rules are already appropriately - substitued. The argument @{text "srules"} stands for these substituted - introduction rules; @{text cnewpreds} are the certified terms coresponding + The function below expects that the introduction rules are already appropriately + substituted. The argument @{text "srules"} stands for these substituted + rules; @{text cnewpreds} are the certified terms coresponding to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for which we prove the introduction principle; @{text "newpred"} is its replacement and @{text "tys"} are the argument types of this predicate. @@ -331,64 +344,102 @@ end *} text {* - In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the + In Line 3 we produce names @{text "\<^raw:$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'"}. In Line 5 we just construct the terms corresponding to these variables. The term variables are applied to the predicate in Line 7 (this corresponds to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9, we first construct the term @{text "\<^raw:$P$>\<^raw:$zs$>"} - and then add the (modified) introduction rules as premises. In case that - no introduction rules are given, the conclusion of this implications needs + and then add the (substituded) 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. - In Line 11 we set up the goal to be proved; then call the tactic for proving the - induction principle. This tactic expects the (certified) predicates with which - the introduction rules have been substituted. This will return a theorem. - However, it is a theorem proved inside the local theory @{text "lthy'"} where - the variables @{text "\<^raw:$zs$>"} are fixed, but free. By exporting this - theorem from @{text "lthy'"} (which contains the @{text "\<^raw:$zs$>"} - as free) to @{text "lthy"} (which does not), we obtain the desired quantifications - @{text "\\<^raw:$zs$>"}. + In Line 11 we set up the goal to be proved; in the next line call the tactic + for proving the induction principle. This tactic expects definitions, the + premise and the (certified) predicates with which the introduction rules + have been substituted. This will return a theorem. However, it is a theorem + proved inside the local theory @{text "lthy'"}, where the variables @{text + "\<^raw:$zs$>"} are fixed, but free. By exporting this theorem from @{text + "lthy'"} (which contains the @{text "\<^raw:$zs$>"} as free) to @{text + "lthy"} (which does not), we obtain the desired quantifications @{text + "\\<^raw:$zs$>"}. - Now it is left to produce the new predicated with which the introduction + (FIXME testcase) + + + Now it is left to produce the new predicates with which the introduction rules are substituted. *} -ML %linenosgray{*fun inductions rules defs preds tyss lthy = +ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy = let val Ps = replicate (length preds) "P" val (newprednames, lthy') = Variable.variant_fixes Ps lthy val thy = ProofContext.theory_of lthy' - val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss + val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss val newpreds = map Free (newprednames ~~ tyss') val cnewpreds = map (cterm_of thy) newpreds - val rules' = map (subst_free (preds ~~ newpreds)) rules + val srules = map (subst_free (preds ~~ newpreds)) rules in - map (prove_induction lthy' defs rules' cnewpreds) - (preds ~~ newpreds ~~ tyss) + map (prove_induction lthy' defs srules cnewpreds) + (preds ~~ newpreds ~~ arg_tyss) |> ProofContext.export lthy' lthy end*} -ML {* - let - val rules = [@{prop "even (0::nat)"}, - @{prop "\n::nat. odd n \ even (Suc n)"}, - @{prop "\n::nat. even n \ odd (Suc n)"}] - val defs = [@{thm even_def}, @{thm odd_def}] - val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] - val tyss = [[@{typ "nat"}], [@{typ "nat"}]] - in - inductions rules defs preds tyss @{context} - end +text {* + In Line 3 we generate a string @{text [quotes] "P"} for each predicate. + In Line 4, we use the same trick as in the previous function, that is making the + @{text "\<^raw:$Ps$>"} fresh and declaring them as fixed but free in + the new local theory @{text "lthy'"}. From the local theory we extract + the ambient theory in Line 6. We need this theory in order to certify + the new predicates. In Line 8 we calculate the types of these new predicates + using the argument types. Next we turn them into terms and subsequently + certify them. We can now produce the substituted introduction rules + (Line 11). Line 14 and 15 just iterate the proofs for all predicates. + From this we obtain a list of theorems. Finally we need to export the + fixed variables @{text "\<^raw:$Ps$>"} to obtain the correct quantification + (Line 16). + + A testcase for this function is +*} + +local_setup %gray {* fn lthy => +let + val rules = [@{prop "even (0::nat)"}, + @{prop "\n::nat. odd n \ even (Suc n)"}, + @{prop "\n::nat. even n \ odd (Suc n)"}] + val defs = [@{thm even_def}, @{thm odd_def}] + val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] + val tyss = [[@{typ "nat"}], [@{typ "nat"}]] + val ind_thms = inductions rules defs preds tyss lthy +in + warning (str_of_thms lthy ind_thms); lthy +end *} -subsection {* Introduction Rules *} +text {* + which prints out + +@{text [display] +"> even z \ +> P 0 \ (\m. Pa m \ P (Suc m)) \ (\m. P m \ Pa (Suc m)) \ P z, +> odd z \ +> P 0 \ (\m. Pa m \ P (Suc m)) \ (\m. P m \ Pa (Suc m)) \ Pa z"} + + + This completes the code for the induction principles. Finally we can + prove the introduction rules. + +*} + +ML {* ObjectLogic.rulify *} + 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})*} @@ -422,7 +473,7 @@ fun introductions_tac defs rules preds i ctxt = EVERY1 [ObjectLogic.rulify_tac, K (rewrite_goals_tac defs), - REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), + REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), subproof1 rules preds i ctxt]*} lemma evenS: @@ -491,7 +542,6 @@ end*} ML{*val spec_parser = - OuterParse.opt_target -- OuterParse.fixes -- Scan.optional (OuterParse.$$$ "where" |-- @@ -501,10 +551,9 @@ ML{*val specification = spec_parser >> - (fn ((loc, pred_specs), rule_specs) => - Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*} + (fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*} -ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" +ML{*val _ = OuterSyntax.local_theory "simple_inductive" "define inductive predicates" OuterKeyword.thy_decl specification*} text {*