src/HOLCF/ex/Hoare.thy
author nipkow
Wed Jan 19 17:40:26 1994 +0100 (1994-01-19)
changeset 244 929fc2c63bd0
child 1150 66512c9e6bd6
permissions -rw-r--r--
HOLCF examples
nipkow@244
     1
(*  Title:	HOLCF/ex/hoare.thy
nipkow@244
     2
    ID:         $Id$
nipkow@244
     3
    Author: 	Franz Regensburger
nipkow@244
     4
    Copyright	1993 Technische Universitaet Muenchen
nipkow@244
     5
nipkow@244
     6
Theory for an example by C.A.R. Hoare 
nipkow@244
     7
nipkow@244
     8
p x = if b1(x) 
nipkow@244
     9
         then p(g(x))
nipkow@244
    10
         else x fi
nipkow@244
    11
nipkow@244
    12
q x = if b1(x) orelse b2(x) 
nipkow@244
    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
nipkow@244
    24
Hoare = Tr2 +
nipkow@244
    25
nipkow@244
    26
consts
nipkow@244
    27
	b1:: "'a -> tr"
nipkow@244
    28
	b2:: "'a -> tr"
nipkow@244
    29
	 g:: "'a -> 'a"
nipkow@244
    30
	p :: "'a -> 'a"
nipkow@244
    31
	q :: "'a -> 'a"
nipkow@244
    32
nipkow@244
    33
rules
nipkow@244
    34
nipkow@244
    35
  p_def  "p == fix[LAM f. LAM x.\
nipkow@244
    36
\                 If b1[x] then f[g[x]] else x fi]"
nipkow@244
    37
nipkow@244
    38
  q_def  "q == fix[LAM f. LAM x.\
nipkow@244
    39
\                 If b1[x] orelse b2[x] then f[g[x]] else x fi]"
nipkow@244
    40
nipkow@244
    41
nipkow@244
    42
end
nipkow@244
    43