# HG changeset patch # User wenzelm # Date 1364390358 -3600 # Node ID 88d1d19fb74f451bcd3e1b178937dc0583aed95d # Parent cec08df2c03024253d50205302b8effe8c90f855 tuned signature and module arrangement; diff -r cec08df2c030 -r 88d1d19fb74f NEWS --- 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 diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/BNF/Tools/bnf_comp.ML --- 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; diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/BNF/Tools/bnf_def.ML --- 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; diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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; diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/BNF/Tools/bnf_gfp.ML --- 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 diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/BNF/Tools/bnf_lfp.ML --- 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 diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/BNF/Tools/bnf_wrap.ML --- 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) => diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/Datatype/datatype.ML --- 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, ...} => diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/Datatype/datatype_codegen.ML --- 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; diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/Datatype/rep_datatype.ML --- 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 [ diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/Function/size.ML --- 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) diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/Quickcheck/random_generators.ML --- 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 diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/enriched_type.ML --- 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; diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/inductive.ML --- 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 diff -r cec08df2c030 -r 88d1d19fb74f src/HOL/Tools/record.ML --- 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'), diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/Isar/class.ML --- 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]) diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/Isar/class_declaration.ML --- 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; diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/Isar/code.ML --- 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 diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/Isar/proof.ML --- 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 *) diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/Isar/skip_proof.ML --- 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; diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/ROOT --- 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" diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/ROOT.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"; diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/goal.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 **) diff -r cec08df2c030 -r 88d1d19fb74f src/Pure/skip_proof.ML --- /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;