Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: SilenceOfDeprecatedMenuBar.java Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Examples/Iff_Oracle.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Makarius
*)

section \<open>Example of Declaring an Oracle\<close>

theory Iff_Oracle
  imports Main
begin

subsection \<open>Oracle declaration\<close>

text \<open>
  This oracle makes tautologies of the form \<^prop>\<open>P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P\<close>.
  The length is specified by an integer, which is checked to be even
  and positive.
\<close>

oracle iff_oracle = \<open>
  let
    fun mk_iff 1 = Var (("P", 0), \<^typ>\<open>bool\<close>)
      | mk_iff n = HOLogic.mk_eq (Var (("P", 0), \<^typ>\<open>bool\<close>), mk_iff (n - 1));
  in
    fn (thy, n) =>
      if n > 0 andalso n mod 2 = 0
      then Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
      else raise Fail ("iff_oracle: " ^ string_of_int n)
  end
\<close>

subsection \<open>Oracle as low-level rule\<close>

ML \<open>iff_oracle (\<^theory>, 2)\<close>
ML \<open>iff_oracle (\<^theory>, 10)\<close>

ML \<open>
  \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
\<close>

text \<open>These oracle calls had better fail.\<close>

ML \<open>
  (iff_oracle (\<^theory>, 5); error "Bad oracle")
    handle Fail _ => writeln "Oracle failed, as expected"
\<close>

ML \<open>
  (iff_oracle (\<^theory>, 1); error "Bad oracle")
    handle Fail _ => writeln "Oracle failed, as expected"
\<close>

subsection \<open>Oracle as proof method\<close>

method_setup iff =
  \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
    SIMPLE_METHOD
      (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)])
        handle Fail _ => no_tac))\<close>

lemma "A \ A"
  by (iff 2)

lemma "A \ A \ A \ A \ A \ A \ A \ A \ A \ A"
  by (iff 10)

lemma "A \ A \ A \ A \ A"
  apply (iff 5)?
  oops

lemma A
  apply (iff 1)?
  oops

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.