| author | wenzelm |
| Wed, 11 Oct 2023 11:37:18 +0200 | |
| changeset 78758 | 05da36bc806f |
| parent 53015 | a1119cf551e8 |
| permissions | -rw-r--r-- |
| 50161 | 1 |
theory Def_Init |
2 |
imports Vars Com |
|
| 43158 | 3 |
begin |
4 |
||
| 50161 | 5 |
subsection "Definite Initialization Analysis" |
| 43158 | 6 |
|
| 45212 | 7 |
inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where |
| 43158 | 8 |
Skip: "D A SKIP A" | |
9 |
Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" | |
|
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
10 |
Seq: "\<lbrakk> D A\<^sub>1 c\<^sub>1 A\<^sub>2; D A\<^sub>2 c\<^sub>2 A\<^sub>3 \<rbrakk> \<Longrightarrow> D A\<^sub>1 (c\<^sub>1;; c\<^sub>2) A\<^sub>3" | |
|
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
11 |
If: "\<lbrakk> vars b \<subseteq> A; D A c\<^sub>1 A\<^sub>1; D A c\<^sub>2 A\<^sub>2 \<rbrakk> \<Longrightarrow> |
|
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
12 |
D A (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (A\<^sub>1 Int A\<^sub>2)" | |
| 43158 | 13 |
While: "\<lbrakk> vars b \<subseteq> A; D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A" |
14 |
||
15 |
inductive_cases [elim!]: |
|
16 |
"D A SKIP A'" |
|
17 |
"D A (x ::= a) A'" |
|
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
50161
diff
changeset
|
18 |
"D A (c1;;c2) A'" |
| 43158 | 19 |
"D A (IF b THEN c1 ELSE c2) A'" |
20 |
"D A (WHILE b DO c) A'" |
|
21 |
||
22 |
lemma D_incr: |
|
23 |
"D A c A' \<Longrightarrow> A \<subseteq> A'" |
|
24 |
by (induct rule: D.induct) auto |
|
25 |
||
26 |
end |