src/HOL/Examples/Iff_Oracle.thy

A further round of proof consolidation

(*  Title:      HOL/Examples/Iff_Oracle.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Makarius
*)

section \<open>Example of Declaring an Oracle\<close>

theory Iff_Oracle
  imports Main
begin

subsection \<open>Oracle declaration\<close>

text \<open>
  This oracle makes tautologies of the form \<^prop>\<open>P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P\<close>.
  The length is specified by an integer, which is checked to be even
  and positive.
\<close>

oracle iff_oracle = \<open>
  let
    fun mk_iff 1 = Var (("P", 0), \<^typ>\<open>bool\<close>)
      | mk_iff n = HOLogic.mk_eq (Var (("P", 0), \<^typ>\<open>bool\<close>), mk_iff (n - 1));
  in
    fn (thy, n) =>
      if n > 0 andalso n mod 2 = 0
      then Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
      else raise Fail ("iff_oracle: " ^ string_of_int n)
  end
\<close>


subsection \<open>Oracle as low-level rule\<close>

ML \<open>iff_oracle (\<^theory>, 2)\<close>
ML \<open>iff_oracle (\<^theory>, 10)\<close>

ML \<open>
  \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
\<close>

text \<open>These oracle calls had better fail.\<close>

ML \<open>
  (iff_oracle (\<^theory>, 5); error "Bad oracle")
    handle Fail _ => writeln "Oracle failed, as expected"
\<close>

ML \<open>
  (iff_oracle (\<^theory>, 1); error "Bad oracle")
    handle Fail _ => writeln "Oracle failed, as expected"
\<close>


subsection \<open>Oracle as proof method\<close>

method_setup iff =
  \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
    SIMPLE_METHOD
      (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)])
        handle Fail _ => no_tac))\<close>


lemma "A \<longleftrightarrow> A"
  by (iff 2)

lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
  by (iff 10)

lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A"
  apply (iff 5)?
  oops

lemma A
  apply (iff 1)?
  oops

end