Re: [isabelle] Wellsortedness error by using user defined function in quickcheck

Hi Yuhui,

Now I've got a new problem to give a code attribute for the following function.
	"funimage r x = (THE y. (x, y) ∈ r)"

I give a weaker version of code definition, i.e
	(funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))
This is neither weaker nor stronger. Moreover, your code definition is not a proper specification at all - in fact it is unprovable. Otherwise, you would get the following inconsistency

"0 = funimage (set [(0, 0), (0, 1)]) 0 = funimage (set [(0, 1), (0, 0)]) 0 = 1"

because "set [(0, 0), (0, 1)] = set [(0, 1), (0, 0)]". In effect, you try to exploit additional structure of the list when there is no such in the type of sets.

I wonder if there is undefined value for list to represent the invalid case, e.g. return the invalid value when y is not unique. Also I'm trying to giving assumptions for the the code attribute, which is
"x : Domain (set ss) ==>  functional (set ss) ==>  (funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))"
Then I receive a warning "Not a equation".
Code equations must not make assumptions about the parameters. However, you can move the assumptions into a test:

lemma [code]:
  "funimage (set ss) x =
   (if x : Domain (set ss) & functional (set ss)
    then snd (hd (filter (λ (x0, y0). x = x0) ss))
    else funimage (set ss) x)"

This should be provable and the code generator accepts it. If all your use contexts ensure the preconditions themselves, then this equation is perfectly fine. However, if you plan to use quickcheck, you will probably get into non-termination very quickly.

Therefore, it is better to have the else branch raise an exception than to risk non-termination. You can do so as follows:

definition funimage_not_unique :: "(unit => 'a) => 'a"
where [simp]: "funimage_not_unique f = f ()"

code_abort funimage_not_unique

lemma [code]:
  "funimage (set ss) x =
   (if x : Domain (set ss) & functional (set ss)
    then snd (hd (filter (λ (x0, y0). x = x0) ss))
    else funimage_not_unique (%_. funimage (set ss) x))"

code_abort funimage_not_unique
tells the code generator to raise an exeption with message "funimage_not_unique" whenever the generated code executes funimage_not_unique. The constant funimage_not_unique itself is almost the identity, i.e., it does not change the else branch fundamentally. The unit closure ensures termination in strict languages like ML, because it prohibits to evaluate the argument of funimage_not_unique, which would recurse endlessly.

Some examples of this technique can be found in the HOL sources, e.g., in Predicate.thy. In fact, Predicate already provides an executable definite description operator (which has been described in [1]). Hence, the following should also work (not tested!):

  "funimage (set ss) x =
   Predicate.the (pred_of_set (set (filter (λ (x0, y0). x = x0) ss)))"

Hope this helps,

[1] Andreas Lochbihler, Lukas Bulwahn, Animating the Formalised Semantics of a Java-like Language, Marko van Eekelen and Herman Geuvers and Julien Schmalz and Freek Wiedijk (Ed.), Interactive Theorem Proving, pp. 216--232, Springer, 2011.

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.