--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Jul 03 16:53:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Jul 03 20:41:41 2013 +0200
@@ -480,8 +480,7 @@
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (flip mk_leq) relphis pre_phis));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (phis @ pre_phis) (Logic.list_implies (prems, concl))) tac
+ Goal.prove_sorry lthy (map (fst o dest_Free) (phis @ pre_phis)) prems concl tac
|> Thm.close_derivation
|> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
end;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Jul 03 16:53:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Jul 03 20:41:41 2013 +0200
@@ -103,7 +103,7 @@
val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
thm list -> thm list -> thm -> thm list -> tactic
val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ {prems: thm list, context: Proof.context} -> tactic
val mk_rel_coinduct_coind_tac: int -> thm -> int list -> thm list -> thm list -> thm list ->
thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_rel_coinduct_ind_tac: int -> int list -> thm list -> thm list list -> int -> thm ->
@@ -1634,9 +1634,10 @@
end;
fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s
- {context = ctxt, prems = _} =
+ {context = ctxt, prems = CIHs} =
let val n = length in_rels;
in
+ Method.insert_tac CIHs 1 THEN
unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
REPEAT_DETERM (etac exE 1) THEN
CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Jul 03 16:53:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Jul 03 20:41:41 2013 +0200
@@ -65,7 +65,7 @@
thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ {prems: thm list, context: Proof.context} -> tactic
val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
tactic
@@ -846,19 +846,19 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
-fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = _} =
+fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
let val n = length ks;
in
unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
- EVERY' (map3 (fn i => fn ctor_rel => fn rel_mono_strong =>
- EVERY' [rtac impI, dtac (ctor_rel RS iffD1), select_prem_tac n (dtac @{thm spec2}) i,
- etac mp, etac rel_mono_strong,
+ EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
+ EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
+ etac rel_mono_strong,
REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
EVERY' (map (fn j =>
EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
Goal.assume_rule_tac ctxt]) ks)])
- ks ctor_rels rel_mono_strongs)] 1
+ IHs ctor_rels rel_mono_strongs)] 1
end;
end;