isabelle: src/HOLCF/Powerdomains.thy@84edf7177d73 (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
40216 366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems huffman parents: 39989 diff changeset	37	lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems huffman parents: 39989 diff changeset	38	lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems huffman parents: 39989 diff changeset	39	lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems huffman parents: 39989 diff changeset	40
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems huffman parents: 39989 diff changeset	41	lemmas [domain_deflation] =
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems huffman parents: 39989 diff changeset	42	deflation_upper_map deflation_lower_map deflation_convex_map
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems huffman parents: 39989 diff changeset	43
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	44	setup {*
40487 1320a0747974 implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data huffman parents: 40218 diff changeset	45	fold Domain_Take_Proofs.add_map_function
1320a0747974 implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data huffman parents: 40218 diff changeset	46	[(@{type_name "upper_pd"}, @{const_name upper_map}, [true]),
1320a0747974 implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data huffman parents: 40218 diff changeset	47	(@{type_name "lower_pd"}, @{const_name lower_map}, [true]),
1320a0747974 implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data huffman parents: 40218 diff changeset	48	(@{type_name "convex_pd"}, @{const_name convex_map}, [true])]
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: diff changeset	49	*}
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	end

author	huffman
	Wed, 17 Nov 2010 11:07:02 -0800
changeset 40619	84edf7177d73
parent 40487	1320a0747974
child 40737	2037021f034f
permissions	-rw-r--r--