--- 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 \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> 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 \<equiv> 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 \<equiv> 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] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> 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 @@
(\<forall>a b t. \<not> a = b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> 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