Test.thy
changeset 122 420e03a2d9cc
parent 46 331137d43625
child 127 38c6acf03f68
equal deleted inserted replaced
121:c80a08ff2a85 122:420e03a2d9cc
   283 lemma single_valued_waits2:
   283 lemma single_valued_waits2:
   284   assumes "vt s"
   284   assumes "vt s"
   285   shows "single_valuedP (waits2 s)"
   285   shows "single_valuedP (waits2 s)"
   286 using assms
   286 using assms
   287 unfolding single_valued_def
   287 unfolding single_valued_def
   288 by (metis Collect_splitD fst_eqD sndI waits2_unique)
   288 by (simp add: Product_Type.Collect_case_prodD waits2_unique)
   289 
   289 
   290 lemma single_valued_holds2:
   290 lemma single_valued_holds2:
   291   assumes "vt s"
   291   assumes "vt s"
   292   shows "single_valuedP (\<lambda>cs th. holds2 s th cs)"
   292   shows "single_valuedP (\<lambda>cs th. holds2 s th cs)"
   293 unfolding single_valued_def holds2_def holds_def by simp
   293 unfolding single_valued_def holds2_def holds_def by simp