30 "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'" |
30 "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'" |
31 by (auto simp:wq_def Let_def cp_def split:list.splits) |
31 by (auto simp:wq_def Let_def cp_def split:list.splits) |
32 |
32 |
33 context valid_trace |
33 context valid_trace |
34 begin |
34 begin |
|
35 |
|
36 lemma actor_inv: |
|
37 assumes "PIP s e" |
|
38 and "\<not> isCreate e" |
|
39 shows "actor e \<in> runing s" |
|
40 using assms |
|
41 by (induct, auto) |
35 |
42 |
36 lemma ind [consumes 0, case_names Nil Cons, induct type]: |
43 lemma ind [consumes 0, case_names Nil Cons, induct type]: |
37 assumes "PP []" |
44 assumes "PP []" |
38 and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow> |
45 and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow> |
39 PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))" |
46 PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))" |
1617 qed |
1624 qed |
1618 moreover from cs_not_in |
1625 moreover from cs_not_in |
1619 have "cs \<notin> (holdents (V thread cs#s) thread)" by auto |
1626 have "cs \<notin> (holdents (V thread cs#s) thread)" by auto |
1620 ultimately show ?thesis by (simp add:cntCS_def) |
1627 ultimately show ?thesis by (simp add:cntCS_def) |
1621 qed |
1628 qed |
|
1629 |
|
1630 lemma count_rec1 [simp]: |
|
1631 assumes "Q e" |
|
1632 shows "count Q (e#es) = Suc (count Q es)" |
|
1633 using assms |
|
1634 by (unfold count_def, auto) |
|
1635 |
|
1636 lemma count_rec2 [simp]: |
|
1637 assumes "\<not>Q e" |
|
1638 shows "count Q (e#es) = (count Q es)" |
|
1639 using assms |
|
1640 by (unfold count_def, auto) |
|
1641 |
|
1642 lemma count_rec3 [simp]: |
|
1643 shows "count Q [] = 0" |
|
1644 by (unfold count_def, auto) |
|
1645 |
|
1646 lemma cntP_diff_inv: |
|
1647 assumes "cntP (e#s) th \<noteq> cntP s th" |
|
1648 shows "isP e \<and> actor e = th" |
|
1649 proof(cases e) |
|
1650 case (P th' pty) |
|
1651 show ?thesis |
|
1652 by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", |
|
1653 insert assms P, auto simp:cntP_def) |
|
1654 qed (insert assms, auto simp:cntP_def) |
|
1655 |
|
1656 lemma isP_E: |
|
1657 assumes "isP e" |
|
1658 obtains cs where "e = P (actor e) cs" |
|
1659 using assms by (cases e, auto) |
|
1660 |
|
1661 lemma isV_E: |
|
1662 assumes "isV e" |
|
1663 obtains cs where "e = V (actor e) cs" |
|
1664 using assms by (cases e, auto) (* ccc *) |
|
1665 |
|
1666 lemma cntV_diff_inv: |
|
1667 assumes "cntV (e#s) th \<noteq> cntV s th" |
|
1668 shows "isV e \<and> actor e = th" |
|
1669 proof(cases e) |
|
1670 case (V th' pty) |
|
1671 show ?thesis |
|
1672 by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", |
|
1673 insert assms V, auto simp:cntV_def) |
|
1674 qed (insert assms, auto simp:cntV_def) |
1622 |
1675 |
1623 context valid_trace |
1676 context valid_trace |
1624 begin |
1677 begin |
1625 |
1678 |
1626 text {* (* ddd *) \noindent |
1679 text {* (* ddd *) \noindent |