author | wenzelm |
Sun, 06 Jan 2019 15:04:34 +0100 | |
changeset 69605 | a96320074298 |
parent 69597 | ff784d5a5bfb |
child 72806 | 4fa08e083865 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Hoare/Hoare_Logic_Abort.thy |
13857 | 2 |
Author: Leonor Prensa Nieto & Tobias Nipkow |
3 |
Copyright 2003 TUM |
|
4 |
||
5 |
Like Hoare.thy, but with an Abort statement for modelling run time errors. |
|
6 |
*) |
|
7 |
||
35320
f80aee1ed475
dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents:
35113
diff
changeset
|
8 |
theory Hoare_Logic_Abort |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
9 |
imports Main |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
21588
diff
changeset
|
10 |
begin |
13857 | 11 |
|
42174 | 12 |
type_synonym 'a bexp = "'a set" |
13 |
type_synonym 'a assn = "'a set" |
|
13857 | 14 |
|
58310 | 15 |
datatype 'a com = |
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
16 |
Basic "'a \<Rightarrow> 'a" |
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
17 |
| Abort |
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
18 |
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) |
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
19 |
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
20 |
| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
35113 | 21 |
|
35054 | 22 |
abbreviation annskip ("SKIP") where "SKIP == Basic id" |
13857 | 23 |
|
42174 | 24 |
type_synonym 'a sem = "'a option => 'a option => bool" |
13857 | 25 |
|
36643 | 26 |
inductive Sem :: "'a com \<Rightarrow> 'a sem" |
27 |
where |
|
28 |
"Sem (Basic f) None None" |
|
29 |
| "Sem (Basic f) (Some s) (Some (f s))" |
|
30 |
| "Sem Abort s None" |
|
31 |
| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'" |
|
32 |
| "Sem (IF b THEN c1 ELSE c2 FI) None None" |
|
33 |
| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" |
|
34 |
| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" |
|
35 |
| "Sem (While b x c) None None" |
|
36 |
| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)" |
|
37 |
| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow> |
|
38 |
Sem (While b x c) (Some s) s'" |
|
13857 | 39 |
|
36643 | 40 |
inductive_cases [elim!]: |
41 |
"Sem (Basic f) s s'" "Sem (c1;c2) s s'" |
|
42 |
"Sem (IF b THEN c1 ELSE c2 FI) s s'" |
|
13857 | 43 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35320
diff
changeset
|
44 |
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where |
67613 | 45 |
"Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q" |
13857 | 46 |
|
47 |
||
35054 | 48 |
syntax |
42152
6c17259724b2
Hoare syntax: standard abstraction syntax admits source positions;
wenzelm
parents:
42054
diff
changeset
|
49 |
"_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
35054 | 50 |
|
51 |
syntax |
|
35320
f80aee1ed475
dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents:
35113
diff
changeset
|
52 |
"_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" |
35054 | 53 |
("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
54 |
syntax ("" output) |
|
35320
f80aee1ed475
dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents:
35113
diff
changeset
|
55 |
"_hoare_abort" :: "['a assn,'a com,'a assn] => bool" |
35054 | 56 |
("{_} // _ // {_}" [0,55,0] 50) |
42152
6c17259724b2
Hoare syntax: standard abstraction syntax admits source positions;
wenzelm
parents:
42054
diff
changeset
|
57 |
|
69605 | 58 |
ML_file \<open>hoare_syntax.ML\<close> |
69597 | 59 |
parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close> |
42153 | 60 |
print_translation |
69597 | 61 |
\<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close> |
13857 | 62 |
|
63 |
||
67410 | 64 |
section \<open>The proof rules\<close> |
13857 | 65 |
|
66 |
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
|
67 |
by (auto simp:Valid_def) |
|
68 |
||
69 |
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q" |
|
70 |
by (auto simp:Valid_def) |
|
71 |
||
72 |
lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R" |
|
73 |
by (auto simp:Valid_def) |
|
74 |
||
75 |
lemma CondRule: |
|
76 |
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')} |
|
77 |
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42174
diff
changeset
|
78 |
by (fastforce simp:Valid_def image_def) |
13857 | 79 |
|
36643 | 80 |
lemma While_aux: |
81 |
assumes "Sem (WHILE b INV {i} DO c OD) s s'" |
|
82 |
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow> |
|
83 |
s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)" |
|
84 |
using assms |
|
85 |
by (induct "WHILE b INV {i} DO c OD" s s') auto |
|
13857 | 86 |
|
87 |
lemma WhileRule: |
|
88 |
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q" |
|
89 |
apply(simp add:Valid_def) |
|
90 |
apply(simp (no_asm) add:image_def) |
|
91 |
apply clarify |
|
36643 | 92 |
apply(drule While_aux) |
93 |
apply assumption |
|
13857 | 94 |
apply blast |
95 |
apply blast |
|
96 |
done |
|
97 |
||
98 |
lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q" |
|
99 |
by(auto simp:Valid_def) |
|
100 |
||
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
21588
diff
changeset
|
101 |
|
62042 | 102 |
subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close> |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
21588
diff
changeset
|
103 |
|
67613 | 104 |
lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}" |
24470
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
21588
diff
changeset
|
105 |
by blast |
41c81e23c08d
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
wenzelm
parents:
21588
diff
changeset
|
106 |
|
69605 | 107 |
ML_file \<open>hoare_tac.ML\<close> |
13857 | 108 |
|
62042 | 109 |
method_setup vcg = \<open> |
110 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close> |
|
13857 | 111 |
"verification condition generator" |
112 |
||
62042 | 113 |
method_setup vcg_simp = \<open> |
30549 | 114 |
Scan.succeed (fn ctxt => |
62042 | 115 |
SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close> |
13857 | 116 |
"verification condition generator plus simplification" |
117 |
||
67410 | 118 |
\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close> |
13875 | 119 |
syntax |
35352 | 120 |
"_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71) |
121 |
"_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61) |
|
13875 | 122 |
translations |
35101 | 123 |
"P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI" |
34940 | 124 |
"a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)" |
67410 | 125 |
\<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close> |
13875 | 126 |
|
67410 | 127 |
text \<open> |
128 |
Note: there is no special syntax for guarded array access. Thus |
|
129 |
you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>. |
|
130 |
\<close> |
|
13875 | 131 |
|
13857 | 132 |
end |