equal
deleted
inserted
replaced
802 apply(ind_cases " step s (P (hd (wq s cs)) cs)") |
802 apply(ind_cases " step s (P (hd (wq s cs)) cs)") |
803 apply(simp add:s_RAG_def wq_def cs_holding_def) |
803 apply(simp add:s_RAG_def wq_def cs_holding_def) |
804 apply(auto) |
804 apply(auto) |
805 done |
805 done |
806 |
806 |
807 (* FIXME: Unused |
|
808 lemma simple_A: |
|
809 fixes A |
|
810 assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y" |
|
811 shows "A = {} \<or> (\<exists> a. A = {a})" |
|
812 proof(cases "A = {}") |
|
813 case True thus ?thesis by simp |
|
814 next |
|
815 case False then obtain a where "a \<in> A" by auto |
|
816 with h have "A = {a}" by auto |
|
817 thus ?thesis by simp |
|
818 qed |
|
819 *) |
|
820 |
807 |
821 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs" |
808 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs" |
822 by (unfold s_RAG_def, auto) |
809 by (unfold s_RAG_def, auto) |
823 |
810 |
824 lemma acyclic_RAG: |
811 lemma acyclic_RAG: |
2090 apply(simp add: Let_def) |
2077 apply(simp add: Let_def) |
2091 apply(subst (2) schs.simps) |
2078 apply(subst (2) schs.simps) |
2092 apply(simp add: Let_def) |
2079 apply(simp add: Let_def) |
2093 done |
2080 done |
2094 |
2081 |
2095 |
2082 (* FIXME: NOT NEEDED *) |
2096 lemma runing_unique: |
2083 lemma runing_unique: |
2097 fixes th1 th2 s |
2084 fixes th1 th2 s |
2098 assumes vt: "vt s" |
2085 assumes vt: "vt s" |
2099 and runing_1: "th1 \<in> runing s" |
2086 and runing_1: "th1 \<in> runing s" |
2100 and runing_2: "th2 \<in> runing s" |
2087 and runing_2: "th2 \<in> runing s" |
2278 from runing_2 show "th2 \<in> readys s" by (simp add:runing_def) |
2265 from runing_2 show "th2 \<in> readys s" by (simp add:runing_def) |
2279 qed |
2266 qed |
2280 qed |
2267 qed |
2281 qed |
2268 qed |
2282 qed |
2269 qed |
|
2270 |
2283 |
2271 |
2284 lemma create_pre: |
2272 lemma create_pre: |
2285 assumes stp: "step s e" |
2273 assumes stp: "step s e" |
2286 and not_in: "th \<notin> threads s" |
2274 and not_in: "th \<notin> threads s" |
2287 and is_in: "th \<in> threads (e#s)" |
2275 and is_in: "th \<in> threads (e#s)" |