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
     1 (* Author: Tobias Nipkow *)
     2 
     3 section "Definite Initialization Analysis"
     4 
     5 theory Vars imports Com
     6 begin
     7 
     8 subsection "The Variables in an Expression"
     9 
    10 text{* We need to collect the variables in both arithmetic and boolean
    11 expressions. For a change we do not introduce two functions, e.g.\ @{text
    12 avars} and @{text bvars}, but we overload the name @{text vars}
    13 via a \emph{type class}, a device that originated with Haskell: *}
    14  
    15 class vars =
    16 fixes vars :: "'a \<Rightarrow> vname set"
    17 
    18 text{* This defines a type class ``vars'' with a single
    19 function of (coincidentally) the same name. Then we define two separated
    20 instances of the class, one for @{typ aexp} and one for @{typ bexp}: *}
    21 
    22 instantiation aexp :: vars
    23 begin
    24 
    25 fun vars_aexp :: "aexp \<Rightarrow> vname set" where
    26 "vars (N n) = {}" |
    27 "vars (V x) = {x}" |
    28 "vars (Plus a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
    29 
    30 instance ..
    31 
    32 end
    33 
    34 value "vars (Plus (V ''x'') (V ''y''))"
    35 
    36 instantiation bexp :: vars
    37 begin
    38 
    39 fun vars_bexp :: "bexp \<Rightarrow> vname set" where
    40 "vars (Bc v) = {}" |
    41 "vars (Not b) = vars b" |
    42 "vars (And b\<^sub>1 b\<^sub>2) = vars b\<^sub>1 \<union> vars b\<^sub>2" |
    43 "vars (Less a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
    44 
    45 instance ..
    46 
    47 end
    48 
    49 value "vars (Less (Plus (V ''z'') (V ''y'')) (V ''x''))"
    50 
    51 abbreviation
    52   eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
    53  ("(_ =/ _/ on _)" [50,0,50] 50) where
    54 "f = g on X == \<forall> x \<in> X. f x = g x"
    55 
    56 lemma aval_eq_if_eq_on_vars[simp]:
    57   "s\<^sub>1 = s\<^sub>2 on vars a \<Longrightarrow> aval a s\<^sub>1 = aval a s\<^sub>2"
    58 apply(induction a)
    59 apply simp_all
    60 done
    61 
    62 lemma bval_eq_if_eq_on_vars:
    63   "s\<^sub>1 = s\<^sub>2 on vars b \<Longrightarrow> bval b s\<^sub>1 = bval b s\<^sub>2"
    64 proof(induction b)
    65   case (Less a1 a2)
    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
    67   thus ?case by simp
    68 qed simp_all
    69 
    70 fun lvars :: "com \<Rightarrow> vname set" where
    71 "lvars SKIP = {}" |
    72 "lvars (x::=e) = {x}" |
    73 "lvars (c1;;c2) = lvars c1 \<union> lvars c2" |
    74 "lvars (IF b THEN c1 ELSE c2) = lvars c1 \<union> lvars c2" |
    75 "lvars (WHILE b DO c) = lvars c"
    76 
    77 fun rvars :: "com \<Rightarrow> vname set" where
    78 "rvars SKIP = {}" |
    79 "rvars (x::=e) = vars e" |
    80 "rvars (c1;;c2) = rvars c1 \<union> rvars c2" |
    81 "rvars (IF b THEN c1 ELSE c2) = vars b \<union> rvars c1 \<union> rvars c2" |
    82 "rvars (WHILE b DO c) = vars b \<union> rvars c"
    83 
    84 instantiation com :: vars
    85 begin
    86 
    87 definition "vars_com c = lvars c \<union> rvars c"
    88 
    89 instance ..
    90 
    91 end
    92 
    93 lemma vars_com_simps[simp]:
    94   "vars SKIP = {}"
    95   "vars (x::=e) = {x} \<union> vars e"
    96   "vars (c1;;c2) = vars c1 \<union> vars c2"
    97   "vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2"
    98   "vars (WHILE b DO c) = vars b \<union> vars c"
    99 by(auto simp: vars_com_def)
   100 
   101 lemma finite_avars[simp]: "finite(vars(a::aexp))"
   102 by(induction a) simp_all
   103 
   104 lemma finite_bvars[simp]: "finite(vars(b::bexp))"
   105 by(induction b) simp_all
   106 
   107 lemma finite_lvars[simp]: "finite(lvars(c))"
   108 by(induction c) simp_all
   109 
   110 lemma finite_rvars[simp]: "finite(rvars(c))"
   111 by(induction c) simp_all
   112 
   113 lemma finite_cvars[simp]: "finite(vars(c::com))"
   114 by(simp add: vars_com_def)
   115 
   116 end