--- a/ProgTutorial/Package/Ind_Code.thy Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy Thu Jul 30 15:51:51 2009 +0200
@@ -36,7 +36,7 @@
text {*
It returns the definition (as a theorem) and the local theory in which the
definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag
- attached to the theorem (others possibile flags are @{ML [index] definitionK in Thm}
+ attached to the theorem (other possibile flags are @{ML [index] definitionK in Thm}
and @{ML [index] 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
@@ -113,7 +113,7 @@
predicate. A testcase for this function is
*}
-local_setup %gray{* fn lthy =>
+local_setup %gray {* fn lthy =>
let
val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
in
@@ -132,10 +132,14 @@
If we try out the function with the rules for freshness
*}
-local_setup %gray{* fn lthy =>
- (writeln (Syntax.string_of_term lthy
- (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
- lthy) *}
+local_setup %gray {* fn lthy =>
+let
+ val def = defn_aux lthy fresh_orules
+ [fresh_pred] (fresh_pred, fresh_arg_tys)
+in
+ writeln (Syntax.string_of_term lthy def); lthy
+end *}
+
text {*
we obtain
@@ -169,7 +173,8 @@
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
+ behind the local theory using the function @{ML [index] theory_of in ProofContext}
+ (Line 3); with this theory we can use the function
@{ML [index] atomize_term in ObjectLogic} 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
@@ -187,7 +192,7 @@
text {*
where we feed into the function all parameters corresponding to
- the @{text even}-@{text odd} example. The definitions we obtain
+ the @{text even}/@{text odd} example. The definitions we obtain
are:
@{text [display, break]
@@ -199,8 +204,8 @@
Note that in the testcase we return the local theory @{text lthy}
(not the modified @{text lthy'}). As a result the test case has no effect
on the ambient theory. The reason is that if we introduce the
- definition again, we pollute the name space with two versions of @{text "even"}
- and @{text "odd"}.
+ definition again, we pollute the name space with two versions of
+ @{text "even"} and @{text "odd"}. We want to avoid this here.
This completes the code for introducing the definitions. Next we deal with
the induction principles.
@@ -234,12 +239,12 @@
*}
ML{*fun inst_spec ctrm =
- Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
+ Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
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 following tactic, called @{text inst_spec_tac}\label{fun:instspectac}.
+ in the following tactic.\label{fun:instspectac}.
*}
ML{*fun inst_spec_tac ctrms =
@@ -278,11 +283,15 @@
text {*
We have to give it as arguments the definitions, the premise (a list of
formulae) and the instantiations. The premise is @{text "even n"} in lemma
- @{thm [source] manual_ind_prin_even}; in our code it will always be a list
+ @{thm [source] manual_ind_prin_even} shown above; in our code it will always be a list
consisting of a single formula. Compare this tactic with the manual proof
for the lemma @{thm [source] manual_ind_prin_even}: as you can see there is
almost a one-to-one correspondence between the \isacommand{apply}-script and
- the @{ML ind_tac}. Two testcases for this tactic are:
+ the @{ML ind_tac}. We first rewrite the goal to use only object connectives (Line 2),
+ "cut in" the premise (Line 3), unfold the definitions (Line 4), instantiate
+ the assumptions of the goal (Line 5) and then conclude with @{ML assume_tac}.
+
+ Two testcases for this tactic are:
*}
lemma automatic_ind_prin_even:
@@ -370,23 +379,24 @@
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
- expects the definitions, the premise and the (certified) predicates with
- which the introduction rules have been substituted. The code in these two
- lines will return a theorem. However, it is a theorem
- proved inside the local theory @{text "lthy'"}, where the variables @{text
- "zs"} are free, but fixed (see Line 4). By exporting this theorem from @{text
- "lthy'"} (which contains the @{text "zs"} as free variables) to @{text
- "lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}.
- A testcase for this function is
+ In Line 11 we set up the goal to be proved using the function @{ML [index]
+ prove in Goal}; in the next line we call the tactic for proving the
+ induction principle. As mentioned before, this tactic expects the
+ definitions, the premise and the (certified) predicates with which the
+ introduction rules have been substituted. The code in these two lines will
+ return a theorem. However, it is a theorem proved inside the local theory
+ @{text "lthy'"}, where the variables @{text "zs"} are free, but fixed (see
+ Line 4). By exporting this theorem from @{text "lthy'"} (which contains the
+ @{text "zs"} as free variables) to @{text "lthy"} (which does not), we
+ obtain the desired schematic variables @{text "?zs"}. A testcase for this
+ function is
*}
-local_setup %gray{* fn lthy =>
+local_setup %gray {* fn lthy =>
let
- val newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]
- val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
- val newpred = @{term "P::nat\<Rightarrow>bool"}
+ val newpreds = [@{term "P::nat \<Rightarrow> bool"}, @{term "Q::nat \<Rightarrow> bool"}]
+ val cnewpreds = [@{cterm "P::nat \<Rightarrow> bool"}, @{cterm "Q::nat \<Rightarrow> bool"}]
+ val newpred = @{term "P::nat \<Rightarrow> bool"}
val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules
val intro =
prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
@@ -529,8 +539,11 @@
@{thm [source] imp_elims_test}:
@{ML_response_fake [display, gray]
-"writeln (string_of_thm_no_vars @{context}
- (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
+"let
+ val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
+in
+ writeln (string_of_thm_no_vars @{context} res)
+end"
"C"}
Now we set up the proof for the introduction rule as follows:
@@ -552,7 +565,8 @@
THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
text {*
- The function in Line 2 ``rulifies'' the lemma. This will turn out to
+ The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better}
+ This will turn out to
be important later on. Applying this tactic in our proof of @{text "fresh_Lem"}
*}
@@ -581,22 +595,13 @@
"prems2"}. To do this separation, it is best to open a subproof with the
tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as
list of @{ML_type cterm}s) and the assumptions (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:
+ The problem with @{ML SUBPROOF}, however, is that it always expects us to
+ completely discharge the goal (see Section~\ref{sec:simpletacs}). This is
+ a bit inconvenient for our gradual explanation of the proof here. Therefore
+ we use first the function @{ML [index] FOCUS}, which does same as @{ML SUBPROOF}
+ but does not require us to completely discharge the goal.
*}
(*<*)oops(*>*)
-ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*}
-
-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. Once we are finished, we
- just have to replace it with @{ML SUBPROOF}.
-*}
-
text_raw {*
\begin{figure}[t]
\begin{minipage}{\textwidth}
@@ -611,7 +616,7 @@
in
s |> separate "\n"
|> implode
- |> writeln
+ |> tracing
end*}
text_raw{*
\end{isabelle}
@@ -625,18 +630,19 @@
First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
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
+ function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS} will
supply us the @{text "params"} and @{text "prems"} as lists, we can
separate them using the function @{ML [index] chop}.
*}
-ML{*fun chop_test_tac preds rules =
- SUBPROOF_test (fn {params, prems, context, ...} =>
+ML %linenosgray{*fun chop_test_tac preds rules =
+ FOCUS (fn {params, prems, context, ...} =>
let
- val (params1, params2) = chop (length params - length preds) (map snd params)
+ val cparams = map snd params
+ val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
- chop_print params1 params2 prems1 prems2 context; no_tac
+ chop_print params1 params2 prems1 prems2 context; all_tac
end) *}
text {*
@@ -644,12 +650,14 @@
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
+ Therefore we only have to subtract in Line 5 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
+ with the @{text "prems"} in line 6: the last premises in the goal state come from
unfolding the definition of the predicate in the conclusion. So we can
just subtract the number of rules from the number of all premises.
- Applying this tactic in our example
+ To check our calculations we print them out in Line 8 using the
+ function @{ML chop_print} from Figure~\ref{fig:chopprint} and then
+ just do nothing, that is @{ML all_tac}. Applying this tactic in our example
*}
(*<*)
@@ -657,7 +665,7 @@
shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
apply(tactic {* expand_tac @{thms fresh_def} *})
(*>*)
-apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} *})
+apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} 1 *})
(*<*)oops(*>*)
text {*
@@ -691,19 +699,18 @@
To use this premise with @{ML rtac}, we need to instantiate its
quantifiers (with @{text params1}) and transform it into rule
- format (using @{ML [index] rulify in ObjectLogic}. So we can modify the
- subproof as follows:
+ format (using @{ML [index] rulify in ObjectLogic}). So we can modify the
+ code as follows:
*}
ML %linenosgray{*fun apply_prem_tac i preds rules =
- SUBPROOF_test (fn {params, prems, context, ...} =>
+ FOCUS (fn {params, prems, context, ...} =>
let
- val (params1, params2) = chop (length params - length preds) (map snd params)
+ val cparams = map snd params
+ val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
- THEN print_tac ""
- THEN no_tac
end) *}
text {*
@@ -719,16 +726,15 @@
shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
apply(tactic {* expand_tac @{thms fresh_def} *})
(*>*)
-apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} *})
+apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
(*<*)oops(*>*)
text {*
- Since we print out the goal state just after the application of
- @{ML rtac} (Line 8), we can see the goal state we obtain:
+ The goal state we obtain is:
\begin{isabelle}
- @{text "1."}~@{prop "a \<noteq> b"}\\
- @{text "2."}~@{prop "fresh a t"}
+ @{text "1."}~@{text "\<dots> \<Longrightarrow> "}~@{prop "a \<noteq> b"}\\
+ @{text "2."}~@{text "\<dots> \<Longrightarrow> "}~@{prop "fresh a t"}
\end{isabelle}
As expected there are two subgoals, where the first comes from the
@@ -773,7 +779,8 @@
ML{*fun prove_intro_tac i preds rules =
SUBPROOF (fn {params, prems, ...} =>
let
- val (params1, params2) = chop (length params - length preds) (map snd params)
+ val cparams = map snd params
+ val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -781,7 +788,7 @@
end) *}
text {*
- Note that the tactic is now @{ML SUBPROOF}, not @{ML SUBPROOF_test}.
+ Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS} anymore.
The full proof of the introduction rule is as follows:
*}
@@ -792,7 +799,9 @@
done
text {*
- Phew! ...Unfortunately, not everything is done yet. If you look closely
+ Phew!\ldots
+
+ 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
@@ -802,8 +811,8 @@
lemma accpartI:
shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
apply(tactic {* expand_tac @{thms accpart_def} *})
-apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *})
-apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})
+apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})
+apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})
txt {*
Here @{ML chop_test_tac} prints out the following
@@ -868,7 +877,8 @@
ML %linenosgray{*fun prove_intro_tac i preds rules =
SUBPROOF (fn {params, prems, context, ...} =>
let
- val (params1, params2) = chop (length params - length preds) (map snd params)
+ val cparams = map snd params
+ val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -952,15 +962,15 @@
three wrappers this function:
*}
-ML{*fun reg_many qname ((name, attrs), thms) =
+ML{*fun note_many qname ((name, attrs), thms) =
LocalTheory.note Thm.theoremK
((Binding.qualify false qname name, attrs), thms)
-fun reg_single1 qname ((name, attrs), thm) =
- reg_many qname ((name, attrs), [thm])
+fun note_single1 qname ((name, attrs), thm) =
+ note_many qname ((name, attrs), [thm])
-fun reg_single2 name attrs (qname, thm) =
- reg_many (Binding.name_of qname) ((name, attrs), [thm]) *}
+fun note_single2 name attrs (qname, thm) =
+ note_many (Binding.name_of qname) ((name, attrs), [thm]) *}
text {*
The function that ``holds everything together'' is @{text "add_inductive"}.
@@ -985,10 +995,10 @@
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"}
+ lthy' |> note_many mut_name ((@{binding "intros"}, []), intro_rules)
+ ||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins)
+ ||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules)
+ ||>> fold_map (note_single2 @{binding "induct"}
[Attrib.internal (K (RuleCases.case_names case_names)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))])