Theory Typing_Framework_2

(*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM
*)

section ‹Typing and Dataflow Analysis Framework›

theory Typing_Framework_2 imports Typing_Framework_1 begin

text ‹
  The relationship between dataflow analysis and a welltyped-instruction predicate. 
›

definition is_bcv :: "'s ord ⇒ 's ⇒ 's step_type ⇒ nat ⇒ 's set ⇒ ('s list ⇒ 's list) ⇒ bool"
where
  "is_bcv r T step n A bcv ⟷ (∀τs⇩0 ∈ nlists n A.
  (∀p<n. (bcv τs⇩0)!p ≠ T) = (∃τs ∈ nlists n A. τs⇩0 [⊑⇩r] τs ∧ wt_step r T step τs))"

end