isabelle: src/HOLCF/Powerdomains.thy@9f6ed6840e8d (annotated)

35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	1	(* Title: HOLCF/Powerdomains.thy
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	2	Author: Brian Huffman
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	3	*)
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	4
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	5	header {* Powerdomains *}
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	6
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	7	theory Powerdomains
39974 b525988432e9 major reorganization/simplification of HOLCF type classes: huffman parents: 39973 diff changeset	8	imports ConvexPD Domain
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	9	begin
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	10
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	11	lemma isodefl_upper:
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	12	"isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	13	apply (rule isodeflI)
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	14	apply (simp add: cast_upper_defl cast_isodefl)
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	15	apply (simp add: emb_upper_pd_def prj_upper_pd_def)
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	16	apply (simp add: upper_map_map)
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	17	done
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	18
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	19	lemma isodefl_lower:
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	20	"isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	21	apply (rule isodeflI)
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	22	apply (simp add: cast_lower_defl cast_isodefl)
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	23	apply (simp add: emb_lower_pd_def prj_lower_pd_def)
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	24	apply (simp add: lower_map_map)
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	25	done
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	26
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	27	lemma isodefl_convex:
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	28	"isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	29	apply (rule isodeflI)
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	30	apply (simp add: cast_convex_defl cast_isodefl)
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	31	apply (simp add: emb_convex_pd_def prj_convex_pd_def)
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	32	apply (simp add: convex_map_map)
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	33	done
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	34
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	35	subsection {* Domain package setup for powerdomains *}
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	36
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	37	setup {*
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	38	fold Domain_Isomorphism.add_type_constructor
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	39	[(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	40	@{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
35479 dffffe36344a store deflation thms for map functions in theory data huffman parents: 35473 diff changeset	41	@{thm deflation_upper_map}),
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	42
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	43	(@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	44	@{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
35479 dffffe36344a store deflation thms for map functions in theory data huffman parents: 35473 diff changeset	45	@{thm deflation_lower_map}),
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	46
39989 ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	47	(@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a) huffman parents: 39974 diff changeset	48	@{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
35479 dffffe36344a store deflation thms for map functions in theory data huffman parents: 35473 diff changeset	49	@{thm deflation_convex_map})]
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	50	*}
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	51
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	52	end

author	huffman
	Tue, 12 Oct 2010 05:48:15 -0700
changeset 40004	9f6ed6840e8d
parent 39989	ad60d7311f43
child 40216	366309dfaf60
permissions	-rw-r--r--