src/HOL/UNITY/Guar.thy
changeset 16647 c6d81ddebb0e
parent 16417 9bc16273c2d4
child 27682 25aceefd4786
equal deleted inserted replaced
16646:666774b0d1b0 16647:c6d81ddebb0e
   429 (* Proposition 2 *)
   429 (* Proposition 2 *)
   430 lemma wx_subset: "(wx X)<=X"
   430 lemma wx_subset: "(wx X)<=X"
   431 by (unfold wx_def, auto)
   431 by (unfold wx_def, auto)
   432 
   432 
   433 lemma wx_ex_prop: "ex_prop (wx X)"
   433 lemma wx_ex_prop: "ex_prop (wx X)"
   434 apply (simp add: wx_def ex_prop_equiv, safe, blast)
   434 apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast)
   435 apply force 
   435 apply force 
   436 done
   436 done
   437 
   437 
   438 lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
   438 lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
   439 by (auto simp add: wx_def)
   439 by (auto simp add: wx_def)