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