--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 12 13:27:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 12 13:48:15 2014 +0200
@@ -1729,7 +1729,7 @@
(fn {context = ctxt, prems = _} =>
mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
(flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
- rel_distinct_thms)
+ rel_distinct_thms (map rel_eq_of_bnf live_nesting_bnfs))
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -1858,7 +1858,7 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms
- (flat sel_thmss))
+ (flat sel_thmss) (map map_id0_of_bnf live_nesting_bnfs))
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Sep 12 13:27:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Sep 12 13:48:15 2014 +0200
@@ -29,7 +29,8 @@
thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
- val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
+ val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list ->
+ thm list -> tactic
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 ->
@@ -40,7 +41,7 @@
val mk_rel_induct0_tac: Proof.context -> thm -> thm list -> cterm list -> thm list ->
thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
- thm list -> thm list -> tactic
+ thm list -> thm list -> thm list -> tactic
val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic
val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> thm list -> tactic
@@ -253,14 +254,14 @@
handle THM _ => thm RS eqTrueI) discs) THEN
ALLGOALS (rtac refl ORELSE' rtac TrueI);
-fun mk_map_sel_tac ctxt ct exhaust discs maps sels =
+fun mk_map_sel_tac ctxt ct exhaust discs maps sels map_id0s =
TRYALL Goal.conjunction_tac THEN
ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
REPEAT_DETERM o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
@{thms not_True_eq_False not_False_eq_True}) THEN
TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
- unfold_thms_tac ctxt (maps @ sels) THEN
+ unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN
ALLGOALS (rtac refl);
fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
@@ -312,11 +313,11 @@
TRYALL (rtac refl ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
-fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts =
+fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels 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 (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
+ unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @ @{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