<commit_before>(*  Title:      HOL/UNITY/Comp.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Composition

From Chandy and Sanders, "Reasoning About Program Composition"
*)

Comp = Union +

constdefs

  (*Existential and Universal properties.  I formalize the two-program
    case, proving equivalence with Chandy and Sanders's n-ary definitions*)

  ex_prop  :: 'a program set => bool
   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"

  strict_ex_prop  :: 'a program set => bool
   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"

  uv_prop  :: 'a program set => bool
   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"

  strict_uv_prop  :: 'a program set => bool
   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"

  (*Ill-defined programs can arise through "Join"*)
  welldef :: 'a program set  
   "welldef == {F. Init F ~= {}}"

  component :: ['a program, 'a program] => bool     (infixl 50)
   "F component H == EX G. F Join G = H"

  guarantees :: ['a program set, 'a program set] => 'a program set
                                                    (infixl "guar" 65)
   "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"

  refines :: ['a program, 'a program, 'a program set] => bool
			("(3_ refines _ wrt _)" [10,10,10] 10)
   "G refines F wrt X ==
      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"

  iso_refines :: ['a program, 'a program, 'a program set] => bool
			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
   "G iso_refines F wrt X ==
      F : welldef Int X --> G : welldef Int X"

end<commit_msg>changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE<commit_after>(*  Title:      HOL/UNITY/Comp.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Composition

From Chandy and Sanders, "Reasoning About Program Composition"
*)

Comp = Union +

constdefs

  (*Existential and Universal properties.  I formalize the two-program
    case, proving equivalence with Chandy and Sanders's n-ary definitions*)

  ex_prop  :: 'a program set => bool
   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"

  strict_ex_prop  :: 'a program set => bool
   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"

  uv_prop  :: 'a program set => bool
   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"

  strict_uv_prop  :: 'a program set => bool
   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"

  (*Ill-defined programs can arise through "Join"*)
  welldef :: 'a program set  
   "welldef == {F. Init F ~= {}}"

  component :: ['a program, 'a program] => bool     (infixl 50)
   "F component H == EX G. F Join G = H"

  guar :: ['a program set, 'a program set] => 'a program set
   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"

  refines :: ['a program, 'a program, 'a program set] => bool
			("(3_ refines _ wrt _)" [10,10,10] 10)
   "G refines F wrt X ==
      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"

  iso_refines :: ['a program, 'a program, 'a program set] => bool
			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
   "G iso_refines F wrt X ==
      F : welldef Int X --> G : welldef Int X"

end
{'fraction_non_alphanumeric': 0.14682884448305822, 'fraction_numerical': 0.015059368664929048, 'mean_word_length': 2.546201232032854, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4899222', 'n_tokens_mistral': 1325, 'n_tokens_neox': 1235, 'n_words': 480}