Theory Typing_Framework

(*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
    ID:         $Id: Typing_Framework.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2000 TUM
*)

header {* \isaheader{Typing and Dataflow Analysis Framework} *}

theory Typing_Framework = Semilattices:

text {* 
  The relationship between dataflow analysis and a welltyped-instruction predicate. 
*}
types
  's step_type = "nat => 's => (nat × 's) list"

constdefs
  stable :: "'s ord => 's step_type => 's list => nat => bool"
  "stable r step τs p ≡ ∀(q,τ) ∈ set (step p (τs!p)). τ \<sqsubseteq>r τs!q"

  stables :: "'s ord => 's step_type => 's list => bool"
  "stables r step τs ≡ ∀p < size τs. stable r step τs p"

  wt_step :: "'s ord => 's => 's step_type => 's list => bool"
  "wt_step r T step τs ≡ ∀p<size τs. τs!p ≠ T ∧ stable r step τs p"

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

end