Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

2018-07-16T07:50:07Z

Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso en 18:05 2 feb 2011

2011-02-02T18:05:01Z

Jalonso en 17:56 2 feb 2011

2011-02-02T17:56:34Z

Jalonso en 17:45 2 feb 2011

2011-02-02T17:45:30Z

Jalonso: Protegió «Relación 1a» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2011-02-02T17:29:30Z

Protegió «Relación 1a» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso en 17:28 2 feb 2011

2011-02-02T17:28:45Z

Jalonso: Página creada con ' header {* Deducción natural proposicional } theory LogicaProposicional imports Main begin text { En esta teoría se presentan los ejemplos del tema ...'

2011-02-02T17:23:13Z

Página creada con '<source lang="isar"> header {* Deducción natural proposicional *} theory LogicaProposicional imports Main begin text {* En esta teoría se presentan los ejemplos del tema ...'

Página nueva

<source lang="isar">
header {* Deducción natural proposicional *}

theory LogicaProposicional
imports Main
begin

text {*
En esta teoría se presentan los ejemplos del tema de deducción natural
proposicional 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-2.pdf

La página al lado de cada teorema indica la página de las anteriores
transparencias donde se encuentra la demostración.
*}

section {* Reglas de la conjunción *}

text {*
La regla de introducción de la conjunción es
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
Las reglas de eliminación de la conjunción son
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
*}

lemma -- "p. 4"
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 by (rule conjunct2)
show "q ∧ r" using 3 2 by (rule conjI)
qed

lemma
assumes 1: "(p ∧ q) ∧ r" and
2: "s ∧ t"
shows "q ∧ s"
proof -
have 3: "p ∧ q" using 1 by (rule conjunct1)
have 4: "q" using 3 by (rule conjunct2)
have 5: "s" using 2 by (rule conjunct1)
show "q ∧ s" using 4 5 by (rule conjI)
qed

section {* Reglas de la doble negación *}

text {*
La regla de eliminación de la doble negación es
· notnotD: ¬¬ P ⟹ P
Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
introducción de la doble negación
. notnotI: P ⟹ ¬¬ P
que, de momento, no detallamos su demostración.
*}

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

lemma -- "p. 5"
assumes 1: "p" and
2: "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have 3: "¬¬p" using 1 by (rule notnotI)
have 4: "q ∧ r" using 2 by (rule notnotD)
have 5: "r" using 4 by (rule conjunct2)
show "¬¬p ∧ r" using 3 5 by (rule conjI)
qed

section {* Regla de eliminación del condicional *}

text {*
La regla de eliminación del condicional es la regla del modus ponens
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
*}

lemma -- "p. 6"
assumes 1: "¬p ∧ q" and
2: "¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using 2 1 by (rule mp)
qed

lemma -- "p. 6"
assumes 1: "p" and
2: "p ⟶ q" and
3: "p ⟶ (q ⟶ r)"
shows "r"
proof -
have 4: "q" using 2 1 by (rule mp)
have 5: "q ⟶ r" using 3 1 by (rule mp)
show "r" using 5 4 by (rule mp)
qed

section {* Regla derivada del modus tollens *}

text {*
Para ajustarnos al tema de LI vamos a introducir la regla del modus
tollens
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
sin, de momento, detallar su demostración.
*}

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

lemma -- "p. 7"
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p" and
3: "¬r"
shows "¬q"
proof -
have 4: "q ⟶ r" using 1 2 by (rule mp)
show "¬q" using 4 3 by (rule mt)
qed

lemma -- "p. 7"
assumes 1: "¬p ⟶ q" and
2: "¬q"
shows "p"
proof -
have 3: "¬¬p" using 1 2 by (rule mt)
show "p" using 3 by (rule notnotD)
qed

lemma
assumes 1: "p ⟶ ¬q" and
2: "q"
shows "¬p"
proof -
have 3: "¬¬q" using 2 by (rule notnotI)
show "¬p" using 1 3 by (rule mt)
qed

section {* Regla de introducción del condicional *}

text {*
La regla de introducción del condicional es
· impI: (P ⟹ Q) ⟹ P ⟶ Q
*}

lemma -- "p. 8"
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof -
{ assume 3: "¬q"
have "¬p" using 1 3 by (rule mt)
} thus "¬q ⟶ ¬p" by (rule impI)
qed

lemma -- "p. 8"
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
assume 3: "¬q"
show "¬p" using 1 3 by (rule mt)
qed

lemma -- "p. 8"
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume 3: "¬q"
show "¬p" using 1 3 by (rule mt)
qed

lemma -- "p. 9"
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof -
{ assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have "¬¬q" using 1 3 by (rule mt)
} thus "p ⟶ ¬¬q" by (rule impI)
qed

lemma -- "p. 9"
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof (rule impI)
assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
show "¬¬q" using 1 3 by (rule mt)
qed

lemma -- "p. 9"
"p ⟶ p"
proof (rule impI)
qed

lemma -- "p. 10"
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof -
{ assume 1: "q ⟶ r"
{ assume 2: "¬q ⟶ ¬p"
{ assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
have "r" using 1 6 by (rule mp)
} hence "p ⟶ r" by (rule impI)
} hence "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI)
} thus "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

lemma -- "p. 10"
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 by (rule mp)
qed
qed
qed

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

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

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

section {* Reglas de la disyunción *}

text {*
Las reglas de la introducción de la disyunción son
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
La regla de elimación de la disyunción es
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
*}

lemma -- "p. 11"
assumes 1: "p ∨ q"
shows "q ∨ p"
using 1
proof (rule disjE)
{ assume 2: "p"
show "q ∨ p" using 2 by (rule disjI2) }
next
{ assume 3: "q"
show "q ∨ p" using 3 by (rule disjI1) }
qed

lemma -- "p. 12"
assumes 1: "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume 2: "p ∨ q"
thus "p ∨ r"
proof (rule disjE)
{ assume 3: "p"
show "p ∨ r" using 3 by (rule disjI1) }
next
{ assume 4: "q"
have 5: "r" using 1 4 by (rule mp)
show "p ∨ r" using 5 by (rule disjI2) }
qed
qed

lemma
assumes 1: "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using 1
proof (rule disjE)
{ assume 2: "p ∨ q"
thus "p ∨ (q ∨ r)"
proof (rule disjE)
{ assume 3: "p"
show "p ∨ (q ∨ r)" using 3 by (rule disjI1) }
next
{ assume 4: "q"
have 5: "q ∨ r" using 4 by (rule disjI1)
show "p ∨ (q ∨ r)" using 5 by (rule disjI2) }
qed }
next
{ assume 6: "r"
have 7: "q ∨ r" using 6 by (rule disjI2)
show "p ∨ (q ∨ r)" using 7 by (rule disjI2) }
qed

lemma
assumes 1: "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 2: "p" using 1 ..
have "q ∨ r" using 1 ..
thus "(p ∧ q) ∨ (p ∧ r)"
proof (rule disjE)
{ assume 3: "q"
have "p ∧ q" using 2 3 by (rule conjI)
thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1) }
next
{ assume 4: "r"
have "p ∧ r" using 2 4 by (rule conjI)
thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2) }
qed
qed

section {* Regla de copia *}

lemma -- "p. 13"
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof
assume "q"
show "p" using 1 by this
qed
qed

lemma -- "p. 13"
"p ⟶ (q ⟶ p)"
proof
assume "p"
thus "q ⟶ p" by (rule impI)
qed

section {* Reglas de la negación *}

text {*
La regla de eliminación de lo falso es
· FalseE: False ⟹ P
La regla de eliminación de la negación es
· notE: ⟦¬P; P⟧ ⟹ R
La regla de introducción de la negación es
· notI: (P ⟹ False) ⟹ ¬P
*}

lemma -- "p. 15"
assumes 1: "¬p ∨ q"
shows "p ⟶ q"
proof
assume 2: "p"
note 1
thus "q"
proof (rule disjE)
{ assume 3: "¬p"
show "q" using 3 2 by (rule notE) }
next
{ assume "q"
thus "q" by this}
qed
qed

lemma -- "p. 16"
assumes 1: "p ⟶ q" and
2: "p ⟶ ¬q"
shows "¬p"
proof (rule notI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "¬q" using 2 3 by (rule mp)
show False using 5 4 by (rule notE)
qed

lemma
assumes 1: "p ⟶ ¬p"
shows "¬p"
proof (rule notI)
assume 2: "p"
have 3: "¬p" using 1 2 by (rule mp)
show False using 3 2 by (rule notE)
qed

lemma
assumes 1: "p ∧ ¬q ⟶ r" and
2: "¬r" and
3: "p"
shows "q"
proof -
have "¬¬q"
proof (rule notI)
assume 4: "¬q"
have 5: "p ∧ ¬q" using 3 4 by (rule conjI)
have 6: "r" using 1 5 by (rule mp)
show False using 2 6 by (rule notE)
qed
thus "q" by (rule notnotD)
qed

lemma
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p" and
3: "¬r"
shows "¬q"
proof (rule notI)
assume 4: "q"
have 5: "q ⟶ r" using 1 2 by (rule mp)
have 6: "r" using 5 4 by (rule mp)
show False using 3 6 by (rule notE)
qed

section {* Reglas del bicondicional *}

text {*
La regla de introducción del bicondicional es
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
Las reglas de eliminación del bicondicional son
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
*}

lemma -- "p. 17"
"(p ∧ q) = (q ∧ p)"
proof (rule iffI)
{ assume 1: "p ∧ q"
have 2: "p" using 1 by (rule conjunct1)
have 3: "q" using 1 by (rule conjunct2)
show "q ∧ p" using 3 2 by (rule conjI) }
next
{ assume 4: "q ∧ p"
have 5: "q" using 4 by (rule conjunct1)
have 6: "p" using 4 by (rule conjunct2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

lemma -- "p. 18"
assumes 1: "p = q" and
2: "p ∨ q"
shows "p ∧ q"
using 2
proof (rule disjE)
{ assume 3: "p"
have 4: "q" using 1 3 by (rule iffD1)
show "p ∧ q" using 3 4 by (rule conjI) }
next
{ assume 5: "q"
have 6: "p" using 1 5 by (rule iffD2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

section {* Reglas derivadas *}

subsection {* Regla del modus tollens *}

lemma -- "p. 20"
assumes 1: "F ⟶ G" and
2: "¬G"
shows "¬F"
proof (rule notI)
assume 3: "F"
have 4: "G" using 1 3 by (rule mp)
show False using 2 4 by (rule notE)
qed

subsection {* Regla de la introducción de la doble negación *}

lemma -- "p. 21"
assumes 1: "F"
shows "¬¬F"
proof (rule notI)
assume 2: "¬F"
show False using 2 1 by (rule notE)
qed

subsection {* Regla de reducción al absurdo *}

lemma -- "p. 22"
assumes 1: "¬F ⟶ False"
shows "F"
proof -
have 2: "¬¬F"
proof (rule notI)
assume 3: "¬F"
show False using 1 3 by (rule mp)
qed
show "F" using 2 by (rule notnotD)
qed

text {*
La regla de reducción al absurdo en Isabelle se correponde con la
regla de contradicción
· ccontr: (¬P ⟹ False) ⟹ P
*}

subsection {* Ley del tercio excluso *}

text {*
La ley del tercio excluso es
· excluded_middle: ¬P ∨ P
Puede demostrarse como se muestra a continuación.
*}

lemma -- "p. 23"
"F ∨ ¬F"
proof (rule ccontr)
assume 1: "¬(F ∨ ¬F)"
thus False
proof (rule notE)
show "F ∨ ¬F"
proof (rule disjI2)
show "¬F"
proof (rule notI)
assume 2: "F"
hence 3: "F ∨ ¬F" by (rule disjI1)
show False using 1 3 by (rule notE)
qed
qed
qed
qed

lemma -- "p. 24"
assumes 1: "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "¬p ∨ q"
proof (rule disjE)
{ assume "¬p"
thus "¬p ∨ q" by (rule disjI1) }
next
{ assume 2: "p"
have "q" using 1 2 by (rule mp)
thus "¬p ∨ q" by (rule disjI2) }
qed
qed

end
</source>

@@ Línea 4: / Línea 4: @@
 La página al lado de cada teorema indica la página de las anteriorestransparencias donde se encuentra la demostración.
-<source lang="isar">
+<source lang="isabelle">
 header {* Deducción natural proposicional *}

← Revisión anterior		Revisión del 18:05 2 feb 2011
Línea 1:		Línea 1:
−	En esta teoría se presentan los ejemplos del tema de deducción ~~naturalproposicional~~ siguiendo la presentación de Huth y Ryan en su libro [http://www.cs.bham.ac.uk/research/projects/lics Logic in Computer Science] y, más concretamente, a la forma como se explica en la asignatura de [http://www.cs.us.es/~jalonso/cursos/li-10 Lógica informática] y que puede verse en	+	En esta teoría se presentan los ejemplos del tema de deducción natural proposicional siguiendo la presentación de Huth y Ryan en su libro [http://www.cs.bham.ac.uk/research/projects/lics Logic in Computer Science] y, más concretamente, a la forma como se explica en la asignatura de [http://www.cs.us.es/~jalonso/cursos/li-10 Lógica informática] y que puede verse en
	las [http://www.cs.us.es/~jalonso/cursos/li-10/temas/tema-2.pdf transparencias del tema 2].		las [http://www.cs.us.es/~jalonso/cursos/li-10/temas/tema-2.pdf transparencias del tema 2].

← Revisión anterior		Revisión del 17:56 2 feb 2011
Línea 5:		Línea 5:

	<source lang="isar">		<source lang="isar">
−
−	~~1 header~~
−	~~2 Main~~
−	~~3 maybe~~
−	~~4 Bool~~
−	~~5 IOError~~
−
−
	header {* Deducción natural proposicional *}		header {* Deducción natural proposicional *}

← Revisión anterior		Revisión del 17:45 2 feb 2011
Línea 5:		Línea 5:

	<source lang="isar">		<source lang="isar">
		+
		+	1 header
		+	2 Main
		+	3 maybe
		+	4 Bool
		+	5 IOError
		+
		+
	header {* Deducción natural proposicional *}		header {* Deducción natural proposicional *}

← Revisión anterior	Revisión del 17:29 2 feb 2011
(Sin diferencias)

@@ Línea 1: / Línea 1: @@
 <source lang="isar">
 header {* Deducción natural proposicional *}
@@ Línea 5: / Línea 10: @@
 imports Main
 begin
 section {* Reglas de la conjunción *}

Relación 1a - Historial de revisiones