equal
deleted
inserted
replaced
2070 by (unfold s_depend_def, auto simp:cs_waiting_def) |
2070 by (unfold s_depend_def, auto simp:cs_waiting_def) |
2071 from wq_threads [OF vt this] show ?thesis . |
2071 from wq_threads [OF vt this] show ?thesis . |
2072 qed |
2072 qed |
2073 |
2073 |
2074 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" |
2074 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" |
2075 proof(unfold cp_def wq_def, induct s) |
2075 unfolding cp_def wq_def |
2076 case (Cons e s') |
2076 apply(induct s rule: schs.induct) |
2077 show ?case |
2077 apply(simp add: Let_def cpreced_initial) |
2078 by (auto simp:Let_def) |
2078 apply(simp add: Let_def) |
2079 next |
2079 apply(simp add: Let_def) |
2080 case Nil |
2080 apply(simp add: Let_def) |
2081 show ?case by (auto simp:Let_def) |
2081 apply(subst (2) schs.simps) |
2082 qed |
2082 apply(simp add: Let_def) |
|
2083 apply(subst (2) schs.simps) |
|
2084 apply(simp add: Let_def) |
|
2085 done |
2083 |
2086 |
2084 |
2087 |
2085 lemma runing_unique: |
2088 lemma runing_unique: |
2086 fixes th1 th2 s |
2089 fixes th1 th2 s |
2087 assumes vt: "vt step s" |
2090 assumes vt: "vt step s" |