equal
deleted
inserted
replaced
67 |
67 |
68 lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object" |
68 lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object" |
69 apply (unfold is_class_def) |
69 apply (unfold is_class_def) |
70 apply (simp (no_asm_simp)) |
70 apply (simp (no_asm_simp)) |
71 done |
71 done |
|
72 |
|
73 lemma is_class_xcpt [simp]: "wf_prog wf_mb G \<Longrightarrow> is_class G (Xcpt x)" |
|
74 apply (simp add: wf_prog_def wf_syscls_def) |
|
75 apply (simp add: is_class_def class_def) |
|
76 apply clarify |
|
77 apply (erule_tac x = x in allE) |
|
78 apply clarify |
|
79 apply (auto intro!: map_of_SomeI) |
|
80 done |
72 |
81 |
73 lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+" |
82 lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+" |
74 apply( frule r_into_trancl) |
83 apply( frule r_into_trancl) |
75 apply( drule subcls1D) |
84 apply( drule subcls1D) |
76 apply(clarify) |
85 apply(clarify) |