author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 52131 | 366fa32ee2a3 |
child 56245 | 84fc7dfa3cd4 |
permissions | -rw-r--r-- |
12869 | 1 |
(* Title: HOL/ex/SVC_Oracle.thy |
2 |
Author: Lawrence C Paulson |
|
3 |
Copyright 1999 University of Cambridge |
|
4 |
||
40945 | 5 |
Based upon the work of Søren T. Heilmann. |
17388 | 6 |
*) |
12869 | 7 |
|
17388 | 8 |
header {* Installing an oracle for SVC (Stanford Validity Checker) *} |
12869 | 9 |
|
16836 | 10 |
theory SVC_Oracle |
11 |
imports Main |
|
12 |
begin |
|
12869 | 13 |
|
48891 | 14 |
ML_file "svc_funcs.ML" |
15 |
||
12869 | 16 |
consts |
17 |
iff_keep :: "[bool, bool] => bool" |
|
18 |
iff_unfold :: "[bool, bool] => bool" |
|
19 |
||
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35267
diff
changeset
|
20 |
hide_const iff_keep iff_unfold |
16836 | 21 |
|
28290 | 22 |
oracle svc_oracle = Svc.oracle |
12869 | 23 |
|
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
24 |
ML {* |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
25 |
(* |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
26 |
Installing the oracle for SVC (Stanford Validity Checker) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
27 |
|
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
28 |
The following code merely CALLS the oracle; |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
29 |
the soundness-critical functions are at svc_funcs.ML |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
30 |
|
40945 | 31 |
Based upon the work of Søren T. Heilmann |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
32 |
*) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
33 |
|
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
34 |
|
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
35 |
(*Generalize an Isabelle formula, replacing by Vars |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
36 |
all subterms not intelligible to SVC.*) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
37 |
fun svc_abstract t = |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
38 |
let |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
39 |
(*The oracle's result is given to the subgoal using compose_tac because |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
40 |
its premises are matched against the assumptions rather than used |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
41 |
to make subgoals. Therefore , abstraction must copy the parameters |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
42 |
precisely and make them available to all generated Vars.*) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
43 |
val params = Term.strip_all_vars t |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
44 |
and body = Term.strip_all_body t |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
45 |
val Us = map #2 params |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
46 |
val nPar = length params |
32740 | 47 |
val vname = Unsynchronized.ref "V_a" |
48 |
val pairs = Unsynchronized.ref ([] : (term*term) list) |
|
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
49 |
fun insert t = |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
50 |
let val T = fastype_of t |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
51 |
val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
52 |
in vname := Symbol.bump_string (!vname); |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
53 |
pairs := (t, v) :: !pairs; |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
54 |
v |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
55 |
end; |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
56 |
fun replace t = |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
57 |
case t of |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
58 |
Free _ => t (*but not existing Vars, lest the names clash*) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
59 |
| Bound _ => t |
52131 | 60 |
| _ => (case AList.lookup Envir.aeconv (!pairs) t of |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
61 |
SOME v => v |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
62 |
| NONE => insert t) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
63 |
(*abstraction of a numeric literal*) |
25929
6bfef23e26be
avoiding direct references to numeral presentation
haftmann
parents:
25919
diff
changeset
|
64 |
fun lit t = if can HOLogic.dest_number t then t else replace t; |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
65 |
(*abstraction of a real/rational expression*) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
66 |
fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
67 |
| rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
41460
diff
changeset
|
68 |
| rat ((c as Const(@{const_name Fields.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
69 |
| rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
70 |
| rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x) |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
71 |
| rat t = lit t |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
72 |
(*abstraction of an integer expression: no div, mod*) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
73 |
fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
74 |
| int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
75 |
| int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
76 |
| int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x) |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
77 |
| int t = lit t |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
78 |
(*abstraction of a natural number expression: no minus*) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
79 |
fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
80 |
| nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
81 |
| nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
82 |
| nat t = lit t |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
83 |
(*abstraction of a relation: =, <, <=*) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
84 |
fun rel (T, c $ x $ y) = |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
85 |
if T = HOLogic.realT then c $ (rat x) $ (rat y) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
86 |
else if T = HOLogic.intT then c $ (int x) $ (int y) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
87 |
else if T = HOLogic.natT then c $ (nat x) $ (nat y) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
88 |
else if T = HOLogic.boolT then c $ (fm x) $ (fm y) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
89 |
else replace (c $ x $ y) (*non-numeric comparison*) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
90 |
(*abstraction of a formula*) |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
91 |
and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q) |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
92 |
| fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q) |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38558
diff
changeset
|
93 |
| fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q) |
38558 | 94 |
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p) |
95 |
| fm ((c as Const(@{const_name True}, _))) = c |
|
96 |
| fm ((c as Const(@{const_name False}, _))) = c |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
97 |
| fm (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset
|
98 |
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) |
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset
|
99 |
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
100 |
| fm t = replace t |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
101 |
(*entry point, and abstraction of a meta-formula*) |
38558 | 102 |
fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p) |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
103 |
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
104 |
| mt t = fm t (*it might be a formula*) |
46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
44064
diff
changeset
|
105 |
in (Logic.list_all (params, mt body), !pairs) end; |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
106 |
|
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
107 |
|
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
108 |
(*Present the entire subgoal to the oracle, assumptions and all, but possibly |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
109 |
abstracted. Use via compose_tac, which performs no lifting but will |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
110 |
instantiate variables.*) |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
111 |
|
28290 | 112 |
val svc_tac = CSUBGOAL (fn (ct, i) => |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
113 |
let |
28290 | 114 |
val thy = Thm.theory_of_cterm ct; |
115 |
val (abs_goal, _) = svc_abstract (Thm.term_of ct); |
|
116 |
val th = svc_oracle (Thm.cterm_of thy abs_goal); |
|
117 |
in compose_tac (false, th, 0) i end |
|
118 |
handle TERM _ => no_tac); |
|
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
20813
diff
changeset
|
119 |
*} |
20813 | 120 |
|
12869 | 121 |
end |