src/HOLCF/ex/Hoare.thy
author sandnerr
Fri, 13 Dec 1996 12:01:26 +0100
changeset 2380 90280b3a538b
parent 2379 2e55b396e24c
child 10835 f4745d77e620
permissions -rw-r--r--
Dummy change to document the change in revision 1.5: Parent theory changed to HOLCF.thy (former Tr2.thy) . Was necessary because the use of HOLCF_ss in Hoare.ML, which has been extended by the introduction of the Lift theories.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
     1
(*  Title:      HOLCF/ex/hoare.thy
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
     3
    Author:     Franz Regensburger
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
     4
    Copyright   1993 Technische Universitaet Muenchen
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     5
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     6
Theory for an example by C.A.R. Hoare 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     7
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
     8
p x = if b1 x 
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
     9
         then p (g x)
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    10
         else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    11
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    12
q x = if b1 x orelse b2 x 
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    13
         then q (g x)
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    14
         else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    15
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    16
Prove: for all b1 b2 g . 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    17
            q o p  = q 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    18
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    19
In order to get a nice notation we fix the functions b1,b2 and g in the
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    20
signature of this example
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    21
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    22
*)
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    23
2380
90280b3a538b Dummy change to document the change in revision 1.5:
sandnerr
parents: 2379
diff changeset
    24
Hoare = HOLCF + 
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    25
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    26
consts
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
    27
        b1:: "'a -> tr"
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
    28
        b2:: "'a -> tr"
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
    29
         g:: "'a -> 'a"
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
    30
        p :: "'a -> 'a"
21eb5e156d91 expanded tabs
clasohm
parents: 1168
diff changeset
    31
        q :: "'a -> 'a"
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    32
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    33
defs
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    34
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    35
  p_def  "p == fix`(LAM f. LAM x.
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    36
                 If b1`x then f`(g`x) else x fi)"
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    37
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    38
  q_def  "q == fix`(LAM f. LAM x.
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    39
                 If b1`x orelse b2`x then f`(g`x) else x fi)"
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    40
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    41
end
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    42