201 text {* Let us assume the following four string conversion functions: *}

   202 

   203 ML{*fun str_of_cterm ctxt t =  

   204    Syntax.string_of_term ctxt (term_of t)

   205 

   206 fun str_of_cterms ctxt ts =  

   207   commas (map (str_of_cterm ctxt) ts)

   208 

   209 fun str_of_thm ctxt thm =

   210   let

   211     val {prop, ...} = crep_thm thm

   212   in 

   213     str_of_cterm ctxt prop

   214   end

   215 

   216 fun str_of_thms ctxt thms =  

   217   commas (map (str_of_thm ctxt) thms)*}

   218 

   219 text {*

   220   and the following function

   221 *}

   222 

   223 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 

   224   let 

   225     val str_of_params = str_of_cterms context params

   226     val str_of_asms = str_of_cterms context asms

   227     val str_of_concl = str_of_cterm context concl

   228     val str_of_prems = str_of_thms context prems   

   229     val str_of_schms = str_of_cterms context (snd schematics)    

   230  

   231     val _ = (warning ("params: " ^ str_of_params);

   232              warning ("schematics: " ^ str_of_schms);

   233              warning ("asms: " ^ str_of_asms);

   234              warning ("concl: " ^ str_of_concl);

   235              warning ("prems: " ^ str_of_prems))

   236   in

   237     no_tac 

   238   end*}

   239 

   240 text {*

   241   then the tactic @{ML SUBPROOF} fixes the parameters and binds the various components

   242   of a proof state into a record. For example 

   243 *}

   244 

   245 lemma 

   246   shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"

   247 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?

   248 

   249 txt {*

   250   prints out 

   251 

   252   \begin{center}

   253   \begin{tabular}{ll}

   254   params:     & @{term x}, @{term y}\\

   255   schematics: & @{term z}\\

   256   asms:       & @{term "A x y"}\\

   257   concl:      & @{term "B y x \<longrightarrow> C (z y) x"}\\

   258   prems:      & @{term "A x y"}

   259   \end{tabular}

   260   \end{center}

   261 

   262   Continuing the proof script with

   263 *}

   264 

   265 apply(rule impI)

   266 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?

   267 

   268 txt {*

   269   prints out 

   270 

   271   \begin{center}

   272   \begin{tabular}{ll}

   273   params:     & @{term x}, @{term y}\\

   274   schematics: & @{term z}\\

   275   asms:       & @{term "A x y"}, @{term "B y x"}\\

   276   concl:      & @{term "C (z y) x"}\\

   277   prems:      & @{term "A x y"}, @{term "B y x"}

   278   \end{tabular}

   279   \end{center}

   280 *}

   281 (*<*)oops(*>*)

   282 

   283 

   346 section {* Structured Proofs *}

   347 

   348 lemma True

   349 proof

   350 

   351   {

   352     fix A B C

   353     assume r: "A & B \<Longrightarrow> C"

   354     assume A B

   355     then have "A & B" ..

   356     then have C by (rule r)

   357   }

   358 

   359   {

   360     fix A B C

   361     assume r: "A & B \<Longrightarrow> C"

   362     assume A B

   363     note conjI [OF this]

   364     note r [OF this]

   365   }

   366 oops

   367 

   368 ML {* fun prop ctxt s =

   369   Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}

   370 

   371 ML {* 

   372   val ctxt0 = @{context};

   373   val ctxt = ctxt0;

   374   val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;

   375   val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;

   376   val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;

   377   val this = [@{thm conjI} OF this]; 

   378   val this = r OF this;

   379   val this = Assumption.export false ctxt ctxt0 this 

   380   val this = Variable.export ctxt ctxt0 [this] 

   381 *}