haftmann@24281: (* Title: HOL/Library/Eval_Witness.thy haftmann@24281: Author: Alexander Krauss, TU Muenchen haftmann@24281: *) haftmann@24281: haftmann@24281: header {* Evaluation Oracle with ML witnesses *} haftmann@24281: haftmann@24281: theory Eval_Witness haftmann@30663: imports List Main haftmann@24281: begin haftmann@24281: haftmann@24281: text {* haftmann@24281: We provide an oracle method similar to "eval", but with the haftmann@24281: possibility to provide ML values as witnesses for existential haftmann@24281: statements. haftmann@24281: haftmann@24281: Our oracle can prove statements of the form @{term "EX x. P x"} haftmann@24281: where @{term "P"} is an executable predicate that can be compiled to haftmann@24281: ML. The oracle generates code for @{term "P"} and applies haftmann@24281: it to a user-specified ML value. If the evaluation haftmann@24281: returns true, this is effectively a proof of @{term "EX x. P x"}. haftmann@24281: haftmann@24281: However, this is only sound if for every ML value of the given type haftmann@24281: there exists a corresponding HOL value, which could be used in an haftmann@24281: explicit proof. Unfortunately this is not true for function types, haftmann@24281: since ML functions are not equivalent to the pure HOL haftmann@24281: functions. Thus, the oracle can only be used on first-order haftmann@24281: types. haftmann@24281: haftmann@24281: We define a type class to mark types that can be safely used haftmann@24281: with the oracle. haftmann@24281: *} haftmann@24281: haftmann@29608: class ml_equiv haftmann@24281: haftmann@24281: text {* haftmann@24281: Instances of @{text "ml_equiv"} should only be declared for those types, haftmann@24281: where the universe of ML values coincides with the HOL values. haftmann@24281: haftmann@24281: Since this is essentially a statement about ML, there is no haftmann@24281: logical characterization. haftmann@24281: *} haftmann@24281: haftmann@24281: instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) haftmann@24281: instance bool :: ml_equiv .. haftmann@24281: instance list :: (ml_equiv) ml_equiv .. haftmann@24281: haftmann@39471: ML {* wenzelm@41472: structure Eval_Method = Proof_Data wenzelm@41472: ( haftmann@39471: type T = unit -> bool wenzelm@41472: (* FIXME avoid user error with non-user text *) haftmann@39471: fun init _ () = error "Eval_Method" haftmann@39471: ) haftmann@39471: *} haftmann@39471: wenzelm@28290: oracle eval_witness_oracle = {* fn (cgoal, ws) => haftmann@24281: let wenzelm@28290: val thy = Thm.theory_of_cterm cgoal; wenzelm@28290: val goal = Thm.term_of cgoal; haftmann@24281: fun check_type T = haftmann@24281: if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"]) haftmann@24281: then T wenzelm@26939: else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses") haftmann@24281: haftmann@24281: fun dest_exs 0 t = t haftmann@38558: | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = haftmann@24281: Abs (v, check_type T, dest_exs (n - 1) b) wenzelm@40316: | dest_exs _ _ = raise Fail "dest_exs"; haftmann@24835: val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); haftmann@24281: in haftmann@39471: if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws wenzelm@28290: then Thm.cterm_of thy goal wenzelm@28290: else @{cprop True} (*dummy*) haftmann@24281: end haftmann@24281: *} haftmann@24281: haftmann@24281: haftmann@24281: method_setup eval_witness = {* wenzelm@30549: Scan.lift (Scan.repeat Args.name) >> wenzelm@47432: (fn ws => K (SIMPLE_METHOD' wenzelm@47432: (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)))) wenzelm@30549: *} "evaluation with ML witnesses" haftmann@24281: haftmann@24281: haftmann@24281: subsection {* Toy Examples *} haftmann@24281: haftmann@24281: text {* haftmann@24281: Note that we must use the generated data structure for the haftmann@24281: naturals, since ML integers are different. haftmann@24281: *} haftmann@24281: haftmann@26114: (*lemma "\n::nat. n = 1" haftmann@26114: apply (eval_witness "Suc Zero_nat") haftmann@26114: done*) haftmann@24281: haftmann@24281: text {* haftmann@24281: Since polymorphism is not allowed, we must specify the haftmann@24281: type explicitly: haftmann@24281: *} haftmann@24281: haftmann@24281: lemma "\l. length (l::bool list) = 3" haftmann@24281: apply (eval_witness "[true,true,true]") haftmann@24281: done haftmann@24281: haftmann@24281: text {* Multiple witnesses *} haftmann@24281: haftmann@24281: lemma "\k l. length (k::bool list) = length (l::bool list)" haftmann@24281: apply (eval_witness "[]" "[]") haftmann@24281: done haftmann@24281: haftmann@24281: haftmann@24281: subsection {* Discussion *} haftmann@24281: haftmann@24281: subsubsection {* Conflicts *} haftmann@24281: haftmann@24281: text {* haftmann@24281: This theory conflicts with EfficientNat, since the @{text ml_equiv} instance haftmann@24281: for natural numbers is not valid when they are mapped to ML haftmann@24281: integers. With that theory loaded, we could use our oracle to prove haftmann@24281: @{term "\n. n < 0"} by providing @{text "~1"} as a witness. haftmann@24281: haftmann@24281: This shows that @{text ml_equiv} declarations have to be used with care, haftmann@24281: taking the configuration of the code generator into account. haftmann@24281: *} haftmann@24281: haftmann@24281: subsubsection {* Haskell *} haftmann@24281: haftmann@24281: text {* haftmann@24281: If we were able to run generated Haskell code, the situation would haftmann@24281: be much nicer, since Haskell functions are pure and could be used as haftmann@24281: witnesses for HOL functions: Although Haskell functions are partial, haftmann@24281: we know that if the evaluation terminates, they are ``sufficiently haftmann@24281: defined'' and could be completed arbitrarily to a total (HOL) function. haftmann@24281: haftmann@24281: This would allow us to provide access to very efficient data haftmann@24281: structures via lookup functions coded in Haskell and provided to HOL haftmann@24281: as witnesses. haftmann@24281: *} haftmann@24281: haftmann@24281: end