# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1233779198 0
# Node ID 7235374f34c85b66073b5bac0663fab74ace7c67
# Parent  531e453c9d674b3e8deac0016bc5970b50b18931
added some preliminary notes about SUBPROOF

diff -r 531e453c9d67 -r 7235374f34c8 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Fri Jan 30 16:58:31 2009 +0100
+++ b/CookBook/Tactical.thy	Wed Feb 04 20:26:38 2009 +0000
@@ -198,6 +198,89 @@
 apply(tactic {* print_tac "foo message" *})
 (*<*)oops(*>*)
 
+text {* Let us assume the following four string conversion functions: *}
+
+ML{*fun str_of_cterm ctxt t =  
+   Syntax.string_of_term ctxt (term_of t)
+
+fun str_of_cterms ctxt ts =  
+  commas (map (str_of_cterm ctxt) ts)
+
+fun str_of_thm ctxt thm =
+  let
+    val {prop, ...} = crep_thm thm
+  in 
+    str_of_cterm ctxt prop
+  end
+
+fun str_of_thms ctxt thms =  
+  commas (map (str_of_thm ctxt) thms)*}
+
+text {*
+  and the following function
+*}
+
+ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
+  let 
+    val str_of_params = str_of_cterms context params
+    val str_of_asms = str_of_cterms context asms
+    val str_of_concl = str_of_cterm context concl
+    val str_of_prems = str_of_thms context prems   
+    val str_of_schms = str_of_cterms context (snd schematics)    
+ 
+    val _ = (warning ("params: " ^ str_of_params);
+             warning ("schematics: " ^ str_of_schms);
+             warning ("asms: " ^ str_of_asms);
+             warning ("concl: " ^ str_of_concl);
+             warning ("prems: " ^ str_of_prems))
+  in
+    no_tac 
+  end*}
+
+text {*
+  then the tactic @{ML SUBPROOF} fixes the parameters and binds the various components
+  of a proof state into a record. For example 
+*}
+
+lemma 
+  shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
+apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+
+txt {*
+  prints out 
+
+  \begin{center}
+  \begin{tabular}{ll}
+  params:     & @{term x}, @{term y}\\
+  schematics: & @{term z}\\
+  asms:       & @{term "A x y"}\\
+  concl:      & @{term "B y x \<longrightarrow> C (z y) x"}\\
+  prems:      & @{term "A x y"}
+  \end{tabular}
+  \end{center}
+
+  Continuing the proof script with
+*}
+
+apply(rule impI)
+apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+
+txt {*
+  prints out 
+
+  \begin{center}
+  \begin{tabular}{ll}
+  params:     & @{term x}, @{term y}\\
+  schematics: & @{term z}\\
+  asms:       & @{term "A x y"}, @{term "B y x"}\\
+  concl:      & @{term "C (z y) x"}\\
+  prems:      & @{term "A x y"}, @{term "B y x"}
+  \end{tabular}
+  \end{center}
+*}
+(*<*)oops(*>*)
+
+
 text {*
   @{ML PRIMITIVE}? @{ML SUBGOAL} see page 32 in ref
 *}
@@ -222,7 +305,7 @@
 
 
 text {*
-  @{ML EVERY} @{ML REPEAT} @{ML SUBPROOF}
+  @{ML EVERY} @{ML REPEAT} 
 
   @{ML rewrite_goals_tac}
   @{ML cut_facts_tac}
@@ -260,6 +343,42 @@
 
 *}
 
+section {* Structured Proofs *}
+
+lemma True
+proof
+
+  {
+    fix A B C
+    assume r: "A & B \<Longrightarrow> C"
+    assume A B
+    then have "A & B" ..
+    then have C by (rule r)
+  }
+
+  {
+    fix A B C
+    assume r: "A & B \<Longrightarrow> C"
+    assume A B
+    note conjI [OF this]
+    note r [OF this]
+  }
+oops
+
+ML {* fun prop ctxt s =
+  Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}
+
+ML {* 
+  val ctxt0 = @{context};
+  val ctxt = ctxt0;
+  val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;
+  val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;
+  val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;
+  val this = [@{thm conjI} OF this]; 
+  val this = r OF this;
+  val this = Assumption.export false ctxt ctxt0 this 
+  val this = Variable.export ctxt ctxt0 [this] 
+*}
 
 
 end
\ No newline at end of file