src/ZF/Constructible/Relative.thy
changeset 13350 626b79677dfa
parent 13348 374d05460db4
child 13352 3cd767f8d78b
     1.1 --- a/src/ZF/Constructible/Relative.thy	Thu Jul 11 16:57:14 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Thu Jul 11 17:18:28 2002 +0200
     1.3 @@ -49,6 +49,12 @@
     1.4      "cartprod(M,A,B,z) == 
     1.5  	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
     1.6  
     1.7 +  is_sum :: "[i=>o,i,i,i] => o"
     1.8 +    "is_sum(M,A,B,Z) == 
     1.9 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
    1.10 +       number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
    1.11 +       cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
    1.12 +
    1.13    is_converse :: "[i=>o,i,i] => o"
    1.14      "is_converse(M,r,z) == 
    1.15  	\<forall>x[M]. x \<in> z <-> 
    1.16 @@ -163,6 +169,15 @@
    1.17    number3 :: "[i=>o,i] => o"
    1.18      "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
    1.19  
    1.20 +  is_quasinat :: "[i=>o,i] => o"
    1.21 +    "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
    1.22 +
    1.23 +  is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
    1.24 +    "is_nat_case(M, a, is_b, k, z) == 
    1.25 +       (empty(M,k) --> z=a) &
    1.26 +       (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
    1.27 +       (is_quasinat(M,k) | z=0)"
    1.28 +
    1.29  
    1.30  subsection {*The relativized ZF axioms*}
    1.31  constdefs
    1.32 @@ -607,13 +622,30 @@
    1.33       "n \<in> nat ==> M(n)"
    1.34  by (induct n rule: nat_induct, simp_all)
    1.35  
    1.36 -lemma (in M_triv_axioms) nat_case_closed:
    1.37 +lemma (in M_triv_axioms) nat_case_closed [intro,simp]:
    1.38    "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
    1.39  apply (case_tac "k=0", simp) 
    1.40  apply (case_tac "\<exists>m. k = succ(m)", force)
    1.41  apply (simp add: nat_case_def) 
    1.42  done
    1.43  
    1.44 +lemma (in M_triv_axioms) quasinat_abs [simp]: 
    1.45 +     "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
    1.46 +by (auto simp add: is_quasinat_def quasinat_def)
    1.47 +
    1.48 +lemma (in M_triv_axioms) nat_case_abs [simp]: 
    1.49 +  assumes b_abs: "!!x y. M(x) --> M(y) --> (is_b(x,y) <-> y = b(x))"
    1.50 +  shows
    1.51 +     "[| M(k); M(z) |] ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
    1.52 +apply (case_tac "quasinat(k)") 
    1.53 + prefer 2 
    1.54 + apply (simp add: is_nat_case_def non_nat_case) 
    1.55 + apply (force simp add: quasinat_def) 
    1.56 +apply (simp add: quasinat_def is_nat_case_def)
    1.57 +apply (elim disjE exE) 
    1.58 + apply (simp_all add: b_abs) 
    1.59 +done
    1.60 +
    1.61  lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
    1.62       "M(Inl(a)) <-> M(a)"
    1.63  by (simp add: Inl_def) 
    1.64 @@ -831,6 +863,10 @@
    1.65       "[| M(A); M(B) |] ==> M(A+B)"
    1.66  by (simp add: sum_def)
    1.67  
    1.68 +lemma (in M_axioms) sum_abs [simp]:
    1.69 +     "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
    1.70 +by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
    1.71 +
    1.72  
    1.73  subsubsection {*converse of a relation*}
    1.74  
    1.75 @@ -1096,4 +1132,5 @@
    1.76  apply (simp add: funspace_succ nat_into_M) 
    1.77  done
    1.78  
    1.79 +
    1.80  end