# HG changeset patch
# User paulson
# Date 893764338 -7200
# Node ID d275fd349f3daffa609cfa407a0b5af18ee588c5
# Parent  b8f2ec739530fb1ea6d3d09aab1cfe43e4039a13
new thms, really demos of the final coalgebra theorem

diff -r b8f2ec739530 -r d275fd349f3d src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Tue Apr 28 13:51:39 1998 +0200
+++ b/src/ZF/Coind/Map.ML	Tue Apr 28 13:52:18 1998 +0200
@@ -6,6 +6,32 @@
 
 open Map;
 
+(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
+
+
+goalw Map.thy [TMap_def]
+     "{0,1} <= {1} Un TMap(I, {0,1})";
+by (Blast_tac 1);
+result();
+
+goalw Map.thy [TMap_def]
+     "{0} Un TMap(I,1) <= {1} Un TMap(I, {0} Un TMap(I,1))";
+by (Blast_tac 1);
+result();
+
+goalw Map.thy [TMap_def]
+     "{0,1} Un TMap(I,2) <= {1} Un TMap(I, {0,1} Un TMap(I,2))";
+by (Blast_tac 1);
+result();
+
+goalw Map.thy [TMap_def]
+     "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) <= \
+\     {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
+(*twice as fast as Blast_tac alone*)
+by (Safe_tac THEN ALLGOALS Blast_tac);
+result();
+
+
 (* ############################################################ *)
 (* Lemmas                                                       *)
 (* ############################################################ *)
@@ -132,7 +158,7 @@
 qed "pmap_domainD";
 
 (* ############################################################ *)
-(* Equalitites                                                  *)
+(* Equalities                                                   *)
 (* ############################################################ *)
 
 (** Domain **)