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