isabelle: src/HOL/Option.thy@74e970389def (annotated)

2019 b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	1	(* Title: Option.thy
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	2	ID: $Id$
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	3	Author: Tobias Nipkow
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	5
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	6	Datatype 'a option
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	7	*)
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	8
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4752 diff changeset	9	Option = Datatype +
4133 0a08c2b9b1ed added the, option_map, and case analysis theorems oheimb parents: 2019 diff changeset	10
2019 b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	11	datatype 'a option = None \| Some 'a
4133 0a08c2b9b1ed added the, option_map, and case analysis theorems oheimb parents: 2019 diff changeset	12
9001 93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	13	consts
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	14	the :: "'a option => 'a"
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	15	o2s :: "'a option => 'a set"
4133 0a08c2b9b1ed added the, option_map, and case analysis theorems oheimb parents: 2019 diff changeset	16
9001 93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	17	primrec
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	18	"the (Some x) = x"
4133 0a08c2b9b1ed added the, option_map, and case analysis theorems oheimb parents: 2019 diff changeset	19
9001 93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	20	primrec
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	21	"o2s None = {}"
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	22	"o2s (Some x) = {x}"
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	23
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary. berghofe parents: 5445 diff changeset	24	constdefs
4133 0a08c2b9b1ed added the, option_map, and case analysis theorems oheimb parents: 2019 diff changeset	25	option_map :: "('a => 'b) => ('a option => 'b option)"
4192 c38ab5af38b5 replaced 8bit characters oheimb parents: 4133 diff changeset	26	"option_map == %f y. case y of None => None \| Some x => Some (f x)"
4133 0a08c2b9b1ed added the, option_map, and case analysis theorems oheimb parents: 2019 diff changeset	27
2019 b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	28	end

author	nipkow
	Mon, 29 Jan 2001 23:02:21 +0100
changeset 10996	74e970389def
parent 9001	93af64f54bf2
permissions	-rw-r--r--