equal
deleted
inserted
replaced
543 by auto |
543 by auto |
544 |
544 |
545 lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object" |
545 lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object" |
546 apply (case_tac T) |
546 apply (case_tac T) |
547 apply (auto) |
547 apply (auto) |
548 apply (subgoal_tac "G\<turnstile>pid_field_type\<preceq>\<^sub>C Object") |
548 apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object") |
549 apply (auto intro: subcls_ObjectI) |
549 apply (auto intro: subcls_ObjectI) |
550 done |
550 done |
551 |
551 |
552 lemma widen_trans_lemma [rule_format (no_asm)]: |
552 lemma widen_trans_lemma [rule_format (no_asm)]: |
553 "\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T" |
553 "\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T" |