src/HOL/Complex/CStar.thy
changeset 17292 5c613b64bf0a
parent 15234 ec91a90c604e
child 17298 ad73fb6144cf
equal deleted inserted replaced
17291:94f6113fe9ed 17292:5c613b64bf0a
   184 lemma InternalCSets_starsetC_n [simp]: "( *sc* X) \<in> InternalCSets"
   184 lemma InternalCSets_starsetC_n [simp]: "( *sc* X) \<in> InternalCSets"
   185 by (auto simp add: InternalCSets_def starsetC_starsetC_n_eq)
   185 by (auto simp add: InternalCSets_def starsetC_starsetC_n_eq)
   186 
   186 
   187 lemma InternalCSets_UNIV_diff:
   187 lemma InternalCSets_UNIV_diff:
   188     "X \<in> InternalCSets ==> UNIV - X \<in> InternalCSets"
   188     "X \<in> InternalCSets ==> UNIV - X \<in> InternalCSets"
       
   189 apply (subgoal_tac "UNIV - X = - X")
   189 by (auto intro: InternalCSets_Compl)
   190 by (auto intro: InternalCSets_Compl)
   190 
   191 
   191 text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*}
   192 text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*}
   192 
   193 
   193 lemma starsetC_n_starsetC: "\<forall>n. (As n = A) ==> *scn* As = *sc* A"
   194 lemma starsetC_n_starsetC: "\<forall>n. (As n = A) ==> *scn* As = *sc* A"