61 |
61 |
62 (* |
62 (* |
63 Soundness and completeness of vc |
63 Soundness and completeness of vc |
64 *) |
64 *) |
65 |
65 |
66 declare hoare.intros [intro] |
66 declare hoare.conseq [intro] |
67 |
67 |
68 lemma l: "!s. P s --> P s" by fast |
|
69 |
68 |
70 lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}" |
69 lemma vc_sound: "(ALL s. vc c Q s) \<Longrightarrow> |- {awp c Q} astrip c {Q}" |
71 apply (induct c arbitrary: Q) |
70 proof(induct c arbitrary: Q) |
72 apply (simp_all (no_asm)) |
71 case (Awhile b I c) |
73 apply fast |
72 show ?case |
74 apply fast |
73 proof(simp, rule While') |
75 apply fast |
74 from `\<forall>s. vc (Awhile b I c) Q s` |
76 (* if *) |
75 have vc: "ALL s. vc c I s" and IQ: "ALL s. I s \<and> \<not> b s \<longrightarrow> Q s" and |
77 apply atomize |
76 awp: "ALL s. I s & b s --> awp c I s" by simp_all |
78 apply (tactic "deepen_tac @{claset} 4 1") |
77 from vc have "|- {awp c I} astrip c {I}" using Awhile.hyps by blast |
79 (* while *) |
78 with awp show "|- {\<lambda>s. I s \<and> b s} astrip c {I}" |
80 apply atomize |
79 by(rule strengthen_pre) |
81 apply (intro allI impI) |
80 show "\<forall>s. I s \<and> \<not> b s \<longrightarrow> Q s" by(rule IQ) |
82 apply (rule conseq) |
81 qed |
83 apply (rule l) |
82 qed auto |
84 apply (rule While) |
|
85 defer |
|
86 apply fast |
|
87 apply (rule_tac P="awp c fun2" in conseq) |
|
88 apply fast |
|
89 apply fast |
|
90 apply fast |
|
91 done |
|
92 |
83 |
93 lemma awp_mono [rule_format (no_asm)]: |
|
94 "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)" |
|
95 apply (induct c) |
|
96 apply (simp_all (no_asm_simp)) |
|
97 apply (rule allI, rule allI, rule impI) |
|
98 apply (erule allE, erule allE, erule mp) |
|
99 apply (erule allE, erule allE, erule mp, assumption) |
|
100 done |
|
101 |
84 |
102 lemma vc_mono [rule_format (no_asm)]: |
85 lemma awp_mono: |
103 "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)" |
86 "(!s. P s --> Q s) ==> awp c P s ==> awp c Q s" |
104 apply (induct c) |
87 proof (induct c arbitrary: P Q s) |
105 apply (simp_all (no_asm_simp)) |
88 case Asemi thus ?case by simp metis |
106 apply safe |
89 qed simp_all |
107 apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) |
90 |
108 prefer 2 apply assumption |
91 lemma vc_mono: |
109 apply (fast elim: awp_mono) |
92 "(!s. P s --> Q s) ==> vc c P s ==> vc c Q s" |
110 done |
93 proof(induct c arbitrary: P Q) |
|
94 case Asemi thus ?case by simp (metis awp_mono) |
|
95 qed simp_all |
111 |
96 |
112 lemma vc_complete: assumes der: "|- {P}c{Q}" |
97 lemma vc_complete: assumes der: "|- {P}c{Q}" |
113 shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))" |
98 shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))" |
114 (is "? ac. ?Eq P c Q ac") |
99 (is "? ac. ?Eq P c Q ac") |
115 using der |
100 using der |