more robust tactic

--- a/src/HOL/BNF/Examples/Misc_Data.thy	Wed Jul 31 15:24:07 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy	Wed Jul 31 16:50:41 2013 +0200
@@ -150,6 +150,8 @@
 and s8 = S8 nat
 *)
 
+datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
+datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
 datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
 datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
 

--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Jul 31 15:24:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Jul 31 16:50:41 2013 +0200
@@ -1009,17 +1009,34 @@
 
         fun mk_in_bd () =
           let
+            val bdT = fst (dest_relT (fastype_of bnf_bd_As));
+            val bdTs = replicate live bdT;
+            val bd_bnfT = mk_bnf_T bdTs CA;
+            val surj_imp_ordLeq_inst = (if live = 0 then TrueI else
+              let
+                val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As';
+                val funTs = map (fn T => bdT --> T) ranTs;
+                val ran_bnfT = mk_bnf_T ranTs CA;
+                val (revTs, Ts) = `rev (bd_bnfT :: funTs);
+                val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
+                val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
+                  (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
+                    map Bound (live - 1 downto 0)) $ Bound live));
+                val cts = [NONE, SOME (certify lthy tinst)];
+              in
+                Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
+              end);
             val bd = mk_cexp
               (if live = 0 then ctwo
                 else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)
-              (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV
-                (mk_bnf_T (replicate live (fst (dest_relT (fastype_of bnf_bd_As)))) CA))));
+              (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV bd_bnfT)));
             val in_bd_goal =
               fold_rev Logic.all As
                 (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
           in
             Goal.prove_sorry lthy [] [] in_bd_goal
-              (mk_in_bd_tac live (Lazy.force map_comp') (Lazy.force map_id') (#map_cong0 axioms)
+              (mk_in_bd_tac live surj_imp_ordLeq_inst
+                (Lazy.force map_comp') (Lazy.force map_id') (#map_cong0 axioms)
                 (map Lazy.force set_map') (#set_bd axioms) (#bd_card_order axioms)
                 bd_Card_order bd_Cinfinite bd_Cnotzero)
             |> Thm.close_derivation

--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Jul 31 15:24:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Jul 31 16:50:41 2013 +0200
@@ -31,8 +31,8 @@
   val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm ->
     {prems: thm list, context: Proof.context} -> tactic
 
-  val mk_in_bd_tac: int -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm -> thm ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_in_bd_tac: int -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm ->
+    thm -> {prems: 'a, context: Proof.context} -> tactic
 end;
 
 structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -232,7 +232,7 @@
         REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
   end;
 
-fun mk_in_bd_tac live map_comp' map_id' map_cong0 set_map's set_bds
+fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp' map_id' map_cong0 set_map's set_bds
   bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
   if live = 0 then
     rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
@@ -269,7 +269,7 @@
         rtac @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN
       unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
       unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
-      EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm surj_imp_ordLeq}, rtac subsetI,
+      EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac surj_imp_ordLeq_inst, rtac subsetI,
         Method.insert_tac inserts, REPEAT_DETERM o dtac meta_spec,
         REPEAT_DETERM o eresolve_tac [exE, Tactic.make_elim conjunct1], etac CollectE,
         if live = 1 then K all_tac
@@ -284,13 +284,14 @@
         REPEAT_DETERM_N (2 * live) o atac,
         REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans),
         rtac refl,
-        rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
-        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
-           map_comp' RS sym, map_id']),
+        rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac (Drule.rotate_prems 1 @{thm image_eqI}),
         REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
         CONJ_WRAP' (fn thm =>
           rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
-        set_map's] 1
+        set_map's,
+        rtac sym,
+        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
+           map_comp' RS sym, map_id'])] 1
   end;
 
 end;