src/HOL/ex/SVC_Oracle.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 25929 6bfef23e26be
child 28290 4cc2b6046258
permissions -rw-r--r--
moved global ML bindings to global place;
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*)
haftmann@25929
    65
    fun lit t = if can HOLogic.dest_number t then t else replace t;
wenzelm@24470
    66
    (*abstraction of a real/rational expression*)
wenzelm@24470
    67
    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    68
      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    69
      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    70
      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
wenzelm@24470
    71
      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
wenzelm@24470
    72
      | rat t = lit t
wenzelm@24470
    73
    (*abstraction of an integer expression: no div, mod*)
wenzelm@24470
    74
    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
wenzelm@24470
    75
      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
wenzelm@24470
    76
      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
wenzelm@24470
    77
      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
wenzelm@24470
    78
      | int t = lit t
wenzelm@24470
    79
    (*abstraction of a natural number expression: no minus*)
wenzelm@24470
    80
    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
wenzelm@24470
    81
      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
wenzelm@24470
    82
      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
wenzelm@24470
    83
      | nat t = lit t
wenzelm@24470
    84
    (*abstraction of a relation: =, <, <=*)
wenzelm@24470
    85
    fun rel (T, c $ x $ y) =
wenzelm@24470
    86
            if T = HOLogic.realT then c $ (rat x) $ (rat y)
wenzelm@24470
    87
            else if T = HOLogic.intT then c $ (int x) $ (int y)
wenzelm@24470
    88
            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
wenzelm@24470
    89
            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
wenzelm@24470
    90
            else replace (c $ x $ y)   (*non-numeric comparison*)
wenzelm@24470
    91
    (*abstraction of a formula*)
wenzelm@24470
    92
    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
wenzelm@24470
    93
      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
wenzelm@24470
    94
      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
wenzelm@24470
    95
      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
wenzelm@24470
    96
      | fm ((c as Const("True", _))) = c
wenzelm@24470
    97
      | fm ((c as Const("False", _))) = c
wenzelm@24470
    98
      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
wenzelm@24470
    99
      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
wenzelm@24470
   100
      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
wenzelm@24470
   101
      | fm t = replace t
wenzelm@24470
   102
    (*entry point, and abstraction of a meta-formula*)
wenzelm@24470
   103
    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
wenzelm@24470
   104
      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
wenzelm@24470
   105
      | mt t = fm t  (*it might be a formula*)
wenzelm@24470
   106
  in (list_all (params, mt body), !pairs) end;
wenzelm@24470
   107
wenzelm@24470
   108
wenzelm@24470
   109
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
wenzelm@24470
   110
  abstracted.  Use via compose_tac, which performs no lifting but will
wenzelm@24470
   111
  instantiate variables.*)
wenzelm@24470
   112
wenzelm@24470
   113
fun svc_tac i st =
wenzelm@24470
   114
  let
wenzelm@24470
   115
    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
wenzelm@24470
   116
    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
wenzelm@24470
   117
   in compose_tac (false, th, 0) i st end
wenzelm@24470
   118
   handle TERM _ => no_tac st;
wenzelm@24470
   119
*}
wenzelm@20813
   120
wenzelm@12869
   121
end