src/HOL/ex/SVC_Oracle.thy
author wenzelm
Wed Aug 29 11:10:28 2007 +0200 (2007-08-29)
changeset 24470 41c81e23c08d
parent 20813 379ce56e5dc2
child 25919 8b1c0d434824
permissions -rw-r--r--
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm@12869
     1
(*  Title:      HOL/ex/SVC_Oracle.thy
wenzelm@12869
     2
    ID:         $Id$
wenzelm@12869
     3
    Author:     Lawrence C Paulson
wenzelm@12869
     4
    Copyright   1999  University of Cambridge
wenzelm@12869
     5
wenzelm@17388
     6
Based upon the work of Søren T. Heilmann.
wenzelm@17388
     7
*)
wenzelm@12869
     8
wenzelm@17388
     9
header {* Installing an oracle for SVC (Stanford Validity Checker) *}
wenzelm@12869
    10
wenzelm@16836
    11
theory SVC_Oracle
wenzelm@16836
    12
imports Main
wenzelm@24470
    13
uses "svc_funcs.ML"
wenzelm@16836
    14
begin
wenzelm@12869
    15
wenzelm@12869
    16
consts
wenzelm@12869
    17
  iff_keep :: "[bool, bool] => bool"
wenzelm@12869
    18
  iff_unfold :: "[bool, bool] => bool"
wenzelm@12869
    19
wenzelm@16836
    20
hide const iff_keep iff_unfold
wenzelm@16836
    21
wenzelm@12869
    22
oracle
wenzelm@16836
    23
  svc_oracle ("term") = Svc.oracle
wenzelm@12869
    24
wenzelm@24470
    25
ML {*
wenzelm@24470
    26
(*
wenzelm@24470
    27
Installing the oracle for SVC (Stanford Validity Checker)
wenzelm@24470
    28
wenzelm@24470
    29
The following code merely CALLS the oracle;
wenzelm@24470
    30
  the soundness-critical functions are at svc_funcs.ML
wenzelm@24470
    31
wenzelm@24470
    32
Based upon the work of Søren T. Heilmann
wenzelm@24470
    33
*)
wenzelm@24470
    34
wenzelm@24470
    35
wenzelm@24470
    36
(*Generalize an Isabelle formula, replacing by Vars
wenzelm@24470
    37
  all subterms not intelligible to SVC.*)
wenzelm@24470
    38
fun svc_abstract t =
wenzelm@24470
    39
  let
wenzelm@24470
    40
    (*The oracle's result is given to the subgoal using compose_tac because
wenzelm@24470
    41
      its premises are matched against the assumptions rather than used
wenzelm@24470
    42
      to make subgoals.  Therefore , abstraction must copy the parameters
wenzelm@24470
    43
      precisely and make them available to all generated Vars.*)
wenzelm@24470
    44
    val params = Term.strip_all_vars t
wenzelm@24470
    45
    and body   = Term.strip_all_body t
wenzelm@24470
    46
    val Us = map #2 params
wenzelm@24470
    47
    val nPar = length params
wenzelm@24470
    48
    val vname = ref "V_a"
wenzelm@24470
    49
    val pairs = ref ([] : (term*term) list)
wenzelm@24470
    50
    fun insert t =
wenzelm@24470
    51
        let val T = fastype_of t
wenzelm@24470
    52
            val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
wenzelm@24470
    53
        in  vname := Symbol.bump_string (!vname);
wenzelm@24470
    54
            pairs := (t, v) :: !pairs;
wenzelm@24470
    55
            v
wenzelm@24470
    56
        end;
wenzelm@24470
    57
    fun replace t =
wenzelm@24470
    58
        case t of
wenzelm@24470
    59
            Free _  => t  (*but not existing Vars, lest the names clash*)
wenzelm@24470
    60
          | Bound _ => t
wenzelm@24470
    61
          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
wenzelm@24470
    62
                      SOME v => v
wenzelm@24470
    63
                    | NONE   => insert t)
wenzelm@24470
    64
    (*abstraction of a numeric literal*)
wenzelm@24470
    65
    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
wenzelm@24470
    66
      | lit (t as Const(@{const_name HOL.one}, _)) = t
wenzelm@24470
    67
      | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
wenzelm@24470
    68
      | lit t = replace t
wenzelm@24470
    69
    (*abstraction of a real/rational expression*)
wenzelm@24470
    70
    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    71
      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    72
      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    73
      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    74
      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
wenzelm@24470
    75
      | rat t = lit t
wenzelm@24470
    76
    (*abstraction of an integer expression: no div, mod*)
wenzelm@24470
    77
    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
wenzelm@24470
    78
      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
wenzelm@24470
    79
      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
wenzelm@24470
    80
      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
wenzelm@24470
    81
      | int t = lit t
wenzelm@24470
    82
    (*abstraction of a natural number expression: no minus*)
wenzelm@24470
    83
    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
wenzelm@24470
    84
      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
wenzelm@24470
    85
      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
wenzelm@24470
    86
      | nat t = lit t
wenzelm@24470
    87
    (*abstraction of a relation: =, <, <=*)
wenzelm@24470
    88
    fun rel (T, c $ x $ y) =
wenzelm@24470
    89
            if T = HOLogic.realT then c $ (rat x) $ (rat y)
wenzelm@24470
    90
            else if T = HOLogic.intT then c $ (int x) $ (int y)
wenzelm@24470
    91
            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
wenzelm@24470
    92
            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
wenzelm@24470
    93
            else replace (c $ x $ y)   (*non-numeric comparison*)
wenzelm@24470
    94
    (*abstraction of a formula*)
wenzelm@24470
    95
    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
wenzelm@24470
    96
      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
wenzelm@24470
    97
      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
wenzelm@24470
    98
      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
wenzelm@24470
    99
      | fm ((c as Const("True", _))) = c
wenzelm@24470
   100
      | fm ((c as Const("False", _))) = c
wenzelm@24470
   101
      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
wenzelm@24470
   102
      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
wenzelm@24470
   103
      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
wenzelm@24470
   104
      | fm t = replace t
wenzelm@24470
   105
    (*entry point, and abstraction of a meta-formula*)
wenzelm@24470
   106
    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
wenzelm@24470
   107
      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
wenzelm@24470
   108
      | mt t = fm t  (*it might be a formula*)
wenzelm@24470
   109
  in (list_all (params, mt body), !pairs) end;
wenzelm@24470
   110
wenzelm@24470
   111
wenzelm@24470
   112
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
wenzelm@24470
   113
  abstracted.  Use via compose_tac, which performs no lifting but will
wenzelm@24470
   114
  instantiate variables.*)
wenzelm@24470
   115
wenzelm@24470
   116
fun svc_tac i st =
wenzelm@24470
   117
  let
wenzelm@24470
   118
    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
wenzelm@24470
   119
    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
wenzelm@24470
   120
   in compose_tac (false, th, 0) i st end
wenzelm@24470
   121
   handle TERM _ => no_tac st;
wenzelm@24470
   122
wenzelm@24470
   123
wenzelm@24470
   124
(*check if user has SVC installed*)
wenzelm@24470
   125
fun svc_enabled () = getenv "SVC_HOME" <> "";
wenzelm@24470
   126
fun if_svc_enabled f x = if svc_enabled () then f x else ();
wenzelm@24470
   127
*}
wenzelm@20813
   128
wenzelm@12869
   129
end