Relación 4 - Historial de revisiones

Jalonso en 18:40 14 jul 2018

2018-07-14T18:40:51Z

Jospermon1 en 11:48 1 mar 2018

2018-03-01T11:48:55Z

Macmerflo en 18:42 15 feb 2018

2018-02-15T18:42:44Z

Cesgongut en 19:15 13 feb 2018

2018-02-13T19:15:07Z

Cesgongut en 18:57 13 feb 2018

2018-02-13T18:57:28Z

Jalonso: Desprotegió «Relación 4»

2018-02-10T05:42:02Z

Desprotegió «Relación 4»

Jalonso en 08:11 14 dic 2017

2017-12-14T08:11:17Z

Mostrar los cambios

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

2017-12-14T07:39:37Z

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

Rafcabgon en 05:49 14 dic 2017

2017-12-14T05:49:38Z

Rafferrod en 01:56 14 dic 2017

2017-12-14T01:56:44Z

← Revisión anterior		Revisión del 18:40 14 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R4: Cuantificadores sobre listas *}		chapter {* R4: Cuantificadores sobre listas *}

@@ Línea 20: / Línea 20: @@
 (* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
-    macmerflo rafferrod *)
+    macmerflo rafferrod jospermon1*)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p []     = True"
@@ Línea 42: / Línea 42: @@
 (* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
-    macmerflo rafferrod *)
+    macmerflo rafferrod jospermon1*)
 fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "algunos p []      = False"
@@ Línea 57: / Línea 57: @@
 *}
   (* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
-     macmerflo rafferrod *)
+     macmerflo rafferrod jospermon1*)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
    by (induct xs) auto
@@ Línea 147: / Línea 147: @@
 (* anddonram edupalhid cesgongut luicedval jescudero rafcabgon diwu2
-    macmerflo cesgongut rafferrod *)
+    macmerflo cesgongut rafferrod jospermon1*)
 lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
    by (induct x) auto
@@ Línea 159: / Línea 159: @@
 (* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
-    cesgongut rafferrod *)
+    cesgongut rafferrod jospermon1*)
 lemma todos_append:
    "todos P (x @ y) = (todos P x ∧ todos P y)"
@@ Línea 257: / Línea 257: @@
       (algunos (λx. (x=False)) xs ∧ algunos (λx. x) xs))"
-(* edupalhid diwu2 rafferrod cesgongut *)
+(* edupalhid diwu2 rafferrod cesgongut jospermon1*)
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
    quickcheck
@@ Línea 270: / Línea 270: @@
 (* anddonram edupalhid jescudero luicedval rafcabgon diwu2 macmerflo
-    cesgongut rafferrod *)
+    cesgongut rafferrod jospermon1*)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
    by (induct xs) auto
@@ Línea 282: / Línea 282: @@
 (* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
-    rafferrod *)
+    rafferrod jospermon1*)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 proof(induct xs)
@@ Línea 318: / Línea 318: @@
 (* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
-    cesgongut rafferrod *)
+    cesgongut rafferrod jospermon1*)
 lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
    by (induct xs) auto
@@ Línea 330: / Línea 330: @@
 (* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
-    cesgongut rafferrod *)
+    cesgongut rafferrod jospermon1*)
 lemma algunos_append:
    "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
@@ Línea 430: / Línea 430: @@
 *}
-(* anddonram edupalhid diwu2 jescudero macmerflo rafferrod rafcabgon *)
+(* anddonram edupalhid diwu2 jescudero macmerflo rafferrod rafcabgon jospermon1*)
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
   by (induct xs) auto
@@ Línea 519: / Línea 519: @@
 *}
-(* anddonram edupalhid diwu2 cesgongut rafferrod rafcabgon macmerflo *)
+(* anddonram edupalhid diwu2 cesgongut rafferrod rafcabgon macmerflo jospermon1*)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
   by (induct xs) auto
@@ Línea 556: / Línea 556: @@
 (* anddonram edupalhd luicedval rafcabgon diwu2 jescudero macmerflo
-    cesgongut rafferrod *)
+    cesgongut rafferrod jospermon1*)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x []     = False"
@@ Línea 572: / Línea 572: @@
 (* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
-    cesgongut rafferrod *)
+    cesgongut rafferrod jospermon1*)
 lemma "estaEn x xs=algunos (λy.(y=x)) xs"
    by (induct xs) auto

@@ Línea 519: / Línea 519: @@
 *}
-(* anddonram edupalhid diwu2 cesgongut rafferrod rafcabgon *)
+(* anddonram edupalhid diwu2 cesgongut rafferrod rafcabgon macmerflo *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
   by (induct xs) auto
@@ Línea 530: / Línea 530: @@
 *}
-(*anddonram edupalhid diwu2 rafferrod cesgongut *)
+(*anddonram edupalhid diwu2 rafferrod cesgongut macmerflo *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 proof (induct xs)

@@ Línea 530: / Línea 530: @@
 *}
-(*anddonram edupalhid diwu2 rafferrod*)
+(*anddonram edupalhid diwu2 rafferrod cesgongut *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 proof (induct xs)

@@ Línea 122: / Línea 122: @@
    finally show "todos (λx. P x ∧ Q x) (a#xs) =
                  (todos P (a#xs) ∧ todos Q (a#xs))" by simp
 qed
@@ Línea 169: / Línea 184: @@
    by (induct xs) (simp_all add: todos_append and_comm)
-(* edupalhid diwu2 macmerflo rafferrod*)
+(* edupalhid diwu2 macmerflo rafferrod *)
 lemma "todos P (rev xs) = todos P xs"
 by (induct xs) (auto simp add: todos_append)
 text {*
@@ Línea 211: / Línea 230: @@
 qed
-(* rafferrod *)
+(* rafferrod cesgongut *)
 lemma "todos P (rev xs) = todos P xs"
 proof (induct xs)
@@ Línea 222: / Línea 241: @@
        by (simp add: todos_append)
      also have "... = (todos P xs ∧ todos P [a])" using HI by simp
-     also have "... = (todos P [a] ∧ todos P xs)" by auto
+     also have "... = (todos P [a] ∧ todos P xs)" by auto  (*/ blast *)
      finally show "todos P (rev (a#xs)) = todos P (a#xs)" by simp
    qed
@@ Línea 238: / Línea 257: @@
       (algunos (λx. (x=False)) xs ∧ algunos (λx. x) xs))"
-(* edupalhid diwu2 rafferrod*)
+(* edupalhid diwu2 rafferrod cesgongut *)
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
    quickcheck
@@ Línea 344: / Línea 363: @@
 lemma "algunos P (rev xs) = algunos P xs"
 by (induct xs) (auto simp add: algunos_append)
 text {*
@@ Línea 383: / Línea 406: @@
 qed
-(*rafferrod*)
+(* rafferrod cesgongut *)
 lemma "algunos P (rev xs) = algunos P xs"
 proof (induct xs)
@@ Línea 394: / Línea 417: @@
      by (simp add: algunos_append)
    also have "... = (algunos P xs ∨ algunos P [a])" using HI by simp
-   also have "... = (algunos P [a] ∨ algunos P xs)" by auto
+   also have "... = (algunos P [a] ∨ algunos P xs)" by auto (*/ blast *)
    finally show "algunos P (rev (a#xs)) = algunos P (a#xs)" by simp
 qed
@@ Línea 468: / Línea 491: @@
    finally show "algunos (λx. P x ∨ Q x) (a#xs) =
                  (algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
 qed

← Revisión anterior	Revisión del 05:42 10 feb 2018
(Sin diferencias)

← Revisión anterior	Revisión del 07:39 14 dic 2017
(Sin diferencias)

@@ Línea 387: / Línea 387: @@
 *}
-  (*anddonram edupalhid diwu2 jescudero macmerflo rafferrod*)
+  (*anddonram edupalhid diwu2 jescudero macmerflo rafferrod rafcabgon*)
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
   by (induct xs) auto
@@ Línea 448: / Línea 448: @@
 *}
-  (*anddonram edupalhid diwu2 cesgongut rafferrod*)
+  (*anddonram edupalhid diwu2 cesgongut rafferrod rafcabgon*)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
   by (induct xs) auto

@@ Línea 498: / Línea 498: @@
 *}
-  (*anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo cesgongut*)
+  (*anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo cesgongut rafferrod*)
 lemma "estaEn x xs=algunos (λy.(y=x)) xs"
    by (induct xs) auto
-(*anddonram edupalhid luicedval rafcabgon jescudero macmerflo cesgongut*)
+(*anddonram edupalhid luicedval rafcabgon jescudero macmerflo cesgongut rafferrod*)
 lemma "estaEn x xs=algunos (λy.(y=x)) xs"
 proof (induct xs)