src/HOLCF/ex/Hoare.thy
author wenzelm
Tue Sep 06 19:28:58 2005 +0200 (2005-09-06)
changeset 17291 94f6113fe9ed
parent 14981 e73f8140af78
child 19742 86f21beabafc
permissions -rw-r--r--
converted to Isar theory format;
clasohm@1479
     1
(*  Title:      HOLCF/ex/hoare.thy
nipkow@244
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@244
     4
wenzelm@12036
     5
Theory for an example by C.A.R. Hoare
nipkow@244
     6
wenzelm@17291
     7
p x = if b1 x
regensbu@1168
     8
         then p (g x)
nipkow@244
     9
         else x fi
nipkow@244
    10
wenzelm@17291
    11
q x = if b1 x orelse b2 x
regensbu@1168
    12
         then q (g x)
nipkow@244
    13
         else x fi
nipkow@244
    14
wenzelm@17291
    15
Prove: for all b1 b2 g .
wenzelm@17291
    16
            q o p  = q
nipkow@244
    17
nipkow@244
    18
In order to get a nice notation we fix the functions b1,b2 and g in the
nipkow@244
    19
signature of this example
nipkow@244
    20
nipkow@244
    21
*)
nipkow@244
    22
wenzelm@17291
    23
theory Hoare
wenzelm@17291
    24
imports HOLCF
wenzelm@17291
    25
begin
nipkow@244
    26
nipkow@244
    27
consts
wenzelm@17291
    28
  b1 :: "'a -> tr"
wenzelm@17291
    29
  b2 :: "'a -> tr"
wenzelm@17291
    30
  g :: "'a -> 'a"
wenzelm@17291
    31
  p :: "'a -> 'a"
wenzelm@17291
    32
  q :: "'a -> 'a"
nipkow@244
    33
regensbu@1168
    34
defs
wenzelm@17291
    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
wenzelm@17291
    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
wenzelm@17291
    41
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17291
    42
nipkow@244
    43
end