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