equal
deleted
inserted
replaced
766 subsubsection {* Atomizing meta-level connectives *} |
766 subsubsection {* Atomizing meta-level connectives *} |
767 |
767 |
768 lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" |
768 lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" |
769 proof |
769 proof |
770 assume "!!x. P x" |
770 assume "!!x. P x" |
771 show "ALL x. P x" by (rule allI) |
771 then show "ALL x. P x" .. |
772 next |
772 next |
773 assume "ALL x. P x" |
773 assume "ALL x. P x" |
774 thus "!!x. P x" by (rule allE) |
774 thus "!!x. P x" by (rule allE) |
775 qed |
775 qed |
776 |
776 |
1217 #> EqSubst.setup |
1217 #> EqSubst.setup |
1218 *} |
1218 *} |
1219 |
1219 |
1220 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
1220 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
1221 proof |
1221 proof |
1222 assume prem: "True \<Longrightarrow> PROP P" |
1222 assume "True \<Longrightarrow> PROP P" |
1223 from prem [OF TrueI] show "PROP P" . |
1223 from this [OF TrueI] show "PROP P" . |
1224 next |
1224 next |
1225 assume "PROP P" |
1225 assume "PROP P" |
1226 show "PROP P" . |
1226 then show "PROP P" . |
1227 qed |
1227 qed |
1228 |
1228 |
1229 lemma ex_simps: |
1229 lemma ex_simps: |
1230 "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" |
1230 "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" |
1231 "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))" |
1231 "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))" |