[isabelle] Strictness



Hi,

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
composition:

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...

Thanks,

Lutz


-- 
--------------------------------------
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
www.dfki.de/sks/staff/lschrode
--------------------------------------


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

Geschäftsführung:
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.