# HG changeset patch
# User huffman
# Date 1271181867 25200
# Node ID 6afa012a8f5cb4812adccf9ff36f15bc8e56dabd
# Parent  64b6374a21a81741bc571d9d2e65752c2e647332
bring HOLCF/ex/Domain_Proofs.thy up to date

diff -r 64b6374a21a8 -r 6afa012a8f5c src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Tue Apr 13 15:30:15 2010 +0200
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Tue Apr 13 11:04:27 2010 -0700
@@ -55,20 +55,23 @@
 definition baz_defl :: "TypeRep \<rightarrow> TypeRep"
 where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
+lemma defl_apply_thms:
+  "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"
+  "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
+  "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
+unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
+
 text {* Unfold rules for each combinator. *}
 
 lemma foo_defl_unfold:
   "foo_defl\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
-unfolding foo_defl_def bar_defl_def baz_defl_def
-by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>REP(tr))"
-unfolding foo_defl_def bar_defl_def baz_defl_def
-by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>REP(tr))"
-unfolding foo_defl_def bar_defl_def baz_defl_def
-by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 text "The automation for the previous steps will be quite similar to
 how the fixrec package works."
@@ -308,6 +311,12 @@
 definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
 where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
 
+lemma map_apply_thms:
+  "foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))"
+  "bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
+  "baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
+unfolding foo_map_def bar_map_def baz_map_def by simp_all
+
 text {* Prove isodefl rules for all map functions simultaneously. *}
 
 lemma isodefl_foo_bar_baz:
@@ -316,8 +325,7 @@
   "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
   isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
   isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
- apply (simp add: foo_map_def bar_map_def baz_map_def)
- apply (simp add: foo_defl_def bar_defl_def baz_defl_def)
+unfolding map_apply_thms defl_apply_thms
  apply (rule parallel_fix_ind)
    apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
   apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
@@ -366,65 +374,100 @@
 
 (********************************************************************)
 
-subsection {* Step 5: Define copy functions, prove reach lemmas *}
-
-text {* Define copy functions just like the old domain package does. *}
-
-definition
-  foo_copy ::
-    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
-       'a foo \<rightarrow> 'a foo"
-where
-  "foo_copy = (\<Lambda> p. foo_abs oo
-        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
-          oo foo_rep)"
+subsection {* Step 5: Define take functions, prove lub-take lemmas *}
 
 definition
-  bar_copy ::
-    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
-       'a bar \<rightarrow> 'a bar"
-where
-  "bar_copy = (\<Lambda> p. bar_abs oo
-        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)"
-
-definition
-  baz_copy ::
-    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
-       'a baz \<rightarrow> 'a baz"
-where
-  "baz_copy = (\<Lambda> p. baz_abs oo
-        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)"
-
-definition
-  foo_bar_baz_copy ::
+  foo_bar_baz_takeF ::
     "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
      ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
 where
-  "foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))"
+  "foo_bar_baz_takeF = (\<Lambda> p.
+    ( foo_abs oo
+        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
+          oo foo_rep
+    , bar_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
+    , baz_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
+    ))"
+
+lemma foo_bar_baz_takeF_beta:
+  "foo_bar_baz_takeF\<cdot>p =
+    ( foo_abs oo
+        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
+          oo foo_rep
+    , bar_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
+    , baz_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
+    )"
+unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp)
+
+definition
+  foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
+where
+  "foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))"
+
+definition
+  bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
+where
+  "bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
 
-lemma fix_foo_bar_baz_copy:
-  "fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)"
-unfolding foo_map_def bar_map_def baz_map_def
-apply (subst beta_cfun, simp)+
-apply (subst pair_collapse)+
-apply (rule cfun_arg_cong)
-unfolding foo_bar_baz_mapF_def split_def
-unfolding foo_bar_baz_copy_def
-unfolding foo_copy_def bar_copy_def baz_copy_def
-apply (subst beta_cfun, simp)+
-apply (rule refl)
+definition
+  baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
+where
+  "baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
+
+lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take"
+unfolding foo_take_def bar_take_def baz_take_def
+by (intro ch2ch_fst ch2ch_snd chain_iterate)+
+
+lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>"
+unfolding foo_take_def bar_take_def baz_take_def
+by (simp only: iterate_0 fst_strict snd_strict)+
+
+lemma take_Suc_thms:
+  "foo_take (Suc n) =
+    foo_abs oo ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(bar_take n))) oo foo_rep"
+  "bar_take (Suc n) =
+    bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep"
+  "baz_take (Suc n) =
+    baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep"
+unfolding foo_take_def bar_take_def baz_take_def
+by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+
+
+lemma lub_take_lemma:
+  "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
+    = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
+apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
+apply (simp only: map_apply_thms pair_collapse)
+apply (simp only: fix_def2)
+apply (rule lub_eq)
+apply (rule nat.induct)
+apply (simp only: iterate_0 Pair_strict take_0_thms)
+apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
+                  foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
 done
 
-lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy fst_conv snd_conv
-unfolding foo_map_ID by (rule ID1)
+lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
+apply (rule trans [OF _ foo_map_ID])
+using lub_take_lemma
+apply (elim Pair_inject)
+apply assumption
+done
 
-lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy fst_conv snd_conv
-unfolding bar_map_ID by (rule ID1)
+lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID"
+apply (rule trans [OF _ bar_map_ID])
+using lub_take_lemma
+apply (elim Pair_inject)
+apply assumption
+done
 
-lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy fst_conv snd_conv
-unfolding baz_map_ID by (rule ID1)
+lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID"
+apply (rule trans [OF _ baz_map_ID])
+using lub_take_lemma
+apply (elim Pair_inject)
+apply assumption
+done
 
 end