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