isabelle: src/HOL/Real/PNat.thy@c97c3ad15d2e (annotated)

5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	1	(* Title : PNat.thy
7219 4e3f386c2e37 inserted Id: lines paulson parents: 7077 diff changeset	2	ID : $Id$
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	3	Author : Jacques D. Fleuriot
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	4	Copyright : 1998 University of Cambridge
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5	Description : The positive naturals
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	6	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	7
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9	PNat = Arith +
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	11	typedef
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	12	pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	13
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	14	instance
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	15	pnat :: {ord, plus, times}
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	16
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	17	consts
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	18
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	19	pSuc :: pnat => pnat
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	20	"1p" :: pnat ("1p")
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	21
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	22	constdefs
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	23
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	24	pnat_of_nat :: nat => pnat
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	25	"pnat_of_nat n == Abs_pnat(n + 1)"
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	26
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	27	defs
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	28
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	29	pnat_one_def
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	30	"1p == Abs_pnat(1)"
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	31	pnat_Suc_def
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	32	"pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	33
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	34	pnat_add_def
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	35	"x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))"
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	36
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	37	pnat_mult_def
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	38	"x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))"
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	39
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	40	pnat_less_def
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	41	"x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)"
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	42
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5078 diff changeset	43	pnat_le_def
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	44	"x <= (y::pnat) == ~(y < x)"
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	45
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	46	end

author	wenzelm
	Sat, 25 Sep 1999 13:05:38 +0200
changeset 7596	c97c3ad15d2e
parent 7562	8519d5019309
child 8856	435187ffc64e
permissions	-rw-r--r--