made tactic more robust w.r.t. dead variables; tuned;
--- 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;
--- 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