no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Tue Sep 04 12:10:19 2012 +0200
@@ -188,8 +188,10 @@
if ! quick_and_dirty then
replicate ilive no_thm
else
- map (fn goal => Skip_Proof.prove lthy [] [] goal
- (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer))))
+ map (fn goal =>
+ Skip_Proof.prove lthy [] [] goal
+ (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
+ |> Thm.close_derivation)
(map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) comp_sets comp_sets_alt);
fun comp_map_cong_tac _ =
@@ -227,6 +229,7 @@
in
Skip_Proof.prove lthy [] [] goal
(fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
+ |> Thm.close_derivation
end;
fun comp_in_bd_tac _ =
@@ -346,7 +349,7 @@
val goal =
fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt)));
in
- Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac)
+ Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
end;
fun killN_in_bd_tac _ =
@@ -455,7 +458,7 @@
val goal =
fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt)))
in
- Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac)
+ Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
end;
fun liftN_in_bd_tac _ =
@@ -543,6 +546,7 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt)));
in
Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
+ |> Thm.close_derivation
end;
fun permute_in_bd_tac _ =
@@ -731,13 +735,13 @@
val pred_unfold = Local_Defs.unfold lthy'
(map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def;
- fun note thmN thms =
- snd o Local_Theory.note
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
+ val notes =
+ [(rel_unfoldN, [rel_unfold]),
+ (pred_unfoldN, [pred_unfold])]
+ |> map (fn (thmN, thms) =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
in
- (bnf', lthy'
- |> note rel_unfoldN [rel_unfold]
- |> note pred_unfoldN [pred_unfold])
+ (bnf', lthy' |> Local_Theory.notes notes |> snd)
end;
fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 04 12:10:19 2012 +0200
@@ -829,11 +829,7 @@
let
val (axioms, wit_thms) = apfst (mk_axioms live) (chop (length goals) thms);
- val bd_Card_order =
- Skip_Proof.prove lthy [] []
- (HOLogic.mk_Trueprop (mk_Card_order (bnf_bd_As)))
- (fn _ => mk_Card_order_tac (#bd_card_order axioms));
-
+ val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]};
val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
@@ -855,6 +851,7 @@
in
Skip_Proof.prove lthy [] [] goal
(fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
+ |> Thm.close_derivation
end;
val collect_set_natural = mk_lazy mk_collect_set_natural;
@@ -868,6 +865,7 @@
(mk_subset (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
in
Skip_Proof.prove lthy [] [] goal_in_mono (K (mk_in_mono_tac live))
+ |> Thm.close_derivation
end;
val in_mono = mk_lazy mk_in_mono;
@@ -881,6 +879,7 @@
(HOLogic.mk_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA'))));
in
Skip_Proof.prove lthy [] [] goal_in_cong (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
+ |> Thm.close_derivation
end;
val in_cong = mk_lazy mk_in_cong;
@@ -982,6 +981,7 @@
Skip_Proof.prove lthy [] [] goal
(fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong axioms)
(#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_natural'))
+ |> Thm.close_derivation
end;
val map_wppull = mk_lazy mk_map_wppull;
@@ -997,6 +997,7 @@
(mk_rel_Gr_tac bnf_rel_def (#map_id axioms) (#map_cong axioms)
(#map_wpull axioms) (Lazy.force in_cong) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_natural'))
+ |> Thm.close_derivation
end;
val rel_Gr = mk_lazy mk_rel_Gr;
@@ -1013,6 +1014,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
(mk_rel_mono_tac bnf_rel_def (Lazy.force in_mono))
+ |> Thm.close_derivation
end;
fun mk_rel_cong () =
@@ -1023,6 +1025,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
(fn _ => (TRY o hyp_subst_tac THEN' rtac refl) 1)
+ |> Thm.close_derivation
end;
val rel_mono = mk_lazy mk_rel_mono;
@@ -1034,6 +1037,7 @@
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (Term.list_comb (relAsAs, map Id_const As'), Id_const CA')))
(mk_rel_Id_tac live (Lazy.force rel_Gr) (#map_id axioms))
+ |> Thm.close_derivation
end;
val rel_Id = mk_lazy mk_rel_Id;
@@ -1047,9 +1051,11 @@
val le_thm = Skip_Proof.prove lthy [] [] le_goal
(mk_rel_converse_le_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
(Lazy.force map_comp') (map Lazy.force set_natural'))
+ |> Thm.close_derivation
val goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
in
Skip_Proof.prove lthy [] [] goal (fn _ => mk_rel_converse_tac le_thm)
+ |> Thm.close_derivation
end;
val rel_converse = mk_lazy mk_rel_converse;
@@ -1066,6 +1072,7 @@
Skip_Proof.prove lthy [] [] goal
(mk_rel_O_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
(Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
+ |> Thm.close_derivation
end;
val rel_O = mk_lazy mk_rel_O;
@@ -1085,6 +1092,7 @@
fold_rev Logic.all (x :: y :: Rs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
in
Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac bnf_rel_def (length bnf_sets))
+ |> Thm.close_derivation
end;
val in_rel = mk_lazy mk_in_rel;
@@ -1104,48 +1112,55 @@
val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
wits bnf_rel bnf_pred;
-
- fun note thmN thms =
- snd o Local_Theory.note
- ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []), thms);
-
- fun lazy_note thmN thms = note thmN (map Lazy.force thms);
in
(bnf, lthy
|> (if fact_policy = Note_All_Facts_and_Axioms then
let
val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
+ val notes =
+ [(bd_card_orderN, [#bd_card_order axioms]),
+ (bd_cinfiniteN, [#bd_cinfinite axioms]),
+ (bd_Card_orderN, [#bd_Card_order facts]),
+ (bd_CinfiniteN, [#bd_Cinfinite facts]),
+ (bd_CnotzeroN, [#bd_Cnotzero facts]),
+ (collect_set_naturalN, [Lazy.force (#collect_set_natural facts)]),
+ (in_bdN, [#in_bd axioms]),
+ (in_monoN, [Lazy.force (#in_mono facts)]),
+ (in_relN, [Lazy.force (#in_rel facts)]),
+ (map_compN, [#map_comp axioms]),
+ (map_idN, [#map_id axioms]),
+ (map_wpullN, [#map_wpull axioms]),
+ (set_naturalN, #set_natural axioms),
+ (set_bdN, #set_bd axioms)] @
+ map2 pair witNs wit_thms
+ |> map (fn (thmN, thms) =>
+ ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
+ [(thms, [])]));
in
- note bd_card_orderN [#bd_card_order axioms]
- #> note bd_cinfiniteN [#bd_cinfinite axioms]
- #> note bd_Card_orderN [#bd_Card_order facts]
- #> note bd_CinfiniteN [#bd_Cinfinite facts]
- #> note bd_CnotzeroN [#bd_Cnotzero facts]
- #> lazy_note collect_set_naturalN [#collect_set_natural facts]
- #> note in_bdN [#in_bd axioms]
- #> lazy_note in_monoN [#in_mono facts]
- #> lazy_note in_relN [#in_rel facts]
- #> note map_compN [#map_comp axioms]
- #> note map_idN [#map_id axioms]
- #> note map_wpullN [#map_wpull axioms]
- #> note set_naturalN (#set_natural axioms)
- #> note set_bdN (#set_bd axioms)
- #> fold2 note witNs wit_thms
+ Local_Theory.notes notes #> snd
end
else
I)
|> (if fact_policy = Note_All_Facts_and_Axioms orelse
fact_policy = Derive_All_Facts_Note_Most then
- lazy_note rel_IdN [#rel_Id facts]
- #> lazy_note rel_GrN [#rel_Gr facts]
- #> lazy_note rel_converseN [#rel_converse facts]
- #> lazy_note rel_ON [#rel_O facts]
- #> lazy_note map_id'N [#map_id' facts]
- #> lazy_note map_comp'N [#map_comp' facts]
- #> note map_congN [#map_cong axioms]
- #> lazy_note set_natural'N (#set_natural' facts)
- #> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
+ let
+ val notes =
+ [(map_congN, [#map_cong axioms]),
+ (rel_IdN, [Lazy.force (#rel_Id facts)]),
+ (rel_GrN, [Lazy.force (#rel_Gr facts)]),
+ (rel_converseN, [Lazy.force (#rel_converse facts)]),
+ (rel_ON, [Lazy.force (#rel_O facts)]),
+ (map_id'N, [Lazy.force (#map_id' facts)]),
+ (map_comp'N, [Lazy.force (#map_comp' facts)]),
+ (set_natural'N, map Lazy.force (#set_natural' facts))]
+ |> map (fn (thmN, thms) =>
+ ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
+ [(thms, [])]));
+ in
+ Local_Theory.notes notes #> snd
+ #> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
+ end
else
I))
end;
@@ -1163,9 +1178,10 @@
Skip_Proof.prove lthy [] [] wit_goal wits_tac
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
- |> map (map (Thm.forall_elim_vars 0));
+ |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0))
in
- (map2 (Skip_Proof.prove lthy [] []) goals (map (unfold_defs_tac lthy defs) tacs))
+ (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
+ goals (map (unfold_defs_tac lthy defs) tacs))
|> (fn thms => after_qed (map single thms @ wit_thms) lthy)
end) oo prepare_def const_policy fact_policy qualify
(fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 12:10:19 2012 +0200
@@ -62,11 +62,6 @@
val ls = 1 upto m;
val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
- fun note thmN thms = snd o Local_Theory.note
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
- fun notes thmN thmss = fold2 (fn b => fn thms => snd o Local_Theory.note
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms)) bs thmss;
-
(* TODO: check if m, n etc are sane *)
val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
@@ -243,6 +238,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
(K (mk_map_comp_id_tac map_comp))
+ |> Thm.close_derivation
end;
val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
@@ -261,6 +257,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
(K (mk_map_congL_tac m map_cong map_id'))
+ |> Thm.close_derivation
end;
val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
@@ -281,7 +278,7 @@
prems concls xFs xFs_copy;
in
map (fn goal => Skip_Proof.prove lthy [] [] goal
- (K ((hyp_subst_tac THEN' rtac refl) 1))) goals
+ (K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals
end;
val timer = time (timer "Derived simple theorems");
@@ -344,7 +341,7 @@
(Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
in
map (fn goals => map (fn goal => Skip_Proof.prove lthy [] [] goal
- (K (mk_coalg_set_tac coalg_def))) goals) goalss
+ (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
end;
val coalg_set_thmss' = transpose coalg_set_thmss;
@@ -360,6 +357,7 @@
(K (stac coalg_def 1 THEN CONJ_WRAP
(K (EVERY' [rtac ballI, rtac CollectI,
CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss))
+ |> Thm.close_derivation
end;
val timer = time (timer "Coalgebra definition & thms");
@@ -424,7 +422,8 @@
(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 =
- Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def));
+ Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def))
+ |> Thm.close_derivation;
in
(map prove image_goals, map prove elim_goals)
end;
@@ -439,6 +438,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
(K (mk_mor_incl_tac mor_def map_id's))
+ |> Thm.close_derivation
end;
val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
@@ -455,6 +455,7 @@
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
(Logic.list_implies (prems, concl)))
(K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms))
+ |> Thm.close_derivation
end;
val mor_cong_thm =
@@ -467,6 +468,7 @@
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
(Logic.list_implies (prems, concl)))
(K ((hyp_subst_tac THEN' atac) 1))
+ |> Thm.close_derivation
end;
val mor_UNIV_thm =
@@ -480,6 +482,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
(K (mk_mor_UNIV_tac morE_thms mor_def))
+ |> Thm.close_derivation
end;
val mor_str_thm =
@@ -491,6 +494,7 @@
(fold_rev Logic.all 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
end;
val mor_sum_case_thm =
@@ -503,6 +507,7 @@
(fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop
(mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls)))
(K (mk_mor_sum_case_tac ks mor_UNIV_thm))
+ |> Thm.close_derivation
end;
val timer = time (timer "Morphism definition & thms");
@@ -634,15 +639,16 @@
in
(map3 (fn goals => fn defs => fn rec_Sucs =>
map3 (fn goal => fn def => fn rec_Suc =>
- Skip_Proof.prove lthy [] [] goal
- (K (mk_set_incl_hset_tac def rec_Suc)))
+ Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hset_tac def rec_Suc))
+ |> Thm.close_derivation)
goals defs rec_Sucs)
set_incl_hset_goalss hset_defss hset_rec_Sucss,
map3 (fn goalss => fn defsi => fn rec_Sucs =>
map3 (fn k => fn goals => fn defsk =>
map4 (fn goal => fn defk => fn defi => fn rec_Suc =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k)))
+ (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k))
+ |> Thm.close_derivation)
goals defsk defsi rec_Sucs)
ks goalss hset_defss)
set_hset_incl_hset_goalsss hset_defss hset_rec_Sucss)
@@ -671,7 +677,8 @@
ss zs setssAs hsetssAs;
in
map2 (map2 (fn goal => fn thms =>
- Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hin_tac thms))))
+ Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hin_tac thms))
+ |> Thm.close_derivation))
set_incl_hin_goalss set_hset_incl_hset_thmsss
end;
@@ -707,7 +714,8 @@
map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
- (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs)))
+ (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs))
+ |> Thm.close_derivation)
goals ctss hset_rec_0ss' hset_rec_Sucss'
end;
@@ -721,7 +729,8 @@
in
map3 (fn goal => fn hset_defs => fn hset_rec_minimal =>
Skip_Proof.prove lthy [] [] goal
- (mk_hset_minimal_tac n hset_defs hset_rec_minimal))
+ (mk_hset_minimal_tac n hset_defs hset_rec_minimal)
+ |> Thm.close_derivation)
goals hset_defss' hset_rec_minimal_thms
end;
@@ -747,7 +756,8 @@
singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
(K (mk_mor_hset_rec_tac m n cts j hset_rec_0s hset_rec_Sucs
- morE_thms set_natural'ss coalg_set_thmss))))
+ morE_thms set_natural'ss coalg_set_thmss)))
+ |> Thm.close_derivation)
ls goals ctss hset_rec_0ss' hset_rec_Sucss'
end;
@@ -766,7 +776,8 @@
in
map3 (map3 (fn goal => fn hset_def => fn mor_hset_rec =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_mor_hset_tac hset_def mor_hset_rec))))
+ (K (mk_mor_hset_tac hset_def mor_hset_rec))
+ |> Thm.close_derivation))
goalss hset_defss' mor_hset_rec_thmss
end;
@@ -832,6 +843,7 @@
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
(Logic.list_implies (prems, concl)))
(K ((hyp_subst_tac THEN' atac) 1))
+ |> Thm.close_derivation
end;
val bis_rel_thm =
@@ -850,6 +862,7 @@
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
(HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_bis As Bs ss B's s's Rs, rhs))))
(K (mk_bis_rel_tac m bis_def rel_defs map_comp's map_congs set_natural'ss))
+ |> Thm.close_derivation
end;
val bis_converse_thm =
@@ -858,7 +871,8 @@
(Logic.mk_implies
(HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
- (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converses));
+ (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converses))
+ |> Thm.close_derivation;
val bis_O_thm =
let
@@ -872,6 +886,7 @@
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
(Logic.list_implies (prems, concl)))
(K (mk_bis_O_tac m bis_rel_thm rel_congs rel_Os))
+ |> Thm.close_derivation
end;
val bis_Gr_thm =
@@ -883,6 +898,7 @@
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
(Logic.list_implies ([coalg_prem, mor_prem], concl)))
(mk_bis_Gr_tac bis_rel_thm rel_Grs mor_image_thms morE_thms coalg_in_thms)
+ |> Thm.close_derivation
end;
val bis_image2_thm = bis_cong_thm OF
@@ -904,6 +920,7 @@
(fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
(Logic.mk_implies (prem, concl)))
(mk_bis_Union_tac bis_def in_mono'_thms)
+ |> Thm.close_derivation
end;
(* self-bisimulation *)
@@ -959,7 +976,8 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (As @ Bs @ ss)
(HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
- (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm));
+ (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm))
+ |> Thm.close_derivation;
val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
(bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct1 RS mk_conjunctN n i)) ks;
@@ -973,7 +991,7 @@
(Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
in
map3 (fn goal => fn i => fn def => Skip_Proof.prove lthy [] [] goal
- (K (mk_incl_lsbis_tac n i def))) goals ks lsbis_defs
+ (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation) goals ks lsbis_defs
end;
val equiv_lsbis_thms =
@@ -985,7 +1003,8 @@
map3 (fn goal => fn l_incl => fn incl_l =>
Skip_Proof.prove lthy [] [] goal
(K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
- bis_diag_thm bis_converse_thm bis_O_thm)))
+ bis_diag_thm bis_converse_thm bis_O_thm))
+ |> Thm.close_derivation)
goals lsbis_incl_thms incl_lsbis_thms
end;
@@ -1269,7 +1288,8 @@
val coalgT_thm =
Skip_Proof.prove lthy [] []
(fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
- (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_natural'ss);
+ (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_natural'ss)
+ |> Thm.close_derivation;
val card_of_carT_thms =
let
@@ -1285,6 +1305,7 @@
(fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs)))
(K (mk_card_of_carT_tac m isNode_defs sbd_sbd_thm
sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds))
+ |> Thm.close_derivation
in
map (fn def => @{thm ordLeq_transitive[OF
card_of_mono1[OF ord_eq_le_trans[OF _ Collect_restrict']]]} OF [def, card_of_carT])
@@ -1310,7 +1331,8 @@
fn carT_def => fn strT_def => fn isNode_def => fn set_naturals =>
map2 (fn goal => fn set_natural =>
Skip_Proof.prove lthy [] [] goal
- (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural))
+ (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural)
+ |> Thm.close_derivation)
goals (drop m set_naturals))
ks goalss carT_defs strT_defs isNode_defs set_natural'ss
end;
@@ -1354,7 +1376,8 @@
(K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts
carT_defs strT_defs isNode_defs
set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss'
- coalgT_thm set_natural'ss))))
+ coalgT_thm set_natural'ss)))
+ |> Thm.close_derivation)
ls goals ctss set_incl_hset_thmss' set_hset_incl_hset_thmsss''
end;
@@ -1375,9 +1398,10 @@
map5 (fn carT_prem => fn isNode_prems => fn in_prem => fn concls => fn strT_hset_thmss =>
map4 (fn isNode_prem => fn concl => fn isNode_def => fn strT_hset_thms =>
Skip_Proof.prove lthy [] []
- (fold_rev Logic.all (Kl :: lab :: kl :: As @ As_copy)
- (Logic.list_implies ([carT_prem, prem, isNode_prem, in_prem], concl)))
- (mk_isNode_hset_tac n isNode_def strT_hset_thms))
+ (fold_rev Logic.all (Kl :: lab :: kl :: As @ As_copy)
+ (Logic.list_implies ([carT_prem, prem, isNode_prem, in_prem], concl)))
+ (mk_isNode_hset_tac n isNode_def strT_hset_thms)
+ |> Thm.close_derivation)
isNode_prems concls isNode_defs
(if m = 0 then replicate n [] else transpose strT_hset_thmss))
carT_prems isNode_premss in_prems conclss
@@ -1556,7 +1580,8 @@
val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss)));
+ (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss))
+ |> Thm.close_derivation);
val Lev_sbd' = mk_specN n Lev_sbd;
in
@@ -1574,7 +1599,8 @@
val length_Lev = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs)));
+ (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs))
+ |> Thm.close_derivation);
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;
@@ -1585,8 +1611,8 @@
val goals = map2 mk_goal ks zs;
val length_Levs' = map2 (fn goal => fn length_Lev =>
- Skip_Proof.prove lthy [] [] goal
- (K (mk_length_Lev'_tac length_Lev))) goals length_Levs;
+ Skip_Proof.prove lthy [] [] goal (K (mk_length_Lev'_tac length_Lev))
+ |> Thm.close_derivation) goals length_Levs;
in
(length_Levs, length_Levs')
end;
@@ -1603,7 +1629,8 @@
val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)));
+ (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)))
+ |> Thm.close_derivation;
val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev;
in
@@ -1626,7 +1653,8 @@
val rv_last = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)));
+ (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)))
+ |> Thm.close_derivation;
val rv_last' = mk_specN (n + 1) rv_last;
in
@@ -1651,7 +1679,8 @@
(Skip_Proof.prove lthy [] []
(Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
(K (mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
- coalg_set_thmss from_to_sbd_thmss)));
+ coalg_set_thmss from_to_sbd_thmss)))
+ |> Thm.close_derivation;
val set_rv_Lev' = mk_specN (n + 1) set_rv_Lev;
in
@@ -1689,7 +1718,8 @@
val set_Lev = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)));
+ (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
+ |> Thm.close_derivation;
val set_Lev' = mk_specN (3 * n + 1) set_Lev;
in
@@ -1727,7 +1757,8 @@
val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss
- from_to_sbd_thmss to_sbd_inj_thmss)));
+ from_to_sbd_thmss to_sbd_inj_thmss)))
+ |> Thm.close_derivation;
val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
in
@@ -1746,7 +1777,8 @@
to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
- set_natural'ss coalg_set_thmss map_comp_id_thms map_congs map_arg_cong_thms);
+ set_natural'ss coalg_set_thmss map_comp_id_thms map_congs map_arg_cong_thms)
+ |> Thm.close_derivation;
val timer = time (timer "Behavioral morphism");
@@ -1776,19 +1808,22 @@
in
map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms)))
+ (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms))
+ |> Thm.close_derivation)
goals lsbisE_thms map_comp_id_thms map_congs
end;
val coalg_final_thm = Skip_Proof.prove lthy [] [] (fold_rev Logic.all As
(HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs)))
(K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
- set_natural'ss coalgT_set_thmss));
+ set_natural'ss coalgT_set_thmss))
+ |> Thm.close_derivation;
val mor_T_final_thm = Skip_Proof.prove lthy [] [] (fold_rev Logic.all As
(HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs
(map (mk_proj o mk_LSBIS As) ks))))
- (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms));
+ (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms))
+ |> Thm.close_derivation;
val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
val in_car_final_thms = map (fn mor_image' => mor_image' OF
@@ -1892,12 +1927,14 @@
Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs unfs car_finals str_finals Rep_Ts))
(mk_mor_Rep_tac m (mor_def :: unf_defs) Reps Abs_inverses coalg_final_set_thmss
- map_comp_id_thms map_congL_thms);
+ map_comp_id_thms map_congL_thms)
+ |> Thm.close_derivation;
val mor_Abs =
Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs unfs Abs_Ts))
- (mk_mor_Abs_tac (mor_def :: unf_defs) Abs_inverses);
+ (mk_mor_Abs_tac (mor_def :: unf_defs) Abs_inverses)
+ |> Thm.close_derivation;
in
(mor_Rep, mor_Abs)
end;
@@ -1946,6 +1983,7 @@
(HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs unfs (map (mk_coiter Ts ss) ks))))
(K (mk_mor_coiter_tac m mor_UNIV_thm unf_defs coiter_defs Abs_inverses' morEs'
map_comp_id_thms map_congs))
+ |> Thm.close_derivation
end;
val coiter_thms = map (fn thm => (thm OF [mor_coiter_thm, UNIV_I]) RS sym) morE_thms;
@@ -1959,7 +1997,8 @@
`split_conj_thm (Skip_Proof.prove lthy [] [] goal
(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)))
+ lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects))
+ |> Thm.close_derivation)
end;
val unique_mor_thms =
@@ -1975,7 +2014,8 @@
val unique_mor = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ coiter_fs @ coiter_fs_copy @ zs)
(Logic.list_implies (prems, unique)))
- (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm));
+ (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm))
+ |> Thm.close_derivation;
in
map (fn thm => conjI RSN (2, thm RS mp)) (split_conj_thm unique_mor)
end;
@@ -1992,7 +2032,8 @@
val unique_mor = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (ss @ coiter_fs) (Logic.mk_implies (prem, unique)))
- (K (mk_coiter_unique_mor_tac raw_coind_thms bis_thm mor_thm coiter_defs));
+ (K (mk_coiter_unique_mor_tac raw_coind_thms bis_thm mor_thm coiter_defs))
+ |> Thm.close_derivation;
in
`split_conj_thm unique_mor
end;
@@ -2054,7 +2095,8 @@
in
map5 (fn goal => fn fld_def => fn coiter => fn map_comp_id => fn map_congL =>
Skip_Proof.prove lthy [] [] goal
- (mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unf_thms))
+ (mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unf_thms)
+ |> Thm.close_derivation)
goals fld_defs coiter_thms map_comp_id_thms map_congL_thms
end;
@@ -2139,8 +2181,9 @@
in
map3 (fn goal => fn coiter => fn map_cong =>
Skip_Proof.prove lthy [] [] goal
- (mk_corec_tac m corec_defs coiter map_cong corec_Inl_sum_thms))
- goals coiter_thms map_congs
+ (mk_corec_tac m corec_defs coiter map_cong corec_Inl_sum_thms)
+ |> Thm.close_derivation)
+ goals coiter_thms map_congs
end;
val timer = time (timer "corec definitions & thms");
@@ -2185,7 +2228,8 @@
val rel_coinduct = Local_Defs.unfold lthy @{thms diag_UNIV}
(Skip_Proof.prove lthy [] [] rel_coinduct_goal
- (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm)));
+ (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
+ |> Thm.close_derivation);
fun mk_unf_prem upto_eq phi unf map_nth sets Jz Jz_copy FJz =
let
@@ -2216,7 +2260,8 @@
val unf_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (unf_prems, concl));
val unf_coinduct = Skip_Proof.prove lthy [] [] unf_coinduct_goal
- (K (mk_unf_coinduct_tac m ks raw_coind_thm bis_def));
+ (K (mk_unf_coinduct_tac m ks raw_coind_thm bis_def))
+ |> Thm.close_derivation;
val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
@@ -2224,13 +2269,15 @@
val rel_coinduct_upto = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (rel_upto_prems, concl)))
- (K (mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids)));
+ (K (mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids)))
+ |> Thm.close_derivation;
val unf_coinduct_upto = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (unf_upto_prems, concl)))
(K (mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def
- (tcoalg_thm RS bis_diag_thm))));
+ (tcoalg_thm RS bis_diag_thm))))
+ |> Thm.close_derivation;
val pred_coinduct = rel_coinduct
|> Local_Defs.unfold lthy @{thms Id_def'}
@@ -2338,9 +2385,11 @@
HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf))));
val goals = map4 mk_goal fs_maps map_FTFT's unfs unf's;
val cTs = map (SOME o certifyT lthy) FTs';
- val maps = map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong =>
- Skip_Proof.prove lthy [] [] goal
- (K (mk_map_tac m n cT coiter map_comp' map_cong)))
+ val maps =
+ map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong =>
+ Skip_Proof.prove lthy [] [] goal
+ (K (mk_map_tac m n cT coiter map_comp' map_cong))
+ |> Thm.close_derivation)
goals cTs coiter_thms map_comp's map_congs;
in
map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
@@ -2355,7 +2404,8 @@
fs_maps gs_maps fgs_maps)))
in
split_conj_thm (Skip_Proof.prove lthy [] [] goal
- (K (mk_map_comp_tac m n map_thms map_comps map_congs coiter_unique_thm)))
+ (K (mk_map_comp_tac m n map_thms map_comps map_congs coiter_unique_thm))
+ |> Thm.close_derivation)
end;
val (map_unique_thms, map_unique_thm) =
@@ -2369,7 +2419,8 @@
(map2 (curry HOLogic.mk_eq) us fs_maps));
val unique = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (mk_map_unique_tac coiter_unique_thm map_comps);
+ (mk_map_unique_tac coiter_unique_thm map_comps)
+ |> Thm.close_derivation;
in
`split_conj_thm unique
end;
@@ -2408,7 +2459,8 @@
val set_le_thmss = map split_conj_thm
(map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)))
+ (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss))
+ |> Thm.close_derivation)
le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss');
val simp_goalss = map (map2 (fn z => fn goal =>
@@ -2417,7 +2469,8 @@
in
map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets))))
+ (K (mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets))
+ |> Thm.close_derivation))
simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
end;
@@ -2443,10 +2496,12 @@
val ctss =
map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
- val thms = map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (mk_col_natural_tac cts rec_0s rec_Sucs map_simp_thms set_natural'ss)))
+ val thms =
+ map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (mk_col_natural_tac cts rec_0s rec_Sucs map_simp_thms set_natural'ss))
+ |> Thm.close_derivation)
goals ctss hset_rec_0ss' hset_rec_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2464,11 +2519,13 @@
val ctss =
map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
- val thms = map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_col_bd_tac m j cts rec_0s rec_Sucs
- sbd_Card_order sbd_Cinfinite set_sbdss))))
+ val thms =
+ map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (K (mk_col_bd_tac m j cts rec_0s rec_Sucs
+ sbd_Card_order sbd_Cinfinite set_sbdss)))
+ |> Thm.close_derivation)
ls goals ctss hset_rec_0ss' hset_rec_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2513,6 +2570,7 @@
(Skip_Proof.prove lthy [] [] goal
(K (mk_mcong_tac m (rtac coinduct) map_comp's map_simp_thms map_congs set_natural'ss
set_hset_thmss set_hset_hset_thmsss)))
+ |> Thm.close_derivation
in
split_conj_thm thm
end;
@@ -2547,6 +2605,7 @@
in
Skip_Proof.prove lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms
set_natural'ss pickWP_assms_tacs)
+ |> Thm.close_derivation
end;
val (mor_thePull_fst_thm, mor_thePull_snd_thm, mor_thePull_pick_thm) =
@@ -2569,11 +2628,11 @@
(Logic.mk_implies (wpull_prem, mor_pick));
in
(Skip_Proof.prove lthy [] [] goal_fst (mk_mor_thePull_fst_tac m mor_def map_wpull_thms
- map_comp's pickWP_assms_tacs),
+ map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
Skip_Proof.prove lthy [] [] goal_snd (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
- map_comp's pickWP_assms_tacs),
+ map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
Skip_Proof.prove lthy [] [] goal_pick (mk_mor_thePull_pick_tac mor_def coiter_thms
- map_comp's))
+ map_comp's) |> Thm.close_derivation)
end;
val pick_col_thmss =
@@ -2593,10 +2652,12 @@
val goals =
map (fn concl => Logic.mk_implies (wpull_prem, HOLogic.mk_Trueprop concl)) concls;
- val thms = map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal
- (mk_pick_col_tac m j cts rec_0s rec_Sucs coiter_thms set_natural'ss map_wpull_thms
- pickWP_assms_tacs)))
+ val thms =
+ map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+ singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal
+ (mk_pick_col_tac m j cts rec_0s rec_Sucs coiter_thms set_natural'ss map_wpull_thms
+ pickWP_assms_tacs))
+ |> Thm.close_derivation)
ls goals ctss hset_rec_0ss' hset_rec_Sucss';
in
map (map (fn thm => thm RS mp) o split_conj_thm o mk_specN n) thms
@@ -2785,7 +2846,8 @@
in
map2 (fn goal => fn induct =>
Skip_Proof.prove lthy [] [] goal
- (mk_coind_wit_tac induct coiter_thms (flat set_natural'ss) wit_thms))
+ (mk_coind_wit_tac induct coiter_thms (flat set_natural'ss) wit_thms)
+ |> Thm.close_derivation)
goals hset_induct_thms
|> map split_conj_thm
|> transpose
@@ -2861,8 +2923,9 @@
fn map_simp => fn set_simps => fn unf_inject => fn unf_fld =>
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
- unf_inject unf_fld set_naturals set_incls set_set_inclss)))
+ (K (mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
+ unf_inject unf_fld set_naturals set_incls set_set_inclss))
+ |> Thm.close_derivation)
ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
unf_inject_thms unf_fld_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
@@ -2875,42 +2938,64 @@
val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
in
map3 (fn goal => fn pred_def => fn Jrel_unfold =>
- Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Jpred_defs Jrel_unfold))
+ Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Jpred_defs Jrel_unfold)
+ |> Thm.close_derivation)
goals pred_defs Jrel_unfold_thms
end;
val timer = time (timer "additional properties");
val ls' = if m = 1 then [0] else ls;
+
+ val Jbnf_common_notes =
+ [(map_uniqueN, [fold_maps map_unique_thm])] @
+ map2 (fn i => fn thm => (mk_set_inductN i, [thm])) ls' set_induct_thms
+ |> map (fn (thmN, thms) =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+ val Jbnf_notes =
+ [(map_simpsN, map single folded_map_simp_thms),
+ (set_inclN, set_incl_thmss),
+ (set_set_inclN, map flat set_set_incl_thmsss), (* nicer names? *)
+ (rel_unfoldN, map single Jrel_unfold_thms),
+ (pred_unfoldN, map single Jpred_unfold_thms)] @
+ map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
+ |> maps (fn (thmN, thmss) =>
+ map2 (fn b => fn thms =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+ bs thmss)
in
- lthy
- |> note map_uniqueN [fold_maps map_unique_thm]
- |> notes map_simpsN (map single folded_map_simp_thms)
- |> fold2 (fn i => notes (mk_set_simpsN i) o map single) ls' folded_set_simp_thmss
- |> notes set_inclN set_incl_thmss
- |> notes set_set_inclN (map flat set_set_incl_thmsss) (* nicer names? *)
- |> fold2 (fn i => note (mk_set_inductN i) o single) ls' set_induct_thms
- |> notes rel_unfoldN (map single Jrel_unfold_thms)
- |> notes pred_unfoldN (map single Jpred_unfold_thms)
+ lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd
end;
+
+ val common_notes =
+ [(unf_coinductN, [unf_coinduct_thm]),
+ (rel_coinductN, [rel_coinduct_thm]),
+ (pred_coinductN, [pred_coinduct_thm]),
+ (unf_coinduct_uptoN, [unf_coinduct_upto_thm]),
+ (rel_coinduct_uptoN, [rel_coinduct_upto_thm]),
+ (pred_coinduct_uptoN, [pred_coinduct_upto_thm])]
+ |> map (fn (thmN, thms) =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+ val notes =
+ [(coiterN, coiter_thms),
+ (coiter_uniqueN, coiter_unique_thms),
+ (corecN, corec_thms),
+ (unf_fldN, unf_fld_thms),
+ (fld_unfN, fld_unf_thms),
+ (unf_injectN, unf_inject_thms),
+ (unf_exhaustN, unf_exhaust_thms),
+ (fld_injectN, fld_inject_thms),
+ (fld_exhaustN, fld_exhaust_thms),
+ (fld_coiterN, fld_coiter_thms)]
+ |> map (apsnd (map single))
+ |> maps (fn (thmN, thmss) =>
+ map2 (fn b => fn thms =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+ bs thmss)
in
- lthy
- |> notes coiterN (map single coiter_thms)
- |> notes coiter_uniqueN (map single coiter_unique_thms)
- |> notes corecN (map single corec_thms)
- |> notes unf_fldN (map single unf_fld_thms)
- |> notes fld_unfN (map single fld_unf_thms)
- |> notes unf_injectN (map single unf_inject_thms)
- |> notes unf_exhaustN (map single unf_exhaust_thms)
- |> notes fld_injectN (map single fld_inject_thms)
- |> notes fld_exhaustN (map single fld_exhaust_thms)
- |> notes fld_coiterN (map single fld_coiter_thms)
- |> note unf_coinductN [unf_coinduct_thm]
- |> note rel_coinductN [rel_coinduct_thm]
- |> note pred_coinductN [pred_coinduct_thm]
- |> note unf_coinduct_uptoN [unf_coinduct_upto_thm]
- |> note rel_coinduct_uptoN [rel_coinduct_upto_thm]
- |> note pred_coinduct_uptoN [pred_coinduct_upto_thm]
+ lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
val _ =
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 12:10:19 2012 +0200
@@ -31,11 +31,6 @@
val m = live - n (*passive, if 0 don't generate a new bnf*)
val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
- fun note thmN thms = snd o Local_Theory.note
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
- fun notes thmN thmss = fold2 (fn b => fn thms => snd o Local_Theory.note
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms)) bs thmss;
-
(* TODO: check if m, n etc are sane *)
val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
@@ -176,6 +171,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
(K (mk_map_comp_id_tac map_comp))
+ |> Thm.close_derivation
end;
val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
@@ -193,6 +189,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
(K (mk_map_congL_tac m map_cong map_id'))
+ |> Thm.close_derivation
end;
val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
@@ -252,8 +249,9 @@
fold_rev Logic.all (x :: As @ Bs @ ss)
(Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
in
- map (fn goal => Skip_Proof.prove lthy [] [] goal
- (K (mk_alg_set_tac alg_def))) goals
+ map (fn goal =>
+ Skip_Proof.prove lthy [] [] goal (K (mk_alg_set_tac alg_def)) |> Thm.close_derivation)
+ goals
end;
fun mk_talg ATs BTs = mk_alg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
@@ -265,6 +263,7 @@
in
Skip_Proof.prove lthy [] [] goal
(K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
+ |> Thm.close_derivation
end;
val timer = time (timer "Algebra definition & thms");
@@ -280,8 +279,9 @@
in
map2 (fn goal => fn alg_set =>
Skip_Proof.prove lthy [] []
- goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms)))
- goals alg_set_thms
+ goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms))
+ |> Thm.close_derivation)
+ goals alg_set_thms
end;
val timer = time (timer "Proved nonemptiness");
@@ -348,7 +348,7 @@
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 =
- Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def));
+ Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
in
(map prove image_goals, map prove elim_goals)
end;
@@ -361,6 +361,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
(K (mk_mor_incl_tac mor_def map_id's))
+ |> Thm.close_derivation
end;
val mor_comp_thm =
@@ -375,6 +376,7 @@
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
(Logic.list_implies (prems, concl)))
(K (mk_mor_comp_tac mor_def set_natural'ss map_comp_id_thms))
+ |> Thm.close_derivation
end;
val mor_inv_thm =
@@ -393,6 +395,7 @@
(Logic.list_implies (prems, concl)))
(K (mk_mor_inv_tac alg_def mor_def
set_natural'ss morE_thms map_comp_id_thms map_congL_thms))
+ |> Thm.close_derivation
end;
val mor_cong_thm =
@@ -405,6 +408,7 @@
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
(Logic.list_implies (prems, concl)))
(K ((hyp_subst_tac THEN' atac) 1))
+ |> Thm.close_derivation
end;
val mor_str_thm =
@@ -416,6 +420,7 @@
(fold_rev Logic.all 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
end;
val mor_convol_thm =
@@ -428,6 +433,7 @@
(fold_rev Logic.all (s's @ prod_ss) (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
end;
val mor_UNIV_thm =
@@ -441,6 +447,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
(K (mk_mor_UNIV_tac m morE_thms mor_def))
+ |> Thm.close_derivation
end;
val timer = time (timer "Morphism definition & thms");
@@ -471,6 +478,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
(K (mk_iso_alt_tac mor_image_thms mor_inv_thm))
+ |> Thm.close_derivation
end;
val timer = time (timer "Isomorphism definition & thms");
@@ -492,14 +500,16 @@
val copy_str_thm = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
(Logic.list_implies (all_prems, alg)))
- (K (mk_copy_str_tac set_natural'ss alg_def alg_set_thms));
+ (K (mk_copy_str_tac set_natural'ss alg_def alg_set_thms))
+ |> Thm.close_derivation;
val iso = HOLogic.mk_Trueprop
(mk_iso B's (map5 mk_s fs ss mapsBsAs yFs yFs') Bs ss inv_fs fs_copy);
val copy_alg_thm = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
(Logic.list_implies (all_prems, iso)))
- (K (mk_copy_alg_tac set_natural'ss alg_set_thms mor_def iso_alt_thm copy_str_thm));
+ (K (mk_copy_alg_tac set_natural'ss alg_set_thms mor_def iso_alt_thm copy_str_thm))
+ |> Thm.close_derivation;
val ex = HOLogic.mk_Trueprop
(list_exists_free s's
@@ -508,7 +518,8 @@
val ex_copy_alg_thm = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
(Logic.list_implies (prems, ex)))
- (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm));
+ (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm))
+ |> Thm.close_derivation;
in
(copy_alg_thm, ex_copy_alg_thm)
end;
@@ -584,6 +595,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all idxs (Logic.list_implies ([prem], concl)))
(K (mk_bd_limit_tac n suc_bd_Cinfinite))
+ |> Thm.close_derivation
end;
val timer = time (timer "Bounds");
@@ -622,7 +634,8 @@
(Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
val min_algs_thm = Skip_Proof.prove lthy [] [] goal
- (K (mk_min_algs_tac suc_bd_worel in_cong'_thms));
+ (K (mk_min_algs_tac suc_bd_worel in_cong'_thms))
+ |> Thm.close_derivation;
val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
@@ -630,9 +643,11 @@
fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_relChain suc_bd
(Term.absfree idx' min_alg)));
- val monos = map2 (fn goal => fn min_algs =>
- Skip_Proof.prove lthy [] [] goal (K (mk_min_algs_mono_tac min_algs)))
- (map mk_mono_goal min_algss) min_algs_thms;
+ val monos =
+ map2 (fn goal => fn min_algs =>
+ Skip_Proof.prove lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
+ |> Thm.close_derivation)
+ (map mk_mono_goal min_algss) min_algs_thms;
val Asuc_bd = mk_Asuc_bd As;
@@ -647,7 +662,8 @@
(K (mk_min_algs_card_of_tac card_cT card_ct
m suc_bd_worel min_algs_thms in_bd_sums
sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
- suc_bd_Asuc_bd Asuc_bd_Cinfinite Asuc_bd_Cnotzero)));
+ suc_bd_Asuc_bd Asuc_bd_Cinfinite Asuc_bd_Cnotzero)))
+ |> Thm.close_derivation;
val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_subset min_algss Bs);
@@ -659,7 +675,8 @@
(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)));
+ suc_bd_worel min_algs_thms alg_set_thms)))
+ |> Thm.close_derivation;
in
(min_algs_thms, monos, card_of, least)
end;
@@ -712,20 +729,23 @@
val goal = fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_alg As min_algs ss));
val alg_min_alg = Skip_Proof.prove lthy [] [] goal
(K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
- set_bd_sumss min_algs_thms min_algs_mono_thms));
+ set_bd_sumss min_algs_thms min_algs_mono_thms))
+ |> Thm.close_derivation;
val Asuc_bd = mk_Asuc_bd As;
fun mk_card_of_thm min_alg def = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (As @ ss)
(HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
(K (mk_card_of_min_alg_tac def card_of_min_algs_thm
- suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite));
+ suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
+ |> Thm.close_derivation;
val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
fun mk_least_thm min_alg B def = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (As @ Bs @ ss)
(Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_subset min_alg B))))
- (K (mk_least_min_alg_tac def least_min_algs_thm));
+ (K (mk_least_min_alg_tac def least_min_algs_thm))
+ |> Thm.close_derivation;
val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
@@ -735,11 +755,10 @@
(fold_rev Logic.all (Bs @ ss)
(Logic.mk_implies (incl_prem,
HOLogic.mk_Trueprop (mk_mor incl_min_algs ss Bs ss active_ids))))
- (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1));
+ (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
+ |> Thm.close_derivation;
in
- (alg_min_alg,
- map2 mk_card_of_thm min_algs min_alg_defs,
- leasts, incl)
+ (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
end;
val timer = time (timer "Minimal algebra definition & thms");
@@ -821,12 +840,14 @@
(*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
val alg_init_thm = Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_alg passive_UNIVs car_inits str_inits))
- (K (rtac alg_min_alg_thm 1));
+ (K (rtac alg_min_alg_thm 1))
+ |> Thm.close_derivation;
val alg_select_thm = Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_Ball II
(Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
(mk_alg_select_tac Abs_IIT_inverse_thm)
+ |> Thm.close_derivation;
val mor_select_thm =
let
@@ -842,6 +863,7 @@
(fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (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_natural'ss str_init_defs))
+ |> Thm.close_derivation
end;
val (init_ex_mor_thm, init_unique_mor_thms) =
@@ -852,7 +874,8 @@
val ex_mor = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
(mk_init_ex_mor_tac Abs_IIT_inverse_thm ex_copy_alg_thm alg_min_alg_thm
- card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm);
+ card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm)
+ |> Thm.close_derivation;
val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
val mor_prems = map HOLogic.mk_Trueprop
@@ -865,7 +888,8 @@
(fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
(Logic.list_implies (prems @ mor_prems, unique)))
(K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
- in_mono'_thms alg_set_thms morE_thms map_congs));
+ in_mono'_thms alg_set_thms morE_thms map_congs))
+ |> Thm.close_derivation;
in
(ex_mor, split_conj_thm unique_mor)
end;
@@ -898,6 +922,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all init_phis (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
end;
val timer = time (timer "Initiality definition & thms");
@@ -929,7 +954,8 @@
fun mk_inver_thm mk_tac rep abs X thm =
Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_inver rep abs X))
- (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1));
+ (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
+ |> Thm.close_derivation;
val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses;
val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits
@@ -1009,13 +1035,15 @@
val mor_Rep =
Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs flds car_inits str_inits Rep_Ts))
- (mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps);
+ (mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps)
+ |> Thm.close_derivation;
val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
val mor_Abs =
Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs flds Abs_Ts))
- (K (mk_mor_Abs_tac inv inver_Abss inver_Reps));
+ (K (mk_mor_Abs_tac inv inver_Abss inver_Reps))
+ |> Thm.close_derivation;
in
(mor_Rep, mor_Abs)
end;
@@ -1068,6 +1096,7 @@
(Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs flds active_UNIVs ss (map (mk_iter Ts ss) ks)))
(K (mk_mor_iter_tac cT ct iter_defs ex_mor (mor_comp RS mor_cong))))
+ |> Thm.close_derivation
end;
val iter_thms = map (fn morE => rule_by_tactic lthy
@@ -1082,7 +1111,8 @@
val unique_mor = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
(K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms T_subset2s Reps
- mor_comp_thm mor_Abs_thm mor_iter_thm));
+ mor_comp_thm mor_Abs_thm mor_iter_thm))
+ |> Thm.close_derivation;
in
`split_conj_thm unique_mor
end;
@@ -1149,8 +1179,9 @@
in
map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iter_thms)))
- goals unf_defs iter_thms map_comp_id_thms map_congL_thms
+ (K (mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iter_thms))
+ |> Thm.close_derivation)
+ goals unf_defs iter_thms map_comp_id_thms map_congL_thms
end;
val unf_fld_thms = map (fn thm => thm RS @{thm pointfree_idE}) unf_o_fld_thms;
@@ -1228,7 +1259,8 @@
val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs;
in
map2 (fn goal => fn iter =>
- Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms))
+ Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms)
+ |> Thm.close_derivation)
goals iter_thms
end;
@@ -1263,7 +1295,9 @@
(Skip_Proof.prove lthy [] []
(fold_rev Logic.all (phis @ Izs) goal)
(K (mk_fld_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm
- Rep_inverses Abs_inverses Reps T_subset1s T_subset2s)), rev (Term.add_tfrees goal []))
+ Rep_inverses Abs_inverses Reps T_subset1s T_subset2s))
+ |> Thm.close_derivation,
+ rev (Term.add_tfrees goal []))
end;
val cTs = map (SOME o certifyT lthy o TFree) induct_params;
@@ -1303,7 +1337,8 @@
in
(singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
- (mk_fld_induct2_tac cTs cts fld_induct_thm weak_fld_induct_thms)),
+ (mk_fld_induct2_tac cTs cts fld_induct_thm weak_fld_induct_thms))
+ |> Thm.close_derivation,
rev (Term.add_tfrees goal []))
end;
@@ -1367,9 +1402,10 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (fs_map, fld),
HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps)))));
val goals = map4 mk_goal fs_maps map_FTFT's flds fld's;
- val maps = map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
- Skip_Proof.prove lthy [] [] goal
- (K (mk_map_tac m n iter map_comp_id map_cong)))
+ val maps =
+ map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
+ Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iter map_comp_id map_cong))
+ |> Thm.close_derivation)
goals iter_thms map_comp_id_thms map_congs;
in
map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
@@ -1386,7 +1422,8 @@
(map2 (curry HOLogic.mk_eq) us fs_maps));
val unique = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs));
+ (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs))
+ |> Thm.close_derivation;
in
`split_conj_thm unique
end;
@@ -1427,7 +1464,7 @@
val goalss =
map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss;
val setss = map (map2 (fn iter => fn goal =>
- Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)))
+ Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)) |> Thm.close_derivation)
iter_thms) goalss;
fun mk_simp_goal pas_set act_sets sets fld z set =
@@ -1442,8 +1479,9 @@
val set_simpss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats))))
- set_natural'ss) ls simp_goalss setss;
+ (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats)))
+ |> Thm.close_derivation)
+ set_natural'ss) ls simp_goalss setss;
in
(set_simpss, setss)
end;
@@ -1485,10 +1523,11 @@
fs setss_by_range setss_by_range';
fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss map_simp_thms;
- val thms = map5 (fn goal => fn csets => fn set_simps => fn induct => fn i =>
- singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
- (mk_tac induct csets set_simps i)))
+ val thms =
+ map5 (fn goal => fn csets => fn set_simps => fn induct => fn i =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets set_simps i))
+ |> Thm.close_derivation)
goals csetss set_simp_thmss inducts ls;
in
map split_conj_thm thms
@@ -1511,9 +1550,11 @@
(map2 mk_set_bd Izs sets))) setss_by_range;
fun mk_tac induct = mk_set_bd_tac m (rtac induct) bd_Cinfinite set_bd_cpowss;
- val thms = map4 (fn goal => fn set_simps => fn induct => fn i =>
- singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal (mk_tac induct set_simps i)))
+ val thms =
+ map4 (fn goal => fn set_simps => fn induct => fn i =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Skip_Proof.prove lthy [] [] goal (mk_tac induct set_simps i))
+ |> Thm.close_derivation)
goals set_simp_thmss inducts ls;
in
map split_conj_thm thms
@@ -1542,7 +1583,8 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
- (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms));
+ (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms))
+ |> Thm.close_derivation;
in
split_conj_thm thm
end;
@@ -1568,7 +1610,8 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
- (mk_incl_min_alg_tac (rtac induct) Fset_set_thmsss alg_set_thms alg_min_alg_thm));
+ (mk_incl_min_alg_tac (rtac induct) Fset_set_thmsss alg_set_thms alg_min_alg_thm))
+ |> Thm.close_derivation;
in
split_conj_thm thm
end;
@@ -1610,7 +1653,8 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
(K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls map_simp_thms
- (transpose set_simp_thmss) Fset_set_thmsss fld_inject_thms)));
+ (transpose set_simp_thmss) Fset_set_thmsss fld_inject_thms)))
+ |> Thm.close_derivation;
in
split_conj_thm thm
end;
@@ -1708,7 +1752,8 @@
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
(K (mk_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
- fld_inject fld_unf set_naturals set_incls set_set_inclss)))
+ fld_inject fld_unf set_naturals set_incls set_set_inclss))
+ |> Thm.close_derivation)
ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
fld_inject_thms fld_unf_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
@@ -1721,37 +1766,58 @@
val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
in
map3 (fn goal => fn pred_def => fn Irel_unfold =>
- Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold))
+ Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold)
+ |> Thm.close_derivation)
goals pred_defs Irel_unfold_thms
end;
val timer = time (timer "additional properties");
val ls' = if m = 1 then [0] else ls
+
+ val Ibnf_common_notes =
+ [(map_uniqueN, [fold_maps map_unique_thm])]
+ |> map (fn (thmN, thms) =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+ val Ibnf_notes =
+ [(map_simpsN, map single folded_map_simp_thms),
+ (set_inclN, set_incl_thmss),
+ (set_set_inclN, map flat set_set_incl_thmsss), (* nicer names? *)
+ (rel_unfoldN, map single Irel_unfold_thms),
+ (pred_unfoldN, map single Ipred_unfold_thms)] @
+ map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
+ |> maps (fn (thmN, thmss) =>
+ map2 (fn b => fn thms =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+ bs thmss)
in
- lthy
- |> note map_uniqueN [fold_maps map_unique_thm]
- |> notes map_simpsN (map single folded_map_simp_thms)
- |> fold2 (fn i => notes (mk_set_simpsN i) o map single) ls' folded_set_simp_thmss
- |> notes set_inclN set_incl_thmss
- |> notes set_set_inclN (map flat set_set_incl_thmsss)
- |> notes rel_unfoldN (map single Irel_unfold_thms)
- |> notes pred_unfoldN (map single Ipred_unfold_thms)
+ lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
end;
+ val common_notes =
+ [(fld_inductN, [fld_induct_thm]),
+ (fld_induct2N, [fld_induct2_thm])]
+ |> map (fn (thmN, thms) =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+ val notes =
+ [(iterN, iter_thms),
+ (iter_uniqueN, iter_unique_thms),
+ (recN, rec_thms),
+ (unf_fldN, unf_fld_thms),
+ (fld_unfN, fld_unf_thms),
+ (unf_injectN, unf_inject_thms),
+ (unf_exhaustN, unf_exhaust_thms),
+ (fld_injectN, fld_inject_thms),
+ (fld_exhaustN, fld_exhaust_thms)]
+ |> map (apsnd (map single))
+ |> maps (fn (thmN, thmss) =>
+ map2 (fn b => fn thms =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+ bs thmss)
in
- lthy
- |> notes iterN (map single iter_thms)
- |> notes iter_uniqueN (map single iter_unique_thms)
- |> notes recN (map single rec_thms)
- |> notes unf_fldN (map single unf_fld_thms)
- |> notes fld_unfN (map single fld_unf_thms)
- |> notes unf_injectN (map single unf_inject_thms)
- |> notes unf_exhaustN (map single unf_exhaust_thms)
- |> notes fld_injectN (map single fld_inject_thms)
- |> notes fld_exhaustN (map single fld_exhaust_thms)
- |> note fld_inductN [fld_induct_thm]
- |> note fld_induct2N [fld_induct2_thm]
+ lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
val _ =