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