src/HOL/ex/SVC_Oracle.thy
author haftmann
Fri Aug 27 10:56:46 2010 +0200 (2010-08-27)
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38864 4abe644fcea5
permissions -rw-r--r--
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
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@36176
    20
hide_const iff_keep iff_unfold
wenzelm@16836
    21
wenzelm@28290
    22
oracle svc_oracle = Svc.oracle
wenzelm@12869
    23
wenzelm@24470
    24
ML {*
wenzelm@24470
    25
(*
wenzelm@24470
    26
Installing the oracle for SVC (Stanford Validity Checker)
wenzelm@24470
    27
wenzelm@24470
    28
The following code merely CALLS the oracle;
wenzelm@24470
    29
  the soundness-critical functions are at svc_funcs.ML
wenzelm@24470
    30
wenzelm@24470
    31
Based upon the work of Søren T. Heilmann
wenzelm@24470
    32
*)
wenzelm@24470
    33
wenzelm@24470
    34
wenzelm@24470
    35
(*Generalize an Isabelle formula, replacing by Vars
wenzelm@24470
    36
  all subterms not intelligible to SVC.*)
wenzelm@24470
    37
fun svc_abstract t =
wenzelm@24470
    38
  let
wenzelm@24470
    39
    (*The oracle's result is given to the subgoal using compose_tac because
wenzelm@24470
    40
      its premises are matched against the assumptions rather than used
wenzelm@24470
    41
      to make subgoals.  Therefore , abstraction must copy the parameters
wenzelm@24470
    42
      precisely and make them available to all generated Vars.*)
wenzelm@24470
    43
    val params = Term.strip_all_vars t
wenzelm@24470
    44
    and body   = Term.strip_all_body t
wenzelm@24470
    45
    val Us = map #2 params
wenzelm@24470
    46
    val nPar = length params
wenzelm@32740
    47
    val vname = Unsynchronized.ref "V_a"
wenzelm@32740
    48
    val pairs = Unsynchronized.ref ([] : (term*term) list)
wenzelm@24470
    49
    fun insert t =
wenzelm@24470
    50
        let val T = fastype_of t
wenzelm@24470
    51
            val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
wenzelm@24470
    52
        in  vname := Symbol.bump_string (!vname);
wenzelm@24470
    53
            pairs := (t, v) :: !pairs;
wenzelm@24470
    54
            v
wenzelm@24470
    55
        end;
wenzelm@24470
    56
    fun replace t =
wenzelm@24470
    57
        case t of
wenzelm@24470
    58
            Free _  => t  (*but not existing Vars, lest the names clash*)
wenzelm@24470
    59
          | Bound _ => t
wenzelm@24470
    60
          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
wenzelm@24470
    61
                      SOME v => v
wenzelm@24470
    62
                    | NONE   => insert t)
wenzelm@24470
    63
    (*abstraction of a numeric literal*)
haftmann@25929
    64
    fun lit t = if can HOLogic.dest_number t then t else replace t;
wenzelm@24470
    65
    (*abstraction of a real/rational expression*)
haftmann@35267
    66
    fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
haftmann@35267
    67
      | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
haftmann@35084
    68
      | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
haftmann@35267
    69
      | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
haftmann@35267
    70
      | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
wenzelm@24470
    71
      | rat t = lit t
wenzelm@24470
    72
    (*abstraction of an integer expression: no div, mod*)
haftmann@35267
    73
    fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
haftmann@35267
    74
      | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
haftmann@35267
    75
      | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y)
haftmann@35267
    76
      | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x)
wenzelm@24470
    77
      | int t = lit t
wenzelm@24470
    78
    (*abstraction of a natural number expression: no minus*)
haftmann@35267
    79
    fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
haftmann@35267
    80
      | nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
wenzelm@24470
    81
      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
wenzelm@24470
    82
      | nat t = lit t
wenzelm@24470
    83
    (*abstraction of a relation: =, <, <=*)
wenzelm@24470
    84
    fun rel (T, c $ x $ y) =
wenzelm@24470
    85
            if T = HOLogic.realT then c $ (rat x) $ (rat y)
wenzelm@24470
    86
            else if T = HOLogic.intT then c $ (int x) $ (int y)
wenzelm@24470
    87
            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
wenzelm@24470
    88
            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
wenzelm@24470
    89
            else replace (c $ x $ y)   (*non-numeric comparison*)
wenzelm@24470
    90
    (*abstraction of a formula*)
haftmann@38795
    91
    and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
haftmann@38795
    92
      | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
haftmann@38786
    93
      | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
haftmann@38558
    94
      | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
haftmann@38558
    95
      | fm ((c as Const(@{const_name True}, _))) = c
haftmann@38558
    96
      | fm ((c as Const(@{const_name False}, _))) = c
haftmann@38549
    97
      | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
haftmann@35092
    98
      | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
haftmann@35092
    99
      | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
wenzelm@24470
   100
      | fm t = replace t
wenzelm@24470
   101
    (*entry point, and abstraction of a meta-formula*)
haftmann@38558
   102
    fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
wenzelm@24470
   103
      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
wenzelm@24470
   104
      | mt t = fm t  (*it might be a formula*)
wenzelm@24470
   105
  in (list_all (params, mt body), !pairs) end;
wenzelm@24470
   106
wenzelm@24470
   107
wenzelm@24470
   108
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
wenzelm@24470
   109
  abstracted.  Use via compose_tac, which performs no lifting but will
wenzelm@24470
   110
  instantiate variables.*)
wenzelm@24470
   111
wenzelm@28290
   112
val svc_tac = CSUBGOAL (fn (ct, i) =>
wenzelm@24470
   113
  let
wenzelm@28290
   114
    val thy = Thm.theory_of_cterm ct;
wenzelm@28290
   115
    val (abs_goal, _) = svc_abstract (Thm.term_of ct);
wenzelm@28290
   116
    val th = svc_oracle (Thm.cterm_of thy abs_goal);
wenzelm@28290
   117
   in compose_tac (false, th, 0) i end
wenzelm@28290
   118
   handle TERM _ => no_tac);
wenzelm@24470
   119
*}
wenzelm@20813
   120
wenzelm@12869
   121
end