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--
added Determinants to Library
     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