equal
deleted
inserted
replaced
1072 in |
1072 in |
1073 rtac rule i |
1073 rtac rule i |
1074 end) |
1074 end) |
1075 *} |
1075 *} |
1076 |
1076 |
1077 section {* General shape of the lifting procedure *} |
1077 section {* General Shape of the Lifting Procedure *} |
1078 |
1078 |
1079 (* - A is the original raw theorem *) |
1079 (* - A is the original raw theorem *) |
1080 (* - B is the regularized theorem *) |
1080 (* - B is the regularized theorem *) |
1081 (* - C is the rep/abs injected version of B *) |
1081 (* - C is the rep/abs injected version of B *) |
1082 (* - D is the lifted theorem *) |
1082 (* - D is the lifted theorem *) |
1125 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1125 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1126 end |
1126 end |
1127 *} |
1127 *} |
1128 |
1128 |
1129 ML {* |
1129 ML {* |
1130 (* leaves three subgoales to be proved *) |
1130 (* the tactic leaves three subgoals to be proved *) |
1131 fun procedure_tac ctxt rthm = |
1131 fun procedure_tac ctxt rthm = |
1132 ObjectLogic.full_atomize_tac |
1132 ObjectLogic.full_atomize_tac |
1133 THEN' gen_frees_tac ctxt |
1133 THEN' gen_frees_tac ctxt |
1134 THEN' CSUBGOAL (fn (goal, i) => |
1134 THEN' CSUBGOAL (fn (goal, i) => |
1135 let |
1135 let |
1140 in |
1140 in |
1141 (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i |
1141 (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i |
1142 end) |
1142 end) |
1143 *} |
1143 *} |
1144 |
1144 |
1145 ML {* |
1145 (* automatic proofs *) |
1146 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
1146 ML {* |
|
1147 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
1147 |
1148 |
1148 fun WARN (tac, msg) i st = |
1149 fun WARN (tac, msg) i st = |
1149 case Seq.pull ((SOLVES' tac) i st) of |
1150 case Seq.pull ((SOLVES' tac) i st) of |
1150 NONE => (warning msg; Seq.single st) |
1151 NONE => (warning msg; Seq.single st) |
1151 | seqcell => Seq.make (fn () => seqcell) |
1152 | seqcell => Seq.make (fn () => seqcell) |