equal
deleted
inserted
replaced
1115 |
1115 |
1116 ML {* |
1116 ML {* |
1117 fun atomize_goal thy gl = |
1117 fun atomize_goal thy gl = |
1118 let |
1118 let |
1119 val vars = map Free (Term.add_frees gl []); |
1119 val vars = map Free (Term.add_frees gl []); |
1120 fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm; |
1120 val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all; |
1121 val gla = fold lambda_all vars (@{term "Trueprop"} $ gl) |
1121 fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm; |
|
1122 val glv = fold lambda_all vars gl |
|
1123 val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv)) |
1122 val glf = Type.legacy_freeze gla |
1124 val glf = Type.legacy_freeze gla |
1123 val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf)) |
1125 in |
1124 in |
1126 if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf |
1125 term_of glac |
1127 end |
1126 end |
1128 *} |
1127 *} |
1129 |
|
1130 |
|
1131 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *} |
|
1132 ML {* atomize_goal @{theory} @{term "x = xa \<Longrightarrow> a # x = a # xa"} *} |
1128 |
1133 |
1129 |
1134 |
1130 ML {* |
1135 ML {* |
1131 (* builds the relation for respects *) |
1136 (* builds the relation for respects *) |
1132 |
1137 |
1510 in |
1515 in |
1511 Thm.varifyT t_rv |
1516 Thm.varifyT t_rv |
1512 end |
1517 end |
1513 *} |
1518 *} |
1514 |
1519 |
|
1520 ML {* |
|
1521 fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal = |
|
1522 let |
|
1523 val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal; |
|
1524 val (_, lthy2) = note (name, lifted_thm) lthy; |
|
1525 in |
|
1526 lthy2 |
|
1527 end |
|
1528 *} |
|
1529 |
1515 |
1530 |
1516 end |
1531 end |
1517 |
1532 |
1518 |
1533 |