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" ›
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 und die Messung sind noch experimentell.
