--- a/src/HOL/Bali/DefiniteAssignment.thy Mon Dec 11 12:28:16 2006 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Dec 11 16:06:14 2006 +0100
@@ -513,25 +513,6 @@
brk :: "breakass" --{* Definetly assigned variables for
abrupt completion with a break *}
-consts da :: "(env \<times> lname set \<times> term \<times> assigned) set"
-text {* The environment @{term env} is only needed for the
- conditional @{text "_ ? _ : _"}.
- The definite assignment rules refer to the typing rules here to
- distinguish boolean and other expressions.
- *}
-
-syntax
-da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool"
- ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
-
-translations
- "E\<turnstile> B \<guillemotright>t\<guillemotright> A" == "(E,B,t,A) \<in> da"
-
-text {* @{text B}: the ''assigned'' variables before evaluating term @{text t};
- @{text A}: the ''assigned'' variables after evaluating term @{text t}
-*}
-
-
constdefs rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
"rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x"
@@ -543,35 +524,45 @@
constdefs range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
"\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}"
-inductive "da" intros
-
- Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
+text {*
+In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},
+@{text B} denotes the ''assigned'' variables before evaluating term @{text t},
+whereas @{text A} denotes the ''assigned'' variables after evaluating term @{text t}.
+The environment @{term E} is only needed for the conditional @{text "_ ? _ : _"}.
+The definite assignment rules refer to the typing rules here to
+distinguish boolean and other expressions.
+*}
- Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
- Lab: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; nrm A = nrm C \<inter> (brk C) l; brk A = rmlab l (brk C)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A"
+inductive2
+ da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
+where
+ Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
- Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
- nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"
+| Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
+| Lab: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; nrm A = nrm C \<inter> (brk C) l; brk A = rmlab l (brk C)\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A"
- If: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;
- Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
- Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
- nrm A = nrm C1 \<inter> nrm C2;
- brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A"
+| Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
+ nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"
+
+| If: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;
+ Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
+ Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
+ nrm A = nrm C1 \<inter> nrm C2;
+ brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A"
--{* Note that @{term E} is not further used, because we take the specialized
sets that also consider if the expression evaluates to true or false.
Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break
map of @{term E} will be the trivial one. So
- @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to enshure the definite assignment in
+ @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to ensure the definite assignment in
expression @{term e}.
Notice the implicit analysis of a constant boolean expression @{term e}
in this rule. For example, if @{term e} is constantly @{term True} then
@@ -585,12 +576,12 @@
contribution.
*}
- Loop: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;
- Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
- nrm A = nrm C \<inter> (B \<union> assigns_if False e);
- brk A = brk C\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
+| Loop: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;
+ Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
+ nrm A = nrm C \<inter> (B \<union> assigns_if False e);
+ brk A = brk C\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
--{* The @{text Loop} rule resembles some of the ideas of the @{text If} rule.
For the @{term "nrm A"} the set @{term "B \<union> assigns_if False e"}
will be @{term UNIV} if the condition is constantly true. To normally exit
@@ -602,14 +593,14 @@
handle the breaks specially.
*}
- Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B;
- nrm A = UNIV;
- brk A = (case jump of
- Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV
- | Cont l \<Rightarrow> \<lambda> k. UNIV
- | Ret \<Rightarrow> \<lambda> k. UNIV)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"
+| Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B;
+ nrm A = UNIV;
+ brk A = (case jump of
+ Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV
+ | Cont l \<Rightarrow> \<lambda> k. UNIV
+ | Ret \<Rightarrow> \<lambda> k. UNIV)\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"
--{* In case of a break to label @{term l} the corresponding break set is all
variables assigned before the break. The assigned variables for normal
completion of the @{term Jmp} is @{term UNIV}, because the statement will
@@ -618,21 +609,21 @@
assigned.
*}
- Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk>
- \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
+| Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk>
+ \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
- Try: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
- Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
- nrm A = nrm C1 \<inter> nrm C2;
- brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk>
- \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
+| Try: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
+ Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
+ nrm A = nrm C1 \<inter> nrm C2;
+ brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk>
+ \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
- Fin: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
- Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
- nrm A = nrm C1 \<union> nrm C2;
- brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A"
+| Fin: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
+ Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
+ nrm A = nrm C1 \<union> nrm C2;
+ brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A"
--{* The set of assigned variables before execution @{term c2} are the same
as before execution @{term c1}, because @{term c1} could throw an exception
and so we can't guarantee that any variable will be assigned in @{term c1}.
@@ -671,7 +662,7 @@
and @{text NewA}
*}
- Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
+| Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
--{* Wellformedness of a program will ensure, that every static initialiser
is definetly assigned and the jumps are nested correctly. The case here
for @{term Init} is just for convenience, to get a proper precondition
@@ -679,91 +670,91 @@
expand the initialisation on every point where it is triggerred by the
evaluation rules.
*}
- NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
+| NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
+
+| NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"
- NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"
+| Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"
- Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"
+| Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"
- Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"
+| Lit: "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
- Lit: "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
+| UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"
- UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"
+| CondAnd: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if True e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
+ nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>
+ assigns_if False (BinOp CondAnd e1 e2));
+ brk A = (\<lambda> l. UNIV) \<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A"
- CondAnd: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if True e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
- nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>
- assigns_if False (BinOp CondAnd e1 e2));
+| CondOr: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if False e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
+ nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>
+ assigns_if False (BinOp CondOr e1 e2));
brk A = (\<lambda> l. UNIV) \<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A"
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A"
- CondOr: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if False e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
- nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>
- assigns_if False (BinOp CondOr e1 e2));
- brk A = (\<lambda> l. UNIV) \<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A"
+| BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A;
+ binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"
- BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A;
- binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"
+| Super: "This \<in> B
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
- Super: "This \<in> B
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
-
- AccLVar: "\<lbrakk>vn \<in> B;
- nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A"
+| AccLVar: "\<lbrakk>vn \<in> B;
+ nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A"
--{* To properly access a local variable we have to test the definite
assignment here. The variable must occur in the set @{term B}
*}
- Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn;
- Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"
+| Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn;
+ Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"
- AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A"
+| AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A"
- Ass: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V; Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"
+| Ass: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V; Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"
- CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
- Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
- Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
- Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
- nrm A = B \<union> (assigns_if True (c ? e1 : e2) \<inter>
- assigns_if False (c ? e1 : e2));
- brk A = (\<lambda> l. UNIV)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A"
+| CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
+ Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
+ Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
+ Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
+ nrm A = B \<union> (assigns_if True (c ? e1 : e2) \<inter>
+ assigns_if False (c ? e1 : e2));
+ brk A = (\<lambda> l. UNIV)\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A"
- Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
- Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
- Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
- Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
- nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A"
+| Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
+ Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
+ Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
+ Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
+ nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A"
- Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"
+| Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"
-- {* The interplay of @{term Call}, @{term Methd} and @{term Body}:
Why rules for @{term Methd} and @{term Body} at all? Note that a
@@ -786,16 +777,16 @@
also a precondition for type-safety and so we can omit some assertion
that are already ensured by well-typedness.
*}
- Methd: "\<lbrakk>methd (prg Env) D sig = Some m;
- Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A
- \<rbrakk>
+| Methd: "\<lbrakk>methd (prg Env) D sig = Some m;
+ Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A
+ \<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A"
+
+| Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C;
+ nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk>
\<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A"
-
- Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C;
- nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A"
+ Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A"
-- {* Note that @{term A} is not correlated to @{term C}. If the body
statement returns abruptly with return, evaluation of @{term Body}
will absorb this return and complete normally. So we cannot trivially
@@ -809,21 +800,21 @@
set and then this information must be carried over to the @{term Body}
rule by the conformance predicate of the state.
*}
- LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>"
+| LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>"
- FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A"
-
- AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk>
+| FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
\<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A"
+ Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A"
- Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>"
+| AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A"
- Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk>
- \<Longrightarrow>
- Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A"
+| Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>"
+
+| Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk>
+ \<Longrightarrow>
+ Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A"
declare inj_term_sym_simps [simp]
@@ -832,7 +823,7 @@
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
*}
-inductive_cases da_elim_cases [cases set]:
+inductive_cases2 da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
"Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A"
"Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
@@ -1076,7 +1067,7 @@
from Expr.prems Expr.hyps
show ?case by cases simp
next
- case (Lab A B C Env c l B' A')
+ case (Lab Env B c C A l B' A')
have A: "nrm A = nrm C \<inter> brk C l" "brk A = rmlab l (brk C)" .
have "PROP ?Hyp Env B \<langle>c\<rangle> C" .
moreover
@@ -1102,7 +1093,7 @@
ultimately show ?case
by simp
next
- case (Comp A B C1 C2 Env c1 c2 B' A')
+ case (Comp Env B c1 C1 c2 C2 A B' A')
have A: "nrm A = nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2" .
have "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'" .
then obtain C1' C2'
@@ -1123,7 +1114,7 @@
show ?case
by auto
next
- case (If A B C1 C2 E Env c1 c2 e B' A')
+ case (If Env B e E c1 C1 c2 C2 A B' A')
have A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2" .
have "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'" .
then obtain C1' C2'
@@ -1144,7 +1135,7 @@
show ?case
by auto
next
- case (Loop A B C E Env c e l B' A')
+ case (Loop Env B e E c C A l B' A')
have A: "nrm A = nrm C \<inter> (B \<union> assigns_if False e)"
"brk A = brk C" .
have "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'" .
@@ -1180,12 +1171,12 @@
ultimately show ?case
by auto
next
- case (Jmp A B Env jump B' A')
+ case (Jmp jump B A Env B' A')
thus ?case by (elim da_elim_cases) (auto split: jump.splits)
next
case Throw thus ?case by - (erule da_elim_cases, auto)
next
- case (Try A B C C1 C2 Env c1 c2 vn B' A')
+ case (Try Env B c1 C1 vn C c2 C2 A B' A')
have A: "nrm A = nrm C1 \<inter> nrm C2"
"brk A = brk C1 \<Rightarrow>\<inter> brk C2" .
have "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'" .
@@ -1210,7 +1201,7 @@
show ?case
by auto
next
- case (Fin A B C1 C2 Env c1 c2 B' A')
+ case (Fin Env B c1 C1 c2 C2 A B' A')
have A: "nrm A = nrm C1 \<union> nrm C2"
"brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)" .
have "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'" .
@@ -1247,7 +1238,7 @@
next
case UnOp thus ?case by - (erule da_elim_cases, auto)
next
- case (CondAnd A B E1 E2 Env e1 e2 B' A')
+ case (CondAnd Env B e1 E1 e2 E2 A B' A')
have A: "nrm A = B \<union>
assigns_if True (BinOp CondAnd e1 e2) \<inter>
assigns_if False (BinOp CondAnd e1 e2)"
@@ -1276,7 +1267,7 @@
next
case Ass thus ?case by - (erule da_elim_cases, auto)
next
- case (CondBool A B C E1 E2 Env c e1 e2 B' A')
+ case (CondBool Env c e1 e2 B C E1 E2 A B' A')
have A: "nrm A = B \<union>
assigns_if True (c ? e1 : e2) \<inter>
assigns_if False (c ? e1 : e2)"
@@ -1295,7 +1286,7 @@
with A A' show ?case
by auto
next
- case (Cond A B C E1 E2 Env c e1 e2 B' A')
+ case (Cond Env c e1 e2 B C E1 E2 A B' A')
have A: "nrm A = nrm E1 \<inter> nrm E2"
"brk A = (\<lambda>l. UNIV)" .
have not_bool: "\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)" .
@@ -1354,7 +1345,7 @@
next
case Expr thus ?case by (iprover intro: da.Expr)
next
- case (Lab A B C Env c l B')
+ case (Lab Env B c C A l B')
have "PROP ?Hyp Env B \<langle>c\<rangle>" .
moreover
have B': "B \<subseteq> B'" .
@@ -1364,7 +1355,7 @@
by (iprover intro: da.Lab)
thus ?case ..
next
- case (Comp A B C1 C2 Env c1 c2 B')
+ case (Comp Env B c1 C1 c2 C2 A B')
have da_c1: "Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" .
have "PROP ?Hyp Env B \<langle>c1\<rangle>" .
moreover
@@ -1383,7 +1374,7 @@
by (iprover intro: da.Comp)
thus ?case ..
next
- case (If A B C1 C2 E Env c1 c2 e B')
+ case (If Env B e E c1 C1 c2 C2 A B')
have B': "B \<subseteq> B'" .
obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
@@ -1417,7 +1408,7 @@
by (iprover intro: da.If)
thus ?case ..
next
- case (Loop A B C E Env c e l B')
+ case (Loop Env B e E c C A l B')
have B': "B \<subseteq> B'" .
obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
@@ -1441,7 +1432,7 @@
by (iprover intro: da.Loop )
thus ?case ..
next
- case (Jmp A B Env jump B')
+ case (Jmp jump B A Env B')
have B': "B \<subseteq> B'" .
with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' "
by auto
@@ -1460,7 +1451,7 @@
next
case Throw thus ?case by (iprover intro: da.Throw )
next
- case (Try A B C C1 C2 Env c1 c2 vn B')
+ case (Try Env B c1 C1 vn C c2 C2 A B')
have B': "B \<subseteq> B'" .
obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
proof -
@@ -1485,7 +1476,7 @@
by (iprover intro: da.Try )
thus ?case ..
next
- case (Fin A B C1 C2 Env c1 c2 B')
+ case (Fin Env B c1 C1 c2 C2 A B')
have B': "B \<subseteq> B'" .
obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
proof -
@@ -1519,7 +1510,7 @@
next
case UnOp thus ?case by (iprover intro: da.UnOp)
next
- case (CondAnd A B E1 E2 Env e1 e2 B')
+ case (CondAnd Env B e1 E1 e2 E2 A B')
have B': "B \<subseteq> B'" .
obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
@@ -1541,7 +1532,7 @@
by (iprover intro: da.CondAnd)
thus ?case ..
next
- case (CondOr A B E1 E2 Env e1 e2 B')
+ case (CondOr Env B e1 E1 e2 E2 A B')
have B': "B \<subseteq> B'" .
obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
@@ -1563,7 +1554,7 @@
by (iprover intro: da.CondOr)
thus ?case ..
next
- case (BinOp A B E1 Env binop e1 e2 B')
+ case (BinOp Env B e1 E1 e2 A binop B')
have B': "B \<subseteq> B'" .
obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
@@ -1593,7 +1584,7 @@
by auto
thus ?case by (iprover intro: da.Super)
next
- case (AccLVar A B Env vn B')
+ case (AccLVar vn B A Env B')
have "vn \<in> B" .
moreover
have "B \<subseteq> B'" .
@@ -1602,7 +1593,7 @@
next
case Acc thus ?case by (iprover intro: da.Acc)
next
- case (AssLVar A B E Env e vn B')
+ case (AssLVar Env B e E A vn B')
have B': "B \<subseteq> B'" .
then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
by (rule AssLVar.hyps [elim_format]) iprover
@@ -1611,7 +1602,7 @@
by (iprover intro: da.AssLVar)
thus ?case ..
next
- case (Ass A B Env V e v B')
+ case (Ass v Env B V e A B')
have B': "B \<subseteq> B'" .
have "\<forall>vn. v \<noteq> LVar vn".
moreover
@@ -1637,7 +1628,7 @@
by (iprover intro: da.Ass)
thus ?case ..
next
- case (CondBool A B C E1 E2 Env c e1 e2 B')
+ case (CondBool Env c e1 e2 B C E1 E2 A B')
have B': "B \<subseteq> B'" .
have "Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" .
moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
@@ -1673,7 +1664,7 @@
by (iprover intro: da.CondBool)
thus ?case ..
next
- case (Cond A B C E1 E2 Env c e1 e2 B')
+ case (Cond Env c e1 e2 B C E1 E2 A B')
have B': "B \<subseteq> B'" .
have "\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" .
moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
@@ -1709,7 +1700,7 @@
by (iprover intro: da.Cond)
thus ?case ..
next
- case (Call A B E Env accC args e mn mode pTs statT B')
+ case (Call Env B e E args A accC statT mode mn pTs B')
have B': "B \<subseteq> B'" .
obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
@@ -1735,7 +1726,7 @@
next
case Methd thus ?case by (iprover intro: da.Methd)
next
- case (Body A B C D Env c B')
+ case (Body Env B c C A D B')
have B': "B \<subseteq> B'" .
obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'"
proof -
@@ -1763,7 +1754,7 @@
next
case FVar thus ?case by (iprover intro: da.FVar)
next
- case (AVar A B E1 Env e1 e2 B')
+ case (AVar Env B e1 E1 e2 A B')
have B': "B \<subseteq> B'" .
obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
@@ -1789,7 +1780,7 @@
next
case Nil thus ?case by (iprover intro: da.Nil)
next
- case (Cons A B E Env e es B')
+ case (Cons Env B e E es A B')
have B': "B \<subseteq> B'" .
obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -