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