--- a/NEWS Wed Mar 27 14:08:03 2013 +0100
+++ b/NEWS Wed Mar 27 14:19:18 2013 +0100
@@ -106,6 +106,14 @@
rings. INCOMPATIBILITY.
+*** ML ***
+
+* More uniform naming of goal functions for skipped proofs:
+
+ Skip_Proof.prove ~> Goal.prove_sorry
+ Skip_Proof.prove_global ~> Goal.prove_sorry_global
+
+
*** System ***
* Discontinued "isabelle usedir" option -P (remote path) and -r (reset
--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Mar 27 14:19:18 2013 +0100
@@ -175,7 +175,7 @@
[]
else
map (fn goal =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_comp_set_alt_tac ctxt (collect_set_natural_of_bnf outer))
|> Thm.close_derivation)
@@ -209,7 +209,7 @@
val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
in
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
|> Thm.close_derivation
end;
@@ -324,7 +324,7 @@
val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
in
- Skip_Proof.prove lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
+ Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
end;
fun in_bd_tac _ =
@@ -426,7 +426,7 @@
val in_alt = mk_in (drop n Asets) bnf_sets T;
val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
in
- Skip_Proof.prove lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
+ Goal.prove_sorry lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
end;
fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
@@ -501,7 +501,7 @@
val in_alt = mk_in (permute_rev Asets) bnf_sets T;
val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
in
- Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
+ Goal.prove_sorry lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
|> Thm.close_derivation
end;
--- a/src/HOL/BNF/Tools/bnf_def.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Mar 27 14:19:18 2013 +0100
@@ -923,7 +923,7 @@
(*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
in
- Skip_Proof.prove lthy [] [] goal (K (mk_collect_set_natural_tac (#set_natural axioms)))
+ Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_natural_tac (#set_natural axioms)))
|> Thm.close_derivation
end;
@@ -937,7 +937,7 @@
(Logic.list_implies (prems_mono, HOLogic.mk_Trueprop
(mk_subset (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
in
- Skip_Proof.prove lthy [] [] in_mono_goal (K (mk_in_mono_tac live))
+ Goal.prove_sorry lthy [] [] in_mono_goal (K (mk_in_mono_tac live))
|> Thm.close_derivation
end;
@@ -951,7 +951,7 @@
(Logic.list_implies (prems_cong, HOLogic.mk_Trueprop
(HOLogic.mk_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA'))));
in
- Skip_Proof.prove lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
+ Goal.prove_sorry lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
|> Thm.close_derivation
end;
@@ -993,7 +993,7 @@
fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ e1s @ e2s @ p1s @ p2s)
(Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
in
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry 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
@@ -1009,7 +1009,7 @@
val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
@@ -1026,7 +1026,7 @@
val mono_prems = mk_srel_prems mk_subset;
val mono_concl = mk_srel_concl (uncurry mk_subset);
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
(mk_srel_mono_tac srel_O_Grs (Lazy.force in_mono))
|> Thm.close_derivation
@@ -1037,7 +1037,7 @@
val cong_prems = mk_srel_prems (curry HOLogic.mk_eq);
val cong_concl = mk_srel_concl HOLogic.mk_eq;
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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
@@ -1048,7 +1048,7 @@
fun mk_srel_Id () =
let val srelAsAs = mk_bnf_srel self_setRTs CA' CA' in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (Term.list_comb (srelAsAs, map Id_const As'), Id_const CA')))
(mk_srel_Id_tac live (Lazy.force srel_Gr) (#map_id axioms))
@@ -1063,13 +1063,13 @@
val lhs = Term.list_comb (srelBsAs, map mk_converse Rs);
val rhs = mk_converse (Term.list_comb (srel, Rs));
val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
- val le_thm = Skip_Proof.prove lthy [] [] le_goal
+ val le_thm = Goal.prove_sorry lthy [] [] le_goal
(mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal (fn _ => mk_srel_converse_tac le_thm)
+ Goal.prove_sorry lthy [] [] goal (fn _ => mk_srel_converse_tac le_thm)
|> Thm.close_derivation
end;
@@ -1083,7 +1083,7 @@
val rhs = mk_rel_comp (Term.list_comb (srel, Rs), Term.list_comb (srelBsCs, Ss));
val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
(Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
@@ -1105,7 +1105,7 @@
val goal =
fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal (mk_in_srel_tac srel_O_Grs (length bnf_sets))
+ Goal.prove_sorry lthy [] [] goal (mk_in_srel_tac srel_O_Grs (length bnf_sets))
|> Thm.close_derivation
end;
@@ -1238,12 +1238,12 @@
mk_unfold_thms_then_tac lthy one_step_defs wit_tac;
val wit_goals = map mk_conjunction_balanced' wit_goalss;
val wit_thms =
- Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
+ Goal.prove_sorry lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
in
- map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
+ map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
|> (fn thms => after_qed (map single thms @ wit_thms) lthy)
end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Mar 27 14:19:18 2013 +0100
@@ -474,7 +474,7 @@
fold_rev Logic.all [w, u]
(mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
(certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
|> Thm.close_derivation
@@ -801,7 +801,7 @@
val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
val thm =
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
nested_set_natural's pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
@@ -852,7 +852,7 @@
(nested_map_ids'' @ nesting_map_ids'') rec_defs) fp_rec_thms ctr_defss;
fun prove goal tac =
- Skip_Proof.prove lthy [] [] goal (tac o #context)
+ Goal.prove_sorry lthy [] [] goal (tac o #context)
|> Thm.close_derivation;
in
(map2 (map2 prove) fold_goalss fold_tacss, map2 (map2 prove) rec_goalss rec_tacss)
@@ -955,7 +955,7 @@
val strong_goal = mk_goal strong_rs;
fun prove dtor_coinduct' goal =
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
exhaust_thms ctr_defss disc_thmsss sel_thmsss)
|> singleton (Proof_Context.export names_lthy lthy)
@@ -1032,7 +1032,7 @@
fp_rec_thms pre_map_defs ctr_defss;
fun prove goal tac =
- Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
+ Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
@@ -1068,7 +1068,7 @@
map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
fun prove goal tac =
- Skip_Proof.prove lthy [] [] goal (tac o #context)
+ Goal.prove_sorry lthy [] [] goal (tac o #context)
|> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
|> Thm.close_derivation;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Mar 27 14:19:18 2013 +0100
@@ -247,7 +247,7 @@
val rhs =
Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_map_comp_id_tac map_comp))
|> Thm.close_derivation
@@ -265,7 +265,7 @@
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
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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
@@ -286,7 +286,7 @@
fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl)))
prems concls xFs xFs_copy;
in
- map (fn goal => Skip_Proof.prove lthy [] [] goal
+ map (fn goal => Goal.prove_sorry lthy [] [] goal
(K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals
end;
@@ -348,7 +348,7 @@
fold_rev Logic.all (x :: As @ Bs @ ss)
(Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
in
- map (fn goals => map (fn goal => Skip_Proof.prove lthy [] [] goal
+ map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal
(K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
end;
@@ -361,7 +361,7 @@
val goal = fold_rev Logic.all ss
(HOLogic.mk_Trueprop (mk_tcoalg passiveAs activeAs ss))
in
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(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))
@@ -428,7 +428,7 @@
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 =
- Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def))
+ Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
|> Thm.close_derivation;
in
(map prove image_goals, map prove elim_goals)
@@ -441,7 +441,7 @@
val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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
@@ -457,7 +457,7 @@
val concl =
HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
in
- Skip_Proof.prove lthy [] []
+ 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)))
(K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms))
@@ -470,7 +470,7 @@
(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
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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))
@@ -485,7 +485,7 @@
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
- Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
+ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_mor_UNIV_tac morE_thms mor_def))
|> Thm.close_derivation
end;
@@ -495,7 +495,7 @@
val maps = map2 (fn Ds => fn bnf => Term.list_comb
(mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs;
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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))
@@ -508,7 +508,7 @@
mk_sum_case (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
s's sum_ss map_Inls;
in
- Skip_Proof.prove lthy [] []
+ 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)))
(K (mk_mor_sum_case_tac ks mor_UNIV_thm))
@@ -642,14 +642,14 @@
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))
+ Goal.prove_sorry 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
+ Goal.prove_sorry lthy [] [] goal
(K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k))
|> Thm.close_derivation)
goals defsk defsi rec_Sucs)
@@ -680,7 +680,7 @@
ss zs setssAs hsetssAs;
in
map2 (map2 (fn goal => fn thms =>
- Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hin_tac thms))
+ Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hin_tac thms))
|> Thm.close_derivation))
set_incl_hin_goalss set_hset_incl_hset_thmsss
end;
@@ -716,7 +716,7 @@
in
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
+ (Goal.prove_sorry lthy [] [] goal
(mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs))
|> Thm.close_derivation)
goals ctss hset_rec_0ss' hset_rec_Sucss'
@@ -731,7 +731,7 @@
(Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
in
map3 (fn goal => fn hset_defs => fn hset_rec_minimal =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_hset_minimal_tac n hset_defs hset_rec_minimal)
|> Thm.close_derivation)
goals hset_defss' hset_rec_minimal_thms
@@ -757,7 +757,7 @@
in
map5 (fn j => fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
+ (Goal.prove_sorry 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)))
|> Thm.close_derivation)
@@ -778,7 +778,7 @@
mk_prem x B], mk_concl j T i f x))) ks fs zs Bs) ls passiveAs;
in
map3 (map3 (fn goal => fn hset_def => fn mor_hset_rec =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (mk_mor_hset_tac hset_def mor_hset_rec))
|> Thm.close_derivation))
goalss hset_defss' mor_hset_rec_thmss
@@ -841,7 +841,7 @@
(mk_bis As Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
val concl = HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs_copy);
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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))
@@ -860,7 +860,7 @@
(bis_le, Library.foldr1 HOLogic.mk_conj
(map6 mk_conjunct Rs ss s's zs z's relsAsBs))
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
(mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
(K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss))
@@ -868,7 +868,7 @@
end;
val bis_converse_thm =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
(Logic.mk_implies
(HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
@@ -884,7 +884,7 @@
val concl =
HOLogic.mk_Trueprop (mk_bis As Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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_srel_thm srel_congs srel_Os))
@@ -896,7 +896,7 @@
val concl =
HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map2 mk_Gr Bs fs));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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_srel_thm srel_Grs mor_image_thms morE_thms coalg_in_thms)
@@ -918,7 +918,7 @@
val concl =
HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map (mk_UNION Idx) Ris));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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)
@@ -974,7 +974,7 @@
end;
val sbis_lsbis_thm =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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))
@@ -991,7 +991,7 @@
val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs)
(Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
in
- map3 (fn goal => fn i => fn def => Skip_Proof.prove lthy [] [] goal
+ 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
end;
@@ -1002,7 +1002,7 @@
(Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs;
in
map3 (fn goal => fn l_incl => fn incl_l =>
- Skip_Proof.prove lthy [] [] goal
+ 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)
@@ -1279,7 +1279,7 @@
val hset_strTss = map (fn i => map2 (mk_hset strTAs i) ls passiveAs) ks;
val coalgT_thm =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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)
|> Thm.close_derivation;
@@ -1294,7 +1294,7 @@
(mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo))
(mk_cexp sbd sbd);
val card_of_carT =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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))
@@ -1323,7 +1323,7 @@
map6 (fn i => fn goals =>
fn carT_def => fn strT_def => fn isNode_def => fn set_naturals =>
map2 (fn goal => fn set_natural =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_carT_set_tac n i carT_def strT_def isNode_def set_natural)
|> Thm.close_derivation)
goals (drop m set_naturals))
@@ -1365,7 +1365,7 @@
in
map5 (fn j => fn goal => fn cts => fn set_incl_hsets => fn set_hset_incl_hsetss =>
singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
+ (Goal.prove_sorry lthy [] [] goal
(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'
@@ -1390,7 +1390,7 @@
in
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 [] []
+ Goal.prove_sorry 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)
@@ -1569,7 +1569,7 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss))
|> Thm.close_derivation);
@@ -1588,7 +1588,7 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
val length_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_length_Lev_tac cts Lev_0s Lev_Sucs))
|> Thm.close_derivation);
@@ -1601,7 +1601,7 @@
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))
+ Goal.prove_sorry lthy [] [] goal (K (mk_length_Lev'_tac length_Lev))
|> Thm.close_derivation) goals length_Levs;
in
(length_Levs, length_Levs')
@@ -1618,7 +1618,7 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)))
|> Thm.close_derivation;
@@ -1642,7 +1642,7 @@
val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl];
val rv_last = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)))
|> Thm.close_derivation;
@@ -1666,7 +1666,7 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] []
+ (Goal.prove_sorry 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)))
@@ -1707,7 +1707,7 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
val set_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
|> Thm.close_derivation;
@@ -1745,7 +1745,7 @@
val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+ (Goal.prove_sorry 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)))
|> Thm.close_derivation;
@@ -1759,7 +1759,7 @@
end;
val mor_beh_thm =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
(mk_mor_beh_tac m mor_def mor_cong_thm
@@ -1797,19 +1797,19 @@
val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
in
map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(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
+ val coalg_final_thm = Goal.prove_sorry 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))
|> Thm.close_derivation;
- val mor_T_final_thm = Skip_Proof.prove lthy [] [] (fold_rev Logic.all As
+ val mor_T_final_thm = Goal.prove_sorry 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))
@@ -1912,14 +1912,14 @@
val (mor_Rep_thm, mor_Abs_thm) =
let
val mor_Rep =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
(mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
map_comp_id_thms map_congL_thms)
|> Thm.close_derivation;
val mor_Abs =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
(mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses)
|> Thm.close_derivation;
@@ -1966,7 +1966,7 @@
val morEs' = map (fn thm =>
(thm OF [tcoalg_thm RS mor_final_thm, UNIV_I]) RS sym) morE_thms;
in
- Skip_Proof.prove lthy [] []
+ 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))))
(K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
@@ -1982,7 +1982,7 @@
(map2 (fn R => fn T => mk_subset R (Id_const T)) TRs Ts));
val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
in
- `split_conj_thm (Skip_Proof.prove lthy [] [] goal
+ `split_conj_thm (Goal.prove_sorry 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))
@@ -1999,7 +1999,7 @@
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs));
- val unique_mor = Skip_Proof.prove lthy [] []
+ val unique_mor = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs)
(Logic.list_implies (prems, unique)))
(K (mk_unique_mor_tac raw_coind_thms bis_image2_thm))
@@ -2018,7 +2018,7 @@
val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm];
- val unique_mor = Skip_Proof.prove lthy [] []
+ val unique_mor = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
(K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
|> Thm.close_derivation;
@@ -2081,7 +2081,7 @@
val goals = map3 mk_goal dtors ctors FTs;
in
map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms)
|> Thm.close_derivation)
goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms
@@ -2169,7 +2169,7 @@
val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
in
map3 (fn goal => fn unfold => fn map_cong =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms)
|> Thm.close_derivation)
goals dtor_unfold_thms map_congs
@@ -2221,7 +2221,7 @@
val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []);
val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV}
- (Skip_Proof.prove lthy [] [] dtor_srel_coinduct_goal
+ (Goal.prove_sorry lthy [] [] dtor_srel_coinduct_goal
(K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
|> Thm.close_derivation);
@@ -2253,7 +2253,7 @@
val strong_prems = mk_prems true;
val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
- val dtor_map_coinduct = Skip_Proof.prove lthy [] [] dtor_map_coinduct_goal
+ val dtor_map_coinduct = Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
(K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
|> Thm.close_derivation;
@@ -2261,13 +2261,13 @@
val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] []
+ (Goal.prove_sorry lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl)))
(K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids)))
|> Thm.close_derivation;
val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] []
+ (Goal.prove_sorry lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl)))
(K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
(tcoalg_thm RS bis_Id_on_thm))))
@@ -2383,7 +2383,7 @@
val cTs = map (SOME o certifyT lthy) FTs';
val maps =
map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (mk_map_tac m n cT unfold map_comp' map_cong))
|> Thm.close_derivation)
goals cTs dtor_unfold_thms map_comp's map_congs;
@@ -2399,7 +2399,7 @@
HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
fs_maps gs_maps fgs_maps)))
in
- split_conj_thm (Skip_Proof.prove lthy [] [] goal
+ split_conj_thm (Goal.prove_sorry lthy [] [] goal
(K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm))
|> Thm.close_derivation)
end;
@@ -2414,7 +2414,7 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) us fs_maps));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
(mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps)
|> Thm.close_derivation
@@ -2448,7 +2448,7 @@
(mk_goals (uncurry mk_subset));
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
+ Goal.prove_sorry lthy [] [] goal
(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');
@@ -2458,7 +2458,7 @@
(mk_goals HOLogic.mk_eq);
in
map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (mk_dtor_set_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'
@@ -2489,7 +2489,7 @@
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)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
(mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_natural'ss))
|> Thm.close_derivation)
goals ctss hset_rec_0ss' hset_rec_Sucss';
@@ -2512,7 +2512,7 @@
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)
+ (Goal.prove_sorry 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)
@@ -2557,7 +2557,7 @@
(map4 mk_map_cong setss_by_bnf Jzs fs_maps fs_copy_maps));
val thm = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
+ (Goal.prove_sorry lthy [] [] goal
(K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss
set_hset_thmss set_hset_hset_thmsss)))
|> Thm.close_derivation
@@ -2593,7 +2593,7 @@
val goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps)
(Logic.mk_implies (wpull_prem, coalg));
in
- Skip_Proof.prove lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms
+ Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms
set_natural'ss pickWP_assms_tacs)
|> Thm.close_derivation
end;
@@ -2617,11 +2617,11 @@
val pick_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps)
(Logic.mk_implies (wpull_prem, mor_pick));
in
- (Skip_Proof.prove lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms
+ (Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms
map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
- Skip_Proof.prove lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
+ Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
- Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
+ Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
map_comp's) |> Thm.close_derivation)
end;
@@ -2644,7 +2644,7 @@
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
+ singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal
(mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_natural'ss
map_wpull_thms pickWP_assms_tacs))
|> Thm.close_derivation)
@@ -2838,7 +2838,7 @@
val goals = map5 mk_goal setss_by_range ys ys_copy ys'_copy ls;
in
map2 (fn goal => fn induct =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms)
|> Thm.close_derivation)
goals dtor_hset_induct_thms
@@ -2915,7 +2915,7 @@
map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
@@ -2931,7 +2931,7 @@
val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
in
map3 (fn goal => fn srel_def => fn dtor_Jsrel =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_ctor_or_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel)
|> Thm.close_derivation)
goals srel_defs dtor_Jsrel_thms
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Mar 27 14:19:18 2013 +0100
@@ -183,7 +183,7 @@
val rhs = Term.list_comb (mapAsCs,
take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_map_comp_id_tac map_comp))
|> Thm.close_derivation
@@ -200,7 +200,7 @@
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
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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
@@ -263,7 +263,7 @@
(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)) |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] goal (K (mk_alg_set_tac alg_def)) |> Thm.close_derivation)
goals
end;
@@ -274,7 +274,7 @@
val goal = fold_rev Logic.all ss
(HOLogic.mk_Trueprop (mk_talg passiveAs activeAs ss))
in
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
|> Thm.close_derivation
end;
@@ -291,7 +291,7 @@
fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (alg_prem, concl))) concls;
in
map2 (fn goal => fn alg_set =>
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms))
|> Thm.close_derivation)
goals alg_set_thms
@@ -359,7 +359,7 @@
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 =
- Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
+ Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
in
(map prove image_goals, map prove elim_goals)
end;
@@ -369,7 +369,7 @@
val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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
@@ -383,7 +383,7 @@
val concl =
HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
in
- Skip_Proof.prove lthy [] []
+ 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)))
(K (mk_mor_comp_tac mor_def set_natural'ss map_comp_id_thms))
@@ -401,7 +401,7 @@
map4 mk_inv_prem fs inv_fs Bs B's);
val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
(Logic.list_implies (prems, concl)))
(K (mk_mor_inv_tac alg_def mor_def
@@ -415,7 +415,7 @@
(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
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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))
@@ -427,7 +427,7 @@
val maps = map2 (fn Ds => fn bnf => Term.list_comb
(mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs;
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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))
@@ -440,7 +440,7 @@
mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s))
s's prod_ss map_fsts;
in
- Skip_Proof.prove lthy [] []
+ 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)))
(K (mk_mor_convol_tac ks mor_def))
@@ -455,7 +455,7 @@
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
- Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
+ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_mor_UNIV_tac m morE_thms mor_def))
|> Thm.close_derivation
end;
@@ -485,7 +485,7 @@
HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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
@@ -507,7 +507,7 @@
val alg = HOLogic.mk_Trueprop
(mk_alg passive_UNIVs B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
- val copy_str_thm = Skip_Proof.prove lthy [] []
+ val copy_str_thm = Goal.prove_sorry 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))
@@ -515,7 +515,7 @@
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 [] []
+ val copy_alg_thm = Goal.prove_sorry 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))
@@ -525,7 +525,7 @@
(list_exists_free s's
(HOLogic.mk_conj (mk_alg passive_UNIVs B's s's,
mk_iso B's s's Bs ss inv_fs fs_copy)));
- val ex_copy_alg_thm = Skip_Proof.prove lthy [] []
+ val ex_copy_alg_thm = Goal.prove_sorry 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))
@@ -602,7 +602,7 @@
val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd
(Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(fold_rev Logic.all idxs (Logic.list_implies ([prem], concl)))
(K (mk_bd_limit_tac n suc_bd_Cinfinite))
|> Thm.close_derivation
@@ -643,7 +643,7 @@
val goal = fold_rev Logic.all (idx :: As @ ss)
(Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
- val min_algs_thm = Skip_Proof.prove lthy [] [] goal
+ val min_algs_thm = Goal.prove_sorry lthy [] [] goal
(K (mk_min_algs_tac suc_bd_worel in_cong'_thms))
|> Thm.close_derivation;
@@ -655,7 +655,7 @@
val monos =
map2 (fn goal => fn min_algs =>
- Skip_Proof.prove lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
+ Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
|> Thm.close_derivation)
(map mk_mono_goal min_algss) min_algs_thms;
@@ -667,7 +667,7 @@
val card_ct = certify lthy (Term.absfree idx' card_conjunction);
val card_of = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] []
+ (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_bd_sums
@@ -681,7 +681,7 @@
val least_ct = certify lthy (Term.absfree idx' least_conjunction);
val least = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] []
+ (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
@@ -736,13 +736,13 @@
val min_algs = map (mk_min_alg As ss) ks;
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
+ 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 sum_Cinfinite
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 [] []
+ fun mk_card_of_thm min_alg def = Goal.prove_sorry 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
@@ -750,7 +750,7 @@
|> 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 [] []
+ fun mk_least_thm min_alg B def = Goal.prove_sorry 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))
@@ -760,7 +760,7 @@
val incl_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
val incl_min_algs = map (mk_min_alg passive_UNIVs ss) ks;
- val incl = Skip_Proof.prove lthy [] []
+ val incl = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss)
(Logic.mk_implies (incl_prem,
HOLogic.mk_Trueprop (mk_mor incl_min_algs ss Bs ss active_ids))))
@@ -845,12 +845,12 @@
val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks;
(*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
- val alg_init_thm = Skip_Proof.prove lthy [] []
+ val alg_init_thm = Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_alg passive_UNIVs car_inits str_inits))
(K (rtac alg_min_alg_thm 1))
|> Thm.close_derivation;
- val alg_select_thm = Skip_Proof.prove lthy [] []
+ val alg_select_thm = Goal.prove_sorry 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)
@@ -866,7 +866,7 @@
(mk_mor car_inits str_inits Bs ss
(map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(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))
@@ -878,7 +878,7 @@
val prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
val concl = HOLogic.mk_Trueprop
(list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
- val ex_mor = Skip_Proof.prove lthy [] []
+ val ex_mor = Goal.prove_sorry 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)
@@ -891,7 +891,7 @@
fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
val unique = HOLogic.mk_Trueprop
(Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
- val unique_mor = Skip_Proof.prove lthy [] []
+ val unique_mor = Goal.prove_sorry lthy [] []
(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
@@ -926,7 +926,7 @@
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 mk_Ball car_inits init_phis));
in
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry 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
@@ -955,7 +955,7 @@
val Abs_inverses = map #Abs_inverse T_loc_infos;
fun mk_inver_thm mk_tac rep abs X thm =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_inver rep abs X))
(K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
|> Thm.close_derivation;
@@ -1034,14 +1034,14 @@
fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases];
val bijs = map3 mk_bij Rep_injects Reps Rep_casess;
val mor_Rep =
- Skip_Proof.prove lthy [] []
+ Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
(mk_mor_Rep_tac ctor_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 [] []
+ Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
(K (mk_mor_Abs_tac inv inver_Abss inver_Reps))
|> Thm.close_derivation;
@@ -1094,7 +1094,7 @@
val ct = certify lthy fold_fun
in
singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove 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 ex_mor (mor_comp RS mor_cong))))
|> Thm.close_derivation
@@ -1109,7 +1109,7 @@
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 = Skip_Proof.prove lthy [] []
+ val unique_mor = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (ss @ fs) (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))
@@ -1178,7 +1178,7 @@
val goals = map3 mk_goal dtors ctors FTs;
in
map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_congL =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_fold_thms))
|> Thm.close_derivation)
goals dtor_defs ctor_fold_thms map_comp_id_thms map_congL_thms
@@ -1259,7 +1259,7 @@
val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
in
map2 (fn goal => fn foldx =>
- Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
+ Goal.prove_sorry lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
|> Thm.close_derivation)
goals ctor_fold_thms
end;
@@ -1292,7 +1292,7 @@
val goal = Logic.list_implies (prems, concl);
in
- (Skip_Proof.prove lthy [] []
+ (Goal.prove_sorry lthy [] []
(fold_rev Logic.all (phis @ Izs) goal)
(K (mk_ctor_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm
Rep_inverses Abs_inverses Reps))
@@ -1336,7 +1336,7 @@
val goal = Logic.list_implies (prems, concl);
in
(singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
+ (Goal.prove_sorry lthy [] [] goal
(mk_ctor_induct2_tac cTs cts ctor_induct_thm weak_ctor_induct_thms))
|> Thm.close_derivation,
rev (Term.add_tfrees goal []))
@@ -1408,7 +1408,7 @@
val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
val maps =
map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong =>
- Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
+ Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
|> Thm.close_derivation)
goals ctor_fold_thms map_comp_id_thms map_congs;
in
@@ -1424,7 +1424,7 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) us fs_maps));
- val unique = Skip_Proof.prove lthy [] []
+ val unique = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
(K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
|> Thm.close_derivation;
@@ -1468,7 +1468,7 @@
val goalss =
map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss;
val setss = map (map2 (fn foldx => fn goal =>
- Skip_Proof.prove lthy [] [] goal (K (mk_set_tac foldx)) |> Thm.close_derivation)
+ Goal.prove_sorry lthy [] [] goal (K (mk_set_tac foldx)) |> Thm.close_derivation)
ctor_fold_thms) goalss;
fun mk_simp_goal pas_set act_sets sets ctor z set =
@@ -1482,7 +1482,7 @@
ls setss_by_range;
val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
|> Thm.close_derivation)
set_natural'ss) ls simp_goalss setss;
@@ -1530,7 +1530,7 @@
val thms =
map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets ctor_sets i))
+ (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i))
|> Thm.close_derivation)
goals csetss ctor_set_thmss inducts ls;
in
@@ -1557,7 +1557,7 @@
val thms =
map4 (fn goal => fn ctor_sets => fn induct => fn i =>
singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal (mk_tac induct ctor_sets i))
+ (Goal.prove_sorry lthy [] [] goal (mk_tac induct ctor_sets i))
|> Thm.close_derivation)
goals ctor_set_thmss inducts ls;
in
@@ -1586,7 +1586,7 @@
(map4 mk_map_cong setss_by_bnf Izs fs_maps fs_copy_maps));
val thm = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
+ (Goal.prove_sorry lthy [] [] goal
(mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs ctor_map_thms))
|> Thm.close_derivation;
in
@@ -1613,7 +1613,7 @@
(map3 mk_incl Izs setss_by_bnf ks));
val thm = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
+ (Goal.prove_sorry lthy [] [] goal
(mk_incl_min_alg_tac (rtac induct) Fset_set_thmsss alg_set_thms alg_min_alg_thm))
|> Thm.close_derivation;
in
@@ -1655,7 +1655,7 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals));
val thm = singleton (Proof_Context.export names_lthy lthy)
- (Skip_Proof.prove lthy [] [] goal
+ (Goal.prove_sorry lthy [] [] goal
(K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
(transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms)))
|> Thm.close_derivation;
@@ -1756,7 +1756,7 @@
map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
@@ -1772,7 +1772,7 @@
val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
in
map3 (fn goal => fn srel_def => fn ctor_Isrel =>
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(mk_ctor_or_dtor_rel_tac srel_def Irel_defs Isrel_defs ctor_Isrel)
|> Thm.close_derivation)
goals srel_defs ctor_Isrel_thms
--- a/src/HOL/BNF/Tools/bnf_wrap.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML Wed Mar 27 14:19:18 2013 +0100
@@ -381,7 +381,7 @@
HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u',
Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs));
in
- Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
+ Goal.prove_sorry lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
|> Thm.close_derivation
end;
@@ -415,7 +415,7 @@
val m = the_single ms;
val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
in
- Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
+ Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy)
end;
@@ -426,7 +426,7 @@
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
nth exist_xs_u_eq_ctrs (k - 1));
in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
(nth distinct_thms (2 - k)) uexhaust_thm)
|> Thm.close_derivation
@@ -470,7 +470,7 @@
HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
fun prove tac goal =
- Skip_Proof.prove lthy [] [] goal (K tac)
+ Goal.prove_sorry lthy [] [] goal (K tac)
|> Thm.close_derivation;
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
@@ -495,7 +495,7 @@
fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
in
- Skip_Proof.prove lthy [] [] goal (fn _ =>
+ Goal.prove_sorry lthy [] [] goal (fn _ =>
mk_disc_exhaust_tac n exhaust_thm discI_thms)
|> Thm.close_derivation
end;
@@ -514,7 +514,7 @@
val goals = map3 mk_goal ctrs udiscs uselss;
in
map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_collapse_tac ctxt m discD sel_thms)
|> Thm.close_derivation
|> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
@@ -540,7 +540,7 @@
val uncollapse_thms =
map (fn NONE => Drule.dummy_thm | SOME thm => thm RS sym) collapse_thm_opts;
in
- [Skip_Proof.prove lthy [] [] goal (fn _ =>
+ [Goal.prove_sorry lthy [] [] goal (fn _ =>
mk_expand_tac n ms (inst_thm u disc_exhaust_thm)
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
disc_exclude_thmsss')]
@@ -553,7 +553,7 @@
fun mk_body f usels = Term.list_comb (f, usels);
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
in
- [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
|> map Thm.close_derivation
|> Proof_Context.export names_lthy lthy
@@ -574,8 +574,8 @@
mk_Trueprop_eq (ufcase, vgcase));
val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
in
- (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms),
- Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1)))
+ (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms),
+ Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
|> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
end;
@@ -596,12 +596,12 @@
(map3 mk_disjunct xctrs xss xfs)));
val split_thm =
- Skip_Proof.prove lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
(fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy);
val split_asm_thm =
- Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
mk_split_asm_tac ctxt split_thm)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy);
@@ -646,7 +646,7 @@
end;
fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
- map2 (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])) goalss tacss
+ map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
|> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Mar 27 14:19:18 2013 +0100
@@ -355,7 +355,7 @@
val rewrites = def_thms @ map mk_meta_eq rec_rewrites;
val char_thms' =
- map (fn eqn => Skip_Proof.prove_global thy' [] [] eqn
+ map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn
(fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
in (thy', char_thms' @ char_thms) end;
@@ -377,7 +377,7 @@
val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
val f = Free ("f", Ts ---> U);
in
- Skip_Proof.prove_global thy [] []
+ Goal.prove_sorry_global thy [] []
(Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
(map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
@@ -416,7 +416,7 @@
val inj_thms' = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) inj_thms;
val inj_thm =
- Skip_Proof.prove_global thy5 [] []
+ Goal.prove_sorry_global thy5 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
(fn _ => EVERY
[(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
@@ -442,7 +442,7 @@
val inj_thms'' = map (fn r => r RS datatype_injI) (Datatype_Aux.split_conj_thm inj_thm);
val elem_thm =
- Skip_Proof.prove_global thy5 [] []
+ Goal.prove_sorry_global thy5 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
(fn _ =>
EVERY [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
@@ -480,7 +480,7 @@
if length descr = 1 then []
else
drop (length newTs) (Datatype_Aux.split_conj_thm
- (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
+ (Goal.prove_sorry_global thy5 [] [] iso_t (fn _ => EVERY
[(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
@@ -511,7 +511,7 @@
val inj_thms = map fst newT_iso_inj_thms;
val rewrites = @{thm o_def} :: constr_defs @ map (mk_meta_eq o #2) newT_iso_axms;
in
- Skip_Proof.prove_global thy5 [] [] eqn
+ Goal.prove_sorry_global thy5 [] [] eqn
(fn _ => EVERY
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
@@ -537,7 +537,7 @@
fun prove [] = []
| prove (t :: ts) =
let
- val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
+ val dist_thm = Goal.prove_sorry_global thy5 [] [] t (fn _ =>
EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
in dist_thm :: Drule.zero_var_indexes (dist_thm RS not_sym) :: prove ts end;
in prove end;
@@ -555,7 +555,7 @@
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
Lim_inject, Suml_inject, Sumr_inject])
in
- Skip_Proof.prove_global thy5 [] [] t
+ Goal.prove_sorry_global thy5 [] [] t
(fn _ => EVERY
[rtac iffI 1,
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
@@ -610,7 +610,7 @@
val cert = cterm_of thy6;
val indrule_lemma =
- Skip_Proof.prove_global thy6 [] []
+ Goal.prove_sorry_global thy6 [] []
(Logic.mk_implies
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls)))
@@ -629,7 +629,7 @@
val dt_induct_prop = Datatype_Prop.make_ind descr;
val dt_induct =
- Skip_Proof.prove_global thy6 []
+ Goal.prove_sorry_global thy6 []
(Logic.strip_imp_prems dt_induct_prop)
(Logic.strip_imp_concl dt_induct_prop)
(fn {prems, ...} =>
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Mar 27 14:19:18 2013 +0100
@@ -86,7 +86,7 @@
(HOL_basic_ss addsimps
(map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)));
fun prove prop =
- Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+ Goal.prove_sorry_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
|> Simpdata.mk_eq;
in (map prove (triv_injects @ injects @ distincts), prove refl) end;
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Mar 27 14:19:18 2013 +0100
@@ -50,7 +50,7 @@
refl RS
(nth (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i RSN (2, rev_mp));
in
- Skip_Proof.prove_global thy []
+ Goal.prove_sorry_global thy []
(Logic.strip_imp_prems t)
(Logic.strip_imp_concl t)
(fn {prems, ...} =>
@@ -208,7 +208,7 @@
(((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
in
- Datatype_Aux.split_conj_thm (Skip_Proof.prove_global thy1 [] []
+ Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts)) (K tac))
end;
@@ -248,7 +248,7 @@
val rec_thms =
map (fn t =>
- Skip_Proof.prove_global thy2 [] [] t
+ Goal.prove_sorry_global thy2 [] [] t
(fn _ => EVERY
[rewrite_goals_tac reccomb_defs,
rtac @{thm the1_equality} 1,
@@ -330,7 +330,7 @@
val case_thms =
(map o map) (fn t =>
- Skip_Proof.prove_global thy2 [] [] t
+ Goal.prove_sorry_global thy2 [] [] t
(fn _ =>
EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
(Datatype_Prop.make_cases case_names descr thy2);
@@ -363,8 +363,8 @@
EVERY [rtac exhaustion' 1,
ALLGOALS (asm_simp_tac (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))];
in
- (Skip_Proof.prove_global thy [] [] t1 (K tac),
- Skip_Proof.prove_global thy [] [] t2 (K tac))
+ (Goal.prove_sorry_global thy [] [] t1 (K tac),
+ Goal.prove_sorry_global thy [] [] t2 (K tac))
end;
val split_thm_pairs =
@@ -384,7 +384,7 @@
fun prove_weak_case_congs new_type_names case_names descr thy =
let
fun prove_weak_case_cong t =
- Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
val weak_case_congs =
@@ -405,7 +405,7 @@
fun tac i 0 = EVERY [TRY (rtac disjI1 i), hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
| tac i n = rtac disjI2 i THEN tac i (n - 1);
in
- Skip_Proof.prove_global thy [] [] t
+ Goal.prove_sorry_global thy [] [] t
(fn _ =>
EVERY [rtac allI 1,
Datatype_Aux.exh_tac (K exhaustion) 1,
@@ -428,7 +428,7 @@
val [v] = Term.add_vars (concl_of nchotomy') [];
val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
in
- Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} =>
let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) in
EVERY [
--- a/src/HOL/Tools/Function/size.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/Function/size.ML Wed Mar 27 14:19:18 2013 +0100
@@ -159,7 +159,7 @@
fun prove_unfolded_size_eqs size_ofp fs =
if null recTs2 then []
- else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs []
+ else Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
map (mk_unfolded_size_eq (AList.lookup op =
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
@@ -193,7 +193,7 @@
fun prove_size_eqs p size_fns size_ofp simpset =
maps (fn (((_, (_, _, constrs)), size_const), T) =>
- map (fn constr => Drule.export_without_context (Skip_Proof.prove ctxt [] []
+ map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
(gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
size_ofp size_const T constr)
(fn _ => simp_tac simpset 1))) constrs)
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Mar 27 14:19:18 2013 +0100
@@ -107,7 +107,7 @@
val tac = ALLGOALS (rtac rule)
THEN ALLGOALS (simp_tac rew_ss)
THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
- val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
+ val simp = Goal.prove_sorry lthy' [v] [] eq (K tac);
in (simp, lthy') end;
end;
@@ -144,7 +144,7 @@
ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}]));
- in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
+ in (map (fn prop => Goal.prove_sorry lthy [v] [] prop tac) eqs, lthy) end;
in
lthy
|> random_aux_primrec aux_eq'
@@ -165,7 +165,7 @@
let
val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
- in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
+ in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
val b = Binding.conceal (Binding.qualify true prfx
(Binding.qualify true name (Binding.name "simps")));
in
--- a/src/HOL/Tools/enriched_type.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/enriched_type.ML Wed Mar 27 14:19:18 2013 +0100
@@ -125,7 +125,7 @@
(mapper21 $ (mapper32 $ x), mapper31 $ x);
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
- fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop
+ fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
(K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
THEN' Simplifier.asm_lr_simp_tac compositionality_ss
THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
@@ -148,7 +148,7 @@
val rhs = HOLogic.id_const T;
val (id_prop, identity_prop) = pairself
(HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
- fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop
+ fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
(K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss)));
in (id_prop, prove_identity) end;
--- a/src/HOL/Tools/inductive.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Mar 27 14:19:18 2013 +0100
@@ -363,7 +363,7 @@
fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
(message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
" Proving monotonicity ...";
- (if skip_mono then Skip_Proof.prove else Goal.prove_future) ctxt
+ (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt
[] []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
@@ -388,7 +388,7 @@
val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI];
val intrs = map_index (fn (i, intr) =>
- Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY
+ Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
[rewrite_goals_tac rec_preds_defs,
rtac (unfold RS iffD2) 1,
EVERY1 (select_disj (length intr_ts) (i + 1)),
@@ -432,7 +432,7 @@
val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
map mk_elim_prem (map #1 c_intrs)
in
- (Skip_Proof.prove ctxt'' [] prems P
+ (Goal.prove_sorry ctxt'' [] prems P
(fn {prems, ...} => EVERY
[cut_tac (hd prems) 1,
rewrite_goals_tac rec_preds_defs,
@@ -506,7 +506,7 @@
EVERY (map (fn p => rtac p 1) prems')
end) ctxt' 1);
in
- Skip_Proof.prove ctxt' [] [] eq (fn _ =>
+ Goal.prove_sorry ctxt' [] [] eq (fn _ =>
rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN
EVERY (map_index prove_intr1 c_intrs) THEN
(if null c_intrs then etac @{thm FalseE} 1
@@ -715,7 +715,7 @@
val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
- val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl
+ val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
(fn {prems, ...} => EVERY
[rewrite_goals_tac [inductive_conj_def],
DETERM (rtac raw_fp_induct 1),
@@ -732,7 +732,7 @@
(inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
conjI, refl] 1)) prems)]);
- val lemma = Skip_Proof.prove ctxt'' [] []
+ val lemma = Goal.prove_sorry ctxt'' [] []
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
[rewrite_goals_tac rec_preds_defs,
REPEAT (EVERY
--- a/src/HOL/Tools/record.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/HOL/Tools/record.ML Wed Mar 27 14:19:18 2013 +0100
@@ -1339,7 +1339,7 @@
Logic.mk_equals
(Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
in
- SOME (Skip_Proof.prove_global thy [] [] prop
+ SOME (Goal.prove_sorry_global thy [] [] prop
(fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
end handle TERM _ => NONE)
@@ -1582,7 +1582,7 @@
val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
simplify HOL_ss
- (Skip_Proof.prove_global defs_thy [] [] inject_prop
+ (Goal.prove_sorry_global defs_thy [] [] inject_prop
(fn _ =>
simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
REPEAT_DETERM
@@ -1613,7 +1613,7 @@
end);
val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [] split_meta_prop
+ Goal.prove_sorry_global defs_thy [] [] split_meta_prop
(fn _ =>
EVERY1
[rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
@@ -1623,7 +1623,7 @@
val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
let val (assm, concl) = induct_prop in
- Skip_Proof.prove_global defs_thy [] [assm] concl
+ Goal.prove_sorry_global defs_thy [] [assm] concl
(fn {prems, ...} =>
cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
resolve_tac prems 2 THEN
@@ -2081,7 +2081,7 @@
val (sel_convs, upd_convs) =
timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () =>
grouped 10 Par_List.map (fn prop =>
- Skip_Proof.prove_global defs_thy [] [] prop
+ Goal.prove_sorry_global defs_thy [] [] prop
(K (ALLGOALS (asm_full_simp_tac sel_upd_ss)))) (sel_conv_props @ upd_conv_props))
|> chop (length sel_conv_props);
@@ -2095,7 +2095,7 @@
val parent_induct = Option.map #induct_scheme (try List.last parents);
val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [] induct_scheme_prop
+ Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop
(fn _ =>
EVERY
[case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
@@ -2103,7 +2103,7 @@
asm_simp_tac HOL_basic_ss 1]));
val induct = timeit_msg ctxt "record induct proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
+ Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
try_param_tac rN induct_scheme 1
THEN try_param_tac "more" @{thm unit.induct} 1
THEN resolve_tac prems 1));
@@ -2114,7 +2114,7 @@
get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});
val init_ss = HOL_basic_ss addsimps ext_defs;
in
- Skip_Proof.prove_global defs_thy [] [] surjective_prop
+ Goal.prove_sorry_global defs_thy [] [] surjective_prop
(fn _ =>
EVERY
[rtac surject_assist_idE 1,
@@ -2125,19 +2125,19 @@
end);
val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
+ Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
(fn {prems, ...} =>
resolve_tac prems 1 THEN
rtac surjective 1));
val cases = timeit_msg ctxt "record cases proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [] cases_prop
+ Goal.prove_sorry_global defs_thy [] [] cases_prop
(fn _ =>
try_param_tac rN cases_scheme 1 THEN
ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps @{thms unit_all_eq1}))));
val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [] split_meta_prop
+ Goal.prove_sorry_global defs_thy [] [] split_meta_prop
(fn _ =>
EVERY1
[rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
@@ -2146,14 +2146,14 @@
REPEAT o etac @{thm meta_allE}, atac]));
val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [] split_object_prop
+ Goal.prove_sorry_global defs_thy [] [] split_object_prop
(fn _ =>
rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
rtac split_meta 1));
val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [] split_ex_prop
+ Goal.prove_sorry_global defs_thy [] [] split_ex_prop
(fn _ =>
simp_tac
(HOL_basic_ss addsimps
@@ -2162,7 +2162,7 @@
rtac split_object 1));
val equality = timeit_msg ctxt "record equality proof:" (fn () =>
- Skip_Proof.prove_global defs_thy [] [] equality_prop
+ Goal.prove_sorry_global defs_thy [] [] equality_prop
(fn _ => asm_full_simp_tac (record_ss addsimps (split_meta :: sel_convs)) 1));
val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'),
--- a/src/Pure/Isar/class.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/Pure/Isar/class.ML Wed Mar 27 14:19:18 2013 +0100
@@ -251,7 +251,7 @@
[Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
(fst o rules thy) sub];
val classrel =
- Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+ Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
(K (EVERY (map (TRYALL o Tactic.rtac) intros)));
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
--- a/src/Pure/Isar/class_declaration.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/Pure/Isar/class_declaration.ML Wed Mar 27 14:19:18 2013 +0100
@@ -78,7 +78,7 @@
| NONE => const_morph);
val thm'' = Morphism.thm const_eq_morph thm';
val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
- in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+ in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
(* of_class *)
@@ -96,7 +96,7 @@
REPEAT (SOMEGOAL
(Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
ORELSE' Tactic.assume_tac));
- val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
+ val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
--- a/src/Pure/Isar/code.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/Pure/Isar/code.ML Wed Mar 27 14:19:18 2013 +0100
@@ -1113,7 +1113,7 @@
val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
- in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
+ in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end;
fun add_case thm thy =
let
--- a/src/Pure/Isar/proof.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/Pure/Isar/proof.ML Wed Mar 27 14:19:18 2013 +0100
@@ -1026,23 +1026,13 @@
(* skip proofs *)
-local
-
-fun skipped_proof state =
- Context_Position.if_visible (context_of state) Output.report
- (Markup.markup Markup.bad "Skipped proof");
-
-in
-
fun local_skip_proof int state =
local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
- skipped_proof state;
+ Skip_Proof.report (context_of state);
fun global_skip_proof int state =
global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
- skipped_proof state;
-
-end;
+ Skip_Proof.report (context_of state);
(* common goal statements *)
--- a/src/Pure/Isar/skip_proof.ML Wed Mar 27 14:08:03 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: Pure/Isar/skip_proof.ML
- Author: Markus Wenzel, TU Muenchen
-
-Skipping proofs -- via oracle (in quick and dirty mode) or by forking
-(parallel mode).
-*)
-
-signature SKIP_PROOF =
-sig
- val make_thm_cterm: cterm -> thm
- val make_thm: theory -> term -> thm
- val cheat_tac: theory -> tactic
- val prove: Proof.context -> string list -> term list -> term ->
- ({prems: thm list, context: Proof.context} -> tactic) -> thm
- val prove_global: theory -> string list -> term list -> term ->
- ({prems: thm list, context: Proof.context} -> tactic) -> thm
-end;
-
-structure Skip_Proof: SKIP_PROOF =
-struct
-
-(* oracle setup *)
-
-val (_, make_thm_cterm) =
- Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
-
-fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
-
-
-(* basic cheating *)
-
-fun cheat_tac thy st =
- ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
-
-fun prove ctxt xs asms prop tac =
- if ! quick_and_dirty then
- Goal.prove ctxt xs asms prop (fn _ => cheat_tac (Proof_Context.theory_of ctxt))
- else (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop tac;
-
-fun prove_global thy xs asms prop tac =
- Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
-
-end;
--- a/src/Pure/ROOT Wed Mar 27 14:08:03 2013 +0100
+++ b/src/Pure/ROOT Wed Mar 27 14:19:18 2013 +0100
@@ -129,7 +129,6 @@
"Isar/rule_cases.ML"
"Isar/rule_insts.ML"
"Isar/runtime.ML"
- "Isar/skip_proof.ML"
"Isar/spec_rules.ML"
"Isar/specification.ML"
"Isar/token.ML"
@@ -241,6 +240,7 @@
"search.ML"
"sign.ML"
"simplifier.ML"
+ "skip_proof.ML"
"sorts.ML"
"subgoal.ML"
"tactic.ML"
--- a/src/Pure/ROOT.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/Pure/ROOT.ML Wed Mar 27 14:19:18 2013 +0100
@@ -180,6 +180,7 @@
use "ML/ml_compiler.ML";
if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
+use "skip_proof.ML";
use "goal.ML";
(*proof context*)
@@ -217,7 +218,6 @@
use "Isar/attrib.ML";
use "ML/ml_antiquote.ML";
use "Isar/context_rules.ML";
-use "Isar/skip_proof.ML";
use "Isar/method.ML";
use "Isar/proof.ML";
use "Isar/element.ML";
--- a/src/Pure/goal.ML Wed Mar 27 14:08:03 2013 +0100
+++ b/src/Pure/goal.ML Wed Mar 27 14:19:18 2013 +0100
@@ -46,6 +46,10 @@
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global: theory -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
+ val prove_sorry: Proof.context -> string list -> term list -> term ->
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
+ val prove_sorry_global: theory -> string list -> term list -> term ->
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val extract: int -> int -> thm -> thm Seq.seq
val retrofit: int -> int -> thm -> thm -> thm Seq.seq
val conjunction_tac: int -> tactic
@@ -318,6 +322,15 @@
fun prove_global thy xs asms prop tac =
Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
+fun prove_sorry ctxt xs asms prop tac =
+ if ! quick_and_dirty then
+ prove ctxt xs asms prop (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt))
+ else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac;
+
+fun prove_sorry_global thy xs asms prop tac =
+ Drule.export_without_context
+ (prove_sorry (Proof_Context.init_global thy) xs asms prop tac);
+
(** goal structure **)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/skip_proof.ML Wed Mar 27 14:19:18 2013 +0100
@@ -0,0 +1,38 @@
+(* Title: Pure/skip_proof.ML
+ Author: Makarius
+
+Skip proof via oracle invocation.
+*)
+
+signature SKIP_PROOF =
+sig
+ val report: Proof.context -> unit
+ val make_thm_cterm: cterm -> thm
+ val make_thm: theory -> term -> thm
+ val cheat_tac: theory -> tactic
+end;
+
+structure Skip_Proof: SKIP_PROOF =
+struct
+
+(* report *)
+
+fun report ctxt =
+ Context_Position.if_visible ctxt Output.report
+ (Markup.markup Markup.bad "Skipped proof");
+
+
+(* oracle setup *)
+
+val (_, make_thm_cterm) =
+ Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
+
+fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
+
+
+(* cheat_tac *)
+
+fun cheat_tac thy st =
+ ALLGOALS (rtac (make_thm thy (Var (("A", 0), propT)))) st;
+
+end;