src/HOL/IMP/Sem_Equiv.thy
changeset 48909 b2dea007e55e
parent 47818 151d137f1095
child 52021 59963cda805a
     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