1122 \end{isabelle} |
1122 \end{isabelle} |
1123 |
1123 |
1124 as an introduction rule. Applying it directly can lead to unexpected |
1124 as an introduction rule. Applying it directly can lead to unexpected |
1125 behaviour since the unification has more than one solution. One way round |
1125 behaviour since the unification has more than one solution. One way round |
1126 this problem is to instantiate the schematic variables @{text "?P"} and |
1126 this problem is to instantiate the schematic variables @{text "?P"} and |
1127 @{text "?x"}. instantiation function for theorems is @{ML_ind instantiate |
1127 @{text "?x"}. instantiation function for theorems is |
1128 in Drule} from the structure @{ML_struct Drule}. One problem, however, is |
1128 @{ML_ind instantiate_normalize in Drule} from the structure |
|
1129 @{ML_struct Drule}. One problem, however, is |
1129 that this function expects the instantiations as lists of @{ML_type ctyp} |
1130 that this function expects the instantiations as lists of @{ML_type ctyp} |
1130 and @{ML_type cterm} pairs: |
1131 and @{ML_type cterm} pairs: |
1131 |
1132 |
1132 \begin{isabelle} |
1133 \begin{isabelle} |
1133 @{ML instantiate in Drule}@{text ":"} |
1134 @{ML instantiate_normalize in Drule}@{text ":"} |
1134 @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} |
1135 @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} |
1135 \end{isabelle} |
1136 \end{isabelle} |
1136 |
1137 |
1137 This means we have to transform the environment the higher-order matching |
1138 This means we have to transform the environment the higher-order matching |
1138 function returns into such an instantiation. For this we use the functions |
1139 function returns into such an instantiation. For this we use the functions |
1181 "let |
1182 "let |
1182 val pat = Logic.strip_imp_concl (prop_of @{thm spec}) |
1183 val pat = Logic.strip_imp_concl (prop_of @{thm spec}) |
1183 val trm = @{term \"Trueprop (Q True)\"} |
1184 val trm = @{term \"Trueprop (Q True)\"} |
1184 val inst = matcher_inst @{theory} pat trm 1 |
1185 val inst = matcher_inst @{theory} pat trm 1 |
1185 in |
1186 in |
1186 Drule.instantiate inst @{thm spec} |
1187 Drule.instantiate_normalize inst @{thm spec} |
1187 end" |
1188 end" |
1188 "\<forall>x. Q x \<Longrightarrow> Q True"} |
1189 "\<forall>x. Q x \<Longrightarrow> Q True"} |
1189 |
1190 |
1190 Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the |
1191 Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the |
1191 conclusion of @{thm [source] spec} contains one. |
1192 conclusion of @{thm [source] spec} contains one. |