109 |
109 |
110 (*Rotates the given subgoal to be the last. Useful when re-playing |
110 (*Rotates the given subgoal to be the last. Useful when re-playing |
111 an old proof script, when the proof of an early subgoal fails. |
111 an old proof script, when the proof of an early subgoal fails. |
112 DOES NOT WORK FOR TYPE VARIABLES. |
112 DOES NOT WORK FOR TYPE VARIABLES. |
113 Similar to drule/rotate_prems*) |
113 Similar to drule/rotate_prems*) |
114 fun defer_tac i state = |
114 fun defer_rule i state = |
115 let val (state',thaw) = freeze_thaw state |
115 let val (state',thaw) = freeze_thaw state |
116 val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) |
116 val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) |
117 val hyp::hyps' = List.drop(hyps, i-1) |
117 val hyp::hyps' = List.drop(hyps, i-1) |
118 in implies_intr hyp (implies_elim_list state' (map assume hyps)) |
118 in implies_intr hyp (implies_elim_list state' (map assume hyps)) |
119 |> implies_intr_list (List.take(hyps, i-1) @ hyps') |
119 |> implies_intr_list (List.take(hyps, i-1) @ hyps') |
120 |> thaw |
120 |> thaw |
121 |> Seq.single |
121 end; |
122 end |
122 |
123 handle _ => Seq.empty; |
123 fun defer_tac i state = |
|
124 (case try (defer_rule i) state of |
|
125 Some state' => Seq.single state' |
|
126 | None => Seq.empty); |
124 |
127 |
125 |
128 |
126 (*Makes a rule by applying a tactic to an existing rule*) |
129 (*Makes a rule by applying a tactic to an existing rule*) |
127 fun rule_by_tactic tac rl = |
130 fun rule_by_tactic tac rl = |
128 let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
131 let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |