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