src/HOL/IMP/Vars.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 45716 ccf2cbe86d70
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@43158
     3
header "Definite Assignment Analysis"
kleing@43158
     4
kleing@43158
     5
theory Vars imports Util BExp
kleing@43158
     6
begin
kleing@43158
     7
kleing@43158
     8
subsection "The Variables in an Expression"
kleing@43158
     9
kleing@43158
    10
text{* We need to collect the variables in both arithmetic and boolean
kleing@43158
    11
expressions. For a change we do not introduce two functions, e.g.\ @{text
kleing@43158
    12
avars} and @{text bvars}, but we overload the name @{text vars}
kleing@43158
    13
via a \emph{type class}, a device that originated with Haskell: *}
kleing@43158
    14
 
kleing@43158
    15
class vars =
nipkow@45212
    16
fixes vars :: "'a \<Rightarrow> vname set"
kleing@43158
    17
kleing@43158
    18
text{* This defines a type class ``vars'' with a single
kleing@43158
    19
function of (coincidentally) the same name. Then we define two separated
kleing@43158
    20
instances of the class, one for @{typ aexp} and one for @{typ bexp}: *}
kleing@43158
    21
kleing@43158
    22
instantiation aexp :: vars
kleing@43158
    23
begin
kleing@43158
    24
nipkow@45212
    25
fun vars_aexp :: "aexp \<Rightarrow> vname set" where
kleing@43158
    26
"vars_aexp (N n) = {}" |
kleing@43158
    27
"vars_aexp (V x) = {x}" |
kleing@43158
    28
"vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2"
kleing@43158
    29
kleing@43158
    30
instance ..
kleing@43158
    31
kleing@43158
    32
end
kleing@43158
    33
kleing@43158
    34
value "vars(Plus (V ''x'') (V ''y''))"
kleing@43158
    35
kleing@43158
    36
text{* We need to convert functions to lists before we can view them: *}
kleing@43158
    37
kleing@43158
    38
value "show  (vars(Plus (V ''x'') (V ''y'')))"
kleing@43158
    39
kleing@43158
    40
instantiation bexp :: vars
kleing@43158
    41
begin
kleing@43158
    42
nipkow@45212
    43
fun vars_bexp :: "bexp \<Rightarrow> vname set" where
nipkow@45200
    44
"vars_bexp (Bc v) = {}" |
kleing@43158
    45
"vars_bexp (Not b) = vars_bexp b" |
kleing@43158
    46
"vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |
kleing@43158
    47
"vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
kleing@43158
    48
kleing@43158
    49
instance ..
kleing@43158
    50
kleing@43158
    51
end
kleing@43158
    52
kleing@43158
    53
value "show  (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"
kleing@43158
    54
kleing@43158
    55
abbreviation
kleing@43158
    56
  eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
kleing@43158
    57
 ("(_ =/ _/ on _)" [50,0,50] 50) where
kleing@43158
    58
"f = g on X == \<forall> x \<in> X. f x = g x"
kleing@43158
    59
kleing@43158
    60
lemma aval_eq_if_eq_on_vars[simp]:
kleing@43158
    61
  "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
nipkow@45015
    62
apply(induction a)
kleing@43158
    63
apply simp_all
kleing@43158
    64
done
kleing@43158
    65
kleing@43158
    66
lemma bval_eq_if_eq_on_vars:
kleing@43158
    67
  "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
nipkow@45015
    68
proof(induction b)
kleing@43158
    69
  case (Less a1 a2)
kleing@43158
    70
  hence "aval a1 s\<^isub>1 = aval a1 s\<^isub>2" and "aval a2 s\<^isub>1 = aval a2 s\<^isub>2" by simp_all
kleing@43158
    71
  thus ?case by simp
kleing@43158
    72
qed simp_all
kleing@43158
    73
kleing@43158
    74
end