--- a/src/HOL/BNF/Tools/coinduction.ML Tue Nov 05 18:16:16 2013 +0100
+++ b/src/HOL/BNF/Tools/coinduction.ML Thu Oct 17 17:14:06 2013 +0200
@@ -75,7 +75,7 @@
map3 (fn name => fn T => fn (_, rhs) =>
HOLogic.mk_eq (Free (name, T), rhs))
names Ts raw_eqs;
- val phi = map (HOLogic.dest_Trueprop o prop_of) prems @ eqs
+ val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
|> try (Library.foldr1 HOLogic.mk_conj)
|> the_default @{term True}
|> list_exists_free vars
@@ -89,8 +89,8 @@
HEADGOAL (EVERY' [rtac thm,
EVERY' (map (fn var =>
rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
- EVERY' (map (fn prem => rtac conjI THEN' rtac prem) prems),
- CONJ_WRAP' (K (rtac refl)) eqs,
+ if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
+ else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
K (ALLGOALS_SKIP skip
(REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
@@ -100,11 +100,11 @@
let
val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
val inv_thms = init @ [last];
- val eqs = drop p inv_thms;
+ val eqs = take e inv_thms;
fun is_local_var t =
member (fn (t, (_, t')) => t aconv (term_of t')) params t;
val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
- val assms = assms' @ take p inv_thms
+ val assms = assms' @ drop e inv_thms
in
HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
unfold_thms_tac ctxt eqs