src/HOL/IMP/Vars.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45774 9b11989f38b0
child 49972 f11f8905d9fd
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
header "Definite Assignment Analysis"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
45716
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
     5
theory Vars imports BExp
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
45716
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
     8
subsection "Show sets of variables as lists"
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
     9
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    10
text {* Sets may be infinite and are not always displayed by element 
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    11
  if computed as values. Lists do not have this problem. 
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    12
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    13
  We define a function @{text show} that converts a set of
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    14
  variable names into a list. To keep things simple, we rely on
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    15
  the convention that we only use single letter names.
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    16
*}
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    17
definition 
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    18
  letters :: "string list" where
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    19
  "letters = map (\<lambda>c. [c]) chars"
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    20
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    21
definition 
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    22
  "show" :: "string set \<Rightarrow> string list" where
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    23
  "show S = filter (\<lambda>x. x \<in> S) letters" 
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    24
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    25
value "show {''x'', ''z''}"
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45212
diff changeset
    26
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
subsection "The Variables in an Expression"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
text{* We need to collect the variables in both arithmetic and boolean
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
expressions. For a change we do not introduce two functions, e.g.\ @{text
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
avars} and @{text bvars}, but we overload the name @{text vars}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
via a \emph{type class}, a device that originated with Haskell: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
 
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
class vars =
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45200
diff changeset
    35
fixes vars :: "'a \<Rightarrow> vname set"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
text{* This defines a type class ``vars'' with a single
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
function of (coincidentally) the same name. Then we define two separated
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
instances of the class, one for @{typ aexp} and one for @{typ bexp}: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
instantiation aexp :: vars
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45200
diff changeset
    44
fun vars_aexp :: "aexp \<Rightarrow> vname set" where
45774
nipkow
parents: 45716
diff changeset
    45
"vars (N n) = {}" |
nipkow
parents: 45716
diff changeset
    46
"vars (V x) = {x}" |
nipkow
parents: 45716
diff changeset
    47
"vars (Plus a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
instance ..
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    51
end
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    52
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
value "vars(Plus (V ''x'') (V ''y''))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
text{* We need to convert functions to lists before we can view them: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
value "show  (vars(Plus (V ''x'') (V ''y'')))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    58
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    59
instantiation bexp :: vars
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    60
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    61
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45200
diff changeset
    62
fun vars_bexp :: "bexp \<Rightarrow> vname set" where
45774
nipkow
parents: 45716
diff changeset
    63
"vars (Bc v) = {}" |
nipkow
parents: 45716
diff changeset
    64
"vars (Not b) = vars b" |
nipkow
parents: 45716
diff changeset
    65
"vars (And b\<^isub>1 b\<^isub>2) = vars b\<^isub>1 \<union> vars b\<^isub>2" |
nipkow
parents: 45716
diff changeset
    66
"vars (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
instance ..
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
end
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    71
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
value "show  (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
abbreviation
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    75
  eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    76
 ("(_ =/ _/ on _)" [50,0,50] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
"f = g on X == \<forall> x \<in> X. f x = g x"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    78
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    79
lemma aval_eq_if_eq_on_vars[simp]:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    80
  "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    81
apply(induction a)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    82
apply simp_all
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    83
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    84
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    85
lemma bval_eq_if_eq_on_vars:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    86
  "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    87
proof(induction b)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    88
  case (Less a1 a2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    89
  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
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    90
  thus ?case by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    91
qed simp_all
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    92
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    93
end