| Quellcodebibliothek Statistik Leitseite 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.thySprache: 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
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09