src/HOL/ex/SVC_Oracle.thy
changeset 24470 41c81e23c08d
parent 20813 379ce56e5dc2
child 25919 8b1c0d434824
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Aug 29 10:20:22 2007 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Aug 29 11:10:28 2007 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  theory SVC_Oracle
     1.6  imports Main
     1.7 -uses "svc_funcs.ML" ("svc_oracle.ML")
     1.8 +uses "svc_funcs.ML"
     1.9  begin
    1.10  
    1.11  consts
    1.12 @@ -22,6 +22,108 @@
    1.13  oracle
    1.14    svc_oracle ("term") = Svc.oracle
    1.15  
    1.16 -use "svc_oracle.ML"
    1.17 +ML {*
    1.18 +(*
    1.19 +Installing the oracle for SVC (Stanford Validity Checker)
    1.20 +
    1.21 +The following code merely CALLS the oracle;
    1.22 +  the soundness-critical functions are at svc_funcs.ML
    1.23 +
    1.24 +Based upon the work of Søren T. Heilmann
    1.25 +*)
    1.26 +
    1.27 +
    1.28 +(*Generalize an Isabelle formula, replacing by Vars
    1.29 +  all subterms not intelligible to SVC.*)
    1.30 +fun svc_abstract t =
    1.31 +  let
    1.32 +    (*The oracle's result is given to the subgoal using compose_tac because
    1.33 +      its premises are matched against the assumptions rather than used
    1.34 +      to make subgoals.  Therefore , abstraction must copy the parameters
    1.35 +      precisely and make them available to all generated Vars.*)
    1.36 +    val params = Term.strip_all_vars t
    1.37 +    and body   = Term.strip_all_body t
    1.38 +    val Us = map #2 params
    1.39 +    val nPar = length params
    1.40 +    val vname = ref "V_a"
    1.41 +    val pairs = ref ([] : (term*term) list)
    1.42 +    fun insert t =
    1.43 +        let val T = fastype_of t
    1.44 +            val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
    1.45 +        in  vname := Symbol.bump_string (!vname);
    1.46 +            pairs := (t, v) :: !pairs;
    1.47 +            v
    1.48 +        end;
    1.49 +    fun replace t =
    1.50 +        case t of
    1.51 +            Free _  => t  (*but not existing Vars, lest the names clash*)
    1.52 +          | Bound _ => t
    1.53 +          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
    1.54 +                      SOME v => v
    1.55 +                    | NONE   => insert t)
    1.56 +    (*abstraction of a numeric literal*)
    1.57 +    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
    1.58 +      | lit (t as Const(@{const_name HOL.one}, _)) = t
    1.59 +      | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
    1.60 +      | lit t = replace t
    1.61 +    (*abstraction of a real/rational expression*)
    1.62 +    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.63 +      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.64 +      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.65 +      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.66 +      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
    1.67 +      | rat t = lit t
    1.68 +    (*abstraction of an integer expression: no div, mod*)
    1.69 +    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.70 +      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.71 +      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.72 +      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
    1.73 +      | int t = lit t
    1.74 +    (*abstraction of a natural number expression: no minus*)
    1.75 +    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.76 +      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.77 +      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
    1.78 +      | nat t = lit t
    1.79 +    (*abstraction of a relation: =, <, <=*)
    1.80 +    fun rel (T, c $ x $ y) =
    1.81 +            if T = HOLogic.realT then c $ (rat x) $ (rat y)
    1.82 +            else if T = HOLogic.intT then c $ (int x) $ (int y)
    1.83 +            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    1.84 +            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    1.85 +            else replace (c $ x $ y)   (*non-numeric comparison*)
    1.86 +    (*abstraction of a formula*)
    1.87 +    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.88 +      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.89 +      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.90 +      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    1.91 +      | fm ((c as Const("True", _))) = c
    1.92 +      | fm ((c as Const("False", _))) = c
    1.93 +      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.94 +      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.95 +      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.96 +      | fm t = replace t
    1.97 +    (*entry point, and abstraction of a meta-formula*)
    1.98 +    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    1.99 +      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
   1.100 +      | mt t = fm t  (*it might be a formula*)
   1.101 +  in (list_all (params, mt body), !pairs) end;
   1.102 +
   1.103 +
   1.104 +(*Present the entire subgoal to the oracle, assumptions and all, but possibly
   1.105 +  abstracted.  Use via compose_tac, which performs no lifting but will
   1.106 +  instantiate variables.*)
   1.107 +
   1.108 +fun svc_tac i st =
   1.109 +  let
   1.110 +    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
   1.111 +    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
   1.112 +   in compose_tac (false, th, 0) i st end
   1.113 +   handle TERM _ => no_tac st;
   1.114 +
   1.115 +
   1.116 +(*check if user has SVC installed*)
   1.117 +fun svc_enabled () = getenv "SVC_HOME" <> "";
   1.118 +fun if_svc_enabled f x = if svc_enabled () then f x else ();
   1.119 +*}
   1.120  
   1.121  end