author | blanchet |
Thu, 11 Sep 2014 18:54:36 +0200 | |
changeset 58305 | 57752a91eec4 |
parent 55660 | f0f895716a8b |
child 58310 | 91ea607a34d8 |
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 |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
15 |
datatype_new 'a com = |
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 |
13857 | 45 |
"Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q" |
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 |
|
48891 | 58 |
ML_file "hoare_syntax.ML" |
52143 | 59 |
parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, K Hoare_Syntax.hoare_vars_tr)] *} |
42153 | 60 |
print_translation |
52143 | 61 |
{* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"}))] *} |
13857 | 62 |
|
63 |
||
64 |
(*** The proof rules ***) |
|
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 |
|
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
|
102 |
subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *} |
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 |
|
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
|
104 |
lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" |
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 |
|
48891 | 107 |
ML_file "hoare_tac.ML" |
13857 | 108 |
|
109 |
method_setup vcg = {* |
|
55660 | 110 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac))) *} |
13857 | 111 |
"verification condition generator" |
112 |
||
113 |
method_setup vcg_simp = {* |
|
30549 | 114 |
Scan.succeed (fn ctxt => |
55660 | 115 |
SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt))) *} |
13857 | 116 |
"verification condition generator plus simplification" |
117 |
||
13875 | 118 |
(* Special syntax for guarded statements and guarded array updates: *) |
119 |
||
120 |
syntax |
|
35352 | 121 |
"_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71) |
122 |
"_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61) |
|
13875 | 123 |
translations |
35101 | 124 |
"P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI" |
34940 | 125 |
"a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)" |
13875 | 126 |
(* reverse translation not possible because of duplicate "a" *) |
127 |
||
128 |
text{* Note: there is no special syntax for guarded array access. Thus |
|
129 |
you must write @{text"j < length a \<rightarrow> a[i] := a!j"}. *} |
|
130 |
||
13857 | 131 |
end |