isabelle: src/HOL/Integ/IntPower.thy@fdf7e9388be7 (annotated)

9509 0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	1	(* Title: IntPower.thy
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	2	ID: $Id$
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	3	Author: Thomas M. Rasmussen
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	4	Copyright 2000 University of Cambridge
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	5
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	6	Integer powers
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	7	*)
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	8
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	9	IntPower = IntDiv +
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	10
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	11	instance
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	12	int :: {power}
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	13
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	14	primrec
11868 56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11701 diff changeset	15	power_0 "p ^ 0 = 1"
9509 0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	16	power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	17
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	18	end

author	berghofe
	Thu, 10 Oct 2002 14:19:17 +0200
changeset 13636	fdf7e9388be7
parent 11868	56db9f3a6b3e
child 14259	79f7d3451b1e
permissions	-rw-r--r--