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