139 \item [$trans$] declares theorems as transitivity rules. |
148 \item [$trans$] declares theorems as transitivity rules. |
140 |
149 |
141 \end{descr} |
150 \end{descr} |
142 |
151 |
143 |
152 |
144 \section{Named local contexts (cases)}\label{sec:cases} |
153 \subsection{Generalized elimination}\label{sec:obtain} |
145 |
|
146 \indexisarcmd{case}\indexisarcmd{print-cases} |
|
147 \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} |
|
148 \begin{matharray}{rcl} |
|
149 \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
150 \isarcmd{print_cases}^* & : & \isarkeep{proof} \\ |
|
151 case_names & : & \isaratt \\ |
|
152 params & : & \isaratt \\ |
|
153 consumes & : & \isaratt \\ |
|
154 \end{matharray} |
|
155 |
|
156 Basically, Isar proof contexts are built up explicitly using commands like |
|
157 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical |
|
158 verification tasks this can become hard to manage, though. In particular, a |
|
159 large number of local contexts may emerge from case analysis or induction over |
|
160 inductive sets and types. |
|
161 |
|
162 \medskip |
|
163 |
|
164 The $\CASENAME$ command provides a shorthand to refer to certain parts of |
|
165 logical context symbolically. Proof methods may provide an environment of |
|
166 named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of |
|
167 $\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
168 |
|
169 It is important to note that $\CASENAME$ does \emph{not} provide any means to |
|
170 peek at the current goal state, which is treated as strictly non-observable in |
|
171 Isar! Instead, the cases considered here usually emerge in a canonical way |
|
172 from certain pieces of specification that appear in the theory somewhere else |
|
173 (e.g.\ in an inductive definition, or recursive function). See also |
|
174 \S\ref{sec:induct-method} for more details of how this works in HOL. |
|
175 |
|
176 \medskip |
|
177 |
|
178 Named cases may be exhibited in the current proof context only if both the |
|
179 proof method and the rules involved support this. Case names and parameters |
|
180 of basic rules may be declared by hand as well, by using appropriate |
|
181 attributes. Thus variant versions of rules that have been derived manually |
|
182 may be used in advanced case analysis later. |
|
183 |
|
184 \railalias{casenames}{case\_names} |
|
185 \railterm{casenames} |
|
186 |
|
187 \begin{rail} |
|
188 'case' nameref attributes? |
|
189 ; |
|
190 casenames (name + ) |
|
191 ; |
|
192 'params' ((name * ) + 'and') |
|
193 ; |
|
194 'consumes' nat? |
|
195 ; |
|
196 \end{rail} |
|
197 %FIXME bug in rail |
|
198 |
|
199 \begin{descr} |
|
200 \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, |
|
201 as provided by an appropriate proof method (such as $cases$ and $induct$ in |
|
202 Isabelle/HOL, see \S\ref{sec:induct-method}). The command $\CASE{c}$ |
|
203 abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
204 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current |
|
205 state, using Isar proof language notation. This is a diagnostic command; |
|
206 $undo$ does not apply. |
|
207 \item [$case_names~\vec c$] declares names for the local contexts of premises |
|
208 of some theorem; $\vec c$ refers to the \emph{suffix} of the list of |
|
209 premises. |
|
210 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
|
211 premises $1, \dots, n$ of some theorem. An empty list of names may be given |
|
212 to skip positions, leaving the present parameters unchanged. |
|
213 |
|
214 Note that the default usage of case rules does \emph{not} directly expose |
|
215 parameters to the proof context (see also \S\ref{sec:induct-method-proper}). |
|
216 \item [$consumes~n$] declares the number of ``major premises'' of a rule, |
|
217 i.e.\ the number of facts to be consumed when it is applied by an |
|
218 appropriate proof method (cf.\ \S\ref{sec:induct-method}). The default |
|
219 value of $consumes$ is $n = 1$, which is appropriate for the usual kind of |
|
220 cases and induction rules for inductive sets (cf.\ \S\ref{sec:inductive}). |
|
221 Rules without any $consumes$ declaration given are treated as if |
|
222 $consumes~0$ had been specified. |
|
223 |
|
224 Note that explicit $consumes$ declarations are only rarely needed; this is |
|
225 already taken care of automatically by the higher-level $cases$ and $induct$ |
|
226 declarations, see also \S\ref{sec:induct-att}. |
|
227 \end{descr} |
|
228 |
|
229 |
|
230 \section{Generalized existence}\label{sec:obtain} |
|
231 |
154 |
232 \indexisarcmd{obtain} |
155 \indexisarcmd{obtain} |
233 \begin{matharray}{rcl} |
156 \begin{matharray}{rcl} |
234 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
157 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
235 \end{matharray} |
158 \end{matharray} |
236 |
159 |
237 Generalized existence means that additional elements with certain properties |
160 Generalized elimination means that additional elements with certain properties |
238 may introduced in the current context. Technically, the $\OBTAINNAME$ |
161 may introduced in the current context, by virtue of a locally proven |
239 language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see |
162 ``soundness statement''. Technically speaking, the $\OBTAINNAME$ language |
240 also see \S\ref{sec:proof-context}), together with a soundness proof of its |
163 element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see |
241 additional claim. According to the nature of existential reasoning, |
164 \S\ref{sec:proof-context}), together with a soundness proof of its additional |
242 assumptions get eliminated from any result exported from the context later, |
165 claim. According to the nature of existential reasoning, assumptions get |
243 provided that the corresponding parameters do \emph{not} occur in the |
166 eliminated from any result exported from the context later, provided that the |
244 conclusion. |
167 corresponding parameters do \emph{not} occur in the conclusion. |
245 |
168 |
246 \begin{rail} |
169 \begin{rail} |
247 'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and') |
170 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and') |
248 ; |
171 ; |
249 \end{rail} |
172 \end{rail} |
250 |
173 |
251 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ |
174 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ |
252 shall refer to (optional) facts indicated for forward chaining. |
175 shall refer to (optional) facts indicated for forward chaining. |
848 is declared, else the rule itself is declared as an introduction rule. |
774 is declared, else the rule itself is declared as an introduction rule. |
849 |
775 |
850 The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, |
776 The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, |
851 and omits the Simplifier declaration. Thus the declaration does not have |
777 and omits the Simplifier declaration. Thus the declaration does not have |
852 any effect on automated proof tools, but only on simple methods such as |
778 any effect on automated proof tools, but only on simple methods such as |
853 $rule$ (see \S\ref{sec:misc-methods}). |
779 $rule$ (see \S\ref{sec:misc-meth-att}). |
854 \end{descr} |
780 \end{descr} |
855 |
781 |
856 |
782 |
857 \section{Proof by cases and induction}\label{sec:induct-method} |
783 \section{Proof by cases and induction}\label{sec:cases-induct} |
858 |
784 |
859 \subsection{Proof methods}\label{sec:induct-method-proper} |
785 \subsection{Rule contexts}\label{sec:rule-cases} |
|
786 |
|
787 \indexisarcmd{case}\indexisarcmd{print-cases} |
|
788 \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} |
|
789 \begin{matharray}{rcl} |
|
790 \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
791 \isarcmd{print_cases}^* & : & \isarkeep{proof} \\ |
|
792 case_names & : & \isaratt \\ |
|
793 params & : & \isaratt \\ |
|
794 consumes & : & \isaratt \\ |
|
795 \end{matharray} |
|
796 |
|
797 Basically, Isar proof contexts are built up explicitly using commands like |
|
798 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical |
|
799 verification tasks this can become hard to manage, though. In particular, a |
|
800 large number of local contexts may emerge from case analysis or induction over |
|
801 inductive sets and types. |
|
802 |
|
803 \medskip |
|
804 |
|
805 The $\CASENAME$ command provides a shorthand to refer to certain parts of |
|
806 logical context symbolically. Proof methods may provide an environment of |
|
807 named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of |
|
808 $\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
809 |
|
810 FIXME |
|
811 |
|
812 It is important to note that $\CASENAME$ does \emph{not} provide any means to |
|
813 peek at the current goal state, which is treated as strictly non-observable in |
|
814 Isar! Instead, the cases considered here usually emerge in a canonical way |
|
815 from certain pieces of specification that appear in the theory somewhere else |
|
816 (e.g.\ in an inductive definition, or recursive function). |
|
817 |
|
818 FIXME |
|
819 |
|
820 \medskip |
|
821 |
|
822 Named cases may be exhibited in the current proof context only if both the |
|
823 proof method and the rules involved support this. Case names and parameters |
|
824 of basic rules may be declared by hand as well, by using appropriate |
|
825 attributes. Thus variant versions of rules that have been derived manually |
|
826 may be used in advanced case analysis later. |
|
827 |
|
828 \railalias{casenames}{case\_names} |
|
829 \railterm{casenames} |
|
830 |
|
831 \begin{rail} |
|
832 'case' nameref attributes? |
|
833 ; |
|
834 casenames (name + ) |
|
835 ; |
|
836 'params' ((name * ) + 'and') |
|
837 ; |
|
838 'consumes' nat? |
|
839 ; |
|
840 \end{rail} |
|
841 %FIXME bug in rail |
|
842 |
|
843 \begin{descr} |
|
844 \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, |
|
845 as provided by an appropriate proof method (such as $cases$ and $induct$, |
|
846 see \S\ref{sec:cases-induct-meth}). The command $\CASE{c}$ abbreviates |
|
847 $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
848 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current |
|
849 state, using Isar proof language notation. This is a diagnostic command; |
|
850 $undo$ does not apply. |
|
851 \item [$case_names~\vec c$] declares names for the local contexts of premises |
|
852 of some theorem; $\vec c$ refers to the \emph{suffix} of the list of |
|
853 premises. |
|
854 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
|
855 premises $1, \dots, n$ of some theorem. An empty list of names may be given |
|
856 to skip positions, leaving the present parameters unchanged. |
|
857 |
|
858 Note that the default usage of case rules does \emph{not} directly expose |
|
859 parameters to the proof context (see also \S\ref{sec:cases-induct-meth}). |
|
860 \item [$consumes~n$] declares the number of ``major premises'' of a rule, |
|
861 i.e.\ the number of facts to be consumed when it is applied by an |
|
862 appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default |
|
863 value of $consumes$ is $n = 1$, which is appropriate for the usual kind of |
|
864 cases and induction rules for inductive sets (cf.\ |
|
865 \S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given |
|
866 are treated as if $consumes~0$ had been specified. |
|
867 |
|
868 Note that explicit $consumes$ declarations are only rarely needed; this is |
|
869 already taken care of automatically by the higher-level $cases$ and $induct$ |
|
870 declarations, see also \S\ref{sec:cases-induct-att}. |
|
871 \end{descr} |
|
872 |
|
873 |
|
874 \subsection{Proof methods}\label{sec:cases-induct-meth} |
860 |
875 |
861 \indexisarmeth{cases}\indexisarmeth{induct} |
876 \indexisarmeth{cases}\indexisarmeth{induct} |
862 \begin{matharray}{rcl} |
877 \begin{matharray}{rcl} |
863 cases & : & \isarmeth \\ |
878 cases & : & \isarmeth \\ |
864 induct & : & \isarmeth \\ |
879 induct & : & \isarmeth \\ |
867 The $cases$ and $induct$ methods provide a uniform interface to case analysis |
882 The $cases$ and $induct$ methods provide a uniform interface to case analysis |
868 and induction over datatypes, inductive sets, and recursive functions. The |
883 and induction over datatypes, inductive sets, and recursive functions. The |
869 corresponding rules may be specified and instantiated in a casual manner. |
884 corresponding rules may be specified and instantiated in a casual manner. |
870 Furthermore, these methods provide named local contexts that may be invoked |
885 Furthermore, these methods provide named local contexts that may be invoked |
871 via the $\CASENAME$ proof command within the subsequent proof text (cf.\ |
886 via the $\CASENAME$ proof command within the subsequent proof text (cf.\ |
872 \S\ref{sec:cases}). This accommodates compact proof texts even when reasoning |
887 \S\ref{sec:rule-cases}). This accommodates compact proof texts even when |
873 about large specifications. |
888 reasoning about large specifications. |
874 |
889 |
875 Note that the full spectrum of this generic functionality is currently only |
890 Note that the full spectrum of this generic functionality is currently only |
876 supported by Isabelle/HOL, when used in conjunction with advanced definitional |
891 supported by Isabelle/HOL, when used in conjunction with advanced definitional |
877 packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}). |
892 packages (see especially \S\ref{sec:hol-datatype} and |
|
893 \S\ref{sec:hol-inductive}). |
878 |
894 |
879 \begin{rail} |
895 \begin{rail} |
880 'cases' spec |
896 'cases' spec |
881 ; |
897 ; |
882 'induct' spec |
898 'induct' spec |
918 Additional parameters may be specified as $ps$; these are applied after the |
934 Additional parameters may be specified as $ps$; these are applied after the |
919 primary instantiation in the same manner as by the $of$ attribute (cf.\ |
935 primary instantiation in the same manner as by the $of$ attribute (cf.\ |
920 \S\ref{sec:pure-meth-att}). This feature is rarely needed in practice; a |
936 \S\ref{sec:pure-meth-att}). This feature is rarely needed in practice; a |
921 typical application would be to specify additional arguments for rules |
937 typical application would be to specify additional arguments for rules |
922 stemming from parameterized inductive definitions (see also |
938 stemming from parameterized inductive definitions (see also |
923 \S\ref{sec:inductive}). |
939 \S\ref{sec:hol-inductive}). |
924 |
940 |
925 The $open$ option causes the parameters of the new local contexts to be |
941 The $open$ option causes the parameters of the new local contexts to be |
926 exposed to the current proof context. Thus local variables stemming from |
942 exposed to the current proof context. Thus local variables stemming from |
927 distant parts of the theory development may be introduced in an implicit |
943 distant parts of the theory development may be introduced in an implicit |
928 manner, which can be quite confusing to the reader. Furthermore, this |
944 manner, which can be quite confusing to the reader. Furthermore, this |
947 |
963 |
948 Additional parameters (including the $open$ option) may be given in the same |
964 Additional parameters (including the $open$ option) may be given in the same |
949 way as for $cases$, see above. |
965 way as for $cases$, see above. |
950 \end{descr} |
966 \end{descr} |
951 |
967 |
952 Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as |
968 Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as |
953 determined by the instantiated rule \emph{before} it has been applied to the |
969 determined by the instantiated rule \emph{before} it has been applied to the |
954 internal proof state.\footnote{As a general principle, Isar proof text may |
970 internal proof state.\footnote{As a general principle, Isar proof text may |
955 never refer to parts of proof states directly.} Thus proper use of symbolic |
971 never refer to parts of proof states directly.} Thus proper use of symbolic |
956 cases usually require the rule to be instantiated fully, as far as the |
972 cases usually require the rule to be instantiated fully, as far as the |
957 emerging local contexts and subgoals are concerned. In particular, for |
973 emerging local contexts and subgoals are concerned. In particular, for |
982 x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. |
998 x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. |
983 |
999 |
984 \medskip |
1000 \medskip |
985 |
1001 |
986 Facts presented to either method are consumed according to the number of |
1002 Facts presented to either method are consumed according to the number of |
987 ``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and |
1003 ``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}), |
988 \S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules |
1004 which is usually $0$ for plain cases and induction rules of datatypes etc.\ |
989 of datatypes etc.\ and $1$ for rules of inductive sets and the like. The |
1005 and $1$ for rules of inductive sets and the like. The remaining facts are |
990 remaining facts are inserted into the goal verbatim before the actual $cases$ |
1006 inserted into the goal verbatim before the actual $cases$ or $induct$ rule is |
991 or $induct$ rule is applied (thus facts may be even passed through an |
1007 applied (thus facts may be even passed through an induction). |
992 induction). |
|
993 |
1008 |
994 Note that whenever facts are present, the default rule selection scheme would |
1009 Note that whenever facts are present, the default rule selection scheme would |
995 provide a ``set'' rule only, with the first fact consumed and the rest |
1010 provide a ``set'' rule only, with the first fact consumed and the rest |
996 inserted into the goal. In order to pass all facts into a ``type'' rule |
1011 inserted into the goal. In order to pass all facts into a ``type'' rule |
997 instead, one would have to specify this explicitly, e.g.\ by appending |
1012 instead, one would have to specify this explicitly, e.g.\ by appending |
998 ``$type: name$'' to the method argument. |
1013 ``$type: name$'' to the method argument. |
999 |
1014 |
1000 |
1015 |
1001 \subsection{Declaring rules}\label{sec:induct-att} |
1016 \subsection{Declaring rules}\label{sec:cases-induct-att} |
1002 |
1017 |
1003 \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct} |
1018 \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct} |
1004 \begin{matharray}{rcl} |
1019 \begin{matharray}{rcl} |
1005 \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\ |
1020 \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\ |
1006 cases & : & \isaratt \\ |
1021 cases & : & \isaratt \\ |
1020 The $cases$ and $induct$ attributes augment the corresponding context of rules |
1035 The $cases$ and $induct$ attributes augment the corresponding context of rules |
1021 for reasoning about inductive sets and types. The standard rules are already |
1036 for reasoning about inductive sets and types. The standard rules are already |
1022 declared by advanced definitional packages. For special applications, these |
1037 declared by advanced definitional packages. For special applications, these |
1023 may be replaced manually by variant versions. |
1038 may be replaced manually by variant versions. |
1024 |
1039 |
1025 Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to |
1040 Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:rule-cases}) to |
1026 adjust names of cases and parameters of a rule. |
1041 adjust names of cases and parameters of a rule. |
1027 |
1042 |
1028 The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of |
1043 The $consumes$ declaration (cf.\ \S\ref{sec:rule-cases}) is taken care of |
1029 automatically (if none had been given already): $consumes~0$ is specified for |
1044 automatically (if none had been given already): $consumes~0$ is specified for |
1030 ``type'' rules and $consumes~1$ for ``set'' rules. |
1045 ``type'' rules and $consumes~1$ for ``set'' rules. |
|
1046 |
|
1047 |
|
1048 \section{Object-logic setup}\label{sec:object-logic} |
|
1049 |
|
1050 The very starting point for any Isabelle object-logic is a ``truth judgment'' |
|
1051 that links object-level statements to the meta-logic (with its minimal |
|
1052 language of $prop$ that covers universal quantification $\Forall$ and |
|
1053 implication $\Imp$). Common object-logics are sufficiently expressive to |
|
1054 \emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own |
|
1055 language. This is useful in certain situations where a rule needs to be |
|
1056 viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x |
|
1057 \in A \Imp P(x)$ versus $\forall x \in A. P(x)$). |
|
1058 |
|
1059 From the following language elements, only the $atomize$ method and |
|
1060 $rule_format$ attribute are occasionally required by end-users, the rest is |
|
1061 mainly for those who need to setup their own object-logic. In the latter case |
|
1062 existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as |
|
1063 realistic examples. |
|
1064 |
|
1065 Further generic tools may refer to the information provided by object-logic |
|
1066 declarations internally (such as locales \S\ref{sec:locale}, or the Classical |
|
1067 Reasoner \S\ref{sec:classical}). |
|
1068 |
|
1069 \indexisarcmd{judgment} |
|
1070 \indexisarmeth{atomize}\indexisaratt{atomize} |
|
1071 \indexisaratt{rule-format}\indexisaratt{rulify} |
|
1072 |
|
1073 \begin{matharray}{rcl} |
|
1074 \isarcmd{judgment} & : & \isartrans{theory}{theory} \\ |
|
1075 atomize & : & \isarmeth \\ |
|
1076 atomize & : & \isaratt \\ |
|
1077 rule_format & : & \isaratt \\ |
|
1078 rulify & : & \isaratt \\ |
|
1079 \end{matharray} |
|
1080 |
|
1081 \railalias{ruleformat}{rule\_format} |
|
1082 \railterm{ruleformat} |
|
1083 |
|
1084 \begin{rail} |
|
1085 'judgment' constdecl |
|
1086 ; |
|
1087 ruleformat ('(' noasm ')')? |
|
1088 ; |
|
1089 \end{rail} |
|
1090 |
|
1091 \begin{descr} |
|
1092 |
|
1093 \item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the |
|
1094 truth judgment of the current object-logic. Its type $\sigma$ should |
|
1095 specify a coercion of the category of object-level propositions to $prop$ of |
|
1096 the Pure meta-logic; the mixfix annotation $syn$ would typically just link |
|
1097 the object language (internally of syntactic category $logic$) with that of |
|
1098 $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any |
|
1099 theory development. |
|
1100 |
|
1101 \item [$atomize$] (as a method) rewrites any non-atomic premises of a |
|
1102 sub-goal, using the meta-level equations that have been declared via |
|
1103 $atomize$ (as an attribute) beforehand. As a result, heavily nested goals |
|
1104 become amenable to fundamental operations such as resolution (cf.\ the |
|
1105 $rule$ method) and proof-by-assumption (cf.\ $assumption$). |
|
1106 |
|
1107 A typical collection of $atomize$ rules for a particular object-logic would |
|
1108 provide an internalization for each of the connectives of $\Forall$, $\Imp$, |
|
1109 $\equiv$; meta-level conjunction expressed as $\All{\PROP\,C} (A \Imp B \Imp |
|
1110 \PROP\,C) \Imp PROP\,C$ should be covered as well. |
|
1111 |
|
1112 \item [$rule_format$] rewrites a theorem by the equalities declared as |
|
1113 $rulify$ rules in the current object-logic. By default, the result is fully |
|
1114 normalized, including assumptions and conclusions at any depth. The |
|
1115 $no_asm$ option restricts the transformation to the conclusion of a rule. |
|
1116 |
|
1117 In common object logics (HOL, FOL, ZF), the effect of $rule_format$ is to |
|
1118 replace (bounded) universal quantification ($\forall$) and implication |
|
1119 ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$. |
|
1120 |
|
1121 \end{descr} |
1031 |
1122 |
1032 |
1123 |
1033 %%% Local Variables: |
1124 %%% Local Variables: |
1034 %%% mode: latex |
1125 %%% mode: latex |
1035 %%% TeX-master: "isar-ref" |
1126 %%% TeX-master: "isar-ref" |