src/HOL/ex/Iff_Oracle.thy
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59030 67baff6f697c
child 60754 02924903a6fd
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm@40239
     1
(*  Title:      HOL/ex/Iff_Oracle.thy
paulson@1537
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@40239
     3
    Author:     Makarius
paulson@1537
     4
*)
paulson@1537
     5
wenzelm@59030
     6
section \<open>Example of Declaring an Oracle\<close>
paulson@16063
     7
wenzelm@29752
     8
theory Iff_Oracle
wenzelm@40239
     9
imports Main
wenzelm@16832
    10
begin
wenzelm@3817
    11
wenzelm@59030
    12
subsection \<open>Oracle declaration\<close>
wenzelm@16832
    13
wenzelm@59030
    14
text \<open>
wenzelm@59030
    15
  This oracle makes tautologies of the form @{prop "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"}.
wenzelm@16832
    16
  The length is specified by an integer, which is checked to be even
wenzelm@16832
    17
  and positive.
wenzelm@59030
    18
\<close>
wenzelm@3817
    19
wenzelm@59030
    20
oracle iff_oracle = \<open>
wenzelm@16832
    21
  let
wenzelm@40239
    22
    fun mk_iff 1 = Var (("P", 0), @{typ bool})
wenzelm@40239
    23
      | mk_iff n = HOLogic.mk_eq (Var (("P", 0), @{typ bool}), mk_iff (n - 1));
wenzelm@16832
    24
  in
wenzelm@28290
    25
    fn (thy, n) =>
wenzelm@16832
    26
      if n > 0 andalso n mod 2 = 0
wenzelm@59621
    27
      then Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
wenzelm@16832
    28
      else raise Fail ("iff_oracle: " ^ string_of_int n)
wenzelm@16832
    29
  end
wenzelm@59030
    30
\<close>
wenzelm@3817
    31
wenzelm@16832
    32
wenzelm@59030
    33
subsection \<open>Oracle as low-level rule\<close>
wenzelm@59030
    34
wenzelm@59030
    35
ML \<open>iff_oracle (@{theory}, 2)\<close>
wenzelm@59030
    36
ML \<open>iff_oracle (@{theory}, 10)\<close>
wenzelm@3817
    37
wenzelm@59030
    38
ML \<open>
wenzelm@59030
    39
  Thm.peek_status (iff_oracle (@{theory}, 10));
wenzelm@59030
    40
  @{assert} (#oracle it);
wenzelm@59030
    41
\<close>
wenzelm@3817
    42
wenzelm@59030
    43
text \<open>These oracle calls had better fail.\<close>
wenzelm@3817
    44
wenzelm@59030
    45
ML \<open>
wenzelm@59030
    46
  (iff_oracle (@{theory}, 5); error "Bad oracle")
wenzelm@59030
    47
    handle Fail _ => writeln "Oracle failed, as expected"
wenzelm@59030
    48
\<close>
wenzelm@59030
    49
wenzelm@59030
    50
ML \<open>
wenzelm@40239
    51
  (iff_oracle (@{theory}, 1); error "Bad oracle")
wenzelm@59030
    52
    handle Fail _ => writeln "Oracle failed, as expected"
wenzelm@59030
    53
\<close>
wenzelm@3817
    54
wenzelm@16832
    55
wenzelm@59030
    56
subsection \<open>Oracle as proof method\<close>
wenzelm@3817
    57
wenzelm@59030
    58
method_setup iff =
wenzelm@59030
    59
  \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
wenzelm@30510
    60
    SIMPLE_METHOD
wenzelm@42361
    61
      (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
wenzelm@59030
    62
        handle Fail _ => no_tac))\<close>
wenzelm@3817
    63
wenzelm@16832
    64
wenzelm@59030
    65
lemma "A \<longleftrightarrow> A"
wenzelm@16832
    66
  by (iff 2)
wenzelm@3817
    67
wenzelm@59030
    68
lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
wenzelm@16832
    69
  by (iff 10)
wenzelm@16832
    70
wenzelm@59030
    71
lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
wenzelm@16832
    72
  apply (iff 5)?
wenzelm@16832
    73
  oops
wenzelm@16832
    74
wenzelm@16832
    75
lemma A
wenzelm@16832
    76
  apply (iff 1)?
wenzelm@16832
    77
  oops
wenzelm@3817
    78
paulson@16063
    79
end