src/HOL/UNITY/Comp.thy
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5612 e981ca6f7332
child 6012 1894bfc4aee9
permissions -rw-r--r--
Drule.rev_triv_goal;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Comp.thy
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     5
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     6
Composition
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     7
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     8
From Chandy and Sanders, "Reasoning About Program Composition"
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     9
*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    10
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    11
Comp = Union +
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    12
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    13
constdefs
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    14
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    15
  (*Existential and Universal properties.  I formalize the two-program
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    16
    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    17
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    18
  ex_prop  :: 'a program set => bool
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    19
   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    20
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    21
  strict_ex_prop  :: 'a program set => bool
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    22
   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    23
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    24
  uv_prop  :: 'a program set => bool
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    25
   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (F Join G) : X)"
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    26
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    27
  strict_uv_prop  :: 'a program set => bool
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    28
   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (F Join G : X))"
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    29
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    30
  (*Ill-defined programs can arise through "Join"*)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    31
  welldef :: 'a program set  
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    32
   "welldef == {F. Init F ~= {}}"
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    33
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    34
  component :: ['a program, 'a program] => bool
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    35
   "component F H == EX G. F Join G = H"
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    36
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    37
  guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    38
   "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    39
5612
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    40
  refines :: ['a program, 'a program, 'a program set] => bool
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    41
			("(3_ refines _ wrt _)" [10,10,10] 10)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    42
   "G refines F wrt X ==
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    43
      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    44
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    45
  iso_refines :: ['a program, 'a program, 'a program set] => bool
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    46
			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    47
   "G iso_refines F wrt X ==
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    48
      F : welldef Int X --> G : welldef Int X"
e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents: 5597
diff changeset
    49
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    50
end