src/HOL/Library/Eval_Witness.thy
author wenzelm
Thu, 18 Sep 2008 19:39:44 +0200
changeset 28290 4cc2b6046258
parent 28054 2b84d34c5d02
child 29608 564ea783ace8
permissions -rw-r--r--
simplified oracle interface;
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
27487
c8a6ce181805 absolute imports of HOL/*.thy theories
haftmann
parents: 27368
diff changeset
    10
imports Plain "~~/src/HOL/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
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    49
ML {*
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    50
structure Eval_Witness_Method =
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    51
struct
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    52
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    53
val eval_ref : (unit -> bool) option ref = ref NONE;
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    54
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    55
end;
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    56
*}
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 26939
diff changeset
    57
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    58
oracle eval_witness_oracle = {* fn (cgoal, ws) =>
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    59
let
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    60
  val thy = Thm.theory_of_cterm cgoal;
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    61
  val goal = Thm.term_of cgoal;
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    62
  fun check_type T = 
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    63
    if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    64
    then T
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26114
diff changeset
    65
    else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    66
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    67
  fun dest_exs  0 t = t
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    68
    | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    69
      Abs (v, check_type T, dest_exs (n - 1) b)
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    70
    | dest_exs _ _ = sys_error "dest_exs";
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24281
diff changeset
    71
  val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    72
in
28054
2b84d34c5d02 restructured and split code serializer module
haftmann
parents: 27487
diff changeset
    73
  if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    74
  then Thm.cterm_of thy goal
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    75
  else @{cprop True} (*dummy*)
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    76
end
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    77
*}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    78
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    79
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    80
method_setup eval_witness = {*
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    81
let
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    82
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    83
fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    84
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    85
in
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    86
  Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28054
diff changeset
    87
    Method.SIMPLE_METHOD' (eval_tac ws))
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    88
end
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    89
*} "Evaluation with ML witnesses"
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    90
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    91
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    92
subsection {* Toy Examples *}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    93
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    94
text {* 
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    95
  Note that we must use the generated data structure for the
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    96
  naturals, since ML integers are different.
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    97
*}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
    98
26114
53eb3ff08cce non-operative code antiquotation
haftmann
parents: 25595
diff changeset
    99
(*lemma "\<exists>n::nat. n = 1"
53eb3ff08cce non-operative code antiquotation
haftmann
parents: 25595
diff changeset
   100
apply (eval_witness "Suc Zero_nat")
53eb3ff08cce non-operative code antiquotation
haftmann
parents: 25595
diff changeset
   101
done*)
24281
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   102
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   103
text {* 
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   104
  Since polymorphism is not allowed, we must specify the
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   105
  type explicitly:
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   106
*}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   107
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   108
lemma "\<exists>l. length (l::bool list) = 3"
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   109
apply (eval_witness "[true,true,true]")
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   110
done
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   111
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   112
text {* Multiple witnesses *}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   113
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   114
lemma "\<exists>k l. length (k::bool list) = length (l::bool list)"
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   115
apply (eval_witness "[]" "[]")
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   116
done
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   117
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   118
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   119
subsection {* Discussion *}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   120
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   121
subsubsection {* Conflicts *}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   122
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   123
text {* 
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   124
  This theory conflicts with EfficientNat, since the @{text ml_equiv} instance
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   125
  for natural numbers is not valid when they are mapped to ML
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   126
  integers. With that theory loaded, we could use our oracle to prove
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   127
  @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness.
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   128
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   129
  This shows that @{text ml_equiv} declarations have to be used with care,
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   130
  taking the configuration of the code generator into account.
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   131
*}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   132
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   133
subsubsection {* Haskell *}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   134
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   135
text {*
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   136
  If we were able to run generated Haskell code, the situation would
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   137
  be much nicer, since Haskell functions are pure and could be used as
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   138
  witnesses for HOL functions: Although Haskell functions are partial,
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   139
  we know that if the evaluation terminates, they are ``sufficiently
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   140
  defined'' and could be completed arbitrarily to a total (HOL) function.
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   141
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   142
  This would allow us to provide access to very efficient data
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   143
  structures via lookup functions coded in Haskell and provided to HOL
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   144
  as witnesses. 
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   145
*}
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   146
7d0334b69711 added Eval_Witness theory
haftmann
parents:
diff changeset
   147
end