--- /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
--- a/src/HOL/Library/Library.thy Wed Aug 15 08:57:39 2007 +0200
+++ b/src/HOL/Library/Library.thy Wed Aug 15 08:57:40 2007 +0200
@@ -12,6 +12,7 @@
Continuity
Efficient_Nat
Eval
+ Eval_Witness
Executable_Rat
Executable_Real
Executable_Set