src/ZF/Univ.thy
changeset 13269 3ba9be497c33
parent 13255 407ad9c3036d
child 13288 9a870391ff66
equal deleted inserted replaced
13268:240509babf00 13269:3ba9be497c33
     9 
     9 
    10 NOTE: univ(A) could be a translation; would simplify many proofs!
    10 NOTE: univ(A) could be a translation; would simplify many proofs!
    11   But Ind_Syntax.univ refers to the constant "Univ.univ"
    11   But Ind_Syntax.univ refers to the constant "Univ.univ"
    12 *)
    12 *)
    13 
    13 
    14 theory Univ = Epsilon + Sum + Finite + mono:
    14 theory Univ = Epsilon + Cardinal:
    15 
    15 
    16 constdefs
    16 constdefs
    17   Vfrom       :: "[i,i]=>i"
    17   Vfrom       :: "[i,i]=>i"
    18     "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
    18     "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
    19 
    19 
    35     "univ(A) == Vfrom(A,nat)"
    35     "univ(A) == Vfrom(A,nat)"
    36 
    36 
    37 
    37 
    38 text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    38 text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    39 lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
    39 lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
    40 apply (subst Vfrom_def [THEN def_transrec])
    40 by (subst Vfrom_def [THEN def_transrec], simp)
    41 apply simp
       
    42 done
       
    43 
    41 
    44 subsubsection{* Monotonicity *}
    42 subsubsection{* Monotonicity *}
    45 
    43 
    46 lemma Vfrom_mono [rule_format]:
    44 lemma Vfrom_mono [rule_format]:
    47      "A<=B ==> \<forall>j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
    45      "A<=B ==> \<forall>j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
   448 apply (blast intro: VsetD [THEN ltD] Ord_trans) 
   446 apply (blast intro: VsetD [THEN ltD] Ord_trans) 
   449 apply (blast intro: i_subset_Vfrom [THEN subsetD]
   447 apply (blast intro: i_subset_Vfrom [THEN subsetD]
   450                     Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
   448                     Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
   451 done
   449 done
   452 
   450 
       
   451 lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
       
   452 apply (erule nat_induct)
       
   453  apply (simp add: Vfrom_0) 
       
   454 apply (simp add: Vset_succ) 
       
   455 done
       
   456 
   453 subsubsection{* Reasoning about sets in terms of their elements' ranks *}
   457 subsubsection{* Reasoning about sets in terms of their elements' ranks *}
   454 
   458 
   455 lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   459 lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   456 apply (rule subsetI)
   460 apply (rule subsetI)
   457 apply (erule rank_lt [THEN VsetI])
   461 apply (erule rank_lt [THEN VsetI])
   481 subsubsection{* Recursion over Vset levels! *}
   485 subsubsection{* Recursion over Vset levels! *}
   482 
   486 
   483 text{*NOT SUITABLE FOR REWRITING: recursive!*}
   487 text{*NOT SUITABLE FOR REWRITING: recursive!*}
   484 lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
   488 lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
   485 apply (unfold Vrec_def)
   489 apply (unfold Vrec_def)
   486 apply (subst transrec)
   490 apply (subst transrec, simp)
   487 apply simp
       
   488 apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
   491 apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
   489 done
   492 done
   490 
   493 
   491 text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
   494 text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
   492 lemma def_Vrec:
   495 lemma def_Vrec: