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