541 *) |
522 *) |
542 |
523 |
543 constdefs range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) |
524 constdefs range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) |
544 "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}" |
525 "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}" |
545 |
526 |
546 inductive "da" intros |
527 text {* |
547 |
528 In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"}, |
548 Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
529 @{text B} denotes the ''assigned'' variables before evaluating term @{text t}, |
549 |
530 whereas @{text A} denotes the ''assigned'' variables after evaluating term @{text t}. |
550 Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
531 The environment @{term E} is only needed for the conditional @{text "_ ? _ : _"}. |
551 \<Longrightarrow> |
532 The definite assignment rules refer to the typing rules here to |
552 Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A" |
533 distinguish boolean and other expressions. |
553 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> |
534 *} |
554 \<Longrightarrow> |
535 |
555 Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A" |
536 inductive2 |
556 |
537 da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71) |
557 Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
538 where |
558 nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk> |
539 Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
559 \<Longrightarrow> |
540 |
560 Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A" |
541 | Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
561 |
542 \<Longrightarrow> |
562 If: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; |
543 Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A" |
563 Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
544 | 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> |
564 Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
545 \<Longrightarrow> |
565 nrm A = nrm C1 \<inter> nrm C2; |
546 Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A" |
566 brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk> |
547 |
567 \<Longrightarrow> |
548 | Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
568 Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A" |
549 nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk> |
|
550 \<Longrightarrow> |
|
551 Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A" |
|
552 |
|
553 | If: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; |
|
554 Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
|
555 Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
|
556 nrm A = nrm C1 \<inter> nrm C2; |
|
557 brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk> |
|
558 \<Longrightarrow> |
|
559 Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A" |
569 |
560 |
570 --{* Note that @{term E} is not further used, because we take the specialized |
561 --{* Note that @{term E} is not further used, because we take the specialized |
571 sets that also consider if the expression evaluates to true or false. |
562 sets that also consider if the expression evaluates to true or false. |
572 Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break |
563 Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break |
573 map of @{term E} will be the trivial one. So |
564 map of @{term E} will be the trivial one. So |
574 @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to enshure the definite assignment in |
565 @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to ensure the definite assignment in |
575 expression @{term e}. |
566 expression @{term e}. |
576 Notice the implicit analysis of a constant boolean expression @{term e} |
567 Notice the implicit analysis of a constant boolean expression @{term e} |
577 in this rule. For example, if @{term e} is constantly @{term True} then |
568 in this rule. For example, if @{term e} is constantly @{term True} then |
578 @{term "assigns_if False e = UNIV"} and therefor @{term "nrm C2=UNIV"}. |
569 @{term "assigns_if False e = UNIV"} and therefor @{term "nrm C2=UNIV"}. |
579 So finally @{term "nrm A = nrm C1"}. For the break maps this trick |
570 So finally @{term "nrm A = nrm C1"}. For the break maps this trick |
600 only handles continue labels, not break labels. The break label will be |
591 only handles continue labels, not break labels. The break label will be |
601 handled by an enclosing @{term Lab} statement. So we don't have to |
592 handled by an enclosing @{term Lab} statement. So we don't have to |
602 handle the breaks specially. |
593 handle the breaks specially. |
603 *} |
594 *} |
604 |
595 |
605 Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B; |
596 | Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B; |
606 nrm A = UNIV; |
597 nrm A = UNIV; |
607 brk A = (case jump of |
598 brk A = (case jump of |
608 Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV |
599 Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV |
609 | Cont l \<Rightarrow> \<lambda> k. UNIV |
600 | Cont l \<Rightarrow> \<lambda> k. UNIV |
610 | Ret \<Rightarrow> \<lambda> k. UNIV)\<rbrakk> |
601 | Ret \<Rightarrow> \<lambda> k. UNIV)\<rbrakk> |
611 \<Longrightarrow> |
602 \<Longrightarrow> |
612 Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A" |
603 Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A" |
613 --{* In case of a break to label @{term l} the corresponding break set is all |
604 --{* In case of a break to label @{term l} the corresponding break set is all |
614 variables assigned before the break. The assigned variables for normal |
605 variables assigned before the break. The assigned variables for normal |
615 completion of the @{term Jmp} is @{term UNIV}, because the statement will |
606 completion of the @{term Jmp} is @{term UNIV}, because the statement will |
616 never complete normally. For continue and return the break map is the |
607 never complete normally. For continue and return the break map is the |
617 trivial one. In case of a return we enshure that the result value is |
608 trivial one. In case of a return we enshure that the result value is |
618 assigned. |
609 assigned. |
619 *} |
610 *} |
620 |
611 |
621 Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk> |
612 | Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk> |
622 \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A" |
613 \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A" |
623 |
614 |
624 Try: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
615 | Try: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
625 Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
616 Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
626 nrm A = nrm C1 \<inter> nrm C2; |
617 nrm A = nrm C1 \<inter> nrm C2; |
627 brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk> |
618 brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk> |
628 \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A" |
619 \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A" |
629 |
620 |
630 Fin: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
621 | Fin: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
631 Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
622 Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
632 nrm A = nrm C1 \<union> nrm C2; |
623 nrm A = nrm C1 \<union> nrm C2; |
633 brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk> |
624 brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk> |
634 \<Longrightarrow> |
625 \<Longrightarrow> |
635 Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" |
626 Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" |
636 --{* The set of assigned variables before execution @{term c2} are the same |
627 --{* The set of assigned variables before execution @{term c2} are the same |
637 as before execution @{term c1}, because @{term c1} could throw an exception |
628 as before execution @{term c1}, because @{term c1} could throw an exception |
638 and so we can't guarantee that any variable will be assigned in @{term c1}. |
629 and so we can't guarantee that any variable will be assigned in @{term c1}. |
639 The @{text Finally} statement completes |
630 The @{text Finally} statement completes |
640 normally if both @{term c1} and @{term c2} complete normally. If @{term c1} |
631 normally if both @{term c1} and @{term c2} complete normally. If @{term c1} |
669 to fit to these circumstances. If an initialization is involved during |
660 to fit to these circumstances. If an initialization is involved during |
670 evaluation of the expression (evaluation rules @{text FVar}, @{text NewC} |
661 evaluation of the expression (evaluation rules @{text FVar}, @{text NewC} |
671 and @{text NewA} |
662 and @{text NewA} |
672 *} |
663 *} |
673 |
664 |
674 Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
665 | Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
675 --{* Wellformedness of a program will ensure, that every static initialiser |
666 --{* Wellformedness of a program will ensure, that every static initialiser |
676 is definetly assigned and the jumps are nested correctly. The case here |
667 is definetly assigned and the jumps are nested correctly. The case here |
677 for @{term Init} is just for convenience, to get a proper precondition |
668 for @{term Init} is just for convenience, to get a proper precondition |
678 for the induction hypothesis in various proofs, so that we don't have to |
669 for the induction hypothesis in various proofs, so that we don't have to |
679 expand the initialisation on every point where it is triggerred by the |
670 expand the initialisation on every point where it is triggerred by the |
680 evaluation rules. |
671 evaluation rules. |
681 *} |
672 *} |
682 NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
673 | NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
683 |
674 |
684 NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
675 | NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
685 \<Longrightarrow> |
676 \<Longrightarrow> |
686 Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A" |
677 Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A" |
687 |
678 |
688 Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
679 | Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
689 \<Longrightarrow> |
680 \<Longrightarrow> |
690 Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A" |
681 Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A" |
691 |
682 |
692 Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
683 | Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
693 \<Longrightarrow> |
684 \<Longrightarrow> |
694 Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A" |
685 Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A" |
695 |
686 |
696 Lit: "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
687 | Lit: "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
697 |
688 |
698 UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
689 | UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
699 \<Longrightarrow> |
690 \<Longrightarrow> |
700 Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A" |
691 Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A" |
701 |
692 |
702 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; |
693 | 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; |
703 nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> |
694 nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> |
704 assigns_if False (BinOp CondAnd e1 e2)); |
695 assigns_if False (BinOp CondAnd e1 e2)); |
|
696 brk A = (\<lambda> l. UNIV) \<rbrakk> |
|
697 \<Longrightarrow> |
|
698 Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A" |
|
699 |
|
700 | 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; |
|
701 nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> |
|
702 assigns_if False (BinOp CondOr e1 e2)); |
705 brk A = (\<lambda> l. UNIV) \<rbrakk> |
703 brk A = (\<lambda> l. UNIV) \<rbrakk> |
706 \<Longrightarrow> |
704 \<Longrightarrow> |
707 Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A" |
705 Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A" |
708 |
706 |
709 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; |
707 | BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A; |
710 nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> |
708 binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk> |
711 assigns_if False (BinOp CondOr e1 e2)); |
709 \<Longrightarrow> |
712 brk A = (\<lambda> l. UNIV) \<rbrakk> |
710 Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A" |
713 \<Longrightarrow> |
711 |
714 Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A" |
712 | Super: "This \<in> B |
715 |
713 \<Longrightarrow> |
716 BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A; |
714 Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
717 binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk> |
715 |
718 \<Longrightarrow> |
716 | AccLVar: "\<lbrakk>vn \<in> B; |
719 Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A" |
717 nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk> |
720 |
718 \<Longrightarrow> |
721 Super: "This \<in> B |
719 Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A" |
722 \<Longrightarrow> |
|
723 Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
|
724 |
|
725 AccLVar: "\<lbrakk>vn \<in> B; |
|
726 nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk> |
|
727 \<Longrightarrow> |
|
728 Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A" |
|
729 --{* To properly access a local variable we have to test the definite |
720 --{* To properly access a local variable we have to test the definite |
730 assignment here. The variable must occur in the set @{term B} |
721 assignment here. The variable must occur in the set @{term B} |
731 *} |
722 *} |
732 |
723 |
733 Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; |
724 | Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; |
734 Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk> |
725 Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk> |
735 \<Longrightarrow> |
726 \<Longrightarrow> |
736 Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A" |
727 Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A" |
737 |
728 |
738 AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk> |
729 | AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk> |
739 \<Longrightarrow> |
730 \<Longrightarrow> |
740 Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A" |
731 Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A" |
741 |
732 |
742 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> |
733 | 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> |
743 \<Longrightarrow> |
734 \<Longrightarrow> |
744 Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A" |
735 Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A" |
745 |
736 |
746 CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean); |
737 | CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean); |
747 Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; |
738 Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; |
748 Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; |
739 Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; |
749 Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
740 Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
750 nrm A = B \<union> (assigns_if True (c ? e1 : e2) \<inter> |
741 nrm A = B \<union> (assigns_if True (c ? e1 : e2) \<inter> |
751 assigns_if False (c ? e1 : e2)); |
742 assigns_if False (c ? e1 : e2)); |
752 brk A = (\<lambda> l. UNIV)\<rbrakk> |
743 brk A = (\<lambda> l. UNIV)\<rbrakk> |
753 \<Longrightarrow> |
744 \<Longrightarrow> |
754 Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" |
745 Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" |
755 |
746 |
756 Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean); |
747 | Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean); |
757 Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; |
748 Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; |
758 Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; |
749 Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; |
759 Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
750 Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
760 nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk> |
751 nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk> |
761 \<Longrightarrow> |
752 \<Longrightarrow> |
762 Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" |
753 Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" |
763 |
754 |
764 Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk> |
755 | Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk> |
765 \<Longrightarrow> |
756 \<Longrightarrow> |
766 Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A" |
757 Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A" |
767 |
758 |
768 -- {* The interplay of @{term Call}, @{term Methd} and @{term Body}: |
759 -- {* The interplay of @{term Call}, @{term Methd} and @{term Body}: |
769 Why rules for @{term Methd} and @{term Body} at all? Note that a |
760 Why rules for @{term Methd} and @{term Body} at all? Note that a |
770 Java source program will not include bare @{term Methd} or @{term Body} |
761 Java source program will not include bare @{term Methd} or @{term Body} |
771 terms. These terms are just introduced during evaluation. So definite |
762 terms. These terms are just introduced during evaluation. So definite |
784 rules, and therefor we have to establish the definite assignment of the |
775 rules, and therefor we have to establish the definite assignment of the |
785 sub-evaluation during the type-safety proof. Note that well-typedness is |
776 sub-evaluation during the type-safety proof. Note that well-typedness is |
786 also a precondition for type-safety and so we can omit some assertion |
777 also a precondition for type-safety and so we can omit some assertion |
787 that are already ensured by well-typedness. |
778 that are already ensured by well-typedness. |
788 *} |
779 *} |
789 Methd: "\<lbrakk>methd (prg Env) D sig = Some m; |
780 | Methd: "\<lbrakk>methd (prg Env) D sig = Some m; |
790 Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A |
781 Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A |
791 \<rbrakk> |
782 \<rbrakk> |
|
783 \<Longrightarrow> |
|
784 Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A" |
|
785 |
|
786 | Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C; |
|
787 nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk> |
792 \<Longrightarrow> |
788 \<Longrightarrow> |
793 Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A" |
789 Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A" |
794 |
|
795 Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C; |
|
796 nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk> |
|
797 \<Longrightarrow> |
|
798 Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A" |
|
799 -- {* Note that @{term A} is not correlated to @{term C}. If the body |
790 -- {* Note that @{term A} is not correlated to @{term C}. If the body |
800 statement returns abruptly with return, evaluation of @{term Body} |
791 statement returns abruptly with return, evaluation of @{term Body} |
801 will absorb this return and complete normally. So we cannot trivially |
792 will absorb this return and complete normally. So we cannot trivially |
802 get the assigned variables of the body statement since it has not |
793 get the assigned variables of the body statement since it has not |
803 completed normally or with a break. |
794 completed normally or with a break. |
807 definite assignment only talks about normal completion and breaks. So |
798 definite assignment only talks about normal completion and breaks. So |
808 for a return the @{term Jump} rule ensures that the result variable is |
799 for a return the @{term Jump} rule ensures that the result variable is |
809 set and then this information must be carried over to the @{term Body} |
800 set and then this information must be carried over to the @{term Body} |
810 rule by the conformance predicate of the state. |
801 rule by the conformance predicate of the state. |
811 *} |
802 *} |
812 LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" |
803 | LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" |
813 |
804 |
814 FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
805 | FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
815 \<Longrightarrow> |
|
816 Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" |
|
817 |
|
818 AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk> |
|
819 \<Longrightarrow> |
806 \<Longrightarrow> |
820 Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" |
807 Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" |
821 |
808 |
822 Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" |
809 | AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk> |
823 |
810 \<Longrightarrow> |
824 Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk> |
811 Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" |
825 \<Longrightarrow> |
812 |
826 Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A" |
813 | Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" |
|
814 |
|
815 | Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk> |
|
816 \<Longrightarrow> |
|
817 Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A" |
827 |
818 |
828 |
819 |
829 declare inj_term_sym_simps [simp] |
820 declare inj_term_sym_simps [simp] |
830 declare assigns_if.simps [simp del] |
821 declare assigns_if.simps [simp del] |
831 declare split_paired_All [simp del] split_paired_Ex [simp del] |
822 declare split_paired_All [simp del] split_paired_Ex [simp del] |
832 ML_setup {* |
823 ML_setup {* |
833 change_simpset (fn ss => ss delloop "split_all_tac"); |
824 change_simpset (fn ss => ss delloop "split_all_tac"); |
834 *} |
825 *} |
835 inductive_cases da_elim_cases [cases set]: |
826 inductive_cases2 da_elim_cases [cases set]: |
836 "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" |
827 "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" |
837 "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" |
828 "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" |
838 "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A" |
829 "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A" |
839 "Env\<turnstile> B \<guillemotright>In1r (Expr e)\<guillemotright> A" |
830 "Env\<turnstile> B \<guillemotright>In1r (Expr e)\<guillemotright> A" |
840 "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> c\<rangle>\<guillemotright> A" |
831 "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> c\<rangle>\<guillemotright> A" |
1591 have B': "B \<subseteq> B'" . |
1582 have B': "B \<subseteq> B'" . |
1592 with Super.hyps have "This \<in> B' " |
1583 with Super.hyps have "This \<in> B' " |
1593 by auto |
1584 by auto |
1594 thus ?case by (iprover intro: da.Super) |
1585 thus ?case by (iprover intro: da.Super) |
1595 next |
1586 next |
1596 case (AccLVar A B Env vn B') |
1587 case (AccLVar vn B A Env B') |
1597 have "vn \<in> B" . |
1588 have "vn \<in> B" . |
1598 moreover |
1589 moreover |
1599 have "B \<subseteq> B'" . |
1590 have "B \<subseteq> B'" . |
1600 ultimately have "vn \<in> B'" by auto |
1591 ultimately have "vn \<in> B'" by auto |
1601 thus ?case by (iprover intro: da.AccLVar) |
1592 thus ?case by (iprover intro: da.AccLVar) |
1602 next |
1593 next |
1603 case Acc thus ?case by (iprover intro: da.Acc) |
1594 case Acc thus ?case by (iprover intro: da.Acc) |
1604 next |
1595 next |
1605 case (AssLVar A B E Env e vn B') |
1596 case (AssLVar Env B e E A vn B') |
1606 have B': "B \<subseteq> B'" . |
1597 have B': "B \<subseteq> B'" . |
1607 then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" |
1598 then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" |
1608 by (rule AssLVar.hyps [elim_format]) iprover |
1599 by (rule AssLVar.hyps [elim_format]) iprover |
1609 then obtain A' where |
1600 then obtain A' where |
1610 "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'" |
1601 "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'" |
1611 by (iprover intro: da.AssLVar) |
1602 by (iprover intro: da.AssLVar) |
1612 thus ?case .. |
1603 thus ?case .. |
1613 next |
1604 next |
1614 case (Ass A B Env V e v B') |
1605 case (Ass v Env B V e A B') |
1615 have B': "B \<subseteq> B'" . |
1606 have B': "B \<subseteq> B'" . |
1616 have "\<forall>vn. v \<noteq> LVar vn". |
1607 have "\<forall>vn. v \<noteq> LVar vn". |
1617 moreover |
1608 moreover |
1618 obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'" |
1609 obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'" |
1619 proof - |
1610 proof - |