equal
deleted
inserted
replaced
86 case (While P b f c) |
86 case (While P b f c) |
87 show ?case |
87 show ?case |
88 proof |
88 proof |
89 fix s |
89 fix s |
90 show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)" |
90 show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)" |
91 proof(induct "f s" arbitrary: s rule: less_induct) |
91 proof(induction "f s" arbitrary: s rule: less_induct) |
92 case (less n) |
92 case (less n) |
93 thus ?case by (metis While(2) WhileFalse WhileTrue) |
93 thus ?case by (metis While(2) WhileFalse WhileTrue) |
94 qed |
94 qed |
95 qed |
95 qed |
96 next |
96 next |
135 Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)" |
135 Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)" |
136 |
136 |
137 text{* The relation is in fact a function: *} |
137 text{* The relation is in fact a function: *} |
138 |
138 |
139 lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'" |
139 lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'" |
140 proof(induct arbitrary: n' rule:Its.induct) |
140 proof(induction arbitrary: n' rule:Its.induct) |
141 (* new release: |
141 (* new release: |
142 case Its_0 thus ?case by(metis Its.cases) |
142 case Its_0 thus ?case by(metis Its.cases) |
143 next |
143 next |
144 case Its_Suc thus ?case by(metis Its.cases big_step_determ) |
144 case Its_Suc thus ?case by(metis Its.cases big_step_determ) |
145 qed |
145 qed |
158 qed |
158 qed |
159 |
159 |
160 text{* For all terminating loops, @{const Its} yields a result: *} |
160 text{* For all terminating loops, @{const Its} yields a result: *} |
161 |
161 |
162 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n" |
162 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n" |
163 proof(induct "WHILE b DO c" s t rule: big_step_induct) |
163 proof(induction "WHILE b DO c" s t rule: big_step_induct) |
164 case WhileFalse thus ?case by (metis Its_0) |
164 case WhileFalse thus ?case by (metis Its_0) |
165 next |
165 next |
166 case WhileTrue thus ?case by (metis Its_Suc) |
166 case WhileTrue thus ?case by (metis Its_Suc) |
167 qed |
167 qed |
168 |
168 |
177 lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk> |
177 lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk> |
178 \<Longrightarrow> its b c s = Suc(its b c s')" |
178 \<Longrightarrow> its b c s = Suc(its b c s')" |
179 by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality) |
179 by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality) |
180 |
180 |
181 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
181 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
182 proof (induct c arbitrary: Q) |
182 proof (induction c arbitrary: Q) |
183 case SKIP show ?case by simp (blast intro:hoaret.Skip) |
183 case SKIP show ?case by simp (blast intro:hoaret.Skip) |
184 next |
184 next |
185 case Assign show ?case by simp (blast intro:hoaret.Assign) |
185 case Assign show ?case by simp (blast intro:hoaret.Assign) |
186 next |
186 next |
187 case Semi thus ?case by simp (blast intro:hoaret.Semi) |
187 case Semi thus ?case by simp (blast intro:hoaret.Semi) |