El problema de los infectados
Decidir si es cierto que
Existe una persona tal que si dicha persona se infecta, entonces todas las personas se infectan.
En la formalización se usará I(x) para representar que la persona x está infectada. El problema consiste en completar la siguiente teoría de Isabelle/HOL:
|
1 2 3 4 5 6 7 8 |
theory Infectados imports Main begin lemma "∃x. (I x ⟶ (∀y. I y))" by simp end |
Soluciones con Isabelle/HOL
|
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 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 |
theory Infectados imports Main begin (* 1ª solución (automática) *) lemma "∃x. (I x ⟶ (∀y. I y))" by simp (* 2ª solución (estructurada) *) lemma "∃x. (I x ⟶ (∀y. I y))" proof - have "¬ (∀y. I y) ∨ (∀y. I y)" .. then show "∃x. (I x ⟶ (∀y. I y))" proof assume "¬ (∀y. I y)" then have "∃y. ¬(I y)" by simp then obtain a where "¬ I a" .. then have "I a ⟶ (∀y. I y)" by simp then show "∃x. (I x ⟶ (∀y. I y))" .. next assume "∀y. I y" then show "∃x. (I x ⟶ (∀y. I y))" by simp qed qed (* 3ª solución (detallada con lemas auxiliares) *) lemma aux1: assumes "¬ (∀y. I y)" shows "∃y. ¬(I y)" proof (rule ccontr) assume "∄y. ¬ I y" have "∀y. I y" proof fix a show "I a" proof (rule ccontr) assume "¬ I a" then have "∃y. ¬ I y" by (rule exI) with ‹∄y. ¬ I y› show False by (rule notE) qed qed with assms show False by (rule notE) qed lemma aux2: assumes "¬P" shows "P ⟶ Q" proof assume "P" with assms show "Q" by (rule notE) qed lemma aux3: assumes "∄x. P x" shows "∀x. ¬ P x" proof fix a show "¬ P a" proof assume "P a" then have "∃x. P x" by (rule exI) with assms show False by (rule notE) qed qed lemma aux4: assumes "Q" shows "∃x. (P x ⟶ Q)" proof (rule ccontr) assume "∄x. (P x ⟶ Q)" then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3) then have "¬ (P a ⟶ Q)" by (rule allE) moreover have "P a ⟶ Q" proof assume "P a" show "Q" using assms by this qed ultimately show False by (rule notE) qed lemma "∃x. (I x ⟶ (∀y. I y))" proof - have "¬ (∀y. I y) ∨ (∀y. I y)" .. then show "∃x. (I x ⟶ (∀y. I y))" proof assume "¬ (∀y. I y)" then have "∃y. ¬(I y)" by (rule aux1) then obtain a where "¬ I a" by (rule exE) then have "I a ⟶ (∀y. I y)" by (rule aux2) then show "∃x. (I x ⟶ (∀y. I y))" by (rule exI) next assume "∀y. I y" then show "∃x. (I x ⟶ (∀y. I y))" by (rule aux4) 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>
