author | haftmann |

Wed Aug 15 08:57:40 2007 +0200 (2007-08-15) | |

changeset 24281 | 7d0334b69711 |

parent 24280 | c9867bdf2424 |

child 24282 | 9b64aa297524 |

added Eval_Witness theory

src/HOL/Library/Eval_Witness.thy | file | annotate | diff | revisions | |

src/HOL/Library/Library.thy | file | annotate | diff | revisions |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Library/Eval_Witness.thy Wed Aug 15 08:57:40 2007 +0200 1.3 @@ -0,0 +1,138 @@ 1.4 +(* Title: HOL/Library/Eval_Witness.thy 1.5 + ID: $Id$ 1.6 + Author: Alexander Krauss, TU Muenchen 1.7 + 1.8 +*) 1.9 + 1.10 +header {* Evaluation Oracle with ML witnesses *} 1.11 + 1.12 +theory Eval_Witness 1.13 +imports Main 1.14 +begin 1.15 + 1.16 +text {* 1.17 + We provide an oracle method similar to "eval", but with the 1.18 + possibility to provide ML values as witnesses for existential 1.19 + statements. 1.20 + 1.21 + Our oracle can prove statements of the form @{term "EX x. P x"} 1.22 + where @{term "P"} is an executable predicate that can be compiled to 1.23 + ML. The oracle generates code for @{term "P"} and applies 1.24 + it to a user-specified ML value. If the evaluation 1.25 + returns true, this is effectively a proof of @{term "EX x. P x"}. 1.26 + 1.27 + However, this is only sound if for every ML value of the given type 1.28 + there exists a corresponding HOL value, which could be used in an 1.29 + explicit proof. Unfortunately this is not true for function types, 1.30 + since ML functions are not equivalent to the pure HOL 1.31 + functions. Thus, the oracle can only be used on first-order 1.32 + types. 1.33 + 1.34 + We define a type class to mark types that can be safely used 1.35 + with the oracle. 1.36 +*} 1.37 + 1.38 +class ml_equiv = type 1.39 + 1.40 +text {* 1.41 + Instances of @{text "ml_equiv"} should only be declared for those types, 1.42 + where the universe of ML values coincides with the HOL values. 1.43 + 1.44 + Since this is essentially a statement about ML, there is no 1.45 + logical characterization. 1.46 +*} 1.47 + 1.48 +instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) 1.49 +instance bool :: ml_equiv .. 1.50 +instance list :: (ml_equiv) ml_equiv .. 1.51 + 1.52 +oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => 1.53 +let 1.54 + fun check_type T = 1.55 + if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"]) 1.56 + then T 1.57 + else error ("Type " ^ quote (Sign.string_of_typ thy T) ^ " not allowed for ML witnesses") 1.58 + 1.59 + fun dest_exs 0 t = t 1.60 + | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 1.61 + Abs (v, check_type T, dest_exs (n - 1) b) 1.62 + | dest_exs _ _ = sys_error "dest_exs"; 1.63 + 1.64 + val ct = Thm.cterm_of thy (dest_exs (length ws) (HOLogic.dest_Trueprop goal)) 1.65 +in 1.66 + if CodePackage.satisfies thy ct ws 1.67 + then goal 1.68 + else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*) 1.69 +end 1.70 +*} 1.71 + 1.72 + 1.73 +method_setup eval_witness = {* 1.74 +let 1.75 + 1.76 +fun eval_tac ws thy = 1.77 + SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i) 1.78 + 1.79 +in 1.80 + Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => 1.81 + Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt))) 1.82 +end 1.83 +*} "Evaluation with ML witnesses" 1.84 + 1.85 + 1.86 +subsection {* Toy Examples *} 1.87 + 1.88 +text {* 1.89 + Note that we must use the generated data structure for the 1.90 + naturals, since ML integers are different. 1.91 +*} 1.92 + 1.93 +lemma "\<exists>n::nat. n = 1" 1.94 +apply (eval_witness "Isabelle_Eval.Suc Isabelle_Eval.Zero_nat") 1.95 +done 1.96 + 1.97 +text {* 1.98 + Since polymorphism is not allowed, we must specify the 1.99 + type explicitly: 1.100 +*} 1.101 + 1.102 +lemma "\<exists>l. length (l::bool list) = 3" 1.103 +apply (eval_witness "[true,true,true]") 1.104 +done 1.105 + 1.106 +text {* Multiple witnesses *} 1.107 + 1.108 +lemma "\<exists>k l. length (k::bool list) = length (l::bool list)" 1.109 +apply (eval_witness "[]" "[]") 1.110 +done 1.111 + 1.112 + 1.113 +subsection {* Discussion *} 1.114 + 1.115 +subsubsection {* Conflicts *} 1.116 + 1.117 +text {* 1.118 + This theory conflicts with EfficientNat, since the @{text ml_equiv} instance 1.119 + for natural numbers is not valid when they are mapped to ML 1.120 + integers. With that theory loaded, we could use our oracle to prove 1.121 + @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness. 1.122 + 1.123 + This shows that @{text ml_equiv} declarations have to be used with care, 1.124 + taking the configuration of the code generator into account. 1.125 +*} 1.126 + 1.127 +subsubsection {* Haskell *} 1.128 + 1.129 +text {* 1.130 + If we were able to run generated Haskell code, the situation would 1.131 + be much nicer, since Haskell functions are pure and could be used as 1.132 + witnesses for HOL functions: Although Haskell functions are partial, 1.133 + we know that if the evaluation terminates, they are ``sufficiently 1.134 + defined'' and could be completed arbitrarily to a total (HOL) function. 1.135 + 1.136 + This would allow us to provide access to very efficient data 1.137 + structures via lookup functions coded in Haskell and provided to HOL 1.138 + as witnesses. 1.139 +*} 1.140 + 1.141 +end 1.142 \ No newline at end of file

2.1 --- a/src/HOL/Library/Library.thy Wed Aug 15 08:57:39 2007 +0200 2.2 +++ b/src/HOL/Library/Library.thy Wed Aug 15 08:57:40 2007 +0200 2.3 @@ -12,6 +12,7 @@ 2.4 Continuity 2.5 Efficient_Nat 2.6 Eval 2.7 + Eval_Witness 2.8 Executable_Rat 2.9 Executable_Real 2.10 Executable_Set