isabelle: src/HOL/Hyperreal/HyperPow.thy@399c8103a98f (annotated)

10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	1	(* Title : HyperPow.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	2	Author : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	3	Copyright : 1998 University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	4	Description : Powers theory for hyperreals
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5	*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	6
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	7	HyperPow = HRealAbs + HyperNat + RealPow +
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	8
10778 2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	9	( First: hypnat is linearly ordered )
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	10
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	11	instance hypnat :: order (hypnat_le_refl,hypnat_le_trans,hypnat_le_anti_sym,
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	12	hypnat_less_le)
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	13	instance hypnat :: linorder (hypnat_le_linear)
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	14
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	15	instance hypnat :: plus_ac0(hypnat_add_commute,hypnat_add_assoc,
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	16	hypnat_add_zero_left)
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	17
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10751 diff changeset	18
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	19	instance hypreal :: {power}
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	20
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	21	consts hpowr :: "[hypreal,nat] => hypreal"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	22	primrec
11713 883d559b0b8c sane numerals (stage 3): provide generic "1" on all number types; wenzelm parents: 10834 diff changeset	23	hpowr_0 "r ^ 0 = (1::hypreal)"
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	24	hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	25
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	26	consts
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	27	"pow" :: [hypreal,hypnat] => hypreal (infixr 80)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	28
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	29	defs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	30
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	31	(* hypernatural powers of hyperreals *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	32	hyperpow_def
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	33	"(R::hypreal) pow (N::hypnat)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	34	== Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
10834 a7897aebbffc * empty log message * nipkow parents: 10797 diff changeset	35	hyprel``{%n::nat. (X n) ^ (Y n)})"
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	36	end

author	kleing
	Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840	399c8103a98f
parent 11713	883d559b0b8c
child 14348	744c868ee0b7
permissions	-rw-r--r--