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