equal
deleted
inserted
replaced
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) |