src/HOL/ex/Iff_Oracle.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 42814 5af15f1e2ef6
child 50126 3dec88149176
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/ex/Iff_Oracle.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 *)
     5 
     6 header {* Example of Declaring an Oracle *}
     7 
     8 theory Iff_Oracle
     9 imports Main
    10 begin
    11 
    12 subsection {* Oracle declaration *}
    13 
    14 text {*
    15   This oracle makes tautologies of the form @{prop "P <-> P <-> P <-> P"}.
    16   The length is specified by an integer, which is checked to be even
    17   and positive.
    18 *}
    19 
    20 oracle iff_oracle = {*
    21   let
    22     fun mk_iff 1 = Var (("P", 0), @{typ bool})
    23       | mk_iff n = HOLogic.mk_eq (Var (("P", 0), @{typ bool}), mk_iff (n - 1));
    24   in
    25     fn (thy, n) =>
    26       if n > 0 andalso n mod 2 = 0
    27       then Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
    28       else raise Fail ("iff_oracle: " ^ string_of_int n)
    29   end
    30 *}
    31 
    32 
    33 subsection {* Oracle as low-level rule *}
    34 
    35 ML {* iff_oracle (@{theory}, 2) *}
    36 ML {* iff_oracle (@{theory}, 10) *}
    37 ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *}
    38 
    39 text {* These oracle calls had better fail. *}
    40 
    41 ML {*
    42   (iff_oracle (@{theory}, 5); error "Bad oracle")
    43     handle Fail _ => warning "Oracle failed, as expected"
    44 *}
    45 
    46 ML {*
    47   (iff_oracle (@{theory}, 1); error "Bad oracle")
    48     handle Fail _ => warning "Oracle failed, as expected"
    49 *}
    50 
    51 
    52 subsection {* Oracle as proof method *}
    53 
    54 method_setup iff = {*
    55   Scan.lift Parse.nat >> (fn n => fn ctxt =>
    56     SIMPLE_METHOD
    57       (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
    58         handle Fail _ => no_tac))
    59 *}
    60 
    61 
    62 lemma "A <-> A"
    63   by (iff 2)
    64 
    65 lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
    66   by (iff 10)
    67 
    68 lemma "A <-> A <-> A <-> A <-> A"
    69   apply (iff 5)?
    70   oops
    71 
    72 lemma A
    73   apply (iff 1)?
    74   oops
    75 
    76 end