src/HOL/IMP/Sem_Equiv.thy
changeset 44070 cebb7abb54b1
child 44261 e44f465c00a1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Mon Aug 08 16:47:55 2011 +0200
     1.3 @@ -0,0 +1,165 @@
     1.4 +header "Semantic Equivalence up to a Condition"
     1.5 +
     1.6 +theory Sem_Equiv
     1.7 +imports Hoare_Sound_Complete
     1.8 +begin
     1.9 +
    1.10 +definition
    1.11 +  equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
    1.12 +where
    1.13 +  "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
    1.14 +
    1.15 +definition 
    1.16 +  bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
    1.17 +where 
    1.18 +  "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
    1.19 +
    1.20 +lemma equiv_up_to_True:
    1.21 +  "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')"
    1.22 +  by (simp add: equiv_def equiv_up_to_def)
    1.23 +
    1.24 +lemma equiv_up_to_weaken:
    1.25 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'"
    1.26 +  by (simp add: equiv_up_to_def)
    1.27 +
    1.28 +lemma equiv_up_toI:
    1.29 +  "(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'"
    1.30 +  by (unfold equiv_up_to_def) blast
    1.31 +
    1.32 +lemma equiv_up_toD1:
    1.33 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
    1.34 +  by (unfold equiv_up_to_def) blast
    1.35 +
    1.36 +lemma equiv_up_toD2:
    1.37 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
    1.38 +  by (unfold equiv_up_to_def) blast
    1.39 +
    1.40 +
    1.41 +lemma equiv_up_to_refl [simp, intro!]:
    1.42 +  "P \<Turnstile> c \<sim> c"
    1.43 +  by (auto simp: equiv_up_to_def)
    1.44 +
    1.45 +lemma equiv_up_to_sym:
    1.46 +  "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
    1.47 +  by (auto simp: equiv_up_to_def)
    1.48 +
    1.49 +lemma equiv_up_to_trans [trans]:
    1.50 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
    1.51 +  by (auto simp: equiv_up_to_def)
    1.52 +
    1.53 +
    1.54 +lemma bequiv_up_to_refl [simp, intro!]:
    1.55 +  "P \<Turnstile> b <\<sim>> b"
    1.56 +  by (auto simp: bequiv_up_to_def)
    1.57 +
    1.58 +lemma bequiv_up_to_sym:
    1.59 +  "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
    1.60 +  by (auto simp: bequiv_up_to_def)
    1.61 +
    1.62 +lemma bequiv_up_to_trans [trans]:
    1.63 +  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
    1.64 +  by (auto simp: bequiv_up_to_def)
    1.65 +
    1.66 +
    1.67 +lemma equiv_up_to_hoare:
    1.68 +  "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
    1.69 +  unfolding hoare_valid_def equiv_up_to_def by blast
    1.70 +
    1.71 +lemma equiv_up_to_hoare_eq:
    1.72 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
    1.73 +  by (rule equiv_up_to_hoare)
    1.74 +
    1.75 +
    1.76 +lemma equiv_up_to_semi:
    1.77 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
    1.78 +  P \<Turnstile> (c; d) \<sim> (c'; d')"
    1.79 +  by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
    1.80 +
    1.81 +lemma equiv_up_to_while_lemma:
    1.82 +  shows "(d,s) \<Rightarrow> s' \<Longrightarrow> 
    1.83 +         P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
    1.84 +         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
    1.85 +         \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
    1.86 +         P s \<Longrightarrow> 
    1.87 +         d = WHILE b DO c \<Longrightarrow> 
    1.88 +         (WHILE b' DO c', s) \<Rightarrow> s'"  
    1.89 +proof (induct rule: big_step_induct)
    1.90 +  case (WhileTrue b s1 c s2 s3)
    1.91 +  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
    1.92 +  
    1.93 +  from WhileTrue.prems
    1.94 +  have "P \<Turnstile> b <\<sim>> b'" by simp
    1.95 +  with `bval b s1` `P s1`
    1.96 +  have "bval b' s1" by (simp add: bequiv_up_to_def)
    1.97 +  moreover
    1.98 +  from WhileTrue.prems
    1.99 +  have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
   1.100 +  with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
   1.101 +  have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
   1.102 +  moreover
   1.103 +  from WhileTrue.prems
   1.104 +  have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
   1.105 +  with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
   1.106 +  have "P s2" by (simp add: hoare_valid_def)
   1.107 +  hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
   1.108 +  ultimately 
   1.109 +  show ?case by blast
   1.110 +next
   1.111 +  case WhileFalse
   1.112 +  thus ?case by (auto simp: bequiv_up_to_def)
   1.113 +qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
   1.114 +
   1.115 +lemma bequiv_context_subst:
   1.116 +  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
   1.117 +  by (auto simp: bequiv_up_to_def)
   1.118 +
   1.119 +lemma equiv_up_to_while:
   1.120 +  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
   1.121 +   \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
   1.122 +   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
   1.123 +  apply (safe intro!: equiv_up_toI)
   1.124 +   apply (auto intro: equiv_up_to_while_lemma)[1]
   1.125 +  apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
   1.126 +  apply (drule equiv_up_to_sym [THEN iffD1])
   1.127 +  apply (drule bequiv_up_to_sym [THEN iffD1])
   1.128 +  apply (auto intro: equiv_up_to_while_lemma)[1]
   1.129 +  done
   1.130 +
   1.131 +lemma equiv_up_to_while_weak:
   1.132 +  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> 
   1.133 +   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
   1.134 +  by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken 
   1.135 +               simp: hoare_valid_def)
   1.136 +
   1.137 +lemma equiv_up_to_if:
   1.138 +  "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>
   1.139 +   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
   1.140 +  by (auto simp: bequiv_up_to_def equiv_up_to_def)
   1.141 +
   1.142 +lemma equiv_up_to_if_weak:
   1.143 +  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
   1.144 +   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
   1.145 +  by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
   1.146 +
   1.147 +lemma equiv_up_to_if_True [intro!]:
   1.148 +  "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
   1.149 +  by (auto simp: equiv_up_to_def) 
   1.150 +
   1.151 +lemma equiv_up_to_if_False [intro!]:
   1.152 +  "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
   1.153 +  by (auto simp: equiv_up_to_def)
   1.154 +
   1.155 +lemma equiv_up_to_while_False [intro!]:
   1.156 +  "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
   1.157 +  by (auto simp: equiv_up_to_def)
   1.158 +
   1.159 +lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
   1.160 + by (induct rule: big_step_induct) auto
   1.161 +  
   1.162 +lemma equiv_up_to_while_True [intro!,simp]:
   1.163 +  "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
   1.164 +  unfolding equiv_up_to_def
   1.165 +  by (blast dest: while_never)
   1.166 +
   1.167 +
   1.168 +end
   1.169 \ No newline at end of file