--- a/ProgTutorial/General.thy Sun Oct 18 21:22:44 2009 +0200
+++ b/ProgTutorial/General.thy Mon Oct 19 02:02:21 2009 +0200
@@ -316,9 +316,14 @@
function that strips off the outermost quantifiers in a term.
*}
-ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
- strip_alls t |>> cons (Free (n, T))
- | strip_alls t = ([], t) *}
+ML{*fun strip_alls t =
+let
+ fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
+in
+ case t of
+ Const ("All", _) $ Abs body => aux body
+ | _ => ([], t)
+end*}
text {*
The function returns a pair consisting of the stripped off variables and
@@ -343,10 +348,25 @@
end"
"x = y"}
- Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls}
- returned. The reason is that the head of the list the function @{ML subst_bounds}
- takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}
- and so on.
+ Note that in Line 4 we had to reverse the list of variables that @{ML
+ strip_alls} returned. The reason is that the head of the list the function
+ @{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next
+ element for @{ML "Bound 1"} and so on.
+
+ Notice also that this function might introduce name clashes, since we
+ substitute just a variable with the name recorded in an abstraction. This
+ name is by no means unique. If clashes need to be avoided, then we should
+ use the function @{ML_ind dest_abs in Term}, which returns the body where
+ the lose de Bruijn index is replaced by a unique free variable. For example
+
+
+ @{ML_response_fake [display,gray]
+ "let
+ val app = Bound 0 $ Free (\"x\", @{typ nat})
+in
+ Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, app)
+end"
+ "(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
There are also many convenient functions that construct specific HOL-terms
in the structure @{ML_struct HOLogic}. For
@@ -936,7 +956,7 @@
The simplifier can be used to unfold definition in theorms. To show
this we build the theorem @{term "True \<equiv> True"} (Line 1) and then
- unfold the constant according to its definition (Line 2).
+ unfold the constant @{term "True"} according to its definition (Line 2).
@{ML_response_fake [display,gray,linenos]
"Thm.reflexive @{cterm \"True\"}
@@ -946,9 +966,12 @@
"(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
Often it is necessary to transform theorems to and from the object
- logic. For example, the function @{ML_ind rulify in ObjectLogic}
- replaces all @{text "\<longrightarrow>"} and @{text "\<forall>"} into the equivalents of the
- meta logic. For example
+ logic, that is eplacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} with @{text "\<Longrightarrow>"}
+ and @{text "\<And>"}, respectively. A reason for such transformations is
+ that definitions can only be stated using object logic connectives, while
+ theorems using the connectives from the meta logic are more convenient for
+ reasoning. The function @{ML_ind rulify in ObjectLogic} replaces all
+ object connectives by equivalents in the meta logic. For example
@{ML_response_fake [display, gray]
"ObjectLogic.rulify @{thm foo_test2}"
@@ -975,8 +998,9 @@
@{thm [display] list.induct}
we have to first abstract over the meta variables @{text "?P"} and
- @{text "?list"}. For this we can use the function
- @{ML_ind forall_intr_vars in Drule}.
+ @{text "?list"} in the theorem. For this we can use the function
+ @{ML_ind forall_intr_vars in Drule}. This allows us to implement the
+ following function for atomizing a theorem.
*}
ML{*fun atomize_thm thm =
@@ -988,15 +1012,16 @@
end*}
text {*
- For the theorem @{thm [source] list.induct}, this function produces:
+ This function produces for the theorem @{thm [source] list.induct}
@{ML_response_fake [display, gray]
"atomize_thm @{thm list.induct}"
"\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
Theorems can also be produced from terms by giving an explicit proof.
- One way to achive this is by using the function @{ML_ind prove in Goal}.
- For example below we prove the term @{term "P \<Longrightarrow> P"}.
+ One way to achive this is by using the function @{ML_ind prove in Goal}
+ in the structure @{ML_struct Goal}. For example below we prove the term
+ @{term "P \<Longrightarrow> P"}.
@{ML_response_fake [display,gray]
"let
@@ -1007,35 +1032,37 @@
end"
"?P \<Longrightarrow> ?P"}
- This function takes as second argument a list of strings. This list specifies
- which variables should be turned into meta-variables once the term is proved.
- The proof is given in form of a tactic as last argument. We explain tactics in
- Chapter~\ref{chp:tactical}. In the code above the tactic proved the theorem
+ This function takes first a context and second a list of strings. This list
+ specifies which variables should be turned into meta-variables once the term
+ is proved. The fourth argument is the term to be proved. The fifth is a
+ corresponding proof given in form of a tactic. We explain tactics in
+ Chapter~\ref{chp:tactical}. In the code above, the tactic proves the theorem
by assumption.
- Theorems also contain auxiliary data, such their names and kind, but also
- names for cases etc. This data is stored in a string-string list and can
- be retrieved with the function @{ML_ind get_tags in Thm}. Assume the
- following lemma.
+ Theorems also contain auxiliary data, such as the name of the theorem, its
+ kind, the names for cases and so on. This data is stored in a string-string
+ list and can be retrieved with the function @{ML_ind get_tags in
+ Thm}. Assume the following lemma.
*}
lemma foo_data: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
text {*
- The auxiliary data of this lemma is as follows.
+ So far the the auxiliary data of this lemma is:
@{ML_response_fake [display,gray]
"Thm.get_tags @{thm foo_data}"
"[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
- When we store lemmas in the theorem database, we can explicitly extend the data
- associated with this lemma by attaching case names.
+ When we store lemmas in the theorem database, we may want to explicitly extend
+ this data by attaching case names to the two premises of the lemma. This can
+ be achieved with the function @{ML_ind name in RuleCases}.
*}
local_setup %gray {*
LocalTheory.note Thm.lemmaK
((@{binding "foo_data'"}, []),
- [(RuleCases.name ["foo_case1", "foo_case2"]
+ [(RuleCases.name ["foo_case_one", "foo_case_two"]
@{thm foo_data})]) #> snd *}
text {*
@@ -1044,69 +1071,101 @@
@{ML_response_fake [display,gray]
"Thm.get_tags @{thm foo_data'}"
"[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"),
- (\"case_names\", \"foo_case1;foo_case2\")]"}
+ (\"case_names\", \"foo_case_one;foo_case_two\")]"}
- You notice the difference when using the proof methods @{ML_text cases}
- or @{ML_text induct}. In the proof below
+ You can notice the case names on the user level when using the proof
+ methods @{ML_text cases} and @{ML_text induct}. In the proof below
*}
lemma
- "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+ shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
proof (cases rule: foo_data')
-print_cases
+
(*<*)oops(*>*)
+text_raw{*
+\begin{tabular}{@ {}l}
+\isacommand{print\_cases}\\
+@{text "> cases:"}\\
+@{text "> foo_case_one:"}\\
+@{text "> let \"?case\" = \"?P\""}\\
+@{text "> foo_case_two:"}\\
+@{text "> let \"?case\" = \"?P\""}
+\end{tabular}*}
text {*
- we can proceed by analysing the cases @{ML_text "foo_case1"} and
- @{ML_text "foo_case2"}. While if the theorem has no names, then
- the cases have standard names @{ML_text 1}, @{ML_text 2} and so
+ we can proceed by analysing the cases @{text "foo_case1"} and
+ @{text "foo_case2"}. While if the theorem has no names, then
+ the cases have standard names @{text 1}, @{text 2} and so
on. This can be seen in the proof below.
*}
lemma
- "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+ shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
proof (cases rule: foo_data)
-print_cases
+
(*<*)oops(*>*)
+text_raw{*
+\begin{tabular}{@ {}l}
+\isacommand{print\_cases}\\
+@{text "> cases:"}\\
+@{text "> 1:"}\\
+@{text "> let \"?case\" = \"?P\""}\\
+@{text "> 2:"}\\
+@{text "> let \"?case\" = \"?P\""}
+\end{tabular}*}
+
text {*
- TBD below
-
- One great feature of Isabelle is its document preparation system where
+ One great feature of Isabelle is its document preparation system, where
proved theorems can be quoted in the text directly from the formalisation.
-
- (FIXME: example for how to add theorem styles)
+ This helps minimises cut-and-paste errors. However, sometimes the verbatim
+ quoting is not what is wanted. For such situations Isabelle allows the
+ installation of \emph{styles}. These are, roughly speaking, functions from
+ terms to terms. The input term stands for the theorem to be presented.
+ Let us assume we want to display theorems without leading quantifiers.
+ For this we can implement the following function that strips off
+ meta-quantifiers.
*}
-ML {*
-fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) =
- strip_assums_all ((a, T)::params, t)
- | strip_assums_all (params, B) = (params, B)
+ML {*fun strip_all (Const (@{const_name "All"}, _) $ Abs body) =
+ Term.dest_abs body |> snd |> strip_all
+ | strip_all (Const (@{const_name "Trueprop"}, _) $ t) = strip_all t
+ | strip_all t = t*}
+
+ML {* strip_all @{term "\<forall>x y z. P x y z"}*}
-fun style_parm_premise i ctxt t =
- let val prems = Logic.strip_imp_prems t in
- if i <= length prems
- then let val (params,t) = strip_assums_all([], nth prems (i - 1))
- in subst_bounds(map Free params, t) end
- else error ("Not enough premises for prem" ^ string_of_int i ^
- " in propositon: " ^ string_of_term ctxt t)
- end;
+text {*
+ Now we can install this function as the theorem style named
+ @{text "strip_all"}.
+*}
+
+setup %gray {*
+ Term_Style.setup "strip_all" (Scan.succeed (K strip_all))
+*}
+
+text {*
+ We can test the theorem style with the following theorem
*}
-ML {*
-strip_assums_all ([], @{term "\<And>x y. A x y"})
-*}
+theorem style_test:
+ shows "\<forall>x y z. (x, x) = (y, z)" sorry
+
+text {*
+ Now printing out the theorem @{thm [source] style_test} normally
+ in a document produces
+
+ @{thm [display] style_test}
-(*
-setup %gray {*
- TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
- TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
+ as expected. But with the theorem style @{text "@{thm (strip_all) \<dots>}"}
+ we obtain
+
+ @{thm [display] (strip_all) style_test}
+
+ without the leading quantifiers. Such theorem styles allow one to
+ print out theorems in documents formatted in any way wanted. Next we
+ explain theorem attributes, which is another mechanism for treating
+ theorems.
*}
-*)
-lemma
- shows "A \<Longrightarrow> B"
- and "C \<Longrightarrow> D"
-oops
section {* Theorem Attributes\label{sec:attributes} *}