src/HOL/ex/Iff_Oracle.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 60754 02924903a6fd
child 69597 ff784d5a5bfb
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/Iff_Oracle.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 *)
     5 
     6 section \<open>Example of Declaring an Oracle\<close>
     7 
     8 theory Iff_Oracle
     9 imports Main
    10 begin
    11 
    12 subsection \<open>Oracle declaration\<close>
    13 
    14 text \<open>
    15   This oracle makes tautologies of the form @{prop "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"}.
    16   The length is specified by an integer, which is checked to be even
    17   and positive.
    18 \<close>
    19 
    20 oracle iff_oracle = \<open>
    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.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
    28       else raise Fail ("iff_oracle: " ^ string_of_int n)
    29   end
    30 \<close>
    31 
    32 
    33 subsection \<open>Oracle as low-level rule\<close>
    34 
    35 ML \<open>iff_oracle (@{theory}, 2)\<close>
    36 ML \<open>iff_oracle (@{theory}, 10)\<close>
    37 
    38 ML \<open>
    39   Thm.peek_status (iff_oracle (@{theory}, 10));
    40   @{assert} (#oracle it);
    41 \<close>
    42 
    43 text \<open>These oracle calls had better fail.\<close>
    44 
    45 ML \<open>
    46   (iff_oracle (@{theory}, 5); error "Bad oracle")
    47     handle Fail _ => writeln "Oracle failed, as expected"
    48 \<close>
    49 
    50 ML \<open>
    51   (iff_oracle (@{theory}, 1); error "Bad oracle")
    52     handle Fail _ => writeln "Oracle failed, as expected"
    53 \<close>
    54 
    55 
    56 subsection \<open>Oracle as proof method\<close>
    57 
    58 method_setup iff =
    59   \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
    60     SIMPLE_METHOD
    61       (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)])
    62         handle Fail _ => no_tac))\<close>
    63 
    64 
    65 lemma "A \<longleftrightarrow> A"
    66   by (iff 2)
    67 
    68 lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
    69   by (iff 10)
    70 
    71 lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
    72   apply (iff 5)?
    73   oops
    74 
    75 lemma A
    76   apply (iff 1)?
    77   oops
    78 
    79 end