--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 18:12:16 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 23:32:45 2016 +0200
@@ -119,9 +119,10 @@
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 -> 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 -> thm list -> thm list -> string -> BNF_Def.bnf ->
+ BNF_Def.bnf list -> typ -> term -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list ->
+ thm -> thm list -> thm list -> thm list -> 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
@@ -702,8 +703,9 @@
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_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
+ live_nesting_rel_eqs live_nesting_rel_eq_onps fp_nested_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
+ extra_unfolds_map extra_unfolds_set extra_unfolds_rel 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 =
@@ -872,7 +874,7 @@
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'
- live_nesting_map_ident0s ctr_defs')
+ live_nesting_map_ident0s ctr_defs' extra_unfolds_map)
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end;
@@ -898,7 +900,7 @@
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 live_nesting_rel_eqs
- ctr_defs')
+ ctr_defs' extra_unfolds_rel)
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end;
@@ -928,7 +930,7 @@
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
- live_nesting_rel_eqs ctr_defs')
+ live_nesting_rel_eqs ctr_defs' extra_unfolds_rel)
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end)
@@ -1294,8 +1296,9 @@
val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
(top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})));
- val eq_onps = map (rel_eq_onp_with_tops_of)
- (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps);
+ val eq_onps = map rel_eq_onp_with_tops_of
+ (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps @
+ fp_nested_rel_eq_onps);
val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) live_As);
val cts = map (SOME o Thm.cterm_of lthy) (map mk_eq_onp Ps);
@@ -1309,11 +1312,11 @@
val conjuncts = try (get_rhs #> HOLogic.dest_conj) rel_inject |> the_default [];
fun postproc thm =
- if conjuncts <> [] then
+ if null conjuncts then
+ thm RS (@{thm eq_onp_same_args} RS iffD1)
+ else
@{thm box_equals} OF [thm, @{thm eq_onp_same_args},
- pred_eq_onp_conj conjuncts |> unfold_thms lthy @{thms simp_thms(21)}]
- else
- thm RS (@{thm eq_onp_same_args} RS iffD1);
+ pred_eq_onp_conj conjuncts |> unfold_thms lthy @{thms simp_thms(21)}];
in
rel_inject
|> Thm.instantiate' cTs cts
@@ -2467,9 +2470,9 @@
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_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
+ 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 18:12:16 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 23:32:45 2016 +0200
@@ -32,7 +32,8 @@
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 -> thm list -> tactic
+ val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> 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
@@ -40,7 +41,8 @@
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 -> thm list -> tactic
+ val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> 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 ->
@@ -390,11 +392,12 @@
(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' live_nesting_map_ident0s ctr_defs' =
+fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_ident0s ctr_defs'
+ extra_unfolds =
TRYALL Goal.conjunction_tac 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
+ live_nesting_map_ident0s @ ctr_defs' @ extra_unfolds @ 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 =
@@ -416,10 +419,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 live_nesting_rel_eqs ctr_defs' =
+fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel live_nesting_rel_eqs ctr_defs'
+ extra_unfolds =
TRYALL Goal.conjunction_tac 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
+ ctr_defs' @ extra_unfolds @ 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]);
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Sun Sep 11 18:12:16 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Sun Sep 11 23:32:45 2016 +0200
@@ -505,9 +505,9 @@
map dest_TFree live_As
|> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);
- val ((bnf, _), (_, lthy)) =
- bnf_of_typ false Do_Inline I flatten_tyargs [Term.dest_TFree Y]
- (map Term.dest_TFree dead_Es) T ((empty_comp_cache, empty_unfolds), lthy)
+ val ((bnf, _), (_, lthy)) =
+ bnf_of_typ false Do_Inline I flatten_tyargs [Term.dest_TFree Y] (map Term.dest_TFree dead_Es)
+ T ((empty_comp_cache, empty_unfolds), lthy)
handle BAD_DEAD (Y, Y_backdrop) =>
(case Y_backdrop of
Type (bad_tc, _) =>
@@ -1668,8 +1668,7 @@
cutSsig_def algLam_def corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf
dead_ssig_bnf =
let
- val SOME prod_fp_sugar = fp_sugar_of ctxt @{type_name prod};
- val prod_bnf = #fp_bnf prod_fp_sugar;
+ val SOME prod_bnf = bnf_of ctxt @{type_name prod};
val f' = substT Z fpT f;
val dead_ssig_map' = substT Z fpT dead_ssig_map;