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."
El problema consiste en completar la siguiente teoría de Isabelle/HOL:
theory El_problema_de_los_infectados imports Main begin lemma "∃x. (I x ⟶ (∀y. I y))" by sorry end
en la que se ha usado I(x) para representar que la persona x está infectada.
Soluciones
theory El_problema_de_los_infectados imports Main begin (* 1ª solución (automática) *) lemma "∃x. (I x ⟶ (∀y. I y))" by auto (* 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 auto then obtain a where "¬ I a" .. then have "I a ⟶ (∀y. I y)" by auto then show "∃x. (I x ⟶ (∀y. I y))" .. next assume "∀y. I y" then show "∃x. (I x ⟶ (∀y. I y))" by auto 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)" by (rule excluded_middle) then show "∃x. (I x ⟶ (∀y. I y))" proof (rule disjE) 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