12 apply (simp add:s2ss_def) |
12 apply (simp add:s2ss_def) |
13 apply (tactic {*my_seteq_tac 1*}) |
13 apply (tactic {*my_seteq_tac 1*}) |
14 apply (rule_tac x = obj in exI) |
14 apply (rule_tac x = obj in exI) |
15 thm co2sobj_other |
15 thm co2sobj_other |
16 apply (simp add:co2sobj_other) |
16 apply (simp add:co2sobj_other) |
17 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
17 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
18 apply (tactic {*my_setiff_tac 1*}) |
18 apply (tactic {*my_setiff_tac 1*}) |
19 apply (rule_tac x = obj in exI) |
19 apply (rule_tac x = obj in exI) |
20 apply (frule_tac obj = obj in co2sobj_other) |
20 apply (frule_tac obj = obj in co2sobj_other) |
21 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
21 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
22 done |
22 done |
23 |
23 |
24 lemma s2ss_bind: |
24 lemma s2ss_bind: |
25 "valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s" |
25 "valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s" |
26 apply (simp add:s2ss_def) |
26 apply (simp add:s2ss_def) |
27 apply (tactic {*my_seteq_tac 1*}) |
27 apply (tactic {*my_seteq_tac 1*}) |
28 apply (rule_tac x = obj in exI) |
28 apply (rule_tac x = obj in exI) |
29 apply (simp add:co2sobj_other) |
29 apply (simp add:co2sobj_other) |
30 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
30 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
31 apply (tactic {*my_setiff_tac 1*}) |
31 apply (tactic {*my_setiff_tac 1*}) |
32 apply (rule_tac x = obj in exI) |
32 apply (rule_tac x = obj in exI) |
33 apply (frule_tac obj = obj in co2sobj_other) |
33 apply (frule_tac obj = obj in co2sobj_other) |
34 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
34 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
35 done |
35 done |
36 |
36 |
37 lemma s2ss_connect: |
37 lemma s2ss_connect: |
38 "valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s" |
38 "valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s" |
39 apply (simp add:s2ss_def) |
39 apply (simp add:s2ss_def) |
40 apply (tactic {*my_seteq_tac 1*}) |
40 apply (tactic {*my_seteq_tac 1*}) |
41 apply (rule_tac x = obj in exI) |
41 apply (rule_tac x = obj in exI) |
42 apply (simp add:co2sobj_other) |
42 apply (simp add:co2sobj_other) |
43 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
43 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
44 apply (tactic {*my_setiff_tac 1*}) |
44 apply (tactic {*my_setiff_tac 1*}) |
45 apply (rule_tac x = obj in exI) |
45 apply (rule_tac x = obj in exI) |
46 apply (frule_tac obj = obj in co2sobj_other) |
46 apply (frule_tac obj = obj in co2sobj_other) |
47 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
47 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
48 done |
48 done |
49 |
49 |
50 lemma s2ss_listen: |
50 lemma s2ss_listen: |
51 "valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s" |
51 "valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s" |
52 apply (simp add:s2ss_def) |
52 apply (simp add:s2ss_def) |
53 apply (tactic {*my_seteq_tac 1*}) |
53 apply (tactic {*my_seteq_tac 1*}) |
54 apply (rule_tac x = obj in exI) |
54 apply (rule_tac x = obj in exI) |
55 apply (simp add:co2sobj_other) |
55 apply (simp add:co2sobj_other) |
56 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
56 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
57 apply (tactic {*my_setiff_tac 1*}) |
57 apply (tactic {*my_setiff_tac 1*}) |
58 apply (rule_tac x = obj in exI) |
58 apply (rule_tac x = obj in exI) |
59 apply (frule_tac obj = obj in co2sobj_other) |
59 apply (frule_tac obj = obj in co2sobj_other) |
60 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
60 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
61 done |
61 done |
62 |
62 |
63 lemma s2ss_accept: |
63 lemma s2ss_accept: |
64 "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s" |
64 "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s" |
65 apply (simp add:s2ss_def) |
65 apply (simp add:s2ss_def) |
66 apply (tactic {*my_seteq_tac 1*}) |
66 apply (tactic {*my_seteq_tac 1*}) |
67 apply (rule_tac x = obj in exI) |
67 apply (rule_tac x = obj in exI) |
68 apply (simp add:co2sobj_other) |
68 apply (simp add:co2sobj_other) |
69 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
69 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
70 apply (tactic {*my_setiff_tac 1*}) |
70 apply (tactic {*my_setiff_tac 1*}) |
71 apply (rule_tac x = obj in exI) |
71 apply (rule_tac x = obj in exI) |
72 apply (frule_tac obj = obj in co2sobj_other) |
72 apply (frule_tac obj = obj in co2sobj_other) |
73 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
73 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
74 done |
74 done |
75 |
75 |
76 lemma s2ss_send: |
76 lemma s2ss_send: |
77 "valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s" |
77 "valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s" |
78 apply (simp add:s2ss_def) |
78 apply (simp add:s2ss_def) |
79 apply (tactic {*my_seteq_tac 1*}) |
79 apply (tactic {*my_seteq_tac 1*}) |
80 apply (rule_tac x = obj in exI) |
80 apply (rule_tac x = obj in exI) |
81 apply (simp add:co2sobj_other) |
81 apply (simp add:co2sobj_other) |
82 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
82 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
83 apply (tactic {*my_setiff_tac 1*}) |
83 apply (tactic {*my_setiff_tac 1*}) |
84 apply (rule_tac x = obj in exI) |
84 apply (rule_tac x = obj in exI) |
85 apply (frule_tac obj = obj in co2sobj_other) |
85 apply (frule_tac obj = obj in co2sobj_other) |
86 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
86 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
87 done |
87 done |
88 |
88 |
89 lemma s2ss_recv: |
89 lemma s2ss_recv: |
90 "valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s" |
90 "valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s" |
91 apply (simp add:s2ss_def) |
91 apply (simp add:s2ss_def) |
92 apply (tactic {*my_seteq_tac 1*}) |
92 apply (tactic {*my_seteq_tac 1*}) |
93 apply (rule_tac x = obj in exI) |
93 apply (rule_tac x = obj in exI) |
94 apply (simp add:co2sobj_other) |
94 apply (simp add:co2sobj_other) |
95 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
95 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
96 apply (tactic {*my_setiff_tac 1*}) |
96 apply (tactic {*my_setiff_tac 1*}) |
97 apply (rule_tac x = obj in exI) |
97 apply (rule_tac x = obj in exI) |
98 apply (frule_tac obj = obj in co2sobj_other) |
98 apply (frule_tac obj = obj in co2sobj_other) |
99 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
99 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
100 done |
100 done |
101 |
101 |
102 lemma s2ss_shutdown: |
102 lemma s2ss_shutdown: |
103 "valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s" |
103 "valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s" |
104 apply (simp add:s2ss_def) |
104 apply (simp add:s2ss_def) |
105 apply (tactic {*my_seteq_tac 1*}) |
105 apply (tactic {*my_seteq_tac 1*}) |
106 apply (rule_tac x = obj in exI) |
106 apply (rule_tac x = obj in exI) |
107 apply (simp add:co2sobj_other) |
107 apply (simp add:co2sobj_other) |
108 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
108 apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
109 apply (tactic {*my_setiff_tac 1*}) |
109 apply (tactic {*my_setiff_tac 1*}) |
110 apply (rule_tac x = obj in exI) |
110 apply (rule_tac x = obj in exI) |
111 apply (frule_tac obj = obj in co2sobj_other) |
111 apply (frule_tac obj = obj in co2sobj_other) |
112 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
112 apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits) |
113 done |
113 done |
114 |
114 |
115 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
115 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
116 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
116 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
117 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
117 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |