[isabelle] Strictness


I am presently using the function package in a course; specifically, I
am letting the students prove the rules of a Hoare calculus for partial
correctness over a simple imperative language. The recursive definition
of the semantics is, of course, a partial function, with clauses such as

"Sem (c1 ;;; c2) s = Sem c2 (Sem c1 s)"

where ;;; is sequential composition. Now from a clause such as the above
one would wish to conclude a strictness lemma, in the case of sequential

lemma seq_dom: "Sem_dom (c1;;;c2, s) ==>  Sem_dom (c1, s) &
Sem_dom (c2, Sem c1 s)"

Indeed this can be proved, but the only way I found is somewhat
involved: as indicated in the tutorial for the function package, one can
use the fact that Sem_dom is accp Sem_rel, and apply accp_downward in
connection with Sem_rel.intros. However, one then runs across a somewhat
hidden feature: Sem_rel.intros mentions Sem_sumC, not Sem, and one needs
to unfold the definition of Sem in terms of Sem_sumC to make things work
as expected.

Am I overlooking something? One sort of suspects that strictness
assertions such as the above might be available neatly packaged, say as
"Sem.strictness" or so...



PD Dr. Lutz Schröder
Senior Researcher
DFKI Bremen	
Safe and Secure Cognitive Systems
Cartesium, Enrique-Schmidt-Str. 5
D-28359 Bremen

phone: (+49) 421-218-64216
Fax:   (+49) 421-218-9864216
mail: Lutz.Schroeder at dfki.de

Deutsches Forschungszentrum für Künstliche Intelligenz GmbH
Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern

Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313

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