8 theory Hoare_Logic_Abort |
8 theory Hoare_Logic_Abort |
9 imports Main |
9 imports Main |
10 uses ("hoare_syntax.ML") ("hoare_tac.ML") |
10 uses ("hoare_syntax.ML") ("hoare_tac.ML") |
11 begin |
11 begin |
12 |
12 |
13 types |
13 type_synonym 'a bexp = "'a set" |
14 'a bexp = "'a set" |
14 type_synonym 'a assn = "'a set" |
15 'a assn = "'a set" |
|
16 |
15 |
17 datatype |
16 datatype |
18 'a com = Basic "'a \<Rightarrow> 'a" |
17 'a com = Basic "'a \<Rightarrow> 'a" |
19 | Abort |
18 | Abort |
20 | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) |
19 | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) |
21 | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
20 | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
22 | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
21 | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
23 |
22 |
24 abbreviation annskip ("SKIP") where "SKIP == Basic id" |
23 abbreviation annskip ("SKIP") where "SKIP == Basic id" |
25 |
24 |
26 types 'a sem = "'a option => 'a option => bool" |
25 type_synonym 'a sem = "'a option => 'a option => bool" |
27 |
26 |
28 inductive Sem :: "'a com \<Rightarrow> 'a sem" |
27 inductive Sem :: "'a com \<Rightarrow> 'a sem" |
29 where |
28 where |
30 "Sem (Basic f) None None" |
29 "Sem (Basic f) None None" |
31 | "Sem (Basic f) (Some s) (Some (f s))" |
30 | "Sem (Basic f) (Some s) (Some (f s))" |