--- a/ProgTutorial/FirstSteps.thy Sun Apr 26 23:45:22 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Wed Apr 29 00:36:14 2009 +0200
@@ -1142,6 +1142,59 @@
next section)
*}
+section {* Setups (TBD) *}
+
+text {*
+ In the previous section we used \isacommand{setup} in order to make
+ a theorem attribute known to Isabelle. What happens behind the scenes
+ is that \isacommand{setup} expects a function of type
+ @{ML_type "theory -> theory"}: the input theory is the current theory and the
+ output the theory where the theory attribute has been stored.
+
+ This is a fundamental principle in Isabelle. A similar situation occurs
+ for example with declaring constants. The function that declares a
+ constant on the ML-level is @{ML Sign.add_consts_i}.
+ If you write\footnote{Recall that ML-code needs to be
+ enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
+*}
+
+ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
+
+text {*
+ for declaring the constant @{text "BAR"} with type @{typ nat} and
+ run the code, then you indeed obtain a theory as result. But if you
+ query the constant on the Isabelle level using the command \isacommand{term}
+
+ \begin{isabelle}
+ \isacommand{term}~@{text [quotes] "BAR"}\\
+ @{text "> \"BAR\" :: \"'a\""}
+ \end{isabelle}
+
+ you do not obtain a constant of type @{typ nat}, but a free variable (printed in
+ blue) of polymorphic type. The problem is that the ML-expression above did
+ not register the declaration with the current theory. This is what the command
+ \isacommand{setup} is for. The constant is properly declared with
+*}
+
+setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
+
+text {*
+ Now
+
+ \begin{isabelle}
+ \isacommand{term}~@{text [quotes] "BAR"}\\
+ @{text "> \"BAR\" :: \"nat\""}
+ \end{isabelle}
+
+ returns a (black) constant with the type @{typ nat}.
+
+ A similar command is \isacommand{local\_setup}, which expects a function
+ of type @{ML_type "local_theory -> local_theory"}. Later on we will also
+ use the commands \isacommand{method\_setup} for installing methods in the
+ current theory and \isacommand{simproc\_setup} for adding new simprocs to
+ the current simpset.
+*}
+
section {* Theorem Attributes *}
text {*
@@ -1219,6 +1272,18 @@
@{text "> "}~@{thm test[my_sym]}
\end{isabelle}
+ An alternative for setting up an attribute is the function @{ML Attrib.setup}.
+ So instead of using \isacommand{attribute\_setup}, you can also set up the
+ attribute as follows:
+*}
+
+ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
+ "applying the sym rule" *}
+
+text {*
+ This gives a function from @{ML_type "Context.theory -> Context.theory"}, which
+ can be used for example with \isacommand{setup}.
+
As an example of a slightly more complicated theorem attribute, we implement
our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
as argument and resolve the proved theorem with this list (one theorem
@@ -1510,58 +1575,6 @@
*}
-section {* Setups (TBD) *}
-
-text {*
- In the previous section we used \isacommand{setup} in order to make
- a theorem attribute known to Isabelle. What happens behind the scenes
- is that \isacommand{setup} expects a function of type
- @{ML_type "theory -> theory"}: the input theory is the current theory and the
- output the theory where the theory attribute has been stored.
-
- This is a fundamental principle in Isabelle. A similar situation occurs
- for example with declaring constants. The function that declares a
- constant on the ML-level is @{ML Sign.add_consts_i}.
- If you write\footnote{Recall that ML-code needs to be
- enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
-*}
-
-ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
-
-text {*
- for declaring the constant @{text "BAR"} with type @{typ nat} and
- run the code, then you indeed obtain a theory as result. But if you
- query the constant on the Isabelle level using the command \isacommand{term}
-
- \begin{isabelle}
- \isacommand{term}~@{text [quotes] "BAR"}\\
- @{text "> \"BAR\" :: \"'a\""}
- \end{isabelle}
-
- you do not obtain a constant of type @{typ nat}, but a free variable (printed in
- blue) of polymorphic type. The problem is that the ML-expression above did
- not register the declaration with the current theory. This is what the command
- \isacommand{setup} is for. The constant is properly declared with
-*}
-
-setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
-
-text {*
- Now
-
- \begin{isabelle}
- \isacommand{term}~@{text [quotes] "BAR"}\\
- @{text "> \"BAR\" :: \"nat\""}
- \end{isabelle}
-
- returns a (black) constant with the type @{typ nat}.
-
- A similar command is \isacommand{local\_setup}, which expects a function
- of type @{ML_type "local_theory -> local_theory"}. Later on we will also
- use the commands \isacommand{method\_setup} for installing methods in the
- current theory and \isacommand{simproc\_setup} for adding new simprocs to
- the current simpset.
-*}
section {* Theories, Contexts and Local Theories (TBD) *}
--- a/ProgTutorial/Package/Ind_Intro.thy Sun Apr 26 23:45:22 2009 +0200
+++ b/ProgTutorial/Package/Ind_Intro.thy Wed Apr 29 00:36:14 2009 +0200
@@ -17,13 +17,13 @@
\medskip
HOL is based on just a few primitive constants, like equality and
implication, whose properties are described by axioms. All other concepts,
- such as inductive predicates, datatypes or recursive functions, have to be defined
- in terms of those constants, and the desired properties, for example
- induction theorems or recursion equations, have to be derived from the definitions
+ such as inductive predicates, datatypes or recursive functions, are defined
+ in terms of those primitives, and the desired properties, for example
+ induction theorems or recursion equations, are derived from the definitions
by a formal proof. Since it would be very tedious for a user to define
complex inductive predicates or datatypes ``by hand'' just using the
primitive operators of higher order logic, \emph{definitional packages} have
- been implemented automating such work. Thanks to those packages, the user
+ been implemented to automate such work. Thanks to those packages, the user
can give a high-level specification, for example a list of introduction
rules or constructors, and the package then does all the low-level
definitions and proofs behind the scenes. In this chapter we explain how
@@ -32,11 +32,11 @@
As the running example we have chosen a rather simple package for defining
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
+ the basis of Isabelle/HOL's standard inductive definition package. Instead, we
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
+ does neither support introduction rules involving arbitrary monotonic
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.
--- a/ProgTutorial/Tactical.thy Sun Apr 26 23:45:22 2009 +0200
+++ b/ProgTutorial/Tactical.thy Wed Apr 29 00:36:14 2009 +0200
@@ -734,7 +734,7 @@
Of course, this example is
contrived: there are much simpler methods available in Isabelle for
- implementing a proof procedure analysing a goal according to its topmost
+ implementing a tactic analysing a goal according to its topmost
connective. These simpler methods use tactic combinators, which we will
explain in the next section.
@@ -808,8 +808,8 @@
ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
text {*
- will first try out whether rule @{text disjI} applies and after that
- @{text conjI}. To see this consider the proof
+ will first try out whether rule @{text disjI} applies and in case of failure
+ will try @{text conjI}. To see this consider the proof
*}
lemma shows "True \<and> False" and "Foo \<or> Bar"
@@ -865,8 +865,21 @@
text {*
Remember that we chose to implement @{ML select_tac'} so that it
- always succeeds. This can be potentially very confusing for the user,
- for example, in cases where the goal is the form
+ always succeeds by adding @{ML all_tac} at the end of the tactic
+ list. The same can be achieved with the tactic combinator @{ML TRY}.
+ For example:
+*}
+
+ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+ rtac @{thm notI}, rtac @{thm allI}]*}
+text_raw{*\label{tac:selectprimeprime}*}
+
+text {*
+ This tactic behaves in the same way as @{ML select_tac'}: it tries out
+ one of the given tactics and if none applies leaves the goal state
+ unchanged. This, however, can be potentially very confusing when visible to
+ the user, for example, in cases where the goal is the form
+
*}
lemma shows "E \<Longrightarrow> F"
@@ -877,7 +890,8 @@
(*<*)oops(*>*)
text {*
- In this case no rule applies. The problem for the user is that there is little
+ In this case no rule applies, but because of @{ML TRY} or the inclusion of @{ML all_tac}
+ the tactics do not fail. The problem with this is that for the user there is little
chance to see whether or not progress in the proof has been made. By convention
therefore, tactics visible to the user should either change something or fail.
@@ -928,7 +942,7 @@
this is not possible).
If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
- need to implement it as
+ can implement it as
*}
ML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
@@ -936,7 +950,7 @@
text {*
since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
- If you look closely at the goal state above, the tactics @{ML repeat_xmp_tac}
+ If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
that goals 2 and 3 are not analysed. This is because the tactic
is applied repeatedly only to the first subgoal. To analyse also all
@@ -1116,7 +1130,7 @@
\end{center}
\end{isabelle}
- with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
+ with @{text "constr"} being a constant, like @{const "If"} or @{const "Let"}.
Every simpset contains only
one congruence rule for each term-constructor, which however can be
overwritten. The user can declare lemmas to be congruence rules using the
@@ -1137,7 +1151,7 @@
\begin{readmore}
For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
- @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in
+ @{ML_file "HOL/Tools/simpdata.ML"}. The generic splitter is implemented in
@{ML_file "Provers/splitter.ML"}.
\end{readmore}
@@ -1165,25 +1179,24 @@
\begin{isabelle}*}
ML{*fun print_ss ctxt ss =
let
- val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
+ val {simps, congs, procs, ...} = Simplifier.dest_ss ss
fun name_thm (nm, thm) =
" " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm)
fun name_ctrm (nm, ctrm) =
" " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
- val s = ["Simplification rules:"] @ (map name_thm simps) @
- ["Congruences rules:"] @ (map name_thm congs) @
- ["Simproc patterns:"] @ (map name_ctrm procs)
+ val s = ["Simplification rules:"] @ map name_thm simps @
+ ["Congruences rules:"] @ map name_thm congs @
+ ["Simproc patterns:"] @ map name_ctrm procs
in
- s |> separate "\n"
- |> implode
+ s |> cat_lines
|> writeln
end*}
text_raw {*
\end{isabelle}
\end{minipage}
-\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
+\caption{The function @{ML Simplifier.dest_ss} returns a record containing
all printable information stored in a simpset. We are here only interested in the
simplification rules, congruence rules and simprocs.\label{fig:printss}}
\end{figure} *}
@@ -1287,7 +1300,8 @@
The simplifier is often used to unfold definitions in a proof. For this the
- simplifier contains the @{ML rewrite_goals_tac}. Suppose for example the
+ simplifier implements the tactic @{ML rewrite_goals_tac}.\footnote{FIXME:
+ see LocalDefs infrastructure.} Suppose for example the
definition
*}
@@ -1499,7 +1513,7 @@
you can use the function:
*}
-ML %linenosgray{*fun fail_sp_aux simpset redex =
+ML %linenosgray{*fun fail_simproc simpset redex =
let
val ctxt = Simplifier.the_context simpset
val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex))
@@ -1517,7 +1531,7 @@
done by adding the simproc to the current simpset as follows
*}
-simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
+simproc_setup %gray fail ("Suc n") = {* K fail_simproc *}
text {*
where the second argument specifies the pattern and the right-hand side
@@ -1547,16 +1561,16 @@
with the declaration
*}
-declare [[simproc del: fail_sp]]
+declare [[simproc del: fail]]
text {*
If you want to see what happens with just \emph{this} simproc, without any
- interference from other rewrite rules, you can call @{text fail_sp}
+ interference from other rewrite rules, you can call @{text fail}
as follows:
*}
lemma shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail}]) 1*})
(*<*)oops(*>*)
text {*
@@ -1566,11 +1580,11 @@
Setting up a simproc using the command \isacommand{simproc\_setup} will
always add automatically the simproc to the current simpset. If you do not
want this, then you have to use a slightly different method for setting
- up the simproc. First the function @{ML fail_sp_aux} needs to be modified
+ up the simproc. First the function @{ML fail_simproc} needs to be modified
to
*}
-ML{*fun fail_sp_aux' simpset redex =
+ML{*fun fail_simproc' simpset redex =
let
val ctxt = Simplifier.the_context simpset
val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
@@ -1586,12 +1600,12 @@
*}
-ML{*val fail_sp' =
+ML{*val fail' =
let
val thy = @{theory}
val pat = [@{term "Suc n"}]
in
- Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+ Simplifier.simproc_i thy "fail_simproc'" pat (K fail_simproc')
end*}
text {*
@@ -1606,11 +1620,11 @@
*}
lemma shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail']) 1*})
(*<*)oops(*>*)
text {*
- The simproc @{ML fail_sp'} prints out the sequence
+ The simproc @{ML fail'} prints out the sequence
@{text [display]
"> Suc 0
@@ -1633,7 +1647,7 @@
*}
-ML{*fun plus_one_sp_aux ss redex =
+ML{*fun plus_one_simproc ss redex =
case redex of
@{term "Suc 0"} => NONE
| _ => SOME @{thm plus_one}*}
@@ -1642,12 +1656,12 @@
and set up the simproc as follows.
*}
-ML{*val plus_one_sp =
+ML{*val plus_one =
let
val thy = @{theory}
val pat = [@{term "Suc n"}]
in
- Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+ Simplifier.simproc_i thy "sproc +1" pat (K plus_one_simproc)
end*}
text {*
@@ -1658,7 +1672,7 @@
*}
lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
txt{*
where the simproc produces the goal state
@@ -1670,8 +1684,8 @@
text {*
As usual with rewriting you have to worry about looping: you already have
- a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
- the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+ a loop with @{ML plus_one}, if you apply it with the default simpset (because
+ the default simpset contains a rule which just does the opposite of @{ML plus_one},
namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful
in choosing the right simpset to which you add a simproc.
@@ -1735,7 +1749,7 @@
theorem for the simproc.
*}
-ML{*fun nat_number_sp_aux ss t =
+ML{*fun nat_number_simproc ss t =
let
val ctxt = Simplifier.the_context ss
in
@@ -1744,18 +1758,18 @@
end*}
text {*
- This function uses the fact that @{ML dest_suc_trm} might throw an exception
+ This function uses the fact that @{ML dest_suc_trm} might raise an exception
@{ML TERM}. In this case there is nothing that can be rewritten and therefore no
theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc
on an example, you can set it up as follows:
*}
-ML{*val nat_number_sp =
+ML{*val nat_number =
let
val thy = @{theory}
val pat = [@{term "Suc n"}]
in
- Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux)
+ Simplifier.simproc_i thy "nat_number" pat (K nat_number_simproc)
end*}
text {*
@@ -1763,7 +1777,7 @@
*}
lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
txt {*
you obtain the more legible goal state
@@ -1846,14 +1860,14 @@
val ten = @{cterm \"10::nat\"}
val thm = Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
in
- #prop (rep_thm thm)
+ Thm.prop_of thm
end"
"Const (\"==\",\<dots>) $
(Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $
(Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
The argument @{ML true} in @{ML Thm.beta_conversion} indicates that
- the right-hand side will be fully beta-normalised. If instead
+ the right-hand side should be fully beta-normalised. If instead
@{ML false} is given, then only a single beta-reduction is performed
on the outer-most level. For example
@@ -1891,7 +1905,7 @@
Note, however, that the function @{ML Conv.rewr_conv} only rewrites the
outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
exactly the
- left-hand side of the theorem, then @{ML Conv.rewr_conv} raises
+ left-hand side of the theorem, then @{ML Conv.rewr_conv} fails by raising
the exception @{ML CTERM}.
This very primitive way of rewriting can be made more powerful by
@@ -1962,15 +1976,15 @@
stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
the conversion to the first argument of an application.
- The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
+ The function @{ML Conv.abs_conv} applies a conversion under an abstraction.
For example:
@{ML_response_fake [display,gray]
"let
- val conv = K (Conv.rewr_conv @{thm true_conj1})
+ val conv = Conv.rewr_conv @{thm true_conj1}
val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
in
- Conv.abs_conv conv @{context} ctrm
+ Conv.abs_conv (K conv) @{context} ctrm
end"
"\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
@@ -2071,11 +2085,11 @@
Here is a tactic doing exactly that:
*}
-ML{*fun true1_tac ctxt = CSUBGOAL (fn (goal, i) =>
+ML{*fun true1_tac ctxt =
CONVERSION
(Conv.params_conv ~1 (fn ctxt =>
(Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
- Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i)*}
+ Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt)*}
text {*
We call the conversions with the argument @{ML "~1"}. This is to
@@ -2100,9 +2114,10 @@
As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
the conclusion according to @{ML all_true1_conv}.
- To sum up this section, conversions are not as powerful as the simplifier
- and simprocs; the advantage of conversions, however, is that you never have
- to worry about non-termination.
+ To sum up this section, conversions are more general than the simplifier
+ or simprocs, but you have to do more work yourself. Also conversions are
+ often much less efficient than the simplifier. The advantage of conversions,
+ however, that they provide much less room for non-termination.
\begin{exercise}\label{ex:addconversion}
Write a tactic that does the same as the simproc in exercise
@@ -2120,7 +2135,7 @@
\begin{readmore}
See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.
- Further conversions are defined in @{ML_file "Pure/thm.ML"},
+ Some basic conversions are defined in @{ML_file "Pure/thm.ML"},
@{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
\end{readmore}