--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Domain_Aux.thy Mon Mar 08 08:12:48 2010 -0800
@@ -0,0 +1,50 @@
+(* Title: HOLCF/Domain_Aux.thy
+ Author: Brian Huffman
+*)
+
+header {* Domain package support *}
+
+theory Domain_Aux
+imports Ssum Sprod Fixrec
+uses
+ ("Tools/Domain/domain_take_proofs.ML")
+begin
+
+subsection {* Proofs about take functions *}
+
+text {*
+ This section contains lemmas that are used in a module that supports
+ the domain isomorphism package; the module contains proofs related
+ to take functions and the finiteness predicate.
+*}
+
+lemma deflation_abs_rep:
+ fixes abs and rep and d
+ assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
+ assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
+ shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
+by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
+
+lemma deflation_chain_min:
+ assumes chain: "chain d"
+ assumes defl: "\<And>n. deflation (d n)"
+ shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
+proof (rule linorder_le_cases)
+ assume "m \<le> n"
+ with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
+ by (rule deflation_below_comp1 [OF defl defl])
+ moreover from `m \<le> n` have "min m n = m" by simp
+ ultimately show ?thesis by simp
+next
+ assume "n \<le> m"
+ with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
+ by (rule deflation_below_comp2 [OF defl defl])
+ moreover from `n \<le> m` have "min m n = n" by simp
+ ultimately show ?thesis by simp
+qed
+
+use "Tools/Domain/domain_take_proofs.ML"
+
+end
--- a/src/HOLCF/IsaMakefile Mon Mar 08 07:37:11 2010 -0800
+++ b/src/HOLCF/IsaMakefile Mon Mar 08 08:12:48 2010 -0800
@@ -39,6 +39,7 @@
Discrete.thy \
Deflation.thy \
Domain.thy \
+ Domain_Aux.thy \
Eventual.thy \
Ffun.thy \
Fixrec.thy \
--- a/src/HOLCF/Representable.thy Mon Mar 08 07:37:11 2010 -0800
+++ b/src/HOLCF/Representable.thy Mon Mar 08 08:12:48 2010 -0800
@@ -5,51 +5,12 @@
header {* Representable Types *}
theory Representable
-imports Algebraic Universal Ssum Sprod One Fixrec
+imports Algebraic Universal Ssum Sprod One Fixrec Domain_Aux
uses
("Tools/repdef.ML")
- ("Tools/Domain/domain_take_proofs.ML")
("Tools/Domain/domain_isomorphism.ML")
begin
-subsection {* Preliminaries: Take proofs *}
-
-text {*
- This section contains lemmas that are used in a module that supports
- the domain isomorphism package; the module contains proofs related
- to take functions and the finiteness predicate.
-*}
-
-lemma deflation_abs_rep:
- fixes abs and rep and d
- assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
- assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
- shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
-by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
-
-lemma deflation_chain_min:
- assumes chain: "chain d"
- assumes defl: "\<And>n. deflation (d n)"
- shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
-proof (rule linorder_le_cases)
- assume "m \<le> n"
- with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
- by (rule deflation_below_comp1 [OF defl defl])
- moreover from `m \<le> n` have "min m n = m" by simp
- ultimately show ?thesis by simp
-next
- assume "n \<le> m"
- with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
- by (rule deflation_below_comp2 [OF defl defl])
- moreover from `n \<le> m` have "min m n = n" by simp
- ultimately show ?thesis by simp
-qed
-
-use "Tools/Domain/domain_take_proofs.ML"
-
-
subsection {* Class of representable types *}
text "Overloaded embedding and projection functions between