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
```