694   Let us begin with describing the unification and matching function for

   694   Let us begin with describing the unification and matching functions for

  1094   For higher-order

  1094   For higher-order matching the function is called @{ML_ind matchers in Unify}

  1095   matching the function is called @{ML_ind matchers in Unify} implemented

  1095   implemented in the structure @{ML_struct Unify}. Also this function returns

  1096   in the structure @{ML_struct Unify}. Also this

  1096   sequences with possibly more than one matcher.  Like @{ML unifiers in

  1097   function returns sequences with possibly more than one matcher.

  1097   Unify}, this function does not raise an exception in case of failure, but

  1098   Like @{ML unifiers in Unify}, this function does not raise an exception

  1098   returns an empty sequence. It also first tries out whether the matching

  1099   in case of failure, but returns an empty sequence. It also first tries 

  1099   problem can be solved by first-order matching.

  1100   out whether the matching problem can be solved by first-order matching.

  1100 

  1101   Higher-order matching might be necessary for instantiating a theorem

  1102   appropriately (theorems and their instantiation will be described in more

  1103   detail in Sections~\ref{sec:theorems}). This is for example the 

  1104   case when applying the rule @{thm [source] spec}:

  1105 

  1106   \begin{isabelle}

  1107   \isacommand{thm}~@{thm [source] spec}\\

  1108   @{text "> "}~@{thm spec}

  1109   \end{isabelle}

  1110 

  1111   as an introduction rule. One way is to instantiate this rule. The

  1112   instantiation function for theorems is @{ML_ind instantiate in Drule} from

  1113   the structure @{ML_struct Drule}. One problem, however, is that this 

  1114   function expects the instantiations as lists of @{ML_type ctyp} and 

  1115   @{ML_type cterm} pairs:

  1116 

  1117   \begin{isabelle}

  1118   @{ML instantiate in Drule}@{text ":"}

  1119   @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}

  1120   \end{isabelle}

  1121 

  1122   This means we have to transform the environment the higher-order matching 

  1123   function returns into such an instantiation. For this we use the functions

  1124   @{ML_ind term_env in Envir} and @{ML_ind type_env in Envir}, which extract

  1125   from an environment the corresponding variable mappings for schematic type 

  1126   and term variables. These mappings can be turned into proper 

  1127   @{ML_type ctyp}-pairs with the function

  1128 *}

  1129 

  1130 ML{*fun prep_trm thy (x, (T, t)) = 

  1131   (cterm_of thy (Var (x, T)), cterm_of thy t)*} 

  1132 

  1133 text {*

  1134   and into proper @{ML_type cterm}-pairs with

  1135 *}

  1136 

  1137 ML{*fun prep_ty thy (x, (S, ty)) = 

  1138   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}

  1139 

  1140 text {*

  1141   We can now calculate the instantiations from the matching function. 

  1142 *}

  1143 

  1144 ML %linenosgray{*fun matcher_inst thy pat trm i = 

  1145 let

  1146   val univ = Unify.matchers thy [(pat, trm)] 

  1147   val env = nth (Seq.list_of univ) i

  1148   val tenv = Vartab.dest (Envir.term_env env)

  1149   val tyenv = Vartab.dest (Envir.type_env env)

  1150 in

  1151   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)

  1152 end*}

  1153 

  1154 text {*

  1155   In Line 3 we obtain the higher-order matcher. We assume there is a finite

  1156   number of them and select the one we are interested in via the parameter 

  1157   @{text i} in the next line. In Lines 5 and 6 we destruct the resulting 

  1158   environments using the function @{ML_ind dest in Vartab}. Finally, we need 

  1159   to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective 

  1160   environments (Line 8). As a simple example we instantiate the 

  1161   @{thm [source] conjI}-rule as follows

  1162 

  1163   @{ML_response_fake [gray,display] 

  1164   "let  

  1165   val pat = Logic.strip_imp_concl (prop_of @{thm spec})

  1166   val trm = @{term \"Trueprop (P True)\"}

  1167   val inst = matcher_inst @{theory} pat trm 1

  1168 in

  1169   Drule.instantiate inst @{thm conjI}

  1170 end"

  1171   "\<forall>x. P x \<Longrightarrow> P True"}

  1292 section {* Theorems *}

  1363 section {* Theorems\label{sec:theorems} *}