319 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =

   319 ML{*fun strip_alls t =

   320                                     strip_alls t |>> cons (Free (n, T))

   320 let 

   321   | strip_alls t = ([], t) *}

   321   fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))

   322 in

   323   case t of

   324     Const ("All", _) $ Abs body => aux body

   325   | _ => ([], t)

   326 end*}

   346   Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls}

   351   Note that in Line 4 we had to reverse the list of variables that @{ML

   347   returned. The reason is that the head of the list the function @{ML subst_bounds}

   352   strip_alls} returned. The reason is that the head of the list the function

   348   takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}

   353   @{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next

   349   and so on. 

   354   element for @{ML "Bound 1"} and so on. 

   355 

   356   Notice also that this function might introduce name clashes, since we

   357   substitute just a variable with the name recorded in an abstraction. This

   358   name is by no means unique. If clashes need to be avoided, then we should

   359   use the function @{ML_ind dest_abs in Term}, which returns the body where

   360   the lose de Bruijn index is replaced by a unique free variable. For example

   361 

   362 

   363   @{ML_response_fake [display,gray]

   364   "let

   365   val app = Bound 0 $ Free (\"x\", @{typ nat})

   366 in

   367   Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, app)

   368 end"

   369   "(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}

   939   unfold the constant according to its definition (Line 2).

   959   unfold the constant @{term "True"} according to its definition (Line 2).

   949   logic.  For example, the function @{ML_ind rulify in ObjectLogic}

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

   950   replaces all @{text "\<longrightarrow>"} and @{text "\<forall>"} into the equivalents of the 

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

   951   meta logic. For example

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

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

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

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

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

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

   979   @{ML_ind forall_intr_vars in Drule}. 

  1002   @{ML_ind forall_intr_vars in Drule}. This allows us to implement the

  1003   following function for atomizing a theorem.

   991   For the theorem @{thm [source] list.induct}, this function produces:

  1015   This function produces for the theorem @{thm [source] list.induct}

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

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

   999   For example below we prove the term @{term "P \<Longrightarrow> P"}.

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

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

  1010   This function takes as second argument a list of strings. This list specifies

  1035   This function takes first a context and second a list of strings. This list

  1011   which variables should be turned into meta-variables once the term is proved.

  1036   specifies which variables should be turned into meta-variables once the term

  1012   The proof is given in form of a tactic as last argument. We explain tactics in 

  1037   is proved.  The fourth argument is the term to be proved. The fifth is a

  1013   Chapter~\ref{chp:tactical}. In the code above the tactic proved the theorem 

  1038   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

  1016   Theorems also contain auxiliary data, such their names and kind, but also 

  1042   Theorems also contain auxiliary data, such as the name of the theorem, its

  1017   names for cases etc. This data is stored in a string-string list and can

  1043   kind, the names for cases and so on. This data is stored in a string-string

  1018   be retrieved with the function @{ML_ind get_tags in Thm}. Assume the

  1044   list and can be retrieved with the function @{ML_ind get_tags in

  1019   following lemma. 

  1045   Thm}. Assume the following lemma.

  1025   The auxiliary data of this lemma is as follows. 

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

  1031   When we store lemmas in the theorem database, we can explicitly extend the data 

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

  1032   associated with this lemma by attaching case names.  

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

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

  1038       [(RuleCases.name ["foo_case1", "foo_case2"] 

  1065       [(RuleCases.name ["foo_case_one", "foo_case_two"] 

  1047  (\"case_names\", \"foo_case1;foo_case2\")]"}

  1074  (\"case_names\", \"foo_case_one;foo_case_two\")]"}

  1048 

  1075 

  1049   You notice the difference when using the proof methods @{ML_text cases} 

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

  1050   or @{ML_text induct}. In the proof below

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

  1054   "Q \<Longrightarrow> Q \<Longrightarrow> Q"

  1081   shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"

  1056 print_cases

  1083 

  1058 

  1085 text_raw{*

  1059 text {*

  1086 \begin{tabular}{@ {}l}

  1060   we can proceed by analysing the cases @{ML_text "foo_case1"} and 

  1087 \isacommand{print\_cases}\\

  1061   @{ML_text "foo_case2"}. While if the theorem has no names, then

  1088 @{text "> cases:"}\\

  1062   the cases have standard names @{ML_text 1}, @{ML_text 2} and so 

  1089 @{text ">   foo_case_one:"}\\

  1090 @{text ">     let \"?case\" = \"?P\""}\\

  1091 @{text ">   foo_case_two:"}\\

  1092 @{text ">     let \"?case\" = \"?P\""}

  1093 \end{tabular}*}

  1094 

  1095 text {*

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

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

  1098   the cases have standard names @{text 1}, @{text 2} and so 

  1067   "Q \<Longrightarrow> Q \<Longrightarrow> Q"

  1103   shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"

  1069 print_cases

  1105 

  1071 

  1107 text_raw{*

  1072 text {*

  1108 \begin{tabular}{@ {}l}

  1073   TBD below

  1109 \isacommand{print\_cases}\\

  1074 

  1110 @{text "> cases:"}\\

  1075   One great feature of Isabelle is its document preparation system where

  1111 @{text ">   1:"}\\

  1112 @{text ">     let \"?case\" = \"?P\""}\\

  1113 @{text ">   2:"}\\

  1114 @{text ">     let \"?case\" = \"?P\""}

  1115 \end{tabular}*}

  1116 

  1117 

  1118 text {*

  1119   One great feature of Isabelle is its document preparation system, where

  1077 

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

  1078   (FIXME: example for how to add theorem styles)

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

  1079 *}

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

  1080 

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

  1081 ML {*

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

  1082 fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) =

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

  1083       strip_assums_all ((a, T)::params, t)

  1127   meta-quantifiers.

  1084   | strip_assums_all (params, B) = (params, B)

  1128 *}

  1085 

  1129 

  1086 fun style_parm_premise i ctxt t =

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

  1087   let val prems = Logic.strip_imp_prems t in

  1131       Term.dest_abs body |> snd |> strip_all

  1088     if i <= length prems

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

  1089     then let val (params,t) = strip_assums_all([], nth prems (i - 1))

  1133   | strip_all t = t*}

  1090          in subst_bounds(map Free params, t) end

  1134 

  1091     else error ("Not enough premises for prem" ^ string_of_int i ^

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

  1092       " in propositon: " ^ string_of_term ctxt t)

  1136 

  1093   end;

  1137 text {*

  1094 *}

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

  1095 

  1139   @{text "strip_all"}. 

  1096 ML {*

  1140 *}

  1097 strip_assums_all ([], @{term "\<And>x y. A x y"})

  1141 

  1098 *}

  1099 

  1100 (*

  1102   TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>

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

  1103   TermStyle.add_style "no_all_prem2" (style_parm_premise 2)

  1144 *}

  1104 *}

  1145 

  1105 *)

  1146 text {*

  1106 lemma 

  1147   We can test the theorem style with the following theorem

  1107   shows "A \<Longrightarrow> B"

  1148 *}

  1108   and   "C \<Longrightarrow> D"

  1149 

  1109 oops

  1150 theorem style_test:

  1151   shows "\<forall>x y z. (x, x) = (y, z)" sorry

  1152 

  1153 text {*

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

  1155   in a document produces

  1156 

  1157   @{thm [display] style_test}

  1158 

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

  1160   we obtain

  1161 

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

  1163   

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

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

  1166   explain theorem attributes, which is another mechanism for treating

  1167   theorems.

  1168 *}