author | haftmann |
Fri, 22 Feb 2008 16:31:37 +0100 | |
changeset 26114 | 53eb3ff08cce |
parent 25595 | 6c48275f9c76 |
child 26939 | 1035c89b4c02 |
permissions | -rw-r--r-- |
24281 | 1 |
(* Title: HOL/Library/Eval_Witness.thy |
2 |
ID: $Id$ |
|
3 |
Author: Alexander Krauss, TU Muenchen |
|
4 |
||
5 |
*) |
|
6 |
||
7 |
header {* Evaluation Oracle with ML witnesses *} |
|
8 |
||
9 |
theory Eval_Witness |
|
25595 | 10 |
imports List |
24281 | 11 |
begin |
12 |
||
13 |
text {* |
|
14 |
We provide an oracle method similar to "eval", but with the |
|
15 |
possibility to provide ML values as witnesses for existential |
|
16 |
statements. |
|
17 |
||
18 |
Our oracle can prove statements of the form @{term "EX x. P x"} |
|
19 |
where @{term "P"} is an executable predicate that can be compiled to |
|
20 |
ML. The oracle generates code for @{term "P"} and applies |
|
21 |
it to a user-specified ML value. If the evaluation |
|
22 |
returns true, this is effectively a proof of @{term "EX x. P x"}. |
|
23 |
||
24 |
However, this is only sound if for every ML value of the given type |
|
25 |
there exists a corresponding HOL value, which could be used in an |
|
26 |
explicit proof. Unfortunately this is not true for function types, |
|
27 |
since ML functions are not equivalent to the pure HOL |
|
28 |
functions. Thus, the oracle can only be used on first-order |
|
29 |
types. |
|
30 |
||
31 |
We define a type class to mark types that can be safely used |
|
32 |
with the oracle. |
|
33 |
*} |
|
34 |
||
35 |
class ml_equiv = type |
|
36 |
||
37 |
text {* |
|
38 |
Instances of @{text "ml_equiv"} should only be declared for those types, |
|
39 |
where the universe of ML values coincides with the HOL values. |
|
40 |
||
41 |
Since this is essentially a statement about ML, there is no |
|
42 |
logical characterization. |
|
43 |
*} |
|
44 |
||
45 |
instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) |
|
46 |
instance bool :: ml_equiv .. |
|
47 |
instance list :: (ml_equiv) ml_equiv .. |
|
48 |
||
49 |
oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => |
|
50 |
let |
|
51 |
fun check_type T = |
|
52 |
if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"]) |
|
53 |
then T |
|
54 |
else error ("Type " ^ quote (Sign.string_of_typ thy T) ^ " not allowed for ML witnesses") |
|
55 |
||
56 |
fun dest_exs 0 t = t |
|
57 |
| dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = |
|
58 |
Abs (v, check_type T, dest_exs (n - 1) b) |
|
59 |
| dest_exs _ _ = sys_error "dest_exs"; |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24281
diff
changeset
|
60 |
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
24281 | 61 |
in |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24281
diff
changeset
|
62 |
if CodePackage.satisfies thy t ws |
24281 | 63 |
then goal |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24281
diff
changeset
|
64 |
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*) |
24281 | 65 |
end |
66 |
*} |
|
67 |
||
68 |
||
69 |
method_setup eval_witness = {* |
|
70 |
let |
|
71 |
||
72 |
fun eval_tac ws thy = |
|
73 |
SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i) |
|
74 |
||
75 |
in |
|
76 |
Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => |
|
77 |
Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt))) |
|
78 |
end |
|
79 |
*} "Evaluation with ML witnesses" |
|
80 |
||
81 |
||
82 |
subsection {* Toy Examples *} |
|
83 |
||
84 |
text {* |
|
85 |
Note that we must use the generated data structure for the |
|
86 |
naturals, since ML integers are different. |
|
87 |
*} |
|
88 |
||
26114 | 89 |
(*lemma "\<exists>n::nat. n = 1" |
90 |
apply (eval_witness "Suc Zero_nat") |
|
91 |
done*) |
|
24281 | 92 |
|
93 |
text {* |
|
94 |
Since polymorphism is not allowed, we must specify the |
|
95 |
type explicitly: |
|
96 |
*} |
|
97 |
||
98 |
lemma "\<exists>l. length (l::bool list) = 3" |
|
99 |
apply (eval_witness "[true,true,true]") |
|
100 |
done |
|
101 |
||
102 |
text {* Multiple witnesses *} |
|
103 |
||
104 |
lemma "\<exists>k l. length (k::bool list) = length (l::bool list)" |
|
105 |
apply (eval_witness "[]" "[]") |
|
106 |
done |
|
107 |
||
108 |
||
109 |
subsection {* Discussion *} |
|
110 |
||
111 |
subsubsection {* Conflicts *} |
|
112 |
||
113 |
text {* |
|
114 |
This theory conflicts with EfficientNat, since the @{text ml_equiv} instance |
|
115 |
for natural numbers is not valid when they are mapped to ML |
|
116 |
integers. With that theory loaded, we could use our oracle to prove |
|
117 |
@{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness. |
|
118 |
||
119 |
This shows that @{text ml_equiv} declarations have to be used with care, |
|
120 |
taking the configuration of the code generator into account. |
|
121 |
*} |
|
122 |
||
123 |
subsubsection {* Haskell *} |
|
124 |
||
125 |
text {* |
|
126 |
If we were able to run generated Haskell code, the situation would |
|
127 |
be much nicer, since Haskell functions are pure and could be used as |
|
128 |
witnesses for HOL functions: Although Haskell functions are partial, |
|
129 |
we know that if the evaluation terminates, they are ``sufficiently |
|
130 |
defined'' and could be completed arbitrarily to a total (HOL) function. |
|
131 |
||
132 |
This would allow us to provide access to very efficient data |
|
133 |
structures via lookup functions coded in Haskell and provided to HOL |
|
134 |
as witnesses. |
|
135 |
*} |
|
136 |
||
137 |
end |