# HG changeset patch # User traytel # Date 1443214894 -7200 # Node ID f49644098959b0f2e6410234c4b4a1b38b99ccce # Parent 0478ba10152a2ae19fa33954945ae90924eee676 restructure fresh variable generation to make exports more wellformed diff -r 0478ba10152a -r f49644098959 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:01:31 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:01:34 2015 +0200 @@ -157,41 +157,18 @@ val sum_bdT = fst (dest_relT (fastype_of sum_bd)); val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []); - val ((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')), - Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy), - self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), - (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), names_lthy) = lthy + val ((((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), xFs), yFs), yFs_copy), + names_lthy) = + lthy |> mk_Frees' "b" activeAs - ||>> mk_Frees "b" activeAs - ||>> mk_Frees "b" activeAs - ||>> mk_Frees "b" activeBs - ||>> mk_Frees' "y" passiveAs ||>> mk_Frees "B" BTs - ||>> mk_Frees "B" BTs - ||>> mk_Frees "B'" B'Ts - ||>> mk_Frees "B''" B''Ts ||>> mk_Frees "s" sTs - ||>> mk_Frees "sums" sum_sTs - ||>> mk_Frees "s'" s'Ts - ||>> mk_Frees "s''" s''Ts - ||>> mk_Frees "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "f" self_fTs - ||>> mk_Frees "g" gTs ||>> mk_Frees "g" all_gTs ||>> mk_Frees "x" FTsAs ||>> mk_Frees "y" FTsBs - ||>> mk_Frees "y" FTsBs - ||>> mk_Frees "x" FRTs - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT - ||>> mk_Frees "R" setRTs - ||>> mk_Frees "R" setRTs - ||>> mk_Frees "R'" setR'Ts - ||>> mk_Frees "R" setsRTs - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") idxT - ||>> yield_singleton (mk_Frees "I") (HOLogic.mk_setT idxT) - ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs); + ||>> mk_Frees "y" FTsBs; val passive_UNIVs = map HOLogic.mk_UNIV passiveAs; val passive_eqs = map HOLogic.eq_const passiveAs; @@ -320,6 +297,14 @@ Term.list_comb (Const (coalg, coalgT), args) end; + val((((((zs, zs'), Bs), B's), ss), s's), names_lthy) = + lthy + |> mk_Frees' "b" activeAs + ||>> mk_Frees "B" BTs + ||>> mk_Frees "B'" B'Ts + ||>> mk_Frees "s" sTs + ||>> mk_Frees "s'" s'Ts; + val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss); val coalg_in_thms = map (fn i => @@ -400,6 +385,25 @@ Term.list_comb (Const (mor, morT), args) end; + val (((((((((((((((zs, z's), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), + fs_copy), gs), RFs), Rs), names_lthy) = + lthy + |> mk_Frees "b" activeAs + ||>> mk_Frees "b" activeBs + ||>> mk_Frees "B" BTs + ||>> mk_Frees "B" BTs + ||>> mk_Frees "B'" B'Ts + ||>> mk_Frees "B''" B''Ts + ||>> mk_Frees "s" sTs + ||>> mk_Frees "sums" sum_sTs + ||>> mk_Frees "s'" s'Ts + ||>> mk_Frees "s''" s''Ts + ||>> mk_Frees "f" fTs + ||>> mk_Frees "f" fTs + ||>> mk_Frees "g" gTs + ||>> mk_Frees "x" FRTs + ||>> mk_Frees "R" setRTs; + val mor_prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs); val (mor_image_thms, morE_thms) = @@ -550,6 +554,27 @@ Term.list_comb (Const (bis, bisT), args) end; + val (((((((((((((((((zs, z's), Bs), B's), B''s), ss), s's), s''s), fs), (Rtuple, Rtuple')), Rs), + Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), names_lthy) = + lthy + |> mk_Frees "b" activeAs + ||>> mk_Frees "b" activeBs + ||>> mk_Frees "B" BTs + ||>> mk_Frees "B'" B'Ts + ||>> mk_Frees "B''" B''Ts + ||>> mk_Frees "s" sTs + ||>> mk_Frees "s'" s'Ts + ||>> mk_Frees "s''" s''Ts + ||>> mk_Frees "f" fTs + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT + ||>> mk_Frees "R" setRTs + ||>> mk_Frees "R" setRTs + ||>> mk_Frees "R'" setR'Ts + ||>> mk_Frees "R" setsRTs + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") idxT + ||>> yield_singleton (mk_Frees "I") (HOLogic.mk_setT idxT) + ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs); + val bis_cong_thm = let val prems = map HOLogic.mk_Trueprop @@ -640,8 +665,6 @@ fun mk_sbis Bs ss Rs = mk_bis Bs ss Bs ss Rs; - val sbis_prem = HOLogic.mk_Trueprop (mk_sbis Bs ss sRs); - (* largest self-bisimulation *) val lsbis_binds = mk_internal_bs lsbisN; @@ -679,6 +702,16 @@ Term.list_comb (Const (nth lsbiss (i - 1), lsbisT), args) end; + val (((((zs, zs'), Bs), ss), sRs), names_lthy) = + lthy + |> mk_Frees' "b" activeAs + ||>> mk_Frees "B" BTs + ||>> mk_Frees "s" sTs + ||>> mk_Frees "R" setsRTs; + + val sbis_prem = HOLogic.mk_Trueprop (mk_sbis Bs ss sRs); + val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss); + val sbis_lsbis_thm = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks))) (fn {context = ctxt, prems = _} => @@ -800,10 +833,15 @@ Term.absfree z' (mk_InN activeAs z i)) ks zs zs'); val rv_recT = fastype_of Nil; - val (((((((((((sumx, sumx'), (kks, kks')), (kl, kl')), (kl_copy, kl'_copy)), (Kl, Kl')), - (lab, lab')), (Kl_lab, Kl_lab')), xs), (Lev_rec, Lev_rec')), (rv_rec, rv_rec')), - names_lthy) = names_lthy - |> yield_singleton (apfst (op ~~) oo mk_Frees' "sumx") sum_sbdT + val (((((((((((((((zs, zs'), zs_copy), ss), (nat, nat')), + (sumx, sumx')), (kks, kks')), (kl, kl')), (kl_copy, kl'_copy)), (Kl, Kl')), (lab, lab')), + (Kl_lab, Kl_lab')), xs), (Lev_rec, Lev_rec')), (rv_rec, rv_rec')), _) = + lthy + |> mk_Frees' "b" activeAs + ||>> mk_Frees "b" activeAs + ||>> mk_Frees "s" sTs + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "sumx") sum_sbdT ||>> mk_Frees' "k" sbdTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT @@ -1093,6 +1131,15 @@ Term.list_comb (Const (nth behs (i - 1), behT), ss) end; + val ((((((zs, zs_copy), zs_copy2), ss), (nat, nat')), (kl, kl')), names_lthy) = + lthy + |> mk_Frees "b" activeAs + ||>> mk_Frees "b" activeAs + ||>> mk_Frees "b" activeAs + ||>> mk_Frees "s" sTs + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT; + val (length_Lev_thms, length_Lev'_thms) = let fun mk_conjunct i z = HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), @@ -1326,21 +1373,11 @@ HOLogic.mk_tuple (map (fn U => absdummy U empty) Ts)) emptys; val hrecTs = map fastype_of Zeros; - val (((((((((((((Jzs, Jzs'), Jz's), Jzs_copy), Jz's_copy), Jzs1), Jzs2), - TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss), (hrecs, hrecs')), - names_lthy) = names_lthy - |> mk_Frees' "z" Ts - ||>> mk_Frees "y" Ts' - ||>> mk_Frees "z'" Ts - ||>> mk_Frees "y'" Ts' - ||>> mk_Frees "z1" Ts - ||>> mk_Frees "z2" Ts - ||>> mk_Frees "r" (map (mk_relT o `I) Ts) - ||>> mk_Frees "f" unfold_fTs - ||>> mk_Frees "s" corec_sTs - ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts) - ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) - ||>> mk_Frees' "rec" hrecTs; + val (((zs, ss), (Jzs, Jzs')), _) = + lthy + |> mk_Frees "b" activeAs + ||>> mk_Frees "s" sTs + ||>> mk_Frees' "z" Ts; fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_"); val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind; @@ -1418,6 +1455,13 @@ val unfold_defs = map (fn def => mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) unfold_def_frees; + val ((((ss, TRs), unfold_fs), corec_ss), names_lthy) = + lthy + |> mk_Frees "s" sTs + ||>> mk_Frees "r" (map (mk_relT o `I) Ts) + ||>> mk_Frees "f" unfold_fTs + ||>> mk_Frees "s" corec_sTs; + val mor_unfold_thm = let val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses; @@ -1552,7 +1596,7 @@ fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_"); val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind; - val corec_strs = + fun mk_corec_strs corec_ss = @{map 3} (fn dtor => fn sum_s => fn mapx => mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) @@ -1560,7 +1604,7 @@ fun corec_spec i T AT = fold_rev (Term.absfree o Term.dest_Free) corec_ss - (HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT)); + (HOLogic.mk_comp (mk_unfold Ts (mk_corec_strs corec_ss) i, Inr_const T AT)); val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) = lthy @@ -1587,6 +1631,17 @@ val corec_defs = map (fn def => mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees; + val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), names_lthy) = + lthy + |> mk_Frees "b" activeAs + ||>> mk_Frees "z" Ts + ||>> mk_Frees "z'" Ts + ||>> mk_Frees "z1" Ts + ||>> mk_Frees "z2" Ts + ||>> mk_Frees "f" unfold_fTs + ||>> mk_Frees "s" corec_sTs + ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); + val case_sums = map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks; val dtor_corec_thms = @@ -1612,7 +1667,7 @@ val corec_unique_mor_thm = let val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs; - val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs corec_strs UNIVs dtors id_fs); + val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs (mk_corec_strs corec_ss) UNIVs dtors id_fs); fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq unfold_fs ks)); @@ -1684,13 +1739,15 @@ val sndsTsTs' = map snd_const prodTsTs'; val activephiTs = map2 mk_pred2T activeAs activeBs; val activeJphiTs = map2 mk_pred2T Ts Ts'; - val (((((Jphis, Jpsi1s), Jpsi2s), activephis), activeJphis), names_lthy) = names_lthy - |> mk_Frees "R" JphiTs - ||>> mk_Frees "R" Jpsi1Ts - ||>> mk_Frees "Q" Jpsi2Ts - ||>> mk_Frees "S" activephiTs + + val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; + + val ((((Jzs, Jz's), Jphis), activeJphis), _) = + lthy + |> mk_Frees "z" Ts + ||>> mk_Frees "y" Ts' + ||>> mk_Frees "R" JphiTs ||>> mk_Frees "JR" activeJphiTs; - val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; fun mk_Jrel_DEADID_coinduct_thm () = mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis @@ -1710,17 +1767,14 @@ val fTs = map2 (curry op -->) passiveAs passiveBs; val gTs = map2 (curry op -->) passiveBs passiveCs; val uTs = map2 (curry op -->) Ts Ts'; - - val (((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)), - (ys_copy, ys'_copy)), Kss), names_lthy) = names_lthy - |> mk_Frees' "f" fTs + val (((((((nat, nat'), (Jzs, Jzs')), (hrecs, hrecs')), (fs, fs')), fs_copy), gs), _) = + lthy + |> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT + ||>> mk_Frees' "z" Ts + ||>> mk_Frees' "rec" hrecTs + ||>> mk_Frees' "f" fTs ||>> mk_Frees "f" fTs - ||>> mk_Frees "g" gTs - ||>> mk_Frees "u" uTs - ||>> mk_Frees' "b" Ts' - ||>> mk_Frees' "b" Ts' - ||>> mk_Frees' "y" passiveAs - ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) Ts) ATs);; + ||>> mk_Frees "g" gTs; val map_FTFT's = map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; @@ -1815,14 +1869,39 @@ fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds; val Jmaps = mk_Jmaps passiveAs passiveBs; + val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs); + + val timer = time (timer "bnf constants for the new datatypes"); + + val ((((((((((((((((((((ys, ys'), (nat, nat')), (Jzs, Jzs')), Jz's), Jzs_copy), Jz's_copy), + dtor_set_induct_phiss), Jphis), Jpsi1s), Jpsi2s), activeJphis), fs), fs_copy), gs), us), + (Jys, Jys')), (Jys_copy, Jys'_copy)), (ys_copy, ys'_copy)), Kss), names_lthy) = + lthy + |> mk_Frees' "y" passiveAs + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT + ||>> mk_Frees' "z" Ts + ||>> mk_Frees "y" Ts' + ||>> mk_Frees "z'" Ts + ||>> mk_Frees "y'" Ts' + ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) + ||>> mk_Frees "R" JphiTs + ||>> mk_Frees "R" Jpsi1Ts + ||>> mk_Frees "Q" Jpsi2Ts + ||>> mk_Frees "JR" activeJphiTs + ||>> mk_Frees "f" fTs + ||>> mk_Frees "f" fTs + ||>> mk_Frees "g" gTs + ||>> mk_Frees "u" uTs + ||>> mk_Frees' "b" Ts' + ||>> mk_Frees' "b" Ts' + ||>> mk_Frees' "y" passiveAs + ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) Ts) ATs); + val fs_Jmaps = map (fn m => Term.list_comb (m, fs)) Jmaps; val fs_copy_Jmaps = map (fn m => Term.list_comb (m, fs_copy)) Jmaps; val gs_Jmaps = map (fn m => Term.list_comb (m, gs)) (mk_Jmaps passiveBs passiveCs); val fgs_Jmaps = map (fn m => Term.list_comb (m, map2 (curry HOLogic.mk_comp) gs fs)) (mk_Jmaps passiveAs passiveCs); - val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs); - - val timer = time (timer "bnf constants for the new datatypes"); val (dtor_Jmap_thms, Jmap_thms) = let @@ -2181,7 +2260,8 @@ val zipFTs = mk_FTs zip_ranTs; val zipTs = @{map 3} (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs; val zip_zTs = mk_Ts passiveABs; - val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = names_lthy + val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = + names_lthy |> mk_Frees "zip" zipTs ||>> mk_Frees' "ab" passiveABs ||>> mk_Frees' "z" zip_zTs; @@ -2520,6 +2600,11 @@ lthy) end; + val ((Jphis, activephis), _) = + lthy + |> mk_Frees "R" JphiTs + ||>> mk_Frees "S" activephiTs; + val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) sym_map_comps map_cong0s; diff -r 0478ba10152a -r f49644098959 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 25 23:01:31 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 25 23:01:34 2015 +0200 @@ -117,23 +117,13 @@ bd0s Dss bnfs; val witss = map wits_of_bnf bnfs; - val (((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s), - fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), - names_lthy) = lthy + val ((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), (xFs, xFs')), names_lthy) = + lthy |> mk_Frees' "z" activeAs ||>> mk_Frees "B" BTs - ||>> mk_Frees "B" BTs - ||>> mk_Frees "B'" B'Ts - ||>> mk_Frees "B''" B''Ts ||>> mk_Frees "s" sTs - ||>> mk_Frees "prods" prod_sTs - ||>> mk_Frees "s'" s'Ts - ||>> mk_Frees "s''" s''Ts ||>> mk_Frees "f" fTs - ||>> mk_Frees "f" fTs - ||>> mk_Frees "f" inv_fTs ||>> mk_Frees "f" self_fTs - ||>> mk_Frees "g" gTs ||>> mk_Frees "g" all_gTs ||>> mk_Frees' "x" FTsAs; @@ -268,6 +258,16 @@ Term.list_comb (Const (alg, algT), args) end; + val ((((((((zs, zs'), Bs), B's), ss), s's), fs), (xFs, xFs')), names_lthy) = + lthy + |> mk_Frees' "z" activeAs + ||>> mk_Frees "B" BTs + ||>> mk_Frees "B'" B'Ts + ||>> mk_Frees "s" sTs + ||>> mk_Frees "s'" s'Ts + ||>> mk_Frees "f" fTs + ||>> mk_Frees' "x" FTsAs; + val alg_set_thms = let val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss); @@ -350,6 +350,22 @@ Term.list_comb (Const (mor, morT), args) end; + val ((((((((((((Bs, Bs_copy), B's), B''s), ss), prod_ss), s's), s''s), fs), fs_copy), gs), xFs), + names_lthy) = + lthy + |> mk_Frees "B" BTs + ||>> mk_Frees "B" BTs + ||>> mk_Frees "B'" B'Ts + ||>> mk_Frees "B''" B''Ts + ||>> mk_Frees "s" sTs + ||>> mk_Frees "prods" prod_sTs + ||>> mk_Frees "s'" s'Ts + ||>> mk_Frees "s''" s''Ts + ||>> mk_Frees "f" fTs + ||>> mk_Frees "f" fTs + ||>> mk_Frees "g" gTs + ||>> mk_Frees "x" FTsAs; + val morE_thms = let val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs); @@ -535,15 +551,14 @@ val II_sTs = map2 (fn Ds => fn bnf => mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs; - val (((((((idxs, Asi_name), (idx, idx')), (jdx, jdx')), II_Bs), II_ss), Asuc_fs), - names_lthy) = names_lthy - |> mk_Frees "i" (replicate n suc_bdT) + val ((((((Bs, ss), idxs), Asi_name), (idx, idx')), (jdx, jdx')), names_lthy) = + lthy + |> mk_Frees "B" BTs + ||>> mk_Frees "s" sTs + ||>> mk_Frees "i" (replicate n suc_bdT) ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi")) ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT - ||>> mk_Frees "IIB" II_BTs - ||>> mk_Frees "IIs" II_sTs - ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs); + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT; val suc_bd_limit_thm = let @@ -683,6 +698,11 @@ val min_algs = map (mk_min_alg ss) ks; + val ((Bs, ss), names_lthy) = + lthy + |> mk_Frees "B" BTs + ||>> mk_Frees "s" sTs; + val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) = let val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss); @@ -738,14 +758,12 @@ val init_FTs = map2 (fn Ds => mk_T_of_bnf Ds (passiveAs @ active_initTs)) Dss bnfs; val init_fTs = map (fn T => initT --> T) activeAs; - val (((((((iidx, iidx'), init_xs), (init_xFs, init_xFs')), - init_fs), init_fs_copy), init_phis), names_lthy) = names_lthy - |> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT - ||>> mk_Frees "ix" active_initTs - ||>> mk_Frees' "x" init_FTs - ||>> mk_Frees "f" init_fTs - ||>> mk_Frees "f" init_fTs - ||>> mk_Frees "P" (replicate n (mk_pred1T initT)); + val ((((II_Bs, II_ss), (iidx, iidx')), init_xFs), _) = + lthy + |> mk_Frees "IIB" II_BTs + ||>> mk_Frees "IIs" II_sTs + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT + ||>> mk_Frees "x" init_FTs; val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss) (HOLogic.mk_conj (HOLogic.mk_eq (iidx, @@ -790,6 +808,19 @@ val car_inits = map (mk_min_alg str_inits) ks; + val (((((((((Bs, ss), Asuc_fs), (iidx, iidx')), init_xs), (init_xFs, init_xFs')), init_fs), + init_fs_copy), init_phis), names_lthy) = + lthy + |> mk_Frees "B" BTs + ||>> mk_Frees "s" sTs + ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs) + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT + ||>> mk_Frees "ix" active_initTs + ||>> mk_Frees' "x" init_FTs + ||>> mk_Frees "f" init_fTs + ||>> mk_Frees "f" init_fTs + ||>> mk_Frees "P" (replicate n (mk_pred1T initT)); + val alg_init_thm = infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) str_inits) alg_min_alg_thm; @@ -909,20 +940,10 @@ val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts; val rec_UNIVs = map2 (HOLogic.mk_UNIV oo curry HOLogic.mk_prodT) Ts activeAs; - val (((((((((Izs1, Izs1'), (Izs2, Izs2')), xFs), yFs), (AFss, AFss')), - (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy - |> mk_Frees' "z1" Ts - ||>> mk_Frees' "z2" Ts' - ||>> mk_Frees "x" FTs - ||>> mk_Frees "y" FTs' - ||>> mk_Freess' "z" setFTss - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT - ||>> mk_Frees "f" fTs - ||>> mk_Frees "s" rec_sTs; - - val Izs = map2 retype_const_or_free Ts zs; - val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis; - val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis; + val ((ss, (fold_f, fold_f')), _) = + lthy + |> mk_Frees "s" sTs + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT; fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind; @@ -1007,6 +1028,16 @@ (* algebra copies *) + val (((((((Bs, B's), ss), s's), inv_fs), fs), rec_ss), names_lthy) = + lthy + |> mk_Frees "B" BTs + ||>> mk_Frees "B'" B'Ts + ||>> mk_Frees "s" sTs + ||>> mk_Frees "s'" s'Ts + ||>> mk_Frees "f" inv_fTs + ||>> mk_Frees "f" fTs + ||>> mk_Frees "s" rec_sTs; + val copy_thm = let val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) :: @@ -1156,14 +1187,14 @@ fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_"); val rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o rec_bind; - val rec_strs = + fun mk_rec_strs rec_ss = @{map 3} (fn ctor => fn prod_s => fn mapx => mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) ctors rec_ss rec_maps; fun rec_spec i T AT = fold_rev (Term.absfree o Term.dest_Free) rec_ss - (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i)); + (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts (mk_rec_strs rec_ss) i)); val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) = lthy @@ -1189,6 +1220,21 @@ val rec_defs = map (fn def => mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees; + val (((((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), fs), rec_ss), init_phis), + names_lthy) = + lthy + |> mk_Frees "z" Ts + ||>> mk_Frees' "z1" Ts + ||>> mk_Frees' "z2" Ts' + ||>> mk_Frees "x" FTs + ||>> mk_Frees "y" FTs' + ||>> mk_Frees "f" fTs + ||>> mk_Frees "s" rec_sTs + ||>> mk_Frees "P" (replicate n (mk_pred1T initT)); + + val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis; + val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis; + val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks; val ctor_rec_thms = let @@ -1212,7 +1258,7 @@ val rec_unique_mor_thm = let val id_fs = map2 (fn T => fn f => mk_convol (HOLogic.id_const T, f)) Ts fs; - val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs rec_strs id_fs); + val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs (mk_rec_strs rec_ss) id_fs); fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks)); in @@ -1321,12 +1367,7 @@ val Ipsi2Ts = map2 mk_pred2T passiveCs passiveBs; val activephiTs = map2 mk_pred2T activeAs activeBs; val activeIphiTs = map2 mk_pred2T Ts Ts'; - val (((((Iphis, Ipsi1s), Ipsi2s), activephis), activeIphis), names_lthy) = names_lthy - |> mk_Frees "R" IphiTs - ||>> mk_Frees "R" Ipsi1Ts - ||>> mk_Frees "Q" Ipsi2Ts - ||>> mk_Frees "S" activephiTs - ||>> mk_Frees "IR" activeIphiTs; + val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; (*register new datatypes as BNFs*) @@ -1340,11 +1381,10 @@ val fTs = map2 (curry op -->) passiveAs passiveBs; val uTs = map2 (curry op -->) Ts Ts'; - val (((((fs, fs'), fs_copy), us), (ys, ys')), - names_lthy) = names_lthy + val ((((fs, fs'), (AFss, AFss')), (ys, ys')), _) = + lthy |> mk_Frees' "f" fTs - ||>> mk_Frees "f" fTs - ||>> mk_Frees "u" uTs + ||>> mk_Freess' "z" setFTss ||>> mk_Frees' "y" passiveAs; val map_FTFT's = map2 (fn Ds => @@ -1469,6 +1509,22 @@ ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE) lthy) bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy; + val ((((((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), xFs), yFs))), Iphis), Ipsi1s), + Ipsi2s), fs), fs_copy), us), (ys, ys')), names_lthy) = + lthy + |> mk_Frees "z" Ts + ||>> mk_Frees' "z1" Ts + ||>> mk_Frees' "z2" Ts' + ||>> mk_Frees "x" FTs + ||>> mk_Frees "y" FTs' + ||>> mk_Frees "R" IphiTs + ||>> mk_Frees "R" Ipsi1Ts + ||>> mk_Frees "Q" Ipsi2Ts + ||>> mk_Frees "f" fTs + ||>> mk_Frees "f" fTs + ||>> mk_Frees "u" uTs + ||>> mk_Frees' "y" passiveAs; + val (_, Iconsts, Iconst_defs, mk_Iconsts) = @{split_list 4} Ibnf_consts; val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = @{split_list 5} Iconsts; val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = @{split_list 5} Iconst_defs; @@ -1790,6 +1846,14 @@ ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy) end; + val ((((((xFs, yFs)), Iphis), activephis), activeIphis), _) = + lthy + |> mk_Frees "x" FTs + ||>> mk_Frees "y" FTs' + ||>> mk_Frees "R" IphiTs + ||>> mk_Frees "S" activephiTs + ||>> mk_Frees "IR" activeIphiTs; + val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm diff -r 0478ba10152a -r f49644098959 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 25 23:01:31 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 25 23:01:34 2015 +0200 @@ -460,21 +460,19 @@ val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss; - val ((((((((([exh_y], (xss, xss')), yss), fs), gs), [h]), [u', v']), [w]), (p, p')), - names_lthy) = + val (((((((((exh_y, xss), yss), fs), gs), u), v), w), (p, p'))) = no_defs_lthy - |> mk_Frees "y" [fcT] (* for compatibility with "datatype_realizer.ML" *) - ||>> mk_Freess' "x" ctr_Tss + |> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *) + ||>> mk_Freess "x" ctr_Tss ||>> mk_Freess "y" ctr_Tss ||>> mk_Frees "f" case_Ts ||>> mk_Frees "g" case_Ts - ||>> mk_Frees "h" [B --> C] - ||>> (apfst (map (rpair fcT)) oo Variable.variant_fixes) [fc_b_name, fc_b_name ^ "'"] - ||>> mk_Frees "z" [B] - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; + ||>> yield_singleton (mk_Frees fc_b_name) fcT + ||>> yield_singleton (mk_Frees (fc_b_name ^ "'")) fcT + ||>> yield_singleton (mk_Frees "z") B + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT + |> fst; - val u = Free u'; - val v = Free v'; val q = Free (fst p', mk_pred1T B); val xctrs = map2 (curry Term.list_comb) ctrs xss; @@ -518,21 +516,8 @@ val casexC = mk_case As C case0; val casexBool = mk_case As HOLogic.boolT case0; - val fcase = Term.list_comb (casex, fs); - - val ufcase = fcase $ u; - val vfcase = fcase $ v; - - val eta_fcase = Term.list_comb (casex, eta_fs); - val eta_gcase = Term.list_comb (casex, eta_gs); - - val eta_ufcase = eta_fcase $ u; - val eta_vgcase = eta_gcase $ v; - fun mk_uu_eq () = HOLogic.mk_eq (u, u); - val uv_eq = mk_Trueprop_eq (u, v); - val exist_xs_u_eq_ctrs = map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss; @@ -685,6 +670,34 @@ fun after_qed ([exhaust_thm] :: thmss) lthy = let + val ((((((((xss, xss'), fs), gs), h), (u, u')), v), p), names_lthy) = + lthy + |> mk_Freess' "x" ctr_Tss + ||>> mk_Frees "f" case_Ts + ||>> mk_Frees "g" case_Ts + ||>> yield_singleton (mk_Frees "h") (B --> C) + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT + ||>> yield_singleton (mk_Frees (fc_b_name ^ "'")) fcT + ||>> yield_singleton (mk_Frees "P") HOLogic.boolT; + + val xfs = map2 (curry Term.list_comb) fs xss; + val xgs = map2 (curry Term.list_comb) gs xss; + + val fcase = Term.list_comb (casex, fs); + + val ufcase = fcase $ u; + val vfcase = fcase $ v; + + val eta_fcase = Term.list_comb (casex, eta_fs); + val eta_gcase = Term.list_comb (casex, eta_gs); + + val eta_ufcase = eta_fcase $ u; + val eta_vgcase = eta_gcase $ v; + + fun mk_uu_eq () = HOLogic.mk_eq (u, u); + + val uv_eq = mk_Trueprop_eq (u, v); + val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat; val rho_As = @@ -743,8 +756,7 @@ mk_case_cong_tac ctxt uexhaust_thm case_thms), Goal.prove_sorry lthy [] [] weak_goal (fn {context = ctxt, prems = _} => etac ctxt arg_cong 1)) - |> apply2 (singleton (Proof_Context.export names_lthy lthy) #> - Thm.close_derivation) + |> apply2 (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy)) end; val split_lhs = q $ ufcase;