Demostración asistida por ordenador (2011-12) - Contribuciones del usuario [es]

Ejercicios del tema 4

2011-04-14T13:33:37Z

Mjoseh: Página creada con '<source lang="isar"> theory Relacion_10 imports Main begin section {* Deducción natural de primer orden *} text {* Los ejercicios de esta relación deben de resolverse usan...'

<source lang="isar">
theory Relacion_10
imports Main
begin

section {* Deducción natural de primer orden *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional y de primer
orden:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
oops

lemma ejercicio_2:
assumes "∃x. ¬P x"
shows " ¬(∀x. P x)"
oops

lemma ejercicio_3:
assumes "∀x. P x"
shows "∀y. P y"
oops

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
oops

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬Q x"
shows "¬(∃x. P x ∧ Q x)"
oops

lemma ejercicio_6:
assumes "∀x. ∀y. P x y"
shows "∀u. ∀v. P u v"
oops

lemma ejercicio_7:
assumes "∃x. ∃y. P x y"
shows "∃u. ∃v. P u v"
oops

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
oops

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
oops

lemma ejercicio_10:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

lemma ejercicio_11:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
oops

lemma ejercicio_12:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
oops

lemma ejercicio_13:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
oops

lemma ejercicio_14:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
oops

lemma ejercicio_15:
assumes "∀x.∀y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
oops

lemma ejercicio_16:
assumes "¬(∀x. ¬P x)"
shows "∃x. P x"
oops

lemma ejercicio_17:
assumes "∀x. ¬P x"
shows "¬(∃x. P x)"
oops

lemma ejercicio_18:
assumes "∃x. P x"
shows "¬(∀x. ¬P x)"
oops

lemma ejercicio_19:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
oops

lemma ejercicio_20:
assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
"∀x. ¬R x x"
shows "∀x.∀y. R x y ⟶ ¬R y x"
oops

lemma ejercicio_21:
assumes "∀x. P x ∨ Q x" and
"∃x. ¬Q x" and
"∀x. R x ⟶ ¬P x"
shows "∃x. ¬R x"
oops

lemma ejercicio_22:
assumes "∀x. P x ⟶ Q x ∨ R x" and
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
oops

lemma ejercicio_23:
assumes "∃x.∃y. R x y ∨ R y x"
shows "∃x.∃y. R x y"
oops

end
</source>

Tema 4 ej

2011-04-14T13:33:26Z

Ejercicios

2011-04-14T13:33:05Z

Mjoseh:

== Ejercicios de ''Demostración asistida por ordenador'' ==
* '''Tema 2:''' Razonamiento sobre programas ([[Rel_1|Enunciado]] y [[Relación 1|Solución colaborativa]]).
* '''Tema 3:''' Deducción natural proposicional con Isabelle ([[Tema_3_ej|Enunciado]] y [[Ejercicios del tema 3 |Solución colaborativa]]).
* '''Tema 4:''' Deducción natural en lógica de primer orden con Isabelle ([[Tema_4_ej|Enunciado]] y [[Ejercicios del tema 4 |Solución colaborativa]]).

Tema 4: Deducción natural en lógica de primer orden con Isabelle

2011-04-14T13:28:05Z

Mjoseh:

<source lang="isar">
header {* Deducción natural en la lógica de primer orden *}

theory LogicaDePrimerOrdenEj
imports Main
begin

text {*
En esta teoría se presentan los ejemplos del tema de deducción natural
en lógica de primer orden siguiendo la presentación de Huth y Ryan en su
libro "Logic in Computer Science"
http://www.cs.bham.ac.uk/research/projects/lics/ y, más concretamente,
a la forma como se explica en la asignatura de "Lógica informática" y
que puede verse en http://www.cs.us.es/~jalonso/cursos/li/temas/tema-7.pdf
*}

text {*
Se usarán las reglas del modus tollen y de la introducción de la
doble negación.
*}

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma notnotI:
"P ⟹ ¬¬P"
by auto

lemma
assumes "P(c)" and
"∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
proof (rule notI)
assume 1: "Q(c)"
have 2: "P(c) ⟶ ¬Q(c)" using assms(2) by (rule allE)
have 3: "¬¬Q(c)" using 1 by (rule notnotI)
have 4: "¬P(c)" using 2 3 by (rule mt)
thus "False" using assms(1) by (rule notE)
qed

lemma
assumes "∀x. (P x ⟶ ¬(Q x))" and
"∀x. P x"
shows "∀x. ¬(Q x)"
proof (rule allI)
fix x
have 1: "P x ⟶ ¬(Q x)" using assms(1) by (rule allE)
have 2: "P x" using assms(2) by (rule allE)
show "¬(Q x)" using 1 2 by (rule mp)
qed

lemma
assumes "∀x. P x"
shows "∃x. P x"
proof -
fix a
have "P a" using assms by (rule allE)
thus "∃x. P x" by (rule exI)
qed

lemma
assumes "∀x. (P x ⟶ Q x)" and
"∃x. P x"
shows "∃x. Q x"
proof -
obtain a where 1: "P a" using assms(2) by (rule exE)
have 2: "P a ⟶ Q a" using assms(1) by (rule allE)
have "Q a" using 2 1 by (rule mp)
thus "∃x. Q x" by (rule exI)
qed

lemma
assumes "∀x. (Q x ⟶ R x)" and
"∃x . (P x ∧ Q x)"
shows "∃x . (P x ∧ R x)"
proof -
obtain a where 1: "P a ∧ Q a" using assms(2) by (rule exE)
have 2: "Q a ⟶ R a" using assms(1) by (rule allE)
have 3: "Q a" using 1 by (rule conjunct2)
have 4: "R a" using 2 3 by (rule mp)
have 5: "P a" using 1 by (rule conjunct1)
hence "P a ∧ R a" using 4 by (rule conjI)
thus "∃x . (P x ∧ R x)" by (rule exI)
qed

lemma
assumes "∃x. P x" and
"∀x.∀y. (P x ⟶ Q y)"
shows "∀y. Q y"
proof (rule allI)
fix b
obtain a where 1: "P a" using assms(1) by (rule exE)
have "∀y. (P a ⟶ Q y)" using assms(2) by (rule allE)
hence "P a ⟶ Q b" by (rule allE)
thus "Q b" using 1 by (rule mp)
qed

lemma
assumes "∃x. ¬P x"
shows " ¬(∀x. P x)"
proof (rule notI)
assume 1: "∀x. P x"
obtain a where 2: "¬P a" using assms(1) by (rule exE)
have 3: "P a" using 1 by (rule allE)
show False using 2 3 by (rule notE)
qed

lemma
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
using assms
proof (rule disjE)
{ assume 1: "∀x. P x"
show "∀x. P x ∨ Q x"
proof (rule allI)
fix x
have "P x" using 1 by (rule allE)
thus "P x ∨ Q x" by (rule disjI1)
qed }
next
{ assume 2: "∀x. Q x"
show "∀x. P x ∨ Q x"
proof (rule allI)
fix x
have "Q x" using 2 by (rule allE)
thus "P x ∨ Q x" by (rule disjI2)
qed }
qed

lemma
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
assume 1: "∀x. P x"
show "∀x. Q x"
proof (rule allI)
fix x
have 2: "P x ⟶ Q x" using assms by (rule allE)
have 3: "P x" using 1 by (rule allE)
show "Q x" using 2 3 by (rule mp)
qed
qed

lemma
assumes "∀x. P x"
shows "∀y. P y"
proof (rule allI)
fix a
show "P a" using assms(1) by (rule allE)
qed

lemma
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
proof (rule impI)
assume 1: "∀x. ¬Q x"
show "∀x. ¬P x"
proof (rule allI)
fix x
have 2: "P x ⟶ Q x" using assms(1) by (rule allE)
have 3: "¬Q x" using 1 by (rule allE)
show "¬P x" using 2 3 by (rule mt)
qed
qed

lemma
assumes "∀x. P x ⟶ ¬Q x"
shows "¬(∃x. P x ∧ Q x)"
proof (rule notI)
assume "∃x. P x ∧ Q x"
then obtain a where 1: "P a ∧ Q a" by (rule exE)
have 2: "P a ⟶ ¬Q a" using assms(1) by (rule allE)
have 3: "P a" using 1 by (rule conjunct1)
have 4: "¬Q a" using 2 3 by (rule mp)
have 5: "Q a" using 1 by (rule conjunct2)
show False using 4 5 by (rule notE)
qed

lemma
assumes "∀x. ∀y. P x y"
shows "∀u. ∀v. P u v"
proof (rule allI)
fix u
show "∀v. P u v"
proof (rule allI)
fix v
have "∀y. P u y" using assms(1) by (rule allE)
thus "P u v" by (rule allE)
qed
qed

lemma
assumes "∃x. ∃y. P x y"
shows "∃u. ∃v. P u v"
proof -
obtain a where "∃y. P a y" using assms(1) by (rule exE)
then obtain b where "P a b" by (rule exE)
hence "∃v. P a v" by (rule exI)
thus "∃u. ∃v. P u v" by (rule exI)
qed

lemma
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof (rule allI)
fix y
obtain a where "∀y. P a y" using assms(1) by (rule exE)
hence "P a y" by (rule allE)
thus "∃x. P x y" by (rule exI)
qed

lemma
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof (rule impI)
assume 1: "P a"
obtain b where "P a ⟶ Q b" using assms(1) by (rule exE)
hence "Q b" using 1 by (rule mp)
thus "∃x. Q x" by (rule exI)
qed

lemma
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
have "¬P a ∨ P a" by (rule excluded_middle)
thus "∃x. P a ⟶ Q x"
proof (rule disjE)
{ assume "¬P a"
hence "P a ⟶ Q b" by simp
thus "∃x. P a ⟶ Q x" by (rule exI) }
next
{ assume "P a"
hence "∃x. Q x" using assms(1) by simp
then obtain c where "Q c" by (rule exE)
hence "P a ⟶ Q c" by simp
thus "∃x. P a ⟶ Q x" by (rule exI) }
qed
qed

lemma
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof (rule allI)
fix x
show "P x ⟶ Q a"
proof
assume "P x"
hence 1: "∃x. P x" by (rule exI)
show "Q a" using assms(1) 1 by (rule mp)
qed
qed

lemma
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof (rule exI)
show "P b ⟶ Q a" using assms(1) ..
qed

lemma
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof -
obtain a where 1: "P a ∧ Q a" using assms(1) by (rule exE)
hence "P a" by (rule conjunct1)
hence 2: "∃x. P x" by (rule exI)
have "Q a" using 1 by (rule conjunct2)
hence 3: "∃x. Q x" by (rule exI)
show "(∃x. P x) ∧ (∃x. Q x)" using 2 3 by (rule conjI)
qed

lemma
assumes "∀x.∀y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof (rule impI)
assume 1: "∃y. P y"
show "∀x. Q x"
proof (rule allI)
fix x
have 2: "∀y. P y ⟶ Q x" using assms by (rule allE)
obtain b where 3: "P b" using 1 by (rule exE)
have "P b ⟶ Q x" using 2 by (rule allE)
thus "Q x" using 3 by (rule mp)
qed
qed

lemma
assumes "¬(∀x. ¬P x)"
shows "∃x. P x"
proof (rule ccontr)
assume 1: "¬(∃x. P x)"
have 2: "∀x. ¬P x"
proof
fix x
show "¬P x"
proof
assume "P x"
hence 3: "∃x. P x" by (rule exI)
show False using 1 3 by (rule notE)
qed
qed
show False using assms(1) 2 by (rule notE)
qed

lemma
assumes "∀x. ¬P x"
shows "¬(∃x. P x)"
proof (rule notI)
assume "∃x. P x"
then obtain a where 1: "P a" by (rule exE)
have "¬P a" using assms(1) by (rule allE)
thus False using 1 by (rule notE)
qed

lemma
assumes "∃x. P x"
shows "¬(∀x. ¬P x)"
proof (rule notI)
assume 1: "∀x. ¬P x"
obtain a where 2: "P a" using assms(1) by (rule exE)
have "¬P a" using 1 by (rule allE)
thus False using 2 by (rule notE)
qed

lemma
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof (rule allI)
fix x
show "P a ⟶ Q x"
proof
assume 1: "P a"
have "∀x. Q x" using assms(1) 1 by (rule mp)
thus "Q x" by (rule allE)
qed
qed

lemma
assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
"∀x. ¬R x x"
shows "∀x.∀y. R x y ⟶ ¬R y x"
proof (rule allI)
fix x
show "∀y. R x y ⟶ ¬R y x"
proof (rule allI)
fix y
show "R x y ⟶ ¬R y x"
proof (rule impI)
assume 1: "R x y"
show "¬R y x"
proof
assume 2: "R y x"
have "∀y.∀z. R x y ∧ R y z ⟶ R x z" using assms(1) by (rule allE)
hence "∀z. R x y ∧ R y z ⟶ R x z" by (rule allE)
hence 3: "R x y ∧ R y x ⟶ R x x" by (rule allE)
have 4: "R x y ∧ R y x" using 1 2 by (rule conjI)
have 5: "R x x" using 3 4 by (rule mp)
have "¬R x x" using assms(2) by (rule allE)
thus False using 5 by (rule notE)
qed
qed
qed
qed

lemma
assumes "∀x. P x ∨ Q x" and
"∃x. ¬Q x" and
"∀x. R x ⟶ ¬P x"
shows "∃x. ¬R x"
proof -
obtain a where 1: "¬Q a" using assms(2) ..
have "P a ∨ Q a" using assms(1) ..
thus "∃x. ¬R x"
proof (rule disjE)
{ assume "P a"
hence 2: "¬¬P a" by (rule notnotI)
have "R a ⟶ ¬P a" using assms(3) by (rule allE)
hence "¬R a" using 2 by (rule mt)
thus "∃x. ¬R x" by (rule exI) }
next
{ assume 3: "Q a"
show "∃x. ¬R x" using 1 3 by (rule notE) }
qed
qed

lemma
assumes "∀x. P x ⟶ Q x ∨ R x" and
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof
fix x
show "P x ⟶ Q x"
proof
assume 1: "P x"
have "P x ⟶ Q x ∨ R x" using assms(1) by (rule allE)
hence "Q x ∨ R x" using 1 by (rule mp)
thus "Q x"
proof (rule disjE)
{ assume "Q x"
thus "Q x" by this }
next
{ assume 2: "R x"
have "P x ∧ R x" using 1 2 by (rule conjI)
hence 3: "∃x. P x ∧ R x" by (rule exI)
show "Q x" using assms(2) 3 by (rule notE) }
qed
qed
qed

lemma
assumes "∃x.∃y. R x y ∨ R y x"
shows "∃x.∃y. R x y"
proof -
obtain a where "∃y. R a y ∨ R y a" using assms(1) by (rule exE)
then obtain b where "R a b ∨ R b a" by (rule exE)
thus "∃x.∃y. R x y"
proof
{ assume "R a b"
hence "∃y. R a y" by (rule exI)
thus "∃x.∃y. R x y" by (rule exI) }
next
{ assume "R b a"
hence "∃y. R b y" by (rule exI)
thus "∃x.∃y. R x y" by (rule exI) }
qed
qed

end
</source>

Tema 4: Deducción natural en lógica de primer orden con Isabelle

2011-04-14T13:27:15Z

Mjoseh:

<source lang="isar">
header {* Deducción natural en la lógica de primer orden *}

theory LogicaDePrimerOrdenEj
imports Main
begin

text {*
En esta teoría se presentan los ejemplos del tema de deducción natural
en lógica de primer orden siguiendo la presentación de Huth y Ryan en su
libro "Logic in Computer Science"
http://www.cs.bham.ac.uk/research/projects/lics/ y, más concretamente,
a la forma como se explica en la asignatura de "Lógica informática" y
que puede verse en http://www.cs.us.es/~jalonso/cursos/li/temas/tema-7.pdf
*}

text {*
Se usarán las reglas del modus tollen y de la introducción de la
doble negación.
*}

lemma mt: "\<lbrakk>F \<longrightarrow> G; \<not>G\<rbrakk> \<Longrightarrow> \<not>F"
by auto

lemma notnotI:
"P \<Longrightarrow> \<not>\<not>P"
by auto

lemma
assumes "P(c)" and
"\<forall>x. (P(x) \<longrightarrow> \<not>Q(x))"
shows "\<not>Q(c)"
proof (rule notI)
assume 1: "Q(c)"
have 2: "P(c) \<longrightarrow> \<not>Q(c)" using assms(2) by (rule allE)
have 3: "\<not>\<not>Q(c)" using 1 by (rule notnotI)
have 4: "\<not>P(c)" using 2 3 by (rule mt)
thus "False" using assms(1) by (rule notE)
qed

lemma
assumes "\<forall>x. (P x \<longrightarrow> \<not>(Q x))" and
"\<forall>x. P x"
shows "\<forall>x. \<not>(Q x)"
proof (rule allI)
fix x
have 1: "P x \<longrightarrow> \<not>(Q x)" using assms(1) by (rule allE)
have 2: "P x" using assms(2) by (rule allE)
show "\<not>(Q x)" using 1 2 by (rule mp)
qed

lemma
assumes "\<forall>x. P x"
shows "\<exists>x. P x"
proof -
fix a
have "P a" using assms by (rule allE)
thus "\<exists>x. P x" by (rule exI)
qed

lemma
assumes "\<forall>x. (P x \<longrightarrow> Q x)" and
"\<exists>x. P x"
shows "\<exists>x. Q x"
proof -
obtain a where 1: "P a" using assms(2) by (rule exE)
have 2: "P a \<longrightarrow> Q a" using assms(1) by (rule allE)
have "Q a" using 2 1 by (rule mp)
thus "\<exists>x. Q x" by (rule exI)
qed

lemma
assumes "\<forall>x. (Q x \<longrightarrow> R x)" and
"\<exists>x . (P x \<and> Q x)"
shows "\<exists>x . (P x \<and> R x)"
proof -
obtain a where 1: "P a \<and> Q a" using assms(2) by (rule exE)
have 2: "Q a \<longrightarrow> R a" using assms(1) by (rule allE)
have 3: "Q a" using 1 by (rule conjunct2)
have 4: "R a" using 2 3 by (rule mp)
have 5: "P a" using 1 by (rule conjunct1)
hence "P a \<and> R a" using 4 by (rule conjI)
thus "\<exists>x . (P x \<and> R x)" by (rule exI)
qed

lemma
assumes "\<exists>x. P x" and
"\<forall>x.\<forall>y. (P x \<longrightarrow> Q y)"
shows "\<forall>y. Q y"
proof (rule allI)
fix b
obtain a where 1: "P a" using assms(1) by (rule exE)
have "\<forall>y. (P a \<longrightarrow> Q y)" using assms(2) by (rule allE)
hence "P a \<longrightarrow> Q b" by (rule allE)
thus "Q b" using 1 by (rule mp)
qed

lemma
assumes "\<exists>x. \<not>P x"
shows " \<not>(\<forall>x. P x)"
proof (rule notI)
assume 1: "\<forall>x. P x"
obtain a where 2: "\<not>P a" using assms(1) by (rule exE)
have 3: "P a" using 1 by (rule allE)
show False using 2 3 by (rule notE)
qed

lemma
assumes "(\<forall>x. P x) \<or> (\<forall>x. Q x)"
shows "\<forall>x. P x \<or> Q x"
using assms
proof (rule disjE)
{ assume 1: "\<forall>x. P x"
show "\<forall>x. P x \<or> Q x"
proof (rule allI)
fix x
have "P x" using 1 by (rule allE)
thus "P x \<or> Q x" by (rule disjI1)
qed }
next
{ assume 2: "\<forall>x. Q x"
show "\<forall>x. P x \<or> Q x"
proof (rule allI)
fix x
have "Q x" using 2 by (rule allE)
thus "P x \<or> Q x" by (rule disjI2)
qed }
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q x"
shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
proof (rule impI)
assume 1: "\<forall>x. P x"
show "\<forall>x. Q x"
proof (rule allI)
fix x
have 2: "P x \<longrightarrow> Q x" using assms by (rule allE)
have 3: "P x" using 1 by (rule allE)
show "Q x" using 2 3 by (rule mp)
qed
qed

lemma
assumes "\<forall>x. P x"
shows "\<forall>y. P y"
proof (rule allI)
fix a
show "P a" using assms(1) by (rule allE)
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q x"
shows "(\<forall>x. \<not>Q x) \<longrightarrow> (\<forall>x. \<not>P x)"
proof (rule impI)
assume 1: "\<forall>x. \<not>Q x"
show "\<forall>x. \<not>P x"
proof (rule allI)
fix x
have 2: "P x \<longrightarrow> Q x" using assms(1) by (rule allE)
have 3: "\<not>Q x" using 1 by (rule allE)
show "\<not>P x" using 2 3 by (rule mt)
qed
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> \<not>Q x"
shows "\<not>(\<exists>x. P x \<and> Q x)"
proof (rule notI)
assume "\<exists>x. P x \<and> Q x"
then obtain a where 1: "P a \<and> Q a" by (rule exE)
have 2: "P a \<longrightarrow> \<not>Q a" using assms(1) by (rule allE)
have 3: "P a" using 1 by (rule conjunct1)
have 4: "\<not>Q a" using 2 3 by (rule mp)
have 5: "Q a" using 1 by (rule conjunct2)
show False using 4 5 by (rule notE)
qed

lemma
assumes "\<forall>x. \<forall>y. P x y"
shows "\<forall>u. \<forall>v. P u v"
proof (rule allI)
fix u
show "\<forall>v. P u v"
proof (rule allI)
fix v
have "\<forall>y. P u y" using assms(1) by (rule allE)
thus "P u v" by (rule allE)
qed
qed

lemma
assumes "\<exists>x. \<exists>y. P x y"
shows "\<exists>u. \<exists>v. P u v"
proof -
obtain a where "\<exists>y. P a y" using assms(1) by (rule exE)
then obtain b where "P a b" by (rule exE)
hence "\<exists>v. P a v" by (rule exI)
thus "\<exists>u. \<exists>v. P u v" by (rule exI)
qed

lemma
assumes "\<exists>x. \<forall>y. P x y"
shows "\<forall>y. \<exists>x. P x y"
proof (rule allI)
fix y
obtain a where "\<forall>y. P a y" using assms(1) by (rule exE)
hence "P a y" by (rule allE)
thus "\<exists>x. P x y" by (rule exI)
qed

lemma
assumes "\<exists>x. P a \<longrightarrow> Q x"
shows "P a \<longrightarrow> (\<exists>x. Q x)"
proof (rule impI)
assume 1: "P a"
obtain b where "P a \<longrightarrow> Q b" using assms(1) by (rule exE)
hence "Q b" using 1 by (rule mp)
thus "\<exists>x. Q x" by (rule exI)
qed

lemma
assumes "P a \<longrightarrow> (\<exists>x. Q x)"
shows "\<exists>x. P a \<longrightarrow> Q x"
proof -
have "\<not>P a \<or> P a" by (rule excluded_middle)
thus "\<exists>x. P a \<longrightarrow> Q x"
proof (rule disjE)
{ assume "\<not>P a"
hence "P a \<longrightarrow> Q b" by simp
thus "\<exists>x. P a \<longrightarrow> Q x" by (rule exI) }
next
{ assume "P a"
hence "\<exists>x. Q x" using assms(1) by simp
then obtain c where "Q c" by (rule exE)
hence "P a \<longrightarrow> Q c" by simp
thus "\<exists>x. P a \<longrightarrow> Q x" by (rule exI) }
qed
qed

lemma
assumes "(\<exists>x. P x) \<longrightarrow> Q a"
shows "\<forall>x. P x \<longrightarrow> Q a"
proof (rule allI)
fix x
show "P x \<longrightarrow> Q a"
proof
assume "P x"
hence 1: "\<exists>x. P x" by (rule exI)
show "Q a" using assms(1) 1 by (rule mp)
qed
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q a"
shows "\<exists>x. P x \<longrightarrow> Q a"
proof (rule exI)
show "P b \<longrightarrow> Q a" using assms(1) ..
qed

lemma
assumes "\<exists>x. P x \<and> Q x"
shows "(\<exists>x. P x) \<and> (\<exists>x. Q x)"
proof -
obtain a where 1: "P a \<and> Q a" using assms(1) by (rule exE)
hence "P a" by (rule conjunct1)
hence 2: "\<exists>x. P x" by (rule exI)
have "Q a" using 1 by (rule conjunct2)
hence 3: "\<exists>x. Q x" by (rule exI)
show "(\<exists>x. P x) \<and> (\<exists>x. Q x)" using 2 3 by (rule conjI)
qed

lemma
assumes "\<forall>x.\<forall>y. P y \<longrightarrow> Q x"
shows "(\<exists>y. P y) \<longrightarrow> (\<forall>x. Q x)"
proof (rule impI)
assume 1: "\<exists>y. P y"
show "\<forall>x. Q x"
proof (rule allI)
fix x
have 2: "\<forall>y. P y \<longrightarrow> Q x" using assms by (rule allE)
obtain b where 3: "P b" using 1 by (rule exE)
have "P b \<longrightarrow> Q x" using 2 by (rule allE)
thus "Q x" using 3 by (rule mp)
qed
qed

lemma
assumes "\<not>(\<forall>x. \<not>P x)"
shows "\<exists>x. P x"
proof (rule ccontr)
assume 1: "\<not>(\<exists>x. P x)"
have 2: "\<forall>x. \<not>P x"
proof
fix x
show "\<not>P x"
proof
assume "P x"
hence 3: "\<exists>x. P x" by (rule exI)
show False using 1 3 by (rule notE)
qed
qed
show False using assms(1) 2 by (rule notE)
qed

lemma
assumes "\<forall>x. \<not>P x"
shows "\<not>(\<exists>x. P x)"
proof (rule notI)
assume "\<exists>x. P x"
then obtain a where 1: "P a" by (rule exE)
have "\<not>P a" using assms(1) by (rule allE)
thus False using 1 by (rule notE)
qed

lemma
assumes "\<exists>x. P x"
shows "\<not>(\<forall>x. \<not>P x)"
proof (rule notI)
assume 1: "\<forall>x. \<not>P x"
obtain a where 2: "P a" using assms(1) by (rule exE)
have "\<not>P a" using 1 by (rule allE)
thus False using 2 by (rule notE)
qed

lemma
assumes "P a \<longrightarrow> (\<forall>x. Q x)"
shows "\<forall>x. P a \<longrightarrow> Q x"
proof (rule allI)
fix x
show "P a \<longrightarrow> Q x"
proof
assume 1: "P a"
have "\<forall>x. Q x" using assms(1) 1 by (rule mp)
thus "Q x" by (rule allE)
qed
qed

lemma
assumes "\<forall>x.\<forall>y.\<forall>z. R x y \<and> R y z \<longrightarrow> R x z" and
"\<forall>x. \<not>R x x"
shows "\<forall>x.\<forall>y. R x y \<longrightarrow> \<not>R y x"
proof (rule allI)
fix x
show "\<forall>y. R x y \<longrightarrow> \<not>R y x"
proof (rule allI)
fix y
show "R x y \<longrightarrow> \<not>R y x"
proof (rule impI)
assume 1: "R x y"
show "\<not>R y x"
proof
assume 2: "R y x"
have "\<forall>y.\<forall>z. R x y \<and> R y z \<longrightarrow> R x z" using assms(1) by (rule allE)
hence "\<forall>z. R x y \<and> R y z \<longrightarrow> R x z" by (rule allE)
hence 3: "R x y \<and> R y x \<longrightarrow> R x x" by (rule allE)
have 4: "R x y \<and> R y x" using 1 2 by (rule conjI)
have 5: "R x x" using 3 4 by (rule mp)
have "\<not>R x x" using assms(2) by (rule allE)
thus False using 5 by (rule notE)
qed
qed
qed
qed

lemma
assumes "\<forall>x. P x \<or> Q x" and
"\<exists>x. \<not>Q x" and
"\<forall>x. R x \<longrightarrow> \<not>P x"
shows "\<exists>x. \<not>R x"
proof -
obtain a where 1: "\<not>Q a" using assms(2) ..
have "P a \<or> Q a" using assms(1) ..
thus "\<exists>x. \<not>R x"
proof (rule disjE)
{ assume "P a"
hence 2: "\<not>\<not>P a" by (rule notnotI)
have "R a \<longrightarrow> \<not>P a" using assms(3) by (rule allE)
hence "\<not>R a" using 2 by (rule mt)
thus "\<exists>x. \<not>R x" by (rule exI) }
next
{ assume 3: "Q a"
show "\<exists>x. \<not>R x" using 1 3 by (rule notE) }
qed
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q x \<or> R x" and
"\<not>(\<exists>x. P x \<and> R x)"
shows "\<forall>x. P x \<longrightarrow> Q x"
proof
fix x
show "P x \<longrightarrow> Q x"
proof
assume 1: "P x"
have "P x \<longrightarrow> Q x \<or> R x" using assms(1) by (rule allE)
hence "Q x \<or> R x" using 1 by (rule mp)
thus "Q x"
proof (rule disjE)
{ assume "Q x"
thus "Q x" by this }
next
{ assume 2: "R x"
have "P x \<and> R x" using 1 2 by (rule conjI)
hence 3: "\<exists>x. P x \<and> R x" by (rule exI)
show "Q x" using assms(2) 3 by (rule notE) }
qed
qed
qed

lemma
assumes "\<exists>x.\<exists>y. R x y \<or> R y x"
shows "\<exists>x.\<exists>y. R x y"
proof -
obtain a where "\<exists>y. R a y \<or> R y a" using assms(1) by (rule exE)
then obtain b where "R a b \<or> R b a" by (rule exE)
thus "\<exists>x.\<exists>y. R x y"
proof
{ assume "R a b"
hence "\<exists>y. R a y" by (rule exI)
thus "\<exists>x.\<exists>y. R x y" by (rule exI) }
next
{ assume "R b a"
hence "\<exists>y. R b y" by (rule exI)
thus "\<exists>x.\<exists>y. R x y" by (rule exI) }
qed
qed

end
</source>

Tema 4: Deducción natural en lógica de primer orden con Isabelle

2011-04-14T13:26:19Z

Mjoseh: Página creada con 'header {* Deducción natural en la lógica de primer orden *} theory LogicaDePrimerOrdenEj imports Main begin text {* En esta teoría se presentan los ejemplos del tema de...'

header {* Deducción natural en la lógica de primer orden *}

theory LogicaDePrimerOrdenEj
imports Main
begin

text {*
En esta teoría se presentan los ejemplos del tema de deducción natural
en lógica de primer orden siguiendo la presentación de Huth y Ryan en su
libro "Logic in Computer Science"
http://www.cs.bham.ac.uk/research/projects/lics/ y, más concretamente,
a la forma como se explica en la asignatura de "Lógica informática" y
que puede verse en http://www.cs.us.es/~jalonso/cursos/li/temas/tema-7.pdf
*}

text {*
Se usarán las reglas del modus tollen y de la introducción de la
doble negación.
*}

lemma mt: "\<lbrakk>F \<longrightarrow> G; \<not>G\<rbrakk> \<Longrightarrow> \<not>F"
by auto

lemma notnotI:
"P \<Longrightarrow> \<not>\<not>P"
by auto

lemma
assumes "P(c)" and
"\<forall>x. (P(x) \<longrightarrow> \<not>Q(x))"
shows "\<not>Q(c)"
proof (rule notI)
assume 1: "Q(c)"
have 2: "P(c) \<longrightarrow> \<not>Q(c)" using assms(2) by (rule allE)
have 3: "\<not>\<not>Q(c)" using 1 by (rule notnotI)
have 4: "\<not>P(c)" using 2 3 by (rule mt)
thus "False" using assms(1) by (rule notE)
qed

lemma
assumes "\<forall>x. (P x \<longrightarrow> \<not>(Q x))" and
"\<forall>x. P x"
shows "\<forall>x. \<not>(Q x)"
proof (rule allI)
fix x
have 1: "P x \<longrightarrow> \<not>(Q x)" using assms(1) by (rule allE)
have 2: "P x" using assms(2) by (rule allE)
show "\<not>(Q x)" using 1 2 by (rule mp)
qed

lemma
assumes "\<forall>x. P x"
shows "\<exists>x. P x"
proof -
fix a
have "P a" using assms by (rule allE)
thus "\<exists>x. P x" by (rule exI)
qed

lemma
assumes "\<forall>x. (P x \<longrightarrow> Q x)" and
"\<exists>x. P x"
shows "\<exists>x. Q x"
proof -
obtain a where 1: "P a" using assms(2) by (rule exE)
have 2: "P a \<longrightarrow> Q a" using assms(1) by (rule allE)
have "Q a" using 2 1 by (rule mp)
thus "\<exists>x. Q x" by (rule exI)
qed

lemma
assumes "\<forall>x. (Q x \<longrightarrow> R x)" and
"\<exists>x . (P x \<and> Q x)"
shows "\<exists>x . (P x \<and> R x)"
proof -
obtain a where 1: "P a \<and> Q a" using assms(2) by (rule exE)
have 2: "Q a \<longrightarrow> R a" using assms(1) by (rule allE)
have 3: "Q a" using 1 by (rule conjunct2)
have 4: "R a" using 2 3 by (rule mp)
have 5: "P a" using 1 by (rule conjunct1)
hence "P a \<and> R a" using 4 by (rule conjI)
thus "\<exists>x . (P x \<and> R x)" by (rule exI)
qed

lemma
assumes "\<exists>x. P x" and
"\<forall>x.\<forall>y. (P x \<longrightarrow> Q y)"
shows "\<forall>y. Q y"
proof (rule allI)
fix b
obtain a where 1: "P a" using assms(1) by (rule exE)
have "\<forall>y. (P a \<longrightarrow> Q y)" using assms(2) by (rule allE)
hence "P a \<longrightarrow> Q b" by (rule allE)
thus "Q b" using 1 by (rule mp)
qed

lemma
assumes "\<exists>x. \<not>P x"
shows " \<not>(\<forall>x. P x)"
proof (rule notI)
assume 1: "\<forall>x. P x"
obtain a where 2: "\<not>P a" using assms(1) by (rule exE)
have 3: "P a" using 1 by (rule allE)
show False using 2 3 by (rule notE)
qed

lemma
assumes "(\<forall>x. P x) \<or> (\<forall>x. Q x)"
shows "\<forall>x. P x \<or> Q x"
using assms
proof (rule disjE)
{ assume 1: "\<forall>x. P x"
show "\<forall>x. P x \<or> Q x"
proof (rule allI)
fix x
have "P x" using 1 by (rule allE)
thus "P x \<or> Q x" by (rule disjI1)
qed }
next
{ assume 2: "\<forall>x. Q x"
show "\<forall>x. P x \<or> Q x"
proof (rule allI)
fix x
have "Q x" using 2 by (rule allE)
thus "P x \<or> Q x" by (rule disjI2)
qed }
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q x"
shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
proof (rule impI)
assume 1: "\<forall>x. P x"
show "\<forall>x. Q x"
proof (rule allI)
fix x
have 2: "P x \<longrightarrow> Q x" using assms by (rule allE)
have 3: "P x" using 1 by (rule allE)
show "Q x" using 2 3 by (rule mp)
qed
qed

lemma
assumes "\<forall>x. P x"
shows "\<forall>y. P y"
proof (rule allI)
fix a
show "P a" using assms(1) by (rule allE)
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q x"
shows "(\<forall>x. \<not>Q x) \<longrightarrow> (\<forall>x. \<not>P x)"
proof (rule impI)
assume 1: "\<forall>x. \<not>Q x"
show "\<forall>x. \<not>P x"
proof (rule allI)
fix x
have 2: "P x \<longrightarrow> Q x" using assms(1) by (rule allE)
have 3: "\<not>Q x" using 1 by (rule allE)
show "\<not>P x" using 2 3 by (rule mt)
qed
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> \<not>Q x"
shows "\<not>(\<exists>x. P x \<and> Q x)"
proof (rule notI)
assume "\<exists>x. P x \<and> Q x"
then obtain a where 1: "P a \<and> Q a" by (rule exE)
have 2: "P a \<longrightarrow> \<not>Q a" using assms(1) by (rule allE)
have 3: "P a" using 1 by (rule conjunct1)
have 4: "\<not>Q a" using 2 3 by (rule mp)
have 5: "Q a" using 1 by (rule conjunct2)
show False using 4 5 by (rule notE)
qed

lemma
assumes "\<forall>x. \<forall>y. P x y"
shows "\<forall>u. \<forall>v. P u v"
proof (rule allI)
fix u
show "\<forall>v. P u v"
proof (rule allI)
fix v
have "\<forall>y. P u y" using assms(1) by (rule allE)
thus "P u v" by (rule allE)
qed
qed

lemma
assumes "\<exists>x. \<exists>y. P x y"
shows "\<exists>u. \<exists>v. P u v"
proof -
obtain a where "\<exists>y. P a y" using assms(1) by (rule exE)
then obtain b where "P a b" by (rule exE)
hence "\<exists>v. P a v" by (rule exI)
thus "\<exists>u. \<exists>v. P u v" by (rule exI)
qed

lemma
assumes "\<exists>x. \<forall>y. P x y"
shows "\<forall>y. \<exists>x. P x y"
proof (rule allI)
fix y
obtain a where "\<forall>y. P a y" using assms(1) by (rule exE)
hence "P a y" by (rule allE)
thus "\<exists>x. P x y" by (rule exI)
qed

lemma
assumes "\<exists>x. P a \<longrightarrow> Q x"
shows "P a \<longrightarrow> (\<exists>x. Q x)"
proof (rule impI)
assume 1: "P a"
obtain b where "P a \<longrightarrow> Q b" using assms(1) by (rule exE)
hence "Q b" using 1 by (rule mp)
thus "\<exists>x. Q x" by (rule exI)
qed

lemma
assumes "P a \<longrightarrow> (\<exists>x. Q x)"
shows "\<exists>x. P a \<longrightarrow> Q x"
proof -
have "\<not>P a \<or> P a" by (rule excluded_middle)
thus "\<exists>x. P a \<longrightarrow> Q x"
proof (rule disjE)
{ assume "\<not>P a"
hence "P a \<longrightarrow> Q b" by simp
thus "\<exists>x. P a \<longrightarrow> Q x" by (rule exI) }
next
{ assume "P a"
hence "\<exists>x. Q x" using assms(1) by simp
then obtain c where "Q c" by (rule exE)
hence "P a \<longrightarrow> Q c" by simp
thus "\<exists>x. P a \<longrightarrow> Q x" by (rule exI) }
qed
qed

lemma
assumes "(\<exists>x. P x) \<longrightarrow> Q a"
shows "\<forall>x. P x \<longrightarrow> Q a"
proof (rule allI)
fix x
show "P x \<longrightarrow> Q a"
proof
assume "P x"
hence 1: "\<exists>x. P x" by (rule exI)
show "Q a" using assms(1) 1 by (rule mp)
qed
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q a"
shows "\<exists>x. P x \<longrightarrow> Q a"
proof (rule exI)
show "P b \<longrightarrow> Q a" using assms(1) ..
qed

lemma
assumes "\<exists>x. P x \<and> Q x"
shows "(\<exists>x. P x) \<and> (\<exists>x. Q x)"
proof -
obtain a where 1: "P a \<and> Q a" using assms(1) by (rule exE)
hence "P a" by (rule conjunct1)
hence 2: "\<exists>x. P x" by (rule exI)
have "Q a" using 1 by (rule conjunct2)
hence 3: "\<exists>x. Q x" by (rule exI)
show "(\<exists>x. P x) \<and> (\<exists>x. Q x)" using 2 3 by (rule conjI)
qed

lemma
assumes "\<forall>x.\<forall>y. P y \<longrightarrow> Q x"
shows "(\<exists>y. P y) \<longrightarrow> (\<forall>x. Q x)"
proof (rule impI)
assume 1: "\<exists>y. P y"
show "\<forall>x. Q x"
proof (rule allI)
fix x
have 2: "\<forall>y. P y \<longrightarrow> Q x" using assms by (rule allE)
obtain b where 3: "P b" using 1 by (rule exE)
have "P b \<longrightarrow> Q x" using 2 by (rule allE)
thus "Q x" using 3 by (rule mp)
qed
qed

lemma
assumes "\<not>(\<forall>x. \<not>P x)"
shows "\<exists>x. P x"
proof (rule ccontr)
assume 1: "\<not>(\<exists>x. P x)"
have 2: "\<forall>x. \<not>P x"
proof
fix x
show "\<not>P x"
proof
assume "P x"
hence 3: "\<exists>x. P x" by (rule exI)
show False using 1 3 by (rule notE)
qed
qed
show False using assms(1) 2 by (rule notE)
qed

lemma
assumes "\<forall>x. \<not>P x"
shows "\<not>(\<exists>x. P x)"
proof (rule notI)
assume "\<exists>x. P x"
then obtain a where 1: "P a" by (rule exE)
have "\<not>P a" using assms(1) by (rule allE)
thus False using 1 by (rule notE)
qed

lemma
assumes "\<exists>x. P x"
shows "\<not>(\<forall>x. \<not>P x)"
proof (rule notI)
assume 1: "\<forall>x. \<not>P x"
obtain a where 2: "P a" using assms(1) by (rule exE)
have "\<not>P a" using 1 by (rule allE)
thus False using 2 by (rule notE)
qed

lemma
assumes "P a \<longrightarrow> (\<forall>x. Q x)"
shows "\<forall>x. P a \<longrightarrow> Q x"
proof (rule allI)
fix x
show "P a \<longrightarrow> Q x"
proof
assume 1: "P a"
have "\<forall>x. Q x" using assms(1) 1 by (rule mp)
thus "Q x" by (rule allE)
qed
qed

lemma
assumes "\<forall>x.\<forall>y.\<forall>z. R x y \<and> R y z \<longrightarrow> R x z" and
"\<forall>x. \<not>R x x"
shows "\<forall>x.\<forall>y. R x y \<longrightarrow> \<not>R y x"
proof (rule allI)
fix x
show "\<forall>y. R x y \<longrightarrow> \<not>R y x"
proof (rule allI)
fix y
show "R x y \<longrightarrow> \<not>R y x"
proof (rule impI)
assume 1: "R x y"
show "\<not>R y x"
proof
assume 2: "R y x"
have "\<forall>y.\<forall>z. R x y \<and> R y z \<longrightarrow> R x z" using assms(1) by (rule allE)
hence "\<forall>z. R x y \<and> R y z \<longrightarrow> R x z" by (rule allE)
hence 3: "R x y \<and> R y x \<longrightarrow> R x x" by (rule allE)
have 4: "R x y \<and> R y x" using 1 2 by (rule conjI)
have 5: "R x x" using 3 4 by (rule mp)
have "\<not>R x x" using assms(2) by (rule allE)
thus False using 5 by (rule notE)
qed
qed
qed
qed

lemma
assumes "\<forall>x. P x \<or> Q x" and
"\<exists>x. \<not>Q x" and
"\<forall>x. R x \<longrightarrow> \<not>P x"
shows "\<exists>x. \<not>R x"
proof -
obtain a where 1: "\<not>Q a" using assms(2) ..
have "P a \<or> Q a" using assms(1) ..
thus "\<exists>x. \<not>R x"
proof (rule disjE)
{ assume "P a"
hence 2: "\<not>\<not>P a" by (rule notnotI)
have "R a \<longrightarrow> \<not>P a" using assms(3) by (rule allE)
hence "\<not>R a" using 2 by (rule mt)
thus "\<exists>x. \<not>R x" by (rule exI) }
next
{ assume 3: "Q a"
show "\<exists>x. \<not>R x" using 1 3 by (rule notE) }
qed
qed

lemma
assumes "\<forall>x. P x \<longrightarrow> Q x \<or> R x" and
"\<not>(\<exists>x. P x \<and> R x)"
shows "\<forall>x. P x \<longrightarrow> Q x"
proof
fix x
show "P x \<longrightarrow> Q x"
proof
assume 1: "P x"
have "P x \<longrightarrow> Q x \<or> R x" using assms(1) by (rule allE)
hence "Q x \<or> R x" using 1 by (rule mp)
thus "Q x"
proof (rule disjE)
{ assume "Q x"
thus "Q x" by this }
next
{ assume 2: "R x"
have "P x \<and> R x" using 1 2 by (rule conjI)
hence 3: "\<exists>x. P x \<and> R x" by (rule exI)
show "Q x" using assms(2) 3 by (rule notE) }
qed
qed
qed

lemma
assumes "\<exists>x.\<exists>y. R x y \<or> R y x"
shows "\<exists>x.\<exists>y. R x y"
proof -
obtain a where "\<exists>y. R a y \<or> R y a" using assms(1) by (rule exE)
then obtain b where "R a b \<or> R b a" by (rule exE)
thus "\<exists>x.\<exists>y. R x y"
proof
{ assume "R a b"
hence "\<exists>y. R a y" by (rule exI)
thus "\<exists>x.\<exists>y. R x y" by (rule exI) }
next
{ assume "R b a"
hence "\<exists>y. R b y" by (rule exI)
thus "\<exists>x.\<exists>y. R x y" by (rule exI) }
qed
qed

end

Temas

2011-04-14T13:25:21Z

Mjoseh:

== Temas de ''Demostración asistida por ordenador'' ==
* [[Tema 1: Isabelle como un lenguaje funcional]].
* [[Tema 2: Razonamiento sobre programas]].
* [[Tema 3: Deducción lógica proposicional con Isabelle]].
* [[Tema 4: Deducción natural en lógica de primer orden con Isabelle]].