335 (* should be modified when socket is model in static *)

   336 lemma s2ss_createsock:

   337   "valid (CreateSock p af st fd inum # s) \<Longrightarrow> s2ss (CreateSock p af st fd inum # s) = s2ss s"

   338 apply (simp add:s2ss_def)

   339 apply (tactic {*my_seteq_tac 1*})

   340 apply (rule_tac x = obj in exI)

   341 apply (simp add:co2sobj_other)

   342 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   343 apply (tactic {*my_setiff_tac 1*})

   344 apply (rule_tac x = obj in exI)

   345 apply (frule_tac obj = obj in co2sobj_other)

   346 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   347 done

   348 

   349 lemma s2ss_bind:

   350   "valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s"

   351 apply (simp add:s2ss_def)

   352 apply (tactic {*my_seteq_tac 1*})

   353 apply (rule_tac x = obj in exI)

   354 apply (simp add:co2sobj_other)

   355 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   356 apply (tactic {*my_setiff_tac 1*})

   357 apply (rule_tac x = obj in exI)

   358 apply (frule_tac obj = obj in co2sobj_other)

   359 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   360 done

   361 

   362 lemma s2ss_connect:

   363   "valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s"

   364 apply (simp add:s2ss_def)

   365 apply (tactic {*my_seteq_tac 1*})

   366 apply (rule_tac x = obj in exI)

   367 apply (simp add:co2sobj_other)

   368 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   369 apply (tactic {*my_setiff_tac 1*})

   370 apply (rule_tac x = obj in exI)

   371 apply (frule_tac obj = obj in co2sobj_other)

   372 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   373 done

   374 

   375 lemma s2ss_listen:

   376   "valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s"

   377 apply (simp add:s2ss_def)

   378 apply (tactic {*my_seteq_tac 1*})

   379 apply (rule_tac x = obj in exI)

   380 apply (simp add:co2sobj_other)

   381 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   382 apply (tactic {*my_setiff_tac 1*})

   383 apply (rule_tac x = obj in exI)

   384 apply (frule_tac obj = obj in co2sobj_other)

   385 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   386 done

   387 

   388 lemma s2ss_accept:

   389   "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s"

   390 apply (simp add:s2ss_def)

   391 apply (tactic {*my_seteq_tac 1*})

   392 apply (rule_tac x = obj in exI)

   393 apply (simp add:co2sobj_other)

   394 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   395 apply (tactic {*my_setiff_tac 1*})

   396 apply (rule_tac x = obj in exI)

   397 apply (frule_tac obj = obj in co2sobj_other)

   398 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   399 done

   400 

   401 lemma s2ss_send:

   402   "valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s"

   403 apply (simp add:s2ss_def)

   404 apply (tactic {*my_seteq_tac 1*})

   405 apply (rule_tac x = obj in exI)

   406 apply (simp add:co2sobj_other)

   407 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   408 apply (tactic {*my_setiff_tac 1*})

   409 apply (rule_tac x = obj in exI)

   410 apply (frule_tac obj = obj in co2sobj_other)

   411 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   412 done

   413 

   414 lemma s2ss_recv:

   415   "valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s"

   416 apply (simp add:s2ss_def)

   417 apply (tactic {*my_seteq_tac 1*})

   418 apply (rule_tac x = obj in exI)

   419 apply (simp add:co2sobj_other)

   420 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   421 apply (tactic {*my_setiff_tac 1*})

   422 apply (rule_tac x = obj in exI)

   423 apply (frule_tac obj = obj in co2sobj_other)

   424 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   425 done

   426 

   427 lemma s2ss_shutdown:

   428   "valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s"

   429 apply (simp add:s2ss_def)

   430 apply (tactic {*my_seteq_tac 1*})

   431 apply (rule_tac x = obj in exI)

   432 apply (simp add:co2sobj_other)

   433 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

   434 apply (tactic {*my_setiff_tac 1*})

   435 apply (rule_tac x = obj in exI)

   436 apply (frule_tac obj = obj in co2sobj_other)

   437 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

   438 done