summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Wed, 15 Aug 2007 08:57:40 +0200 | |

changeset 24281 | 7d0334b69711 |

parent 24280 | c9867bdf2424 |

child 24282 | 9b64aa297524 |

added Eval_Witness theory

src/HOL/Library/Eval_Witness.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Library.thy | file | annotate | diff | comparison | revisions |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Eval_Witness.thy Wed Aug 15 08:57:40 2007 +0200 @@ -0,0 +1,138 @@ +(* Title: HOL/Library/Eval_Witness.thy + ID: $Id$ + Author: Alexander Krauss, TU Muenchen + +*) + +header {* Evaluation Oracle with ML witnesses *} + +theory Eval_Witness +imports Main +begin + +text {* + We provide an oracle method similar to "eval", but with the + possibility to provide ML values as witnesses for existential + statements. + + Our oracle can prove statements of the form @{term "EX x. P x"} + where @{term "P"} is an executable predicate that can be compiled to + ML. The oracle generates code for @{term "P"} and applies + it to a user-specified ML value. If the evaluation + returns true, this is effectively a proof of @{term "EX x. P x"}. + + However, this is only sound if for every ML value of the given type + there exists a corresponding HOL value, which could be used in an + explicit proof. Unfortunately this is not true for function types, + since ML functions are not equivalent to the pure HOL + functions. Thus, the oracle can only be used on first-order + types. + + We define a type class to mark types that can be safely used + with the oracle. +*} + +class ml_equiv = type + +text {* + Instances of @{text "ml_equiv"} should only be declared for those types, + where the universe of ML values coincides with the HOL values. + + Since this is essentially a statement about ML, there is no + logical characterization. +*} + +instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) +instance bool :: ml_equiv .. +instance list :: (ml_equiv) ml_equiv .. + +oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => +let + fun check_type T = + if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"]) + then T + else error ("Type " ^ quote (Sign.string_of_typ thy T) ^ " not allowed for ML witnesses") + + fun dest_exs 0 t = t + | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = + Abs (v, check_type T, dest_exs (n - 1) b) + | dest_exs _ _ = sys_error "dest_exs"; + + val ct = Thm.cterm_of thy (dest_exs (length ws) (HOLogic.dest_Trueprop goal)) +in + if CodePackage.satisfies thy ct ws + then goal + else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*) +end +*} + + +method_setup eval_witness = {* +let + +fun eval_tac ws thy = + SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i) + +in + Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => + Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt))) +end +*} "Evaluation with ML witnesses" + + +subsection {* Toy Examples *} + +text {* + Note that we must use the generated data structure for the + naturals, since ML integers are different. +*} + +lemma "\<exists>n::nat. n = 1" +apply (eval_witness "Isabelle_Eval.Suc Isabelle_Eval.Zero_nat") +done + +text {* + Since polymorphism is not allowed, we must specify the + type explicitly: +*} + +lemma "\<exists>l. length (l::bool list) = 3" +apply (eval_witness "[true,true,true]") +done + +text {* Multiple witnesses *} + +lemma "\<exists>k l. length (k::bool list) = length (l::bool list)" +apply (eval_witness "[]" "[]") +done + + +subsection {* Discussion *} + +subsubsection {* Conflicts *} + +text {* + This theory conflicts with EfficientNat, since the @{text ml_equiv} instance + for natural numbers is not valid when they are mapped to ML + integers. With that theory loaded, we could use our oracle to prove + @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness. + + This shows that @{text ml_equiv} declarations have to be used with care, + taking the configuration of the code generator into account. +*} + +subsubsection {* Haskell *} + +text {* + If we were able to run generated Haskell code, the situation would + be much nicer, since Haskell functions are pure and could be used as + witnesses for HOL functions: Although Haskell functions are partial, + we know that if the evaluation terminates, they are ``sufficiently + defined'' and could be completed arbitrarily to a total (HOL) function. + + This would allow us to provide access to very efficient data + structures via lookup functions coded in Haskell and provided to HOL + as witnesses. +*} + +end \ No newline at end of file