# HG changeset patch
# User desharna
# Date 1406543490 -7200
# Node ID 615223745d4eb0e9fef032fc366aa02f475fa74a
# Parent  d1e9022c01754007b78e49834f44e706c72b8025
made tactic more robust w.r.t. dead variables; tuned;

diff -r d1e9022c0175 -r 615223745d4e src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Jul 27 21:20:11 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 28 12:31:30 2014 +0200
@@ -1467,7 +1467,8 @@
                       val thm = Goal.prove_sorry lthy [] [] goal
                           (fn {context = ctxt, prems = _} =>
                             mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
-                              injects rel_inject_thms distincts rel_distinct_thms)
+                              injects rel_inject_thms distincts rel_distinct_thms
+                              (map rel_eq_of_bnf live_nesting_bnfs))
                         |> singleton (Proof_Context.export names_lthy lthy)
                         |> Thm.close_derivation;
 
diff -r d1e9022c0175 -r 615223745d4e src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Jul 27 21:20:11 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 28 12:31:30 2014 +0200
@@ -28,7 +28,7 @@
   val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
     tactic
   val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
-    thm list -> thm list -> tactic
+    thm list -> thm list -> thm list -> tactic
   val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
     thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
     thm list -> thm list -> thm list -> tactic
@@ -216,11 +216,11 @@
       (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
       selsss));
 
-fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts =
+fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
   HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
     rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
       hyp_subst_tac ctxt) THEN
-  unfold_thms_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
+  unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
     True_implies_equals conj_imp_eq_imp_imp} @
     map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
     map (fn thm => thm RS eqTrueI) rel_injects) THEN
@@ -260,7 +260,7 @@
         unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
           @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
         TRYALL (hyp_subst_tac ctxt) THEN
-        unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
+        unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
           Inr_Inl_False  sum.inject prod.inject}) THEN
         TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
     cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
@@ -269,7 +269,7 @@
   HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
     rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
       hyp_subst_tac ctxt) THEN
-  Local_Defs.unfold_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
+  unfold_thms_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
     ((discs @ distincts) RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
     (rel_injects RL @{thms iffD2[OF eq_True]}) @
     (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN