src/HOL/SVC_Oracle.ML
changeset 7539 680eca63b98e
parent 7304 94c6f8f07631
child 11707 6c45813c2db1
equal deleted inserted replaced
7538:357873391561 7539:680eca63b98e
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     3     Author:     Lawrence C Paulson
     4     Copyright   1999  University of Cambridge
     4     Copyright   1999  University of Cambridge
     5 
     5 
     6 Installing the oracle for SVC (Stanford Validity Checker)
     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
     7 
    10 
     8 Based upon the work of Søren T. Heilmann
    11 Based upon the work of Søren T. Heilmann
     9 *)
    12 *)
    10 
    13 
    11 
    14 
    12 (*Generalize an Isabelle formula, replacing by Vars
    15 (*Generalize an Isabelle formula, replacing by Vars
    13   all subterms not intelligible to SVC.*)
    16   all subterms not intelligible to SVC.*)
    14 fun svc_abstract t =
    17 fun svc_abstract t =
    15   let
    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.*)
    16     val params = Term.strip_all_vars t
    23     val params = Term.strip_all_vars t
    17     and body   = Term.strip_all_body t
    24     and body   = Term.strip_all_body t
    18     val Us = map #2 params
    25     val Us = map #2 params
    19     val nPar = length params
    26     val nPar = length params
    20     val vname = ref "V_a"
    27     val vname = ref "V_a"
    21     val pairs = ref ([] : (term*term) list)
    28     val pairs = ref ([] : (term*term) list)
    22     fun insert t = 
    29     fun insert t = 
    23 	let val T = fastype_of t
    30 	let val T = fastype_of t
    24 	    val v = Unify.combound (Var ((!vname,0), Us--->T),
    31             val v = Unify.combound (Var ((!vname,0), Us--->T),
    25 				    0, nPar)
    32 				    0, nPar)
    26 	in  vname := bump_string (!vname); 
    33 	in  vname := bump_string (!vname); 
    27 	    pairs := (t, v) :: !pairs;
    34 	    pairs := (t, v) :: !pairs;
    28 	    v
    35 	    v
    29 	end;
    36 	end;
    30     fun replace t = 
    37     fun replace t = 
    31 	case t of
    38 	case t of
    32 	    Free _  => t  (*but not existing Vars, lest the names clash*)
    39 	    Free _  => t  (*but not existing Vars, lest the names clash*)
    33 	  | Bound _ => t
    40 	  | Bound _ => t
    34 	  | _ => (case gen_assoc (op aconv) (!pairs, t) of
    41 	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    35 		      Some v => v
    42 		      Some v => v
    36 		    | None   => insert t)
    43 		    | None   => insert t)
    37     (*abstraction of a real/rational expression*)
    44     (*abstraction of a real/rational expression*)
    38     fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
    45     fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
    39       | 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)
    70       | 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)
    71       | 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)
    72       | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    79       | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    73       | fm ((c as Const("True", _))) = c
    80       | fm ((c as Const("True", _))) = c
    74       | fm ((c as Const("False", _))) = c
    81       | fm ((c as Const("False", _))) = c
    75       | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
    82       | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    76       | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
    83       | fm (t as Const("op <",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    77       | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
    84       | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    78       | fm t = replace t
    85       | fm t = replace t
    79     (*entry point, and abstraction of a meta-formula*)
    86     (*entry point, and abstraction of a meta-formula*)
    80     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    87     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    81       | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    88       | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    82       | mt t = fm t  (*it might be a formula*)
    89       | mt t = fm t  (*it might be a formula*)