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