(*  Title:      FOL/ex/IffOracle.thy

    ID:         $Id$

    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

    Copyright   1996  University of Cambridge

*)

header {* Example of Declaring an Oracle *}

theory IffOracle

imports FOL

begin

subsection {* Oracle declaration *}

text {*

  This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.

  The length is specified by an integer, which is checked to be even

  and positive.

*}

oracle iff_oracle (int) = {*

  let

    fun mk_iff 1 = Var (("P", 0), @{typ o})

      | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);

  in

    fn thy => fn n =>

      if n > 0 andalso n mod 2 = 0

      then FOLogic.mk_Trueprop (mk_iff n)

      else raise Fail ("iff_oracle: " ^ string_of_int n)

  end

*}

subsection {* Oracle as low-level rule *}

ML {* iff_oracle @{theory} 2 *}

ML {* iff_oracle @{theory} 10 *}

text {* These oracle calls had better fail. *}

ML {*

  (iff_oracle @{theory} 5; error "?")

    handle Fail _ => warning "Oracle failed, as expected"

*}

ML {*

  (iff_oracle @{theory} 1; error "?")

    handle Fail _ => warning "Oracle failed, as expected"

*}

subsection {* Oracle as proof method *}

method_setup iff = {*

  Method.simple_args Args.nat (fn n => fn ctxt =>

    Method.SIMPLE_METHOD

      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))

        handle Fail _ => no_tac))

*} "iff oracle"

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