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
     1 (* Author: Tobias Nipkow *)
     2 
     3 header "Definite Assignment Analysis"
     4 
     5 theory Vars imports Util BExp
     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_aexp (N n) = {}" |
    27 "vars_aexp (V x) = {x}" |
    28 "vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2"
    29 
    30 instance ..
    31 
    32 end
    33 
    34 value "vars(Plus (V ''x'') (V ''y''))"
    35 
    36 text{* We need to convert functions to lists before we can view them: *}
    37 
    38 value "show  (vars(Plus (V ''x'') (V ''y'')))"
    39 
    40 instantiation bexp :: vars
    41 begin
    42 
    43 fun vars_bexp :: "bexp \<Rightarrow> vname set" where
    44 "vars_bexp (Bc v) = {}" |
    45 "vars_bexp (Not b) = vars_bexp b" |
    46 "vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |
    47 "vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
    48 
    49 instance ..
    50 
    51 end
    52 
    53 value "show  (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"
    54 
    55 abbreviation
    56   eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
    57  ("(_ =/ _/ on _)" [50,0,50] 50) where
    58 "f = g on X == \<forall> x \<in> X. f x = g x"
    59 
    60 lemma aval_eq_if_eq_on_vars[simp]:
    61   "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
    62 apply(induction a)
    63 apply simp_all
    64 done
    65 
    66 lemma bval_eq_if_eq_on_vars:
    67   "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
    68 proof(induction b)
    69   case (Less a1 a2)
    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
    71   thus ?case by simp
    72 qed simp_all
    73 
    74 end