isabelle: src/HOL/BNF_Util.thy@8ae6f86a3477 (annotated)

55059 ef2e0fb783c6 tuned comments blanchet parents: 55058 diff changeset	1	(* Title: HOL/BNF_Util.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
49282 c057e1b39f16 renamed "BNF_Library" to "BNF_Util" blanchet parents: 49276 diff changeset	3	Author: Jasmin Blanchette, TU Muenchen
48975 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	Library for bounded natural functors.
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 {* Library for Bounded Natural Functors *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	10
49282 c057e1b39f16 renamed "BNF_Library" to "BNF_Util" blanchet parents: 49276 diff changeset	11	theory BNF_Util
55056 b5c94200d081 renamed '_FP' files to 'BNF_' files blanchet parents: 55054 diff changeset	12	imports BNF_Cardinal_Arithmetic
55054 e1f3714bc508 moved subset of 'HOL-Cardinals' needed for BNF into 'HOL' blanchet parents: 54841 diff changeset	13	Transfer (FIXME: define fun_rel here, reuse in Transfer once this theory is in HOL)
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	14	begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	15
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	16	definition collect where
49463 83ac281bcdc2 provide predicator, define relator blanchet parents: 49314 diff changeset	17	"collect F x = (\<Union>f \<in> F. f x)"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	18
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	19	lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	20	by simp
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 sndI: "x = (y, z) \<Longrightarrow> snd x = z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	23	by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	24
55066 4e5ddf3162ac tuning blanchet parents: 55062 diff changeset	25	lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	26	unfolding bij_def inj_on_def by auto blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	27
49312 c874ff5658dc moved theorems closer to where they are used blanchet parents: 49310 diff changeset	28	(* Operator: *)
c874ff5658dc moved theorems closer to where they are used blanchet parents: 49310 diff changeset	29	definition "Gr A f = {(a, f a) \| a. a \<in> A}"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	30
51893 596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 49510 diff changeset	31	definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead traytel parents: 49510 diff changeset	32
55062 6d3fad6f01c9 made BNF compile after move to HOL blanchet parents: 55059 diff changeset	33	ML_file "Tools/BNF/bnf_util.ML"
6d3fad6f01c9 made BNF compile after move to HOL blanchet parents: 55059 diff changeset	34	ML_file "Tools/BNF/bnf_tactics.ML"
49283 97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy" blanchet parents: 49282 diff changeset	35
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	36	end

author	blanchet
	Mon, 20 Jan 2014 18:24:56 +0100
changeset 55071	8ae6f86a3477
parent 55066	4e5ddf3162ac
child 55084	8ee9aabb2bca
permissions	-rw-r--r--