src/HOL/IMP/Live.thy
 changeset 45212 e87feee00a4c parent 45015 fdac1e9880eb child 45770 5d35cb2c0f02
1.1 --- a/src/HOL/IMP/Live.thy	Wed Oct 19 23:07:48 2011 +0200
1.2 +++ b/src/HOL/IMP/Live.thy	Thu Oct 20 09:48:00 2011 +0200
1.3 @@ -7,7 +7,7 @@
1.5  subsection "Liveness Analysis"
1.7 -fun L :: "com \<Rightarrow> name set \<Rightarrow> name set" where
1.8 +fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
1.9  "L SKIP X = X" |
1.10  "L (x ::= a) X = X-{x} \<union> vars a" |
1.11  "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
1.12 @@ -18,14 +18,14 @@
1.14  value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
1.16 -fun "kill" :: "com \<Rightarrow> name set" where
1.17 +fun "kill" :: "com \<Rightarrow> vname set" where
1.18  "kill SKIP = {}" |
1.19  "kill (x ::= a) = {x}" |
1.20  "kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
1.21  "kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
1.22  "kill (WHILE b DO c) = {}"
1.24 -fun gen :: "com \<Rightarrow> name set" where
1.25 +fun gen :: "com \<Rightarrow> vname set" where
1.26  "gen SKIP = {}" |
1.27  "gen (x ::= a) = vars a" |
1.28  "gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
1.29 @@ -94,7 +94,7 @@
1.30  subsection "Program Optimization"
1.32  text{* Burying assignments to dead variables: *}
1.33 -fun bury :: "com \<Rightarrow> name set \<Rightarrow> com" where
1.34 +fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
1.35  "bury SKIP X = SKIP" |
1.36  "bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
1.37  "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |