src/HOL/Library/Eval_Witness.thy
author haftmann
Tue Feb 19 19:44:10 2013 +0100 (2013-02-19)
changeset 51188 9b5bf1a9a710
parent 47432 e1576d13e933
permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
     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