--- a/ProgTutorial/General.thy	Sat Oct 10 20:27:51 2009 +0200
+++ b/ProgTutorial/General.thy	Sun Oct 11 01:47:15 2009 +0200
@@ -874,24 +874,36 @@
 (\<lambda>x. x) = (\<lambda>x. x)"}
 
   Other function produce terms that can be pattern-matched. 
-  Suppose the following theorem.
+  Suppose the following two theorems.
 *}
 
-lemma foo_test: 
-  shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry
+lemma  
+  shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C" 
+  and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
 
 text {*
-  We can deconstruct it into premises and conclusion. 
+  We can deconstruct them into premises and conclusions as follows. 
 
  @{ML_response_fake [display,gray]
 "let
-  val thm = @{thm foo_test}
+  val ctxt = @{context}
+  fun prems_and_concl thm =
+     [\"Premises: \" ^ 
+        (string_of_terms ctxt (Thm.prems_of thm))] @ 
+     [\"Conclusion: \" ^ 
+        (string_of_term ctxt (Thm.concl_of thm))]
+     |> cat_lines
+     |> tracing
 in
-  (Thm.prems_of thm, [Thm.concl_of thm]) 
-  |> pairself (tracing o string_of_terms @{context})
+  prems_and_concl @{thm foo_test1};
+  prems_and_concl @{thm foo_test2}
 end"
-"?A, ?B
-?C"}
+"Premises: ?A, ?B
+Conclusion: ?C
+Premises: 
+Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
+
+  Note that in the second case, there is no premise.
 
   \begin{readmore}
   For the functions @{text "assume"}, @{text "forall_elim"} etc 
@@ -899,11 +911,83 @@
   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   \end{readmore}
 
+
+  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
+
+  @{ML_response_fake [display, gray]
+  "ObjectLogic.rulify @{thm foo_test2}"
+  "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
+
+  The transformation in the other direction can be achieved with function
+  @{ML_ind atomize in ObjectLogic} and the following code.
+
+  @{ML_response_fake [display,gray]
+  "let
+  val thm = @{thm foo_test1}
+  val meta_eq = ObjectLogic.atomize (cprop_of thm)
+in
+  MetaSimplifier.rewrite_rule [meta_eq] thm
+end"
+  "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
+
+  In this code the function @{ML atomize in ObjectLogic} produces 
+  a meta-equation between the given theorem and the theorem transformed
+  into the object logic. The function @{ML_ind rewrite_rule in MetaSimplifier}
+  unfolds this meta-equation in the given theorem. The result is
+  the theorem with object logic connectives.
+x
+  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
+  
+  @{ML_response_fake [display,gray]
+  "let
+  val trm = @{term \"P \<Longrightarrow> P::bool\"}
+  val tac = K (atac 1)
+in
+  Goal.prove @{context} [\"P\"] [] trm tac
+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. We explain tactics in 
+  Chapter~\ref{chp:tactical}. 
+
+  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. 
+*}
+
+lemma foo_data: "P \<Longrightarrow> P" by assumption
+
+text {*
+  The auxiliary data of this lemma is as follows. 
+
+  @{ML_response_fake [display,gray]
+  "Thm.get_tags @{thm foo_data}"
+  " [(\"name\", \"FirstSteps.foo_data\"), (\"kind\", \"lemma\")]"}
+*}
+
+
+local_setup {*
+  LocalTheory.note Thm.theoremK
+      ((@{binding "rr2"}, []), [(RuleCases.name ["a"] @{thm foo_data})]) #> snd *}
+
+ML {* Thm.get_tags @{thm rr2} *}
+
+lemma
+  "Q \<Longrightarrow> Q"
+proof (induct rule: rr2)
+oops
+
+text {*
   TBD below.
 
-  (FIXME: handy functions working on theorems, like @{ML_ind  rulify in ObjectLogic} and so on) 
-
-  (FIXME: @{ML_ind prove in Goal})
 
   (FIXME: how to add case-names to goal states - maybe in the 
   next section)
@@ -1221,7 +1305,7 @@
 
 
 
-section {* Theories, Contexts and Local Theories (TBD) *}
+section {* Theories (TBD) *}
 
 text {*
   There are theories, proof contexts and local theories (in this order, if you
@@ -1236,6 +1320,10 @@
   valid local theory.
 *}
 
+section {* Contexts (TBD) *}
+
+section {* Local Theories (TBD) *}
+
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML_ind  add_thms_dynamic in PureThy} *}