# HG changeset patch
# User wenzelm
# Date 1364398705 -3600
# Node ID 63327f679cff1b93f8f01c460a8b3036e986a59e
# Parent  c713c9505f6879e40953b189c0f24ddc1a72d0c6
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);

diff -r c713c9505f68 -r 63327f679cff NEWS
--- a/NEWS	Wed Mar 27 14:50:30 2013 +0100
+++ b/NEWS	Wed Mar 27 16:38:25 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 ***
 
diff -r c713c9505f68 -r 63327f679cff etc/options
--- a/etc/options	Wed Mar 27 14:50:30 2013 +0100
+++ b/etc/options	Wed Mar 27 16:38:25 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"
diff -r c713c9505f68 -r 63327f679cff src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/HOL/ROOT	Wed Mar 27 16:38:25 2013 +0100
@@ -424,7 +424,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 +
diff -r c713c9505f68 -r 63327f679cff src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 27 16:38:25 2013 +0100
@@ -1093,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 c713c9505f68 -r 63327f679cff src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 27 16:38:25 2013 +0100
@@ -29,7 +29,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
@@ -229,7 +228,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
@@ -522,7 +520,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 +529,7 @@
         else ();
     in
       if skip andalso not no_skip then
-        SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy))
+        SkipProof (0, (finish (Proof.global_skip_proof true prf), gthy))
       else Proof (Proof_Node.init prf, (finish, gthy))
     end
   | _ => raise UNDEF));
diff -r c713c9505f68 -r 63327f679cff src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Wed Mar 27 16:38:25 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 c713c9505f68 -r 63327f679cff src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Mar 27 16:38:25 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 "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 c713c9505f68 -r 63327f679cff src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/Pure/Tools/build.ML	Wed Mar 27 16:38:25 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 c713c9505f68 -r 63327f679cff src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/Pure/goal.ML	Wed Mar 27 16:38:25 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 ->
@@ -196,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;
@@ -263,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" ^
@@ -290,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
@@ -300,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
diff -r c713c9505f68 -r 63327f679cff src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 27 14:50:30 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 27 16:38:25 2013 +0100
@@ -44,7 +44,7 @@
     Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
       "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",
+      "jedit_timing_threshold", "skip_proofs", "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")