equal
deleted
inserted
replaced
164 lemma InternalNatSets_starsetNat_n [simp]: "( *sNat* X) \<in> InternalNatSets" |
164 lemma InternalNatSets_starsetNat_n [simp]: "( *sNat* X) \<in> InternalNatSets" |
165 by (auto simp add: InternalNatSets_def starsetNat_starsetNat_n_eq) |
165 by (auto simp add: InternalNatSets_def starsetNat_starsetNat_n_eq) |
166 |
166 |
167 lemma InternalNatSets_UNIV_diff: |
167 lemma InternalNatSets_UNIV_diff: |
168 "X \<in> InternalNatSets ==> UNIV - X \<in> InternalNatSets" |
168 "X \<in> InternalNatSets ==> UNIV - X \<in> InternalNatSets" |
|
169 apply (subgoal_tac "UNIV - X = - X") |
169 by (auto intro: InternalNatSets_Compl) |
170 by (auto intro: InternalNatSets_Compl) |
170 |
171 |
171 text{*Nonstandard extension of a set (defined using a constant |
172 text{*Nonstandard extension of a set (defined using a constant |
172 sequence) as a special case of an internal set*} |
173 sequence) as a special case of an internal set*} |
173 lemma starsetNat_n_starsetNat: "\<forall>n. (As n = A) ==> *sNatn* As = *sNat* A" |
174 lemma starsetNat_n_starsetNat: "\<forall>n. (As n = A) ==> *sNatn* As = *sNat* A" |