src/HOL/IMP/Live.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35802 362431732b5e
child 39198 f967a16dfcdd
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
nipkow@28583
     1
theory Live imports Natural
nipkow@28583
     2
begin
nipkow@28583
     3
nipkow@28583
     4
text{* Which variables/locations does an expression depend on?
nipkow@28583
     5
Any set of variables that completely determine the value of the expression,
nipkow@28583
     6
in the worst case all locations: *}
nipkow@28583
     7
nipkow@28583
     8
consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
nipkow@28583
     9
specification (Dep)
nipkow@28583
    10
dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t"
nipkow@28583
    11
by(rule_tac x="%x. UNIV" in exI)(simp add: expand_fun_eq[symmetric])
nipkow@28583
    12
nipkow@28583
    13
text{* The following definition of @{const Dep} looks very tempting
nipkow@28583
    14
@{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
nipkow@28583
    15
but does not work in case @{text e} depends on an infinite set of variables.
nipkow@28583
    16
For example, if @{term"e s"} tests if @{text s} is 0 at infinitely many locations. Then @{term"Dep e"} incorrectly yields the empty set!
nipkow@28583
    17
nipkow@28583
    18
If we had a concrete representation of expressions, we would simply write
nipkow@28583
    19
a recursive free-variables function.
nipkow@28583
    20
*}
nipkow@28583
    21
nipkow@28583
    22
primrec L :: "com \<Rightarrow> loc set \<Rightarrow> loc set" where
nipkow@28583
    23
"L SKIP A = A" |
nipkow@28583
    24
"L (x :== e) A = A-{x} \<union> Dep e" |
nipkow@28583
    25
"L (c1; c2) A = (L c1 \<circ> L c2) A" |
nipkow@28583
    26
"L (IF b THEN c1 ELSE c2) A = Dep b \<union> L c1 A \<union> L c2 A" |
nipkow@28583
    27
"L (WHILE b DO c) A = Dep b \<union> A \<union> L c A"
nipkow@28583
    28
nipkow@28583
    29
primrec "kill" :: "com \<Rightarrow> loc set" where
nipkow@28583
    30
"kill SKIP = {}" |
nipkow@28583
    31
"kill (x :== e) = {x}" |
nipkow@28583
    32
"kill (c1; c2) = kill c1 \<union> kill c2" |
nipkow@28583
    33
"kill (IF b THEN c1 ELSE c2) = Dep b \<union> kill c1 \<inter>  kill c2" |
nipkow@28583
    34
"kill (WHILE b DO c) = {}"
nipkow@28583
    35
nipkow@28583
    36
primrec gen :: "com \<Rightarrow> loc set" where
nipkow@28583
    37
"gen SKIP = {}" |
nipkow@28583
    38
"gen (x :== e) = Dep e" |
nipkow@28583
    39
"gen (c1; c2) = gen c1 \<union> (gen c2-kill c1)" |
nipkow@28583
    40
"gen (IF b THEN c1 ELSE c2) = Dep b \<union> gen c1 \<union> gen c2" |
nipkow@28583
    41
"gen (WHILE b DO c) = Dep b \<union> gen c"
nipkow@28583
    42
nipkow@28583
    43
lemma L_gen_kill: "L c A = gen c \<union> (A - kill c)"
nipkow@28583
    44
by(induct c arbitrary:A) auto
nipkow@28583
    45
nipkow@28583
    46
lemma L_idemp: "L c (L c A) \<subseteq> L c A"
nipkow@28583
    47
by(fastsimp simp add:L_gen_kill)
nipkow@28583
    48
nipkow@28583
    49
theorem L_sound: "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
nipkow@28583
    50
 \<forall>x\<in>A. s' x = t' x"
nipkow@28583
    51
proof (induct c arbitrary: A s t s' t')
nipkow@28583
    52
  case SKIP then show ?case by auto
nipkow@28583
    53
next
nipkow@28583
    54
  case (Assign x e) then show ?case
nipkow@28583
    55
    by (auto simp:update_def ball_Un dest!: dep_on)
nipkow@28583
    56
next
nipkow@28583
    57
  case (Semi c1 c2)
nipkow@28583
    58
  from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
nipkow@28583
    59
    by auto
nipkow@28583
    60
  from Semi(5) obtain t'' where t1: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>c2,t''\<rangle> \<longrightarrow>\<^sub>c t'"
nipkow@28583
    61
    by auto
nipkow@28583
    62
  show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
nipkow@28583
    63
next
nipkow@28583
    64
  case (Cond b c1 c2)
nipkow@28583
    65
  show ?case
nipkow@28583
    66
  proof cases
nipkow@28583
    67
    assume "b s"
nipkow@28583
    68
    hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
nipkow@28583
    69
    have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
nipkow@28583
    70
    hence t: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
nipkow@28583
    71
    show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
nipkow@28583
    72
  next
nipkow@28583
    73
    assume "\<not> b s"
nipkow@28583
    74
    hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
nipkow@28583
    75
    have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
nipkow@28583
    76
    hence t: "\<langle>c2,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
nipkow@28583
    77
    show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
nipkow@28583
    78
  qed
nipkow@28583
    79
next
nipkow@28583
    80
  case (While b c) note IH = this
nipkow@28583
    81
  { fix cw
nipkow@28583
    82
    have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>cw,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
nipkow@28583
    83
          \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
nipkow@28583
    84
    proof (induct arbitrary: t A pred:evalc)
nipkow@28583
    85
      case WhileFalse
nipkow@28583
    86
      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
nipkow@28583
    87
      then have "t' = t" using WhileFalse by auto
nipkow@28583
    88
      then show ?case using WhileFalse by auto
nipkow@28583
    89
    next
nipkow@28583
    90
      case (WhileTrue _ s _ s'' s')
nipkow@28583
    91
      have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
nipkow@28583
    92
      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
nipkow@28583
    93
      then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
nipkow@28583
    94
        using WhileTrue(6,7) by auto
nipkow@28867
    95
      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
wenzelm@32960
    96
        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8)
wenzelm@32960
    97
        by (auto simp:L_gen_kill)
nipkow@35802
    98
      then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
nipkow@35802
    99
      then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
nipkow@28583
   100
    qed auto }
nipkow@35802
   101
-- "a terser version"
nipkow@35802
   102
  { let ?w = "While b c"
nipkow@35802
   103
    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>?w,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
nipkow@35802
   104
          \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
nipkow@35802
   105
    proof (induct ?w s s' arbitrary: t A pred:evalc)
nipkow@35802
   106
      case WhileFalse
nipkow@35802
   107
      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
nipkow@35802
   108
      then have "t' = t" using WhileFalse by auto
nipkow@35802
   109
      then show ?case using WhileFalse by simp
nipkow@35802
   110
    next
nipkow@35802
   111
      case (WhileTrue s s'' s')
nipkow@35802
   112
      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
nipkow@35802
   113
      then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
nipkow@35802
   114
        using WhileTrue(6,7) by auto
nipkow@35802
   115
      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
nipkow@35802
   116
        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(7)
nipkow@35802
   117
        by (auto simp:L_gen_kill)
nipkow@35802
   118
      then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
nipkow@35802
   119
      then show ?case using WhileTrue(5) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
nipkow@35802
   120
    qed }
nipkow@35802
   121
  from this[OF IH(3) IH(4,2)] show ?case by metis
nipkow@28583
   122
qed
nipkow@28583
   123
nipkow@28867
   124
nipkow@28867
   125
primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where
nipkow@28867
   126
"bury SKIP _ = SKIP" |
nipkow@28867
   127
"bury (x :== e) A = (if x:A then x:== e else SKIP)" |
nipkow@28867
   128
"bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" |
nipkow@28867
   129
"bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" |
nipkow@28867
   130
"bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))"
nipkow@28867
   131
nipkow@28867
   132
theorem bury_sound:
nipkow@28867
   133
  "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury c A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
nipkow@28867
   134
   \<forall>x\<in>A. s' x = t' x"
nipkow@28867
   135
proof (induct c arbitrary: A s t s' t')
nipkow@28867
   136
  case SKIP then show ?case by auto
nipkow@28867
   137
next
nipkow@28867
   138
  case (Assign x e) then show ?case
nipkow@28867
   139
    by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on)
nipkow@28867
   140
next
nipkow@28867
   141
  case (Semi c1 c2)
nipkow@28867
   142
  from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
nipkow@28867
   143
    by auto
nipkow@28867
   144
  from Semi(5) obtain t'' where t1: "\<langle>bury c1 (L c2 A),t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>bury c2 A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
nipkow@28867
   145
    by auto
nipkow@28867
   146
  show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
nipkow@28867
   147
next
nipkow@28867
   148
  case (Cond b c1 c2)
nipkow@28867
   149
  show ?case
nipkow@28867
   150
  proof cases
nipkow@28867
   151
    assume "b s"
nipkow@28867
   152
    hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
nipkow@28867
   153
    have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
nipkow@28867
   154
    hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
nipkow@28867
   155
    show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
nipkow@28867
   156
  next
nipkow@28867
   157
    assume "\<not> b s"
nipkow@28867
   158
    hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
nipkow@28867
   159
    have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
nipkow@28867
   160
    hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
nipkow@28867
   161
    show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
nipkow@28867
   162
  qed
nipkow@28867
   163
next
nipkow@28867
   164
  case (While b c) note IH = this
nipkow@28867
   165
  { fix cw
nipkow@28867
   166
    have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>bury cw A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
nipkow@28867
   167
          \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
nipkow@28867
   168
    proof (induct arbitrary: t A pred:evalc)
nipkow@28867
   169
      case WhileFalse
nipkow@28867
   170
      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
nipkow@28867
   171
      then have "t' = t" using WhileFalse by auto
nipkow@28867
   172
      then show ?case using WhileFalse by auto
nipkow@28867
   173
    next
nipkow@28867
   174
      case (WhileTrue _ s _ s'' s')
nipkow@28867
   175
      have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
nipkow@28867
   176
      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
nipkow@28867
   177
      then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
wenzelm@32960
   178
        and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
nipkow@28867
   179
        using WhileTrue(6,7) by auto
nipkow@28867
   180
      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
wenzelm@32960
   181
        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8)
wenzelm@32960
   182
        by (auto simp:L_gen_kill)
nipkow@28867
   183
      moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
nipkow@28867
   184
      ultimately show ?case
wenzelm@32960
   185
        using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
nipkow@28867
   186
    qed auto }
nipkow@35802
   187
  { let ?w = "While b c"
nipkow@35802
   188
    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury ?w A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
nipkow@35802
   189
          \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
nipkow@35802
   190
    proof (induct ?w s s' arbitrary: t A pred:evalc)
nipkow@35802
   191
      case WhileFalse
nipkow@35802
   192
      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
nipkow@35802
   193
      then have "t' = t" using WhileFalse by auto
nipkow@35802
   194
      then show ?case using WhileFalse by simp
nipkow@35802
   195
    next
nipkow@35802
   196
      case (WhileTrue s s'' s')
nipkow@35802
   197
      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
nipkow@35802
   198
      then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
nipkow@35802
   199
        and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
nipkow@35802
   200
        using WhileTrue(6,7) by auto
nipkow@35802
   201
      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
nipkow@35802
   202
        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(7)
nipkow@35802
   203
        by (auto simp:L_gen_kill)
nipkow@35802
   204
      then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
nipkow@35802
   205
      then show ?case
nipkow@35802
   206
        using WhileTrue(5) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
nipkow@35802
   207
    qed }
nipkow@35802
   208
  from this[OF IH(3) IH(4,2)] show ?case by metis
nipkow@28867
   209
qed
nipkow@28867
   210
nipkow@28867
   211
nipkow@28583
   212
end