isabelle: src/HOL/BNF/Examples/TreeFsetI.thy@6bf02eb4ddf7 (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
49508 1e205327f059 adapted examples to renamings blanchet parents: 49463 diff changeset	15	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	16
51804 be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names blanchet parents: 51410 diff changeset	17	codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	18
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	19	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	20	"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	21
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	22	(* tree map (contrived example): *)
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	23	definition tmap where
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	24	"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	25
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	26	lemma tmap_simps[simp]:
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	27	"lab (tmap f t) = f (lab t)"
51410 f0865a641e76 BNF uses fset defined via Lifting/Transfer rather than Quotient traytel parents: 50516 diff changeset	28	"sub (tmap f t) = fmap (tmap f) (sub t)"
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	29	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	30
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	31	lemma "tmap (f o g) x = tmap f (tmap g x)"
49631 9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	32	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	33	apply auto
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	34	apply (unfold fset_rel_def)
9ce0c2cbadb8 modernized example blanchet parents: 49594 diff changeset	35	by auto
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	36
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	37	end

author	traytel
	Thu, 25 Jul 2013 12:25:07 +0200
changeset 52730	6bf02eb4ddf7
parent 51804	be6e703908f4
child 53013	3fbcfa911863
permissions	-rw-r--r--