# HG changeset patch # User blanchet # Date 1444149571 -7200 # Node ID ebf296fe88d7f3d4d0858487674a09946ee97972 # Parent 5b5656a63bd601736cea974e49a2e0d6a6b18804 generate 'case_transfer' unconditionally diff -r 5b5656a63bd6 -r ebf296fe88d7 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 06 17:47:28 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 06 18:39:31 2015 +0200 @@ -560,342 +560,413 @@ b_names Ts thmss) #> filter_out (null o fst o hd o snd); -fun derive_map_set_rel_thms plugins fp live As Bs abs_inverses ctr_defs' fp_nesting_set_maps +fun derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs' fp_nesting_set_maps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs 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 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 = - if live = 0 then - (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy) - else - let - val n = length ctr_Tss; - val ks = 1 upto n; - val ms = map length ctr_Tss; - - val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); - - val fpBT = B_ify_T fpT; - val live_AsBs = filter (op <>) (As ~~ Bs); - val fTs = map (op -->) live_AsBs; - - val (((((((([C, E], xss), yss), fs), Rs), ta), tb), thesis), names_lthy) = lthy - |> fold (fold Variable.declare_typ) [As, Bs] - |> mk_TFrees 2 - ||>> mk_Freess "x" ctr_Tss - ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss) - ||>> 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 selBss = map (map (mk_disc_or_sel Bs)) selss; - - val ctor_cong = - if fp = Least_FP then - Drule.dummy_thm - else - let val ctor' = mk_ctor Bs ctor in - infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctor')] arg_cong + let + val n = length ctr_Tss; + val ks = 1 upto n; + val ms = map length ctr_Tss; + + val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); + + val fpBT = B_ify_T fpT; + val live_AsBs = filter (op <>) (As ~~ Bs); + val fTs = map (op -->) live_AsBs; + + val (((((((xss, yss), fs), Rs), ta), tb), thesis), names_lthy) = lthy + |> fold (fold Variable.declare_typ) [As, Bs] + |> mk_Freess "x" ctr_Tss + ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss) + ||>> 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 ctrAs = map (mk_ctr As) ctrs; + val ctrBs = map (mk_ctr Bs) ctrs; + + fun derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms = + let + val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb; + + 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_map 2} mk_assms ctrAs ctrBs names_lthy; + val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis); + in + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + mk_rel_cases_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of 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 + end; + + fun derive_case_transfer rel_cases_thm = + let + val (S, names_lthy) = yield_singleton (mk_Frees "S") (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 (S :: 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; + in + if live = 0 then + let + val relAsBs = HOLogic.eq_const fpT; + val rel_cases_thm = derive_rel_cases relAsBs [] []; + + val case_transfer_thm = derive_case_transfer rel_cases_thm; + + val notes = + [(case_transferN, [case_transfer_thm], K [])] + |> massage_simple_notes fp_b_name; + + val (noted, lthy') = lthy + |> Local_Theory.notes notes; + + val subst = Morphism.thm (substitute_noted_thm noted); + in + (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []), + lthy') + end + else + let + val mapx = mk_map live As Bs (map_of_bnf fp_bnf); + 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 selBss = map (map (mk_disc_or_sel Bs)) selss; + + val ctor_cong = + if fp = Least_FP then + Drule.dummy_thm + else + let val ctor' = mk_ctor Bs ctor in + infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of 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 + |> Thm.cterm_of lthy 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 - |> Thm.cterm_of lthy - end; - - val cxIns = map2 (mk_cIn ctor) ks xss; - val cyIns = map2 (mk_cIn (Term.map_types B_ify_T 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) - (infer_instantiate' lthy (map (SOME o Thm.cterm_of 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) - (infer_instantiate' lthy [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_inverses @ - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ - @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) - (infer_instantiate' lthy (map (SOME o Thm.cterm_of 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_code_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; - val goal = Logic.mk_conjunction_balanced goals; - val vars = Variable.add_free_names lthy goal []; - in - Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => - mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs) - |> Thm.close_derivation - |> Conjunction.elim_balanced (length goals) - 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 => + val cxIns = map2 (mk_cIn ctor) ks xss; + val cyIns = map2 (mk_cIn (Term.map_types B_ify_T 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) + (infer_instantiate' lthy (map (SOME o Thm.cterm_of 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) + (infer_instantiate' lthy [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_inverses @ + (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ + @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) + (infer_instantiate' lthy (map (SOME o Thm.cterm_of 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_code_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; + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => + mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs) + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + 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 vars = Variable.add_free_names lthy goal []; + val thm = + Goal.prove_sorry lthy vars (flat premss) goal (fn {context = ctxt, prems} => + mk_set_cases_tac ctxt (Thm.cterm_of ctxt ta) prems exhaust set_thms) + |> 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))); + + val ctr_names = quasi_unambiguous_case_names (flat + (map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs))); + val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); + in + (* TODO: @{attributes [elim?]} *) + (thm, [consumes_attr, cases_set_attr, case_names_attr]) + end) setAs) + end; + + val (set_intros_thmssss, 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 (goalssss, _) = + fold_map (fn set => + let val A = HOLogic.dest_setT (range_type (fastype_of set)) in + fold_map (fn ctr => fn ctxt => + let val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt in + fold_map (mk_goals A set (Term.list_comb (ctr, args))) args ctxt' + end) ctrAs + end) setAs lthy; + val goals = flat (flat (flat goalssss)); + in + `(fst o unflattt goalssss) + (if null goals then [] + else + let + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms) + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end) + end; + + val rel_sel_thms = + let + 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 (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of + [] => @{term True} + | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))]; + + fun prove goal = + Variable.add_free_names lthy goal [] + |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => + mk_rel_sel_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust + (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts rel_distinct_thms + live_nesting_rel_eqs)) + |> Thm.close_derivation; + in + map prove goals + end; + + val (rel_cases_thm, rel_cases_attrs) = + let + val thm = derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms; + 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_thm = derive_case_transfer rel_cases_thm; + + val sel_transfer_thms = + if null selAss then [] + else 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 vars = Variable.add_free_names lthy goal []; - val thm = - Goal.prove_sorry lthy vars (flat premss) goal (fn {context = ctxt, prems} => - mk_set_cases_tac ctxt (Thm.cterm_of ctxt ta) prems exhaust set_thms) - |> 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))); - - val ctr_names = quasi_unambiguous_case_names (flat - (map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs))); - val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); + val shared_sels = foldl1 (uncurry (inter (op =))) (map (op ~~) (selAss ~~ selBss)); + val goals = map (uncurry (mk_parametricity_goal names_lthy Rs)) shared_sels; in - (* TODO: @{attributes [elim?]} *) - (thm, [consumes_attr, cases_set_attr, case_names_attr]) - end) setAs) - end; - - val (set_intros_thmssss, 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 (goalssss, _) = - fold_map (fn set => - let val A = HOLogic.dest_setT (range_type (fastype_of set)) in - fold_map (fn ctr => fn ctxt => - let val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt in - fold_map (mk_goals A set (Term.list_comb (ctr, args))) args ctxt' - end) ctrAs - end) setAs lthy; - val goals = flat (flat (flat goalssss)); - in - `(fst o unflattt goalssss) - (if null goals then [] - else - let - val goal = Logic.mk_conjunction_balanced goals; - val vars = Variable.add_free_names lthy goal []; - in - Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms) - |> Thm.close_derivation - |> Conjunction.elim_balanced (length goals) - end) - end; - - val rel_sel_thms = - let - 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 [] + if null goals then [] + else + let + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => + mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm) + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end + end; + + val disc_transfer_thms = + let val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs in + if null goals then + [] else - [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb, - (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of - [] => @{term True} - | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))]; - - fun prove goal = - Variable.add_free_names lthy goal [] - |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_rel_sel_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust (flat disc_thmss) - (flat sel_thmss) rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)) - |> 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, _) = @{fold_map 2} mk_assms ctrAs ctrBs names_lthy; - val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis); - val vars = Variable.add_free_names lthy goal []; - val thm = - Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_rel_cases_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects - rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs) - |> 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_thm = - let - val (S, _) = yield_singleton (mk_Frees "S") (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 (S :: Rs) caseA caseB; - val vars = Variable.add_free_names lthy goal []; - in - Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_case_transfer_tac ctxt rel_cases_thm case_thms) - |> Thm.close_derivation - end; - - val sel_transfer_thms = - if null selAss then [] - else + let + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt + (the_single rel_sel_thms) (the_single exhaust_discs) + (flat (flat distinct_discsss))) + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end + end; + + val map_disc_iff_thms = let - val shared_sels = foldl1 (uncurry (inter (op =))) (map (op ~~) (selAss ~~ selBss)); - val goals = map (uncurry (mk_parametricity_goal names_lthy Rs)) shared_sels; + 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 [] + if null goals then + [] else let val goal = Logic.mk_conjunction_balanced goals; @@ -903,211 +974,167 @@ in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm) + mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) + map_thms) |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) end end; - val disc_transfer_thms = - let val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs in - if null goals then - [] - else - let - val goal = Logic.mk_conjunction_balanced goals; - val vars = Variable.add_free_names lthy goal []; - in - Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt (the_single rel_sel_thms) - (the_single exhaust_discs) (flat (flat distinct_discsss))) - |> Thm.close_derivation - |> Conjunction.elim_balanced (length goals) - end - 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 - let - val goal = Logic.mk_conjunction_balanced goals; - val vars = Variable.add_free_names lthy goal []; - in - Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => - mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms) - |> Thm.close_derivation - |> Conjunction.elim_balanced (length goals) - end - end; - - val (map_sel_thmss, map_sel_thms) = - let - fun mk_goal discA selA selB = - let - val prem = Term.betapply (discA, ta); - 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 goalss = @{map 3} (map2 o mk_goal) discAs selAss selBss; - val goals = flat goalss; - in - `(fst o unflat goalss) - (if null goals then [] - else + val (map_sel_thmss, map_sel_thms) = + let + fun mk_goal discA selA selB = let - val goal = Logic.mk_conjunction_balanced goals; - val vars = Variable.add_free_names lthy goal []; + val prem = Term.betapply (discA, ta); + 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 goalss = @{map 3} (map2 o mk_goal) discAs selAss selBss; + val goals = flat goalss; + in + `(fst o unflat goalss) + (if null goals then [] + else + let + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => + mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms + (flat sel_thmss) live_nesting_map_id0s) + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end) + end; + + val (set_sel_thmssss, set_sel_thms) = + let + fun mk_goal setA discA selA 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 - Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => - mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms - (flat sel_thmss) live_nesting_map_id0s) - |> Thm.close_derivation - |> Conjunction.elim_balanced (length goals) - end) - end; - - val (set_sel_thmssss, set_sel_thms) = - let - fun mk_goal setA discA selA 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') + 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 (goalssss, _) = + fold_map (fn set => @{fold_map 2} (fold_map o mk_goal set) discAs selAss) + setAs names_lthy; + val goals = flat (flat (flat goalssss)); + in + `(fst o unflattt goalssss) + (if null goals then [] else - ([], ctxt) - end; - - val (goalssss, _) = - fold_map (fn set => @{fold_map 2} (fold_map o mk_goal set) discAs selAss) - setAs names_lthy; - val goals = flat (flat (flat goalssss)); - in - `(fst o unflattt goalssss) - (if null goals then [] - else - let - val goal = Logic.mk_conjunction_balanced goals; - val vars = Variable.add_free_names lthy goal []; - in - Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => - mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) - (flat sel_thmss) set0_thms) - |> Thm.close_derivation - |> Conjunction.elim_balanced (length goals) - end) - end; - - val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; - - val anonymous_notes = - [(rel_code_thms, code_attrs @ nitpicksimp_attrs)] - |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); - - val notes = - [(case_transferN, [case_transfer_thm], K []), - (ctr_transferN, ctr_transfer_thms, K []), - (disc_transferN, disc_transfer_thms, K []), - (sel_transferN, sel_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_code_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 map_disc_iff_thms, - map (map subst) map_sel_thmss, - map subst rel_inject_thms, - map subst rel_distinct_thms, - map subst rel_sel_thms, - map subst rel_intro_thms, - [subst rel_cases_thm], - map subst set_thms, - map (map (map (map subst))) set_sel_thmssss, - map (map (map (map subst))) set_intros_thmssss, - map subst set_cases_thms, - map subst ctr_transfer_thms, - [subst case_transfer_thm], - map subst disc_transfer_thms, - map subst sel_transfer_thms), lthy') - end; + let + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => + mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) + (flat sel_thmss) set0_thms) + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end) + end; + + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + + val anonymous_notes = + [(rel_code_thms, code_attrs @ nitpicksimp_attrs)] + |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); + + val notes = + [(case_transferN, [case_transfer_thm], K []), + (ctr_transferN, ctr_transfer_thms, K []), + (disc_transferN, disc_transfer_thms, K []), + (sel_transferN, sel_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_code_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 map_disc_iff_thms, + map (map subst) map_sel_thmss, + map subst rel_inject_thms, + map subst rel_distinct_thms, + map subst rel_sel_thms, + map subst rel_intro_thms, + [subst rel_cases_thm], + map subst set_thms, + map (map (map (map subst))) set_sel_thmssss, + map (map (map (map subst))) set_intros_thmssss, + map subst set_cases_thms, + map subst ctr_transfer_thms, + [subst case_transfer_thm], + map subst disc_transfer_thms, + map subst sel_transfer_thms), lthy') + end + end; type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); @@ -1154,8 +1181,7 @@ val x_Tsss' = map (map flat_rec_arg_args) x_Tssss; val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css; - val ((fss, xssss), lthy) = - lthy + val ((fss, xssss), lthy) = lthy |> mk_Freess "f" f_Tss ||>> mk_Freessss "x" x_Tssss; in @@ -1196,8 +1222,7 @@ val (q_Tssss, g_Tsss, g_Tssss, corec_types) = mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts; - val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = - lthy + val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = lthy |> yield_singleton (mk_Frees "x") dummyT ||>> mk_Frees "a" Cs ||>> mk_Freess "p" p_Tss @@ -1367,8 +1392,7 @@ val fp_b_names = map base_name_of_typ fpTs; - val ((((ps, ps'), xsss), us'), names_lthy) = - lthy + val ((((ps, ps'), xsss), us'), names_lthy) = lthy |> mk_Frees' "P" (map mk_pred1T fpTs) ||>> mk_Freesss "x" ctr_Tsss ||>> Variable.variant_fixes fp_b_names; @@ -1747,8 +1771,7 @@ val discIss = map #discIs ctr_sugars; val sel_thmsss = map #sel_thmss ctr_sugars; - val (((rs, us'), vs'), _) = - lthy + val (((rs, us'), vs'), _) = lthy |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) ||>> Variable.variant_fixes fp_b_names ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); @@ -2148,9 +2171,9 @@ val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') = mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; - fun define_ctrs_dtrs_for_type fp ((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor), - xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), - pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs), + fun define_ctrs_dtrs_for_type fp ((((((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), E), ctor), + dtor), xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), + pre_set_defs), pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs), abs_inject), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_default_eqs) no_defs_lthy = let @@ -2252,7 +2275,7 @@ in (wrap_ctrs #> (fn (ctr_sugar, lthy) => - derive_map_set_rel_thms plugins fp live As Bs abs_inverses ctr_defs' + derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs' fp_nesting_set_maps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs 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 ctr_Tss abs ctr_sugar lthy @@ -2619,9 +2642,9 @@ val lthy'' = lthy' |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs - |> fold_map (define_ctrs_dtrs_for_type fp) (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ - xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~ - pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rels ~~ ns ~~ kss ~~ mss ~~ + |> fold_map (define_ctrs_dtrs_for_type fp) (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ Es ~~ ctors ~~ + dtors ~~ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ + pre_set_defss ~~ pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rels ~~ ns ~~ kss ~~ mss ~~ abss ~~ abs_injects ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss) |> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types diff -r 5b5656a63bd6 -r ebf296fe88d7 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 06 17:47:28 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 06 18:39:31 2015 +0200 @@ -40,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_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> + val mk_rel_cases_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 -> thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> @@ -405,19 +405,20 @@ unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN ALLGOALS (rtac ctxt refl); -fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs= +fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN - unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6) - True_implies_equals conj_imp_eq_imp_imp} @ + unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ + @{thms conj_imp_eq_imp_imp simp_thms(6) True_implies_equals} @ map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @ map (fn thm => thm RS eqTrueI) rel_injects) THEN TRYALL (assume_tac ctxt ORELSE' etac ctxt FalseE ORELSE' - (REPEAT_DETERM o dtac ctxt @{thm meta_spec} THEN' + (REPEAT_DETERM o dtac ctxt meta_spec THEN' TRY o filter_prems_tac ctxt (forall (curry (op <>) (HOLogic.mk_Trueprop @{term False})) o Logic.strip_imp_prems) THEN' - REPEAT_DETERM o (dtac ctxt @{thm meta_mp} THEN' rtac ctxt refl) THEN' Goal.assume_rule_tac ctxt)); + REPEAT_DETERM o (dtac ctxt meta_mp THEN' rtac ctxt refl) THEN' + (assume_tac ctxt ORELSE' Goal.assume_rule_tac ctxt))); fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =