src/HOL/Library/Eval_Witness.thy
author chaieb
Mon Feb 09 17:21:46 2009 +0000 (2009-02-09)
changeset 29847 af32126ee729
parent 29608 564ea783ace8
child 30510 4120fc59dd85
permissions -rw-r--r--
added Determinants to Library
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@29608
    35
class ml_equiv
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
wenzelm@28290
    58
oracle eval_witness_oracle = {* fn (cgoal, ws) =>
haftmann@24281
    59
let
wenzelm@28290
    60
  val thy = Thm.theory_of_cterm cgoal;
wenzelm@28290
    61
  val goal = Thm.term_of cgoal;
haftmann@24281
    62
  fun check_type T = 
haftmann@24281
    63
    if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
haftmann@24281
    64
    then T
wenzelm@26939
    65
    else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
haftmann@24281
    66
haftmann@24281
    67
  fun dest_exs  0 t = t
haftmann@24281
    68
    | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
haftmann@24281
    69
      Abs (v, check_type T, dest_exs (n - 1) b)
haftmann@24281
    70
    | dest_exs _ _ = sys_error "dest_exs";
haftmann@24835
    71
  val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
haftmann@24281
    72
in
haftmann@28054
    73
  if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
wenzelm@28290
    74
  then Thm.cterm_of thy goal
wenzelm@28290
    75
  else @{cprop True} (*dummy*)
haftmann@24281
    76
end
haftmann@24281
    77
*}
haftmann@24281
    78
haftmann@24281
    79
haftmann@24281
    80
method_setup eval_witness = {*
haftmann@24281
    81
let
haftmann@24281
    82
wenzelm@28290
    83
fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
haftmann@24281
    84
wenzelm@28290
    85
in
wenzelm@28290
    86
  Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
wenzelm@28290
    87
    Method.SIMPLE_METHOD' (eval_tac ws))
haftmann@24281
    88
end
haftmann@24281
    89
*} "Evaluation with ML witnesses"
haftmann@24281
    90
haftmann@24281
    91
haftmann@24281
    92
subsection {* Toy Examples *}
haftmann@24281
    93
haftmann@24281
    94
text {* 
haftmann@24281
    95
  Note that we must use the generated data structure for the
haftmann@24281
    96
  naturals, since ML integers are different.
haftmann@24281
    97
*}
haftmann@24281
    98
haftmann@26114
    99
(*lemma "\<exists>n::nat. n = 1"
haftmann@26114
   100
apply (eval_witness "Suc Zero_nat")
haftmann@26114
   101
done*)
haftmann@24281
   102
haftmann@24281
   103
text {* 
haftmann@24281
   104
  Since polymorphism is not allowed, we must specify the
haftmann@24281
   105
  type explicitly:
haftmann@24281
   106
*}
haftmann@24281
   107
haftmann@24281
   108
lemma "\<exists>l. length (l::bool list) = 3"
haftmann@24281
   109
apply (eval_witness "[true,true,true]")
haftmann@24281
   110
done
haftmann@24281
   111
haftmann@24281
   112
text {* Multiple witnesses *}
haftmann@24281
   113
haftmann@24281
   114
lemma "\<exists>k l. length (k::bool list) = length (l::bool list)"
haftmann@24281
   115
apply (eval_witness "[]" "[]")
haftmann@24281
   116
done
haftmann@24281
   117
haftmann@24281
   118
haftmann@24281
   119
subsection {* Discussion *}
haftmann@24281
   120
haftmann@24281
   121
subsubsection {* Conflicts *}
haftmann@24281
   122
haftmann@24281
   123
text {* 
haftmann@24281
   124
  This theory conflicts with EfficientNat, since the @{text ml_equiv} instance
haftmann@24281
   125
  for natural numbers is not valid when they are mapped to ML
haftmann@24281
   126
  integers. With that theory loaded, we could use our oracle to prove
haftmann@24281
   127
  @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness.
haftmann@24281
   128
haftmann@24281
   129
  This shows that @{text ml_equiv} declarations have to be used with care,
haftmann@24281
   130
  taking the configuration of the code generator into account.
haftmann@24281
   131
*}
haftmann@24281
   132
haftmann@24281
   133
subsubsection {* Haskell *}
haftmann@24281
   134
haftmann@24281
   135
text {*
haftmann@24281
   136
  If we were able to run generated Haskell code, the situation would
haftmann@24281
   137
  be much nicer, since Haskell functions are pure and could be used as
haftmann@24281
   138
  witnesses for HOL functions: Although Haskell functions are partial,
haftmann@24281
   139
  we know that if the evaluation terminates, they are ``sufficiently
haftmann@24281
   140
  defined'' and could be completed arbitrarily to a total (HOL) function.
haftmann@24281
   141
haftmann@24281
   142
  This would allow us to provide access to very efficient data
haftmann@24281
   143
  structures via lookup functions coded in Haskell and provided to HOL
haftmann@24281
   144
  as witnesses. 
haftmann@24281
   145
*}
haftmann@24281
   146
haftmann@24281
   147
end