Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
author mueller
Wed, 30 Apr 1997 11:20:15 +0200
changeset 3071 981258186b71
child 3275 3f53f2c876f4
permissions -rw-r--r--
New meta theory for IOA based on HOLCF.

(*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
    ID:         $$
    Author:     Olaf Mueller
    Copyright   1996  TU Muenchen

Correctness of Refinement Mappings in HOLCF/IOA
*)


RefCorrectness = RefMappings + 

consts

  corresp_ex   ::"('a,'s2)ioa => ('s1 => 's2) => 
                  ('a,'s1)execution => ('a,'s2)execution"
  corresp_ex2  ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
                   -> ('s2 => ('a,'s2)pairs)"


defs

corresp_ex_def
  "corresp_ex A f ex == (f (fst ex),(corresp_ex2 A f`(snd ex)) (f (fst ex)))"


corresp_ex2_def
  "corresp_ex2 A f  == (fix`(LAM h ex. (%s. case ex of 
      nil =>  nil
    | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr))))
                              @@ ((h`xs) (f (snd pr))))
                        `x) )))"
 


end
isabelle