isabelle: src/HOL/Arith.thy@3f0ab2c306f7 (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Arith.thy
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6	Arithmetic operators and their definitions
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
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	9	Arith = Nat +
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	11	instance
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12	nat :: {plus, minus, times}
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	consts
1370 7361ac9b024d removed quotes from types in consts and syntax sections clasohm parents: 972 diff changeset	15	pred :: nat => nat
7361ac9b024d removed quotes from types in consts and syntax sections clasohm parents: 972 diff changeset	16	div, mod :: [nat, nat] => nat (infixl 70)
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	17
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	18	defs
2099 c5f004bfcbab Defined pred using nat_case rather than nat_rec. nipkow parents: 1824 diff changeset	19	pred_def "pred(m) == case m of 0 => 0 \| Suc n => n"
1796 c42db9ab8728 Tidied spacing paulson parents: 1475 diff changeset	20
c42db9ab8728 Tidied spacing paulson parents: 1475 diff changeset	21	mod_def "m mod n == wfrec (trancl pred_nat)
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	22	(%f j. if j<n then j else f (j-n)) m"
1796 c42db9ab8728 Tidied spacing paulson parents: 1475 diff changeset	23	div_def "m div n == wfrec (trancl pred_nat)
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	24	(%f j. if j<n then 0 else Suc (f (j-n))) m"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	25
93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	26	primrec "op +" nat
2887 00b8ee790d89 Only layout mods. nipkow parents: 2681 diff changeset	27	"0 + n = n"
00b8ee790d89 Only layout mods. nipkow parents: 2681 diff changeset	28	"Suc m + n = Suc(m + n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	29
93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	30	primrec "op -" nat
2887 00b8ee790d89 Only layout mods. nipkow parents: 2681 diff changeset	31	"m - 0 = m"
00b8ee790d89 Only layout mods. nipkow parents: 2681 diff changeset	32	"m - Suc n = pred(m - n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	33
93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	34	primrec "op *" nat
2887 00b8ee790d89 Only layout mods. nipkow parents: 2681 diff changeset	35	"0 * n = 0"
00b8ee790d89 Only layout mods. nipkow parents: 2681 diff changeset	36	"Suc m * n = n + (m * n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	37
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	38	end

author	paulson
	Wed, 07 May 1997 13:51:22 +0200
changeset 3125	3f0ab2c306f7
parent 2887	00b8ee790d89
child 3235	351565b7321b
permissions	-rw-r--r--