isabelle: src/HOL/BNF_Examples/TreeFsetI.thy@bdc2c6b40bf2 (annotated)

55075 b3d0a02a756d dissolved BNF session blanchet parents: 55071 diff changeset	1	(* Title: HOL/BNF_Examples/TreeFsetI.thy
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	2	Author: Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	3	Author: Andrei Popescu, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	4	Copyright 2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	5
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	6	Finitely branching possibly infinite trees, with sets of children.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	7	*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	8
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	9	header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	10
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	11	theory TreeFsetI
55129 26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong blanchet parents: 55091 diff changeset	12	imports "~~/src/HOL/Library/FSet"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	13	begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	14
51804 be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names blanchet parents: 51410 diff changeset	15	codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	16
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	17	(* tree map (contrived example): *)
54027 e5853a648b59 use new coinduction method and primcorec in examples traytel parents: 54014 diff changeset	18	primcorec tmap where
e5853a648b59 use new coinduction method and primcorec in examples traytel parents: 54014 diff changeset	19	"lab (tmap f t) = f (lab t)" \|
54014 21dac9a60f0c base the fset bnf on the new FSet theory traytel parents: 53013 diff changeset	20	"sub (tmap f t) = fimage (tmap f) (sub t)"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	21
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	22	lemma "tmap (f o g) x = tmap f (tmap g x)"
55933 12ee2c407dad renamed 'fset_rel' to 'rel_fset' blanchet parents: 55129 diff changeset	23	by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	24
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	25	end

author	haftmann
	Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514	bdc2c6b40bf2
parent 55933	12ee2c407dad
permissions	-rw-r--r--