Theory Iff_Oracle

(*  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

subsection ‹Oracle declaration›

text ‹
  This oracle makes tautologies of the form propP  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), typbool)
      | mk_iff n = HOLogic.mk_eq (Var (("P", 0), typbool), mk_iff (n - 1));
    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)

subsection ‹Oracle as low-level rule›

ML iff_oracle (theory, 2)
ML iff_oracle (theory, 10)

ML assert (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (theory, 10)]) = [oracle_nameiff_oracle]);

text ‹These oracle calls had better fail.›

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

ML (iff_oracle (theory, 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 =>
      (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)?

lemma A
  apply (iff 1)?