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

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

5 *)

7 header {* Evaluation Oracle with ML witnesses *}

9 theory Eval_Witness

10 imports Plain "~~/src/HOL/List"

11 begin

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.

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

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.

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

32 with the oracle.

33 *}

35 class ml_equiv = type

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.

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

42 logical characterization.

43 *}

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

46 instance bool :: ml_equiv ..

47 instance list :: (ml_equiv) ml_equiv ..

49 ML {*

50 structure Eval_Witness_Method =

51 struct

53 val eval_ref : (unit -> bool) option ref = ref NONE;

55 end;

56 *}

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

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

78 method_setup eval_witness = {*

79 let

81 fun eval_tac ws thy =

82 SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)

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"

91 subsection {* Toy Examples *}

93 text {*

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

95 naturals, since ML integers are different.

96 *}

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

99 apply (eval_witness "Suc Zero_nat")

100 done*)

102 text {*

103 Since polymorphism is not allowed, we must specify the

104 type explicitly:

105 *}

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

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

109 done

111 text {* Multiple witnesses *}

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

114 apply (eval_witness "[]" "[]")

115 done

118 subsection {* Discussion *}

120 subsubsection {* Conflicts *}

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.

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

132 subsubsection {* Haskell *}

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.

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

146 end