Theory 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