isabelle: src/HOL/Nat.thy@74919e8f221c (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Nat.thy
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	3	Author: Tobias Nipkow
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	4	Copyright 1997 TU Muenchen
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	6	Nat is a partial order
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	9	Nat = NatDef +
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	11	(*install 'automatic' induction tactic, pretending nat is a datatype
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	12	except for induct_tac and exhaust_tac, everything is dummy*)
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	13
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	14	MLtext {\|
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	15	\|> Dtype.add_datatype_info
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	16	("nat", {case_const = Bound 0, case_rewrites = [],
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	17	constructors = [], induct_tac = nat_ind_tac,
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	18	exhaustion = natE,
4613 67a726003cf8 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW nipkow parents: 4104 diff changeset	19	exhaust_tac = fn v => (res_inst_tac [("n",v)] natE)
67a726003cf8 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW nipkow parents: 4104 diff changeset	20	THEN_ALL_NEW (rotate_tac ~1),
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	21	nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	22	\|}
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	23
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	24
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	25	instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4613 diff changeset	26	instance nat :: linorder (nat_le_linear)
1660 8cb42cd97579 * empty log message * oheimb parents: 1625 diff changeset	27
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	28	consts
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	29	"^" :: ['a::power,nat] => 'a (infixr 80)
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	30
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	31	end

author	paulson
	Wed, 15 Jul 1998 14:19:02 +0200
changeset 5148	74919e8f221c
parent 4640	ac6cf9f18653
child 5188	633ec5f6c155
permissions	-rw-r--r--