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