src/HOL/Library/Eval_Witness.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 28054 2b84d34c5d02
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     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 = type
    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 ("term * string list") = {* fn thy => fn (goal, ws) => 
    59 let
    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 ("Ex", _) $ Abs (v,T,b)) = 
    67       Abs (v, check_type T, dest_exs (n - 1) b)
    68     | dest_exs _ _ = sys_error "dest_exs";
    69   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
    70 in
    71   if CodeTarget.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
    72   then goal
    73   else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    74 end
    75 *}
    76 
    77 
    78 method_setup eval_witness = {*
    79 let
    80 
    81 fun eval_tac ws thy = 
    82   SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)
    83 
    84 in 
    85   Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => 
    86     Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt)))
    87 end
    88 *} "Evaluation with ML witnesses"
    89 
    90 
    91 subsection {* Toy Examples *}
    92 
    93 text {* 
    94   Note that we must use the generated data structure for the
    95   naturals, since ML integers are different.
    96 *}
    97 
    98 (*lemma "\<exists>n::nat. n = 1"
    99 apply (eval_witness "Suc Zero_nat")
   100 done*)
   101 
   102 text {* 
   103   Since polymorphism is not allowed, we must specify the
   104   type explicitly:
   105 *}
   106 
   107 lemma "\<exists>l. length (l::bool list) = 3"
   108 apply (eval_witness "[true,true,true]")
   109 done
   110 
   111 text {* Multiple witnesses *}
   112 
   113 lemma "\<exists>k l. length (k::bool list) = length (l::bool list)"
   114 apply (eval_witness "[]" "[]")
   115 done
   116 
   117 
   118 subsection {* Discussion *}
   119 
   120 subsubsection {* Conflicts *}
   121 
   122 text {* 
   123   This theory conflicts with EfficientNat, since the @{text ml_equiv} instance
   124   for natural numbers is not valid when they are mapped to ML
   125   integers. With that theory loaded, we could use our oracle to prove
   126   @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness.
   127 
   128   This shows that @{text ml_equiv} declarations have to be used with care,
   129   taking the configuration of the code generator into account.
   130 *}
   131 
   132 subsubsection {* Haskell *}
   133 
   134 text {*
   135   If we were able to run generated Haskell code, the situation would
   136   be much nicer, since Haskell functions are pure and could be used as
   137   witnesses for HOL functions: Although Haskell functions are partial,
   138   we know that if the evaluation terminates, they are ``sufficiently
   139   defined'' and could be completed arbitrarily to a total (HOL) function.
   140 
   141   This would allow us to provide access to very efficient data
   142   structures via lookup functions coded in Haskell and provided to HOL
   143   as witnesses. 
   144 *}
   145 
   146 end