equal
deleted
inserted
replaced
81 (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<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> |
82 \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> |
83 P s \<Longrightarrow> |
83 P s \<Longrightarrow> |
84 d = WHILE b DO c \<Longrightarrow> |
84 d = WHILE b DO c \<Longrightarrow> |
85 (WHILE b' DO c', s) \<Rightarrow> s'" |
85 (WHILE b' DO c', s) \<Rightarrow> s'" |
86 proof (induct rule: big_step_induct) |
86 proof (induction rule: big_step_induct) |
87 case (WhileTrue b s1 c s2 s3) |
87 case (WhileTrue b s1 c s2 s3) |
88 note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)] |
88 note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)] |
89 |
|
90 from WhileTrue.prems |
89 from WhileTrue.prems |
91 have "P \<Turnstile> b <\<sim>> b'" by simp |
90 have "P \<Turnstile> b <\<sim>> b'" by simp |
92 with `bval b s1` `P s1` |
91 with `bval b s1` `P s1` |
93 have "bval b' s1" by (simp add: bequiv_up_to_def) |
92 have "bval b' s1" by (simp add: bequiv_up_to_def) |
94 moreover |
93 moreover |