# HG changeset patch
# User huffman
# Date 1267491496 28800
# Node ID 63f8121c6585366e978de223342da8f79d4be879
# Parent  dd02201d95b675a9ad1220ad4858612c761b0fb1
generate take_take rules

diff -r dd02201d95b6 -r 63f8121c6585 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Mon Mar 01 16:36:25 2010 -0800
+++ b/src/HOLCF/Representable.thy	Mon Mar 01 16:58:16 2010 -0800
@@ -187,6 +187,26 @@
   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>i. deflation (d i)"
+  shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x"
+proof (rule linorder_le_cases)
+  assume "i \<le> j"
+  with chain have "d i \<sqsubseteq> d j" by (rule chain_mono)
+  then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x"
+    by (rule deflation_below_comp1 [OF defl defl])
+  moreover from `i \<le> j` have "min i j = i" by simp
+  ultimately show ?thesis by simp
+next
+  assume "j \<le> i"
+  with chain have "d j \<sqsubseteq> d i" by (rule chain_mono)
+  then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x"
+    by (rule deflation_below_comp2 [OF defl defl])
+  moreover from `j \<le> i` have "min i j = j" by simp
+  ultimately show ?thesis by simp
+qed
+
 
 subsection {* Proving a subtype is representable *}
 
diff -r dd02201d95b6 -r 63f8121c6585 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 01 16:36:25 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 01 16:58:16 2010 -0800
@@ -463,6 +463,18 @@
     val (take_strict_thms, thy) =
       fold_map prove_take_strict (take_consts ~~ dnames) thy;
 
+    (* prove take/take rules *)
+    fun prove_take_take ((chain_take, deflation_take), dname) thy =
+      let
+        val take_take_thm =
+            @{thm deflation_chain_min} OF [chain_take, deflation_take];
+      in
+        add_qualified_thm "take_take" (dname, take_take_thm) thy
+      end;
+    val (take_take_thms, thy) =
+      fold_map prove_take_take
+        (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+
     val result =
       {
         take_consts = take_consts,