src/HOL/Library/Eval_Witness.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 41472 f6ab14e61604
child 47432 e1576d13e933
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
haftmann@24281
     1
(*  Title:      HOL/Library/Eval_Witness.thy
haftmann@24281
     2
    Author:     Alexander Krauss, TU Muenchen
haftmann@24281
     3
*)
haftmann@24281
     4
haftmann@24281
     5
header {* Evaluation Oracle with ML witnesses *}
haftmann@24281
     6
haftmann@24281
     7
theory Eval_Witness
haftmann@30663
     8
imports List Main
haftmann@24281
     9
begin
haftmann@24281
    10
haftmann@24281
    11
text {* 
haftmann@24281
    12
  We provide an oracle method similar to "eval", but with the
haftmann@24281
    13
  possibility to provide ML values as witnesses for existential
haftmann@24281
    14
  statements.
haftmann@24281
    15
haftmann@24281
    16
  Our oracle can prove statements of the form @{term "EX x. P x"}
haftmann@24281
    17
  where @{term "P"} is an executable predicate that can be compiled to
haftmann@24281
    18
  ML. The oracle generates code for @{term "P"} and applies
haftmann@24281
    19
  it to a user-specified ML value. If the evaluation
haftmann@24281
    20
  returns true, this is effectively a proof of  @{term "EX x. P x"}.
haftmann@24281
    21
haftmann@24281
    22
  However, this is only sound if for every ML value of the given type
haftmann@24281
    23
  there exists a corresponding HOL value, which could be used in an
haftmann@24281
    24
  explicit proof. Unfortunately this is not true for function types,
haftmann@24281
    25
  since ML functions are not equivalent to the pure HOL
haftmann@24281
    26
  functions. Thus, the oracle can only be used on first-order
haftmann@24281
    27
  types.
haftmann@24281
    28
haftmann@24281
    29
  We define a type class to mark types that can be safely used
haftmann@24281
    30
  with the oracle.  
haftmann@24281
    31
*}
haftmann@24281
    32
haftmann@29608
    33
class ml_equiv
haftmann@24281
    34
haftmann@24281
    35
text {*
haftmann@24281
    36
  Instances of @{text "ml_equiv"} should only be declared for those types,
haftmann@24281
    37
  where the universe of ML values coincides with the HOL values.
haftmann@24281
    38
haftmann@24281
    39
  Since this is essentially a statement about ML, there is no
haftmann@24281
    40
  logical characterization.
haftmann@24281
    41
*}
haftmann@24281
    42
haftmann@24281
    43
instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *)
haftmann@24281
    44
instance bool :: ml_equiv ..
haftmann@24281
    45
instance list :: (ml_equiv) ml_equiv ..
haftmann@24281
    46
haftmann@39471
    47
ML {*
wenzelm@41472
    48
structure Eval_Method = Proof_Data
wenzelm@41472
    49
(
haftmann@39471
    50
  type T = unit -> bool
wenzelm@41472
    51
  (* FIXME avoid user error with non-user text *)
haftmann@39471
    52
  fun init _ () = error "Eval_Method"
haftmann@39471
    53
)
haftmann@39471
    54
*}
haftmann@39471
    55
wenzelm@28290
    56
oracle eval_witness_oracle = {* fn (cgoal, ws) =>
haftmann@24281
    57
let
wenzelm@28290
    58
  val thy = Thm.theory_of_cterm cgoal;
wenzelm@28290
    59
  val goal = Thm.term_of cgoal;
haftmann@24281
    60
  fun check_type T = 
haftmann@24281
    61
    if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
haftmann@24281
    62
    then T
wenzelm@26939
    63
    else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
haftmann@24281
    64
haftmann@24281
    65
  fun dest_exs  0 t = t
haftmann@38558
    66
    | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = 
haftmann@24281
    67
      Abs (v, check_type T, dest_exs (n - 1) b)
wenzelm@40316
    68
    | dest_exs _ _ = raise Fail "dest_exs";
haftmann@24835
    69
  val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
haftmann@24281
    70
in
haftmann@39471
    71
  if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws
wenzelm@28290
    72
  then Thm.cterm_of thy goal
wenzelm@28290
    73
  else @{cprop True} (*dummy*)
haftmann@24281
    74
end
haftmann@24281
    75
*}
haftmann@24281
    76
haftmann@24281
    77
haftmann@24281
    78
method_setup eval_witness = {*
wenzelm@30549
    79
  Scan.lift (Scan.repeat Args.name) >>
wenzelm@30549
    80
  (fn ws => K (SIMPLE_METHOD'
wenzelm@30549
    81
    (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
wenzelm@30549
    82
*} "evaluation with ML witnesses"
haftmann@24281
    83
haftmann@24281
    84
haftmann@24281
    85
subsection {* Toy Examples *}
haftmann@24281
    86
haftmann@24281
    87
text {* 
haftmann@24281
    88
  Note that we must use the generated data structure for the
haftmann@24281
    89
  naturals, since ML integers are different.
haftmann@24281
    90
*}
haftmann@24281
    91
haftmann@26114
    92
(*lemma "\<exists>n::nat. n = 1"
haftmann@26114
    93
apply (eval_witness "Suc Zero_nat")
haftmann@26114
    94
done*)
haftmann@24281
    95
haftmann@24281
    96
text {* 
haftmann@24281
    97
  Since polymorphism is not allowed, we must specify the
haftmann@24281
    98
  type explicitly:
haftmann@24281
    99
*}
haftmann@24281
   100
haftmann@24281
   101
lemma "\<exists>l. length (l::bool list) = 3"
haftmann@24281
   102
apply (eval_witness "[true,true,true]")
haftmann@24281
   103
done
haftmann@24281
   104
haftmann@24281
   105
text {* Multiple witnesses *}
haftmann@24281
   106
haftmann@24281
   107
lemma "\<exists>k l. length (k::bool list) = length (l::bool list)"
haftmann@24281
   108
apply (eval_witness "[]" "[]")
haftmann@24281
   109
done
haftmann@24281
   110
haftmann@24281
   111
haftmann@24281
   112
subsection {* Discussion *}
haftmann@24281
   113
haftmann@24281
   114
subsubsection {* Conflicts *}
haftmann@24281
   115
haftmann@24281
   116
text {* 
haftmann@24281
   117
  This theory conflicts with EfficientNat, since the @{text ml_equiv} instance
haftmann@24281
   118
  for natural numbers is not valid when they are mapped to ML
haftmann@24281
   119
  integers. With that theory loaded, we could use our oracle to prove
haftmann@24281
   120
  @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness.
haftmann@24281
   121
haftmann@24281
   122
  This shows that @{text ml_equiv} declarations have to be used with care,
haftmann@24281
   123
  taking the configuration of the code generator into account.
haftmann@24281
   124
*}
haftmann@24281
   125
haftmann@24281
   126
subsubsection {* Haskell *}
haftmann@24281
   127
haftmann@24281
   128
text {*
haftmann@24281
   129
  If we were able to run generated Haskell code, the situation would
haftmann@24281
   130
  be much nicer, since Haskell functions are pure and could be used as
haftmann@24281
   131
  witnesses for HOL functions: Although Haskell functions are partial,
haftmann@24281
   132
  we know that if the evaluation terminates, they are ``sufficiently
haftmann@24281
   133
  defined'' and could be completed arbitrarily to a total (HOL) function.
haftmann@24281
   134
haftmann@24281
   135
  This would allow us to provide access to very efficient data
haftmann@24281
   136
  structures via lookup functions coded in Haskell and provided to HOL
haftmann@24281
   137
  as witnesses. 
haftmann@24281
   138
*}
haftmann@24281
   139
haftmann@24281
   140
end