Replaced instance declarations for sets by instance declarations for bool.
authorberghofe
Wed, 07 May 2008 10:59:52 +0200
changeset 26837 535290c908ae
parent 26836 0e72627ced0e
child 26838 7f7c6a9e083a
Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.
src/HOLCF/SetPcpo.thy
--- a/src/HOLCF/SetPcpo.thy	Wed May 07 10:59:51 2008 +0200
+++ b/src/HOLCF/SetPcpo.thy	Wed May 07 10:59:52 2008 +0200
@@ -9,38 +9,40 @@
 imports Adm
 begin
 
-instantiation set :: (type) po
+instantiation bool :: po
 begin
 
 definition
-  less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)"
+  less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)"
 
 instance
-by (intro_classes, auto simp add: less_set_def)
+by (intro_classes, auto simp add: less_bool_def)
 
 end
 
-instance set :: (finite) finite_po ..
+lemma less_set_eq: "(op \<sqsubseteq>) = (op \<subseteq>)"
+  by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq)
+
+instance bool :: finite_po ..
 
 lemma Union_is_lub: "A <<| Union A"
-unfolding is_lub_def is_ub_def less_set_def by fast
+unfolding is_lub_def is_ub_def less_set_eq by fast
 
-instance set :: (type) cpo
-by (intro_classes, rule exI, rule Union_is_lub)
+instance bool :: cpo ..
 
 lemma lub_eq_Union: "lub = Union"
 by (rule ext, rule thelubI [OF Union_is_lub])
 
-instance set :: (type) pcpo
+instance bool :: pcpo
 proof
-  have "\<forall>y::'a set. {} \<sqsubseteq> y" unfolding less_set_def by simp
-  thus "\<exists>x::'a set. \<forall>y. x \<sqsubseteq> y" ..
+  have "\<forall>y::bool. False \<sqsubseteq> y" unfolding less_bool_def by simp
+  thus "\<exists>x::bool. \<forall>y. x \<sqsubseteq> y" ..
 qed
 
 lemma UU_eq_empty: "\<bottom> = {}"
-by (rule UU_I [symmetric], simp add: less_set_def)
+by (rule UU_I [symmetric], simp add: less_set_eq)
 
-lemmas set_cpo_simps = less_set_def lub_eq_Union UU_eq_empty
+lemmas set_cpo_simps = less_set_eq lub_eq_Union UU_eq_empty
 
 subsection {* Admissibility of set predicates *}