src/HOL/SVC_Oracle.ML
author paulson
Tue Aug 03 13:08:58 1999 +0200 (1999-08-03)
changeset 7162 8737390d1d0a
parent 7144 0feee8201d67
child 7187 676027b1d770
permissions -rw-r--r--
biconditionals and the natural numbers
paulson@7144
     1
(*  Title:      HOL/SVC_Oracle
paulson@7144
     2
    ID:         $Id$
paulson@7144
     3
    Author:     Lawrence C Paulson
paulson@7144
     4
    Copyright   1999  University of Cambridge
paulson@7144
     5
paulson@7144
     6
Installing the oracle for SVC (Stanford Validity Checker)
paulson@7144
     7
paulson@7144
     8
Based upon the work of Søren T. Heilmann
paulson@7144
     9
*)
paulson@7144
    10
paulson@7144
    11
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
paulson@7144
    12
  abstracted.  Use via compose_tac, which performs no lifting but will
paulson@7144
    13
  instantiate variables.*)
paulson@7162
    14
fun svc_tac i st = 
paulson@7162
    15
  let val prem = List.nth (prems_of st, i-1)
paulson@7162
    16
      val th = invoke_oracle thy "svc_oracle" 
paulson@7162
    17
	             (#sign (rep_thm st), Svc.OracleExn prem)
paulson@7162
    18
   in 
paulson@7162
    19
      compose_tac (false, th, 0) i st
paulson@7162
    20
   end 
paulson@7162
    21
   handle Svc.OracleExn _ => Seq.empty
paulson@7162
    22
	| Subscript       => Seq.empty;
paulson@7144
    23
paulson@7144
    24