# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1248946732 -7200
# Node ID ee9d53fbb56be63c781e737f90a5164248d0432f
# Parent  0a567f923b42b35f88999ad063870867a06bb1e7
made changes for SUBPROOF and sat_tac

diff -r 0a567f923b42 -r ee9d53fbb56b ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Tue Jul 28 12:11:33 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Thu Jul 30 11:38:52 2009 +0200
@@ -633,7 +633,7 @@
 ML{*fun chop_test_tac preds rules =
   SUBPROOF_test (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     chop_print params1 params2 prems1 prems2 context; no_tac
@@ -698,7 +698,7 @@
 ML %linenosgray{*fun apply_prem_tac i preds rules =
   SUBPROOF_test (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -773,7 +773,7 @@
 ML{*fun prove_intro_tac i preds rules =
   SUBPROOF (fn {params, prems, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -868,7 +868,7 @@
 ML %linenosgray{*fun prove_intro_tac i preds rules =
   SUBPROOF (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
diff -r 0a567f923b42 -r ee9d53fbb56b ProgTutorial/Package/simple_inductive_package.ML
--- a/ProgTutorial/Package/simple_inductive_package.ML	Tue Jul 28 12:11:33 2009 +0200
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Thu Jul 30 11:38:52 2009 +0200
@@ -129,7 +129,7 @@
  SUBPROOF (fn {params, prems, context = ctxt', ...} =>
   let
     val (prems1, prems2) = chop (length prems - length rules) prems;
-    val (params1, params2) = chop (length params - length preds) params;
+    val (params1, params2) = chop (length params - length preds) (map snd params);
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 
     THEN
diff -r 0a567f923b42 -r ee9d53fbb56b ProgTutorial/Recipes/Sat.thy
--- a/ProgTutorial/Recipes/Sat.thy	Tue Jul 28 12:11:33 2009 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Thu Jul 30 11:38:52 2009 +0200
@@ -101,7 +101,7 @@
 *}
 
 lemma "True"
-apply(tactic {* sat.sat_tac 1 *})
+apply(tactic {* sat.sat_tac @{context} 1 *})
 done
 
 text {*
diff -r 0a567f923b42 -r ee9d53fbb56b ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Tue Jul 28 12:11:33 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Thu Jul 30 11:38:52 2009 +0200
@@ -538,15 +538,19 @@
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
+
+
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
 let 
-  val string_of_params = string_of_cterms context params
+  val string_of_params = string_of_cterms context (map snd params)
+  val test = commas (map fst params)
   val string_of_asms = string_of_cterms context asms
   val string_of_concl = string_of_cterm context concl
   val string_of_prems = string_of_thms_no_vars context prems   
   val string_of_schms = string_of_cterms context (snd schematics)    
  
   val _ = (writeln ("params: " ^ string_of_params);
+           writeln ("param names: " ^ test);
            writeln ("schematics: " ^ string_of_schms);
            writeln ("assumptions: " ^ string_of_asms);
            writeln ("conclusion: " ^ string_of_concl);
@@ -563,7 +567,6 @@
 \end{figure}
 *}
 
-
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 
@@ -1056,6 +1059,8 @@
   will solve all trivial subgoals involving @{term True} or @{term "False"}.
 
   (FIXME: say something about @{ML [index] COND} and COND')
+
+  (FIXME: say something about @{ML [index] FOCUS})
   
   \begin{readmore}
   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
diff -r 0a567f923b42 -r ee9d53fbb56b progtutorial.pdf
Binary file progtutorial.pdf has changed