src/HOL/ex/Iff_Oracle.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 50126 3dec88149176
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
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@16832
     6
header {* Example of Declaring an Oracle *}
paulson@16063
     7
wenzelm@29752
     8
theory Iff_Oracle
wenzelm@40239
     9
imports Main
wenzelm@16832
    10
begin
wenzelm@3817
    11
wenzelm@16832
    12
subsection {* Oracle declaration *}
wenzelm@16832
    13
wenzelm@16832
    14
text {*
wenzelm@40239
    15
  This oracle makes tautologies of the form @{prop "P <-> P <-> P <-> P"}.
wenzelm@16832
    16
  The length is specified by an integer, which is checked to be even
wenzelm@16832
    17
  and positive.
wenzelm@16832
    18
*}
wenzelm@3817
    19
wenzelm@28290
    20
oracle iff_oracle = {*
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@40239
    27
      then Thm.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@16832
    30
*}
wenzelm@3817
    31
wenzelm@16832
    32
wenzelm@16832
    33
subsection {* Oracle as low-level rule *}
wenzelm@3817
    34
wenzelm@28290
    35
ML {* iff_oracle (@{theory}, 2) *}
wenzelm@28290
    36
ML {* iff_oracle (@{theory}, 10) *}
wenzelm@50126
    37
ML {* Thm.peek_status (iff_oracle (@{theory}, 10)) *}
wenzelm@16832
    38
webertj@21863
    39
text {* These oracle calls had better fail. *}
wenzelm@3817
    40
wenzelm@16832
    41
ML {*
wenzelm@40239
    42
  (iff_oracle (@{theory}, 5); error "Bad oracle")
wenzelm@23153
    43
    handle Fail _ => warning "Oracle failed, as expected"
wenzelm@16832
    44
*}
wenzelm@3817
    45
wenzelm@16832
    46
ML {*
wenzelm@40239
    47
  (iff_oracle (@{theory}, 1); error "Bad oracle")
wenzelm@23153
    48
    handle Fail _ => warning "Oracle failed, as expected"
wenzelm@16832
    49
*}
wenzelm@3817
    50
wenzelm@16832
    51
wenzelm@16832
    52
subsection {* Oracle as proof method *}
wenzelm@3817
    53
wenzelm@16832
    54
method_setup iff = {*
wenzelm@36960
    55
  Scan.lift Parse.nat >> (fn n => fn ctxt =>
wenzelm@30510
    56
    SIMPLE_METHOD
wenzelm@42361
    57
      (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
wenzelm@16832
    58
        handle Fail _ => no_tac))
wenzelm@42814
    59
*}
wenzelm@3817
    60
wenzelm@16832
    61
wenzelm@16832
    62
lemma "A <-> A"
wenzelm@16832
    63
  by (iff 2)
wenzelm@3817
    64
wenzelm@16832
    65
lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
wenzelm@16832
    66
  by (iff 10)
wenzelm@16832
    67
wenzelm@16832
    68
lemma "A <-> A <-> A <-> A <-> A"
wenzelm@16832
    69
  apply (iff 5)?
wenzelm@16832
    70
  oops
wenzelm@16832
    71
wenzelm@16832
    72
lemma A
wenzelm@16832
    73
  apply (iff 1)?
wenzelm@16832
    74
  oops
wenzelm@3817
    75
paulson@16063
    76
end