author paulson Fri Jul 19 13:28:19 2002 +0200 (2002-07-19) changeset 13396 11219ca224ab parent 13395 4eb948d1eb4e child 13397 6e5f4d911435
A couple of new theorems for Constructible
 src/ZF/List.thy file | annotate | diff | revisions src/ZF/Main.thy file | annotate | diff | revisions src/ZF/Ordinal.thy file | annotate | diff | revisions
```     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"
```