src/HOL/UNITY/Union.thy
changeset 16977 7c04742abac3
parent 16417 9bc16273c2d4
child 30304 d8e4cd2ac2a1
equal deleted inserted replaced
16976:377962871f5d 16977:7c04742abac3
   330 
   330 
   331 lemmas ok_sym = ok_commute [THEN iffD1, standard]
   331 lemmas ok_sym = ok_commute [THEN iffD1, standard]
   332 
   332 
   333 lemma ok_iff_OK:
   333 lemma ok_iff_OK:
   334      "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
   334      "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
   335 by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
   335 apply (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
   336               all_conj_distrib eq_commute,   blast)
   336               all_conj_distrib)
       
   337 apply blast
       
   338 done
   337 
   339 
   338 lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)"
   340 lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)"
   339 by (auto simp add: ok_def)
   341 by (auto simp add: ok_def)
   340 
   342 
   341 lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)"
   343 lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)"