# HG changeset patch # User blanchet # Date 1403856704 -7200 # Node ID cfc19f0a62611c6f4d24f62366fadb7b67776447 # Parent 882091eb1e9a8a39a3503fab5b3ee01832e3f1f8 compile diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jun 27 10:11:44 2014 +0200 @@ -61,6 +61,7 @@ val map_def_of_bnf: bnf -> thm val map_id0_of_bnf: bnf -> thm val map_id_of_bnf: bnf -> thm + val map_ident0_of_bnf: bnf -> thm val map_ident_of_bnf: bnf -> thm val map_transfer_of_bnf: bnf -> thm val le_rel_OO_of_bnf: bnf -> thm @@ -223,6 +224,7 @@ map_comp: thm lazy, map_cong: thm lazy, map_id: thm lazy, + map_ident0: thm lazy, map_ident: thm lazy, map_transfer: thm lazy, rel_eq: thm lazy, @@ -237,8 +239,8 @@ }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel - inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip set_map rel_cong - rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = { + inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map + rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -251,6 +253,7 @@ map_comp = map_comp, map_cong = map_cong, map_id = map_id, + map_ident0 = map_ident0, map_ident = map_ident, map_transfer = map_transfer, rel_eq = rel_eq, @@ -276,6 +279,7 @@ map_comp, map_cong, map_id, + map_ident0, map_ident, map_transfer, rel_eq, @@ -299,6 +303,7 @@ map_comp = Lazy.map f map_comp, map_cong = Lazy.map f map_cong, map_id = Lazy.map f map_id, + map_ident0 = Lazy.map f map_ident0, map_ident = Lazy.map f map_ident, map_transfer = Lazy.map f map_transfer, rel_eq = Lazy.map f rel_eq, @@ -418,6 +423,7 @@ val map_def_of_bnf = #map_def o #defs o rep_bnf; val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf; val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf; +val map_ident0_of_bnf = Lazy.force o #map_ident0 o #facts o rep_bnf; val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf; val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf; val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf; @@ -1104,6 +1110,7 @@ val in_cong = Lazy.lazy mk_in_cong; val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms)); + val map_ident0 = Lazy.lazy (fn () => mk_map_ident lthy (#map_id0 axioms)); val map_ident = Lazy.lazy (fn () => mk_map_ident lthy (Lazy.force map_id)); val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms)); @@ -1321,8 +1328,8 @@ val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def; val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong - in_mono in_rel inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip - set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO; + in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq + rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO; val wits = map2 mk_witness bnf_wits wit_thms; diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 10:11:44 2014 +0200 @@ -456,9 +456,8 @@ val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; - val live_nesting_map_idents = - map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs; - val fp_nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) fp_nesting_bnfs; + val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; + val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs; val fp_b_names = map base_name_of_typ fpTs; @@ -583,7 +582,7 @@ val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss; val tacss = map4 (map ooo - mk_rec_tac pre_map_defs (fp_nesting_map_idents @ live_nesting_map_idents) rec_defs) + mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs) ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss; fun prove goal tac = @@ -736,8 +735,7 @@ val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_rel_defs = map rel_def_of_bnf pre_bnfs; - val live_nesting_map_idents = - map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs; + val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; val fp_b_names = map base_name_of_typ fpTs; @@ -855,7 +853,7 @@ val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss'; val tacss = - map4 (map ooo mk_corec_tac corec_defs live_nesting_map_idents) + map4 (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s) ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss; fun prove goal tac = diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200 @@ -98,15 +98,15 @@ @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv case_unit_Unity} @ sumprod_thms_map; -fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = +fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ - pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl); + pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl); val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map; -fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt = +fun mk_corec_tac corec_defs map_ident0s ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt = let - val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ corec_unfold_thms @ + val ss = ss_only (pre_map_def :: abs_inverse :: map_ident0s @ corec_unfold_thms @ @{thms o_apply vimage2p_def if_True if_False}) ctxt; in unfold_thms_tac ctxt (ctr_def :: corec_defs) THEN diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200 @@ -80,7 +80,7 @@ disc_exhausts: thm list, sel_defs: thm list, fp_nesting_maps: thm list, - fp_nesting_map_idents: thm list, + fp_nesting_map_ident0s: thm list, fp_nesting_map_comps: thm list, ctr_specs: corec_ctr_spec list}; @@ -466,8 +466,7 @@ {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts, sel_defs = sel_defs, fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs, - fp_nesting_map_idents = - map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs, + fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs, fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs, ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss}; @@ -1175,7 +1174,7 @@ |> single end; - fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_idents, fp_nesting_map_comps, + fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_ident0s, fp_nesting_map_comps, ctr_specs, ...} : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...} : coeqn_data_sel) = @@ -1198,7 +1197,7 @@ val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term; in mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps - fp_nesting_map_idents fp_nesting_map_comps sel_corec k m excludesss + fp_nesting_map_ident0s fp_nesting_map_comps sel_corec k m excludesss |> K |> Goal.prove_sorry lthy [] [] goal |> Thm.close_derivation |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*) diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200 @@ -126,7 +126,7 @@ (etac FalseE ORELSE' resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac)); -fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k +fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k m excludesss = prelude_tac ctxt defs (fun_sel RS trans) THEN cases_tac ctxt k m excludesss THEN @@ -139,7 +139,7 @@ etac notE THEN' atac ORELSE' (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ - mapsx @ map_comps @ map_idents))) ORELSE' + mapsx @ map_ident0s @ map_comps))) ORELSE' fo_rtac @{thm cong} ctxt ORELSE' rtac @{thm ext})); diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200 @@ -79,7 +79,7 @@ type rec_spec = {recx: term, - fp_nesting_map_idents: thm list, + fp_nesting_map_ident0s: thm list, fp_nesting_map_comps: thm list, ctr_specs: rec_ctr_spec list}; @@ -135,7 +135,7 @@ let val thy = Proof_Context.theory_of lthy0; - val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_idents, fp_nesting_map_comps, + val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, n2m, lthy) = get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0; @@ -195,7 +195,7 @@ fun mk_spec ctr_offset ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) = {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx, - fp_nesting_map_idents = fp_nesting_map_idents, fp_nesting_map_comps = fp_nesting_map_comps, + fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps, ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms}; in ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy) @@ -415,10 +415,10 @@ |> (fn [] => NONE | callss => SOME (ctr, callss)) end; -fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx = +fun mk_primrec_tac ctxt num_extra_args map_ident0s map_comps fun_defs recx = unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN - unfold_thms_tac ctxt (nested_simps ctxt @ map_comps @ map_idents) THEN + unfold_thms_tac ctxt (nested_simps ctxt @ map_ident0s @ map_comps) THEN HEADGOAL (rtac refl); fun prepare_primrec nonexhaustive fixes specs lthy0 = @@ -464,7 +464,7 @@ val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call; - fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_idents, fp_nesting_map_comps, ...} + fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...} : rec_spec) (fun_data : eqn_data list) = let val js = @@ -477,7 +477,7 @@ |> map_filter (try (fn (x, [y]) => (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) => - mk_primrec_tac lthy' num_extra_args fp_nesting_map_idents fp_nesting_map_comps + mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps def_thms rec_thm |> K |> Goal.prove_sorry lthy' [] [] user_eqn (* for code extraction from proof terms: *) diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 10:11:44 2014 +0200 @@ -47,12 +47,11 @@ val ctrXs_Tsss = map #ctrXs_Tss fp_sugars; val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss; - val fp_nesting_map_idents = - map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs; + val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; in (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, - fp_nesting_map_idents, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy) + fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy) end; exception NOT_A_MAP of term; diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 10:11:44 2014 +0200 @@ -66,12 +66,13 @@ val rec_o_map_simp_thms = @{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def}; -fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses ctor_rec_o_map = +fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses + ctor_rec_o_map = unfold_thms_tac ctxt [rec_def] THEN HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @ - distinct Thm.eq_thm_prop (live_nesting_map_idents @ abs_inverses) @ rec_o_map_simp_thms) ctxt)); + distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simp_thms) ctxt)); val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; @@ -258,7 +259,7 @@ let val pre_bnfs = map #pre_bnf fp_sugars; val pre_map_defs = map map_def_of_bnf pre_bnfs; - val live_nesting_map_idents = map map_ident_of_bnf live_nesting_bnfs; + val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars; val rec_defs = map #co_rec_def fp_sugars; @@ -303,7 +304,7 @@ val rec_o_map_thms = map3 (fn goal => fn rec_def => fn ctor_rec_o_map => Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} => - mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses + mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses ctor_rec_o_map) |> Thm.close_derivation) rec_o_map_goals rec_defs ctor_rec_o_maps; diff -r 882091eb1e9a -r cfc19f0a6261 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Jun 27 10:11:44 2014 +0200 @@ -36,14 +36,14 @@ fun mk_pred pred_def args T = let - val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq + val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |> head_of |> fst o dest_Const val argsT = map fastype_of args in list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args) end -fun mk_eq_onp arg = +fun mk_eq_onp arg = let val argT = domain_type (fastype_of arg) in @@ -75,17 +75,17 @@ fun mk_relation_constraint name arg = (Const (name, fastype_of arg --> HOLogic.boolT)) $ arg -fun side_constraint_tac bnf constr_defs ctxt i = +fun side_constraint_tac bnf constr_defs ctxt i = let val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf, rel_OO_of_bnf bnf] - in + in (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf) THEN_ALL_NEW atac) i end -fun bi_constraint_tac constr_iff sided_constr_intros ctxt i = - (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN' +fun bi_constraint_tac constr_iff sided_constr_intros ctxt i = + (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN' CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i fun generate_relation_constraint_goal ctxt bnf constraint_def = @@ -97,7 +97,7 @@ |> mk_TFrees live ||>> mk_TFrees live ||>> mk_TFrees (dead_of_bnf bnf) - + val relator = mk_rel_of_bnf Ds As Bs bnf val relsT = map2 mk_pred2T As Bs val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt @@ -112,7 +112,7 @@ let val old_ctxt = ctxt val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def - val thm = Goal.prove ctxt [] [] goal + val thm = Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1) in Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) @@ -122,7 +122,7 @@ let val old_ctxt = ctxt val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def - val thm = Goal.prove ctxt [] [] goal + val thm = Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1) in Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) @@ -136,11 +136,11 @@ val transfer_attr = @{attributes [transfer_rule]} val Tname = base_name_of_bnf bnf fun qualify suffix = Binding.qualified true suffix Tname - + val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs - val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def} + val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def} [snd (nth defs 0), snd (nth defs 1)] - val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def} + val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def} [snd (nth defs 2), snd (nth defs 3)] val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs @@ -174,7 +174,7 @@ val head = Free (Binding.name_of pred_name, headT) val lhs = list_comb (head, args) val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) - val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)), + val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)), ((Binding.empty, []), def)) lthy in (pred_def, lthy) @@ -185,19 +185,19 @@ val n = live_of_bnf bnf val set_map's = set_map_of_bnf bnf in - EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps}, + EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps}, in_rel_of_bnf bnf, pred_def]), rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt, CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp), etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}], hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]}, - etac @{thm DomainPI}]) set_map's, - REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI], + etac @{thm DomainPI}]) set_map's, + REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI], rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym, map_id_of_bnf bnf]), REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]}, rtac @{thm fst_conv}]), rtac CollectI, - CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}), + CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}), REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}], dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's ] i @@ -219,14 +219,14 @@ val lhs = mk_Domainp (list_comb (relator, args)) val rhs = mk_pred pred_def (map mk_Domainp args) T val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop - val thm = Goal.prove ctxt [] [] goal + val thm = Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1) in Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) end fun pred_eq_onp_tac bnf pred_def ctxt i = - (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp}, + (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp}, @{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym)) THEN' rtac (rel_Grp_of_bnf bnf)) i @@ -244,7 +244,7 @@ val lhs = list_comb (relator, map mk_eq_onp args) val rhs = mk_eq_onp (mk_pred pred_def args T) val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop - val thm = Goal.prove ctxt [] [] goal + val thm = Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1) in Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) @@ -259,7 +259,7 @@ fun qualify defname suffix = Binding.qualified true suffix defname val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel" val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp" - val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv + val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))) rel_eq_onp val pred_data = {rel_eq_onp = rel_eq_onp_internal} @@ -279,7 +279,7 @@ let val constr_notes = if dead_of_bnf bnf > 0 then [] else prove_relation_constraints bnf lthy - val relator_eq_notes = if dead_of_bnf bnf > 0 then [] + val relator_eq_notes = if dead_of_bnf bnf > 0 then [] else relator_eq bnf val (pred_notes, lthy) = predicator bnf lthy in @@ -299,8 +299,8 @@ fun prove_pred_inject lthy (fp_sugar:fp_sugar) = let val involved_types = distinct op= ( - map type_name_of_bnf (#nested_bnfs fp_sugar) - @ map type_name_of_bnf (#nesting_bnfs fp_sugar) + map type_name_of_bnf (#fp_nesting_bnfs fp_sugar) + @ map type_name_of_bnf (#live_nesting_bnfs fp_sugar) @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar))) val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types val live = live_of_bnf (bnf_of_fp_sugar fp_sugar) @@ -326,10 +326,10 @@ in thm |> Drule.instantiate' cTs cts - |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv + |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))) |> Local_Defs.unfold lthy eq_onps - |> (fn thm => if conjuncts <> [] then @{thm box_equals} + |> (fn thm => if conjuncts <> [] then @{thm box_equals} OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True] else thm RS (@{thm eq_onp_same_args} RS iffD1)) |> kill_top