|
13957
|
1 |
(* Title: NSInduct.thy
|
|
|
2 |
Author: Jacques D. Fleuriot
|
|
|
3 |
Copyright: 2001 University of Edinburgh
|
|
|
4 |
Description: Nonstandard characterization of induction etc.
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
NSInduct = ComplexArith0 +
|
|
|
8 |
|
|
|
9 |
constdefs
|
|
|
10 |
|
|
|
11 |
starPNat :: (nat => bool) => hypnat => bool ("*pNat* _" [80] 80)
|
|
|
12 |
"*pNat* P == (%x. EX X. (X: Rep_hypnat(x) &
|
|
|
13 |
{n. P(X n)} : FreeUltrafilterNat))"
|
|
|
14 |
|
|
|
15 |
|
|
|
16 |
starPNat2 :: (nat => nat => bool) => hypnat =>hypnat => bool ("*pNat2* _" [80] 80)
|
|
|
17 |
"*pNat2* P == (%x y. EX X. EX Y. (X: Rep_hypnat(x) & Y: Rep_hypnat(y) &
|
|
|
18 |
{n. P(X n) (Y n)} : FreeUltrafilterNat))"
|
|
|
19 |
|
|
|
20 |
hSuc :: hypnat => hypnat
|
|
|
21 |
"hSuc n == n + 1"
|
|
|
22 |
|
|
|
23 |
end |