11 subsection \<open>Main grammar \label{ap:main-grammar}\<close> |
11 subsection \<open>Main grammar \label{ap:main-grammar}\<close> |
12 |
12 |
13 text \<open> |
13 text \<open> |
14 \begin{tabular}{rcl} |
14 \begin{tabular}{rcl} |
15 \<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\ |
15 \<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\ |
16 & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if props for vars "proof"\<close> \\ |
16 & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if name: props for vars "proof"\<close> \\ |
17 & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\ |
17 & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\ |
18 & & \quad\<^theory_text>\<open>fixes vars\<close> \\ |
18 & & \quad\<^theory_text>\<open>fixes vars\<close> \\ |
19 & & \quad\<^theory_text>\<open>assumes name: props\<close> \\ |
19 & & \quad\<^theory_text>\<open>assumes name: props\<close> \\ |
20 & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\ |
20 & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\ |
21 & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\ |
21 & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\ |
23 & & \quad\<^theory_text>\<open>assumes name: props\<close> \\ |
23 & & \quad\<^theory_text>\<open>assumes name: props\<close> \\ |
24 & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\ |
24 & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\ |
25 \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\ |
25 \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\ |
26 & \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\ |
26 & \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\ |
27 \<open>refinement\<close> & = & \<^theory_text>\<open>apply method\<close> \\ |
27 \<open>refinement\<close> & = & \<^theory_text>\<open>apply method\<close> \\ |
28 & \<open>|\<close> & \<^theory_text>\<open>supply facts\<close> \\ |
28 & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\ |
29 & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\ |
29 & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\ |
30 & \<open>|\<close> & \<^theory_text>\<open>using facts\<close> \\ |
30 & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\ |
31 & \<open>|\<close> & \<^theory_text>\<open>unfolding facts\<close> \\ |
31 & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\ |
32 \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\ |
32 \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\ |
33 & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\ |
33 & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\ |
34 & \<open>|\<close> & \<^theory_text>\<open>note name = facts\<close> \\ |
34 & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\ |
35 & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\ |
35 & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\ |
36 & \<open>|\<close> & \<^theory_text>\<open>write name (mixfix)\<close> \\ |
36 & \<open>|\<close> & \<^theory_text>\<open>write name (mixfix)\<close> \\ |
37 & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\ |
37 & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\ |
38 & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\ |
38 & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\ |
39 & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\ |
39 & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\ |