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"
  "is_bcv r T step n A bcv  (τs0  nlists n A.
  (p<n. (bcv τs0)!p  T) = (τs  nlists n A. τs0 [⊑⇩r] τs  wt_step r T step τs))"