src/FOL/ex/Iff_Oracle.thy
changeset 40253 f99ec71de82d
parent 40252 029400b6c893
parent 40242 bb433b0668b8
child 40254 6d1ebaa7a4ba
child 40257 323f7aad54b0
     1.1 --- a/src/FOL/ex/Iff_Oracle.thy	Fri Oct 29 11:04:41 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,76 +0,0 @@
     1.4 -(*  Title:      FOL/ex/Iff_Oracle.thy
     1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -    Copyright   1996  University of Cambridge
     1.7 -*)
     1.8 -
     1.9 -header {* Example of Declaring an Oracle *}
    1.10 -
    1.11 -theory Iff_Oracle
    1.12 -imports FOL
    1.13 -begin
    1.14 -
    1.15 -subsection {* Oracle declaration *}
    1.16 -
    1.17 -text {*
    1.18 -  This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.
    1.19 -  The length is specified by an integer, which is checked to be even
    1.20 -  and positive.
    1.21 -*}
    1.22 -
    1.23 -oracle iff_oracle = {*
    1.24 -  let
    1.25 -    fun mk_iff 1 = Var (("P", 0), @{typ o})
    1.26 -      | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
    1.27 -  in
    1.28 -    fn (thy, n) =>
    1.29 -      if n > 0 andalso n mod 2 = 0
    1.30 -      then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
    1.31 -      else raise Fail ("iff_oracle: " ^ string_of_int n)
    1.32 -  end
    1.33 -*}
    1.34 -
    1.35 -
    1.36 -subsection {* Oracle as low-level rule *}
    1.37 -
    1.38 -ML {* iff_oracle (@{theory}, 2) *}
    1.39 -ML {* iff_oracle (@{theory}, 10) *}
    1.40 -ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *}
    1.41 -
    1.42 -text {* These oracle calls had better fail. *}
    1.43 -
    1.44 -ML {*
    1.45 -  (iff_oracle (@{theory}, 5); error "?")
    1.46 -    handle Fail _ => warning "Oracle failed, as expected"
    1.47 -*}
    1.48 -
    1.49 -ML {*
    1.50 -  (iff_oracle (@{theory}, 1); error "?")
    1.51 -    handle Fail _ => warning "Oracle failed, as expected"
    1.52 -*}
    1.53 -
    1.54 -
    1.55 -subsection {* Oracle as proof method *}
    1.56 -
    1.57 -method_setup iff = {*
    1.58 -  Scan.lift Parse.nat >> (fn n => fn ctxt =>
    1.59 -    SIMPLE_METHOD
    1.60 -      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
    1.61 -        handle Fail _ => no_tac))
    1.62 -*} "iff oracle"
    1.63 -
    1.64 -
    1.65 -lemma "A <-> A"
    1.66 -  by (iff 2)
    1.67 -
    1.68 -lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
    1.69 -  by (iff 10)
    1.70 -
    1.71 -lemma "A <-> A <-> A <-> A <-> A"
    1.72 -  apply (iff 5)?
    1.73 -  oops
    1.74 -
    1.75 -lemma A
    1.76 -  apply (iff 1)?
    1.77 -  oops
    1.78 -
    1.79 -end