author | haftmann |
Sat, 20 Aug 2011 01:33:58 +0200 | |
changeset 44324 | d972b91ed09d |
parent 42174 | d0be2722ce9f |
child 48891 | c0eafbd55de3 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Hoare/Hoare_Logic.thy |
5646 | 2 |
Author: Leonor Prensa Nieto & Tobias Nipkow |
3 |
Copyright 1998 TUM |
|
1335 | 4 |
|
5 |
Sugared semantic embedding of Hoare logic. |
|
5646 | 6 |
Strictly speaking a shallow embedding (as implemented by Norbert Galm |
7 |
following Mike Gordon) would suffice. Maybe the datatype com comes in useful |
|
8 |
later. |
|
1335 | 9 |
*) |
10 |
||
35316
870dfea4f9c0
dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents:
35113
diff
changeset
|
11 |
theory Hoare_Logic |
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:
24472
diff
changeset
|
12 |
imports Main |
42153 | 13 |
uses ("hoare_syntax.ML") ("hoare_tac.ML") |
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
|
14 |
begin |
1335 | 15 |
|
42174 | 16 |
type_synonym 'a bexp = "'a set" |
17 |
type_synonym 'a assn = "'a set" |
|
5646 | 18 |
|
19 |
datatype |
|
35113 | 20 |
'a com = Basic "'a \<Rightarrow> 'a" |
13682 | 21 |
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) |
22 |
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
|
23 |
| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
|
35113 | 24 |
|
35054 | 25 |
abbreviation annskip ("SKIP") where "SKIP == Basic id" |
5646 | 26 |
|
42174 | 27 |
type_synonym 'a sem = "'a => 'a => bool" |
5646 | 28 |
|
36643 | 29 |
inductive Sem :: "'a com \<Rightarrow> 'a sem" |
30 |
where |
|
31 |
"Sem (Basic f) s (f s)" |
|
32 |
| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'" |
|
33 |
| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'" |
|
34 |
| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'" |
|
35 |
| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s" |
|
36 |
| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow> |
|
37 |
Sem (While b x c) s s'" |
|
5646 | 38 |
|
36643 | 39 |
inductive_cases [elim!]: |
40 |
"Sem (Basic f) s s'" "Sem (c1;c2) s s'" |
|
41 |
"Sem (IF b THEN c1 ELSE c2 FI) s s'" |
|
5646 | 42 |
|
38353 | 43 |
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" |
44 |
where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)" |
|
5007 | 45 |
|
46 |
||
35054 | 47 |
syntax |
42152
6c17259724b2
Hoare syntax: standard abstraction syntax admits source positions;
wenzelm
parents:
42054
diff
changeset
|
48 |
"_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
35054 | 49 |
|
50 |
syntax |
|
51 |
"_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" |
|
52 |
("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
|
53 |
syntax ("" output) |
|
54 |
"_hoare" :: "['a assn,'a com,'a assn] => bool" |
|
55 |
("{_} // _ // {_}" [0,55,0] 50) |
|
13764 | 56 |
|
42153 | 57 |
use "hoare_syntax.ML" |
58 |
parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *} |
|
59 |
print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *} |
|
1335 | 60 |
|
13682 | 61 |
|
13857 | 62 |
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
63 |
by (auto simp:Valid_def) |
|
64 |
||
65 |
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q" |
|
66 |
by (auto simp:Valid_def) |
|
67 |
||
68 |
lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R" |
|
69 |
by (auto simp:Valid_def) |
|
70 |
||
71 |
lemma CondRule: |
|
72 |
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')} |
|
73 |
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q" |
|
74 |
by (auto simp:Valid_def) |
|
75 |
||
36643 | 76 |
lemma While_aux: |
77 |
assumes "Sem (WHILE b INV {i} DO c OD) s s'" |
|
78 |
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow> |
|
79 |
s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b" |
|
80 |
using assms |
|
81 |
by (induct "WHILE b INV {i} DO c OD" s s') auto |
|
13857 | 82 |
|
83 |
lemma WhileRule: |
|
84 |
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q" |
|
85 |
apply (clarsimp simp:Valid_def) |
|
36643 | 86 |
apply(drule While_aux) |
87 |
apply assumption |
|
13857 | 88 |
apply blast |
89 |
apply blast |
|
90 |
done |
|
91 |
||
92 |
||
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
|
93 |
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
|
94 |
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
|
95 |
|
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:
24472
diff
changeset
|
96 |
lemmas AbortRule = SkipRule -- "dummy version" |
24472
943ef707396c
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
24470
diff
changeset
|
97 |
use "hoare_tac.ML" |
13682 | 98 |
|
99 |
method_setup vcg = {* |
|
30549 | 100 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} |
13682 | 101 |
"verification condition generator" |
102 |
||
103 |
method_setup vcg_simp = {* |
|
30549 | 104 |
Scan.succeed (fn ctxt => |
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents:
32134
diff
changeset
|
105 |
SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} |
13682 | 106 |
"verification condition generator plus simplification" |
107 |
||
108 |
end |