Theory Typing_Framework

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

section ‹Typing and Dataflow Analysis Framework›

theory Typing_Framework
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)"

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 ∈ list n A.
  (∀p<n. (bcv τs⇩0)!p ≠ T) = (∃τs ∈ list n A. τs⇩0 [⊑⇩r] τs ∧ wt_step r T step τs))"

end