# HG changeset patch # User blanchet # Date 1473629565 -7200 # Node ID 61a03e429cbdf7d552e3897b63f8b0d378463365 # Parent 9c22a97b767445cc323e6e7a3b5d9000b9c344e2 generalized code towards nonuniform (co)datatypes diff -r 9c22a97b7674 -r 61a03e429cbd src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 diff -r 9c22a97b7674 -r 61a03e429cbd src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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]); diff -r 9c22a97b7674 -r 61a03e429cbd src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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;