Relación 11 - Historial de revisiones

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

2018-07-16T15:46:12Z

Texto reemplazado: «isar» por «isabelle»

2014-03-10T00:33:45Z

2014-03-09T22:28:24Z

2014-03-09T22:22:42Z

2014-03-09T22:16:14Z

2014-03-09T22:15:31Z

2014-03-09T22:08:37Z

2014-03-09T22:06:05Z

2014-03-09T20:01:29Z

2014-03-09T19:52:46Z

← Revisión anterior		Revisión del 15:46 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R11: Deducción natural de primer orden *}		header {* R11: Deducción natural de primer orden *}

@@ Línea 896: / Línea 896: @@
      qed
    qed
 end
 </source>

@@ Línea 536: / Línea 536: @@
         p(x) para el padre de x
    ------------------------------------------------------------------ *}
--- "julrobrel "
+-- "julrobrel jaisalmen zoiruicha"
 lemma apli2_ej13_lpo:
      assumes "∀ x. ¬R(x) ⟶ R(p(x))"
@@ Línea 643: / Línea 643: @@
 oops
--- "irealetei"
+-- "irealetei jaisalmen zoiruicha"
 lemma ej_10_auto:
    assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x, y)"

@@ Línea 395: / Línea 395: @@
    ------------------------------------------------------------------ *}
--- "pabflomar maresccas4 domlloriv"
+-- "pabflomar maresccas4 domlloriv zoiruicha jaisalmen"
 lemma ej7_pfm:
@@ Línea 462: / Línea 462: @@
         M: El paciente ha mejorado notablemente.
    ------------------------------------------------------------------ *}
--- "pabflomar"
+-- "pabflomar zoiruicha jaisalmen"
 lemma ej8_pfm:

@@ Línea 254: / Línea 254: @@
    ------------------------------------------------------------------ *}
--- "irealetei maresccas4 domlloriv"
+-- "irealetei maresccas4 domlloriv jaisalmen zoiruicha"
 lemma ej_4_auto:
    assumes "∃y. ∀x. P x y"

@@ Línea 303: / Línea 303: @@
 -- "maresccas4, marescpla: Yo lo tengo sin rallita despues del proof y saltandome el ultimo paso, pero es lo mismo."
 lemma ej_5:
    assumes "∀x. P a x x"

@@ Línea 105: / Línea 105: @@
    fixes P Q
    assumes 0: "P a ⟶ (∃x. Q x)"
-   assumes 50: "¬(∃x.( P a ⟶ Q x))"
+   assumes 70: "¬(∃x.( P a ⟶ Q x))"
    shows "∃x. P a ⟶ Q x"
 proof -
@@ Línea 118: / Línea 118: @@
      next
      {assume 10:  "¬(P a)"
-         have 50: "∀x. ¬(P a ⟶ Q x)" using 50 by (rule no_ex)
+         have 50: "∀x. ¬(P a ⟶ Q x)" using 70 by (rule no_ex)
          fix b
          have "¬( P a ⟶ Q b)" using 50 ..

← Revisión anterior	Revisión del 22:06 9 mar 2014
Línea 95:	Línea 95:


	+	-- "jaisalmen zoiruicha"
	+	lemma implicacion: "⟦P ⟶ Q⟧ ⟹ (¬P ∨ Q)"
	+	by auto

	+	lemma implicacion2: "⟦¬( P ⟶ Q)⟧ ⟹ (P ∧ ¬Q)"
	+	by auto
	+
	+	lemma ej01:
	+	fixes P Q
	+	assumes 0: "P a ⟶ (∃x. Q x)"
	+	assumes 50: "¬(∃x.( P a ⟶ Q x))"
	+	shows "∃x. P a ⟶ Q x"
	+	proof -
	+	have 2: "¬(P a) ∨ (∃x. Q x)" using 0 by (rule implicacion)
	+	then show "∃x. P a ⟶ Q x"
	+	proof (rule disjE)
	+	{assume 1: "(∃x. Q x)"
	+	obtain b where "Q b" using 1 ..
	+	then have "P a ⟶ Q b" ..
	+	then show " ∃x. P a ⟶ Q x" by (rule exI)
	+	}
	+	next
	+	{assume 10: "¬(P a)"
	+	have 50: "∀x. ¬(P a ⟶ Q x)" using 50 by (rule no_ex)
	+	fix b
	+	have "¬( P a ⟶ Q b)" using 50 ..
	+	then have " P a ∧ ¬ Q b" by (rule implicacion2)
	+	then have 20: "P a" ..
	+	have "False" using 10 20 ..
	+	then show " ∃x. P a ⟶ Q x" by (rule ccontr)}
	+	qed
	+	qed

@@ Línea 648: / Línea 648: @@
    shows "∀x. E(x) ∧ N(x)  ⟶ ¬Af(j)"
 using assms by auto
 text {* ---------------------------------------------------------------

@@ Línea 775: / Línea 775: @@
    shows "P(a) ⟶ Q(a)"
 using assms by auto
 -- "maresccas4"