products/Sources/formale Sprachen/Isabelle/Pure/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: SML

Original von: Isabelle©
(*  Title:      Pure/skip_proof.ML
    Author:     Makarius

Skip proof via oracle invocation.
*)

signature SKIP_PROOF =
sig
  val report: Proof.context -> unit
  val make_thm_cterm: cterm -> thm
  val make_thm: theory -> term -> thm
  val cheat_tac: Proof.context -> int -> tactic
end;

structure Skip_Proof: SKIP_PROOF =
struct

(* report *)

fun report ctxt =
  if Context_Position.reports_enabled ctxt then
    Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
  else ();


(* oracle setup *)

val (_, make_thm_cterm) =
  Context.>>>
    (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)));

fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);


(* cheat_tac -- 'sorry' *)

fun cheat_tac ctxt = SUBGOAL (fn (goal, i) =>
  let
    val thy = Proof_Context.theory_of ctxt;
    val assms = Assumption.all_assms_of ctxt;
    val cheat = make_thm thy (Logic.list_implies (map Thm.term_of assms, goal));
    val thm = Drule.implies_elim_list cheat (map Thm.assume assms);
  in PRIMITIVE (Drule.with_subgoal i (Thm.elim_implies thm)) end);

end;

¤ Dauer der Verarbeitung: 0.10 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff