equal
deleted
inserted
replaced
85 |
85 |
86 text{*Nonstandard extension of a set (defined using a constant |
86 text{*Nonstandard extension of a set (defined using a constant |
87 sequence) as a special case of an internal set*} |
87 sequence) as a special case of an internal set*} |
88 |
88 |
89 lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A" |
89 lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A" |
90 apply (drule expand_fun_eq [THEN iffD2]) |
90 apply (drule ext_iff [THEN iffD2]) |
91 apply (simp add: starset_n_def starset_def star_of_def) |
91 apply (simp add: starset_n_def starset_def star_of_def) |
92 done |
92 done |
93 |
93 |
94 |
94 |
95 (*----------------------------------------------------------------*) |
95 (*----------------------------------------------------------------*) |
100 (* Nonstandard extension of a function (defined using a *) |
100 (* Nonstandard extension of a function (defined using a *) |
101 (* constant sequence) as a special case of an internal function *) |
101 (* constant sequence) as a special case of an internal function *) |
102 (*----------------------------------------------------------------*) |
102 (*----------------------------------------------------------------*) |
103 |
103 |
104 lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f" |
104 lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f" |
105 apply (drule expand_fun_eq [THEN iffD2]) |
105 apply (drule ext_iff [THEN iffD2]) |
106 apply (simp add: starfun_n_def starfun_def star_of_def) |
106 apply (simp add: starfun_n_def starfun_def star_of_def) |
107 done |
107 done |
108 |
108 |
109 |
109 |
110 (* |
110 (* |