src/HOL/IMP/Vars.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58889 5b7a9633cfa8
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
wenzelm@58889
     3
section "Definite Initialization Analysis"
kleing@43158
     4
nipkow@51698
     5
theory Vars imports Com
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
nipkow@45774
    26
"vars (N n) = {}" |
nipkow@45774
    27
"vars (V x) = {x}" |
wenzelm@53015
    28
"vars (Plus a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
kleing@43158
    29
kleing@43158
    30
instance ..
kleing@43158
    31
kleing@43158
    32
end
kleing@43158
    33
nipkow@50173
    34
value "vars (Plus (V ''x'') (V ''y''))"
kleing@43158
    35
kleing@43158
    36
instantiation bexp :: vars
kleing@43158
    37
begin
kleing@43158
    38
nipkow@45212
    39
fun vars_bexp :: "bexp \<Rightarrow> vname set" where
nipkow@45774
    40
"vars (Bc v) = {}" |
nipkow@45774
    41
"vars (Not b) = vars b" |
wenzelm@53015
    42
"vars (And b\<^sub>1 b\<^sub>2) = vars b\<^sub>1 \<union> vars b\<^sub>2" |
wenzelm@53015
    43
"vars (Less a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
kleing@43158
    44
kleing@43158
    45
instance ..
kleing@43158
    46
kleing@43158
    47
end
kleing@43158
    48
nipkow@50173
    49
value "vars (Less (Plus (V ''z'') (V ''y'')) (V ''x''))"
kleing@43158
    50
kleing@43158
    51
abbreviation
kleing@43158
    52
  eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
kleing@43158
    53
 ("(_ =/ _/ on _)" [50,0,50] 50) where
kleing@43158
    54
"f = g on X == \<forall> x \<in> X. f x = g x"
kleing@43158
    55
kleing@43158
    56
lemma aval_eq_if_eq_on_vars[simp]:
wenzelm@53015
    57
  "s\<^sub>1 = s\<^sub>2 on vars a \<Longrightarrow> aval a s\<^sub>1 = aval a s\<^sub>2"
nipkow@45015
    58
apply(induction a)
kleing@43158
    59
apply simp_all
kleing@43158
    60
done
kleing@43158
    61
kleing@43158
    62
lemma bval_eq_if_eq_on_vars:
wenzelm@53015
    63
  "s\<^sub>1 = s\<^sub>2 on vars b \<Longrightarrow> bval b s\<^sub>1 = bval b s\<^sub>2"
nipkow@45015
    64
proof(induction b)
kleing@43158
    65
  case (Less a1 a2)
wenzelm@53015
    66
  hence "aval a1 s\<^sub>1 = aval a1 s\<^sub>2" and "aval a2 s\<^sub>1 = aval a2 s\<^sub>2" by simp_all
kleing@43158
    67
  thus ?case by simp
kleing@43158
    68
qed simp_all
kleing@43158
    69
nipkow@52072
    70
fun lvars :: "com \<Rightarrow> vname set" where
nipkow@52072
    71
"lvars SKIP = {}" |
nipkow@52072
    72
"lvars (x::=e) = {x}" |
nipkow@52072
    73
"lvars (c1;;c2) = lvars c1 \<union> lvars c2" |
nipkow@52072
    74
"lvars (IF b THEN c1 ELSE c2) = lvars c1 \<union> lvars c2" |
nipkow@52072
    75
"lvars (WHILE b DO c) = lvars c"
nipkow@52072
    76
nipkow@52072
    77
fun rvars :: "com \<Rightarrow> vname set" where
nipkow@52072
    78
"rvars SKIP = {}" |
nipkow@52072
    79
"rvars (x::=e) = vars e" |
nipkow@52072
    80
"rvars (c1;;c2) = rvars c1 \<union> rvars c2" |
nipkow@52072
    81
"rvars (IF b THEN c1 ELSE c2) = vars b \<union> rvars c1 \<union> rvars c2" |
nipkow@52072
    82
"rvars (WHILE b DO c) = vars b \<union> rvars c"
nipkow@51698
    83
nipkow@51698
    84
instantiation com :: vars
nipkow@51698
    85
begin
nipkow@51698
    86
nipkow@52072
    87
definition "vars_com c = lvars c \<union> rvars c"
nipkow@51698
    88
nipkow@51698
    89
instance ..
nipkow@51698
    90
kleing@43158
    91
end
nipkow@51698
    92
nipkow@52072
    93
lemma vars_com_simps[simp]:
nipkow@52072
    94
  "vars SKIP = {}"
nipkow@52072
    95
  "vars (x::=e) = {x} \<union> vars e"
nipkow@52072
    96
  "vars (c1;;c2) = vars c1 \<union> vars c2"
nipkow@52072
    97
  "vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2"
nipkow@52072
    98
  "vars (WHILE b DO c) = vars b \<union> vars c"
nipkow@52072
    99
by(auto simp: vars_com_def)
nipkow@51698
   100
nipkow@51698
   101
lemma finite_avars[simp]: "finite(vars(a::aexp))"
nipkow@51698
   102
by(induction a) simp_all
nipkow@51698
   103
nipkow@51698
   104
lemma finite_bvars[simp]: "finite(vars(b::bexp))"
nipkow@52072
   105
by(induction b) simp_all
nipkow@52072
   106
nipkow@52072
   107
lemma finite_lvars[simp]: "finite(lvars(c))"
nipkow@52072
   108
by(induction c) simp_all
nipkow@52072
   109
nipkow@52072
   110
lemma finite_rvars[simp]: "finite(rvars(c))"
nipkow@52072
   111
by(induction c) simp_all
nipkow@51698
   112
nipkow@51698
   113
lemma finite_cvars[simp]: "finite(vars(c::com))"
nipkow@52072
   114
by(simp add: vars_com_def)
nipkow@51698
   115
nipkow@51698
   116
end