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 "\A; B\ \ A \ B" apply(tactic {* my_print_tac @{context} *}) @@ -233,7 +236,7 @@ \small\colorbox{gray!20}{ \begin{tabular}{@ {}l@ {}} internal goal state:\\ - @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"} + @{raw_goal_state} \end{tabular}} \end{minipage}\medskip *} @@ -249,7 +252,7 @@ \small\colorbox{gray!20}{ \begin{tabular}{@ {}l@ {}} internal goal state:\\ - @{text "(\A; B\ \ A) \ (\A; B\ \ B) \ (\A; B\ \ A \ B)"} + @{raw_goal_state} \end{tabular}} \end{minipage}\medskip *} @@ -265,7 +268,7 @@ \small\colorbox{gray!20}{ \begin{tabular}{@ {}l@ {}} internal goal state:\\ - @{text "(\A; B\ \ B) \ (\A; B\ \ A \ B)"} + @{raw_goal_state} \end{tabular}} \end{minipage}\medskip *} @@ -281,11 +284,11 @@ \small\colorbox{gray!20}{ \begin{tabular}{@ {}l@ {}} internal goal state:\\ - @{text "\A; B\ \ A \ 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 "\A; B\ \ A \ B"}} the theorem is - @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"}; when you finish the proof the - theorem is @{text "\A; B\ \ A \ B"}.\label{fig:goalstates}} + @{text "(\A; B\ \ A \ B) \ #(\A; B\ \ A \ B)"}; when you finish the proof the + theorem is @{text "#(\A; B\ \ A \ 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 \ \ \ A\<^isub>n \ (C)"} + @{text[display] "A\<^isub>1 \ \ \ A\<^isub>n \ #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 \ (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 \ #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 \ bool)"}; however this constant is invisible - in the figure). This wrapper prevents that premises of @{text C} are + @{text "Const (\"prop\", bool \ 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