isabelle: src/HOL/Sum.thy@cc2340c338f0 (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Sum.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 1992 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	The disjoint sum of two types.
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
1515 4ed79ebab64d Introduced normalize_thm into HOL.ML nipkow parents: 1475 diff changeset	9	Sum = mono + Prod +
923 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	(* type definition *)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1515 diff changeset	13	constdefs
1370 7361ac9b024d removed quotes from types in consts and syntax sections clasohm parents: 1151 diff changeset	14	Inl_Rep :: ['a, 'a, 'b, bool] => bool
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1515 diff changeset	15	"Inl_Rep == (%a. %x y p. x=a & p)"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	16
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1515 diff changeset	17	Inr_Rep :: ['b, 'a, 'b, bool] => bool
9c6ebfab4e05 added constdefs section clasohm parents: 1515 diff changeset	18	"Inr_Rep == (%b. %x y p. y=b & ~p)"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	19
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	20	global
eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	21
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1423 diff changeset	22	typedef (Sum)
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	23	('a, 'b) "+" (infixr 10)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	24	= "{f. (? a. f = Inl_Rep(a::'a)) \| (? b. f = Inr_Rep(b::'b))}"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	25
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	26
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	27	(* abstract constants and syntax *)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	28
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	29	consts
7254 fc7f95f293da Renamed sum_case to basic_sum_case and removed translations for sum_case berghofe parents: 3947 diff changeset	30	Inl :: "'a => 'a + 'b"
fc7f95f293da Renamed sum_case to basic_sum_case and removed translations for sum_case berghofe parents: 3947 diff changeset	31	Inr :: "'b => 'a + 'b"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	32
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	33	(disjoint sum for sets; the operator + is overloaded with wrong type!)
2212 bd705e9de196 plus -> Plus to avoid hiding class plus nipkow parents: 1558 diff changeset	34	Plus :: "['a set, 'b set] => ('a + 'b) set" (infixr 65)
1370 7361ac9b024d removed quotes from types in consts and syntax sections clasohm parents: 1151 diff changeset	35	Part :: ['a set, 'b => 'a] => 'a set
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	36
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	37	local
eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	38
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	39	defs
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	40	Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	41	Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	42
2212 bd705e9de196 plus -> Plus to avoid hiding class plus nipkow parents: 1558 diff changeset	43	sum_def "A Plus B == (Inl``A) Un (Inr``B)"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	44
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	45	(for selecting out the components of a mutually recursive definition)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	46	Part_def "Part A h == A Int {x. ? z. x = h(z)}"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	47
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	48	end

author	paulson
	Mon, 28 Feb 2000 10:49:08 +0100
changeset 8310	cc2340c338f0
parent 7293	959e060f4a2f
child 9311	ab5b24cbaa16
permissions	-rw-r--r--