src/HOL/Library/Eval_Witness.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 28054 2b84d34c5d02
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
haftmann@24281
     1
(*  Title:      HOL/Library/Eval_Witness.thy
haftmann@24281
     2
    ID:         $Id$
haftmann@24281
     3
    Author:     Alexander Krauss, TU Muenchen
haftmann@24281
     4
haftmann@24281
     5
*)
haftmann@24281
     6
haftmann@24281
     7
header {* Evaluation Oracle with ML witnesses *}
haftmann@24281
     8
haftmann@24281
     9
theory Eval_Witness
haftmann@27487
    10
imports Plain "~~/src/HOL/List"
haftmann@24281
    11
begin
haftmann@24281
    12
haftmann@24281
    13
text {* 
haftmann@24281
    14
  We provide an oracle method similar to "eval", but with the
haftmann@24281
    15
  possibility to provide ML values as witnesses for existential
haftmann@24281
    16
  statements.
haftmann@24281
    17
haftmann@24281
    18
  Our oracle can prove statements of the form @{term "EX x. P x"}
haftmann@24281
    19
  where @{term "P"} is an executable predicate that can be compiled to
haftmann@24281
    20
  ML. The oracle generates code for @{term "P"} and applies
haftmann@24281
    21
  it to a user-specified ML value. If the evaluation
haftmann@24281
    22
  returns true, this is effectively a proof of  @{term "EX x. P x"}.
haftmann@24281
    23
haftmann@24281
    24
  However, this is only sound if for every ML value of the given type
haftmann@24281
    25
  there exists a corresponding HOL value, which could be used in an
haftmann@24281
    26
  explicit proof. Unfortunately this is not true for function types,
haftmann@24281
    27
  since ML functions are not equivalent to the pure HOL
haftmann@24281
    28
  functions. Thus, the oracle can only be used on first-order
haftmann@24281
    29
  types.
haftmann@24281
    30
haftmann@24281
    31
  We define a type class to mark types that can be safely used
haftmann@24281
    32
  with the oracle.  
haftmann@24281
    33
*}
haftmann@24281
    34
haftmann@24281
    35
class ml_equiv = type
haftmann@24281
    36
haftmann@24281
    37
text {*
haftmann@24281
    38
  Instances of @{text "ml_equiv"} should only be declared for those types,
haftmann@24281
    39
  where the universe of ML values coincides with the HOL values.
haftmann@24281
    40
haftmann@24281
    41
  Since this is essentially a statement about ML, there is no
haftmann@24281
    42
  logical characterization.
haftmann@24281
    43
*}
haftmann@24281
    44
haftmann@24281
    45
instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *)
haftmann@24281
    46
instance bool :: ml_equiv ..
haftmann@24281
    47
instance list :: (ml_equiv) ml_equiv ..
haftmann@24281
    48
haftmann@27103
    49
ML {*
haftmann@27103
    50
structure Eval_Witness_Method =
haftmann@27103
    51
struct
haftmann@27103
    52
haftmann@27103
    53
val eval_ref : (unit -> bool) option ref = ref NONE;
haftmann@27103
    54
haftmann@27103
    55
end;
haftmann@27103
    56
*}
haftmann@27103
    57
haftmann@24281
    58
oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => 
haftmann@24281
    59
let
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@24281
    66
    | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
haftmann@24281
    67
      Abs (v, check_type T, dest_exs (n - 1) b)
haftmann@24281
    68
    | dest_exs _ _ = sys_error "dest_exs";
haftmann@24835
    69
  val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
haftmann@24281
    70
in
haftmann@27103
    71
  if CodeTarget.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
haftmann@24281
    72
  then goal
haftmann@24835
    73
  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
haftmann@24281
    74
end
haftmann@24281
    75
*}
haftmann@24281
    76
haftmann@24281
    77
haftmann@24281
    78
method_setup eval_witness = {*
haftmann@24281
    79
let
haftmann@24281
    80
haftmann@24281
    81
fun eval_tac ws thy = 
haftmann@24281
    82
  SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)
haftmann@24281
    83
haftmann@24281
    84
in 
haftmann@24281
    85
  Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => 
haftmann@24281
    86
    Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt)))
haftmann@24281
    87
end
haftmann@24281
    88
*} "Evaluation with ML witnesses"
haftmann@24281
    89
haftmann@24281
    90
haftmann@24281
    91
subsection {* Toy Examples *}
haftmann@24281
    92
haftmann@24281
    93
text {* 
haftmann@24281
    94
  Note that we must use the generated data structure for the
haftmann@24281
    95
  naturals, since ML integers are different.
haftmann@24281
    96
*}
haftmann@24281
    97
haftmann@26114
    98
(*lemma "\<exists>n::nat. n = 1"
haftmann@26114
    99
apply (eval_witness "Suc Zero_nat")
haftmann@26114
   100
done*)
haftmann@24281
   101
haftmann@24281
   102
text {* 
haftmann@24281
   103
  Since polymorphism is not allowed, we must specify the
haftmann@24281
   104
  type explicitly:
haftmann@24281
   105
*}
haftmann@24281
   106
haftmann@24281
   107
lemma "\<exists>l. length (l::bool list) = 3"
haftmann@24281
   108
apply (eval_witness "[true,true,true]")
haftmann@24281
   109
done
haftmann@24281
   110
haftmann@24281
   111
text {* Multiple witnesses *}
haftmann@24281
   112
haftmann@24281
   113
lemma "\<exists>k l. length (k::bool list) = length (l::bool list)"
haftmann@24281
   114
apply (eval_witness "[]" "[]")
haftmann@24281
   115
done
haftmann@24281
   116
haftmann@24281
   117
haftmann@24281
   118
subsection {* Discussion *}
haftmann@24281
   119
haftmann@24281
   120
subsubsection {* Conflicts *}
haftmann@24281
   121
haftmann@24281
   122
text {* 
haftmann@24281
   123
  This theory conflicts with EfficientNat, since the @{text ml_equiv} instance
haftmann@24281
   124
  for natural numbers is not valid when they are mapped to ML
haftmann@24281
   125
  integers. With that theory loaded, we could use our oracle to prove
haftmann@24281
   126
  @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness.
haftmann@24281
   127
haftmann@24281
   128
  This shows that @{text ml_equiv} declarations have to be used with care,
haftmann@24281
   129
  taking the configuration of the code generator into account.
haftmann@24281
   130
*}
haftmann@24281
   131
haftmann@24281
   132
subsubsection {* Haskell *}
haftmann@24281
   133
haftmann@24281
   134
text {*
haftmann@24281
   135
  If we were able to run generated Haskell code, the situation would
haftmann@24281
   136
  be much nicer, since Haskell functions are pure and could be used as
haftmann@24281
   137
  witnesses for HOL functions: Although Haskell functions are partial,
haftmann@24281
   138
  we know that if the evaluation terminates, they are ``sufficiently
haftmann@24281
   139
  defined'' and could be completed arbitrarily to a total (HOL) function.
haftmann@24281
   140
haftmann@24281
   141
  This would allow us to provide access to very efficient data
haftmann@24281
   142
  structures via lookup functions coded in Haskell and provided to HOL
haftmann@24281
   143
  as witnesses. 
haftmann@24281
   144
*}
haftmann@24281
   145
haftmann@24281
   146
end