61 case (If b c1 c2) |
61 case (If b c1 c2) |
62 let ?If = "IF b THEN c1 ELSE c2" |
62 let ?If = "IF b THEN c1 ELSE c2" |
63 show ?case |
63 show ?case |
64 proof(rule hoare.If) |
64 proof(rule hoare.If) |
65 show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}" |
65 show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}" |
66 proof(rule strengthen_pre[OF _ If(1)]) |
66 proof(rule strengthen_pre[OF _ If.IH(1)]) |
67 show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto |
67 show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto |
68 qed |
68 qed |
69 show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}" |
69 show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}" |
70 proof(rule strengthen_pre[OF _ If(2)]) |
70 proof(rule strengthen_pre[OF _ If.IH(2)]) |
71 show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto |
71 show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto |
72 qed |
72 qed |
73 qed |
73 qed |
74 next |
74 next |
75 case (While b c) |
75 case (While b c) |
76 let ?w = "WHILE b DO c" |
76 let ?w = "WHILE b DO c" |
77 have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}" |
77 show "\<turnstile> {wp ?w Q} ?w {Q}" |
78 proof(rule hoare.While) |
78 proof(rule While') |
79 show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}" |
79 show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}" |
80 proof(rule strengthen_pre[OF _ While(1)]) |
80 proof(rule strengthen_pre[OF _ While.IH]) |
81 show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto |
81 show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto |
82 qed |
82 qed |
83 qed |
|
84 thus ?case |
|
85 proof(rule weaken_post) |
|
86 show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto |
83 show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto |
87 qed |
84 qed |
88 qed auto |
85 qed auto |
89 |
86 |
90 lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}" |
87 lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}" |