src/HOL/SVC_Oracle.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7539 680eca63b98e
child 11707 6c45813c2db1
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/SVC_Oracle.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1999  University of Cambridge
     5 
     6 Installing the oracle for SVC (Stanford Validity Checker)
     7 
     8 The following code merely CALLS the oracle; 
     9   the soundness-critical functions are at HOL/Tools/svc_funcs.ML
    10 
    11 Based upon the work of Søren T. Heilmann
    12 *)
    13 
    14 
    15 (*Generalize an Isabelle formula, replacing by Vars
    16   all subterms not intelligible to SVC.*)
    17 fun svc_abstract t =
    18   let
    19     (*The oracle's result is given to the subgoal using compose_tac because
    20       its premises are matched against the assumptions rather than used
    21       to make subgoals.  Therefore , abstraction must copy the parameters
    22       precisely and make them available to all generated Vars.*)
    23     val params = Term.strip_all_vars t
    24     and body   = Term.strip_all_body t
    25     val Us = map #2 params
    26     val nPar = length params
    27     val vname = ref "V_a"
    28     val pairs = ref ([] : (term*term) list)
    29     fun insert t = 
    30 	let val T = fastype_of t
    31             val v = Unify.combound (Var ((!vname,0), Us--->T),
    32 				    0, nPar)
    33 	in  vname := bump_string (!vname); 
    34 	    pairs := (t, v) :: !pairs;
    35 	    v
    36 	end;
    37     fun replace t = 
    38 	case t of
    39 	    Free _  => t  (*but not existing Vars, lest the names clash*)
    40 	  | Bound _ => t
    41 	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    42 		      Some v => v
    43 		    | None   => insert t)
    44     (*abstraction of a real/rational expression*)
    45     fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
    46       | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
    47       | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
    48       | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
    49       | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
    50       | rat ((c as Const("RealDef.0r", _))) = c
    51       | rat ((c as Const("RealDef.1r", _))) = c 
    52       | rat (t as Const("Numeral.number_of", _) $ w) = t
    53       | rat t = replace t
    54     (*abstraction of an integer expression: no div, mod*)
    55     fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
    56       | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
    57       | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
    58       | int ((c as Const("uminus", _)) $ x) = c $ (int x)
    59       | int (t as Const("Numeral.number_of", _) $ w) = t
    60       | int t = replace t
    61     (*abstraction of a natural number expression: no minus*)
    62     fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
    63       | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
    64       | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
    65       | nat (t as Const("0", _)) = t
    66       | nat (t as Const("Numeral.number_of", _) $ w) = t
    67       | nat t = replace t
    68     (*abstraction of a relation: =, <, <=*)
    69     fun rel (T, c $ x $ y) =
    70 	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
    71 	    else if T = HOLogic.intT then c $ (int x) $ (int y)
    72 	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    73 	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    74 	    else replace (c $ x $ y)   (*non-numeric comparison*)
    75     (*abstraction of a formula*)
    76     and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    77       | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    78       | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    79       | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    80       | fm ((c as Const("True", _))) = c
    81       | fm ((c as Const("False", _))) = c
    82       | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    83       | fm (t as Const("op <",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    84       | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    85       | fm t = replace t
    86     (*entry point, and abstraction of a meta-formula*)
    87     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    88       | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    89       | mt t = fm t  (*it might be a formula*)
    90   in (list_all (params, mt body), !pairs) end;
    91 
    92 
    93 (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    94   abstracted.  Use via compose_tac, which performs no lifting but will
    95   instantiate variables.*)
    96 local val svc_thy = the_context () in
    97 
    98 fun svc_tac i st = 
    99   let val prem = BasisLibrary.List.nth (prems_of st, i-1)
   100       val (absPrem, _) = svc_abstract prem
   101       val th = invoke_oracle svc_thy "svc_oracle"
   102 	             (#sign (rep_thm st), Svc.OracleExn absPrem)
   103    in 
   104       compose_tac (false, th, 0) i st
   105    end 
   106    handle Svc.OracleExn _ => Seq.empty
   107 	| Subscript       => Seq.empty;
   108 
   109 end;
   110 
   111 
   112 (*check if user has SVC installed*)
   113 fun svc_enabled () = getenv "SVC_HOME" <> "";
   114 fun if_svc_enabled f x = if svc_enabled () then f x else ();