Up to index of Isabelle/HOL/Jinja
theory Typing_Framework(* Title: HOL/MicroJava/BV/Typing_Framework.thy
Author: Tobias Nipkow
Copyright 2000 TUM
*)
header {* \isaheader{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)). τ \<sqsubseteq>⇩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 [\<sqsubseteq>⇩r] τs ∧ wt_step r T step τs))"
end