# HG changeset patch
# User huffman
# Date 1267826164 28800
# Node ID 1785d387627a3a3d665a92473d3a42868d7efe9d
# Parent  47d68e33ca29d5b5d6cf660924efed42b732f1d3
move take_proofs-related stuff to a new section

diff -r 47d68e33ca29 -r 1785d387627a src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Fri Mar 05 13:55:36 2010 -0800
+++ b/src/HOLCF/Representable.thy	Fri Mar 05 13:56:04 2010 -0800
@@ -12,6 +12,38 @@
   ("Tools/Domain/domain_isomorphism.ML")
 begin
 
+subsection {* Preliminaries: Take proofs *}
+
+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
@@ -180,33 +212,6 @@
   shows "abs\<cdot>(rep\<cdot>x) = x"
 unfolding abs_def rep_def by (simp add: REP [symmetric])
 
-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
-
 
 subsection {* Proving a subtype is representable *}
 
@@ -777,7 +782,6 @@
 
 subsection {* Constructing Domain Isomorphisms *}
 
-use "Tools/Domain/domain_take_proofs.ML"
 use "Tools/Domain/domain_isomorphism.ML"
 
 setup {*