added Eval_Witness theory
authorhaftmann
Wed Aug 15 08:57:40 2007 +0200 (2007-08-15)
changeset 242817d0334b69711
parent 24280 c9867bdf2424
child 24282 9b64aa297524
added Eval_Witness theory
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Library.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Eval_Witness.thy	Wed Aug 15 08:57:40 2007 +0200
     1.3 @@ -0,0 +1,138 @@
     1.4 +(*  Title:      HOL/Library/Eval_Witness.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Alexander Krauss, TU Muenchen
     1.7 +
     1.8 +*)
     1.9 +
    1.10 +header {* Evaluation Oracle with ML witnesses *}
    1.11 +
    1.12 +theory Eval_Witness
    1.13 +imports Main
    1.14 +begin
    1.15 +
    1.16 +text {* 
    1.17 +  We provide an oracle method similar to "eval", but with the
    1.18 +  possibility to provide ML values as witnesses for existential
    1.19 +  statements.
    1.20 +
    1.21 +  Our oracle can prove statements of the form @{term "EX x. P x"}
    1.22 +  where @{term "P"} is an executable predicate that can be compiled to
    1.23 +  ML. The oracle generates code for @{term "P"} and applies
    1.24 +  it to a user-specified ML value. If the evaluation
    1.25 +  returns true, this is effectively a proof of  @{term "EX x. P x"}.
    1.26 +
    1.27 +  However, this is only sound if for every ML value of the given type
    1.28 +  there exists a corresponding HOL value, which could be used in an
    1.29 +  explicit proof. Unfortunately this is not true for function types,
    1.30 +  since ML functions are not equivalent to the pure HOL
    1.31 +  functions. Thus, the oracle can only be used on first-order
    1.32 +  types.
    1.33 +
    1.34 +  We define a type class to mark types that can be safely used
    1.35 +  with the oracle.  
    1.36 +*}
    1.37 +
    1.38 +class ml_equiv = type
    1.39 +
    1.40 +text {*
    1.41 +  Instances of @{text "ml_equiv"} should only be declared for those types,
    1.42 +  where the universe of ML values coincides with the HOL values.
    1.43 +
    1.44 +  Since this is essentially a statement about ML, there is no
    1.45 +  logical characterization.
    1.46 +*}
    1.47 +
    1.48 +instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *)
    1.49 +instance bool :: ml_equiv ..
    1.50 +instance list :: (ml_equiv) ml_equiv ..
    1.51 +
    1.52 +oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => 
    1.53 +let
    1.54 +  fun check_type T = 
    1.55 +    if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
    1.56 +    then T
    1.57 +    else error ("Type " ^ quote (Sign.string_of_typ thy T) ^ " not allowed for ML witnesses")
    1.58 +
    1.59 +  fun dest_exs  0 t = t
    1.60 +    | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
    1.61 +      Abs (v, check_type T, dest_exs (n - 1) b)
    1.62 +    | dest_exs _ _ = sys_error "dest_exs";
    1.63 +
    1.64 +  val ct = Thm.cterm_of thy (dest_exs (length ws) (HOLogic.dest_Trueprop goal))
    1.65 +in
    1.66 +  if CodePackage.satisfies thy ct ws
    1.67 +  then goal
    1.68 +  else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
    1.69 +end
    1.70 +*}
    1.71 +
    1.72 +
    1.73 +method_setup eval_witness = {*
    1.74 +let
    1.75 +
    1.76 +fun eval_tac ws thy = 
    1.77 +  SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)
    1.78 +
    1.79 +in 
    1.80 +  Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => 
    1.81 +    Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt)))
    1.82 +end
    1.83 +*} "Evaluation with ML witnesses"
    1.84 +
    1.85 +
    1.86 +subsection {* Toy Examples *}
    1.87 +
    1.88 +text {* 
    1.89 +  Note that we must use the generated data structure for the
    1.90 +  naturals, since ML integers are different.
    1.91 +*}
    1.92 +
    1.93 +lemma "\<exists>n::nat. n = 1"
    1.94 +apply (eval_witness "Isabelle_Eval.Suc Isabelle_Eval.Zero_nat")
    1.95 +done
    1.96 +
    1.97 +text {* 
    1.98 +  Since polymorphism is not allowed, we must specify the
    1.99 +  type explicitly:
   1.100 +*}
   1.101 +
   1.102 +lemma "\<exists>l. length (l::bool list) = 3"
   1.103 +apply (eval_witness "[true,true,true]")
   1.104 +done
   1.105 +
   1.106 +text {* Multiple witnesses *}
   1.107 +
   1.108 +lemma "\<exists>k l. length (k::bool list) = length (l::bool list)"
   1.109 +apply (eval_witness "[]" "[]")
   1.110 +done
   1.111 +
   1.112 +
   1.113 +subsection {* Discussion *}
   1.114 +
   1.115 +subsubsection {* Conflicts *}
   1.116 +
   1.117 +text {* 
   1.118 +  This theory conflicts with EfficientNat, since the @{text ml_equiv} instance
   1.119 +  for natural numbers is not valid when they are mapped to ML
   1.120 +  integers. With that theory loaded, we could use our oracle to prove
   1.121 +  @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness.
   1.122 +
   1.123 +  This shows that @{text ml_equiv} declarations have to be used with care,
   1.124 +  taking the configuration of the code generator into account.
   1.125 +*}
   1.126 +
   1.127 +subsubsection {* Haskell *}
   1.128 +
   1.129 +text {*
   1.130 +  If we were able to run generated Haskell code, the situation would
   1.131 +  be much nicer, since Haskell functions are pure and could be used as
   1.132 +  witnesses for HOL functions: Although Haskell functions are partial,
   1.133 +  we know that if the evaluation terminates, they are ``sufficiently
   1.134 +  defined'' and could be completed arbitrarily to a total (HOL) function.
   1.135 +
   1.136 +  This would allow us to provide access to very efficient data
   1.137 +  structures via lookup functions coded in Haskell and provided to HOL
   1.138 +  as witnesses. 
   1.139 +*}
   1.140 +
   1.141 +end
   1.142 \ No newline at end of file
     2.1 --- a/src/HOL/Library/Library.thy	Wed Aug 15 08:57:39 2007 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Wed Aug 15 08:57:40 2007 +0200
     2.3 @@ -12,6 +12,7 @@
     2.4    Continuity
     2.5    Efficient_Nat
     2.6    Eval
     2.7 +  Eval_Witness
     2.8    Executable_Rat
     2.9    Executable_Real
    2.10    Executable_Set