summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Eval_Witness.thy

author | wenzelm |

Thu Feb 16 22:53:24 2012 +0100 (2012-02-16) | |

changeset 46507 | 1b24c24017dd |

parent 41472 | f6ab14e61604 |

child 47432 | e1576d13e933 |

permissions | -rw-r--r-- |

tuned proofs;

1 (* Title: HOL/Library/Eval_Witness.thy

2 Author: Alexander Krauss, TU Muenchen

3 *)

5 header {* Evaluation Oracle with ML witnesses *}

7 theory Eval_Witness

8 imports List Main

9 begin

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.

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"}.

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.

29 We define a type class to mark types that can be safely used

30 with the oracle.

31 *}

33 class ml_equiv

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.

39 Since this is essentially a statement about ML, there is no

40 logical characterization.

41 *}

43 instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *)

44 instance bool :: ml_equiv ..

45 instance list :: (ml_equiv) ml_equiv ..

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 *}

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")

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 *}

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"

85 subsection {* Toy Examples *}

87 text {*

88 Note that we must use the generated data structure for the

89 naturals, since ML integers are different.

90 *}

92 (*lemma "\<exists>n::nat. n = 1"

93 apply (eval_witness "Suc Zero_nat")

94 done*)

96 text {*

97 Since polymorphism is not allowed, we must specify the

98 type explicitly:

99 *}

101 lemma "\<exists>l. length (l::bool list) = 3"

102 apply (eval_witness "[true,true,true]")

103 done

105 text {* Multiple witnesses *}

107 lemma "\<exists>k l. length (k::bool list) = length (l::bool list)"

108 apply (eval_witness "[]" "[]")

109 done

112 subsection {* Discussion *}

114 subsubsection {* Conflicts *}

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.

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 *}

126 subsubsection {* Haskell *}

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.

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 *}

140 end