src/HOL/IMP/Sem_Equiv.thy
author kleing
Mon Aug 08 16:47:55 2011 +0200 (2011-08-08)
changeset 44070 cebb7abb54b1
child 44261 e44f465c00a1
permissions -rw-r--r--
import constant folding theory into IMP
kleing@44070
     1
header "Semantic Equivalence up to a Condition"
kleing@44070
     2
kleing@44070
     3
theory Sem_Equiv
kleing@44070
     4
imports Hoare_Sound_Complete
kleing@44070
     5
begin
kleing@44070
     6
kleing@44070
     7
definition
kleing@44070
     8
  equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
kleing@44070
     9
where
kleing@44070
    10
  "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
kleing@44070
    11
kleing@44070
    12
definition 
kleing@44070
    13
  bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
kleing@44070
    14
where 
kleing@44070
    15
  "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
kleing@44070
    16
kleing@44070
    17
lemma equiv_up_to_True:
kleing@44070
    18
  "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')"
kleing@44070
    19
  by (simp add: equiv_def equiv_up_to_def)
kleing@44070
    20
kleing@44070
    21
lemma equiv_up_to_weaken:
kleing@44070
    22
  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'"
kleing@44070
    23
  by (simp add: equiv_up_to_def)
kleing@44070
    24
kleing@44070
    25
lemma equiv_up_toI:
kleing@44070
    26
  "(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'"
kleing@44070
    27
  by (unfold equiv_up_to_def) blast
kleing@44070
    28
kleing@44070
    29
lemma equiv_up_toD1:
kleing@44070
    30
  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
kleing@44070
    31
  by (unfold equiv_up_to_def) blast
kleing@44070
    32
kleing@44070
    33
lemma equiv_up_toD2:
kleing@44070
    34
  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
kleing@44070
    35
  by (unfold equiv_up_to_def) blast
kleing@44070
    36
kleing@44070
    37
kleing@44070
    38
lemma equiv_up_to_refl [simp, intro!]:
kleing@44070
    39
  "P \<Turnstile> c \<sim> c"
kleing@44070
    40
  by (auto simp: equiv_up_to_def)
kleing@44070
    41
kleing@44070
    42
lemma equiv_up_to_sym:
kleing@44070
    43
  "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
kleing@44070
    44
  by (auto simp: equiv_up_to_def)
kleing@44070
    45
kleing@44070
    46
lemma equiv_up_to_trans [trans]:
kleing@44070
    47
  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
kleing@44070
    48
  by (auto simp: equiv_up_to_def)
kleing@44070
    49
kleing@44070
    50
kleing@44070
    51
lemma bequiv_up_to_refl [simp, intro!]:
kleing@44070
    52
  "P \<Turnstile> b <\<sim>> b"
kleing@44070
    53
  by (auto simp: bequiv_up_to_def)
kleing@44070
    54
kleing@44070
    55
lemma bequiv_up_to_sym:
kleing@44070
    56
  "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
kleing@44070
    57
  by (auto simp: bequiv_up_to_def)
kleing@44070
    58
kleing@44070
    59
lemma bequiv_up_to_trans [trans]:
kleing@44070
    60
  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
kleing@44070
    61
  by (auto simp: bequiv_up_to_def)
kleing@44070
    62
kleing@44070
    63
kleing@44070
    64
lemma equiv_up_to_hoare:
kleing@44070
    65
  "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
kleing@44070
    66
  unfolding hoare_valid_def equiv_up_to_def by blast
kleing@44070
    67
kleing@44070
    68
lemma equiv_up_to_hoare_eq:
kleing@44070
    69
  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
kleing@44070
    70
  by (rule equiv_up_to_hoare)
kleing@44070
    71
kleing@44070
    72
kleing@44070
    73
lemma equiv_up_to_semi:
kleing@44070
    74
  "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
kleing@44070
    75
  P \<Turnstile> (c; d) \<sim> (c'; d')"
kleing@44070
    76
  by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
kleing@44070
    77
kleing@44070
    78
lemma equiv_up_to_while_lemma:
kleing@44070
    79
  shows "(d,s) \<Rightarrow> s' \<Longrightarrow> 
kleing@44070
    80
         P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
kleing@44070
    81
         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
kleing@44070
    82
         \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
kleing@44070
    83
         P s \<Longrightarrow> 
kleing@44070
    84
         d = WHILE b DO c \<Longrightarrow> 
kleing@44070
    85
         (WHILE b' DO c', s) \<Rightarrow> s'"  
kleing@44070
    86
proof (induct rule: big_step_induct)
kleing@44070
    87
  case (WhileTrue b s1 c s2 s3)
kleing@44070
    88
  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
kleing@44070
    89
  
kleing@44070
    90
  from WhileTrue.prems
kleing@44070
    91
  have "P \<Turnstile> b <\<sim>> b'" by simp
kleing@44070
    92
  with `bval b s1` `P s1`
kleing@44070
    93
  have "bval b' s1" by (simp add: bequiv_up_to_def)
kleing@44070
    94
  moreover
kleing@44070
    95
  from WhileTrue.prems
kleing@44070
    96
  have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
kleing@44070
    97
  with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
kleing@44070
    98
  have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
kleing@44070
    99
  moreover
kleing@44070
   100
  from WhileTrue.prems
kleing@44070
   101
  have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
kleing@44070
   102
  with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
kleing@44070
   103
  have "P s2" by (simp add: hoare_valid_def)
kleing@44070
   104
  hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
kleing@44070
   105
  ultimately 
kleing@44070
   106
  show ?case by blast
kleing@44070
   107
next
kleing@44070
   108
  case WhileFalse
kleing@44070
   109
  thus ?case by (auto simp: bequiv_up_to_def)
kleing@44070
   110
qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
kleing@44070
   111
kleing@44070
   112
lemma bequiv_context_subst:
kleing@44070
   113
  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
kleing@44070
   114
  by (auto simp: bequiv_up_to_def)
kleing@44070
   115
kleing@44070
   116
lemma equiv_up_to_while:
kleing@44070
   117
  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
kleing@44070
   118
   \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
kleing@44070
   119
   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
kleing@44070
   120
  apply (safe intro!: equiv_up_toI)
kleing@44070
   121
   apply (auto intro: equiv_up_to_while_lemma)[1]
kleing@44070
   122
  apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
kleing@44070
   123
  apply (drule equiv_up_to_sym [THEN iffD1])
kleing@44070
   124
  apply (drule bequiv_up_to_sym [THEN iffD1])
kleing@44070
   125
  apply (auto intro: equiv_up_to_while_lemma)[1]
kleing@44070
   126
  done
kleing@44070
   127
kleing@44070
   128
lemma equiv_up_to_while_weak:
kleing@44070
   129
  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> 
kleing@44070
   130
   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
kleing@44070
   131
  by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken 
kleing@44070
   132
               simp: hoare_valid_def)
kleing@44070
   133
kleing@44070
   134
lemma equiv_up_to_if:
kleing@44070
   135
  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
kleing@44070
   136
   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
kleing@44070
   137
  by (auto simp: bequiv_up_to_def equiv_up_to_def)
kleing@44070
   138
kleing@44070
   139
lemma equiv_up_to_if_weak:
kleing@44070
   140
  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
kleing@44070
   141
   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
kleing@44070
   142
  by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
kleing@44070
   143
kleing@44070
   144
lemma equiv_up_to_if_True [intro!]:
kleing@44070
   145
  "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
kleing@44070
   146
  by (auto simp: equiv_up_to_def) 
kleing@44070
   147
kleing@44070
   148
lemma equiv_up_to_if_False [intro!]:
kleing@44070
   149
  "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
kleing@44070
   150
  by (auto simp: equiv_up_to_def)
kleing@44070
   151
kleing@44070
   152
lemma equiv_up_to_while_False [intro!]:
kleing@44070
   153
  "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
kleing@44070
   154
  by (auto simp: equiv_up_to_def)
kleing@44070
   155
kleing@44070
   156
lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
kleing@44070
   157
 by (induct rule: big_step_induct) auto
kleing@44070
   158
  
kleing@44070
   159
lemma equiv_up_to_while_True [intro!,simp]:
kleing@44070
   160
  "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
kleing@44070
   161
  unfolding equiv_up_to_def
kleing@44070
   162
  by (blast dest: while_never)
kleing@44070
   163
kleing@44070
   164
kleing@44070
   165
end