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