12 $\HAVE{a}{\phi}$ & prove local result \\ |
12 $\HAVE{a}{\phi}$ & prove local result \\ |
13 $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\ |
13 $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\ |
14 $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\ |
14 $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\ |
15 $\BG~\dots~\EN$ & declare explicit blocks \\ |
15 $\BG~\dots~\EN$ & declare explicit blocks \\ |
16 $\isarcmd{next}$ & switch implicit blocks \\ |
16 $\isarcmd{next}$ & switch implicit blocks \\ |
17 $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\ |
17 $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\ |
18 $\LET{p = t}$ & \text{abbreviate terms by matching} \\ |
18 $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\ |
19 \end{tabular} |
19 \end{tabular} |
20 |
20 |
21 \begin{matharray}{rcl} |
21 \begin{matharray}{rcl} |
22 theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\ |
22 theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\ |
23 & \Or & \LEMMA{name}{form}~proof \\ |
23 & \Or & \LEMMA{name}{prop}~proof \\ |
24 & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex] |
24 & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex] |
25 proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex] |
25 proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex] |
26 stmt & = & \BG~stmt^*~\EN \\ |
26 stmt & = & \BG~stmt^*~\EN \\ |
27 & \Or & \isarcmd{next} \\ |
27 & \Or & \isarcmd{next} \\ |
28 & \Or & \NOTE{name}{name^+} \\ |
28 & \Or & \NOTE{name}{name^+} \\ |
29 & \Or & \LET{term = term} \\[0.5ex] |
29 & \Or & \LET{term = term} \\[0.5ex] |
30 & \Or & \FIX{var^+} \\ |
30 & \Or & \FIX{var^+} \\ |
31 & \Or & \ASSUME{name}{form^+}\\ |
31 & \Or & \ASSUME{name}{prop^+}\\ |
32 & \Or & \THEN~goal{\dsh}stmt \\ |
32 & \Or & \THEN~goal{\dsh}stmt \\ |
33 & \Or & goal{\dsh}stmt \\ |
33 & \Or & goal{\dsh}stmt \\ |
34 goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\ |
34 goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\ |
35 & \Or & \SHOW{name}{form}~proof \\ |
35 & \Or & \SHOW{name}{prop}~proof \\ |
36 \end{matharray} |
36 \end{matharray} |
37 |
37 |
38 |
38 |
39 \subsection{Abbreviations and synonyms} |
39 \subsection{Abbreviations and synonyms} |
40 |
40 |
42 \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\ |
42 \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\ |
43 \DDOT & \equiv & \BY{rule} \\ |
43 \DDOT & \equiv & \BY{rule} \\ |
44 \DOT & \equiv & \BY{assumption} \\ |
44 \DOT & \equiv & \BY{assumption} \\ |
45 \HENCENAME & \equiv & \THEN~\HAVENAME \\ |
45 \HENCENAME & \equiv & \THEN~\HAVENAME \\ |
46 \THUSNAME & \equiv & \THEN~\SHOWNAME \\ |
46 \THUSNAME & \equiv & \THEN~\SHOWNAME \\ |
47 \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\ |
47 \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\ |
48 \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex] |
48 \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex] |
49 \FROM{this} & \equiv & \THEN \\ |
49 \FROM{this} & \equiv & \THEN \\ |
50 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\ |
50 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\ |
51 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\ |
51 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\ |
52 \end{matharray} |
52 \end{matharray} |
53 |
53 |
65 |
65 |
66 |
66 |
67 \subsection{Diagnostic commands} |
67 \subsection{Diagnostic commands} |
68 |
68 |
69 \begin{matharray}{ll} |
69 \begin{matharray}{ll} |
70 \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\ |
70 \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\ |
71 \isarcmd{term}~t & \text{print term} \\ |
71 \isarcmd{term}~t & \text{print term} \\ |
72 \isarcmd{prop}~\phi & \text{print meta-level proposition} \\ |
72 \isarcmd{prop}~\phi & \text{print meta-level proposition} \\ |
73 \isarcmd{typ}~\tau & \text{print meta-level type} \\ |
73 \isarcmd{typ}~\tau & \text{print meta-level type} \\ |
74 \end{matharray} |
74 \end{matharray} |
75 |
75 |
76 |
76 |
77 \section{Proof methods} |
77 \section{Proof methods} |
78 |
78 |
79 \begin{tabular}{ll} |
79 \begin{tabular}{ll} |
80 \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex] |
80 \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex] |
81 $assumption$ & apply assumption \\ |
81 $assumption$ & apply some assumption \\ |
82 $rule~a@1~\dots~a@n$ & apply some rule \\ |
82 $rule~a@1\;\dots\;a@n$ & apply some rule \\ |
83 $rule$ & apply standard rule (default for $\PROOFNAME$) \\ |
83 $rule$ & apply standard rule (default for $\PROOFNAME$) \\ |
84 $induct~x$ & apply induction rule \\ |
84 $induct~x$ & apply induction rule \\ |
85 $contradiction$ & apply $\neg{}$ elimination rule \\[2ex] |
85 $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex] |
86 |
86 |
87 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex] |
87 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex] |
88 $-$ & \text{no rules} \\ |
88 $-$ & \text{no rules} \\ |
89 $intro~a@1~\dots~a@n$ & \text{introduction rules} \\ |
89 $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\ |
90 $elim~a@1~\dots~a@n$ & \text{elimination rules} \\ |
90 $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\ |
91 $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex] |
91 $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex] |
92 |
92 |
93 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] |
93 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] |
94 $simp$ & Simplifier \\ |
94 $simp$ & Simplifier \\ |
95 $blast$, $fast$ & Classical reasoner \\ |
95 $blast$, $fast$ & Classical Reasoner \\ |
96 $force$, $auto$ & Simplifier + Classical reasoner \\ |
96 $force$, $auto$ & Simplifier + Classical Reasoner \\ |
97 $arith$ & Arithmetic procedure \\ |
97 $arith$ & Arithmetic procedure \\ |
98 \end{tabular} |
98 \end{tabular} |
99 |
99 |
100 |
100 |
101 \section{Attributes} |
101 \section{Attributes} |
102 |
102 |
103 \begin{tabular}{ll} |
103 \begin{tabular}{ll} |
104 \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex] |
104 \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex] |
105 $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\ |
105 $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\ |
106 $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\ |
106 $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\ |
107 $RS~b$ & resolve fact with rule \\ |
107 $RS~b$ & resolve fact with rule \\ |
108 $standard$ & put into standard result form \\ |
108 $standard$ & put into standard result form \\ |
109 $rulify$ & put into object-rule form \\ |
109 $rulify$ & put into object-rule form \\ |
110 $elimify$ & put destruction rule into elimination form \\[1ex] |
110 $elimify$ & put destruction rule into elimination form \\[1ex] |
111 |
111 |
112 \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex] |
112 \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex] |
113 $simp$ & declare Simplifier rules \\ |
113 $simp$ & declare Simplifier rules \\ |
114 $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\ |
114 $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\ |
115 $iff$ & declare Simplifier + Classical reasoner rules \\ |
115 $iff$ & declare Simplifier + Classical Reasoner rules \\ |
116 $trans$ & calculational rules (general transitivity) \\ |
116 $trans$ & declare calculational rules (general transitivity) \\ |
117 \end{tabular} |
117 \end{tabular} |
118 |
|
119 |
118 |
120 %%% Local Variables: |
119 %%% Local Variables: |
121 %%% mode: latex |
120 %%% mode: latex |
122 %%% TeX-master: "isar-ref" |
121 %%% TeX-master: "isar-ref" |
123 %%% End: |
122 %%% End: |