Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/HOL/Examples/ (Isabelle Prover Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quelle Iff_Oracle.thy

Sprache: Isabelle

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

section ‹Example of Declaring an Oracle›

theory Iff_Oracle
  imports Main
begin

subsection ‹Oracle declaration›

text ‹
This oracle makes tautologies of the form prop‹P ⟷ P ⟷ P ⟷ P›.
The length is specified by an integer, which is checked to be even
and positive.
›

oracle iff_oracle = ‹
let
fun mk_iff 1 = Var (("P", 0), typ‹bool›)
| mk_iff n = HOLogic.mk_eq (Var (("P", 0), typ‹bool›), 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
›

subsection ‹Oracle as low-level rule›

ML ‹iff_oracle (🚫, 2)›
ML ‹iff_oracle (🚫, 10)›

ML ‹
🚫 (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (🚫, 10)]) = [🚫‹iff_oracle›]);
›

text ‹These oracle calls had better fail.›

ML ‹
(iff_oracle (🚫, 5); error "Bad oracle")
handle Fail _ => writeln "Oracle failed, as expected"
›

ML ‹
(iff_oracle (🚫, 1); error "Bad oracle")
handle Fail _ => writeln "Oracle failed, as expected"
›

subsection ‹Oracle as proof method›

method_setup iff =
  ‹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))›

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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-29) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

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.