author | haftmann |
Thu, 28 Aug 2008 22:09:20 +0200 | |
changeset 28054 | 2b84d34c5d02 |
parent 27487 | c8a6ce181805 |
child 28290 | 4cc2b6046258 |
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 |
|
27487 | 10 |
imports Plain "~~/src/HOL/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 |
||
27103 | 49 |
ML {* |
50 |
structure Eval_Witness_Method = |
|
51 |
struct |
|
52 |
||
53 |
val eval_ref : (unit -> bool) option ref = ref NONE; |
|
54 |
||
55 |
end; |
|
56 |
*} |
|
57 |
||
24281 | 58 |
oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => |
59 |
let |
|
60 |
fun check_type T = |
|
61 |
if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"]) |
|
62 |
then T |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26114
diff
changeset
|
63 |
else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses") |
24281 | 64 |
|
65 |
fun dest_exs 0 t = t |
|
66 |
| dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = |
|
67 |
Abs (v, check_type T, dest_exs (n - 1) b) |
|
68 |
| dest_exs _ _ = sys_error "dest_exs"; |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24281
diff
changeset
|
69 |
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
24281 | 70 |
in |
28054 | 71 |
if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws |
24281 | 72 |
then goal |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24281
diff
changeset
|
73 |
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*) |
24281 | 74 |
end |
75 |
*} |
|
76 |
||
77 |
||
78 |
method_setup eval_witness = {* |
|
79 |
let |
|
80 |
||
81 |
fun eval_tac ws thy = |
|
82 |
SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i) |
|
83 |
||
84 |
in |
|
85 |
Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => |
|
86 |
Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt))) |
|
87 |
end |
|
88 |
*} "Evaluation with ML witnesses" |
|
89 |
||
90 |
||
91 |
subsection {* Toy Examples *} |
|
92 |
||
93 |
text {* |
|
94 |
Note that we must use the generated data structure for the |
|
95 |
naturals, since ML integers are different. |
|
96 |
*} |
|
97 |
||
26114 | 98 |
(*lemma "\<exists>n::nat. n = 1" |
99 |
apply (eval_witness "Suc Zero_nat") |
|
100 |
done*) |
|
24281 | 101 |
|
102 |
text {* |
|
103 |
Since polymorphism is not allowed, we must specify the |
|
104 |
type explicitly: |
|
105 |
*} |
|
106 |
||
107 |
lemma "\<exists>l. length (l::bool list) = 3" |
|
108 |
apply (eval_witness "[true,true,true]") |
|
109 |
done |
|
110 |
||
111 |
text {* Multiple witnesses *} |
|
112 |
||
113 |
lemma "\<exists>k l. length (k::bool list) = length (l::bool list)" |
|
114 |
apply (eval_witness "[]" "[]") |
|
115 |
done |
|
116 |
||
117 |
||
118 |
subsection {* Discussion *} |
|
119 |
||
120 |
subsubsection {* Conflicts *} |
|
121 |
||
122 |
text {* |
|
123 |
This theory conflicts with EfficientNat, since the @{text ml_equiv} instance |
|
124 |
for natural numbers is not valid when they are mapped to ML |
|
125 |
integers. With that theory loaded, we could use our oracle to prove |
|
126 |
@{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness. |
|
127 |
||
128 |
This shows that @{text ml_equiv} declarations have to be used with care, |
|
129 |
taking the configuration of the code generator into account. |
|
130 |
*} |
|
131 |
||
132 |
subsubsection {* Haskell *} |
|
133 |
||
134 |
text {* |
|
135 |
If we were able to run generated Haskell code, the situation would |
|
136 |
be much nicer, since Haskell functions are pure and could be used as |
|
137 |
witnesses for HOL functions: Although Haskell functions are partial, |
|
138 |
we know that if the evaluation terminates, they are ``sufficiently |
|
139 |
defined'' and could be completed arbitrarily to a total (HOL) function. |
|
140 |
||
141 |
This would allow us to provide access to very efficient data |
|
142 |
structures via lookup functions coded in Haskell and provided to HOL |
|
143 |
as witnesses. |
|
144 |
*} |
|
145 |
||
146 |
end |