A couple of new theorems for Constructible
authorpaulson
Fri Jul 19 13:28:19 2002 +0200 (2002-07-19)
changeset 1339611219ca224ab
parent 13395 4eb948d1eb4e
child 13397 6e5f4d911435
A couple of new theorems for Constructible
src/ZF/List.thy
src/ZF/Main.thy
src/ZF/Ordinal.thy
     1.1 --- a/src/ZF/List.thy	Thu Jul 18 15:21:42 2002 +0200
     1.2 +++ b/src/ZF/List.thy	Fri Jul 19 13:28:19 2002 +0200
     1.3 @@ -28,14 +28,15 @@
     1.4  
     1.5  consts
     1.6    length :: "i=>i"
     1.7 -  hd      :: "i=>i"
     1.8 -  tl      :: "i=>i"
     1.9 +  hd     :: "i=>i"
    1.10 +  tl     :: "i=>i"
    1.11  
    1.12  primrec
    1.13    "length([]) = 0"
    1.14    "length(Cons(a,l)) = succ(length(l))"
    1.15  
    1.16  primrec
    1.17 +  "hd([]) = 0"
    1.18    "hd(Cons(a,l)) = a"
    1.19  
    1.20  primrec
     2.1 --- a/src/ZF/Main.thy	Thu Jul 18 15:21:42 2002 +0200
     2.2 +++ b/src/ZF/Main.thy	Fri Jul 19 13:28:19 2002 +0200
     2.3 @@ -40,6 +40,9 @@
     2.4        ==> Ord(F^n (x))"  
     2.5  by (induct n rule: nat_induct, simp_all)
     2.6  
     2.7 +lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
     2.8 +by (induct_tac n, simp_all)
     2.9 +
    2.10  
    2.11  (* belongs to theory IntDiv *)
    2.12  lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
     3.1 --- a/src/ZF/Ordinal.thy	Thu Jul 18 15:21:42 2002 +0200
     3.2 +++ b/src/ZF/Ordinal.thy	Fri Jul 19 13:28:19 2002 +0200
     3.3 @@ -300,11 +300,16 @@
     3.4  apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) 
     3.5  done
     3.6  
     3.7 -(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
     3.8 +text{*The premise @{term "Ord(i)"} does not suffice.*}
     3.9  lemma trans_Memrel: 
    3.10      "Ord(i) ==> trans(Memrel(i))"
    3.11  by (unfold Ord_def Transset_def trans_def, blast)
    3.12  
    3.13 +text{*However, the following premise is strong enough.*}
    3.14 +lemma Transset_trans_Memrel: 
    3.15 +    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
    3.16 +by (unfold Transset_def trans_def, blast)
    3.17 +
    3.18  (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
    3.19  lemma Transset_Memrel_iff: 
    3.20      "Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A"