src/Pure/skip_proof.ML
author wenzelm
Fri Jul 17 21:40:47 2015 +0200 (2015-07-17)
changeset 60749 f727b99faaf7
parent 59621 291934bac95e
child 60820 d0a88a2182a8
permissions -rw-r--r--
skeleton for interactive debugger;
wenzelm@51551
     1
(*  Title:      Pure/skip_proof.ML
wenzelm@51551
     2
    Author:     Makarius
wenzelm@6888
     3
wenzelm@51551
     4
Skip proof via oracle invocation.
wenzelm@6888
     5
*)
wenzelm@6888
     6
wenzelm@56438
     7
val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
wenzelm@56438
     8
val quick_and_dirty = Config.bool quick_and_dirty_raw;
wenzelm@56438
     9
wenzelm@6888
    10
signature SKIP_PROOF =
wenzelm@6888
    11
sig
wenzelm@51551
    12
  val report: Proof.context -> unit
wenzelm@42409
    13
  val make_thm_cterm: cterm -> thm
wenzelm@11892
    14
  val make_thm: theory -> term -> thm
wenzelm@59498
    15
  val cheat_tac: Proof.context -> int -> tactic
wenzelm@6888
    16
end;
wenzelm@6888
    17
wenzelm@32970
    18
structure Skip_Proof: SKIP_PROOF =
wenzelm@6888
    19
struct
wenzelm@6888
    20
wenzelm@51551
    21
(* report *)
wenzelm@51551
    22
wenzelm@51551
    23
fun report ctxt =
wenzelm@56294
    24
  if Context_Position.is_visible ctxt then
wenzelm@56333
    25
    Output.report [Markup.markup Markup.bad "Skipped proof"]
wenzelm@56294
    26
  else ();
wenzelm@51551
    27
wenzelm@51551
    28
wenzelm@11892
    29
(* oracle setup *)
wenzelm@6888
    30
wenzelm@42409
    31
val (_, make_thm_cterm) =
wenzelm@56436
    32
  Context.>>>
wenzelm@56436
    33
    (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I)));
wenzelm@42409
    34
wenzelm@59621
    35
fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
wenzelm@6888
    36
wenzelm@11892
    37
wenzelm@51551
    38
(* cheat_tac *)
wenzelm@11892
    39
wenzelm@59498
    40
fun cheat_tac ctxt i st =
wenzelm@59498
    41
  resolve_tac ctxt [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
berghofe@26530
    42
wenzelm@6888
    43
end;