src/HOL/IMP/Live.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45784 ddac6eb800c6
child 47818 151d137f1095
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 "Live Variable Analysis"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
theory Live imports Vars Big_Step
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
subsection "Liveness Analysis"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45015
diff changeset
    10
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    11
"L SKIP X = X" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    12
"L (x ::= a) X = X-{x} \<union> vars a" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    14
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45015
diff changeset
    21
fun "kill" :: "com \<Rightarrow> vname set" where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
"kill SKIP = {}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
"kill (x ::= a) = {x}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
"kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
"kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
"kill (WHILE b DO c) = {}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45015
diff changeset
    28
fun gen :: "com \<Rightarrow> vname set" where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
"gen SKIP = {}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
"gen (x ::= a) = vars a" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
"gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
"gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
"gen (WHILE b DO c) = vars b \<union> gen c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
by(induct c arbitrary:X) auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
45771
a70465244096 added lemmas
nipkow
parents: 45770
diff changeset
    38
lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
by(auto simp add:L_gen_kill)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
45771
a70465244096 added lemmas
nipkow
parents: 45770
diff changeset
    41
lemma L_While_lpfp:
45784
nipkow
parents: 45771
diff changeset
    42
  "vars b \<union> X \<union> L c P \<subseteq> P \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
45771
a70465244096 added lemmas
nipkow
parents: 45770
diff changeset
    43
by(simp add: L_gen_kill)
a70465244096 added lemmas
nipkow
parents: 45770
diff changeset
    44
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
subsection "Soundness"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    47
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
theorem L_sound:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
    51
proof (induction arbitrary: X t rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    52
  case Skip then show ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
  case Assign then show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
    by (auto simp: ball_Un)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
  case (Semi c1 s1 s2 c2 s3 X t1)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
    58
  from Semi.IH(1) Semi.prems obtain t2 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    59
    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    60
    by simp blast
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
    61
  from Semi.IH(2)[OF s2t2] obtain t3 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    62
    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    63
    by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    64
  show ?case using t12 t23 s3t3 by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    66
  case (IfTrue b s c1 s' c2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
  hence "s = t on vars b" "s = t on L c1 X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
    "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    71
  thus ?case using `bval b t` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
  case (IfFalse b s c2 s' c1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
  hence "s = t on vars b" "s = t on L c2 X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    75
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    76
  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
    "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    78
  thus ?case using `~bval b t` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    79
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    80
  case (WhileFalse b s c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    81
  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
45770
5d35cb2c0f02 tuned proof
nipkow
parents: 45212
diff changeset
    82
  thus ?case using WhileFalse.prems by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    83
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    84
  case (WhileTrue b s1 c s2 s3 X t1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    85
  let ?w = "WHILE b DO c"
45770
5d35cb2c0f02 tuned proof
nipkow
parents: 45212
diff changeset
    86
  from `bval b s1` WhileTrue.prems have "bval b t1"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    87
    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
45771
a70465244096 added lemmas
nipkow
parents: 45770
diff changeset
    88
  have "s1 = t1 on L c (L ?w X)" using  L_While_pfp WhileTrue.prems
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    89
    by (blast)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
    90
  from WhileTrue.IH(1)[OF this] obtain t2 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    91
    "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
    92
  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    93
    by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    94
  with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    95
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    96
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    97
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    98
subsection "Program Optimization"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    99
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   100
text{* Burying assignments to dead variables: *}
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45015
diff changeset
   101
fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   102
"bury SKIP X = SKIP" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   103
"bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   104
"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   105
"bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   106
"bury (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   107
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   108
text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   109
proof would be very similar. However, we phrase it as a semantics
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   110
preservation property: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   111
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   112
theorem bury_sound:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   113
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   114
  \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   115
proof (induction arbitrary: X t rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   116
  case Skip then show ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   117
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   118
  case Assign then show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   119
    by (auto simp: ball_Un)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   120
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   121
  case (Semi c1 s1 s2 c2 s3 X t1)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   122
  from Semi.IH(1) Semi.prems obtain t2 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   123
    t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   124
    by simp blast
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   125
  from Semi.IH(2)[OF s2t2] obtain t3 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   126
    t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   127
    by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   128
  show ?case using t12 t23 s3t3 by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   129
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   130
  case (IfTrue b s c1 s' c2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   131
  hence "s = t on vars b" "s = t on L c1 X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   132
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   133
  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   134
    "(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   135
  thus ?case using `bval b t` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   136
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   137
  case (IfFalse b s c2 s' c1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   138
  hence "s = t on vars b" "s = t on L c2 X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   139
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   140
  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   141
    "(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   142
  thus ?case using `~bval b t` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   143
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   144
  case (WhileFalse b s c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   145
  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
45770
5d35cb2c0f02 tuned proof
nipkow
parents: 45212
diff changeset
   146
  thus ?case using WhileFalse.prems by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   147
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   148
  case (WhileTrue b s1 c s2 s3 X t1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   149
  let ?w = "WHILE b DO c"
45770
5d35cb2c0f02 tuned proof
nipkow
parents: 45212
diff changeset
   150
  from `bval b s1` WhileTrue.prems have "bval b t1"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   151
    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   152
  have "s1 = t1 on L c (L ?w X)"
45771
a70465244096 added lemmas
nipkow
parents: 45770
diff changeset
   153
    using L_While_pfp WhileTrue.prems by blast
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   154
  from WhileTrue.IH(1)[OF this] obtain t2 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   155
    "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   156
  from WhileTrue.IH(2)[OF this(2)] obtain t3
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   157
    where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   158
    by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   159
  with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   160
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   161
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   162
corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   163
using bury_sound[of c s s' UNIV]
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   164
by (auto simp: fun_eq_iff[symmetric])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   165
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   166
text{* Now the opposite direction. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   167
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   168
lemma SKIP_bury[simp]:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   169
  "SKIP = bury c X \<longleftrightarrow> c = SKIP | (EX x a. c = x::=a & x \<notin> X)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   170
by (cases c) auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   171
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   172
lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   173
by (cases c) auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   174
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   175
lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   176
  (EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   177
by (cases c) auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   178
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   179
lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   180
  (EX c1 c2. c = IF b THEN c1 ELSE c2 &
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   181
     bc1 = bury c1 X & bc2 = bury c2 X)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   182
by (cases c) auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   183
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   184
lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   185
  (EX c'. c = WHILE b DO c' & bc' = bury c' (vars b \<union> X \<union> L c X))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   186
by (cases c) auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   187
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   188
theorem bury_sound2:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   189
  "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   190
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   191
proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   192
  case Skip then show ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   193
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   194
  case Assign then show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   195
    by (auto simp: ball_Un)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   196
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   197
  case (Semi bc1 s1 s2 bc2 s3 c X t1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   198
  then obtain c1 c2 where c: "c = c1;c2"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   199
    and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   200
  note IH = Semi.hyps(2,4)
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   201
  from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   202
    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   203
  from IH(2)[OF bc2 s2t2] obtain t3 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   204
    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   205
    by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   206
  show ?case using c t12 t23 s3t3 by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   207
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   208
  case (IfTrue b s bc1 s' bc2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   209
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   210
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   211
  have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   212
  from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   213
  note IH = IfTrue.hyps(3)
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   214
  from IH[OF bc1 `s = t on L c1 X`] obtain t' where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   215
    "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   216
  thus ?case using c `bval b t` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   217
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   218
  case (IfFalse b s bc2 s' bc1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   219
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   220
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   221
  have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   222
  from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   223
  note IH = IfFalse.hyps(3)
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   224
  from IH[OF bc2 `s = t on L c2 X`] obtain t' where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   225
    "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   226
  thus ?case using c `~bval b t` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   227
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   228
  case (WhileFalse b s c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   229
  hence "~ bval b t" by (auto simp: ball_Un dest: bval_eq_if_eq_on_vars)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   230
  thus ?case using WhileFalse by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   231
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   232
  case (WhileTrue b s1 bc' s2 s3 c X t1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   233
  then obtain c' where c: "c = WHILE b DO c'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   234
    and bc': "bc' = bury c' (vars b \<union> X \<union> L c' X)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   235
  let ?w = "WHILE b DO c'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   236
  from `bval b s1` WhileTrue.prems c have "bval b t1"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   237
    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   238
  note IH = WhileTrue.hyps(3,5)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   239
  have "s1 = t1 on L c' (L ?w X)"
45771
a70465244096 added lemmas
nipkow
parents: 45770
diff changeset
   240
    using L_While_pfp WhileTrue.prems c by blast
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   241
  with IH(1)[OF bc', of t1] obtain t2 where
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   242
    "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   243
  from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   244
    where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   245
    by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   246
  with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   247
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   248
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   249
corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   250
using bury_sound2[of c UNIV]
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   251
by (auto simp: fun_eq_iff[symmetric])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   252
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   253
corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   254
by(metis final_bury_sound final_bury_sound2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   255
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   256
end