1 (* Title: NSInduct.thy |
1 (* Title: NSInduct.thy |
2 Author: Jacques D. Fleuriot |
2 Author: Jacques D. Fleuriot |
3 Copyright: 2001 University of Edinburgh |
3 Copyright: 2001 University of Edinburgh |
4 Description: Nonstandard characterization of induction etc. |
|
5 *) |
4 *) |
6 |
5 |
7 NSInduct = Complex + |
6 header{*Nonstandard Characterization of Induction*} |
|
7 |
|
8 theory NSInduct = Complex: |
8 |
9 |
9 constdefs |
10 constdefs |
10 |
11 |
11 starPNat :: (nat => bool) => hypnat => bool ("*pNat* _" [80] 80) |
12 starPNat :: "(nat => bool) => hypnat => bool" ("*pNat* _" [80] 80) |
12 "*pNat* P == (%x. EX X. (X: Rep_hypnat(x) & |
13 "*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) & |
13 {n. P(X n)} : FreeUltrafilterNat))" |
14 {n. P(X n)} \<in> FreeUltrafilterNat))" |
14 |
15 |
15 |
16 |
16 starPNat2 :: (nat => nat => bool) => hypnat =>hypnat => bool ("*pNat2* _" [80] 80) |
17 starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool" |
17 "*pNat2* P == (%x y. EX X. EX Y. (X: Rep_hypnat(x) & Y: Rep_hypnat(y) & |
18 ("*pNat2* _" [80] 80) |
18 {n. P(X n) (Y n)} : FreeUltrafilterNat))" |
19 "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) & |
|
20 {n. P(X n) (Y n)} \<in> FreeUltrafilterNat))" |
19 |
21 |
20 hSuc :: hypnat => hypnat |
22 hSuc :: "hypnat => hypnat" |
21 "hSuc n == n + 1" |
23 "hSuc n == n + 1" |
22 |
24 |
|
25 |
|
26 lemma starPNat: |
|
27 "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) = |
|
28 ({n. P (X n)} \<in> FreeUltrafilterNat)" |
|
29 by (auto simp add: starPNat_def, ultra) |
|
30 |
|
31 lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n" |
|
32 by (auto simp add: starPNat hypnat_of_nat_eq) |
|
33 |
|
34 lemma hypnat_induct_obj: |
|
35 "(( *pNat* P) 0 & |
|
36 (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) |
|
37 --> ( *pNat* P)(n)" |
|
38 apply (rule eq_Abs_hypnat [of n]) |
|
39 apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra) |
|
40 apply (erule nat_induct) |
|
41 apply (drule_tac x = "hypnat_of_nat n" in spec) |
|
42 apply (rule ccontr) |
|
43 apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add) |
|
44 done |
|
45 |
|
46 lemma hypnat_induct: |
|
47 "[| ( *pNat* P) 0; |
|
48 !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|] |
|
49 ==> ( *pNat* P)(n)" |
|
50 by (insert hypnat_induct_obj [of P n], auto) |
|
51 |
|
52 lemma starPNat2: |
|
53 "(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n})) |
|
54 (Abs_hypnat(hypnatrel``{%n. Y n}))) = |
|
55 ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)" |
|
56 by (auto simp add: starPNat2_def, ultra) |
|
57 |
|
58 lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)" |
|
59 apply (simp add: starPNat2_def) |
|
60 apply (rule ext) |
|
61 apply (rule ext) |
|
62 apply (rule_tac z = x in eq_Abs_hypnat) |
|
63 apply (rule_tac z = y in eq_Abs_hypnat) |
|
64 apply (auto, ultra) |
|
65 done |
|
66 |
|
67 lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)" |
|
68 by (simp add: starPNat2_eq_iff) |
|
69 |
|
70 lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))" |
|
71 apply auto |
|
72 apply (rule_tac z = h in eq_Abs_hypnat, auto) |
|
73 done |
|
74 |
|
75 lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0" |
|
76 by (simp add: hSuc_def) |
|
77 |
|
78 lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff] |
|
79 |
|
80 lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)" |
|
81 by (simp add: hSuc_def hypnat_one_def) |
|
82 |
|
83 lemma nonempty_nat_set_Least_mem: "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S" |
|
84 by (erule LeastI) |
|
85 |
|
86 lemma nonempty_InternalNatSet_has_least: |
|
87 "[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m" |
|
88 apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp) |
|
89 apply (rule_tac z = x in eq_Abs_hypnat) |
|
90 apply (auto dest!: bspec simp add: hypnat_le) |
|
91 apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto) |
|
92 apply (ultra, force dest: nonempty_nat_set_Least_mem) |
|
93 apply (drule_tac x = x in bspec, auto) |
|
94 apply (ultra, auto intro: Least_le) |
|
95 done |
|
96 |
|
97 text{* Goldblatt page 129 Thm 11.3.2*} |
|
98 lemma internal_induct: |
|
99 "[| X \<in> InternalNatSets; 0 \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |] |
|
100 ==> X = (UNIV:: hypnat set)" |
|
101 apply (rule ccontr) |
|
102 apply (frule InternalNatSets_Compl) |
|
103 apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto) |
|
104 apply (subgoal_tac "1 \<le> n") |
|
105 apply (drule_tac x = "n - 1" in bspec, safe) |
|
106 apply (drule_tac x = "n - 1" in spec) |
|
107 apply (drule_tac [2] c = 1 and a = n in add_right_mono) |
|
108 apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv) |
|
109 done |
|
110 |
|
111 ML |
|
112 {* |
|
113 val starPNat = thm "starPNat"; |
|
114 val starPNat_hypnat_of_nat = thm "starPNat_hypnat_of_nat"; |
|
115 val hypnat_induct = thm "hypnat_induct"; |
|
116 val starPNat2 = thm "starPNat2"; |
|
117 val starPNat2_eq_iff = thm "starPNat2_eq_iff"; |
|
118 val starPNat2_eq_iff2 = thm "starPNat2_eq_iff2"; |
|
119 val hSuc_not_zero = thm "hSuc_not_zero"; |
|
120 val zero_not_hSuc = thms "zero_not_hSuc"; |
|
121 val hSuc_hSuc_eq = thm "hSuc_hSuc_eq"; |
|
122 val nonempty_nat_set_Least_mem = thm "nonempty_nat_set_Least_mem"; |
|
123 val nonempty_InternalNatSet_has_least = thm "nonempty_InternalNatSet_has_least"; |
|
124 val internal_induct = thm "internal_induct"; |
|
125 *} |
|
126 |
23 end |
127 end |