Praeclarum theorema

PorJosé A. Alonso 24 febrero 202021 agosto 2021

Demostrar el Praeclarum theorema de Leibniz:

theory Praeclarum_theorema
imports Main
begin

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  oops

end

1

2

3

4

5

6

7

8

theory Praeclarum_theorema

imports Main

begin

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

oops

end

Soluciones con Isabelle/HOL

theory Praeclarum_theorema
imports Main
begin

(* 1ª demostración: automática *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  by simp

(* 2ª demostración: aplicativa *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  apply (rule impI)
  apply (rule impI)
  apply (erule conjE)+
  apply (rule conjI)
   apply (erule mp)
   apply assumption
  apply (erule mp)
  apply assumption
  done

(* 3ª demostración: estructurada *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
proof
  assume "(p ⟶ q) ∧ (r ⟶ s)"
  show "(p ∧ r) ⟶ (q ∧ s)"
  proof
    assume "p ∧ r"
    show "q ∧ s"
    proof
      have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› ..
      moreover have "p" using ‹p ∧ r› ..
      ultimately show "q" ..
    next
      have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› ..
      moreover have "r" using ‹p ∧ r› ..
      ultimately show "s" ..
    qed
  qed
qed

(* 4ª demostración: detallada *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
proof (rule impI)
  assume "(p ⟶ q) ∧ (r ⟶ s)"
  show "(p ∧ r) ⟶ (q ∧ s)"
  proof (rule impI)
    assume "p ∧ r"
    show "q ∧ s"
    proof (rule conjI)
      have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct1)
      moreover have "p" using ‹p ∧ r› by (rule conjunct1)
      ultimately show "q" by (rule mp)
    next
      have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct2)
      moreover have "r" using ‹p ∧ r› by (rule conjunct2)
      ultimately show "s" by (rule mp)
    qed
  qed
qed

end

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

theory Praeclarum_theorema

imports Main

begin

(* 1ª demostración: automática *)

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

by simp

(* 2ª demostración: aplicativa *)

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

apply (rule impI)

apply (rule impI)

apply (erule conjE)+

apply (rule conjI)

apply (erule mp)

apply assumption

apply (erule mp)

apply assumption

done

(* 3ª demostración: estructurada *)

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

proof

assume "(p ⟶ q) ∧ (r ⟶ s)"

show "(p ∧ r) ⟶ (q ∧ s)"

proof

assume "p ∧ r"

show "q ∧ s"

proof

have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› ..

moreover have "p" using ‹p ∧ r› ..

ultimately show "q" ..

next

have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› ..

moreover have "r" using ‹p ∧ r› ..

ultimately show "s" ..

qed

qed

qed

(* 4ª demostración: detallada *)

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

proof (rule impI)

assume "(p ⟶ q) ∧ (r ⟶ s)"

show "(p ∧ r) ⟶ (q ∧ s)"

proof (rule impI)

assume "p ∧ r"

show "q ∧ s"

proof (rule conjI)

have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct1)

moreover have "p" using ‹p ∧ r› by (rule conjunct1)

ultimately show "q" by (rule mp)

next

have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct2)

moreover have "r" using ‹p ∧ r› by (rule conjunct2)

ultimately show "s" by (rule mp)

qed

qed

qed

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

José A. Alonso

5 Comentarios

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
proof (rule impI)
  assume 1: "(p ⟶ q) ∧ (r ⟶ s)"
  have 2: "p ⟶ q" using 1 by (rule conjunct1)
  have 3: "r ⟶ s" using 1 by (rule conjunct2)
  show "(p ∧ r) ⟶ (q ∧ s)"
  proof (rule impI)
    assume 4: "p ∧ r"
    have "p" using 4 by (rule conjunct1)
    have "q" using 2 `p` by (rule mp)
    have "r" using 4 by (rule conjunct2)
    have "s" using 3 `r` by (rule mp)
    show "q ∧ s" using `q` `s` by (rule conjI)
  qed
qed

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

proof (rule impI)

assume 1: "(p ⟶ q) ∧ (r ⟶ s)"

have 2: "p ⟶ q" using 1 by (rule conjunct1)

have 3: "r ⟶ s" using 1 by (rule conjunct2)

show "(p ∧ r) ⟶ (q ∧ s)"

proof (rule impI)

assume 4: "p ∧ r"

have "p" using 4 by (rule conjunct1)

have "q" using 2 `p` by (rule mp)

have "r" using 4 by (rule conjunct2)

have "s" using 3 `r` by (rule mp)

show "q ∧ s" using `q` `s` by (rule conjI)

qed

qed

theory Praeclarum_theorema
imports Main
begin

text ‹ Método aplicativo›

lemma P_th:
  "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  apply (rule)
  apply (erule conjE)
  apply (rule)+
   apply (erule mp)
   apply (erule conjunct1)
  apply (erule mp)
  apply (erule conjunct2)
  done

end

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

theory Praeclarum_theorema

imports Main

begin

text ‹ Método aplicativo›

lemma P_th:

"(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

apply (rule)

apply (erule conjE)

apply (rule)+

apply (erule mp)

apply (erule conjunct1)

apply (erule mp)

apply (erule conjunct2)

done

end

theory Praeclarum_theorema
imports Main
begin

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
proof (rule impI)
  assume 1: "(p ⟶ q) ∧ (r ⟶ s)"
  have 2: "p ⟶ q" using 1 by (rule conjunct1)
  have 3: "r ⟶ s" using 1 by (rule conjunct2)
  show "(p ∧ r) ⟶ (q ∧ s)"
  proof (rule impI)
    assume 4: "(p ∧ r)"
    have 5: "p" using 4 by (rule conjunct1)
    have 6: "r" using 4 by (rule conjunct2)
    have 7: "q" using 2 5 by (rule mp)
    have 8: "s" using 3 6 by (rule mp)
    show "q ∧ s" using 7 8 by (rule conjI)
  qed
qed

end

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

theory Praeclarum_theorema

imports Main

begin

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"

proof (rule impI)

assume 1: "(p ⟶ q) ∧ (r ⟶ s)"

have 2: "p ⟶ q" using 1 by (rule conjunct1)

have 3: "r ⟶ s" using 1 by (rule conjunct2)

show "(p ∧ r) ⟶ (q ∧ s)"

proof (rule impI)

assume 4: "(p ∧ r)"

have 5: "p" using 4 by (rule conjunct1)

have 6: "r" using 4 by (rule conjunct2)

have 7: "q" using 2 5 by (rule mp)

have 8: "s" using 3 6 by (rule mp)

show "q ∧ s" using 7 8 by (rule conjI)

qed

qed

end

antgongar dice:

a las

Isabelle/Isar

theory Praeclarum_theorema imports Main begin lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))" by auto end

1
2
3
4
5
6
7
8

theory Praeclarum_theorema
imports Main
begin

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
by auto

end

Loading...

Responder

Una breve demostración usando Lean.

theorem praeclarum {p q r s : Prop} :
    (p → q) ∧ (r → s) → ((p ∧ r) → (q ∧ s)) :=
    assume ⟨p_implies_q, r_implies_s⟩,
    assume ⟨p, r⟩,
    ⟨p_implies_q p, r_implies_s r⟩

1

2

3

4

5

theorem praeclarum {p q r s : Prop} :

(p → q) ∧ (r → s) → ((p ∧ r) → (q ∧ s)) :=

assume ⟨p_implies_q, r_implies_s⟩,

assume ⟨p, r⟩,

⟨p_implies_q p, r_implies_s r⟩

Escribe un comentarioCancel reply