author sandnerr
Fri, 13 Dec 1996 12:01:26 +0100
changeset 2380 90280b3a538b
parent 2379 2e55b396e24c
child 10835 f4745d77e620
permissions -rw-r--r--
Dummy change to document the change in revision 1.5: Parent theory changed to HOLCF.thy (former Tr2.thy) . Was necessary because the use of HOLCF_ss in Hoare.ML, which has been extended by the introduction of the Lift theories.

(*  Title:      HOLCF/ex/hoare.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Theory for an example by C.A.R. Hoare 

p x = if b1 x 
         then p (g x)
         else x fi

q x = if b1 x orelse b2 x 
         then q (g x)
         else x fi

Prove: for all b1 b2 g . 
            q o p  = q 

In order to get a nice notation we fix the functions b1,b2 and g in the
signature of this example


Hoare = HOLCF + 

        b1:: "'a -> tr"
        b2:: "'a -> tr"
         g:: "'a -> 'a"
        p :: "'a -> 'a"
        q :: "'a -> 'a"


  p_def  "p == fix`(LAM f. LAM x.
                 If b1`x then f`(g`x) else x fi)"

  q_def  "q == fix`(LAM f. LAM x.
                 If b1`x orelse b2`x then f`(g`x) else x fi)"