michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/standard/logic): add imp_or theorems

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-24 12:29:23 -07:00
parent 77c0456be4
commit 5296275c41
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
library/standard/logic.lean
View file

@ -99,6 +99,21 @@ theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b)
(assume Ha, absurd_elim _ Ha Hna)
(assume Hb, absurd_elim _ Hb Hnb)
theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d
:= or_elim H1
(assume Ha : a, or_intro_left _ (H2 Ha))
(assume Hb : b, or_intro_right _ (H3 Hb))
theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c
:= or_elim H1
(assume H2 : a, or_intro_left _ (H H2))
(assume H2 : c, or_intro_right _ H2)
theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b
:= or_elim H1
(assume H2 : c, or_intro_left _ H2)
(assume H2 : a, or_intro_right _ (H H2))
inductive eq {A : Type} (a : A) : A → Prop :=
| refl : eq a a