1.1 --- a/NEWS	Wed Mar 27 14:50:30 2013 +0100
     1.2 +++ b/NEWS	Wed Mar 27 16:38:25 2013 +0100
     1.3 @@ -26,6 +26,8 @@
     1.4  * Dockable window "Timing" provides an overview of relevant command
     1.5  timing information.
     1.6  
     1.7 +* Option to skip over proofs, using implicit 'sorry' internally.
     1.8 +
     1.9  
    1.10  *** Pure ***
    1.11  

     2.1 --- a/etc/options	Wed Mar 27 14:50:30 2013 +0100
     2.2 +++ b/etc/options	Wed Mar 27 16:38:25 2013 +0100
     2.3 @@ -66,7 +66,7 @@
     2.4  option quick_and_dirty : bool = false
     2.5    -- "if true then some tools will OMIT some proofs"
     2.6  option skip_proofs : bool = false
     2.7 -  -- "skip over proofs"
     2.8 +  -- "skip over proofs (implicit 'sorry')"
     2.9  
    2.10  
    2.11  section "Global Session Parameters"

     3.1 --- a/src/HOL/ROOT	Wed Mar 27 14:50:30 2013 +0100
     3.2 +++ b/src/HOL/ROOT	Wed Mar 27 16:38:25 2013 +0100
     3.3 @@ -424,7 +424,7 @@
     3.4      "document/root.tex"
     3.5  
     3.6  session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
     3.7 -  options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
     3.8 +  options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs]
     3.9    theories MicroJava
    3.10  
    3.11  session "HOL-NanoJava" in NanoJava = HOL +

     4.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 27 14:50:30 2013 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 27 16:38:25 2013 +0100
     4.3 @@ -1093,19 +1093,15 @@
     4.4  
     4.5  (* relevant proof states *)
     4.6  
     4.7 -fun is_schematic t =
     4.8 -  Term.exists_subterm Term.is_Var t orelse
     4.9 -  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
    4.10 -
    4.11  fun schematic_goal state =
    4.12    let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state
    4.13 -  in is_schematic prop end;
    4.14 +  in Goal.is_schematic prop end;
    4.15  
    4.16  fun is_relevant state =
    4.17    (case try find_goal state of
    4.18      NONE => true
    4.19    | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
    4.20 -      is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
    4.21 +      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
    4.22  
    4.23  
    4.24  (* full proofs *)

     5.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 27 14:50:30 2013 +0100
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 27 16:38:25 2013 +0100
     5.3 @@ -29,7 +29,6 @@
     5.4    val interact: bool Unsynchronized.ref
     5.5    val timing: bool Unsynchronized.ref
     5.6    val profiling: int Unsynchronized.ref
     5.7 -  val skip_proofs: bool Unsynchronized.ref
     5.8    val program: (unit -> 'a) -> 'a
     5.9    val thread: bool -> (unit -> unit) -> Thread.thread
    5.10    type transition
    5.11 @@ -229,7 +228,6 @@
    5.12  val interact = Unsynchronized.ref false;
    5.13  val timing = Unsynchronized.ref false;
    5.14  val profiling = Unsynchronized.ref 0;
    5.15 -val skip_proofs = Unsynchronized.ref false;
    5.16  
    5.17  fun program body =
    5.18   (body
    5.19 @@ -522,7 +520,7 @@
    5.20    (fn Theory (gthy, _) =>
    5.21      let
    5.22        val (finish, prf) = init int gthy;
    5.23 -      val skip = ! skip_proofs;
    5.24 +      val skip = ! Goal.skip_proofs;
    5.25        val (is_goal, no_skip) =
    5.26          (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
    5.27        val _ =
    5.28 @@ -531,7 +529,7 @@
    5.29          else ();
    5.30      in
    5.31        if skip andalso not no_skip then
    5.32 -        SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy))
    5.33 +        SkipProof (0, (finish (Proof.global_skip_proof true prf), gthy))
    5.34        else Proof (Proof_Node.init prf, (finish, gthy))
    5.35      end
    5.36    | _ => raise UNDEF));

     6.1 --- a/src/Pure/ProofGeneral/preferences.ML	Wed Mar 27 14:50:30 2013 +0100
     6.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Wed Mar 27 16:38:25 2013 +0100
     6.3 @@ -169,7 +169,7 @@
     6.4      bool_pref quick_and_dirty
     6.5        "quick-and-dirty"
     6.6        "Take a few short cuts") (),
     6.7 -  bool_pref Toplevel.skip_proofs
     6.8 +  bool_pref Goal.skip_proofs
     6.9      "skip-proofs"
    6.10      "Skip over proofs",
    6.11    proof_pref,

     7.1 --- a/src/Pure/System/isabelle_process.ML	Wed Mar 27 14:50:30 2013 +0100
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Mar 27 16:38:25 2013 +0100
     7.3 @@ -242,6 +242,7 @@
     7.4          Multithreading.max_threads := Options.int options "threads";
     7.5          if Multithreading.max_threads_value () < 2
     7.6          then Multithreading.max_threads := 2 else ();
     7.7 +        Goal.skip_proofs := Options.bool options "skip_proofs";
     7.8          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
     7.9          Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation";
    7.10          Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold";

     8.1 --- a/src/Pure/Tools/build.ML	Wed Mar 27 14:50:30 2013 +0100
     8.2 +++ b/src/Pure/Tools/build.ML	Wed Mar 27 16:38:25 2013 +0100
     8.3 @@ -59,7 +59,7 @@
     8.4      |> Unsynchronized.setmp Future.ML_statistics true
     8.5      |> no_document options ? Present.no_document
     8.6      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     8.7 -    |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
     8.8 +    |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     8.9      |> Unsynchronized.setmp Printer.show_question_marks_default
    8.10          (Options.bool options "show_question_marks")
    8.11      |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")

     9.1 --- a/src/Pure/goal.ML	Wed Mar 27 14:50:30 2013 +0100
     9.2 +++ b/src/Pure/goal.ML	Wed Mar 27 16:38:25 2013 +0100
     9.3 @@ -6,6 +6,7 @@
     9.4  
     9.5  signature BASIC_GOAL =
     9.6  sig
     9.7 +  val skip_proofs: bool Unsynchronized.ref
     9.8    val parallel_proofs: int Unsynchronized.ref
     9.9    val parallel_subproofs_saturation: int Unsynchronized.ref
    9.10    val parallel_subproofs_threshold: real Unsynchronized.ref
    9.11 @@ -36,6 +37,7 @@
    9.12    val future_enabled_timing: Time.time -> bool
    9.13    val future_result: Proof.context -> thm future -> term -> thm
    9.14    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    9.15 +  val is_schematic: term -> bool
    9.16    val prove_multi: Proof.context -> string list -> term list -> term list ->
    9.17      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    9.18    val prove_future: Proof.context -> string list -> term list -> term ->
    9.19 @@ -196,6 +198,8 @@
    9.20  
    9.21  (* scheduling parameters *)
    9.22  
    9.23 +val skip_proofs = Unsynchronized.ref false;
    9.24 +
    9.25  val parallel_proofs = Unsynchronized.ref 1;
    9.26  val parallel_subproofs_saturation = Unsynchronized.ref 100;
    9.27  val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
    9.28 @@ -263,13 +267,21 @@
    9.29    | NONE => error "Tactic failed");
    9.30  
    9.31  
    9.32 -(* prove_common etc. *)
    9.33 +(* prove variations *)
    9.34 +
    9.35 +fun is_schematic t =
    9.36 +  Term.exists_subterm Term.is_Var t orelse
    9.37 +  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
    9.38  
    9.39  fun prove_common immediate ctxt xs asms props tac =
    9.40    let
    9.41      val thy = Proof_Context.theory_of ctxt;
    9.42      val string_of_term = Syntax.string_of_term ctxt;
    9.43  
    9.44 +    val schematic = exists is_schematic props;
    9.45 +    val future = future_enabled ();
    9.46 +    val skip = not immediate andalso not schematic andalso future andalso ! skip_proofs;
    9.47 +
    9.48      val pos = Position.thread_data ();
    9.49      fun err msg = cat_error msg
    9.50        ("The error(s) above occurred for the goal statement:\n" ^
    9.51 @@ -290,8 +302,11 @@
    9.52  
    9.53      val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops);
    9.54  
    9.55 +    fun tac' args st =
    9.56 +      if skip then ALLGOALS Skip_Proof.cheat_tac st before Skip_Proof.report ctxt
    9.57 +      else tac args st;
    9.58      fun result () =
    9.59 -      (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
    9.60 +      (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
    9.61          NONE => err "Tactic failed"
    9.62        | SOME st =>
    9.63            let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
    9.64 @@ -300,7 +315,7 @@
    9.65              else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
    9.66            end);
    9.67      val res =
    9.68 -      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
    9.69 +      if immediate orelse schematic orelse not future orelse skip
    9.70        then result ()
    9.71        else future_result ctxt' (fork ~1 result) (Thm.term_of stmt);
    9.72    in

    10.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 27 14:50:30 2013 +0100
    10.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 27 16:38:25 2013 +0100
    10.3 @@ -44,7 +44,7 @@
    10.4      Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
    10.5        "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
    10.6        "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter",
    10.7 -      "jedit_timing_threshold", "threads", "threads_trace", "parallel_proofs",
    10.8 +      "jedit_timing_threshold", "skip_proofs", "threads", "threads_trace", "parallel_proofs",
    10.9        "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
   10.10        "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
   10.11        "editor_update_delay", "editor_chart_delay")