src/HOL/MicroJava/BV/Typing_Framework.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 27680 5a557a5afc48
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000 TUM
     5 *)
     6 
     7 header {* \isaheader{Typing and Dataflow Analysis Framework} *}
     8 
     9 theory Typing_Framework imports Listn begin
    10 
    11 text {* 
    12   The relationship between dataflow analysis and a welltyped-instruction predicate. 
    13 *}
    14 types
    15   's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
    16 
    17 constdefs
    18  stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
    19 "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
    20 
    21  stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
    22 "stables r step ss == !p<size ss. stable r step ss p"
    23 
    24  wt_step ::
    25 "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
    26 "wt_step r T step ts ==
    27  !p<size(ts). ts!p ~= T & stable r step ts p"
    28 
    29  is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type 
    30            \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"  
    31 "is_bcv r T step n A bcv == !ss : list n A.
    32    (!p<n. (bcv ss)!p ~= T) =
    33    (? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
    34 
    35 end