src/FOL/ex/IffOracle.thy
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 23153 3cc4a80c4d30
child 25940 6942f3c5dec8
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
     1
(*  Title:      FOL/ex/IffOracle.thy
1537
3f51f0945a3e Example of declaring oracles
paulson
parents:
diff changeset
     2
    ID:         $Id$
3f51f0945a3e Example of declaring oracles
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3f51f0945a3e Example of declaring oracles
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
3f51f0945a3e Example of declaring oracles
paulson
parents:
diff changeset
     5
*)
3f51f0945a3e Example of declaring oracles
paulson
parents:
diff changeset
     6
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
     7
header {* Example of Declaring an Oracle *}
16063
7dd4eb2c8055 oracle example converted to Isar
paulson
parents: 3817
diff changeset
     8
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
     9
theory IffOracle
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    10
imports FOL
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    11
begin
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    12
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    13
subsection {* Oracle declaration *}
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    14
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    15
text {*
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    16
  This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    17
  The length is specified by an integer, which is checked to be even
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    18
  and positive.
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    19
*}
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    20
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    21
oracle iff_oracle (int) = {*
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    22
  let
23153
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    23
    fun mk_iff 1 = Var (("P", 0), @{typ o})
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    24
      | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    25
  in
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    26
    fn thy => fn n =>
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    27
      if n > 0 andalso n mod 2 = 0
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    28
      then FOLogic.mk_Trueprop (mk_iff n)
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    29
      else raise Fail ("iff_oracle: " ^ string_of_int n)
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    30
  end
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    31
*}
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    32
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    33
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    34
subsection {* Oracle as low-level rule *}
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    35
23153
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    36
ML {* iff_oracle @{theory} 2 *}
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    37
ML {* iff_oracle @{theory} 10 *}
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    38
ML {* #der (Thm.rep_thm it) *}
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    39
21863
2cfc838297ff tracing instead of warning
webertj
parents: 18678
diff changeset
    40
text {* These oracle calls had better fail. *}
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    41
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    42
ML {*
23153
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    43
  (iff_oracle @{theory} 5; error "?")
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    44
    handle Fail _ => warning "Oracle failed, as expected"
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    45
*}
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    46
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    47
ML {*
23153
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    48
  (iff_oracle @{theory} 1; error "?")
3cc4a80c4d30 tuned oracle setup;
wenzelm
parents: 21863
diff changeset
    49
    handle Fail _ => warning "Oracle failed, as expected"
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    50
*}
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    51
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    52
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    53
subsection {* Oracle as proof method *}
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    54
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    55
method_setup iff = {*
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    56
  Method.simple_args Args.nat (fn n => fn ctxt =>
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    57
    Method.SIMPLE_METHOD
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    58
      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    59
        handle Fail _ => no_tac))
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    60
*} "iff oracle"
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    61
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    62
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    63
lemma "A <-> A"
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    64
  by (iff 2)
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    65
16832
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    66
lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    67
  by (iff 10)
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    68
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    69
lemma "A <-> A <-> A <-> A <-> A"
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    70
  apply (iff 5)?
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    71
  oops
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    72
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    73
lemma A
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    74
  apply (iff 1)?
f220d1df0f4e new type-safe interface;
wenzelm
parents: 16417
diff changeset
    75
  oops
3817
f20f193d42b4 removed declIffOracle;
wenzelm
parents: 1537
diff changeset
    76
16063
7dd4eb2c8055 oracle example converted to Isar
paulson
parents: 3817
diff changeset
    77
end