# HG changeset patch
# User wenzelm
# Date 1479655084 -3600
# Node ID 488cb71eeb836bb5ee18fc466f1317da719911ab
# Parent  80aaa4ff7fedd69ffc6b5773a5d6d0515ae430b4
more on Isar proof language;

diff -r 80aaa4ff7fed -r 488cb71eeb83 src/Doc/Isar_Ref/Framework.thy
--- a/src/Doc/Isar_Ref/Framework.thy	Sun Nov 20 15:53:07 2016 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy	Sun Nov 20 16:18:04 2016 +0100
@@ -485,11 +485,58 @@
   entities of Pure (propositions, facts, and goals). The Isar proof language
   allows to organize reasoning within the underlying rule calculus of Pure,
   but Isar is not another logical calculus. Isar merely imposes certain
-  structure and policies on Pure inferences.
+  structure and policies on Pure inferences. The main grammar of the Isar
+  proof language is given in \figref{fig:isar-syntax}.
 
-  Isar is intended as an exercise in minimalism. Approximately half of the
-  language is introduced as primitive, the rest defined as derived concepts.
-  The grammar in \appref{ap:main-grammar} describes the core language
+  \begin{figure}[htb]
+  \begin{center}
+  \begin{tabular}{rcl}
+    \<open>main\<close> & \<open>=\<close> & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if name: props for vars\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
+    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
+    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
+    & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
+    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
+    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
+    & & \quad\<^theory_text>\<open>obtains (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
+    \<open>proof\<close> & \<open>=\<close> & \<^theory_text>\<open>"refinement\<^sup>* proper_proof"\<close> \\
+    \<open>refinement\<close> & \<open>=\<close> &  \<^theory_text>\<open>apply method\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
+    \<open>proper_proof\<close> & \<open>=\<close> & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>by method method\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>..\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>.\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>sorry\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>done\<close> \\
+    \<open>statement\<close> & \<open>=\<close> & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>next\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>presume name: props if props for vars\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>define clause\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>case name: "case"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>from thms goal\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>with thms goal\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>also\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>finally goal\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>moreover\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>ultimately goal\<close> \\
+    \<open>goal\<close> & \<open>=\<close> & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>show name: props when name: props for vars "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>consider (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>obtain (name) clause "proof"\<close> \\
+    \<open>clause\<close> & \<open>=\<close> & \<^theory_text>\<open>vars where name: props if props for vars\<close> \\
+  \end{tabular}
+  \end{center}
+  \caption{Main grammar of the Isar proof language}\label{fig:isar-syntax}
+  \end{figure}
+
+  The construction of the Isar proof language proceeds in a bottom-up fashion,
+  as an exercise in purity and minimalism. The grammar in
+  \appref{ap:main-grammar} describes the primitive parts of the core language
   (category \<open>proof\<close>), which is embedded into the main outer theory syntax via
   elements that require a proof (e.g.\ \<^theory_text>\<open>theorem\<close>, \<^theory_text>\<open>lemma\<close>, \<^theory_text>\<open>function\<close>,
   \<^theory_text>\<open>termination\<close>).