# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1249395519 -7200
# Node ID 05e6a33edef665cc5bd331ac6a2366ff60069da4
# Parent  0cbd34857b9e6f49d9dfd2c1485b24a5cc6474a3
added an antiquotation for printing the raw proof state; polished the example about proof state

diff -r 0cbd34857b9e -r 05e6a33edef6 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Mon Aug 03 16:47:01 2009 +0200
+++ b/ProgTutorial/Intro.thy	Tue Aug 04 16:18:39 2009 +0200
@@ -4,6 +4,7 @@
 
 chapter {* Introduction *}
 
+
 text {*
    \begin{flushright}
   {\em
diff -r 0cbd34857b9e -r 05e6a33edef6 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Aug 03 16:47:01 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Aug 04 16:18:39 2009 +0200
@@ -17,6 +17,7 @@
 
 *}
 
+
 section {* Basics of Reasoning with Tactics*}
 
 text {*
@@ -222,6 +223,8 @@
   \begin{boxedminipage}{\textwidth}
   \begin{isabelle}
 *}
+notation (output) "prop"  ("#_" [1000] 1000)
+
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
 apply(tactic {* my_print_tac @{context} *})
 
@@ -233,7 +236,7 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
 *}
@@ -249,7 +252,7 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
 *}
@@ -265,7 +268,7 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
 *}
@@ -281,11 +284,11 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip   
    *}
-done
+(*<*)oops(*>*)
 text_raw {*  
   \end{isabelle}
   \end{boxedminipage}
@@ -294,8 +297,8 @@
   the goal state as represented internally (highlighted boxes). This
   tactic shows that every goal state in Isabelle is represented by a theorem:
   when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
-  @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
-  theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
+  @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
+  theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}.\label{fig:goalstates}}
   \end{figure}
 *}
 
@@ -307,17 +310,17 @@
   proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, 
   internally every goal state is an implication of the form
 
-  @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
+  @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
 
   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
   the subgoals. So after setting up the lemma, the goal state is always of the
-  form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
-  "(C)"}.\footnote{This only applies to single statements. If the lemma
+  form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
+  "#C"}.\footnote{This only applies to single statements. If the lemma
   contains more than one statement, then one has more such implications.} 
   Since the goal @{term C} can potentially be an implication, there is a
   ``protector'' wrapped around it (the wrapper is the outermost constant
-  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant is invisible
-  in the figure). This wrapper prevents that premises of @{text C} are
+  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
+  as an @{text #}). This wrapper prevents that premises of @{text C} are
   misinterpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   @{term C} intact, with the exception of possibly instantiating schematic
diff -r 0cbd34857b9e -r 05e6a33edef6 ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Mon Aug 03 16:47:01 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue Aug 04 16:18:39 2009 +0200
@@ -106,22 +106,22 @@
 
 (* replaces the official subgoal antiquotation with one *)
 (* that is closer to the actual output                  *)
+fun proof_state state =
+    (case try Toplevel.proof_of state of
+      SOME prf => prf
+    | _ => error "No proof state")
+
 fun output_goals  {state = node, ...}  _ = 
 let
   fun subgoals 0 = ""
     | subgoals 1 = "goal (1 subgoal):"
     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
 
-  fun proof_state state =
-    (case try Toplevel.proof_of state of
-      SOME prf => prf
-    | _ => error "No proof state")
-
   val state = proof_state node;
   val goals = Pretty.chunks (Proof.pretty_goals false state);
 
   val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
-  val (As, B) = Logic.strip_horn prop;
+  val (As, _) = Logic.strip_horn prop;
   val output  = (case (length As) of
                       0 => [goals] 
                     | n => [Pretty.str (subgoals n), goals])  
@@ -129,6 +129,20 @@
   ThyOutput.output output
 end
 
+fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
+let
+  val state = proof_state node;
+  val goals = (Proof.get_goal state |> snd |> snd)
+
+  val output  = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]  
+  val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))
+  val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
+in 
+  ThyOutput.output output
+end
+
+
 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
- 
+val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
+
 end;
diff -r 0cbd34857b9e -r 05e6a33edef6 progtutorial.pdf
Binary file progtutorial.pdf has changed