src/HOL/Library/Eval_Witness.thy

--- /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