# HG changeset patch
# User traytel
# Date 1372876901 -7200
# Node ID eb80a16a2b72deccd8721468d503b499b945d81a
# Parent  e62f3fd2035efc740b67fc24a2ce2b5ac995457a
use long goal format in rel_induct theorem

diff -r e62f3fd2035e -r eb80a16a2b72 src/HOL/BNF/Tools/bnf_fp_util.ML
--- 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;
diff -r e62f3fd2035e -r eb80a16a2b72 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- 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))) =>
diff -r e62f3fd2035e -r eb80a16a2b72 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- 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;