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

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

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

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 = {* 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")

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

80 method_setup eval_witness = {*

81 let

83 fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)

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"

92 subsection {* Toy Examples *}

94 text {*

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

96 naturals, since ML integers are different.

97 *}

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

100 apply (eval_witness "Suc Zero_nat")

101 done*)

103 text {*

104 Since polymorphism is not allowed, we must specify the

105 type explicitly:

106 *}

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

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

110 done

112 text {* Multiple witnesses *}

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

115 apply (eval_witness "[]" "[]")

116 done

119 subsection {* Discussion *}

121 subsubsection {* Conflicts *}

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.

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

133 subsubsection {* Haskell *}

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.

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

147 end