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