
diff -r f118240ab44a -r 9f12e53eb121 ProgTutorial/General.thy
--- 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} *}




