diff -r 7b6d81ff9d9a -r 0a8981f52045 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Thu Apr 09 18:11:35 2009 +0000 +++ b/ProgTutorial/Package/Ind_Code.thy Sat Apr 11 19:23:58 2009 +0000 @@ -5,71 +5,73 @@ section {* The Gory Details\label{sec:code} *} text {* - As mentioned before the code falls roughly into three parts: code that deals - with the definitions, withe the induction principles and the introduction - rules, respectively. In addition there are some administrative functions - that string everything together. + As mentioned before the code falls roughly into three parts: the code that deals + with the definitions, with the induction principles and with the introduction + rules. In addition there are some administrative functions that string everything + together. *} subsection {* Definitions *} text {* - We first have to produce for each predicate the definition, whose general form is + We first have to produce for each predicate the user specifies an appropriate + definition, whose general form is @{text [display] "pred \ \zs. \preds. orules \ pred zs"} and then ``register'' the definition inside a local theory. - To do the latter, we use the following wrapper for + To do the latter, we use the following wrapper for the function @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax annotation and a term representing the right-hand side of the definition. *} -ML %linenosgray{*fun make_defn ((predname, syn), trm) lthy = +ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy = let - val arg = ((predname, syn), (Attrib.empty_binding, trm)) + val arg = ((predname, mx), (Attrib.empty_binding, trm)) val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy in (thm, lthy') end*} 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 a flag attached to the - theorem (others possibile flags 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 - use @{ML empty_binding in Attrib} in Line 3, since for our inductive predicates - the definitions do not need to have any theorem attributes. A testcase for this - function is + It returns the definition (as a theorem) and the local theory in which the + definition has been made. In Line 4, @{ML internalK in Thm} is a flag + attached to the theorem (others possibile flags 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.\footnote{FIXME: put in the section about theorems.} We + also use @{ML empty_binding in Attrib} in Line 3, since the definitions for + our inductive predicates are not meant to be seen by the user and therefore + do not need to have any theorem attributes. A testcase for this function is *} local_setup %gray {* fn lthy => let - val arg = ((@{binding "MyTrue"}, NoSyn), @{term True}) + val arg = ((@{binding "My_True"}, NoSyn), @{term True}) val (def, lthy') = make_defn arg lthy in warning (str_of_thm_no_vars lthy' def); lthy' end *} text {* - which introduces the definition @{prop "MyTrue \ True"} and then prints it out. + which introduces the definition @{thm My_True_def} and then prints it out. Since we are testing the function inside \isacommand{local\_setup}, i.e., make actual changes to the ambient theory, we can query the definition with the usual command \isacommand{thm}: \begin{isabelle} - \isacommand{thm}~@{text "MyTrue_def"}\\ - @{text "> MyTrue \ True"} + \isacommand{thm}~@{thm [source] "My_True_def"}\\ + @{text ">"}~@{thm "My_True_def"} \end{isabelle} The next two functions construct the right-hand sides of the definitions, - which are terms of the form + which are terms whose general form is: @{text [display] "\zs. \preds. orules \ pred zs"} - When constructing them, the variables @{text "zs"} need to be chosen so that - they do not occur in the @{text orules} and also be distinct from the @{text - "preds"}. + When constructing these terms, the variables @{text "zs"} need to be chosen so + that they do not occur in the @{text orules} and also be distinct from the + @{text "preds"}. The first function, named @{text defn_aux}, constructs the term for one @@ -145,40 +147,40 @@ (\a b t. \ a = b \ fresh a t \ fresh a (Lam b t)) \ fresh z za"} - The second function, named @{text defns}, has to just iterate the function + The second function, named @{text defns}, has to iterate the function @{ML defn_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 binding names of the predicates; @{text syns} - are the list of syntax annotations for the predicates; @{text "arg_tyss"} is - the list of argument-type-lists. + the list of predicates as @{ML_type term}s; the argument @{text + "prednames"} is the list of binding names of the predicates; @{text mxs} + are the list of syntax, or mixfix, annotations for the predicates; + @{text "arg_tyss"} is the list of argument-type-lists. *} -ML %linenosgray{*fun defns rules preds prednames syns arg_typss lthy = +ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy = let val thy = ProofContext.theory_of lthy val orules = map (ObjectLogic.atomize_term thy) rules val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) in - fold_map make_defn (prednames ~~ syns ~~ defs) lthy + fold_map make_defn (prednames ~~ mxs ~~ defs) lthy end*} text {* 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-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 defn_aux} in Line 5 produces all right-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 + definitions. The actual definitions are then made in Line 7. The result of + the function is a list of theorems and a local theory (the theorems are + registered with the local theory). A testcase for this function is *} local_setup %gray {* fn lthy => let val (defs, lthy') = - defns eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy + defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy in warning (str_of_thms_no_vars lthy' defs); lthy end *} @@ -301,7 +303,7 @@ text {* While the tactic for proving the induction principles is relatively simple, - it will be a bit of work to construct the goals from the introduction rules + it will be a bit more work to construct the goals from the introduction rules the user provides. Therefore let us have a closer look at the first proved theorem: @@ -968,7 +970,7 @@ ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy = let - val syns = map snd pred_specs + val mxs = map snd pred_specs val pred_specs' = map fst pred_specs val prednames = map fst pred_specs' val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs' @@ -976,20 +978,21 @@ val (namesattrs, rules) = split_list rule_specs - val (defs, lthy') = defns rules preds prednames syns tyss lthy - val ind_prin = inds rules defs preds tyss lthy' + val (defs, lthy') = defns rules preds prednames mxs tyss lthy + val ind_prins = inds rules defs preds tyss lthy' val intro_rules = intros rules preds defs lthy' val mut_name = space_implode "_" (map Binding.name_of prednames) val case_names = map (Binding.name_of o fst) namesattrs in lthy' |> reg_many mut_name ((@{binding "intros"}, []), intro_rules) + ||>> reg_many mut_name ((@{binding "inducts"}, []), ind_prins) ||>> fold_map (reg_single1 mut_name) (namesattrs ~~ intro_rules) ||>> fold_map (reg_single2 @{binding "induct"} [Attrib.internal (K (RuleCases.case_names case_names)), Attrib.internal (K (RuleCases.consumes 1)), Attrib.internal (K (Induct.induct_pred ""))]) - (prednames ~~ ind_prin) + (prednames ~~ ind_prins) |> snd end*} @@ -1017,11 +1020,13 @@ proofs correspond to the names of the introduction rules. These are generated in Line 16. - Line 18 now adds to @{text "lthy'"} all the introduction rules - under the name @{text "mut_name.intros"} (see previous paragraph). - Line 19 add further every introduction rule under its own name + Lines 18 and 19 now add to @{text "lthy'"} all the introduction rules + und induction principles under the name @{text "mut_name.intros"} and + @{text "mut_name.inducts"}, respectively (see previous paragraph). + + Line 20 add further every introduction rule under its own name (given by the user).\footnote{FIXME: what happens if the user did not give - any name.} Line 20 registers the induction principles. For this we have + any name.} Line 21 registers the induction principles. For this we have to use some specific attributes. The first @{ML "case_names" in RuleCases} corresponds to the case names that are used by Isar to reference the proof obligations in the induction. The second @{ML "consumes 1" in RuleCases} @@ -1029,7 +1034,8 @@ the predicate over which the induction proceeds) is eliminated. This completes all the code and fits in with the ``front end'' described - in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. Why the mut-name? + in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. + Why the mut-name? What does @{ML Binding.qualify} do?} *} (*<*)end(*>*) \ No newline at end of file