author | wenzelm |
Wed, 23 Dec 2020 22:25:22 +0100 | |
changeset 72990 | db8f94656024 |
parent 72987 | b1be35908165 |
child 73655 | 26a1d66b9077 |
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 |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
4 |
Author: Walter Guttmann (extension to total-correctness proofs) |
13857 | 5 |
*) |
6 |
||
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
7 |
section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
8 |
|
35320
f80aee1ed475
dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents:
35113
diff
changeset
|
9 |
theory Hoare_Logic_Abort |
72990 | 10 |
imports Hoare_Syntax Hoare_Tac |
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
|
11 |
begin |
13857 | 12 |
|
42174 | 13 |
type_synonym 'a bexp = "'a set" |
14 |
type_synonym 'a assn = "'a set" |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
15 |
type_synonym 'a var = "'a \<Rightarrow> nat" |
13857 | 16 |
|
58310 | 17 |
datatype 'a com = |
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
18 |
Basic "'a \<Rightarrow> 'a" |
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
55660
diff
changeset
|
19 |
| Abort |
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
20 |
| Seq "'a com" "'a com" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
21 |
| Cond "'a bexp" "'a com" "'a com" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
22 |
| While "'a bexp" "'a assn" "'a var" "'a com" |
35113 | 23 |
|
35054 | 24 |
abbreviation annskip ("SKIP") where "SKIP == Basic id" |
13857 | 25 |
|
42174 | 26 |
type_synonym 'a sem = "'a option => 'a option => bool" |
13857 | 27 |
|
36643 | 28 |
inductive Sem :: "'a com \<Rightarrow> 'a sem" |
29 |
where |
|
30 |
"Sem (Basic f) None None" |
|
31 |
| "Sem (Basic f) (Some s) (Some (f s))" |
|
32 |
| "Sem Abort s None" |
|
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
33 |
| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
34 |
| "Sem (Cond b c1 c2) None None" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
35 |
| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
36 |
| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'" |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
37 |
| "Sem (While b x y c) None None" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
38 |
| "s \<notin> b \<Longrightarrow> Sem (While b x y c) (Some s) (Some s)" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
39 |
| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow> |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
40 |
Sem (While b x y c) (Some s) s'" |
13857 | 41 |
|
36643 | 42 |
inductive_cases [elim!]: |
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
43 |
"Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
44 |
"Sem (Cond b c1 c2) s s'" |
13857 | 45 |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
46 |
lemma Sem_deterministic: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
47 |
assumes "Sem c s s1" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
48 |
and "Sem c s s2" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
49 |
shows "s1 = s2" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
50 |
proof - |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
51 |
have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
52 |
by (induct rule: Sem.induct) (subst Sem.simps, blast)+ |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
53 |
thus ?thesis |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
54 |
using assms by simp |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
55 |
qed |
13857 | 56 |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
57 |
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
58 |
where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
59 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
60 |
definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
61 |
where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> q)" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
62 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
63 |
lemma tc_implies_pc: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
64 |
"ValidTC p c q \<Longrightarrow> Valid p c q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
65 |
by (smt Sem_deterministic ValidTC_def Valid_def image_iff) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
66 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
67 |
lemma tc_extract_function: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
68 |
"ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
69 |
by (meson ValidTC_def) |
13857 | 70 |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
71 |
text \<open>The proof rules for partial correctness\<close> |
13857 | 72 |
|
73 |
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
|
74 |
by (auto simp:Valid_def) |
|
75 |
||
76 |
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q" |
|
77 |
by (auto simp:Valid_def) |
|
78 |
||
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
79 |
lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R" |
13857 | 80 |
by (auto simp:Valid_def) |
81 |
||
82 |
lemma CondRule: |
|
83 |
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')} |
|
84 |
\<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
|
85 |
by (fastforce simp:Valid_def image_def) |
13857 | 86 |
|
36643 | 87 |
lemma While_aux: |
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
88 |
assumes "Sem (While b i v c) s s'" |
36643 | 89 |
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow> |
90 |
s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)" |
|
91 |
using assms |
|
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
92 |
by (induct "While b i v c" s s') auto |
13857 | 93 |
|
94 |
lemma WhileRule: |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
95 |
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
96 |
apply (clarsimp simp:Valid_def) |
36643 | 97 |
apply(drule While_aux) |
98 |
apply assumption |
|
13857 | 99 |
apply blast |
100 |
apply blast |
|
101 |
done |
|
102 |
||
103 |
lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q" |
|
104 |
by(auto simp:Valid_def) |
|
105 |
||
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
106 |
text \<open>The proof rules for total correctness\<close> |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
107 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
108 |
lemma SkipRuleTC: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
109 |
assumes "p \<subseteq> q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
110 |
shows "ValidTC p (Basic id) q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
111 |
by (metis Sem.intros(2) ValidTC_def assms id_def subsetD) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
112 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
113 |
lemma BasicRuleTC: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
114 |
assumes "p \<subseteq> {s. f s \<in> q}" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
115 |
shows "ValidTC p (Basic f) q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
116 |
by (metis Ball_Collect Sem.intros(2) ValidTC_def assms) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
117 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
118 |
lemma SeqRuleTC: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
119 |
assumes "ValidTC p c1 q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
120 |
and "ValidTC q c2 r" |
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
121 |
shows "ValidTC p (Seq c1 c2) r" |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
122 |
by (meson assms Sem.intros(4) ValidTC_def) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
123 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
124 |
lemma CondRuleTC: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
125 |
assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
126 |
and "ValidTC w c1 q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
127 |
and "ValidTC w' c2 q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
128 |
shows "ValidTC p (Cond b c1 c2) q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
129 |
proof (unfold ValidTC_def, rule allI) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
130 |
fix s |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
131 |
show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) (Some s) (Some t) \<and> t \<in> q)" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
132 |
apply (cases "s \<in> b") |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
133 |
apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2)) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
134 |
by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3)) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
135 |
qed |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
136 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
137 |
lemma WhileRuleTC: |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
138 |
assumes "p \<subseteq> i" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
139 |
and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
140 |
and "i \<inter> uminus b \<subseteq> q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
141 |
shows "ValidTC p (While b i v c) q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
142 |
proof - |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
143 |
{ |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
144 |
fix s n |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
145 |
have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
146 |
proof (induction "n" arbitrary: s rule: less_induct) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
147 |
fix n :: nat |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
148 |
fix s :: 'a |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
149 |
assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
150 |
show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
151 |
proof (rule impI, cases "s \<in> b") |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
152 |
assume 2: "s \<in> b" and "s \<in> i \<and> v s = n" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
153 |
hence "s \<in> i \<inter> b \<inter> {s . v s = n}" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
154 |
using assms(1) by auto |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
155 |
hence "\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
156 |
by (metis assms(2) ValidTC_def) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
157 |
from this obtain t where 3: "Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
158 |
by auto |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
159 |
hence "\<exists>u . Sem (While b i v c) (Some t) (Some u) \<and> u \<in> q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
160 |
using 1 by auto |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
161 |
thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
162 |
using 2 3 Sem.intros(10) by force |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
163 |
next |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
164 |
assume "s \<notin> b" and "s \<in> i \<and> v s = n" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
165 |
thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
166 |
using Sem.intros(9) assms(3) by fastforce |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
167 |
qed |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
168 |
qed |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
169 |
} |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
170 |
thus ?thesis |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
171 |
using assms(1) ValidTC_def by force |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
172 |
qed |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
173 |
|
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
|
174 |
|
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
175 |
subsection \<open>Concrete syntax\<close> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
176 |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
177 |
setup \<open> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
178 |
Hoare_Syntax.setup |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
179 |
{Basic = \<^const_syntax>\<open>Basic\<close>, |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
180 |
Skip = \<^const_syntax>\<open>annskip\<close>, |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
181 |
Seq = \<^const_syntax>\<open>Seq\<close>, |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
182 |
Cond = \<^const_syntax>\<open>Cond\<close>, |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
183 |
While = \<^const_syntax>\<open>While\<close>, |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
184 |
Valid = \<^const_syntax>\<open>Valid\<close>, |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
185 |
ValidTC = \<^const_syntax>\<open>ValidTC\<close>} |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
186 |
\<close> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
187 |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
188 |
\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
189 |
syntax |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
190 |
"_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71) |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
191 |
"_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61) |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
192 |
translations |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
193 |
"P \<rightarrow> c" \<rightleftharpoons> "IF P THEN c ELSE CONST Abort FI" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
194 |
"a[i] := v" \<rightharpoonup> "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)" |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
195 |
\<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
196 |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
197 |
text \<open> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
198 |
Note: there is no special syntax for guarded array access. Thus |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
199 |
you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>. |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
200 |
\<close> |
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
201 |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
202 |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72985
diff
changeset
|
203 |
subsection \<open>Proof methods: VCG\<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
|
204 |
|
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
205 |
declare BasicRule [Hoare_Tac.BasicRule] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
206 |
and SkipRule [Hoare_Tac.SkipRule] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
207 |
and AbortRule [Hoare_Tac.AbortRule] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
208 |
and SeqRule [Hoare_Tac.SeqRule] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
209 |
and CondRule [Hoare_Tac.CondRule] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
210 |
and WhileRule [Hoare_Tac.WhileRule] |
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
|
211 |
|
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
212 |
declare BasicRuleTC [Hoare_Tac.BasicRuleTC] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
213 |
and SkipRuleTC [Hoare_Tac.SkipRuleTC] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
214 |
and SeqRuleTC [Hoare_Tac.SeqRuleTC] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
215 |
and CondRuleTC [Hoare_Tac.CondRuleTC] |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
216 |
and WhileRuleTC [Hoare_Tac.WhileRuleTC] |
13857 | 217 |
|
62042 | 218 |
method_setup vcg = \<open> |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
219 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close> |
13857 | 220 |
"verification condition generator" |
221 |
||
62042 | 222 |
method_setup vcg_simp = \<open> |
30549 | 223 |
Scan.succeed (fn ctxt => |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
224 |
SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close> |
13857 | 225 |
"verification condition generator plus simplification" |
226 |
||
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
227 |
method_setup vcg_tc = \<open> |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
228 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close> |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
229 |
"verification condition generator" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
230 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
231 |
method_setup vcg_tc_simp = \<open> |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
232 |
Scan.succeed (fn ctxt => |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72984
diff
changeset
|
233 |
SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close> |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
234 |
"verification condition generator plus simplification" |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69605
diff
changeset
|
235 |
|
13857 | 236 |
end |