| author | wenzelm |
| Wed, 23 Dec 2020 21:06:31 +0100 | |
| changeset 72987 | b1be35908165 |
| child 72990 | db8f94656024 |
| permissions | -rw-r--r-- |
|
72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Hoare/Hoare_Syntax.thy |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
2 |
Author: Leonor Prensa Nieto & Tobias Nipkow |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
3 |
Author: Walter Guttmann (extension to total-correctness proofs) |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
4 |
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
5 |
Concrete syntax for Hoare logic, with translations for variables. |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
6 |
*) |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
7 |
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
8 |
theory Hoare_Syntax |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
9 |
imports Main |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
10 |
begin |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
11 |
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
12 |
syntax |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
13 |
"_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com" ("(2_ :=/ _)" [70, 65] 61)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
14 |
"_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(_;/ _)" [61,60] 60)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
15 |
"_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
16 |
"_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
17 |
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
18 |
syntax |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
19 |
"_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
20 |
translations |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
21 |
"WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
22 |
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
23 |
syntax |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
24 |
"_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
25 |
"_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool" ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
26 |
syntax (output) |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
27 |
"_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("{_} // _ // {_}" [0,55,0] 50)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
28 |
"_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("[_] // _ // [_]" [0,55,0] 50)
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
29 |
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
30 |
ML_file \<open>hoare_syntax.ML\<close> |
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
31 |
|
|
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
diff
changeset
|
32 |
end |