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;
nipkow@11229
     1
(*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
nipkow@11229
     2
    ID:         $Id$
nipkow@11229
     3
    Author:     Tobias Nipkow
nipkow@11229
     4
    Copyright   2000 TUM
nipkow@11229
     5
*)
nipkow@11229
     6
kleing@12911
     7
header {* \isaheader{Typing and Dataflow Analysis Framework} *}
nipkow@11229
     8
haftmann@16417
     9
theory Typing_Framework imports Listn begin
nipkow@11229
    10
nipkow@11229
    11
text {* 
kleing@13224
    12
  The relationship between dataflow analysis and a welltyped-instruction predicate. 
nipkow@11229
    13
*}
kleing@12516
    14
types
kleing@12516
    15
  's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
nipkow@11229
    16
nipkow@11229
    17
constdefs
kleing@13006
    18
 stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
kleing@12516
    19
"stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
nipkow@11229
    20
kleing@13006
    21
 stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
kleing@12516
    22
"stables r step ss == !p<size ss. stable r step ss p"
nipkow@11229
    23
wenzelm@14653
    24
 wt_step ::
wenzelm@14653
    25
"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
wenzelm@14653
    26
"wt_step r T step ts ==
wenzelm@14653
    27
 !p<size(ts). ts!p ~= T & stable r step ts p"
wenzelm@14653
    28
kleing@13006
    29
 is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type 
kleing@13006
    30
           \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"  
kleing@12516
    31
"is_bcv r T step n A bcv == !ss : list n A.
nipkow@11229
    32
   (!p<n. (bcv ss)!p ~= T) =
kleing@12516
    33
   (? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
nipkow@11229
    34
nipkow@11229
    35
end