isabelle: src/HOL/BNF/Examples/TreeFsetI.thy@9ce0c2cbadb8 (annotated)

49509 163914705f8d renamed top-level theory from "Codatatype" to "BNF" blanchet parents: 49508 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
49509 163914705f8d renamed top-level theory from "Codatatype" to "BNF" blanchet parents: 49508 diff changeset	12	imports "../BNF"
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
49092 5eddc9aaebf1 hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI Christian Sternagel parents: 48980 diff changeset	15	hide_const (open) Sublist.sub
49508 1e205327f059 adapted examples to renamings blanchet parents: 49463 diff changeset	16	hide_fact (open) Quotient_Product.prod_rel_def
49092 5eddc9aaebf1 hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI Christian Sternagel parents: 48980 diff changeset	17
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	18	codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	19
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	20	definition pair_fun (infixr "\<odot>" 50) where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	21	"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	22
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	23	(* tree map (contrived example): *)
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	24	definition tmap where
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	25	"tmap f = treeFsetI_unfold (f o lab) sub"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	26
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	27	lemma tmap_simps[simp]:
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	28	"lab (tmap f t) = f (lab t)"
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	29	"sub (tmap f t) = map_fset (tmap f) (sub t)"
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	30	unfolding tmap_def treeFsetI.sel_unfold by simp+
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	31
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	32	lemma "tmap (f o g) x = tmap f (tmap g x)"
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	33	apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	34	apply auto
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	35	apply (unfold fset_rel_def)
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	36	by auto
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	37
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	38	end

author	blanchet
	Fri, 28 Sep 2012 09:12:49 +0200
changeset 49631	9ce0c2cbadb8
parent 49594	55e798614c45
child 50516	ed6b40d15d1c
permissions	-rw-r--r--