Theory Jinja.Typing_Framework_1

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

section ‹Typing and Dataflow Analysis Framework›

theory Typing_Framework_1 imports Semilattices begin

text ‹
  The relationship between dataflow analysis and a welltyped-instruction predicate. 
›
type_synonym
  's step_type = "nat  's  (nat × 's) list"

definition stable :: "'s ord  's step_type  's list  nat  bool"
where
  "stable r step τs p  ((q,τ)  set (step p (τs!p)). τ ⊑⇩r τs!q)"

definition stables :: "'s ord  's step_type  's list  bool"
where
  "stables r step τs  (p < size τs. stable r step τs p)"

definition wt_step :: "'s ord  's  's step_type  's list  bool"
where
  "wt_step r T step τs  (p<size τs. τs!p  T  stable r step τs p)"

end