Quelle Iff_Oracle.thy Sprache: 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

quality98%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.