--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 24 14:51:10 2014 -0700
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 25 13:14:33 2014 +0100
@@ -239,10 +239,10 @@
val rhs =
Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
+ Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
(fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -257,10 +257,10 @@
val prems = map4 mk_prem (drop m sets) self_fs zs zs';
val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
(K (mk_map_cong0L_tac m map_cong0 map_id))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -273,13 +273,12 @@
val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs';
val concls =
map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps;
- val goals =
- map4 (fn prem => fn concl => fn x => fn y =>
- fold_rev Logic.all (x :: y :: all_gs) (Logic.mk_implies (prem, concl)))
- prems concls yFs yFs_copy;
+ val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls;
in
- map (fn goal => Goal.prove_sorry lthy [] [] goal
- (K ((hyp_subst_tac lthy THEN' rtac refl) 1)) |> Thm.close_derivation) goals
+ map (fn goal =>
+ Goal.prove_sorry lthy [] [] goal (K ((hyp_subst_tac lthy THEN' rtac refl) 1))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)) goals
end;
val timer = time (timer "Derived simple theorems");
@@ -332,26 +331,27 @@
val prems = map2 mk_prem zs Bs;
val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
ss zs setssAs;
- val goalss = map3 (fn x => fn prem => fn concls => map (fn concl =>
- fold_rev Logic.all (x :: Bs @ ss)
- (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
+ val goalss = map2 (fn prem => fn concls => map (fn concl =>
+ Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss;
in
- map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal
- (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
+ map (fn goals => map (fn goal =>
+ Goal.prove_sorry lthy [] [] goal (K (mk_coalg_set_tac coalg_def))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)) goals) goalss
end;
fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);
val tcoalg_thm =
let
- val goal = fold_rev Logic.all ss
- (HOLogic.mk_Trueprop (mk_tcoalg activeAs ss))
+ val goal = HOLogic.mk_Trueprop (mk_tcoalg activeAs ss)
in
Goal.prove_sorry lthy [] [] goal
(K (rtac (coalg_def RS iffD2) 1 THEN CONJ_WRAP
(K (EVERY' [rtac ballI, rtac CollectI,
CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Coalgebra definition & thms");
@@ -401,17 +401,17 @@
val (mor_image_thms, morE_thms) =
let
val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
- fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
- (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
+ fun mk_image_goal f B1 B2 =
+ Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2));
val image_goals = map3 mk_image_goal fs Bs B's;
fun mk_elim_goal B mapAsBs f s s' x =
- fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
- (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
- mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))));
+ Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
+ mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
fun prove goal =
Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
(map prove image_goals, map prove elim_goals)
end;
@@ -423,10 +423,10 @@
val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K (mk_mor_incl_tac mor_def map_ids))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
@@ -439,11 +439,10 @@
val concl =
HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
- (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_cong_thm =
@@ -452,11 +451,10 @@
(map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
- (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K ((hyp_subst_tac lthy THEN' atac) 1))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_UNIV_thm =
@@ -467,9 +465,10 @@
val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
in
- Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
+ Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
(K (mk_mor_UNIV_tac morE_thms mor_def))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_str_thm =
@@ -478,10 +477,10 @@
(mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs;
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all ss (HOLogic.mk_Trueprop
- (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss)))
+ (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss))
(K (mk_mor_str_tac ks mor_UNIV_thm))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_case_sum_thm =
@@ -491,10 +490,10 @@
s's sum_ss map_Inls;
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop
- (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls)))
+ (HOLogic.mk_Trueprop (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls))
(K (mk_mor_case_sum_tac ks mor_UNIV_thm))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Morphism definition & thms");
@@ -550,11 +549,10 @@
(mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
- (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1)
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_rel_thm =
@@ -568,21 +566,19 @@
(bis_le, Library.foldr1 HOLogic.mk_conj
(map6 mk_conjunct Rs ss s's zs z's relsAsBs))
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
- (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)))
+ Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs))
(K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_converse_thm =
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
- (Logic.mk_implies
- (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
- HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs)))))
+ (Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+ HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs))))
(K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val bis_O_thm =
let
@@ -592,11 +588,10 @@
val concl =
HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
- (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_Gr_thm =
@@ -604,12 +599,11 @@
val concl =
HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
- (Logic.list_implies ([coalg_prem, mor_prem], concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies ([coalg_prem, mor_prem], concl))
(fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
morE_thms coalg_in_thms)
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_image2_thm = bis_cong_thm OF
@@ -627,11 +621,10 @@
val concl =
HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Idx :: Bs @ ss @ B's @ s's @ Ris)
- (Logic.mk_implies (prem, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
(fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
(* self-bisimulation *)
@@ -677,11 +670,10 @@
end;
val sbis_lsbis_thm =
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss)
- (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks))))
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks)))
(K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
(bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
@@ -691,24 +683,25 @@
val incl_lsbis_thms =
let
fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
- val goals = map2 (fn i => fn R => fold_rev Logic.all (Bs @ ss @ sRs)
- (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
+ val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs;
in
- map3 (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal
- (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation) goals ks lsbis_defs
+ map3 (fn goal => fn i => fn def =>
+ Goal.prove_sorry lthy [] [] goal (K (mk_incl_lsbis_tac n i def))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)) goals ks lsbis_defs
end;
val equiv_lsbis_thms =
let
fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
- val goals = map2 (fn i => fn B => fold_rev Logic.all (Bs @ ss)
- (Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs;
+ val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs;
in
map3 (fn goal => fn l_incl => fn incl_l =>
Goal.prove_sorry lthy [] [] goal
(K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
bis_Id_on_thm bis_converse_thm bis_O_thm))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals lsbis_incl_thms incl_lsbis_thms
end;
@@ -1089,22 +1082,24 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
- val length_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ val length_Lev =
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs))
- |> Thm.close_derivation);
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val length_Lev' = mk_specN (n + 1) length_Lev;
val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;
- fun mk_goal i z = fold_rev Logic.all (z :: kl :: nat :: ss) (Logic.mk_implies
+ fun mk_goal i z = Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z)),
- HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z))));
+ HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z)));
val goals = map2 mk_goal ks zs;
val length_Levs' = map2 (fn goal => fn length_Lev =>
Goal.prove_sorry lthy [] [] goal (K (mk_length_Lev'_tac length_Lev))
- |> Thm.close_derivation) goals length_Levs;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)) goals length_Levs;
in
(length_Levs, length_Levs')
end;
@@ -1123,10 +1118,11 @@
val cTs = [SOME (certifyT lthy sum_sbdT)];
val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl];
- val rv_last = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)))
- |> Thm.close_derivation;
+ val rv_last =
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val rv_last' = mk_specN (n + 1) rv_last;
in
@@ -1158,10 +1154,11 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
- val set_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
- |> Thm.close_derivation;
+ val set_Lev =
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val set_Lev' = mk_specN (3 * n + 1) set_Lev;
in
@@ -1196,11 +1193,12 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
- val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ val set_image_Lev =
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss
- from_to_sbd_thmss to_sbd_inj_thmss)))
- |> Thm.close_derivation;
+ from_to_sbd_thmss to_sbd_inj_thmss))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
in
@@ -1212,14 +1210,14 @@
val mor_beh_thm =
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all ss (HOLogic.mk_Trueprop
- (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks))))
+ (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks)))
(fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
beh_defs carT_defs strT_defs isNode_defs
to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss
length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss
set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s)
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val timer = time (timer "Behavioral morphism");
@@ -1397,11 +1395,11 @@
val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all ss
- (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
+ (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks)))
(K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
map_comp_id_thms map_cong0s))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
@@ -1410,13 +1408,13 @@
val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
- val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
in
- `split_conj_thm (Goal.prove_sorry lthy [] [] goal
+ `split_conj_thm (Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
(K (mk_raw_coind_tac bis_def bis_cong_thm bis_O_thm bis_converse_thm bis_Gr_thm
tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm
lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
end;
val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
@@ -1429,10 +1427,10 @@
val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
- val unique_mor = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
+ val unique_mor = Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
(K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
`split_conj_thm unique_mor
end;
@@ -1558,7 +1556,7 @@
val lhs = dtor $ (mk_corec corec_ss i $ z);
val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z);
in
- fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
in
@@ -1566,7 +1564,8 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
corec_Inl_sum_thms)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals dtor_unfold_thms map_cong0s
end;
@@ -1578,11 +1577,11 @@
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 mk_fun_eq unfold_fs ks));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
+ Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
(fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
corec_Inl_sum_thms unfold_unique_mor_thm)
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_id0s_o_id =
@@ -1601,9 +1600,6 @@
val (coinduct_params, dtor_coinduct_thm) =
let
- val zs = Jzs1 @ Jzs2;
- val frees = phis @ zs;
-
val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
@@ -1620,13 +1616,13 @@
end;
val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
- val dtor_coinduct_goal =
- fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
+ val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl);
val dtor_coinduct =
Goal.prove_sorry lthy [] [] dtor_coinduct_goal
(K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
(rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct)
end;
@@ -1788,16 +1784,16 @@
val (dtor_Jmap_thms, Jmap_thms) =
let
- fun mk_goal fs_Jmap map dtor dtor' = fold_rev Logic.all fs
- (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
- HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)));
+ fun mk_goal fs_Jmap map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
+ HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor));
val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
val maps =
map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
mk_map_tac m n map_arg_cong unfold map_comp map_cong0)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms;
in
map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
@@ -1813,24 +1809,24 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) us fs_Jmaps));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
- mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
- |> Thm.close_derivation
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
+ mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val Jmap_comp0_thms =
let
- val goal = fold_rev Logic.all (fs @ gs)
- (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map3 (fn fmap => fn gmap => fn fgmap =>
- HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
- fs_Jmaps gs_Jmaps fgs_Jmaps)))
+ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map3 (fn fmap => fn gmap => fn fgmap =>
+ HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
+ fs_Jmaps gs_Jmaps fgs_Jmaps))
in
split_conj_thm (Goal.prove_sorry lthy [] [] goal
(K (mk_map_comp0_tac Jmap_thms map_comp0s dtor_Jmap_unique_thm))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
end;
val timer = time (timer "map functions for the new codatatypes");
@@ -1865,11 +1861,11 @@
map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
in
map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
- col_Sucs))
- |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
+ col_Sucs)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals ctss col_0ss' col_Sucss'
end;
@@ -1877,27 +1873,26 @@
fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
val concls = map2 mk_concl Jsetss_by_range Kss;
- val goals = map3 (fn Ks => fn prems => fn concl =>
- fold_rev Logic.all (Ks @ Jzs)
- (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
+ val goals = map2 (fn prems => fn concl =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls;
in
map2 (fn goal => fn col_minimal =>
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
mk_Jset_minimal_tac ctxt n col_minimal)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals col_minimal_thms
end;
val (dtor_Jset_incl_thmss, dtor_set_Jset_incl_thmsss) =
let
- fun mk_set_incl_Jset dtor x set Jset = fold_rev Logic.all (x :: ss)
- (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x)));
+ fun mk_set_incl_Jset dtor x set Jset =
+ HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x));
fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 =
- fold_rev Logic.all [x, y]
- (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
- HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y))));
+ Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
+ HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y)));
val set_incl_Jset_goalss =
map4 (fn dtor => fn x => fn sets => fn Jsets =>
@@ -1917,7 +1912,8 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
mk_set_incl_Jset_tac rec_Suc)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals rec_Sucs)
set_incl_Jset_goalss col_Sucss,
map2 (fn goalss => fn rec_Sucs =>
@@ -1926,7 +1922,8 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
mk_set_Jset_incl_Jset_tac n rec_Suc k)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals rec_Sucs)
ks goalss)
set_Jset_incl_Jset_goalsss col_Sucss)
@@ -1977,24 +1974,23 @@
FTs_setss dtors Jzs sets)
ls Jsetss_by_range;
- val le_goals = map
- (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
+ val le_goals = map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
(mk_goals (uncurry mk_leq));
val set_le_thmss = map split_conj_thm
(map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
Goal.prove_sorry lthy [] [] goal
(K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
- val ge_goalss = map (map2 (fn z => fn goal =>
- Logic.all z (HOLogic.mk_Trueprop goal)) Jzs)
- (mk_goals (uncurry mk_leq o swap));
+ val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
val set_ge_thmss =
map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
Goal.prove_sorry lthy [] [] goal
(K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
- |> Thm.close_derivation))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)))
ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
in
map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
@@ -2023,11 +2019,11 @@
val thms =
map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
- dtor_Jmap_thms set_mapss))
- |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
+ dtor_Jmap_thms set_mapss)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals ctss col_0ss' col_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2047,11 +2043,11 @@
val thms =
map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
- mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
- |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
+ mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
ls goals ctss col_0ss' col_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2092,11 +2088,12 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
- val thm = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
+ val thm =
+ Goal.prove_sorry lthy [] [] goal
(K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
- set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels)))
+ set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
split_conj_thm thm
end;
@@ -2114,8 +2111,8 @@
val dtor_Jrel_thms =
let
- fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
- (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
+ fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi =
+ mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz'));
val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
in
map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
@@ -2124,7 +2121,8 @@
Goal.prove_sorry lthy [] [] goal
(K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss'
dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss
dtor_set_Jset_incl_thmsss
@@ -2261,10 +2259,10 @@
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
in
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs)))
- |> Thm.close_derivation
+ Goal.prove_sorry lthy [] [] goal
+ (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "helpers for BNF properties");
@@ -2374,8 +2372,8 @@
else @{term False})
else @{term True}));
in
- fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop
- (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)))
+ HOLogic.mk_Trueprop
+ (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))
end;
val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
in
@@ -2383,7 +2381,8 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
(flat set_mapss) wit_thms)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals dtor_Jset_induct_thms
|> map split_conj_thm
|> transpose
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 24 14:51:10 2014 -0700
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 25 13:14:33 2014 +0100
@@ -207,10 +207,10 @@
val rhs = Term.list_comb (mapAsCs,
take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
+ Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
(fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -224,10 +224,10 @@
val prems = map4 mk_prem (drop m sets) self_fs zs zs';
val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
(K (mk_map_cong0L_tac m map_cong0 map_id))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -278,12 +278,13 @@
fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
val concls = map3 mk_concl ss xFs Bs;
- val goals = map3 (fn x => fn prems => fn concl =>
- fold_rev Logic.all (x :: Bs @ ss)
- (Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
+ val goals = map2 (fn prems => fn concl =>
+ Logic.list_implies (alg_prem :: prems, concl)) premss concls;
in
map (fn goal =>
- Goal.prove_sorry lthy [] [] goal (K (mk_alg_set_tac alg_def)) |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] goal (K (mk_alg_set_tac alg_def))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals
end;
@@ -295,13 +296,13 @@
HOLogic.mk_Trueprop (mk_alg Bs ss);
val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
val goals =
- map (fn concl =>
- fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (alg_prem, concl))) concls;
+ map (fn concl => Logic.mk_implies (alg_prem, concl)) concls;
in
map2 (fn goal => fn alg_set =>
- Goal.prove_sorry lthy [] []
- goal (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
- |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] goal
+ (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals alg_set_thms
end;
@@ -355,12 +356,12 @@
fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
(HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
fun mk_elim_goal sets mapAsBs f s s' x T =
- fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
- (Logic.list_implies ([prem, mk_elim_prem sets x T],
- mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
+ Logic.list_implies ([prem, mk_elim_prem sets x T],
+ mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])));
val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
- fun prove goal =
- Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
+ fun prove goal = Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
map prove elim_goals
end;
@@ -370,10 +371,10 @@
val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K (mk_mor_incl_tac mor_def map_ids))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_comp_thm =
@@ -384,11 +385,10 @@
val concl =
HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
- (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K (mk_mor_comp_tac mor_def set_mapss map_comp_id_thms))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_cong_thm =
@@ -397,11 +397,10 @@
(map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
- (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K ((hyp_subst_tac lthy THEN' atac) 1))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_str_thm =
@@ -410,10 +409,11 @@
(mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs;
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all ss (HOLogic.mk_Trueprop
- (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss)))
+ (HOLogic.mk_Trueprop
+ (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss))
(K (mk_mor_str_tac ks mor_def))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_convol_thm =
@@ -423,10 +423,11 @@
s's prod_ss map_fsts;
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (s's @ prod_ss) (HOLogic.mk_Trueprop
- (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts)))
+ (HOLogic.mk_Trueprop
+ (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts))
(K (mk_mor_convol_tac ks mor_def))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_UNIV_thm =
@@ -437,9 +438,10 @@
val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
in
- Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
+ Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
(K (mk_mor_UNIV_tac m morE_thms mor_def))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Morphism definition & thms");
@@ -553,10 +555,10 @@
val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd
(Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all idxs (Logic.list_implies ([prem], concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies ([prem], concl))
(K (mk_bd_limit_tac n suc_bd_Cinfinite))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Bounds");
@@ -592,23 +594,23 @@
val concl = HOLogic.mk_Trueprop
(HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
(map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
- val goal = fold_rev Logic.all (idx :: ss)
- (Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
+ val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl);
val min_algs_thm = Goal.prove_sorry lthy [] [] goal
(K (mk_min_algs_tac suc_bd_worel in_cong'_thms))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
fun mk_mono_goal min_alg =
- fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_relChain suc_bd
- (Term.absfree idx' min_alg)));
+ HOLogic.mk_Trueprop (mk_relChain suc_bd (Term.absfree idx' min_alg));
val monos =
map2 (fn goal => fn min_algs =>
Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
(map mk_mono_goal min_algss) min_algs_thms;
fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
@@ -616,27 +618,29 @@
val card_cT = certifyT lthy suc_bdT;
val card_ct = certify lthy (Term.absfree idx' card_conjunction);
- val card_of = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] []
+ val card_of =
+ Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)))
(K (mk_min_algs_card_of_tac card_cT card_ct
m suc_bd_worel min_algs_thms in_sbds
sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
- suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
- |> Thm.close_derivation;
+ suc_bd_Asuc_bd Asuc_bd_Cinfinite))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
val least_cT = certifyT lthy suc_bdT;
val least_ct = certify lthy (Term.absfree idx' least_conjunction);
- val least = singleton (Proof_Context.export names_lthy lthy)
+ val least =
(Goal.prove_sorry lthy [] []
(Logic.mk_implies (least_prem,
HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction))))
(K (mk_min_algs_least_tac least_cT least_ct
suc_bd_worel min_algs_thms alg_set_thms)))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
(min_algs_thms, monos, card_of, least)
end;
@@ -680,11 +684,12 @@
val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
let
- val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
+ val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss);
val alg_min_alg = Goal.prove_sorry lthy [] [] goal
(K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite
set_sbdss min_algs_thms min_algs_mono_thms))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd))
@@ -694,20 +699,20 @@
val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss)
- (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
+ (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B)))
(K (mk_least_min_alg_tac def least_min_algs_thm))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
val incl = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss)
- (Logic.mk_implies (incl_prem,
- HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids))))
+ (Logic.mk_implies (incl_prem,
+ HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids)))
(K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
(alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
end;
@@ -803,11 +808,11 @@
(mk_mor car_inits str_inits active_UNIVs ss
(map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (iidx :: ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def
alg_select_thm alg_set_thms set_mapss str_init_defs))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val init_unique_mor_thms =
@@ -820,13 +825,12 @@
val unique = HOLogic.mk_Trueprop
(Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
val cts = map (certify lthy) ss;
- val unique_mor = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (init_xs @ Bs @ init_fs @ init_fs_copy)
- (Logic.list_implies (prems @ mor_prems, unique)))
+ val unique_mor =
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
(K (mk_init_unique_mor_tac cts m alg_def alg_init_thm least_min_alg_thms
in_mono'_thms alg_set_thms morE_thms map_cong0s))
- |> Thm.close_derivation);
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
split_conj_thm unique_mor
end;
@@ -856,10 +860,10 @@
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 mk_Ball car_inits init_phis));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all init_phis (Logic.mk_implies (prem, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
(K (mk_init_induct_tac m alg_def alg_init_thm least_min_alg_thms alg_set_thms))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Initiality definition & thms");
@@ -1005,10 +1009,10 @@
val concl = HOLogic.mk_Trueprop (list_exists_free s's
(HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs) (Logic.list_implies (prems, concl)))
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
(K (mk_copy_tac m alg_def mor_def alg_set_thms set_mapss))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val init_ex_mor_thm =
@@ -1016,12 +1020,12 @@
val goal = HOLogic.mk_Trueprop
(list_exists_free fs (mk_mor UNIVs ctors active_UNIVs ss fs));
in
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} =>
- mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
- card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
- |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
+ card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_fold_thm =
@@ -1030,11 +1034,11 @@
val cT = certifyT lthy foldT;
val ct = certify lthy fold_fun
in
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
- (K (mk_mor_fold_tac cT ct fold_defs init_ex_mor_thm mor_cong)))
+ Goal.prove_sorry lthy [] []
+ (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
+ (K (mk_mor_fold_tac cT ct fold_defs init_ex_mor_thm mor_cong))
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
@@ -1046,11 +1050,11 @@
val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
- val unique_mor = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
+ val unique_mor = Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
(K (mk_fold_unique_mor_tac type_defs init_unique_mor_thms Reps
mor_comp_thm mor_Abs_thm mor_fold_thm))
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
`split_conj_thm unique_mor
end;
@@ -1175,14 +1179,15 @@
val lhs = mk_rec rec_ss i $ (ctor $ x);
val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
in
- fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
in
map2 (fn goal => fn foldx =>
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals ctor_fold_thms
end;
@@ -1193,11 +1198,11 @@
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
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (rec_ss @ fs) (Logic.mk_implies (prem, unique)))
+ Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
(fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
fold_unique_mor_thm)
|> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
@@ -1234,11 +1239,11 @@
val goal = Logic.list_implies (prems, concl);
in
- (Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (phis @ Izs) goal)
+ (Goal.prove_sorry lthy [] [] goal
(K (mk_ctor_induct_tac lthy m set_mapss init_induct_thm morE_thms mor_Abs_thm
Rep_inverses Abs_inverses Reps))
- |> Thm.close_derivation,
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy),
rev (Term.add_tfrees goal []))
end;
@@ -1277,11 +1282,11 @@
val cts = map3 (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
val goal = Logic.list_implies (prems, concl);
in
- (singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
- weak_ctor_induct_thms))
- |> Thm.close_derivation,
+ (Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
+ weak_ctor_induct_thms)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy),
rev (Term.add_tfrees goal []))
end;
@@ -1415,16 +1420,17 @@
val (ctor_Imap_thms, ctor_Imap_o_thms) =
let
- fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs
- (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
- HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps))));
+ fun mk_goal fs_map map ctor ctor' =
+ mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
+ HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps)));
val goals = map4 mk_goal fs_Imaps map_FTFT's ctors ctor's;
val maps =
map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
mk_map_tac m n foldx map_comp_id map_cong0)
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals ctor_fold_thms map_comp_id_thms map_cong0s;
in
`(map (fn thm => thm RS @{thm comp_eq_dest})) maps
@@ -1439,11 +1445,11 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) us fs_Imaps));
- val unique = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
+ val unique = Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
`split_conj_thm unique
end;
@@ -1464,9 +1470,9 @@
ctor_fold_thms) goalss;
fun mk_simp_goal pas_set act_sets sets ctor z set =
- Logic.all z (mk_Trueprop_eq (set $ (ctor $ z),
+ mk_Trueprop_eq (set $ (ctor $ z),
mk_union (pas_set $ z,
- Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
+ Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)));
val simp_goalss =
map2 (fn i => fn sets =>
map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
@@ -1476,7 +1482,8 @@
val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
Goal.prove_sorry lthy [] [] goal
(K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
set_mapss) ls simp_goalss setss;
in
ctor_setss
@@ -1520,10 +1527,10 @@
fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms;
val thms =
map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
- |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals csetss ctor_Iset_thmss inducts ls;
in
map split_conj_thm thms
@@ -1548,11 +1555,11 @@
fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd_Cinfinite set_sbdss;
val thms =
map4 (fn goal => fn ctor_sets => fn induct => fn i =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
- mk_tac ctxt induct ctor_sets i))
- |> Thm.close_derivation)
+ mk_tac ctxt induct ctor_sets i)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
goals ctor_Iset_thmss inducts ls;
in
map split_conj_thm thms
@@ -1579,11 +1586,11 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map4 mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
- val thm = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
- map_cong0s ctor_Imap_thms))
- |> Thm.close_derivation;
+ val thm = Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
+ map_cong0s ctor_Imap_thms)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
in
split_conj_thm thm
end;
@@ -1606,8 +1613,8 @@
val ctor_Irel_thms =
let
- fun mk_goal xF yF ctor ctor' Irelphi relphi = fold_rev Logic.all (xF :: yF :: Iphis)
- (mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
+ fun mk_goal xF yF ctor ctor' Irelphi relphi =
+ mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF);
val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
in
map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
@@ -1616,7 +1623,8 @@
Goal.prove_sorry lthy [] [] goal
(K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
- |> Thm.close_derivation)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy))
ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss
ctor_set_Iset_incl_thmsss
@@ -1637,11 +1645,11 @@
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
in
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
- ctor_Irel_thms rel_mono_strongs rel_OOs))
- |> Thm.close_derivation
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
+ ctor_Irel_thms rel_mono_strongs rel_OOs)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "helpers for BNF properties");