# HG changeset patch # User blanchet # Date 1378727278 -7200 # Node ID 185ad6cf65765ae50907b189bbc5831d17763a80 # Parent 077a2758ceb4b1c08ee72f41f4c1307e37fb73ae enriched data structure with necessary theorems diff -r 077a2758ceb4 -r 185ad6cf6576 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Sun Sep 08 19:25:06 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 09 13:47:58 2013 +0200 @@ -23,7 +23,11 @@ split_asm: thm, disc_thmss: thm list list, discIs: thm list, - sel_thmss: thm list list}; + sel_thmss: thm list list, + disc_exhausts: thm list, + collapses: thm list, + expands: thm list, + case_convs: thm list}; val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar @@ -68,10 +72,15 @@ split_asm: thm, disc_thmss: thm list list, discIs: thm list, - sel_thmss: thm list list}; + sel_thmss: thm list list, + disc_exhausts: thm list, + collapses: thm list, + expands: thm list, + case_convs: thm list}; fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, - case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss} = + case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, + disc_exhausts, collapses, expands, case_convs} = {ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, @@ -87,7 +96,11 @@ split_asm = Morphism.thm phi split_asm, disc_thmss = map (map (Morphism.thm phi)) disc_thmss, discIs = map (Morphism.thm phi) discIs, - sel_thmss = map (map (Morphism.thm phi)) sel_thmss}; + sel_thmss = map (map (Morphism.thm phi)) sel_thmss, + disc_exhausts = map (Morphism.thm phi) disc_exhausts, + collapses = map (Morphism.thm phi) collapses, + expands = map (Morphism.thm phi) expands, + case_convs = map (Morphism.thm phi) case_convs}; val rep_compat_prefix = "new"; @@ -762,7 +775,8 @@ nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm, split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss, - discIs = discI_thms, sel_thmss = sel_thmss}, + discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms, + collapses = collapse_thms, expands = expand_thms, case_convs = case_conv_thms}, lthy |> not rep_compat ? (Local_Theory.declaration {syntax = false, pervasive = true} diff -r 077a2758ceb4 -r 185ad6cf6576 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Sun Sep 08 19:25:06 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 09 13:47:58 2013 +0200 @@ -19,7 +19,9 @@ ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, co_iterss: term list list, co_inducts: thm list, - co_iter_thmsss: thm list list list}; + co_iter_thmsss: thm list list list, + disc_co_itersss: thm list list list, + sel_co_iterssss: thm list list list list}; val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar @@ -80,7 +82,7 @@ * (thm list list * thm list list * Args.src list) * (thm list list * thm list list) * (thm list list * thm list list * Args.src list) * (thm list list * thm list list * Args.src list) - * (thm list list * thm list list * Args.src list) + * (thm list list list * thm list list list * Args.src list) val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> @@ -119,7 +121,9 @@ ctr_sugars: ctr_sugar list, co_iterss: term list list, co_inducts: thm list, - co_iter_thmsss: thm list list list}; + co_iter_thmsss: thm list list list, + disc_co_itersss: thm list list list, + sel_co_iterssss: thm list list list list}; fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index; @@ -128,7 +132,7 @@ T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss, - ctr_sugars, co_iterss, co_inducts, co_iter_thmsss} = + ctr_sugars, co_iterss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} = {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs, fp_res = morph_fp_result phi fp_res, @@ -136,7 +140,9 @@ ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, co_iterss = map (map (Morphism.term phi)) co_iterss, co_inducts = map (Morphism.thm phi) co_inducts, - co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss}; + co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss, + disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss, + sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss}; structure Data = Generic_Data ( @@ -161,13 +167,14 @@ (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar))); fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss - ctr_sugars co_iterss co_inducts co_iter_thmsss lthy = + ctr_sugars co_iterss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy = (0, lthy) |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, - co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss} + co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss, + sel_co_iterssss = sel_co_iterssss} lthy)) Ts |> snd; @@ -999,10 +1006,10 @@ end; fun mk_sel_coiter_thms coiter_thmss = - map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss |> map flat; + map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss; - val sel_unfold_thmss = mk_sel_coiter_thms unfold_thmss; - val sel_corec_thmss = mk_sel_coiter_thms corec_thmss; + val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss; + val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss; val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases)); @@ -1018,7 +1025,7 @@ (safe_unfold_thmss, safe_corec_thmss), (disc_unfold_thmss, disc_corec_thmss, simp_attrs), (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs), - (sel_unfold_thmss, sel_corec_thmss, simp_attrs)) + (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs)) end; fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp @@ -1435,7 +1442,7 @@ lthy |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars - iterss [induct_thm] (transpose [fold_thmss, rec_thmss]) + iterss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] [] end; fun derive_and_note_coinduct_coiters_thms_for_types @@ -1448,11 +1455,14 @@ (safe_unfold_thmss, safe_corec_thmss), (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs), (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs), - (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) = + (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) = derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy; + val sel_unfold_thmss = map flat sel_unfold_thmsss; + val sel_corec_thmss = map flat sel_corec_thmsss; + val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; fun flat_coiter_thms coiters disc_coiters sel_coiters = @@ -1495,7 +1505,8 @@ |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm] - (transpose [unfold_thmss, corec_thmss]) + (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss]) + (transpose [sel_unfold_thmsss, sel_corec_thmsss]) end; val lthy'' = lthy' diff -r 077a2758ceb4 -r 185ad6cf6576 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Sun Sep 08 19:25:06 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Sep 09 13:47:58 2013 +0200 @@ -145,19 +145,23 @@ val ctr_sugars = map inst_ctr_sugar ctr_sugars0; - val (co_inducts, un_fold_thmss, co_rec_thmss) = + val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss, + sel_unfold_thmsss, sel_corec_thmsss) = if fp = Least_FP then derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss co_iterss co_iter_defss lthy |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) => - ([induct], fold_thmss, rec_thmss)) + ([induct], fold_thmss, rec_thmss, [], [], [], [])) else derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy - |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) => - (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss)); + |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, + (disc_unfold_thmss, disc_corec_thmss, _), + (sel_unfold_thmsss, sel_corec_thmsss, _)) => + (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss, + disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss)); val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0; @@ -165,7 +169,9 @@ {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss, - co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]} + co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss], + disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss], + sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]} |> morph_fp_sugar phi; in ((true, map_index mk_target_fp_sugar fpTs), lthy) diff -r 077a2758ceb4 -r 185ad6cf6576 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Sun Sep 08 19:25:06 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Sep 09 13:47:58 2013 +0200 @@ -31,7 +31,10 @@ sels: term list, pred: int option, calls: corec_call list, - corec_thm: thm} + collapse: thm, + corec_thm: thm, + disc_corec: thm, + sel_corecs: thm list} type rec_spec = {recx: term, @@ -41,6 +44,9 @@ type corec_spec = {corec: term, + nested_maps: thm list, + nested_map_idents: thm list, + nested_map_comps: thm list, ctr_specs: corec_ctr_spec list} val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> @@ -90,7 +96,10 @@ sels: term list, pred: int option, calls: corec_call list, - corec_thm: thm}; + collapse: thm, + corec_thm: thm, + disc_corec: thm, + sel_corecs: thm list}; type rec_spec = {recx: term, @@ -100,6 +109,9 @@ type corec_spec = {corec: term, + nested_maps: thm list, + nested_map_idents: thm list, + nested_map_comps: thm list, ctr_specs: corec_ctr_spec list}; val id_def = @{thm id_def}; @@ -348,7 +360,7 @@ val thy = Proof_Context.theory_of lthy; val ((nontriv, missing_res_Ts, perm0_kks, - fp_sugars as {fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, + fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, co_inducts = coinduct_thms, ...} :: _), lthy') = nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy; @@ -407,27 +419,38 @@ else No_Corec) g_i | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i'); - fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss corec_thm = + fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs = let val nullary = not (can dest_funT (fastype_of ctr)) in {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho, - calls = map3 (call_of nullary) q_iss f_iss f_Tss, corec_thm = corec_thm} + calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse, + corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs} end; - fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss = + fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss + sel_coiterssss = let val ctrs = #ctrs (nth ctr_sugars index); val discs = #discs (nth ctr_sugars index); val selss = #selss (nth ctr_sugars index); val p_ios = map SOME p_is @ [NONE]; - val corec_thmss = co_rec_of (nth coiter_thmsss index); + val collapses = #collapses (nth ctr_sugars index); + val corec_thms = co_rec_of (nth coiter_thmsss index); + val disc_corecs = co_rec_of (nth disc_coitersss index); + val sel_corecss = co_rec_of (nth sel_coiterssss index); in - map8 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss corec_thmss + map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms + disc_corecs sel_corecss end; - fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, ...} + fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, + disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} p_is q_isss f_isss f_Tsss = {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)), - ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss}; + nested_maps = [] (*FIXME*), + nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs, + nested_map_comps = map map_comp_of_bnf nested_bnfs, + ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss + disc_coitersss sel_coiterssss}; in ((nontriv, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,