20 hide const iff_keep iff_unfold |
20 hide const iff_keep iff_unfold |
21 |
21 |
22 oracle |
22 oracle |
23 svc_oracle ("term") = Svc.oracle |
23 svc_oracle ("term") = Svc.oracle |
24 |
24 |
25 use "svc_oracle.ML" |
25 ML {* |
|
26 (* |
|
27 Installing the oracle for SVC (Stanford Validity Checker) |
|
28 |
|
29 The following code merely CALLS the oracle; |
|
30 the soundness-critical functions are at svc_funcs.ML |
|
31 |
|
32 Based upon the work of Søren T. Heilmann |
|
33 *) |
|
34 |
|
35 |
|
36 (*Generalize an Isabelle formula, replacing by Vars |
|
37 all subterms not intelligible to SVC.*) |
|
38 fun svc_abstract t = |
|
39 let |
|
40 (*The oracle's result is given to the subgoal using compose_tac because |
|
41 its premises are matched against the assumptions rather than used |
|
42 to make subgoals. Therefore , abstraction must copy the parameters |
|
43 precisely and make them available to all generated Vars.*) |
|
44 val params = Term.strip_all_vars t |
|
45 and body = Term.strip_all_body t |
|
46 val Us = map #2 params |
|
47 val nPar = length params |
|
48 val vname = ref "V_a" |
|
49 val pairs = ref ([] : (term*term) list) |
|
50 fun insert t = |
|
51 let val T = fastype_of t |
|
52 val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar) |
|
53 in vname := Symbol.bump_string (!vname); |
|
54 pairs := (t, v) :: !pairs; |
|
55 v |
|
56 end; |
|
57 fun replace t = |
|
58 case t of |
|
59 Free _ => t (*but not existing Vars, lest the names clash*) |
|
60 | Bound _ => t |
|
61 | _ => (case AList.lookup Pattern.aeconv (!pairs) t of |
|
62 SOME v => v |
|
63 | NONE => insert t) |
|
64 (*abstraction of a numeric literal*) |
|
65 fun lit (t as Const(@{const_name HOL.zero}, _)) = t |
|
66 | lit (t as Const(@{const_name HOL.one}, _)) = t |
|
67 | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t |
|
68 | lit t = replace t |
|
69 (*abstraction of a real/rational expression*) |
|
70 fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
|
71 | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
|
72 | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
|
73 | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
|
74 | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x) |
|
75 | rat t = lit t |
|
76 (*abstraction of an integer expression: no div, mod*) |
|
77 fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y) |
|
78 | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y) |
|
79 | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y) |
|
80 | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x) |
|
81 | int t = lit t |
|
82 (*abstraction of a natural number expression: no minus*) |
|
83 fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) |
|
84 | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) |
|
85 | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x) |
|
86 | nat t = lit t |
|
87 (*abstraction of a relation: =, <, <=*) |
|
88 fun rel (T, c $ x $ y) = |
|
89 if T = HOLogic.realT then c $ (rat x) $ (rat y) |
|
90 else if T = HOLogic.intT then c $ (int x) $ (int y) |
|
91 else if T = HOLogic.natT then c $ (nat x) $ (nat y) |
|
92 else if T = HOLogic.boolT then c $ (fm x) $ (fm y) |
|
93 else replace (c $ x $ y) (*non-numeric comparison*) |
|
94 (*abstraction of a formula*) |
|
95 and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q) |
|
96 | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q) |
|
97 | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q) |
|
98 | fm ((c as Const("Not", _)) $ p) = c $ (fm p) |
|
99 | fm ((c as Const("True", _))) = c |
|
100 | fm ((c as Const("False", _))) = c |
|
101 | fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t) |
|
102 | fm (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) |
|
103 | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) |
|
104 | fm t = replace t |
|
105 (*entry point, and abstraction of a meta-formula*) |
|
106 fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p) |
|
107 | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q) |
|
108 | mt t = fm t (*it might be a formula*) |
|
109 in (list_all (params, mt body), !pairs) end; |
|
110 |
|
111 |
|
112 (*Present the entire subgoal to the oracle, assumptions and all, but possibly |
|
113 abstracted. Use via compose_tac, which performs no lifting but will |
|
114 instantiate variables.*) |
|
115 |
|
116 fun svc_tac i st = |
|
117 let |
|
118 val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i) |
|
119 val th = svc_oracle (Thm.theory_of_thm st) abs_goal |
|
120 in compose_tac (false, th, 0) i st end |
|
121 handle TERM _ => no_tac st; |
|
122 |
|
123 |
|
124 (*check if user has SVC installed*) |
|
125 fun svc_enabled () = getenv "SVC_HOME" <> ""; |
|
126 fun if_svc_enabled f x = if svc_enabled () then f x else (); |
|
127 *} |
26 |
128 |
27 end |
129 end |