src/HOL/Library/Eval_Witness.thy

added verification framework for the HeapMonad and quicksort as example for this framework

(*  Title:      HOL/Library/Eval_Witness.thy
    ID:         $Id$
    Author:     Alexander Krauss, TU Muenchen

*)

header {* Evaluation Oracle with ML witnesses *}

theory Eval_Witness
imports Plain "~~/src/HOL/List"
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 ..

ML {*
structure Eval_Witness_Method =
struct

val eval_ref : (unit -> bool) option ref = ref NONE;

end;
*}

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 (Syntax.string_of_typ_global 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 t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
  if CodeTarget.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t 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 "Suc 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