--- 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;
--- 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
--- 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;