isabelle: src/HOL/Arith.thy@7d13a5ace928 (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
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	4	Setup arithmetic proof procedures.
923 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
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	7	theory Arith = Nat
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	8	files "arith_data.ML":
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	9
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	10	setup arith_setup
1796 c42db9ab8728 Tidied spacing paulson parents: 1475 diff changeset	11
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	12	(elimination of `-' on nat)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	13	lemma nat_diff_split:
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	14	"P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	15	by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [RS iffD2])
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	16
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	17	ML {* val nat_diff_split = thm "nat_diff_split" *}
4360 40e5c97e988d pred n -> n-1 nipkow parents: 3366 diff changeset	18
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 8970 diff changeset	19	lemmas [arith_split] = nat_diff_split split_min split_max
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	20
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	21	end

author	wenzelm
	Sun, 30 Jul 2000 13:02:14 +0200
changeset 9473	7d13a5ace928
parent 9436	62bb04ab4b01
child 9618	ff8238561394
permissions	-rw-r--r--