1(*  Title:      Pure/skip_proof.ML
2    Author:     Makarius
3
4Skip proof via oracle invocation.
5*)
6
7signature SKIP_PROOF =
8sig
9  val report: Proof.context -> unit
10  val make_thm_cterm: cterm -> thm
11  val make_thm: theory -> term -> thm
12  val cheat_tac: Proof.context -> int -> tactic
13end;
14
15structure Skip_Proof: SKIP_PROOF =
16struct
17
18(* report *)
19
20fun report ctxt =
21  if Context_Position.is_visible ctxt then
22    Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
23  else ();
24
25
26(* oracle setup *)
27
28val (_, make_thm_cterm) =
29  Context.>>>
30    (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)));
31
32fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
33
34
35(* cheat_tac -- 'sorry' *)
36
37fun cheat_tac ctxt = SUBGOAL (fn (goal, i) =>
38  let
39    val thy = Proof_Context.theory_of ctxt;
40    val assms = Assumption.all_assms_of ctxt;
41    val cheat = make_thm thy (Logic.list_implies (map Thm.term_of assms, goal));
42    val thm = Drule.implies_elim_list cheat (map Thm.assume assms);
43  in PRIMITIVE (Drule.with_subgoal i (Thm.elim_implies thm)) end);
44
45end;
46