src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 41437 5bc117c382ec
parent 41436 480978f80eae
child 42151 4da4fc77664b
equal deleted inserted replaced
41436:480978f80eae 41437:5bc117c382ec
    28 definition
    28 definition
    29   foo_bar_baz_deflF ::
    29   foo_bar_baz_deflF ::
    30     "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
    30     "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
    31 where
    31 where
    32   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
    32   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
    33     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t2)))
    33     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
    34     , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t3))\<cdot>DEFL(tr)))
    34     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
    35     , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"
    35     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
    36 
    36 
    37 lemma foo_bar_baz_deflF_beta:
    37 lemma foo_bar_baz_deflF_beta:
    38   "foo_bar_baz_deflF\<cdot>a\<cdot>t =
    38   "foo_bar_baz_deflF\<cdot>a\<cdot>t =
    39     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(fst (snd t)))))
    39     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
    40     , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
    40     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
    41     , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
    41     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
    42 unfolding foo_bar_baz_deflF_def
    42 unfolding foo_bar_baz_deflF_def
    43 by (simp add: split_def)
    43 by (simp add: split_def)
    44 
    44 
    45 text {* Individual type combinators are projected from the fixed point. *}
    45 text {* Individual type combinators are projected from the fixed point. *}
    46 
    46 
    60 unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
    60 unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
    61 
    61 
    62 text {* Unfold rules for each combinator. *}
    62 text {* Unfold rules for each combinator. *}
    63 
    63 
    64 lemma foo_defl_unfold:
    64 lemma foo_defl_unfold:
    65   "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(bar_defl\<cdot>a))))"
    65   "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
    66 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    66 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    67 
    67 
    68 lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
    68 lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
    69 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    69 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    70 
    70 
    71 lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
    71 lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
    72 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    72 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    73 
    73 
    74 text "The automation for the previous steps will be quite similar to
    74 text "The automation for the previous steps will be quite similar to
    75 how the fixrec package works."
    75 how the fixrec package works."
    76 
    76