20817
|
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 Soren 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 = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
|
|
32 |
in vname := Symbol.bump_string (!vname);
|
|
33 |
pairs := (t, v) :: !pairs;
|
|
34 |
v
|
|
35 |
end;
|
|
36 |
fun replace t =
|
|
37 |
case t of
|
|
38 |
Free _ => t (*but not existing Vars, lest the names clash*)
|
|
39 |
| Bound _ => t
|
|
40 |
| _ => (case AList.lookup Pattern.aeconv (!pairs) t of
|
|
41 |
SOME v => v
|
|
42 |
| NONE => insert t)
|
|
43 |
(*abstraction of a numeric literal*)
|
22997
|
44 |
fun lit (t as Const(@{const_name HOL.zero}, _)) = t
|
|
45 |
| lit (t as Const(@{const_name HOL.one}, _)) = t
|
|
46 |
| lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
|
20817
|
47 |
| lit t = replace t
|
|
48 |
(*abstraction of a real/rational expression*)
|
22997
|
49 |
fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
|
|
50 |
| rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
|
|
51 |
| rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
|
|
52 |
| rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
|
|
53 |
| rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
|
20817
|
54 |
| rat t = lit t
|
|
55 |
(*abstraction of an integer expression: no div, mod*)
|
22997
|
56 |
fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
|
|
57 |
| int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
|
|
58 |
| int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
|
|
59 |
| int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
|
20817
|
60 |
| int t = lit t
|
|
61 |
(*abstraction of a natural number expression: no minus*)
|
22997
|
62 |
fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
|
|
63 |
| nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
|
|
64 |
| nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
|
20817
|
65 |
| nat t = lit t
|
|
66 |
(*abstraction of a relation: =, <, <=*)
|
|
67 |
fun rel (T, c $ x $ y) =
|
|
68 |
if T = HOLogic.realT then c $ (rat x) $ (rat y)
|
|
69 |
else if T = HOLogic.intT then c $ (int x) $ (int y)
|
|
70 |
else if T = HOLogic.natT then c $ (nat x) $ (nat y)
|
|
71 |
else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
|
|
72 |
else replace (c $ x $ y) (*non-numeric comparison*)
|
|
73 |
(*abstraction of a formula*)
|
|
74 |
and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
|
|
75 |
| fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
|
|
76 |
| fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
|
|
77 |
| fm ((c as Const("Not", _)) $ p) = c $ (fm p)
|
|
78 |
| fm ((c as Const("True", _))) = c
|
|
79 |
| fm ((c as Const("False", _))) = c
|
|
80 |
| fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
|
22997
|
81 |
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
|
|
82 |
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
|
20817
|
83 |
| fm t = replace t
|
|
84 |
(*entry point, and abstraction of a meta-formula*)
|
|
85 |
fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
|
|
86 |
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
|
|
87 |
| mt t = fm t (*it might be a formula*)
|
|
88 |
in (list_all (params, mt body), !pairs) end;
|
|
89 |
|
|
90 |
|
|
91 |
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
|
|
92 |
abstracted. Use via compose_tac, which performs no lifting but will
|
|
93 |
instantiate variables.*)
|
|
94 |
|
|
95 |
fun svc_tac i st =
|
|
96 |
let
|
|
97 |
val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
|
|
98 |
val th = svc_oracle (Thm.theory_of_thm st) abs_goal
|
|
99 |
in compose_tac (false, th, 0) i st end
|
|
100 |
handle TERM _ => no_tac st;
|
|
101 |
|
|
102 |
|
|
103 |
(*check if user has SVC installed*)
|
|
104 |
fun svc_enabled () = getenv "SVC_HOME" <> "";
|
|
105 |
fun if_svc_enabled f x = if svc_enabled () then f x else ();
|