1303 |
1303 |
1304 (FIXME: handy functions working on theorems, like @{ML [index] rulify in ObjectLogic} and so on) |
1304 (FIXME: handy functions working on theorems, like @{ML [index] rulify in ObjectLogic} and so on) |
1305 |
1305 |
1306 (FIXME: how to add case-names to goal states - maybe in the |
1306 (FIXME: how to add case-names to goal states - maybe in the |
1307 next section) |
1307 next section) |
1308 *} |
1308 |
|
1309 (FIXME: example for how to add theorem styles) |
|
1310 *} |
|
1311 |
|
1312 ML {* |
|
1313 fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) = |
|
1314 strip_assums_all ((a, T)::params, t) |
|
1315 | strip_assums_all (params, B) = (params, B) |
|
1316 |
|
1317 fun style_parm_premise i ctxt t = |
|
1318 let val prems = Logic.strip_imp_prems t in |
|
1319 if i <= length prems |
|
1320 then let val (params,t) = strip_assums_all([], nth prems (i - 1)) |
|
1321 in subst_bounds(map Free params, t) end |
|
1322 else error ("Not enough premises for prem" ^ string_of_int i ^ |
|
1323 " in propositon: " ^ Syntax.string_of_term ctxt t) |
|
1324 end; |
|
1325 *} |
|
1326 |
|
1327 ML {* |
|
1328 strip_assums_all ([], @{term "\<And>x y. A x y"}) |
|
1329 *} |
|
1330 |
|
1331 setup {* |
|
1332 TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #> |
|
1333 TermStyle.add_style "no_all_prem2" (style_parm_premise 2) |
|
1334 *} |
|
1335 |
1309 |
1336 |
1310 section {* Setups (TBD) *} |
1337 section {* Setups (TBD) *} |
1311 |
1338 |
1312 text {* |
1339 text {* |
1313 In the previous section we used \isacommand{setup} in order to make |
1340 In the previous section we used \isacommand{setup} in order to make |
1673 content of @{ML my_thms} is unchanged. The backtracking mechanism |
1700 content of @{ML my_thms} is unchanged. The backtracking mechanism |
1674 of Isabelle is completely oblivious about what to do with references, but |
1701 of Isabelle is completely oblivious about what to do with references, but |
1675 properly treats ``data slots''! |
1702 properly treats ``data slots''! |
1676 |
1703 |
1677 Since storing theorems in a list is such a common task, there is the special |
1704 Since storing theorems in a list is such a common task, there is the special |
1678 functor @{text NamedThmsFun}, which does most of the work for you. To obtain |
1705 functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain |
1679 a named theorem lists, you just declare |
1706 a named theorem lists, you just declare |
1680 *} |
1707 *} |
1681 |
1708 |
1682 ML{*structure FooRules = NamedThmsFun |
1709 ML{*structure FooRules = Named_Thms |
1683 (val name = "foo" |
1710 (val name = "foo" |
1684 val description = "Rules for foo") *} |
1711 val description = "Rules for foo") *} |
1685 |
1712 |
1686 text {* |
1713 text {* |
1687 and set up the @{ML_struct FooRules} with the command |
1714 and set up the @{ML_struct FooRules} with the command |