src/HOLCF/IOA/meta_theory/RefCorrectness.thy

 (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
     ID:         $Id$
     Author:     Olaf Müller
-
-Correctness of Refinement Mappings in HOLCF/IOA.
 *)
 
+header {* Correctness of Refinement Mappings in HOLCF/IOA *}
 
-RefCorrectness = RefMappings + 
-   
+theory RefCorrectness
+imports RefMappings
+begin
+
 consts
 
-  corresp_ex   ::"('a,'s2)ioa => ('s1 => 's2) => 
+  corresp_ex   ::"('a,'s2)ioa => ('s1 => 's2) =>
                   ('a,'s1)execution => ('a,'s2)execution"
   corresp_exC  ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
                    -> ('s1 => ('a,'s2)pairs)"
   is_fair_ref_map  :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool"
 
 defs
 
-corresp_ex_def
+corresp_ex_def:
   "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
 
 
-corresp_exC_def
-  "corresp_exC A f  == (fix$(LAM h ex. (%s. case ex of 
+corresp_exC_def:
+  "corresp_exC A f  == (fix$(LAM h ex. (%s. case ex of
       nil =>  nil
     | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
                               @@ ((h$xs) (snd pr)))
                         $x) )))"
- 
-is_fair_ref_map_def
-  "is_fair_ref_map f C A == 
+
+is_fair_ref_map_def:
+  "is_fair_ref_map f C A ==
        is_ref_map f C A &
        (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))"
 
 
 
-rules
+axioms
 (* Axioms for fair trace inclusion proof support, not for the correctness proof
-   of refinement mappings ! 
+   of refinement mappings!
    Note: Everything is superseded by LiveIOA.thy! *)
 
-corresp_laststate
+corresp_laststate:
   "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
 
-corresp_Finite
+corresp_Finite:
   "Finite (snd (corresp_ex A f (s,ex))) = Finite ex"
 
-FromAtoC
+FromAtoC:
   "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"
 
-FromCtoA
+FromCtoA:
   "inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
 
 
 (* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is
    an index i from which on no W in ex. But W inf enabled, ie at least once after i
    W is enabled. As W does not occur after i and W is enabling_persistent, W keeps
    enabled until infinity, ie. indefinitely *)
-persistent
+persistent:
   "[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|]
    ==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex"
 
-infpostcond
+infpostcond:
   "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|]
     ==> inf_often (% x. set_was_enabled A W (snd x)) ex"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end