Relación 9 - Historial de revisiones

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

2018-07-16T11:11:21Z

Texto reemplazado: «isar» por «isabelle»

2017-02-01T20:50:44Z

2017-01-31T09:36:24Z

2017-01-30T17:15:15Z

2017-01-26T22:48:25Z

2017-01-26T19:33:44Z

2017-01-26T11:49:43Z

2017-01-26T11:43:06Z

2017-01-26T11:41:50Z

2017-01-26T07:24:28Z

← Revisión anterior		Revisión del 11:11 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R9: Deducción natural LPO en Isabelle/HOL *}		chapter {* R9: Deducción natural LPO en Isabelle/HOL *}

@@ Línea 69: / Línea 69: @@
-(* migtermor ferrenseg juacabsou josgarsan pablucoto marcarmor13*)
+(* migtermor ferrenseg juacabsou josgarsan pablucoto marcarmor13 jeamacpov*)
 lemma ejercicio_1:
    fixes P Q :: "'b ⇒ bool"
@@ Línea 193: / Línea 193: @@
 (* migtermor ferrenseg ivamenjim marcarmor13 serrodcal juacabsou
-    marpoldia1 crigomgom bowma josgarsan rubgonmar pablucoto antsancab1 *)
+    marpoldia1 crigomgom bowma josgarsan rubgonmar pablucoto antsancab1 jeamacpov *)
 lemma ejercicio_2:
    fixes R :: "'b ⇒ 'b ⇒ bool"
@@ Línea 281: / Línea 281: @@
 (* ivamenjim ferrenseg paupeddeg serrodcal juacabsou marpoldia1
-    crigomgom bowma josgarsan rubgonmar pablucoto marcarmor13 antsancab1 pabrodmac *)
+    crigomgom bowma josgarsan rubgonmar pablucoto marcarmor13 antsancab1 pabrodmac jeamacpov *)
 lemma ejercicio_3:
    assumes "(∀x. ∃y. P x y)"
@@ Línea 327: / Línea 327: @@
 qed
-(* migtermor serrodcal crigomgom pablucoto marcarmor13*)
+(* migtermor serrodcal crigomgom pablucoto marcarmor13 jeamacpov*)
 lemma ejercicio_4_2:
    fixes P :: "'b ⇒ 'b ⇒ 'b ⇒ bool"
@@ Línea 420: / Línea 420: @@
 qed
-(* paupeddeg serrodcal juacabsou marpoldia1 crigomgom bowma rubgonmar pablucoto marcarmor13 antsancab1 *)
+(* paupeddeg serrodcal juacabsou marpoldia1 crigomgom bowma rubgonmar pablucoto marcarmor13 antsancab1 jeamacpov *)
 lemma ejercicio_5_3:
    assumes "∀y. Q a y"

@@ Línea 153: / Línea 153: @@
    then show "∃x. P a ⟶ Q x" by simp
 qed
 text {* ---------------------------------------------------------------
@@ Línea 212: / Línea 243: @@
   qed
 qed
 text {* ---------------------------------------------------------------
@@ Línea 219: / Línea 281: @@
 (* ivamenjim ferrenseg paupeddeg serrodcal juacabsou marpoldia1
-    crigomgom bowma josgarsan rubgonmar pablucoto marcarmor13 antsancab1 *)
+    crigomgom bowma josgarsan rubgonmar pablucoto marcarmor13 antsancab1 pabrodmac *)
 lemma ejercicio_3:
    assumes "(∀x. ∃y. P x y)"
@@ Línea 308: / Línea 370: @@
    also have "P (f a) (f a) (f (f a))" using 6 3 by (rule mp)
    then show "∃z. P (f a) z (f (f a))" ..
 qed
@@ Línea 357: / Línea 432: @@
   show "Q a (s a) ∧ Q (s a) (s (s a))"
     using `Q a (s a)` `Q (s a) (s (s a))` by (rule conjI)
 qed
 end
 </source>

@@ Línea 138: / Línea 138: @@
 (* Comentario: Usa simp *)
 text {* ---------------------------------------------------------------
@@ Línea 147: / Línea 162: @@
 (* migtermor ferrenseg ivamenjim marcarmor13 serrodcal juacabsou
-    marpoldia1 crigomgom bowma josgarsan rubgonmar pablucoto*)
+    marpoldia1 crigomgom bowma josgarsan rubgonmar pablucoto antsancab1 *)
 lemma ejercicio_2:
    fixes R :: "'b ⇒ 'b ⇒ bool"
@@ Línea 204: / Línea 219: @@
 (* ivamenjim ferrenseg paupeddeg serrodcal juacabsou marpoldia1
-    crigomgom bowma josgarsan rubgonmar pablucoto marcarmor13*)
+    crigomgom bowma josgarsan rubgonmar pablucoto marcarmor13 antsancab1 *)
 lemma ejercicio_3:
    assumes "(∀x. ∃y. P x y)"
@@ Línea 278: / Línea 293: @@
      using `P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))` `P a (f a) (f a)`
      by (rule mp)
 qed
@@ Línea 315: / Línea 345: @@
 qed
-(* paupeddeg serrodcal juacabsou marpoldia1 crigomgom bowma rubgonmar pablucoto marcarmor13*)
+(* paupeddeg serrodcal juacabsou marpoldia1 crigomgom bowma rubgonmar pablucoto marcarmor13 antsancab1 *)
 lemma ejercicio_5_3:
    assumes "∀y. Q a y"

@@ Línea 69: / Línea 69: @@
-(* migtermor ferrenseg juacabsou josgarsan pablucoto*)
+(* migtermor ferrenseg juacabsou josgarsan pablucoto marcarmor13*)
 lemma ejercicio_1:
    fixes P Q :: "'b ⇒ bool"
@@ Línea 204: / Línea 204: @@
 (* ivamenjim ferrenseg paupeddeg serrodcal juacabsou marpoldia1
-    crigomgom bowma josgarsan rubgonmar pablucoto*)
+    crigomgom bowma josgarsan rubgonmar pablucoto marcarmor13*)
 lemma ejercicio_3:
    assumes "(∀x. ∃y. P x y)"
@@ Línea 250: / Línea 250: @@
 qed
-(* migtermor serrodcal crigomgom pablucoto*)
+(* migtermor serrodcal crigomgom pablucoto marcarmor13*)
 lemma ejercicio_4_2:
    fixes P :: "'b ⇒ 'b ⇒ 'b ⇒ bool"
@@ Línea 315: / Línea 315: @@
 qed
-(* paupeddeg serrodcal juacabsou marpoldia1 crigomgom bowma rubgonmar pablucoto*)
+(* paupeddeg serrodcal juacabsou marpoldia1 crigomgom bowma rubgonmar pablucoto marcarmor13*)
 lemma ejercicio_5_3:
    assumes "∀y. Q a y"

@@ Línea 264: / Línea 264: @@
 qed
-(* paupeddeg juacabsou marpoldia1 bowma rubgonmar *)
+(* paupeddeg juacabsou marpoldia1 bowma rubgonmar josgarsan*)
 lemma ejercicio_4_3:
    fixes P :: "'b ⇒ 'b ⇒ 'b ⇒ bool"

@@ Línea 292: / Línea 292: @@
 : "∀x y. Q x y ⟶ Q (s x) (s y)"
    shows "∃z. Q a z ∧ Q z (s (s a))"
-proof -
+proof
    have 3:"Q a (s a)" using 1 ..
    also have 4:"∀y. Q a y ⟶ Q (s a) (s y)" using 2 ..