1.1 --- a/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 06:01:02 2009 -0800
     1.2 +++ b/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 07:09:04 2009 -0800
     1.3 @@ -31,10 +31,10 @@
     1.4    foo_bar_baz_typF ::
     1.5      "TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep"
     1.6  where
     1.7 -  "foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3). 
     1.8 +  "foo_bar_baz_typF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
     1.9      ( ssum_typ\<cdot>REP(one)\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2))
    1.10      , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3)
    1.11 -    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))"
    1.12 +    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1)))))"
    1.13  
    1.14  lemma foo_bar_baz_typF_beta:
    1.15    "foo_bar_baz_typF\<cdot>a\<cdot>t =
    1.16 @@ -42,7 +42,7 @@
    1.17      , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t)))
    1.18      , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))"
    1.19  unfolding foo_bar_baz_typF_def
    1.20 -by (simp add: csplit_def cfst_def csnd_def)
    1.21 +by (simp add: split_def)
    1.22  
    1.23  text {* Individual type combinators are projected from the fixed point. *}
    1.24  
    1.25 @@ -268,11 +268,16 @@
    1.26  
    1.27  definition
    1.28    foo_bar_baz_mapF ::
    1.29 +  "(_ \<rightarrow> _)
    1.30 +     \<rightarrow> (_ foo \<rightarrow> _ foo) \<times> (_ bar \<rightarrow> _ bar) \<times> (_ baz \<rightarrow> _ baz)
    1.31 +     \<rightarrow> (_ foo \<rightarrow> _ foo) \<times> (_ bar \<rightarrow> _ bar) \<times> (_ baz \<rightarrow> _ baz)"
    1.32 +(*
    1.33    "('a \<rightarrow> 'b)
    1.34       \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)
    1.35       \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)"
    1.36 +*)
    1.37  where
    1.38 -  "foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3).
    1.39 +  "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
    1.40      (
    1.41        foo_abs oo
    1.42          ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
    1.43 @@ -281,7 +286,7 @@
    1.44        bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep
    1.45      ,
    1.46        baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep
    1.47 -    ))"
    1.48 +    )))"
    1.49  
    1.50  lemma foo_bar_baz_mapF_beta:
    1.51    "foo_bar_baz_mapF\<cdot>f\<cdot>d =
    1.52 @@ -295,7 +300,7 @@
    1.53        baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep
    1.54      )"
    1.55  unfolding foo_bar_baz_mapF_def
    1.56 -by (simp add: csplit_def cfst_def csnd_def)
    1.57 +by (simp add: split_def)
    1.58  
    1.59  text {* Individual map functions are projected from the fixed point. *}
    1.60  
    1.61 @@ -368,23 +373,64 @@
    1.62  
    1.63  subsection {* Step 5: Define copy functions, prove reach lemmas *}
    1.64  
    1.65 -definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID"
    1.66 -definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))"
    1.67 -definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))"
    1.68 -definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))"
    1.69 +text {* Define copy functions just like the old domain package does. *}
    1.70 +
    1.71 +definition
    1.72 +  foo_copy ::
    1.73 +    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
    1.74 +       'a foo \<rightarrow> 'a foo"
    1.75 +where
    1.76 +  "foo_copy = Abs_CFun (\<lambda>(d1, d2, d3). foo_abs oo
    1.77 +        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d2))
    1.78 +          oo foo_rep)"
    1.79 +
    1.80 +definition
    1.81 +  bar_copy ::
    1.82 +    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
    1.83 +       'a bar \<rightarrow> 'a bar"
    1.84 +where
    1.85 +  "bar_copy = Abs_CFun (\<lambda>(d1, d2, d3). bar_abs oo
    1.86 +        sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d3) oo bar_rep)"
    1.87 +
    1.88 +definition
    1.89 +  baz_copy ::
    1.90 +    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
    1.91 +       'a baz \<rightarrow> 'a baz"
    1.92 +where
    1.93 +  "baz_copy = Abs_CFun (\<lambda>(d1, d2, d3). baz_abs oo
    1.94 +        sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep)"
    1.95 +
    1.96 +definition
    1.97 +  foo_bar_baz_copy ::
    1.98 +    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
    1.99 +     ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
   1.100 +where
   1.101 +  "foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))"
   1.102  
   1.103  lemma fix_foo_bar_baz_copy:
   1.104    "fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)"
   1.105 -unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def
   1.106 -by simp
   1.107 +unfolding foo_map_def bar_map_def baz_map_def
   1.108 +apply (subst beta_cfun, simp)+
   1.109 +apply (subst pair_collapse)+
   1.110 +apply (rule cfun_arg_cong)
   1.111 +unfolding foo_bar_baz_copy_def
   1.112 +unfolding foo_copy_def bar_copy_def baz_copy_def
   1.113 +unfolding foo_bar_baz_mapF_def
   1.114 +unfolding split_def
   1.115 +apply (subst beta_cfun, simp)+
   1.116 +apply (rule refl)
   1.117 +done
   1.118  
   1.119  lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x"
   1.120 -unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID)
   1.121 +unfolding fix_foo_bar_baz_copy fst_conv snd_conv
   1.122 +unfolding foo_map_ID by (rule ID1)
   1.123  
   1.124  lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
   1.125 -unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID)
   1.126 +unfolding fix_foo_bar_baz_copy fst_conv snd_conv
   1.127 +unfolding bar_map_ID by (rule ID1)
   1.128  
   1.129  lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
   1.130 -unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID)
   1.131 +unfolding fix_foo_bar_baz_copy fst_conv snd_conv
   1.132 +unfolding baz_map_ID by (rule ID1)
   1.133  
   1.134  end