src/Pure/skip_proof.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 64677 8dc24130e8fe
permissions -rw-r--r--
more robust sorted_entries;
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@6888
     7
signature SKIP_PROOF =
wenzelm@6888
     8
sig
wenzelm@51551
     9
  val report: Proof.context -> unit
wenzelm@42409
    10
  val make_thm_cterm: cterm -> thm
wenzelm@11892
    11
  val make_thm: theory -> term -> thm
wenzelm@59498
    12
  val cheat_tac: Proof.context -> int -> tactic
wenzelm@6888
    13
end;
wenzelm@6888
    14
wenzelm@32970
    15
structure Skip_Proof: SKIP_PROOF =
wenzelm@6888
    16
struct
wenzelm@6888
    17
wenzelm@51551
    18
(* report *)
wenzelm@51551
    19
wenzelm@51551
    20
fun report ctxt =
wenzelm@56294
    21
  if Context_Position.is_visible ctxt then
wenzelm@64677
    22
    Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
wenzelm@56294
    23
  else ();
wenzelm@51551
    24
wenzelm@51551
    25
wenzelm@11892
    26
(* oracle setup *)
wenzelm@6888
    27
wenzelm@42409
    28
val (_, make_thm_cterm) =
wenzelm@56436
    29
  Context.>>>
wenzelm@64556
    30
    (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)));
wenzelm@42409
    31
wenzelm@59621
    32
fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
wenzelm@6888
    33
wenzelm@11892
    34
wenzelm@51551
    35
(* cheat_tac *)
wenzelm@11892
    36
wenzelm@59498
    37
fun cheat_tac ctxt i st =
wenzelm@60820
    38
  resolve_tac ctxt [make_thm (Proof_Context.theory_of ctxt) (Var (("A", 0), propT))] i st;
berghofe@26530
    39
wenzelm@6888
    40
end;