211 prefer 26 |
211 prefer 26 |
212 apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *) |
212 apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *) |
213 apply (auto del: conjI dest!: not_initedD gext_new sxalloc_gext halloc_gext |
213 apply (auto del: conjI dest!: not_initedD gext_new sxalloc_gext halloc_gext |
214 simp add: lvar_def fvar_def2 avar_def2 init_lvars_def2 |
214 simp add: lvar_def fvar_def2 avar_def2 init_lvars_def2 |
215 check_field_access_def check_method_access_def Let_def |
215 check_field_access_def check_method_access_def Let_def |
216 split del: if_split_asm split add: sum3.split) |
216 split del: if_split_asm split: sum3.split) |
217 (* 6 subgoals *) |
217 (* 6 subgoals *) |
218 apply force+ |
218 apply force+ |
219 done |
219 done |
220 |
220 |
221 lemma evar_gext_f: |
221 lemma evar_gext_f: |
630 \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> |
630 \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> |
631 \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC" |
631 \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC" |
632 apply (case_tac "mode = IntVir") |
632 apply (case_tac "mode = IntVir") |
633 apply (drule conf_RefTD) |
633 apply (drule conf_RefTD) |
634 apply (force intro!: conf_AddrI |
634 apply (force intro!: conf_AddrI |
635 simp add: obj_class_def split add: obj_tag.split_asm) |
635 simp add: obj_class_def split: obj_tag.split_asm) |
636 apply clarsimp |
636 apply clarsimp |
637 apply safe |
637 apply safe |
638 apply (erule (1) widen.subcls [THEN conf_widen]) |
638 apply (erule (1) widen.subcls [THEN conf_widen]) |
639 apply (erule wf_ws_prog) |
639 apply (erule wf_ws_prog) |
640 |
640 |
653 apply simp |
653 apply simp |
654 done |
654 done |
655 |
655 |
656 lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L); |
656 lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L); |
657 x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)" |
657 x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)" |
658 apply (auto split add: split_abrupt_if simp add: throw_def2) |
658 apply (auto split: split_abrupt_if simp add: throw_def2) |
659 apply (erule conforms_xconf) |
659 apply (erule conforms_xconf) |
660 apply (frule conf_RefTD) |
660 apply (frule conf_RefTD) |
661 apply (auto elim: widen.subcls [THEN conf_widen]) |
661 apply (auto elim: widen.subcls [THEN conf_widen]) |
662 done |
662 done |
663 |
663 |
672 |
672 |
673 lemma Fin_lemma: |
673 lemma Fin_lemma: |
674 "\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L); |
674 "\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L); |
675 dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> |
675 dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> |
676 \<Longrightarrow> (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)" |
676 \<Longrightarrow> (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)" |
677 apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if) |
677 apply (auto elim: eval_gext' conforms_xgext split: split_abrupt_if) |
678 done |
678 done |
679 |
679 |
680 lemma FVar_lemma1: |
680 lemma FVar_lemma1: |
681 "\<lbrakk>table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; |
681 "\<lbrakk>table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; |
682 x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class statC; wf_prog G; G\<turnstile>statC\<preceq>\<^sub>C statDeclC; |
682 x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class statC; wf_prog G; G\<turnstile>statC\<preceq>\<^sub>C statDeclC; |
698 apply (rule var_tys_Some_eq [THEN iffD2]) |
698 apply (rule var_tys_Some_eq [THEN iffD2]) |
699 apply clarsimp |
699 apply clarsimp |
700 apply (erule fields_table_SomeI, simp (no_asm)) |
700 apply (erule fields_table_SomeI, simp (no_asm)) |
701 apply clarsimp |
701 apply clarsimp |
702 apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2]) |
702 apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2]) |
703 apply (auto dest!: widen_Array split add: obj_tag.split) |
703 apply (auto dest!: widen_Array split: obj_tag.split) |
704 apply (rule fields_table_SomeI) |
704 apply (rule fields_table_SomeI) |
705 apply (auto elim!: fields_mono subcls_is_class2) |
705 apply (auto elim!: fields_mono subcls_is_class2) |
706 done |
706 done |
707 |
707 |
708 lemma FVar_lemma2: "error_free state |
708 lemma FVar_lemma2: "error_free state |
827 lemma lconf_map_lname [simp]: |
827 lemma lconf_map_lname [simp]: |
828 "G,s\<turnstile>(case_lname l1 l2)[\<Colon>\<preceq>](case_lname L1 L2) |
828 "G,s\<turnstile>(case_lname l1 l2)[\<Colon>\<preceq>](case_lname L1 L2) |
829 = |
829 = |
830 (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
830 (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
831 apply (unfold lconf_def) |
831 apply (unfold lconf_def) |
832 apply (auto split add: lname.splits) |
832 apply (auto split: lname.splits) |
833 done |
833 done |
834 |
834 |
835 lemma wlconf_map_lname [simp]: |
835 lemma wlconf_map_lname [simp]: |
836 "G,s\<turnstile>(case_lname l1 l2)[\<sim>\<Colon>\<preceq>](case_lname L1 L2) |
836 "G,s\<turnstile>(case_lname l1 l2)[\<sim>\<Colon>\<preceq>](case_lname L1 L2) |
837 = |
837 = |
838 (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
838 (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
839 apply (unfold wlconf_def) |
839 apply (unfold wlconf_def) |
840 apply (auto split add: lname.splits) |
840 apply (auto split: lname.splits) |
841 done |
841 done |
842 |
842 |
843 lemma lconf_map_ename [simp]: |
843 lemma lconf_map_ename [simp]: |
844 "G,s\<turnstile>(case_ename l1 l2)[\<Colon>\<preceq>](case_ename L1 L2) |
844 "G,s\<turnstile>(case_ename l1 l2)[\<Colon>\<preceq>](case_ename L1 L2) |
845 = |
845 = |
846 (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
846 (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
847 apply (unfold lconf_def) |
847 apply (unfold lconf_def) |
848 apply (auto split add: ename.splits) |
848 apply (auto split: ename.splits) |
849 done |
849 done |
850 |
850 |
851 lemma wlconf_map_ename [simp]: |
851 lemma wlconf_map_ename [simp]: |
852 "G,s\<turnstile>(case_ename l1 l2)[\<sim>\<Colon>\<preceq>](case_ename L1 L2) |
852 "G,s\<turnstile>(case_ename l1 l2)[\<sim>\<Colon>\<preceq>](case_ename L1 L2) |
853 = |
853 = |
854 (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
854 (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))" |
855 apply (unfold wlconf_def) |
855 apply (unfold wlconf_def) |
856 apply (auto split add: ename.splits) |
856 apply (auto split: ename.splits) |
857 done |
857 done |
858 |
858 |
859 |
859 |
860 |
860 |
861 lemma defval_conf1 [rule_format (no_asm), elim]: |
861 lemma defval_conf1 [rule_format (no_asm), elim]: |
900 | Res \<Rightarrow> Some (resTy (mthd dm))) |
900 | Res \<Rightarrow> Some (resTy (mthd dm))) |
901 | This \<Rightarrow> if (is_static (mthd sm)) |
901 | This \<Rightarrow> if (is_static (mthd sm)) |
902 then None else Some (Class declC)))" |
902 then None else Some (Class declC)))" |
903 apply (simp add: init_lvars_def2) |
903 apply (simp add: init_lvars_def2) |
904 apply (rule conforms_set_locals) |
904 apply (rule conforms_set_locals) |
905 apply (simp (no_asm_simp) split add: if_split) |
905 apply (simp (no_asm_simp) split: if_split) |
906 apply (drule (4) DynT_conf) |
906 apply (drule (4) DynT_conf) |
907 apply clarsimp |
907 apply clarsimp |
908 (* apply intro *) |
908 (* apply intro *) |
909 apply (drule (3) conforms_init_lvars_lemma |
909 apply (drule (3) conforms_init_lvars_lemma |
910 [where ?lvars="(lcls (mbody (mthd dm)))"]) |
910 [where ?lvars="(lcls (mbody (mthd dm)))"]) |