src/HOL/BCV/DFAandWTI.thy

new distributive laws

(*  Title:      HOL/BCV/DFAandWTI.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1999 TUM

The relationship between dataflow analysis and a welltyped-insruction predicate.
*)

DFAandWTI = SemiLattice +

types 's os = 's option list

constdefs

 stable :: (nat => 's => 's option) => (nat => nat list) => nat => 's os => bool
"stable step succs p sos ==
 !s. sos!p = Some s --> (? t. step p s = Some(t) &
                              (!q:set(succs p). Some t <= sos!q))"

 wti_is_fix_step ::
   "(nat => 's => 's option)
    => (nat => 's os => bool)
    => (nat => nat list)
    => nat => 's set => bool"
"wti_is_fix_step step wti succs n L == !sos p.
   sos : listsn n (option L) & p < n -->
   wti p sos = stable step succs p sos"

 welltyping :: (nat => 's os => bool) => 's os => bool
"welltyping wti tos == !p<size(tos). wti p tos"

 is_dfa ::  ('s os => bool)
            => (nat => 's => 's option)
            => (nat => nat list)
            => nat => 's set => bool
"is_dfa dfa step succs n L == !sos : listsn n (option L).
   dfa sos =
   (? tos : listsn n (option L).
      sos <= tos & (!p < n. stable step succs p tos))"

end