# HG changeset patch
# User paulson
# Date 1027078099 -7200
# Node ID 11219ca224ab093a448591b8a5925848ecbcea31
# Parent  4eb948d1eb4e0b51a94314846f45beeac60645e4
A couple of new theorems for Constructible

diff -r 4eb948d1eb4e -r 11219ca224ab src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Jul 18 15:21:42 2002 +0200
+++ b/src/ZF/List.thy	Fri Jul 19 13:28:19 2002 +0200
@@ -28,14 +28,15 @@
 
 consts
   length :: "i=>i"
-  hd      :: "i=>i"
-  tl      :: "i=>i"
+  hd     :: "i=>i"
+  tl     :: "i=>i"
 
 primrec
   "length([]) = 0"
   "length(Cons(a,l)) = succ(length(l))"
 
 primrec
+  "hd([]) = 0"
   "hd(Cons(a,l)) = a"
 
 primrec
diff -r 4eb948d1eb4e -r 11219ca224ab src/ZF/Main.thy
--- a/src/ZF/Main.thy	Thu Jul 18 15:21:42 2002 +0200
+++ b/src/ZF/Main.thy	Fri Jul 19 13:28:19 2002 +0200
@@ -40,6 +40,9 @@
       ==> Ord(F^n (x))"  
 by (induct n rule: nat_induct, simp_all)
 
+lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
+by (induct_tac n, simp_all)
+
 
 (* belongs to theory IntDiv *)
 lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
diff -r 4eb948d1eb4e -r 11219ca224ab src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Jul 18 15:21:42 2002 +0200
+++ b/src/ZF/Ordinal.thy	Fri Jul 19 13:28:19 2002 +0200
@@ -300,11 +300,16 @@
 apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) 
 done
 
-(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
+text{*The premise @{term "Ord(i)"} does not suffice.*}
 lemma trans_Memrel: 
     "Ord(i) ==> trans(Memrel(i))"
 by (unfold Ord_def Transset_def trans_def, blast)
 
+text{*However, the following premise is strong enough.*}
+lemma Transset_trans_Memrel: 
+    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
+by (unfold Transset_def trans_def, blast)
+
 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
 lemma Transset_Memrel_iff: 
     "Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A"