--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 15:37:09 2016 +0200
@@ -119,9 +119,9 @@
local_theory -> Ctr_Sugar.ctr_sugar * local_theory
val derive_map_set_rel_pred_thms: (string -> bool) -> BNF_Util.fp_kind -> int -> typ list ->
typ list -> typ -> typ -> thm list -> thm list -> thm list -> thm list -> thm list ->
- thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list -> typ -> term ->
- thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm -> typ list list -> term ->
- Ctr_Sugar.ctr_sugar -> Proof.context ->
+ thm list -> thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list ->
+ typ -> term -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm ->
+ typ list list -> term -> Ctr_Sugar.ctr_sugar -> local_theory ->
(thm list * thm list * thm list list * thm list * thm list * thm list * thm list * thm list
* thm list * thm list * thm list list list list * thm list list list list * thm list
* thm list * thm list * thm list * thm list) * local_theory
@@ -701,9 +701,9 @@
end;
fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs fp_nesting_set_maps
- fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
- live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor pre_map_def
- pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
+ fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_map_ident0s live_nesting_set_maps
+ live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor
+ dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss,
injects, distincts, distinct_discsss, ...} : ctr_sugar)
lthy =
@@ -871,7 +871,8 @@
else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans);
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
- mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm' ctr_defs')
+ mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm'
+ live_nesting_map_ident0s ctr_defs')
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end;
@@ -896,7 +897,8 @@
val vars = Variable.add_free_names lthy goal [];
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
- mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs')
+ mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm live_nesting_rel_eqs
+ ctr_defs')
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end;
@@ -925,7 +927,8 @@
val vars = Variable.add_free_names lthy goal [];
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
- mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs')
+ mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm
+ live_nesting_rel_eqs ctr_defs')
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end)
@@ -2462,10 +2465,11 @@
disc_bindings sel_bindingss sel_default_eqs ctrs0 ctor_iff_dtor_thm ctr_defs
#> (fn (ctr_sugar, lthy) =>
derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs
- fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
- live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor
- ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms
- fp_rel_thm ctr_Tss abs ctr_sugar lthy
+ fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s
+ live_nesting_map_ident0s live_nesting_set_maps live_nesting_rel_eqs
+ live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor
+ pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
+ ctr_sugar lthy
|>> pair ctr_sugar)
##>>
(if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 15:37:09 2016 +0200
@@ -8,6 +8,7 @@
signature BNF_FP_DEF_SUGAR_TACTICS =
sig
+ val sumprod_thms_rel: thm list
val sumprod_thms_set: thm list
val basic_sumprod_thms_set: thm list
@@ -31,7 +32,7 @@
val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
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_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
+ val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> 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 ->
thm list -> tactic
@@ -39,7 +40,7 @@
tactic
val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic
- val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
+ val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> tactic
val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
thm list -> thm list -> tactic
val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
@@ -389,10 +390,11 @@
(1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
selsss));
-fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' ctr_defs' =
+fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_ident0s ctr_defs' =
TRYALL Goal.conjunction_tac THEN
- unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @ ctr_defs' @ o_apply ::
- sumprod_thms_map) THEN
+ unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @
+ live_nesting_map_ident0s @
+ ctr_defs' @ sumprod_thms_map @ @{thms o_def[abs_def] id_def}) THEN
ALLGOALS (rtac ctxt refl);
fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
@@ -414,11 +416,11 @@
unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN
ALLGOALS (rtac ctxt refl);
-fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel ctr_defs' =
+fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel live_nesting_rel_eqs ctr_defs' =
TRYALL Goal.conjunction_tac THEN
- unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ ctr_defs' @ o_apply ::
- sumprod_thms_rel @ @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]
- not_False_eq_True}) THEN
+ unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @
+ ctr_defs' @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject
+ sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN
ALLGOALS (resolve_tac ctxt [TrueI, refl]);
fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs =