src/ZF/Univ.thy
 changeset 13269 3ba9be497c33 parent 13255 407ad9c3036d child 13288 9a870391ff66
equal 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:`