# HG changeset patch # User wenzelm # Date 1364415169 -3600 # Node ID a1eb68bd9312ab8ba119c9e2f2eedf33c24d54e2 # Parent 757fa47af9814c1c3f72ae59063429fce9c1afc9# Parent 5b4ae246783038128c24651f22a5dbca82ca5033 merged diff -r 757fa47af981 -r a1eb68bd9312 NEWS --- a/NEWS Wed Mar 27 10:55:05 2013 +0100 +++ b/NEWS Wed Mar 27 21:12:49 2013 +0100 @@ -26,6 +26,8 @@ * Dockable window "Timing" provides an overview of relevant command timing information. +* Option to skip over proofs, using implicit 'sorry' internally. + *** Pure *** @@ -106,6 +108,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 757fa47af981 -r a1eb68bd9312 etc/options --- a/etc/options Wed Mar 27 10:55:05 2013 +0100 +++ b/etc/options Wed Mar 27 21:12:49 2013 +0100 @@ -66,7 +66,7 @@ option quick_and_dirty : bool = false -- "if true then some tools will OMIT some proofs" option skip_proofs : bool = false - -- "skip over proofs" + -- "skip over proofs (implicit 'sorry')" section "Global Session Parameters" @@ -83,6 +83,9 @@ section "Editor Reactivity" +option editor_skip_proofs : bool = false + -- "skip over proofs (implicit 'sorry')" + option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" diff -r 757fa47af981 -r a1eb68bd9312 src/Doc/ROOT --- a/src/Doc/ROOT Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Doc/ROOT Wed Mar 27 21:12:49 2013 +0100 @@ -40,7 +40,7 @@ "document/style.sty" session Functions (doc) in "Functions" = HOL + - options [document_variants = "functions"] + options [document_variants = "functions", skip_proofs = false] theories Functions files "../prepare_document" @@ -145,7 +145,7 @@ "document/root.tex" session Locales (doc) in "Locales" = HOL + - options [document_variants = "locales", pretty_margin = 65] + options [document_variants = "locales", pretty_margin = 65, skip_proofs = false] theories Examples1 Examples2 @@ -295,7 +295,7 @@ "document/root.tex" session Tutorial (doc) in "Tutorial" = HOL + - options [document_variants = "tutorial", print_mode = "brackets"] + options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] theories [thy_output_indent = 5] "ToyList/ToyList" "Ifexpr/Ifexpr" diff -r 757fa47af981 -r a1eb68bd9312 src/FOL/ROOT --- a/src/FOL/ROOT Wed Mar 27 10:55:05 2013 +0100 +++ b/src/FOL/ROOT Wed Mar 27 21:12:49 2013 +0100 @@ -39,6 +39,7 @@ Quantifiers_Cla Miniscope If - theories [document = false] "Locale_Test/Locale_Test" + theories [document = false, skip_proofs = false] + "Locale_Test/Locale_Test" files "document/root.tex" diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/BNF/Tools/bnf_wrap.ML --- a/src/HOL/BNF/Tools/bnf_wrap.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Library/refute.ML Wed Mar 27 21:12:49 2013 +0100 @@ -3202,6 +3202,7 @@ "try to find a model that refutes a given subgoal" (scan_parms -- Scan.optional Parse.nat 1 >> (fn (parms, i) => + Toplevel.unknown_proof o Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state; diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/ROOT --- a/src/HOL/ROOT Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/ROOT Wed Mar 27 21:12:49 2013 +0100 @@ -16,7 +16,7 @@ description {* HOL-Main with explicit proof terms. *} - options [document = false, proofs = 2] + options [document = false, proofs = 2, skip_proofs = false] theories Main files "Tools/Quickcheck/Narrowing_Engine.hs" @@ -354,14 +354,14 @@ theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + - options [document = false, proofs = 2, parallel_proofs = 0] + options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0] theories Hilbert_Classical session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + description {* Examples for program extraction in Higher-Order Logic. *} - options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0] + options [condition = ISABELLE_POLYML, proofs = 2, skip_proofs = false, parallel_proofs = 0] theories [document = false] "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Monad_Syntax" @@ -386,7 +386,8 @@ The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). *} - options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0] + options [document_graph, print_mode = "no_brackets", proofs = 2, skip_proofs = false, + parallel_proofs = 0] theories [document = false] "~~/src/HOL/Library/Code_Target_Int" theories @@ -424,7 +425,7 @@ "document/root.tex" session "HOL-MicroJava-skip_proofs" in MicroJava = HOL + - options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty] + options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs] theories MicroJava session "HOL-NanoJava" in NanoJava = HOL + @@ -535,7 +536,6 @@ Tarski Classical Set_Theory - Meson_Test Termination Coherent PresburgerEx @@ -560,7 +560,9 @@ Set_Comprehension_Pointfree_Tests Parallel_Example IArray_Examples - theories SVC_Oracle + SVC_Oracle + theories [skip_proofs = false] + Meson_Test theories [condition = SVC_HOME] svc_test theories [condition = ZCHAFF_HOME] @@ -742,7 +744,8 @@ theories WordExamples session "HOL-Statespace" in Statespace = HOL + - theories StateSpaceEx + theories [skip_proofs = false] + StateSpaceEx files "document/root.tex" session "HOL-NSA" in NSA = HOL + diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Wed Mar 27 21:12:49 2013 +0100 @@ -175,7 +175,7 @@ val (outcome, _) = Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj - in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end + in if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end end fun atp_tac ctxt completeness override_params timeout prover = diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Mar 27 21:12:49 2013 +0100 @@ -64,12 +64,11 @@ fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th = let - val thy = Proof_Context.theory_of ctxt val override_params = override_params @ [("preplay_timeout", "0"), ("minimize", "false")] val xs = run_prover override_params fact_override i i ctxt th - in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end + in if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end end; diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Function/size.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Mar 27 21:12:49 2013 +0100 @@ -368,11 +368,6 @@ in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end |> `(fn (outcome_code, _) => outcome_code = genuineN) -fun nitpick_trans (params, i) = - Toplevel.keep (fn state => - pick_nits params Normal i (Toplevel.proof_position_of state) - (Toplevel.proof_of state) |> K ()) - fun string_for_raw_param (name, value) = name ^ " = " ^ stringify_raw_param_value value @@ -391,7 +386,11 @@ val _ = Outer_Syntax.improper_command @{command_spec "nitpick"} "try to find a counterexample for a given subgoal using Nitpick" - ((parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans) + (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) => + Toplevel.unknown_proof o + Toplevel.keep (fn state => + ignore (pick_nits params Normal i (Toplevel.proof_position_of state) + (Toplevel.proof_of state))))) val _ = Outer_Syntax.command @{command_spec "nitpick_params"} diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Mar 27 21:12:49 2013 +0100 @@ -1180,7 +1180,7 @@ fun define_quickcheck_predicate t thy = let val (vs, t') = strip_abs t - val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs + val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *) val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' val constname = "quickcheck" @@ -1191,8 +1191,9 @@ val t = Logic.list_implies (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), HOLogic.mk_Trueprop (list_comb (const, map Free vs'))) - val tac = fn _ => Skip_Proof.cheat_tac thy1 - val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t tac + val intro = + Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t + (fn _ => ALLGOALS Skip_Proof.cheat_tac) in ((((full_constname, constT), vs'), intro), thy1) end diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Mar 27 21:12:49 2013 +0100 @@ -134,7 +134,7 @@ fun split_all_pairs thy th = let - val ctxt = Proof_Context.init_global thy + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val ((_, [th']), _) = Variable.import true [th] ctxt val t = prop_of th' val frees = Term.add_frees t [] @@ -148,8 +148,9 @@ in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt val t' = Pattern.rewrite_term thy rewr [] t - val tac = Skip_Proof.cheat_tac thy - val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac) + val th'' = + Goal.prove ctxt (Term.add_free_names t' []) [] t' + (fn _ => ALLGOALS Skip_Proof.cheat_tac) val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th'' in th''' diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Mar 27 21:12:49 2013 +0100 @@ -127,13 +127,13 @@ fun flatten_intros constname intros thy = let - val ctxt = Proof_Context.init_global thy + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val ((_, intros), ctxt') = Variable.import true intros ctxt val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms) (flatten constname) (map prop_of intros) ([], thy) val ctxt'' = Proof_Context.transfer thy' ctxt' - val tac = fn _ => Skip_Proof.cheat_tac thy' - val intros'' = map (fn t => Goal.prove ctxt'' [] [] t tac) intros' + val intros'' = + map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS Skip_Proof.cheat_tac)) intros' |> Variable.export ctxt'' ctxt in (intros'', (local_defs, thy')) diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Mar 27 21:12:49 2013 +0100 @@ -491,7 +491,7 @@ fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) = let - val ctxt = Proof_Context.init_global thy + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [] in Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term @@ -503,7 +503,7 @@ THEN print_tac options "proved one direction" THEN prove_other_direction options ctxt pred mode moded_clauses THEN print_tac options "proved other direction") - else (fn _ => Skip_Proof.cheat_tac thy)) + else (fn _ => ALLGOALS Skip_Proof.cheat_tac)) end; end; \ No newline at end of file diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Mar 27 21:12:49 2013 +0100 @@ -376,7 +376,7 @@ let val eqs_t = mk_equations consts val eqs = map (fn eq => Goal.prove lthy argnames [] eq - (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t + (fn _ => ALLGOALS Skip_Proof.cheat_tac)) eqs_t in fold (fn (name, eq) => Local_Theory.note ((Binding.qualify true prfx diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 27 21:12:49 2013 +0100 @@ -419,6 +419,7 @@ end fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = + Toplevel.unknown_proof o Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/enriched_type.ML --- a/src/HOL/Tools/enriched_type.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/enriched_type.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/inductive.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/record.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Wed Mar 27 21:12:49 2013 +0100 @@ -324,14 +324,13 @@ tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) else () val fm = Prop_Logic.all fms - (* unit -> Thm.thm *) fun make_quick_and_dirty_thm () = let val _ = if !trace_sat then tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." else () - val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ @{term False}) + val False_thm = Skip_Proof.make_thm_cterm @{cprop False} in (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) diff -r 757fa47af981 -r a1eb68bd9312 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/HOL/Tools/try0.ML Wed Mar 27 21:12:49 2013 +0100 @@ -156,6 +156,7 @@ fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt fun try0_trans quad = + Toplevel.unknown_proof o Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of) diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Isar/class.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Isar/class_declaration.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Isar/code.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Isar/method.ML Wed Mar 27 21:12:49 2013 +0100 @@ -20,7 +20,7 @@ val SIMPLE_METHOD: tactic -> method val SIMPLE_METHOD': (int -> tactic) -> method val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method - val cheating: bool -> Proof.context -> method + val cheating: bool -> method val intro: thm list -> method val elim: thm list -> method val unfold: thm list -> Proof.context -> method @@ -112,7 +112,7 @@ in -fun insert_tac [] i = all_tac +fun insert_tac [] _ = all_tac | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); val insert_facts = METHOD (ALLGOALS o insert_tac); @@ -127,10 +127,10 @@ (* cheating *) -fun cheating int ctxt = +fun cheating int = METHOD (fn _ => fn st => if int orelse ! quick_and_dirty then - METHOD (K (Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt))) - else error "Cheating requires quick_and_dirty mode!"; + ALLGOALS Skip_Proof.cheat_tac st + else error "Cheating requires quick_and_dirty mode!"); (* unfold intro/elim rules *) @@ -296,7 +296,7 @@ val default_text = Source (Args.src (("default", []), Position.none)); val this_text = Basic (K this); val done_text = Basic (K (SIMPLE_METHOD all_tac)); -fun sorry_text int = Basic (cheating int); +fun sorry_text int = Basic (K (cheating int)); fun finish_text (NONE, immed) = Basic (finish immed) | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)]; diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Isar/proof.ML Wed Mar 27 21:12:49 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 *) @@ -1103,19 +1093,15 @@ (* relevant proof states *) -fun is_schematic t = - Term.exists_subterm Term.is_Var t orelse - Term.exists_type (Term.exists_subtype Term.is_TVar) t; - fun schematic_goal state = let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state - in is_schematic prop end; + in Goal.is_schematic prop end; fun is_relevant state = (case try find_goal state of NONE => true | SOME (_, (_, {statement = (_, _, prop), goal, ...})) => - is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal)); + Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal)); (* full proofs *) diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/Isar/skip_proof.ML --- a/src/Pure/Isar/skip_proof.ML Wed Mar 27 10:55:05 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 757fa47af981 -r a1eb68bd9312 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Mar 27 21:12:49 2013 +0100 @@ -12,6 +12,7 @@ val is_toplevel: state -> bool val is_theory: state -> bool val is_proof: state -> bool + val is_skipped_proof: state -> bool val level: state -> int val presentation_context_of: state -> Proof.context val previous_context_of: state -> Proof.context option @@ -29,7 +30,6 @@ val interact: bool Unsynchronized.ref val timing: bool Unsynchronized.ref val profiling: int Unsynchronized.ref - val skip_proofs: bool Unsynchronized.ref val program: (unit -> 'a) -> 'a val thread: bool -> (unit -> unit) -> Thread.thread type transition @@ -129,15 +129,16 @@ (*theory with presentation context*) | Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) (*proof node, finish, original theory*) | - SkipProof of int * (generic_theory * generic_theory); + Skipped_Proof of int * (generic_theory * generic_theory); (*proof depth, resulting theory, original theory*) val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE; val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; +val skipped_proof_node = fn Skipped_Proof _ => true | _ => false; fun cases_node f _ (Theory (gthy, _)) = f gthy | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) - | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; + | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy; val context_node = cases_node Context.proof_of Proof.context_of; @@ -154,13 +155,13 @@ fun level (State (NONE, _)) = 0 | level (State (SOME (Theory _), _)) = 0 | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) - | level (State (SOME (SkipProof (d, _)), _)) = d + 1; (*different notion of proof depth!*) + | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1; (*different notion of proof depth!*) fun str_of_state (State (NONE, _)) = "at top level" | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode" | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode" | str_of_state (State (SOME (Proof _), _)) = "in proof mode" - | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode"; + | str_of_state (State (SOME (Skipped_Proof _), _)) = "in skipped proof mode"; (* current node *) @@ -170,6 +171,7 @@ fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); +fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); fun node_case f g state = cases_node f g (node_of state); @@ -206,7 +208,7 @@ NONE => [] | SOME (Theory (gthy, _)) => pretty_context gthy | SOME (Proof (_, (_, gthy))) => pretty_context gthy - | SOME (SkipProof (_, (gthy, _))) => pretty_context gthy) + | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy) |> Pretty.chunks |> Pretty.writeln; fun print_state prf_only state = @@ -215,7 +217,7 @@ | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) - | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) + | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) |> Pretty.markup_chunks Markup.state |> Pretty.writeln; fun pretty_abstract state = Pretty.str (""); @@ -229,7 +231,6 @@ val interact = Unsynchronized.ref false; val timing = Unsynchronized.ref false; val profiling = Unsynchronized.ref 0; -val skip_proofs = Unsynchronized.ref false; fun program body = (body @@ -513,7 +514,7 @@ in Theory (gthy', SOME ctxt') end else raise UNDEF end - | SkipProof (0, (gthy, _)) => Theory (gthy, NONE) + | Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE) | _ => raise UNDEF)); local @@ -522,7 +523,7 @@ (fn Theory (gthy, _) => let val (finish, prf) = init int gthy; - val skip = ! skip_proofs; + val skip = ! Goal.skip_proofs; val (is_goal, no_skip) = (true, Proof.schematic_goal prf) handle ERROR _ => (false, true); val _ = @@ -531,7 +532,7 @@ else (); in if skip andalso not no_skip then - SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy)) + Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) else Proof (Proof_Node.init prf, (finish, gthy)) end | _ => raise UNDEF)); @@ -547,7 +548,7 @@ fun theory_to_proof f = begin_proof (fn _ => fn gthy => - (Context.Theory o Sign.reset_group o Proof_Context.theory_of, + (Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of, (case gthy of Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))); @@ -556,17 +557,17 @@ val forget_proof = transaction (fn _ => (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) - | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) + | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) | _ => raise UNDEF)); val present_proof = present_transaction (fn _ => (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) - | skip as SkipProof _ => skip + | skip as Skipped_Proof _ => skip | _ => raise UNDEF)); fun proofs' f = transaction (fn int => (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) - | skip as SkipProof _ => skip + | skip as Skipped_Proof _ => skip | _ => raise UNDEF)); fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); @@ -578,11 +579,11 @@ | _ => raise UNDEF)); fun skip_proof f = transaction (fn _ => - (fn SkipProof (h, x) => SkipProof (f h, x) + (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x) | _ => raise UNDEF)); fun skip_proof_to_theory pred = transaction (fn _ => - (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF + (fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF | _ => raise UNDEF)); diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/ProofGeneral/preferences.ML Wed Mar 27 21:12:49 2013 +0100 @@ -169,7 +169,7 @@ bool_pref quick_and_dirty "quick-and-dirty" "Take a few short cuts") (), - bool_pref Toplevel.skip_proofs + bool_pref Goal.skip_proofs "skip-proofs" "Skip over proofs", proof_pref, diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/ROOT --- a/src/Pure/ROOT Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/ROOT Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/ROOT.ML Wed Mar 27 21:12:49 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 757fa47af981 -r a1eb68bd9312 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/System/isabelle_process.ML Wed Mar 27 21:12:49 2013 +0100 @@ -242,6 +242,7 @@ Multithreading.max_threads := Options.int options "threads"; if Multithreading.max_threads_value () < 2 then Multithreading.max_threads := 2 else (); + Goal.skip_proofs := Options.bool options "editor_skip_proofs"; Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0); Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation"; Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold"; diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Thy/thy_load.ML Wed Mar 27 21:12:49 2013 +0100 @@ -263,10 +263,13 @@ val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results); val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax (); in - Thy_Output.present_thy minor Keyword.command_tags - (Outer_Syntax.is_markup outer_syntax) res toks - |> Buffer.content - |> Present.theory_output name + if exists (Toplevel.is_skipped_proof o #2) res then + warning ("Cannot present theory with skipped proofs: " ^ quote name) + else + Thy_Output.present_thy minor Keyword.command_tags + (Outer_Syntax.is_markup outer_syntax) res toks + |> Buffer.content + |> Present.theory_output name end; in (thy, present, size text) end; diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Thy/thy_output.ML Wed Mar 27 21:12:49 2013 +0100 @@ -206,7 +206,8 @@ fun check_text (txt, pos) state = (Position.report pos Markup.doc_source; - ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); + if Toplevel.is_skipped_proof state then () + else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/Tools/build.ML Wed Mar 27 21:12:49 2013 +0100 @@ -59,7 +59,7 @@ |> Unsynchronized.setmp Future.ML_statistics true |> no_document options ? Present.no_document |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty") - |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs") + |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs") |> Unsynchronized.setmp Printer.show_question_marks_default (Options.bool options "show_question_marks") |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long") diff -r 757fa47af981 -r a1eb68bd9312 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Pure/goal.ML Wed Mar 27 21:12:49 2013 +0100 @@ -6,6 +6,7 @@ signature BASIC_GOAL = sig + val skip_proofs: bool Unsynchronized.ref val parallel_proofs: int Unsynchronized.ref val parallel_subproofs_saturation: int Unsynchronized.ref val parallel_subproofs_threshold: real Unsynchronized.ref @@ -36,6 +37,7 @@ val future_enabled_timing: Time.time -> bool val future_result: Proof.context -> thm future -> term -> thm val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm + val is_schematic: term -> bool val prove_multi: Proof.context -> string list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> thm list val prove_future: Proof.context -> string list -> term list -> term -> @@ -46,6 +48,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 @@ -192,6 +198,8 @@ (* scheduling parameters *) +val skip_proofs = Unsynchronized.ref false; + val parallel_proofs = Unsynchronized.ref 1; val parallel_subproofs_saturation = Unsynchronized.ref 100; val parallel_subproofs_threshold = Unsynchronized.ref 0.01; @@ -259,13 +267,21 @@ | NONE => error "Tactic failed"); -(* prove_common etc. *) +(* prove variations *) + +fun is_schematic t = + Term.exists_subterm Term.is_Var t orelse + Term.exists_type (Term.exists_subtype Term.is_TVar) t; fun prove_common immediate ctxt xs asms props tac = let val thy = Proof_Context.theory_of ctxt; val string_of_term = Syntax.string_of_term ctxt; + val schematic = exists is_schematic props; + val future = future_enabled (); + val skip = not immediate andalso not schematic andalso future andalso ! skip_proofs; + val pos = Position.thread_data (); fun err msg = cat_error msg ("The error(s) above occurred for the goal statement:\n" ^ @@ -286,8 +302,11 @@ val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); + fun tac' args st = + if skip then ALLGOALS Skip_Proof.cheat_tac st before Skip_Proof.report ctxt + else tac args st; fun result () = - (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of + (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of NONE => err "Tactic failed" | SOME st => let val res = finish ctxt' st handle THM (msg, _, _) => err msg in @@ -296,7 +315,7 @@ else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) end); val res = - if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ()) + if immediate orelse schematic orelse not future orelse skip then result () else future_result ctxt' (fork ~1 result) (Thm.term_of stmt); in @@ -318,6 +337,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 _ => ALLGOALS Skip_Proof.cheat_tac) + 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 757fa47af981 -r a1eb68bd9312 src/Pure/skip_proof.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/skip_proof.ML Wed Mar 27 21:12:49 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: int -> 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 i st = + rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st; + +end; diff -r 757fa47af981 -r a1eb68bd9312 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Tools/jEdit/src/isabelle_options.scala Wed Mar 27 21:12:49 2013 +0100 @@ -45,9 +45,9 @@ "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay", "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter", "jedit_timing_threshold", "threads", "threads_trace", "parallel_proofs", - "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay", - "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages", - "editor_update_delay", "editor_chart_delay") + "parallel_subproofs_saturation", "editor_skip_proofs", "editor_load_delay", + "editor_input_delay", "editor_output_delay", "editor_reparse_limit", + "editor_tracing_messages", "editor_update_delay", "editor_chart_delay") relevant_options.foreach(PIDE.options.value.check_name _) diff -r 757fa47af981 -r a1eb68bd9312 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 27 21:12:49 2013 +0100 @@ -130,7 +130,11 @@ private var timing_threshold = PIDE.options.real("jedit_timing_threshold") - private val threshold_label = new Label("Threshold: ") + private val threshold_tooltip = "Threshold for timing display (seconds)" + + private val threshold_label = new Label("Threshold: ") { + tooltip = threshold_tooltip + } private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) { reactions += { @@ -141,7 +145,7 @@ } handle_update() } - tooltip = "Threshold for timing display (seconds)" + tooltip = threshold_tooltip verifier = ((s: String) => s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false }) } diff -r 757fa47af981 -r a1eb68bd9312 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Tools/quickcheck.ML Wed Mar 27 21:12:49 2013 +0100 @@ -532,8 +532,8 @@ val _ = Outer_Syntax.improper_command @{command_spec "quickcheck"} "try to find counterexample for subgoal" - (parse_args -- Scan.optional Parse.nat 1 - >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i))); + (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => + Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i))); (* automatic testing *) diff -r 757fa47af981 -r a1eb68bd9312 src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Tools/solve_direct.ML Wed Mar 27 21:12:49 2013 +0100 @@ -109,7 +109,8 @@ val _ = Outer_Syntax.improper_command @{command_spec "solve_direct"} "try to solve conjectures directly with existing theorems" - (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); + (Scan.succeed (Toplevel.unknown_proof o + Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); (* hook *) diff -r 757fa47af981 -r a1eb68bd9312 src/Tools/try.ML --- a/src/Tools/try.ML Wed Mar 27 10:55:05 2013 +0100 +++ b/src/Tools/try.ML Wed Mar 27 21:12:49 2013 +0100 @@ -90,7 +90,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "try"} "try a combination of automatic proving and disproving tools" - (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) + (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) (* automatic try *)