Diferencia entre revisiones de «Tema 4a»
De Lógica matemática y fundamentos (2018-19)
m |
|||
Línea 1: | Línea 1: | ||
<source lang="isabelle"> | <source lang="isabelle"> | ||
− | chapter | + | chapter ‹Tema 4a: Deducción natural en lógica de primer orden› |
theory T4a_Deduccion_natural_en_logica_de_primer_orden | theory T4a_Deduccion_natural_en_logica_de_primer_orden | ||
Línea 6: | Línea 6: | ||
begin | begin | ||
− | text | + | text ‹El objetivo de este tema es presentar la deducción natural en |
− | |||
lógica de primer orden con Isabelle/HOL. La presentación se | lógica de primer orden con Isabelle/HOL. La presentación se | ||
basa en los ejemplos de tema 4 del curso LMF que se encuentra | basa en los ejemplos de tema 4 del curso LMF que se encuentra | ||
Línea 14: | Línea 13: | ||
La página al lado de cada ejemplo indica la página de las | La página al lado de cada ejemplo indica la página de las | ||
− | transparencias de LMF donde se encuentra la demostración. | + | transparencias de LMF donde se encuentra la demostración.› |
− | section | + | section ‹Reglas del cuantificador universal› |
− | text | + | text ‹Las reglas del cuantificador universal son |
− | |||
· allE: ⟦∀x. P x; P a ⟹ R⟧ ⟹ R | · allE: ⟦∀x. P x; P a ⟹ R⟧ ⟹ R | ||
· allI: (⋀x. P x) ⟹ ∀x. P x | · allI: (⋀x. P x) ⟹ ∀x. P x | ||
− | + | › | |
− | text | + | subsection ‹Ejemplo 1› |
− | + | ||
+ | text ‹Ejemplo 1 (p. 10). Demostrar que | ||
P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c) | P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c) | ||
− | + | › | |
+ | |||
+ | subsubsection ‹Demostración detallada› | ||
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 38: | Línea 39: | ||
show 4: "¬Q(c)" using 3 1 by (rule mp) | show 4: "¬Q(c)" using 3 1 by (rule mp) | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración estructurada› | ||
― ‹La demostración estructurada es› | ― ‹La demostración estructurada es› | ||
Línea 48: | Línea 51: | ||
then show "¬Q(c)" using assms(1) .. | then show "¬Q(c)" using assms(1) .. | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración automática› | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
Línea 54: | Línea 59: | ||
"∀x. (P(x) ⟶ ¬Q(x))" | "∀x. (P(x) ⟶ ¬Q(x))" | ||
shows "¬Q(c)" | shows "¬Q(c)" | ||
− | using assms | + | using assms |
− | by auto | + | by auto |
+ | |||
+ | subsubsection ‹Demostración aplicativa› | ||
+ | |||
+ | lemma ejemplo_1d: | ||
+ | "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)" | ||
+ | apply (erule allE) (* da ⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c *) | ||
+ | apply (erule mp) (* da P c ⟹ P c *) | ||
+ | apply assumption (* da No subgoals! *) | ||
+ | done | ||
+ | |||
+ | text ‹Explicaciones | ||
+ | apply (erule allE) | ||
+ | + Objetivo: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("¬Q(c)", "∀x. (P(x) ⟶ ¬Q(x))") y | ||
+ | ("?R", "∀x. ?P x") | ||
+ | es ?R / ¬Q(c) | ||
+ | ?P x / P(x) ⟶ ¬Q(x) | ||
+ | + Nuevo objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c" | ||
+ | |||
+ | apply (erule mp) | ||
+ | + Objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c" | ||
+ | + mp: "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q" | ||
+ | + Unificador de ("¬ Q c", "P ?x ⟶ ¬ Q ?x") y | ||
+ | ("?Q", "?P ⟶ ?Q") | ||
+ | es ?Q / ¬ Q c | ||
+ | ?P / P c | ||
+ | + Nuevo objetivo: "P c ⟹ P c" | ||
+ | › | ||
+ | |||
+ | subsection ‹Ejemplo 2› | ||
− | text | + | text ‹Ejemplo 2 (p. 11). Demostrar que |
− | |||
∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x) | ∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x) | ||
− | + | › | |
+ | |||
+ | subsubsection ‹Demostración detallada› | ||
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 86: | Línea 123: | ||
show 5: "¬(Q a)" using 3 4 by (rule mp) | show 5: "¬(Q a)" using 3 4 by (rule mp) | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración estructurada› | ||
― ‹La demostración estructurada es› | ― ‹La demostración estructurada es› | ||
Línea 96: | Línea 135: | ||
have "P a" using assms(2) .. | have "P a" using assms(2) .. | ||
have "P a ⟶ ¬(Q a)" using assms(1) .. | have "P a ⟶ ¬(Q a)" using assms(1) .. | ||
− | then show "¬(Q a)" using | + | then show "¬(Q a)" using ‹P a› .. |
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración automática› | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
Línea 104: | Línea 145: | ||
"∀x. P x" | "∀x. P x" | ||
shows "∀x. ¬(Q x)" | shows "∀x. ¬(Q x)" | ||
− | using assms | + | using assms |
− | by auto | + | by auto |
+ | |||
+ | subsubsection ‹Demostración aplicativa› | ||
+ | |||
+ | lemma ejemplo_2e: | ||
+ | "⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)" | ||
+ | apply (rule allI) (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z); | ||
+ | P (?y4 z)⟧ | ||
+ | ⟹ ¬ Q z*) | ||
+ | apply (erule allE)+ (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z); | ||
+ | P (?y4 z)⟧ | ||
+ | ⟹ ¬ Q z *) | ||
+ | apply (erule mp) (* da ⋀z. P (?y4 z) ⟹ P z *) | ||
+ | apply assumption (* da No subgoals! *) | ||
+ | done | ||
− | section | + | section ‹Reglas del cuantificador existencial› |
− | text | + | text ‹Las reglas del cuantificador existencial son |
− | |||
· exI: P a ⟹ ∃x. P x | · exI: P a ⟹ ∃x. P x | ||
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q | · exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q | ||
Línea 116: | Línea 170: | ||
En la regla exE la nueva variable se introduce mediante la declaración | En la regla exE la nueva variable se introduce mediante la declaración | ||
"obtain ... where ... by (rule exE)" | "obtain ... where ... by (rule exE)" | ||
− | + | › | |
− | text | + | subsection ‹Ejemplo 3› |
− | + | ||
+ | text ‹Ejemplo 3 (p. 12). Demostrar que | ||
∀x. P x ⊢ ∃x. P x | ∀x. P x ⊢ ∃x. P x | ||
− | + | › | |
+ | |||
+ | subsubsection ‹Demostración detallada› | ||
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 132: | Línea 189: | ||
then show "∃x. P x" by (rule exI) | then show "∃x. P x" by (rule exI) | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración estructurada› | ||
― ‹La demostración estructurada es› | ― ‹La demostración estructurada es› | ||
Línea 160: | Línea 219: | ||
show "P a" using assms .. | show "P a" using assms .. | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración automática› | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
Línea 165: | Línea 226: | ||
assumes "∀x. P x" | assumes "∀x. P x" | ||
shows "∃x. P x" | shows "∃x. P x" | ||
− | using assms | + | using assms |
− | by auto | + | by auto |
+ | |||
+ | subsubsection ‹Demostración aplicativa› | ||
+ | |||
+ | lemma ejemplo_3f: | ||
+ | "∀x. P x ⟹ ∃y. P y" | ||
+ | apply (erule allE) (* da P ?x ⟹ ∃y. P y *) | ||
+ | apply (erule exI) (* da No subgoals! *) | ||
+ | done | ||
+ | |||
+ | subsection ‹Ejemplo 4› | ||
− | text | + | text ‹Ejemplo 4 (p. 13). Demostrar |
− | |||
∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x | ∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x | ||
− | + | › | |
+ | |||
+ | subsubsection ‹Demostración detallada› | ||
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 184: | Línea 256: | ||
then show 6: "∃x. Q x" by (rule exI) | then show 6: "∃x. Q x" by (rule exI) | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración estructurada› | ||
― ‹La demostración estructurada es› | ― ‹La demostración estructurada es› | ||
Línea 193: | Línea 267: | ||
obtain a where "P a" using assms(2) .. | obtain a where "P a" using assms(2) .. | ||
have "P a ⟶ Q a" using assms(1) .. | have "P a ⟶ Q a" using assms(1) .. | ||
− | then have "Q a" using | + | then have "Q a" using ‹P a› .. |
then show "∃x. Q x" .. | then show "∃x. Q x" .. | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración automática› | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
Línea 202: | Línea 278: | ||
"∃x. P x" | "∃x. P x" | ||
shows "∃x. Q x" | shows "∃x. Q x" | ||
− | using assms | + | using assms |
− | by auto | + | by auto |
+ | |||
+ | subsubsection ‹Demostración aplicativa› | ||
+ | |||
+ | lemma ejemplo_4f: | ||
+ | "⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z" | ||
+ | apply (erule exE) (* da ⋀y. ⟦∀x. P x ⟶ Q x; P y⟧ ⟹ ∃z. Q z *) | ||
+ | apply (erule allE) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ ∃z. Q z *) | ||
+ | apply (rule exI) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ Q (?z4 y) *) | ||
+ | apply (erule mp) (* da ⋀y. P y ⟹ P (?x2 y) *) | ||
+ | apply assumption (* da No subgoals! *) | ||
+ | done | ||
+ | |||
+ | section ‹Demostración de equivalencias› | ||
+ | |||
+ | subsection ‹Ejemplo 5.1› | ||
− | + | text ‹Ejemplo 5.1 (p. 15). Demostrar | |
+ | ¬∀x. P x ⊢ ∃x. ¬(P x)› | ||
− | + | subsubsection ‹Demostración detallada› | |
− | |||
− | |||
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 224: | Línea 314: | ||
assume "¬P(a)" | assume "¬P(a)" | ||
then have "∃x. ¬P(x)" by (rule exI) | then have "∃x. ¬P(x)" by (rule exI) | ||
− | with | + | with ‹¬(∃x. ¬P(x))› show False by (rule notE) |
qed | qed | ||
qed | qed | ||
with assms show False by (rule notE) | with assms show False by (rule notE) | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración estructurada› | ||
― ‹La demostración estructurada es› | ― ‹La demostración estructurada es› | ||
Línea 243: | Línea 335: | ||
assume "¬P(a)" | assume "¬P(a)" | ||
then have "∃x. ¬P(x)" .. | then have "∃x. ¬P(x)" .. | ||
− | with | + | with ‹¬(∃x. ¬P(x))› show False .. |
qed | qed | ||
qed | qed | ||
with assms show False .. | with assms show False .. | ||
qed | qed | ||
+ | |||
+ | subsubsection ‹Demostración automática› | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
Línea 253: | Línea 347: | ||
assumes "¬(∀x. P(x))" | assumes "¬(∀x. P(x))" | ||
shows "∃x. ¬P(x)" | shows "∃x. ¬P(x)" | ||
− | using assms | + | using assms |
− | by auto | + | by auto |
+ | |||
+ | subsubsection ‹Demostración aplicativa› | ||
+ | |||
+ | lemma ejemplo_5_1d: "¬(∀x. P x) ⟹ ∃y. ¬P y" | ||
+ | apply (rule ccontr) (* da ⟦¬ (∀x. P x); ∄y. ¬ P y⟧ ⟹ False *) | ||
+ | apply (erule notE) (* da ∄y. ¬ P y ⟹ ∀x. P x *) | ||
+ | apply (rule allI) (* da ⋀x. ∄y. ¬ P y ⟹ P x *) | ||
+ | apply (rule ccontr) (* da ⋀x. ⟦∄y. ¬ P y; ¬ P x⟧ ⟹ False *) | ||
+ | apply (erule notE) (* da ⋀x. ¬ P x ⟹ ∃y. ¬ P y *) | ||
+ | apply (erule exI) (* da No subgoals! *) | ||
+ | done | ||
+ | |||
− | text | + | text ‹ |
Ejemplo 5.2 (p. 16). Demostrar | Ejemplo 5.2 (p. 16). Demostrar | ||
− | ∃x. ¬(P x) ⊢ ¬∀x. P | + | ∃x. ¬(P x) ⊢ ¬∀x. P x› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 267: | Línea 373: | ||
assume "∀x. P(x)" | assume "∀x. P(x)" | ||
obtain a where "¬P(a)" using assms by (rule exE) | obtain a where "¬P(a)" using assms by (rule exE) | ||
− | have "P(a)" using | + | have "P(a)" using ‹∀x. P(x)› by (rule allE) |
− | with | + | with ‹¬P(a)› show False by (rule notE) |
qed | qed | ||
Línea 278: | Línea 384: | ||
assume "∀x. P(x)" | assume "∀x. P(x)" | ||
obtain a where "¬P(a)" using assms .. | obtain a where "¬P(a)" using assms .. | ||
− | have "P(a)" using | + | have "P(a)" using ‹∀x. P(x)› .. |
− | with | + | with ‹¬P(a)› show False .. |
qed | qed | ||
Línea 289: | Línea 395: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 5.3 (p. 17). Demostrar | Ejemplo 5.3 (p. 17). Demostrar | ||
− | ⊢ ¬∀x. P x ⟷ ∃x. ¬(P x) | + | ⊢ ¬∀x. P x ⟷ ∃x. ¬(P x)› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 309: | Línea 415: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 6.1 (p. 18). Demostrar | Ejemplo 6.1 (p. 18). Demostrar | ||
− | ∀x. P(x) ∧ Q(x) ⊢ (∀x. P(x)) ∧ (∀x. Q(x)) | + | ∀x. P(x) ∧ Q(x) ⊢ (∀x. P(x)) ∧ (∀x. Q(x))› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 360: | Línea 466: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 6.2 (p. 19). Demostrar | Ejemplo 6.2 (p. 19). Demostrar | ||
− | (∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x) | + | (∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x)› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 374: | Línea 480: | ||
have "∀x. Q(x)" using assms by (rule conjunct2) | have "∀x. Q(x)" using assms by (rule conjunct2) | ||
then have "Q(a)" by (rule allE) | then have "Q(a)" by (rule allE) | ||
− | with | + | with ‹P(a)› show "P(a) ∧ Q(a)" by (rule conjI) |
qed | qed | ||
Línea 387: | Línea 493: | ||
have "∀x. Q(x)" using assms .. | have "∀x. Q(x)" using assms .. | ||
then have "Q(a)" .. | then have "Q(a)" .. | ||
− | with | + | with ‹P(a)› show "P(a) ∧ Q(a)" .. |
qed | qed | ||
Línea 397: | Línea 503: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 6.3 (p. 20). Demostrar | Ejemplo 6.3 (p. 20). Demostrar | ||
− | ⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x)) | + | ⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 412: | Línea 518: | ||
qed | qed | ||
− | text | + | text ‹ |
Ejemplo 7.1 (p. 21). Demostrar | Ejemplo 7.1 (p. 21). Demostrar | ||
− | (∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x) | + | (∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x)› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 457: | Línea 563: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 7.2 (p. 22). Demostrar | Ejemplo 7.2 (p. 22). Demostrar | ||
− | ∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x)) | + | ∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x))› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 504: | Línea 610: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 7.3 (p. 23). Demostrar | Ejemplo 7.3 (p. 23). Demostrar | ||
− | ⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x)) | + | ⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 525: | Línea 631: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 8.1 (p. 24). Demostrar | Ejemplo 8.1 (p. 24). Demostrar | ||
− | ∃x y. P(x,y) ⊢ ∃y x. P(x,y) | + | ∃x y. P(x,y) ⊢ ∃y x. P(x,y)› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 558: | Línea 664: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 8.2. Demostrar | Ejemplo 8.2. Demostrar | ||
− | ∃y x. P(x,y) ⊢ ∃x y. P(x,y) | + | ∃y x. P(x,y) ⊢ ∃x y. P(x,y)› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 591: | Línea 697: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 8.3 (p. 25). Demostrar | Ejemplo 8.3 (p. 25). Demostrar | ||
− | ⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y)) | + | ⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y))› |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 611: | Línea 717: | ||
by auto | by auto | ||
− | section | + | section ‹Reglas de la igualdad› |
− | text | + | text ‹ |
Las reglas básicas de la igualdad son: | Las reglas básicas de la igualdad son: | ||
· refl: t = t | · refl: t = t | ||
· subst: ⟦s = t; P s⟧ ⟹ P t | · subst: ⟦s = t; P s⟧ ⟹ P t | ||
− | + | › | |
− | text | + | text ‹ |
Ejemplo 9 (p. 27). Demostrar | Ejemplo 9 (p. 27). Demostrar | ||
x + 1 = 1 + x, x + 1 > 1 ⟶ x + 1 > 0 ⊢ 1 + x > 1 ⟶ 1 + x > 0 | x + 1 = 1 + x, x + 1 > 1 ⟶ x + 1 > 0 ⊢ 1 + x > 1 ⟶ 1 + x > 0 | ||
− | + | › | |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 649: | Línea 755: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 10 (p. 27). Demostrar | Ejemplo 10 (p. 27). Demostrar | ||
x = y, y = z ⊢ x = z | x = y, y = z ⊢ x = z | ||
− | + | › | |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› | ||
Línea 679: | Línea 785: | ||
by auto | by auto | ||
− | text | + | text ‹ |
Ejemplo 11 (p. 28). Demostrar | Ejemplo 11 (p. 28). Demostrar | ||
s = t ⊢ t = s | s = t ⊢ t = s | ||
− | + | › | |
― ‹La demostración detallada es› | ― ‹La demostración detallada es› |
Revisión actual del 21:03 7 feb 2020
chapter ‹Tema 4a: Deducción natural en lógica de primer orden›
theory T4a_Deduccion_natural_en_logica_de_primer_orden
imports Main
begin
text ‹El objetivo de este tema es presentar la deducción natural en
lógica de primer orden con Isabelle/HOL. La presentación se
basa en los ejemplos de tema 4 del curso LMF que se encuentra
en http://goo.gl/uJj8d (que a su vez se basa en el libro de
Huth y Ryan "Logic in Computer Science" http://goo.gl/qsVpY ).
La página al lado de cada ejemplo indica la página de las
transparencias de LMF donde se encuentra la demostración.›
section ‹Reglas del cuantificador universal›
text ‹Las reglas del cuantificador universal son
· allE: ⟦∀x. P x; P a ⟹ R⟧ ⟹ R
· allI: (⋀x. P x) ⟹ ∀x. P x
›
subsection ‹Ejemplo 1›
text ‹Ejemplo 1 (p. 10). Demostrar que
P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_1a:
assumes 1: "P(c)" and
2: "∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
proof -
have 3: "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)
show 4: "¬Q(c)" using 3 1 by (rule mp)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_1b:
assumes "P(c)"
"∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
proof -
have "P(c) ⟶ ¬Q(c)" using assms(2) ..
then show "¬Q(c)" using assms(1) ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_1c:
assumes "P(c)"
"∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_1d:
"⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
apply (erule allE) (* da ⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c *)
apply (erule mp) (* da P c ⟹ P c *)
apply assumption (* da No subgoals! *)
done
text ‹Explicaciones
apply (erule allE)
+ Objetivo: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("¬Q(c)", "∀x. (P(x) ⟶ ¬Q(x))") y
("?R", "∀x. ?P x")
es ?R / ¬Q(c)
?P x / P(x) ⟶ ¬Q(x)
+ Nuevo objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"
apply (erule mp)
+ Objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"
+ mp: "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q"
+ Unificador de ("¬ Q c", "P ?x ⟶ ¬ Q ?x") y
("?Q", "?P ⟶ ?Q")
es ?Q / ¬ Q c
?P / P c
+ Nuevo objetivo: "P c ⟹ P c"
›
subsection ‹Ejemplo 2›
text ‹Ejemplo 2 (p. 11). Demostrar que
∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_2a:
assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
2: "∀x. P x"
shows "∀x. ¬(Q x)"
proof -
{ fix a
have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
have 4: "P a" using 2 by (rule allE)
have 5: "¬(Q a)" using 3 4 by (rule mp) }
then show "∀x. ¬(Q x)" by (rule allI)
qed
― ‹La demostración detallada hacia atrás es›
lemma ejemplo_2b:
assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
2: "∀x. P x"
shows "∀x. ¬(Q x)"
proof (rule allI)
fix a
have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
have 4: "P a" using 2 by (rule allE)
show 5: "¬(Q a)" using 3 4 by (rule mp)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_2c:
assumes "∀x. (P x ⟶ ¬(Q x))"
"∀x. P x"
shows "∀x. ¬(Q x)"
proof
fix a
have "P a" using assms(2) ..
have "P a ⟶ ¬(Q a)" using assms(1) ..
then show "¬(Q a)" using ‹P a› ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_2d:
assumes "∀x. (P x ⟶ ¬(Q x))"
"∀x. P x"
shows "∀x. ¬(Q x)"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_2e:
"⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)"
apply (rule allI) (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z);
P (?y4 z)⟧
⟹ ¬ Q z*)
apply (erule allE)+ (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z);
P (?y4 z)⟧
⟹ ¬ Q z *)
apply (erule mp) (* da ⋀z. P (?y4 z) ⟹ P z *)
apply assumption (* da No subgoals! *)
done
section ‹Reglas del cuantificador existencial›
text ‹Las reglas del cuantificador existencial son
· exI: P a ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
En la regla exE la nueva variable se introduce mediante la declaración
"obtain ... where ... by (rule exE)"
›
subsection ‹Ejemplo 3›
text ‹Ejemplo 3 (p. 12). Demostrar que
∀x. P x ⊢ ∃x. P x
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_3a:
assumes "∀x. P x"
shows "∃x. P x"
proof -
fix a
have "P a" using assms by (rule allE)
then show "∃x. P x" by (rule exI)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_3b:
assumes "∀x. P x"
shows "∃x. P x"
proof -
fix a
have "P a" using assms ..
then show "∃x. P x" ..
qed
― ‹La demostración estructurada se puede simplificar›
lemma ejemplo_3c:
assumes "∀x. P x"
shows "∃x. P x"
proof (rule exI)
fix a
show "P a" using assms ..
qed
― ‹La demostración estructurada se puede simplificar aún más›
lemma ejemplo_3d:
assumes "∀x. P x"
shows "∃x. P x"
proof
fix a
show "P a" using assms ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_3e:
assumes "∀x. P x"
shows "∃x. P x"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_3f:
"∀x. P x ⟹ ∃y. P y"
apply (erule allE) (* da P ?x ⟹ ∃y. P y *)
apply (erule exI) (* da No subgoals! *)
done
subsection ‹Ejemplo 4›
text ‹Ejemplo 4 (p. 13). Demostrar
∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_4a:
assumes 1: "∀x. (P x ⟶ Q x)" and
2: "∃x. P x"
shows "∃x. Q x"
proof -
obtain a where 3: "P a" using 2 by (rule exE)
have 4: "P a ⟶ Q a" using 1 by (rule allE)
have 5: "Q a" using 4 3 by (rule mp)
then show 6: "∃x. Q x" by (rule exI)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_4b:
assumes "∀x. (P x ⟶ Q x)"
"∃x. P x"
shows "∃x. Q x"
proof -
obtain a where "P a" using assms(2) ..
have "P a ⟶ Q a" using assms(1) ..
then have "Q a" using ‹P a› ..
then show "∃x. Q x" ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_4c:
assumes "∀x. (P x ⟶ Q x)"
"∃x. P x"
shows "∃x. Q x"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_4f:
"⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z"
apply (erule exE) (* da ⋀y. ⟦∀x. P x ⟶ Q x; P y⟧ ⟹ ∃z. Q z *)
apply (erule allE) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ ∃z. Q z *)
apply (rule exI) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ Q (?z4 y) *)
apply (erule mp) (* da ⋀y. P y ⟹ P (?x2 y) *)
apply assumption (* da No subgoals! *)
done
section ‹Demostración de equivalencias›
subsection ‹Ejemplo 5.1›
text ‹Ejemplo 5.1 (p. 15). Demostrar
¬∀x. P x ⊢ ∃x. ¬(P x)›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_5_1a:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume "¬(∃x. ¬P(x))"
have "∀x. P(x)"
proof (rule allI)
fix a
show "P(a)"
proof (rule ccontr)
assume "¬P(a)"
then have "∃x. ¬P(x)" by (rule exI)
with ‹¬(∃x. ¬P(x))› show False by (rule notE)
qed
qed
with assms show False by (rule notE)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_5_1b:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume "¬(∃x. ¬P(x))"
have "∀x. P(x)"
proof
fix a
show "P(a)"
proof (rule ccontr)
assume "¬P(a)"
then have "∃x. ¬P(x)" ..
with ‹¬(∃x. ¬P(x))› show False ..
qed
qed
with assms show False ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_5_1c:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_5_1d: "¬(∀x. P x) ⟹ ∃y. ¬P y"
apply (rule ccontr) (* da ⟦¬ (∀x. P x); ∄y. ¬ P y⟧ ⟹ False *)
apply (erule notE) (* da ∄y. ¬ P y ⟹ ∀x. P x *)
apply (rule allI) (* da ⋀x. ∄y. ¬ P y ⟹ P x *)
apply (rule ccontr) (* da ⋀x. ⟦∄y. ¬ P y; ¬ P x⟧ ⟹ False *)
apply (erule notE) (* da ⋀x. ¬ P x ⟹ ∃y. ¬ P y *)
apply (erule exI) (* da No subgoals! *)
done
text ‹
Ejemplo 5.2 (p. 16). Demostrar
∃x. ¬(P x) ⊢ ¬∀x. P x›
― ‹La demostración detallada es›
lemma ejemplo_5_2a:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
proof (rule notI)
assume "∀x. P(x)"
obtain a where "¬P(a)" using assms by (rule exE)
have "P(a)" using ‹∀x. P(x)› by (rule allE)
with ‹¬P(a)› show False by (rule notE)
qed
― ‹La demostración estructurada es›
lemma ejemplo_5_2b:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
proof
assume "∀x. P(x)"
obtain a where "¬P(a)" using assms ..
have "P(a)" using ‹∀x. P(x)› ..
with ‹¬P(a)› show False ..
qed
― ‹La demostración automática es›
lemma ejemplo_5_2c:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
using assms
by auto
text ‹
Ejemplo 5.3 (p. 17). Demostrar
⊢ ¬∀x. P x ⟷ ∃x. ¬(P x)›
― ‹La demostración detallada es›
lemma ejemplo_5_3a:
"(¬(∀x. P(x))) ⟷ (∃x. ¬P(x))"
proof (rule iffI)
assume "¬(∀x. P(x))"
then show "∃x. ¬P(x)" by (rule ejemplo_5_1a)
next
assume "∃x. ¬P(x)"
then show "¬(∀x. P(x))" by (rule ejemplo_5_2a)
qed
― ‹La demostración automática es›
lemma ejemplo_5_3b:
"(¬(∀x. P(x))) ⟷ (∃x. ¬P(x))"
by auto
text ‹
Ejemplo 6.1 (p. 18). Demostrar
∀x. P(x) ∧ Q(x) ⊢ (∀x. P(x)) ∧ (∀x. Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_6_1a:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof (rule conjI)
show "∀x. P(x)"
proof (rule allI)
fix a
have "P(a) ∧ Q(a)" using assms by (rule allE)
then show "P(a)" by (rule conjunct1)
qed
next
show "∀x. Q(x)"
proof (rule allI)
fix a
have "P(a) ∧ Q(a)" using assms by (rule allE)
then show "Q(a)" by (rule conjunct2)
qed
qed
― ‹La demostración estructurada es›
lemma ejemplo_6_1b:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof
show "∀x. P(x)"
proof
fix a
have "P(a) ∧ Q(a)" using assms ..
then show "P(a)" ..
qed
next
show "∀x. Q(x)"
proof
fix a
have "P(a) ∧ Q(a)" using assms ..
then show "Q(a)" ..
qed
qed
― ‹La demostración automática es›
lemma ejemplo_6_1c:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
using assms
by auto
text ‹
Ejemplo 6.2 (p. 19). Demostrar
(∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x)›
― ‹La demostración detallada es›
lemma ejemplo_6_2a:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
proof (rule allI)
fix a
have "∀x. P(x)" using assms by (rule conjunct1)
then have "P(a)" by (rule allE)
have "∀x. Q(x)" using assms by (rule conjunct2)
then have "Q(a)" by (rule allE)
with ‹P(a)› show "P(a) ∧ Q(a)" by (rule conjI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_6_2b:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
proof
fix a
have "∀x. P(x)" using assms ..
then have "P(a)" by (rule allE)
have "∀x. Q(x)" using assms ..
then have "Q(a)" ..
with ‹P(a)› show "P(a) ∧ Q(a)" ..
qed
― ‹La demostración automática es›
lemma ejemplo_6_2c:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
using assms
by auto
text ‹
Ejemplo 6.3 (p. 20). Demostrar
⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_6_3a:
"(∀x. P(x) ∧ Q(x)) ⟷ ((∀x. P(x)) ∧ (∀x. Q(x)))"
proof (rule iffI)
assume "∀x. P(x) ∧ Q(x)"
then show "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule ejemplo_6_1a)
next
assume "(∀x. P(x)) ∧ (∀x. Q(x))"
then show "∀x. P(x) ∧ Q(x)" by (rule ejemplo_6_2a)
qed
text ‹
Ejemplo 7.1 (p. 21). Demostrar
(∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x)›
― ‹La demostración detallada es›
lemma ejemplo_7_1a:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
proof (rule disjE)
assume "∃x. P(x)"
then obtain a where "P(a)" by (rule exE)
then have "P(a) ∨ Q(a)" by (rule disjI1)
then show "∃x. P(x) ∨ Q(x)" by (rule exI)
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" by (rule exE)
then have "P(a) ∨ Q(a)" by (rule disjI2)
then show "∃x. P(x) ∨ Q(x)" by (rule exI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_7_1b:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
proof
assume "∃x. P(x)"
then obtain a where "P(a)" ..
then have "P(a) ∨ Q(a)" ..
then show "∃x. P(x) ∨ Q(x)" ..
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" ..
then have "P(a) ∨ Q(a)" ..
then show "∃x. P(x) ∨ Q(x)" ..
qed
― ‹La demostración automática es›
lemma ejemplo_7_1c:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
by auto
text ‹
Ejemplo 7.2 (p. 22). Demostrar
∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_7_2a:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
obtain a where "P(a) ∨ Q(a)" using assms by (rule exE)
then show "(∃x. P(x)) ∨ (∃x. Q(x))"
proof (rule disjE)
assume "P(a)"
then have "∃x. P(x)" by (rule exI)
then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI1)
next
assume "Q(a)"
then have "∃x. Q(x)" by (rule exI)
then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI2)
qed
qed
― ‹La demostración estructurada es›
lemma ejercicio_7_2b:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
obtain a where "P(a) ∨ Q(a)" using assms ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))"
proof
assume "P(a)"
then have "∃x. P(x)" ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))" ..
next
assume "Q(a)"
then have "∃x. Q(x)" ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))" ..
qed
qed
― ‹La demostración automática es›
lemma ejercicio_7_2c:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
using assms
by auto
text ‹
Ejemplo 7.3 (p. 23). Demostrar
⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_7_3a:
"((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))"
proof (rule iffI)
assume "(∃x. P(x)) ∨ (∃x. Q(x))"
then show "∃x. P(x) ∨ Q(x)" by (rule ejemplo_7_1a)
next
assume "∃x. P(x) ∨ Q(x)"
then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule ejemplo_7_2a)
qed
― ‹La demostración automática es›
lemma ejemplo_7_3b:
"((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))"
using assms
by auto
text ‹
Ejemplo 8.1 (p. 24). Demostrar
∃x y. P(x,y) ⊢ ∃y x. P(x,y)›
― ‹La demostración detallada es›
lemma ejemplo_8_1a:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
proof -
obtain a where "∃y. P(a,y)" using assms by (rule exE)
then obtain b where "P(a,b)" by (rule exE)
then have "∃x. P(x,b)" by (rule exI)
then show "∃y x. P(x,y)" by (rule exI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_8_1b:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
proof -
obtain a where "∃y. P(a,y)" using assms ..
then obtain b where "P(a,b)" ..
then have "∃x. P(x,b)" ..
then show "∃y x. P(x,y)" ..
qed
― ‹La demostración automática es›
lemma ejemplo_8_1c:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
using assms
by auto
text ‹
Ejemplo 8.2. Demostrar
∃y x. P(x,y) ⊢ ∃x y. P(x,y)›
― ‹La demostración detallada es›
lemma ejemplo_8_2a:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
proof -
obtain b where "∃x. P(x,b)" using assms by (rule exE)
then obtain a where "P(a,b)" by (rule exE)
then have "∃y. P(a,y)" by (rule exI)
then show "∃x y. P(x,y)" by (rule exI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_8_2b:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
proof -
obtain b where "∃x. P(x,b)" using assms ..
then obtain a where "P(a,b)" ..
then have "∃y. P(a,y)" ..
then show "∃x y. P(x,y)" ..
qed
― ‹La demostración estructurada es›
lemma ejemplo_8_2c:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
using assms
by auto
text ‹
Ejemplo 8.3 (p. 25). Demostrar
⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y))›
― ‹La demostración detallada es›
lemma ejemplo_8_3a:
"(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
proof (rule iffI)
assume "∃x y. P(x,y)"
then show "∃y x. P(x,y)" by (rule ejemplo_8_1a)
next
assume "∃y x. P(x,y)"
then show "∃x y. P(x,y)" by (rule ejemplo_8_2a)
qed
― ‹La demostración automática es›
lemma ejemplo_8_3b:
"(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
by auto
section ‹Reglas de la igualdad›
text ‹
Las reglas básicas de la igualdad son:
· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
›
text ‹
Ejemplo 9 (p. 27). Demostrar
x + 1 = 1 + x, x + 1 > 1 ⟶ x + 1 > 0 ⊢ 1 + x > 1 ⟶ 1 + x > 0
›
― ‹La demostración detallada es›
lemma ejemplo_9a:
assumes "x + 1 = 1 + x"
"x + 1 > 1 ⟶ x + 1 > 0"
shows "1 + x > 1 ⟶ 1 + x > 0"
proof -
show "1 + x > 1 ⟶ 1 + x > 0" using assms by (rule subst)
qed
― ‹La demostración estructurada es›
lemma ejemplo_9b:
assumes "x + 1 = 1 + x"
"x + 1 > 1 ⟶ x + 1 > 0"
shows "1 + x > 1 ⟶ 1 + x > 0"
using assms
by (rule subst)
― ‹La demostración automática es›
lemma ejemplo_9c:
assumes "x + 1 = 1 + x"
"x + 1 > 1 ⟶ x + 1 > 0"
shows "1 + x > 1 ⟶ 1 + x > 0"
using assms
by auto
text ‹
Ejemplo 10 (p. 27). Demostrar
x = y, y = z ⊢ x = z
›
― ‹La demostración detallada es›
lemma ejemplo_10a:
assumes "x = y"
"y = z"
shows "x = z"
proof -
show "x = z" using assms(2,1) by (rule subst)
qed
― ‹La demostración estructurada es›
lemma ejemplo_10b:
assumes "x = y"
"y = z"
shows "x = z"
using assms(2,1)
by (rule subst)
― ‹La demostración automática es›
lemma ejemplo_10c:
assumes "x = y"
"y = z"
shows "x = z"
using assms
by auto
text ‹
Ejemplo 11 (p. 28). Demostrar
s = t ⊢ t = s
›
― ‹La demostración detallada es›
lemma ejemplo_11a:
assumes "s = t"
shows "t = s"
proof -
have "s = s" by (rule refl)
with assms show "t = s" by (rule subst)
qed
― ‹La demostración automática es›
lemma ejemplo_11b:
assumes "s = t"
shows "t = s"
using assms
by auto
end