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