src/HOLCF/ex/Hoare.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 2380 90280b3a538b
child 12036 49f6c49454c2
permissions -rw-r--r--
` -> $
clasohm@1479
     1
(*  Title:      HOLCF/ex/hoare.thy
nipkow@244
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
clasohm@1479
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@244
     5
nipkow@244
     6
Theory for an example by C.A.R. Hoare 
nipkow@244
     7
regensbu@1168
     8
p x = if b1 x 
regensbu@1168
     9
         then p (g x)
nipkow@244
    10
         else x fi
nipkow@244
    11
regensbu@1168
    12
q x = if b1 x orelse b2 x 
regensbu@1168
    13
         then q (g x)
nipkow@244
    14
         else x fi
nipkow@244
    15
nipkow@244
    16
Prove: for all b1 b2 g . 
nipkow@244
    17
            q o p  = q 
nipkow@244
    18
nipkow@244
    19
In order to get a nice notation we fix the functions b1,b2 and g in the
nipkow@244
    20
signature of this example
nipkow@244
    21
nipkow@244
    22
*)
nipkow@244
    23
sandnerr@2380
    24
Hoare = HOLCF + 
nipkow@244
    25
nipkow@244
    26
consts
clasohm@1479
    27
        b1:: "'a -> tr"
clasohm@1479
    28
        b2:: "'a -> tr"
clasohm@1479
    29
         g:: "'a -> 'a"
clasohm@1479
    30
        p :: "'a -> 'a"
clasohm@1479
    31
        q :: "'a -> 'a"
nipkow@244
    32
regensbu@1168
    33
defs
nipkow@244
    34
nipkow@10835
    35
  p_def  "p == fix$(LAM f. LAM x.
nipkow@10835
    36
                 If b1$x then f$(g$x) else x fi)"
nipkow@244
    37
nipkow@10835
    38
  q_def  "q == fix$(LAM f. LAM x.
nipkow@10835
    39
                 If b1$x orelse b2$x then f$(g$x) else x fi)"
nipkow@244
    40
nipkow@244
    41
end
nipkow@244
    42