# HG changeset patch # User blanchet # Date 1410796597 -7200 # Node ID 55e83cd308732e7f2752f9b1d7393ad15e77eb83 # Parent 3d64590d97521915ee040e908ec73f54fc015354 refactoring diff -r 3d64590d9752 -r 55e83cd30873 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 15 16:34:05 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 15 17:56:37 2014 +0200 @@ -390,6 +390,502 @@ fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p; +fun massage_simple_notes base = + filter_out (null o #2) + #> map (fn (thmN, thms, f_attrs) => + ((Binding.qualify true base (Binding.name thmN), []), + map_index (fn (i, thm) => ([thm], f_attrs i)) thms)); + +fun massage_multi_notes b_names Ts = + maps (fn (thmN, thmss, attrs) => + map3 (fn b_name => fn Type (T_name, _) => fn thms => + ((Binding.qualify true b_name (Binding.name thmN), attrs T_name), [(thms, [])])) + b_names Ts thmss) + #> filter_out (null o fst o hd o snd); + +fun derive_map_set_rel_thms names_lthy plugins fp live As Bs abs_inverses ctr_defs' + live_nesting_rel_eqs xss yss fp_nesting_set_maps live_nesting_set_maps live_nesting_map_id0s + fp_b_name fp_bnf fpT ctor ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm + fp_set_thms fp_rel_thm n ks ms abs abs_inverse + ({casex, case_thms, discs, selss, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, + distincts, distinct_discsss, ...} : ctr_sugar) + lthy = + if live = 0 then + (([], [], [], []), lthy) + else + let + val B_ify = Term.typ_subst_atomic (As ~~ Bs); + + val fpBT = B_ify fpT; + val live_AsBs = filter (op <>) (As ~~ Bs); + val fTs = map (op -->) live_AsBs; + + val (((((([C, E], fs), Rs), ta), tb), thesis), names_lthy) = names_lthy + |> mk_TFrees 2 + ||>> mk_Frees "f" fTs + ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs) + ||>> yield_singleton (mk_Frees "a") fpT + ||>> yield_singleton (mk_Frees "b") fpBT + ||>> apfst HOLogic.mk_Trueprop o yield_singleton (mk_Frees "thesis") HOLogic.boolT; + + val mapx = mk_map live As Bs (map_of_bnf fp_bnf); + val ctrAs = map (mk_ctr As) ctrs; + val ctrBs = map (mk_ctr Bs) ctrs; + val relAsBs = mk_rel live As Bs (rel_of_bnf fp_bnf); + val setAs = map (mk_set As) (sets_of_bnf fp_bnf); + val discAs = map (mk_disc_or_sel As) discs; + val discBs = map (mk_disc_or_sel Bs) discs; + val selAss = map (map (mk_disc_or_sel As)) selss; + val discAs_selAss = flat (map2 (map o pair) discAs selAss); + + val ctor_cong = + if fp = Least_FP then + Drule.dummy_thm + else + let val ctor' = mk_ctor Bs ctor in + cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong + end; + + fun mk_cIn ctor k xs = + let val absT = domain_type (fastype_of ctor) in + mk_absumprod absT abs n k xs + |> fp = Greatest_FP ? curry (op $) ctor + |> certify lthy + end; + + val cxIns = map2 (mk_cIn ctor) ks xss; + val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss; + + fun mk_map_thm ctr_def' cxIn = + fold_thms lthy [ctr_def'] + (unfold_thms lthy (o_apply :: pre_map_def :: + (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses) + (cterm_instantiate_pos (map (SOME o certify lthy) fs @ [SOME cxIn]) + (if fp = Least_FP then fp_map_thm + else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans)))) + |> singleton (Proof_Context.export names_lthy lthy); + + fun mk_set0_thm fp_set_thm ctr_def' cxIn = + fold_thms lthy [ctr_def'] + (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @ + (if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @ + @{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses) + (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) + |> singleton (Proof_Context.export names_lthy lthy); + + fun mk_set0_thms fp_set_thm = map2 (mk_set0_thm fp_set_thm) ctr_defs' cxIns; + + val map_thms = map2 mk_map_thm ctr_defs' cxIns; + val set0_thmss = map mk_set0_thms fp_set_thms; + val set0_thms = flat set0_thmss; + val set_thms = set0_thms + |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left Un_insert_left}); + + val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); + + fun mk_rel_thm postproc ctr_defs' cxIn cyIn = + fold_thms lthy ctr_defs' + (unfold_thms lthy (pre_rel_def :: abs_inverse :: + (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ + @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) + (cterm_instantiate_pos (map (SOME o certify lthy) Rs @ [SOME cxIn, SOME cyIn]) + fp_rel_thm)) + |> postproc + |> singleton (Proof_Context.export names_lthy lthy); + + fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) = + mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn; + + fun mk_rel_intro_thm m thm = + uncurry_thm m (thm RS iffD2) handle THM _ => thm; + + fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) = + mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def'] cxIn cyIn; + + val rel_flip = rel_flip_of_bnf fp_bnf; + + fun mk_other_half_rel_distinct_thm thm = + flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); + + val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); + val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms; + + val half_rel_distinct_thmss = map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos); + val other_half_rel_distinct_thmss = + map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; + val (rel_distinct_thms, _) = + join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; + + val rel_eq_thms = + map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ + map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms; + + val ctr_transfer_thms = + let val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs in + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; + + val (set_cases_thms, set_cases_attrss) = + let + fun mk_prems assms elem t ctxt = + (case fastype_of t of + Type (type_name, xs) => + (case bnf_of ctxt type_name of + NONE => ([], ctxt) + | SOME bnf => + apfst flat (fold_map (fn set => fn ctxt => + let + val T = HOLogic.dest_setT (range_type (fastype_of set)); + val new_var = not (T = fastype_of elem); + val (x, ctxt') = + if new_var then yield_singleton (mk_Frees "x") T ctxt else (elem, ctxt); + in + mk_prems (mk_Trueprop_mem (x, set $ t) :: assms) elem x ctxt' + |>> map (new_var ? Logic.all x) + end) (map (mk_set xs) (sets_of_bnf bnf)) ctxt)) + | T => + rpair ctxt + (if T = fastype_of elem then [fold (curry Logic.mk_implies) assms thesis] else [])); + in + split_list (map (fn set => + let + val A = HOLogic.dest_setT (range_type (fastype_of set)); + val (elem, names_lthy) = yield_singleton (mk_Frees "e") A names_lthy; + val premss = + map (fn ctr => + let + val (args, names_lthy) = + mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy; + in + flat (zipper_map (fn (prev_args, arg, next_args) => + let + val (args_with_elem, args_without_elem) = + if fastype_of arg = A then + (prev_args @ [elem] @ next_args, prev_args @ next_args) + else + `I (prev_args @ [arg] @ next_args); + in + mk_prems [mk_Trueprop_eq (ta, Term.list_comb (ctr, args_with_elem))] + elem arg names_lthy + |> fst + |> map (fold_rev Logic.all args_without_elem) + end) args) + end) ctrAs; + val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis); + val thm = + Goal.prove_sorry lthy [] (flat premss) goal (fn {context = ctxt, prems} => + mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + |> rotate_prems ~1; + + val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); + val cases_set_attr = + Attrib.internal (K (Induct.cases_pred (name_of_set set))); + in + (* TODO: @{attributes [elim?]} *) + (thm, [consumes_attr, cases_set_attr]) + end) setAs) + end; + + val set_intros_thms = + let + fun mk_goals A setA ctr_args t ctxt = + (case fastype_of t of + Type (type_name, innerTs) => + (case bnf_of ctxt type_name of + NONE => ([], ctxt) + | SOME bnf => + apfst flat (fold_map (fn set => fn ctxt => + let + val T = HOLogic.dest_setT (range_type (fastype_of set)); + val (x, ctxt') = yield_singleton (mk_Frees "x") T ctxt; + val assm = mk_Trueprop_mem (x, set $ t); + in + apfst (map (Logic.mk_implies o pair assm)) (mk_goals A setA ctr_args x ctxt') + end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt)) + | T => (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt)); + + val (goals, names_lthy) = + apfst flat (fold_map (fn set => fn ctxt => + let val A = HOLogic.dest_setT (range_type (fastype_of set)) in + apfst flat (fold_map (fn ctr => fn ctxt => + let + val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt; + val ctr_args = Term.list_comb (ctr, args); + in + apfst flat (fold_map (mk_goals A set ctr_args) args ctxt') + end) ctrAs ctxt) + end) setAs lthy); + in + if null goals then [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; + + val rel_sel_thms = + let + val selBss = map (map (mk_disc_or_sel Bs)) selss; + val n = length discAs; + + fun mk_conjunct n k discA selAs discB selBs = + (if k = n then [] else [HOLogic.mk_eq (discA $ ta, discB $ tb)]) @ + (if null selAs then + [] + else + [Library.foldr HOLogic.mk_imp + (if n = 1 then [] else [discA $ ta, discB $ tb], + Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs []) + (map (rapp ta) selAs) (map (rapp tb) selBs)))]); + + val goals = + if n = 0 then + [] + else + [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb, + (case flat (map5 (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of + [] => @{term True} + | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))]; + + fun prove goal = + Goal.prove_sorry lthy [] [] goal (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 live_nesting_rel_eqs) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation; + in + map prove goals + end; + + val (rel_cases_thm, rel_cases_attrs) = + let + val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb; + val ctrBs = map (mk_ctr Bs) ctrs; + + fun mk_assms ctrA ctrB ctxt = + let + val argA_Ts = binder_types (fastype_of ctrA); + val argB_Ts = binder_types (fastype_of ctrB); + val ((argAs, argBs), names_ctxt) = ctxt + |> mk_Frees "x" argA_Ts + ||>> mk_Frees "y" argB_Ts; + val ctrA_args = list_comb (ctrA, argAs); + val ctrB_args = list_comb (ctrB, argBs); + in + (fold_rev Logic.all (argAs @ argBs) (Logic.list_implies + (mk_Trueprop_eq (ta, ctrA_args) :: mk_Trueprop_eq (tb, ctrB_args) :: + map2 (HOLogic.mk_Trueprop oo build_rel_app lthy Rs []) argAs argBs, + thesis)), + names_ctxt) + end; + + val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy; + val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis); + val thm = + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust injects + rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation; + + val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs); + val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); + val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); + val cases_pred_attr = Attrib.internal o K o Induct.cases_pred; + in + (thm, [consumes_attr, case_names_attr, cases_pred_attr ""]) + end; + + val case_transfer_thms = + let + val (R, names_lthy) = yield_singleton (mk_Frees "R") (mk_pred2T C E) names_lthy; + + val caseA = mk_case As C casex; + val caseB = mk_case Bs E casex; + val goal = mk_parametricity_goal names_lthy (R :: Rs) caseA caseB; + in + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + mk_case_transfer_tac ctxt rel_cases_thm case_thms) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + end; + + val disc_transfer_thms = + let val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs in + if null goals then + [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (K (mk_disc_transfer_tac (the_single rel_sel_thms) (the_single exhaust_discs) + (flat (flat distinct_discsss)))) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; + + val map_disc_iff_thms = + let + val discsB = map (mk_disc_or_sel Bs) discs; + val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs; + + fun mk_goal (discA_t, discB) = + if head_of discA_t aconv HOLogic.Not orelse is_refl_bool discA_t then + NONE + else + SOME (mk_Trueprop_eq (betapply (discB, (Term.list_comb (mapx, fs) $ ta)), discA_t)); + + val goals = map_filter mk_goal (discsA_t ~~ discsB); + in + if null goals then + [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) + map_thms) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; + + val map_sel_thms = + let + fun mk_goal (discA, selA) = + let + val prem = Term.betapply (discA, ta); + val selB = mk_disc_or_sel Bs selA; + val lhs = selB $ (Term.list_comb (mapx, fs) $ ta); + val lhsT = fastype_of lhs; + val map_rhsT = + map_atyps (perhaps (AList.lookup (op =) (map swap live_AsBs))) lhsT; + val map_rhs = build_map lthy [] + (the o (AList.lookup (op =) (live_AsBs ~~ fs))) (map_rhsT, lhsT); + val rhs = (case map_rhs of + Const (@{const_name id}, _) => selA $ ta + | _ => map_rhs $ (selA $ ta)); + val concl = mk_Trueprop_eq (lhs, rhs); + in + if is_refl_bool prem then concl + else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl) + end; + + val goals = map mk_goal discAs_selAss; + in + if null goals then + [] + else + 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) live_nesting_map_id0s) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; + + val set_sel_thms = + let + fun mk_goal discA selA setA ctxt = + let + val prem = Term.betapply (discA, ta); + val sel_rangeT = range_type (fastype_of selA); + val A = HOLogic.dest_setT (range_type (fastype_of setA)); + + fun travese_nested_types t ctxt = + (case fastype_of t of + Type (type_name, innerTs) => + (case bnf_of ctxt type_name of + NONE => ([], ctxt) + | SOME bnf => + let + fun seq_assm a set ctxt = + let + val T = HOLogic.dest_setT (range_type (fastype_of set)); + val (x, ctxt') = yield_singleton (mk_Frees "x") T ctxt; + val assm = mk_Trueprop_mem (x, set $ a); + in + travese_nested_types x ctxt' + |>> map (Logic.mk_implies o pair assm) + end; + in + fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt + |>> flat + end) + | T => + if T = A then ([mk_Trueprop_mem (t, setA $ ta)], ctxt) else ([], ctxt)); + + val (concls, ctxt') = + if sel_rangeT = A then ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt) + else travese_nested_types (selA $ ta) ctxt; + in + if exists_subtype_in [A] sel_rangeT then + if is_refl_bool prem then (concls, ctxt') + else (map (Logic.mk_implies o pair (HOLogic.mk_Trueprop prem)) concls, ctxt') + else + ([], ctxt) + end; + val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) => + fold_map (mk_goal disc sel) setAs) discAs_selAss names_lthy); + in + if null goals then + [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) (flat sel_thmss) + set0_thms) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; + + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + + val anonymous_notes = + [(rel_eq_thms, code_attrs @ nitpicksimp_attrs)] + |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); + + val notes = + [(case_transferN, [case_transfer_thms], K []), + (ctr_transferN, ctr_transfer_thms, K []), + (disc_transferN, disc_transfer_thms, K []), + (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)), + (map_disc_iffN, map_disc_iff_thms, K simp_attrs), + (map_selN, map_sel_thms, K []), + (rel_casesN, [rel_cases_thm], K rel_cases_attrs), + (rel_distinctN, rel_distinct_thms, K simp_attrs), + (rel_injectN, rel_inject_thms, K simp_attrs), + (rel_introsN, rel_intro_thms, K []), + (rel_selN, rel_sel_thms, K []), + (setN, set_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)), + (set_casesN, set_cases_thms, nth set_cases_attrss), + (set_introsN, set_intros_thms, K []), + (set_selN, set_sel_thms, K [])] + |> massage_simple_notes fp_b_name; + + val (noted, lthy') = + lthy + |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) + |> fp = Least_FP + ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms) + |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms) + |> Local_Theory.notes (anonymous_notes @ notes); + + val subst = Morphism.thm (substitute_noted_thm noted); + in + ((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms, + map (map subst) set0_thmss), lthy') + end; + type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) = @@ -588,7 +1084,7 @@ fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = let - val B_ify = typ_subst_nonatomic (As ~~ Bs) + val B_ify = typ_subst_nonatomic (As ~~ Bs); val fpB_Ts = map B_ify fpA_Ts; val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss; val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss; @@ -1198,12 +1694,11 @@ val set_boss = map (map fst o type_args_named_constrained_of_spec) specs; val set_bss = map (map (the_default Binding.empty)) set_boss; - val ((((Bs0, Cs as C1 :: _), Es as E1 :: _), Xs), no_defs_lthy) = + val (((Bs0, Cs), Xs), no_defs_lthy) = no_defs_lthy0 |> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As |> mk_TFrees num_As ||>> mk_TFrees nn - ||>> mk_TFrees nn ||>> variant_tfrees fp_b_names; fun add_fake_type spec = @@ -1355,19 +1850,6 @@ val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; - fun massage_simple_notes base = - filter_out (null o #2) - #> map (fn (thmN, thms, f_attrs) => - ((Binding.qualify true base (Binding.name thmN), []), - map_index (fn (i, thm) => ([thm], f_attrs i)) thms)); - - val massage_multi_notes = - maps (fn (thmN, thmss, attrs) => - map3 (fn fp_b_name => fn Type (T_name, _) => fn thms => - ((Binding.qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) - fp_b_names fpTs thmss) - #> filter_out (null o fst o hd o snd); - val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; val ns = map length ctr_Tsss; val kss = map (fn n => 1 upto n) ns; @@ -1383,7 +1865,6 @@ disc_bindings), sel_bindingss), raw_sel_default_eqs) no_defs_lthy = let val fp_b_name = Binding.name_of fp_b; - val fpBT = B_ify fpT; val ctr_absT = domain_type (fastype_of ctor); @@ -1476,499 +1957,19 @@ (ctr_sugar, lthy' |> Local_Theory.notes anonymous_notes |> snd) end; - fun derive_map_set_rel_thms (ctr_sugar as {casex, case_thms, discs, selss, ctrs, exhaust, - exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss, - ...} : ctr_sugar, lthy) = - if live = 0 then - ((([], [], [], []), ctr_sugar), lthy) - else - let - val rel_flip = rel_flip_of_bnf fp_bnf; - - val live_AsBs = filter (op <>) (As ~~ Bs); - val fTs = map (op -->) live_AsBs; - val (((((fs, Rs), ta), tb), thesis), names_lthy) = names_lthy - |> mk_Frees "f" fTs - ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs) - ||>> yield_singleton (mk_Frees "a") fpT - ||>> yield_singleton (mk_Frees "b") fpBT - ||>> apfst HOLogic.mk_Trueprop o yield_singleton (mk_Frees "thesis") HOLogic.boolT; - val map_term = mk_map live As Bs (map_of_bnf fp_bnf); - val ctrAs = map (mk_ctr As) ctrs; - val ctrBs = map (mk_ctr Bs) ctrs; - val relAsBs = mk_rel live As Bs (rel_of_bnf fp_bnf); - val setAs = map (mk_set As) (sets_of_bnf fp_bnf); - val discAs = map (mk_disc_or_sel As) discs; - val discBs = map (mk_disc_or_sel Bs) discs; - val selAss = map (map (mk_disc_or_sel As)) selss; - val discAs_selAss = flat (map2 (map o pair) discAs selAss); - - val ctor_cong = - if fp = Least_FP then - Drule.dummy_thm - else - let val ctor' = mk_ctor Bs ctor in - cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong - end; - - fun mk_cIn ctor k xs = - let val absT = domain_type (fastype_of ctor) in - mk_absumprod absT abs n k xs - |> fp = Greatest_FP ? curry (op $) ctor - |> certify lthy - end; - - val cxIns = map2 (mk_cIn ctor) ks xss; - val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss; - - fun mk_map_thm ctr_def' cxIn = - fold_thms lthy [ctr_def'] - (unfold_thms lthy (o_apply :: pre_map_def :: - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ - abs_inverses) - (cterm_instantiate_pos (map (SOME o certify lthy) fs @ [SOME cxIn]) - (if fp = Least_FP then fp_map_thm - else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans)))) - |> singleton (Proof_Context.export names_lthy no_defs_lthy); - - fun mk_set0_thm fp_set_thm ctr_def' cxIn = - fold_thms lthy [ctr_def'] - (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @ - (if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @ - @{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses) - (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) - |> singleton (Proof_Context.export names_lthy no_defs_lthy); - - fun mk_set0_thms fp_set_thm = map2 (mk_set0_thm fp_set_thm) ctr_defs' cxIns; - - val map_thms = map2 mk_map_thm ctr_defs' cxIns; - val set0_thmss = map mk_set0_thms fp_set_thms; - val set0_thms = flat set0_thmss; - val set_thms = set0_thms - |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left - Un_insert_left}); - - val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); - - fun mk_rel_thm postproc ctr_defs' cxIn cyIn = - fold_thms lthy ctr_defs' - (unfold_thms lthy (pre_rel_def :: abs_inverse :: - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ - @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) - (cterm_instantiate_pos (map (SOME o certify lthy) Rs @ [SOME cxIn, SOME cyIn]) - fp_rel_thm)) - |> postproc - |> singleton (Proof_Context.export names_lthy no_defs_lthy); - - fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) = - mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn; - - fun mk_rel_intro_thm m thm = - uncurry_thm m (thm RS iffD2) handle THM _ => thm; - - fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) = - mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def'] - cxIn cyIn; - - fun mk_other_half_rel_distinct_thm thm = - flip_rels lthy live thm - RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); - - val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); - val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms; - - val half_rel_distinct_thmss = - map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos); - val other_half_rel_distinct_thmss = - map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; - val (rel_distinct_thms, _) = - join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; - - val rel_eq_thms = - map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ - map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) - rel_inject_thms ms; - - val ctr_transfer_thms = - let val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs in - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => - mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation - end; - - val (set_cases_thms, set_cases_attrss) = - let - fun mk_prems assms elem t ctxt = - (case fastype_of t of - Type (type_name, xs) => - (case bnf_of ctxt type_name of - NONE => ([], ctxt) - | SOME bnf => - apfst flat (fold_map (fn set => fn ctxt => - let - val T = HOLogic.dest_setT (range_type (fastype_of set)); - val new_var = not (T = fastype_of elem); - val (x, ctxt') = - if new_var then yield_singleton (mk_Frees "x") T ctxt - else (elem, ctxt); - in - mk_prems (mk_Trueprop_mem (x, set $ t) :: assms) elem x ctxt' - |>> map (if new_var then Logic.all x else I) - end) (map (mk_set xs) (sets_of_bnf bnf)) ctxt)) - | T => rpair ctxt - (if T = fastype_of elem then [fold (curry Logic.mk_implies) assms thesis] - else [])); - in - split_list (map (fn set => - let - val A = HOLogic.dest_setT (range_type (fastype_of set)); - val (elem, names_lthy) = yield_singleton (mk_Frees "e") A names_lthy; - val premss = - map (fn ctr => - let - val (args, names_lthy) = - mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy; - in - flat (zipper_map (fn (prev_args, arg, next_args) => - let - val (args_with_elem, args_without_elem) = - if fastype_of arg = A then - (prev_args @ [elem] @ next_args, prev_args @ next_args) - else - `I (prev_args @ [arg] @ next_args); - in - mk_prems [mk_Trueprop_eq (ta, Term.list_comb (ctr, args_with_elem))] - elem arg names_lthy - |> fst - |> map (fold_rev Logic.all args_without_elem) - end) args) - end) ctrAs; - val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis); - val thm = - Goal.prove_sorry lthy [] (flat premss) goal (fn {context = ctxt, prems} => - mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms) - |> singleton (Proof_Context.export names_lthy lthy) - |> Thm.close_derivation - |> rotate_prems ~1; - - val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); - val cases_set_attr = - Attrib.internal (K (Induct.cases_pred (name_of_set set))); - in - (* TODO: @{attributes [elim?]} *) - (thm, [consumes_attr, cases_set_attr]) - end) setAs) - end; - - val set_intros_thms = - let - fun mk_goals A setA ctr_args t ctxt = - (case fastype_of t of - Type (type_name, innerTs) => - (case bnf_of ctxt type_name of - NONE => ([], ctxt) - | SOME bnf => - apfst flat (fold_map (fn set => fn ctxt => - let - val T = HOLogic.dest_setT (range_type (fastype_of set)); - val (x, ctxt') = yield_singleton (mk_Frees "x") T ctxt; - val assm = mk_Trueprop_mem (x, set $ t); - in - apfst (map (Logic.mk_implies o pair assm)) - (mk_goals A setA ctr_args x ctxt') - end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt)) - | T => - (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt)); - - val (goals, names_lthy) = - apfst flat (fold_map (fn set => fn ctxt => - let val A = HOLogic.dest_setT (range_type (fastype_of set)) in - apfst flat (fold_map (fn ctr => fn ctxt => - let - val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt; - val ctr_args = Term.list_comb (ctr, args); - in - apfst flat (fold_map (mk_goals A set ctr_args) args ctxt') - end) ctrAs ctxt) - end) setAs lthy); - in - if null goals then [] - else - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation - end; - - val rel_sel_thms = - let - val selBss = map (map (mk_disc_or_sel Bs)) selss; - val n = length discAs; - - fun mk_conjunct n k discA selAs discB selBs = - (if k = n then [] else [HOLogic.mk_eq (discA $ ta, discB $ tb)]) @ - (if null selAs then - [] - else - [Library.foldr HOLogic.mk_imp - (if n = 1 then [] else [discA $ ta, discB $ tb], - Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs []) - (map (rapp ta) selAs) (map (rapp tb) selBs)))]); - - val goals = - if n = 0 then - [] - else - [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb, - (case flat (map5 (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of - [] => @{term True} - | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))]; - - fun prove goal = - Goal.prove_sorry lthy [] [] goal - (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 live_nesting_rel_eqs) - |> singleton (Proof_Context.export names_lthy lthy) - |> Thm.close_derivation; - in - map prove goals - end; - - val (rel_cases_thm, rel_cases_attrs) = - let - val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb; - val ctrBs = map (mk_ctr Bs) ctrs; - - fun mk_assms ctrA ctrB ctxt = - let - val argA_Ts = binder_types (fastype_of ctrA); - val argB_Ts = binder_types (fastype_of ctrB); - val ((argAs, argBs), names_ctxt) = ctxt - |> mk_Frees "x" argA_Ts - ||>> mk_Frees "y" argB_Ts; - val ctrA_args = list_comb (ctrA, argAs); - val ctrB_args = list_comb (ctrB, argBs); - in - (fold_rev Logic.all (argAs @ argBs) (Logic.list_implies - (mk_Trueprop_eq (ta, ctrA_args) :: - mk_Trueprop_eq (tb, ctrB_args) :: - map2 (HOLogic.mk_Trueprop oo build_rel_app lthy Rs []) argAs argBs, - thesis)), - names_ctxt) - end; - - val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy; - val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis); - val thm = - Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => - mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust injects - rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs) - |> singleton (Proof_Context.export names_lthy lthy) - |> Thm.close_derivation; - - val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs); - val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); - val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); - val cases_pred_attr = Attrib.internal o K o Induct.cases_pred; - in - (thm, [consumes_attr, case_names_attr, cases_pred_attr ""]) - end; - - val case_transfer_thms = - let - val (R, names_lthy) = yield_singleton (mk_Frees "R") (mk_pred2T C1 E1) names_lthy; - - val caseA = mk_case As C1 casex; - val caseB = mk_case Bs E1 casex; - val goal = mk_parametricity_goal names_lthy (R :: Rs) caseA caseB; - in - Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => - mk_case_transfer_tac ctxt rel_cases_thm case_thms) - |> singleton (Proof_Context.export names_lthy lthy) - |> Thm.close_derivation - end; - - val disc_transfer_thms = - let val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs in - if null goals then - [] - else - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (K (mk_disc_transfer_tac (the_single rel_sel_thms) (the_single exhaust_discs) - (flat (flat distinct_discsss)))) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation - end; - - val map_disc_iff_thms = - let - val discsB = map (mk_disc_or_sel Bs) discs; - val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs; - - fun mk_goal (discA_t, discB) = - if head_of discA_t aconv HOLogic.Not orelse is_refl_bool discA_t then - NONE - else - SOME (mk_Trueprop_eq - (betapply (discB, (Term.list_comb (map_term, fs) $ ta)), discA_t)); - - val goals = map_filter mk_goal (discsA_t ~~ discsB); - in - if null goals then - [] - else - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => - mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) - map_thms) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation - end; - - val map_sel_thms = - let - fun mk_goal (discA, selA) = - let - val prem = Term.betapply (discA, ta); - val selB = mk_disc_or_sel Bs selA; - val lhs = selB $ (Term.list_comb (map_term, fs) $ ta); - val lhsT = fastype_of lhs; - val map_rhsT = - map_atyps (perhaps (AList.lookup (op =) (map swap live_AsBs))) lhsT; - val map_rhs = build_map lthy [] - (the o (AList.lookup (op =) (live_AsBs ~~ fs))) (map_rhsT, lhsT); - val rhs = (case map_rhs of - Const (@{const_name id}, _) => selA $ ta - | _ => map_rhs $ (selA $ ta)); - val concl = mk_Trueprop_eq (lhs, rhs); - in - if is_refl_bool prem then concl - else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl) - end; - - val goals = map mk_goal discAs_selAss; - in - if null goals then - [] - else - 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) live_nesting_map_id0s) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation - end; - - val set_sel_thms = - let - fun mk_goal discA selA setA ctxt = - let - val prem = Term.betapply (discA, ta); - val sel_rangeT = range_type (fastype_of selA); - val A = HOLogic.dest_setT (range_type (fastype_of setA)); - - fun travese_nested_types t ctxt = - (case fastype_of t of - Type (type_name, innerTs) => - (case bnf_of ctxt type_name of - NONE => ([], ctxt) - | SOME bnf => - let - fun seq_assm a set ctxt = - let - val T = HOLogic.dest_setT (range_type (fastype_of set)); - val (x, ctxt') = yield_singleton (mk_Frees "x") T ctxt; - val assm = mk_Trueprop_mem (x, set $ a); - in - travese_nested_types x ctxt' - |>> map (Logic.mk_implies o pair assm) - end; - in - fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt - |>> flat - end) - | T => - if T = A then ([mk_Trueprop_mem (t, setA $ ta)], ctxt) else ([], ctxt)); - - val (concls, ctxt') = - if sel_rangeT = A then ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt) - else travese_nested_types (selA $ ta) ctxt; - in - if exists_subtype_in [A] sel_rangeT then - if is_refl_bool prem then - (concls, ctxt') - else - (map (Logic.mk_implies o pair (HOLogic.mk_Trueprop prem)) concls, ctxt') - else - ([], ctxt) - end; - val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) => - fold_map (mk_goal disc sel) setAs) discAs_selAss names_lthy); - in - if null goals then - [] - else - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => - mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) - (flat sel_thmss) set0_thms) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation - end; - - val anonymous_notes = - [(rel_eq_thms, code_attrs @ nitpicksimp_attrs)] - |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); - - val notes = - [(case_transferN, [case_transfer_thms], K []), - (ctr_transferN, ctr_transfer_thms, K []), - (disc_transferN, disc_transfer_thms, K []), - (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)), - (map_disc_iffN, map_disc_iff_thms, K simp_attrs), - (map_selN, map_sel_thms, K []), - (rel_casesN, [rel_cases_thm], K rel_cases_attrs), - (rel_distinctN, rel_distinct_thms, K simp_attrs), - (rel_injectN, rel_inject_thms, K simp_attrs), - (rel_introsN, rel_intro_thms, K []), - (rel_selN, rel_sel_thms, K []), - (setN, set_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)), - (set_casesN, set_cases_thms, nth set_cases_attrss), - (set_introsN, set_intros_thms, K []), - (set_selN, set_sel_thms, K [])] - |> massage_simple_notes fp_b_name; - - val (noted, lthy') = - lthy - |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) - |> fp = Least_FP - ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms) - |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms) - |> Local_Theory.notes (anonymous_notes @ notes); - - val subst = Morphism.thm (substitute_noted_thm noted); - in - (((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms, - map (map subst) set0_thmss), ctr_sugar), lthy') - end; - fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); - fun massage_res (((maps_sets_rels, ctr_sugar), co_rec_res), lthy) = + fun massage_res (((ctr_sugar, maps_sets_rels), co_rec_res), lthy) = (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy); in (wrap_ctrs - #> derive_map_set_rel_thms + #> (fn (ctr_sugar, lthy) => + derive_map_set_rel_thms names_lthy plugins fp live As Bs abs_inverses ctr_defs' + live_nesting_rel_eqs xss yss fp_nesting_set_maps live_nesting_set_maps + live_nesting_map_id0s fp_b_name fp_bnf fpT ctor ctor_dtor dtor_ctor pre_map_def + pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms abs abs_inverse + ctr_sugar lthy + |>> pair ctr_sugar) ##>> (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec @@ -2027,7 +2028,7 @@ (recN, rec_thmss, K rec_attrs), (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])), (simpsN, simp_thmss, K [])] - |> massage_multi_notes; + |> massage_multi_notes fp_b_names fpTs; in lthy |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss) @@ -2121,7 +2122,7 @@ (corec_selN, corec_sel_thmss, K corec_sel_attrs), (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])), (simpsN, simp_thmss, K [])] - |> massage_multi_notes; + |> massage_multi_notes fp_b_names fpTs; in lthy |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)