Theory Typing_Framework

theory Typing_Framework
imports Listn
(*  Title:      HOL/MicroJava/DFA/Typing_Framework.thy
Author: Tobias Nipkow
Copyright 2000 TUM
*)


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

theory Typing_Framework
imports Listn
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 ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"

definition stables :: "'s ord => 's step_type => 's list => bool" where
"stables r step ss == !p<size ss. stable r step ss p"

definition wt_step ::
"'s ord => 's => 's step_type => 's list => bool" where
"wt_step r T step ts ==
!p<size(ts). ts!p ~= T & stable r step ts 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 == !ss : list n A.
(!p<n. (bcv ss)!p ~= T) =
(? ts: list n A. ss <=[r] ts & wt_step r T step ts)"


end