author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45218  f115540543d8 
child 47818  151d137f1095 
permissions  rwrr 
44070  1 
header "Semantic Equivalence up to a Condition" 
2 

3 
theory Sem_Equiv 

4 
imports Hoare_Sound_Complete 

5 
begin 

6 

7 
definition 

8 
equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60) 

9 
where 

10 
"P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'" 

11 

12 
definition 

13 
bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60) 

14 
where 

15 
"P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s" 

16 

17 
lemma equiv_up_to_True: 

18 
"((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')" 

19 
by (simp add: equiv_def equiv_up_to_def) 

20 

21 
lemma equiv_up_to_weaken: 

22 
"P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'" 

23 
by (simp add: equiv_up_to_def) 

24 

25 
lemma equiv_up_toI: 

26 
"(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'" 

27 
by (unfold equiv_up_to_def) blast 

28 

29 
lemma equiv_up_toD1: 

30 
"P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'" 

31 
by (unfold equiv_up_to_def) blast 

32 

33 
lemma equiv_up_toD2: 

34 
"P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'" 

35 
by (unfold equiv_up_to_def) blast 

36 

37 

38 
lemma equiv_up_to_refl [simp, intro!]: 

39 
"P \<Turnstile> c \<sim> c" 

40 
by (auto simp: equiv_up_to_def) 

41 

42 
lemma equiv_up_to_sym: 

43 
"(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)" 

44 
by (auto simp: equiv_up_to_def) 

45 

45218  46 
lemma equiv_up_to_trans: 
44070  47 
"P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''" 
48 
by (auto simp: equiv_up_to_def) 

49 

50 

51 
lemma bequiv_up_to_refl [simp, intro!]: 

52 
"P \<Turnstile> b <\<sim>> b" 

53 
by (auto simp: bequiv_up_to_def) 

54 

55 
lemma bequiv_up_to_sym: 

56 
"(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)" 

57 
by (auto simp: bequiv_up_to_def) 

58 

45218  59 
lemma bequiv_up_to_trans: 
44070  60 
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''" 
61 
by (auto simp: bequiv_up_to_def) 

62 

63 

64 
lemma equiv_up_to_hoare: 

65 
"P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})" 

66 
unfolding hoare_valid_def equiv_up_to_def by blast 

67 

68 
lemma equiv_up_to_hoare_eq: 

69 
"P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})" 

70 
by (rule equiv_up_to_hoare) 

71 

72 

73 
lemma equiv_up_to_semi: 

74 
"P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> 

75 
P \<Turnstile> (c; d) \<sim> (c'; d')" 

76 
by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast 

77 

78 
lemma equiv_up_to_while_lemma: 

79 
shows "(d,s) \<Rightarrow> s' \<Longrightarrow> 

80 
P \<Turnstile> b <\<sim>> b' \<Longrightarrow> 

81 
(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 

82 
\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 

83 
P s \<Longrightarrow> 

84 
d = WHILE b DO c \<Longrightarrow> 

85 
(WHILE b' DO c', s) \<Rightarrow> s'" 

45015  86 
proof (induction rule: big_step_induct) 
44070  87 
case (WhileTrue b s1 c s2 s3) 
45015  88 
note IH = WhileTrue.IH(2) [OF WhileTrue.prems(13) _ WhileTrue.prems(5)] 
44070  89 
from WhileTrue.prems 
90 
have "P \<Turnstile> b <\<sim>> b'" by simp 

91 
with `bval b s1` `P s1` 

92 
have "bval b' s1" by (simp add: bequiv_up_to_def) 

93 
moreover 

94 
from WhileTrue.prems 

95 
have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp 

96 
with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2` 

97 
have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def) 

98 
moreover 

99 
from WhileTrue.prems 

100 
have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp 

101 
with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2` 

102 
have "P s2" by (simp add: hoare_valid_def) 

103 
hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH) 

104 
ultimately 

105 
show ?case by blast 

106 
next 

107 
case WhileFalse 

108 
thus ?case by (auto simp: bequiv_up_to_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44261
diff
changeset

109 
qed (fastforce simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+ 
44070  110 

111 
lemma bequiv_context_subst: 

112 
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)" 

113 
by (auto simp: bequiv_up_to_def) 

114 

115 
lemma equiv_up_to_while: 

116 
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 

117 
\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 

118 
P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'" 

119 
apply (safe intro!: equiv_up_toI) 

120 
apply (auto intro: equiv_up_to_while_lemma)[1] 

121 
apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst) 

122 
apply (drule equiv_up_to_sym [THEN iffD1]) 

123 
apply (drule bequiv_up_to_sym [THEN iffD1]) 

124 
apply (auto intro: equiv_up_to_while_lemma)[1] 

125 
done 

126 

127 
lemma equiv_up_to_while_weak: 

128 
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> 

129 
P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44261
diff
changeset

130 
by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken 
44070  131 
simp: hoare_valid_def) 
132 

133 
lemma equiv_up_to_if: 

44261  134 
"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> 
44070  135 
P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'" 
136 
by (auto simp: bequiv_up_to_def equiv_up_to_def) 

137 

138 
lemma equiv_up_to_if_weak: 

139 
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow> 

140 
P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44261
diff
changeset

141 
by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken) 
44070  142 

143 
lemma equiv_up_to_if_True [intro!]: 

144 
"(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1" 

145 
by (auto simp: equiv_up_to_def) 

146 

147 
lemma equiv_up_to_if_False [intro!]: 

148 
"(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2" 

149 
by (auto simp: equiv_up_to_def) 

150 

151 
lemma equiv_up_to_while_False [intro!]: 

152 
"(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP" 

153 
by (auto simp: equiv_up_to_def) 

154 

45200  155 
lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'" 
44070  156 
by (induct rule: big_step_induct) auto 
157 

158 
lemma equiv_up_to_while_True [intro!,simp]: 

45200  159 
"P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP" 
44070  160 
unfolding equiv_up_to_def 
161 
by (blast dest: while_never) 

162 

163 

44261  164 
end 