601   Dyckhoff for this exercise.} 

   601   Dyckhoff for suggesting this exercise and working out the details.} 

   828   to the section about local-setup is given eralier.}

   828   to the section about local-setup is given earlier.}

   836   The first argument @{ML_ind theoremK in Thm} is a kind indicator, which

   836   The fourth argument of @{ML note in LocalTheory} is the list of theorems we

   837   classifies the theorem. There are several such kind indicators: for a

   837   want to store under a name.  The first argument @{ML_ind theoremK in Thm} is

   838   theorem arising from a definition we should use @{ML_ind definitionK in

   838   a kind indicator, which classifies the theorem. There are several such kind

   839   Thm}, for an axiom @{ML_ind axiomK in Thm}, and for ``normal'' theorems the

   839   indicators: for a theorem arising from a definition you should use @{ML_ind

   840   kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK in Thm}.  The second

   840   definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, and for

   841   argument of @{ML note in LocalTheory} is the name under which we store the

   841   ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK

   842   theorem or theorems. The third argument can contain a list of theorem

   842   in Thm}.  The second argument of @{ML note in LocalTheory} is the name under

   843   attributes, which we will explain in detail in Section~\ref{sec:attributes}. 

   843   which we store the theorem or theorems. The third argument can contain a

   844   Below we just use one such attribute in order add

   844   list of theorem attributes, which we will explain in detail in

   845   the theorem to the simpset:

   845   Section~\ref{sec:attributes}. Below we just use one such attribute in order

   846   add the theorem to the simpset:

   855   since Isabelle does not allow us to store two theorems under the same

   856   since Isabelle does not allow us to call  @{ML_ind note in LocalTheory} twice

   856   name. The attribute needs to be wrapped inside the function @{ML_ind

   857   with the same name. The attribute needs to be wrapped inside the function @{ML_ind

   857   internal in Attrib}. If we use the function @{ML get_thm_names_from_ss} from

   858   internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function 

   859   @{ML get_thm_names_from_ss} from

   957   The simplifier can be used to unfold definition in theorms. To show

   959   The simplifier can be used to unfold definition in theorems. To show

   969   logic, that is eplacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} with @{text "\<Longrightarrow>"} 

   971   logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"} 

   970   and @{text "\<And>"}, respectively.  A reason for such transformations is 

   972   and @{text "\<And>"}, or the other way around.  A reason for such a transformation 

   971   that definitions can only be stated using object logic connectives, while 

   973   might be stating a definition. The reason is that definitions can only be 

   972   theorems using the connectives from the meta logic are more convenient for 

   974   stated using object logic connectives, while theorems using the connectives 

   973   reasoning. The function  @{ML_ind rulify in ObjectLogic} replaces all 

   975   from the meta logic are more convenient for reasoning. Therefore there are

   974   object connectives by equivalents in the meta logic. For example

   976   some build in functions which help with these transformations. The function 

   977   @{ML_ind rulify in ObjectLogic} 

   978   replaces all object connectives by equivalents in the meta logic. For example

   996   such as @{thm [source] list.induct}, which is of the form 

  1000   involving meta variables, such as @{thm [source] list.induct}, which 

  1001   is of the form 

  1001   @{text "?list"} in the theorem. For this we can use the function 

  1006   @{text "?list"}. For this we can use the function 

  1022   One way to achive this is by using the function @{ML_ind prove in Goal}

  1027   One way to achieve this is by using the function @{ML_ind prove in Goal}

  1023   in the structure @{ML_struct Goal}. For example below we prove the term 

  1028   in the structure @{ML_struct Goal}. For example below we use this function

  1024   @{term "P \<Longrightarrow> P"}.

  1029   to prove the term @{term "P \<Longrightarrow> P"}.

  1038   corresponding proof given in form of a tactic. We explain tactics in

  1043   corresponding proof given in form of a tactic (we explain tactics in

  1039   Chapter~\ref{chp:tactical}. In the code above, the tactic proves the theorem

  1044   Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem

  1040   by assumption.

  1045   by assumption. As before this code will produce a theorem, but the theorem

  1046   is not yet stored in the theorem database. 

  1045   Thm}. Assume the following lemma.

  1051   Thm}. Assume you prove the following lemma.

  1046 *}

  1052 *}

  1047 

  1053 

  1048 lemma foo_data: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption

  1054 lemma foo_data: 

  1049 

  1055   shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption

  1050 text {*

  1056 

  1051   So far the the auxiliary data of this lemma is: 

  1057 text {*

  1058   The auxiliary data of this lemma can be retrieved using the function 

  1059   @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is 

  1057   When we store lemmas in the theorem database, we may want to explicitly extend 

  1065   consisting of a name and a kind.  When we store lemmas in the theorem database, 

  1058   this data by attaching case names to the two premises of the lemma.  This can

  1066   we might want to explicitly extend this data by attaching case names to the 

  1059   be achieved with the function @{ML_ind name in RuleCases}.

  1067   two premises of the lemma.  This can be done with the function @{ML_ind name in RuleCases}

  1068   from the structure @{ML_struct RuleCases}.

  1076   You can notice the case names on the user level when using the proof 

  1085   You can observe the case names of this lemma on the user level when using 

  1077   methods @{ML_text cases} and @{ML_text induct}. In the proof below

  1086   the proof methods @{ML_text cases} and @{ML_text induct}. In the proof below

  1096   we can proceed by analysing the cases @{text "foo_case1"} and 

  1105   we can proceed by analysing the cases @{text "foo_case_one"} and 

  1097   @{text "foo_case2"}. While if the theorem has no names, then

  1106   @{text "foo_case_two"}. While if the theorem has no names, then

  1120   proved theorems can be quoted in the text directly from the formalisation. 

  1129   proved theorems can be quoted in documents referencing directly their

  1121   This helps minimises cut-and-paste errors. However, sometimes the verbatim

  1130   formalisation. This helps tremendously to minimise cut-and-paste errors. However,

  1122   quoting is not what is wanted. For such situations Isabelle allows the

  1131   sometimes the verbatim quoting is not what is wanted or what can be shown to

  1123   installation of \emph{styles}. These are, roughly speaking, functions from 

  1132   readers. For such situations Isabelle allows the installation of \emph{theorem 

  1124   terms to terms. The input term stands for the theorem to be presented.

  1133   styles}. These are, roughly speaking, functions from terms to terms. The input 

  1125   Let us assume we want to display theorems without leading quantifiers. 

  1134   term stands for the theorem to be presented; the output can be constructed to

  1126   For this we can implement the following function that strips off 

  1135   ones wishes.  Let us, for example, assume we want to quote theorems without

  1127   meta-quantifiers.

  1136   leading @{text \<forall>}-quantifiers. For this we can implement the following function 

  1128 *}

  1137   that strips off meta-quantifiers.

  1129 

  1138 *}

  1130 ML {*fun strip_all (Const (@{const_name "All"}, _) $ Abs body) = 

  1139 

  1131       Term.dest_abs body |> snd |> strip_all

  1140 ML %linenosgray {*fun strip_all_qnt (Const (@{const_name "All"}, _) $ Abs body) = 

  1132   | strip_all (Const (@{const_name "Trueprop"}, _) $ t) = strip_all t

  1141       Term.dest_abs body |> snd |> strip_all_qnt

  1133   | strip_all t = t*}

  1142   | strip_all_qnt (Const (@{const_name "Trueprop"}, _) $ t) = 

  1134 

  1143       strip_all_qnt t

  1135 ML {* strip_all @{term "\<forall>x y z. P x y z"}*}

  1144   | strip_all_qnt t = t*}

  1136 

  1145 

  1137 text {*

  1146 text {*

  1138   Now we can install this function as the theorem style named 

  1147   We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions,

  1139   @{text "strip_all"}. 

  1148   since this function deals correctly with potential name clashes. This function produces

  1149   a pair consisting of the variable and the body of the abstraction. We are only interested

  1150   in the body, which we feed into the recursive call. In Line 3 and 4, we also

  1151   have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 

  1152   install this function as the theorem style named @{text "my_strip_all_qnt"}. 

  1143   Term_Style.setup "strip_all" (Scan.succeed (K strip_all)) 

  1156   Term_Style.setup "my_strip_all_qnt" (Scan.succeed (K strip_all_qnt)) 

  1144 *}

  1157 *}

  1145 

  1158 

  1146 text {*

  1159 text {*

  1147   We can test the theorem style with the following theorem

  1160   We can test this theorem style with the following theorem

  1154   Now printing out the theorem @{thm [source] style_test} normally

  1167   Now printing out in a document the theorem @{thm [source] style_test} normally

  1155   in a document produces

  1168   using @{text "@{thm \<dots>}"} produces

  1156 

  1169 

  1157   @{thm [display] style_test}

  1170   \begin{isabelle}

  1158 

  1171   @{text "@{thm style_test}"}\\

  1159   as expected. But with the theorem style @{text "@{thm (strip_all) \<dots>}"} 

  1172   @{text ">"}~@{thm style_test}

  1173   \end{isabelle}

  1174 

  1175   as expected. But with the theorem style @{text "@{thm (my_strip_all_qnt) \<dots>}"} 

  1162   @{thm [display] (strip_all) style_test}

  1178   \begin{isabelle}

  1163   

  1179   @{text "@{thm (my_strip_all_qnt) style_test}"}\\

  1164   without the leading quantifiers. Such theorem styles allow one to

  1180   @{text ">"}~@{thm (my_strip_all_qnt) style_test}\\

  1165   print out theorems in documents formatted in any way wanted. Next we 

  1181   \end{isabelle}

  1166   explain theorem attributes, which is another mechanism for treating

  1182   

  1167   theorems.

  1183   without the leading quantifiers. We can improve this theorem style by explicitly 

  1168 *}

  1184   giving a list of strings that should be used for the replacement of the

  1169 

  1185   variables. For this we implement the function which takes a list of strings

  1186   and uses them as name in the outermost abstractions.

  1187 *}

  1188 

  1189 ML {*fun rename_all [] t = t

  1190   | rename_all (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 

  1191       Const (@{const_name "All"}, U) $ Abs (x, T, rename_all xs t)

  1192   | rename_all xs (Const (@{const_name "Trueprop"}, U) $ t) =

  1193       rename_all xs t

  1194   | rename_all _ t = t*}

  1195 

  1196 text {*

  1197   We can now install a the modified theorem style as follows

  1198 *}

  1199 

  1200 setup %gray {*

  1201 let

  1202   val parser = Scan.repeat Args.name

  1203   fun action xs = K (rename_all xs #> strip_all_qnt)

  1204 in

  1205   Term_Style.setup "my_strip_all_qnt2" (parser >> action)

  1206 end *}

  1207 

  1208 text {*

  1209   We can now suggest, for example, two variables for stripping 

  1210   off the @{text \<forall>}-quantifiers, namely:

  1211 

  1212   \begin{isabelle}

  1213   @{text "@{thm (my_strip_all_qnt2 x' x'') style_test}"}\\

  1214   @{text ">"}~@{thm (my_strip_all_qnt2 x' x'') style_test}

  1215   \end{isabelle}

  1216 

  1217   Such theorem styles allow one to print out theorems in documents formatted to

  1218   ones heart content. Next we explain theorem attributes, which is another

  1219   mechanism for dealing with theorems.

  1220 

  1221   \begin{readmore}

  1222   Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}.

  1223   \end{readmore}

  1224 *}