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