21 apply (rule someI_ex) |
21 apply (rule someI_ex) |
22 apply (rule freeultrafilter_Ex) |
22 apply (rule freeultrafilter_Ex) |
23 apply (rule nat_infinite) |
23 apply (rule nat_infinite) |
24 done |
24 done |
25 |
25 |
26 lemmas ultrafilter_FUFNat = |
26 interpretation FUFNat: freeultrafilter [FreeUltrafilterNat] |
27 freeultrafilter_FUFNat [THEN freeultrafilter.ultrafilter] |
27 by (cut_tac [!] freeultrafilter_FUFNat, simp_all add: freeultrafilter_def) |
28 |
|
29 lemmas filter_FUFNat = |
|
30 freeultrafilter_FUFNat [THEN freeultrafilter.filter] |
|
31 |
|
32 lemmas FUFNat_empty [iff] = |
|
33 filter_FUFNat [THEN filter.empty] |
|
34 |
|
35 lemmas FUFNat_UNIV [iff] = |
|
36 filter_FUFNat [THEN filter.UNIV] |
|
37 |
28 |
38 text {* This rule takes the place of the old ultra tactic *} |
29 text {* This rule takes the place of the old ultra tactic *} |
39 |
30 |
40 lemma ultra: |
31 lemma ultra: |
41 "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>" |
32 "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>" |
42 by (simp add: Collect_imp_eq |
33 by (simp add: Collect_imp_eq FUFNat.F.Un_iff FUFNat.F.Compl_iff) |
43 ultrafilter_FUFNat [THEN ultrafilter.Un_iff] |
|
44 ultrafilter_FUFNat [THEN ultrafilter.Compl_iff]) |
|
45 |
34 |
46 |
35 |
47 subsection {* Definition of @{text star} type constructor *} |
36 subsection {* Definition of @{text star} type constructor *} |
48 |
37 |
49 constdefs |
38 constdefs |
103 text {* Transfer introduction rules. *} |
92 text {* Transfer introduction rules. *} |
104 |
93 |
105 lemma transfer_ex [transfer_intro]: |
94 lemma transfer_ex [transfer_intro]: |
106 "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
95 "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
107 \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>" |
96 \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>" |
108 by (simp only: ex_star_eq filter.Collect_ex [OF filter_FUFNat]) |
97 by (simp only: ex_star_eq FUFNat.F.Collect_ex) |
109 |
98 |
110 lemma transfer_all [transfer_intro]: |
99 lemma transfer_all [transfer_intro]: |
111 "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
100 "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
112 \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>" |
101 \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>" |
113 by (simp only: all_star_eq ultrafilter.Collect_all [OF ultrafilter_FUFNat]) |
102 by (simp only: all_star_eq FUFNat.F.Collect_all) |
114 |
103 |
115 lemma transfer_not [transfer_intro]: |
104 lemma transfer_not [transfer_intro]: |
116 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>" |
105 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>" |
117 by (simp only: ultrafilter.Collect_not [OF ultrafilter_FUFNat]) |
106 by (simp only: FUFNat.F.Collect_not) |
118 |
107 |
119 lemma transfer_conj [transfer_intro]: |
108 lemma transfer_conj [transfer_intro]: |
120 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
109 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
121 \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>" |
110 \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>" |
122 by (simp only: filter.Collect_conj [OF filter_FUFNat]) |
111 by (simp only: FUFNat.F.Collect_conj) |
123 |
112 |
124 lemma transfer_disj [transfer_intro]: |
113 lemma transfer_disj [transfer_intro]: |
125 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
114 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
126 \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>" |
115 \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>" |
127 by (simp only: ultrafilter.Collect_disj [OF ultrafilter_FUFNat]) |
116 by (simp only: FUFNat.F.Collect_disj) |
128 |
117 |
129 lemma transfer_imp [transfer_intro]: |
118 lemma transfer_imp [transfer_intro]: |
130 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
119 "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
131 \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>" |
120 \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>" |
132 by (simp only: imp_conv_disj transfer_disj transfer_not) |
121 by (simp only: imp_conv_disj transfer_disj transfer_not) |