summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sat, 09 Mar 2013 11:56:01 +0100 | |

changeset 51382 | 51957d006677 |

parent 51381 | 4d691437c076 |

child 51383 | 50fb0f35a14f |

discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types

NEWS | file | annotate | diff | comparison | revisions | |

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

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

--- a/NEWS Fri Mar 08 17:19:27 2013 +0100 +++ b/NEWS Sat Mar 09 11:56:01 2013 +0100 @@ -26,6 +26,9 @@ *** HOL *** +* Discontinued theory src/HOL/Library/Eval_Witness. +INCOMPATIBILITY. + * Discontinued obsolete src/HOL/IsaMakefile (considered legacy since Isabelle2013). Use "isabelle build" to operate on Isabelle sessions.

--- a/src/HOL/Library/Eval_Witness.thy Fri Mar 08 17:19:27 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,140 +0,0 @@ -(* Title: HOL/Library/Eval_Witness.thy - Author: Alexander Krauss, TU Muenchen -*) - -header {* Evaluation Oracle with ML witnesses *} - -theory Eval_Witness -imports List Main -begin - -text {* - We provide an oracle method similar to "eval", but with the - possibility to provide ML values as witnesses for existential - statements. - - Our oracle can prove statements of the form @{term "EX x. P x"} - where @{term "P"} is an executable predicate that can be compiled to - ML. The oracle generates code for @{term "P"} and applies - it to a user-specified ML value. If the evaluation - returns true, this is effectively a proof of @{term "EX x. P x"}. - - However, this is only sound if for every ML value of the given type - there exists a corresponding HOL value, which could be used in an - explicit proof. Unfortunately this is not true for function types, - since ML functions are not equivalent to the pure HOL - functions. Thus, the oracle can only be used on first-order - types. - - We define a type class to mark types that can be safely used - with the oracle. -*} - -class ml_equiv - -text {* - Instances of @{text "ml_equiv"} should only be declared for those types, - where the universe of ML values coincides with the HOL values. - - Since this is essentially a statement about ML, there is no - logical characterization. -*} - -instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) -instance bool :: ml_equiv .. -instance list :: (ml_equiv) ml_equiv .. - -ML {* -structure Eval_Method = Proof_Data -( - type T = unit -> bool - (* FIXME avoid user error with non-user text *) - fun init _ () = error "Eval_Method" -) -*} - -oracle eval_witness_oracle = {* fn (cgoal, ws) => -let - val thy = Thm.theory_of_cterm cgoal; - val goal = Thm.term_of cgoal; - fun check_type T = - if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"]) - then T - else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses") - - fun dest_exs 0 t = t - | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = - Abs (v, check_type T, dest_exs (n - 1) b) - | dest_exs _ _ = raise Fail "dest_exs"; - val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); -in - if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws - then Thm.cterm_of thy goal - else @{cprop True} (*dummy*) -end -*} - - -method_setup eval_witness = {* - Scan.lift (Scan.repeat Args.name) >> - (fn ws => K (SIMPLE_METHOD' - (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)))) -*} "evaluation with ML witnesses" - - -subsection {* Toy Examples *} - -text {* - Note that we must use the generated data structure for the - naturals, since ML integers are different. -*} - -(*lemma "\<exists>n::nat. n = 1" -apply (eval_witness "Suc Zero_nat") -done*) - -text {* - Since polymorphism is not allowed, we must specify the - type explicitly: -*} - -lemma "\<exists>l. length (l::bool list) = 3" -apply (eval_witness "[true,true,true]") -done - -text {* Multiple witnesses *} - -lemma "\<exists>k l. length (k::bool list) = length (l::bool list)" -apply (eval_witness "[]" "[]") -done - - -subsection {* Discussion *} - -subsubsection {* Conflicts *} - -text {* - This theory conflicts with EfficientNat, since the @{text ml_equiv} instance - for natural numbers is not valid when they are mapped to ML - integers. With that theory loaded, we could use our oracle to prove - @{term "\<exists>n. n < 0"} by providing @{text "~1"} as a witness. - - This shows that @{text ml_equiv} declarations have to be used with care, - taking the configuration of the code generator into account. -*} - -subsubsection {* Haskell *} - -text {* - If we were able to run generated Haskell code, the situation would - be much nicer, since Haskell functions are pure and could be used as - witnesses for HOL functions: Although Haskell functions are partial, - we know that if the evaluation terminates, they are ``sufficiently - defined'' and could be completed arbitrarily to a total (HOL) function. - - This would allow us to provide access to very efficient data - structures via lookup functions coded in Haskell and provided to HOL - as witnesses. -*} - -end \ No newline at end of file