Relación 1 - Historial de revisiones

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

2018-07-16T07:50:54Z

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

2011-02-14T19:54:29Z

2011-02-14T19:54:06Z

2011-02-13T21:10:26Z

2011-02-13T21:05:04Z

2011-02-11T01:54:58Z

2011-02-11T01:50:42Z

2011-02-11T01:48:41Z

2011-02-11T01:42:17Z

2011-02-11T01:33:59Z

← Revisión anterior		Revisión del 07:50 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* 1ª relación de ejercicios *}		header {* 1ª relación de ejercicios *}

← Revisión anterior		Revisión del 19:54 14 feb 2011
Línea 1:		Línea 1:
−	<source lang="~~haskell~~">	+	<source lang="isar">
	header {* 1ª relación de ejercicios *}		header {* 1ª relación de ejercicios *}

@@ Línea 63: / Línea 63: @@
 by simp
 lemma
@@ Línea 240: / Línea 247: @@
    from 2 and 4 show False by (rule notE)
 qed
 lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
@@ Línea 252: / Línea 258: @@
    qed
 qed
 lemma "((A ⟶ B) ⟶ A) ⟶ A"

← Revisión anterior		Revisión del 21:05 13 feb 2011
Línea 119:		Línea 119:
	lemma version2: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"		lemma version2: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
	by auto		by auto
		+
		+	-- Otra versión. la sentencia "note" no es necesaria.
		+
		+	lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
		+	proof
		+	assume 1: "(A ∨ B) ∨ C"
		+	moreover
		+	{ assume 4: "(A ∨ B)"
		+	moreover
		+	{ assume 5: "A"
		+	from 5 have 6: "A ∨ (B ∨ C)" by (rule disjI1)}
		+	moreover
		+	{ assume 7: "B"
		+	from 7 have 8: "(B ∨ C)" by (rule disjI1)
		+	from 8 have 9: "A ∨ (B ∨ C)" by (rule disjI2)}
		+	ultimately have "A ∨ (B ∨ C)" by (rule disjE)}
		+	moreover
		+	{ assume 2: "C"
		+	from 2 have 3: "(B ∨ C)" by (rule disjI2)
		+	from 3 have "A ∨ (B ∨ C)" by (rule disjI2)}
		+	ultimately show "A ∨ (B ∨ C)" by (rule disjE)
		+	qed

@@ Línea 194: / Línea 194: @@
    from 1 show "A" by (rule notnotD)
 qed
 -- "Está claro que éste sale
@@ Línea 208: / Línea 207: @@
    from 1 show "¬¬A" by (rule contrapos_pn)
 qed
@@ Línea 220: / Línea 218: @@
    from 2 and 4 show False by (rule notE)
 qed
 lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
@@ Línea 231: / Línea 230: @@
    qed
 qed
@@ Línea 251: / Línea 249: @@
    from 8 show "A" by (rule notnotD)
 qed
 -- "Éste sale por auto pero no
@@ Línea 257: / Línea 254: @@
 lemma "((A ⟶ B) ⟶ A) ⟶ A"
 by auto
 lemma "A ∨ ¬A"
@@ Línea 315: / Línea 313: @@
 qed
 end
 </source>

← Revisión anterior		Revisión del 01:42 11 feb 2011
Línea 181:		Línea 181:
	qed		qed

		+
		+	-- "También se puede obtener directamente
		+	por simplificación"
		+	lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
		+	by simp

← Revisión anterior		Revisión del 01:33 11 feb 2011
Línea 156:		Línea 156:
	qed		qed
	qed		qed
		+
		+
		+	-- "Por simplificación es inmediata
		+	su justificación"
		+	lemma "(A ⟶ (B ⟶C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
		+	by auto