
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@30549:   (fn ws => K (SIMPLE_METHOD'
wenzelm@30549:     (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 "\<exists>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 "\<exists>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 "\<exists>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 "\<exists>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



