equal
deleted
inserted
replaced
9 subsubsection "Soundness" |
9 subsubsection "Soundness" |
10 |
10 |
11 lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}" |
11 lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}" |
12 proof(induction rule: hoare.induct) |
12 proof(induction rule: hoare.induct) |
13 case (While P b c) |
13 case (While P b c) |
14 { fix s t |
14 have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> P s \<Longrightarrow> P t \<and> \<not> bval b t" for s t |
15 have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> P s \<Longrightarrow> P t \<and> \<not> bval b t" |
15 proof(induction "WHILE b DO c" s t rule: big_step_induct) |
16 proof(induction "WHILE b DO c" s t rule: big_step_induct) |
16 case WhileFalse thus ?case by blast |
17 case WhileFalse thus ?case by blast |
17 next |
18 next |
18 case WhileTrue thus ?case |
19 case WhileTrue thus ?case |
19 using While.IH unfolding hoare_valid_def by blast |
20 using While.IH unfolding hoare_valid_def by blast |
20 qed |
21 qed |
|
22 } |
|
23 thus ?case unfolding hoare_valid_def by blast |
21 thus ?case unfolding hoare_valid_def by blast |
24 qed (auto simp: hoare_valid_def) |
22 qed (auto simp: hoare_valid_def) |
25 |
23 |
26 |
24 |
27 subsubsection "Weakest Precondition" |
25 subsubsection "Weakest Precondition" |