src/HOLCF/ex/Domain_Proofs.thy
changeset 40491 6de5839e2fb3
parent 40327 1dfdbd66093a
child 40494 db8a09daba7b
--- a/src/HOLCF/ex/Domain_Proofs.thy	Tue Nov 09 08:41:36 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Tue Nov 09 16:37:13 2010 -0800
@@ -8,8 +8,6 @@
 imports HOLCF
 begin
 
-default_sort bifinite
-
 (*
 
 The definitions and proofs below are for the following recursive
@@ -19,6 +17,9 @@
    and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
    and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
 
+TODO: add another type parameter that is strict,
+to show the different handling of LIFTDEFL vs. DEFL.
+
 *)
 
 (********************************************************************)
@@ -32,13 +33,13 @@
     "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
 where
   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
-    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
     , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
     , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
 
 lemma foo_bar_baz_deflF_beta:
   "foo_bar_baz_deflF\<cdot>a\<cdot>t =
-    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
     , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr))
     , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))"
 unfolding foo_bar_baz_deflF_def
@@ -64,7 +65,7 @@
 text {* Unfold rules for each combinator. *}
 
 lemma foo_defl_unfold:
-  "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)))"
+  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
 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>DEFL(tr))"
@@ -82,13 +83,13 @@
 
 text {* Use @{text pcpodef} with the appropriate type combinator. *}
 
-pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
 
-pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
 
-pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
 
 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
@@ -100,10 +101,19 @@
 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
 
 definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
 definition defl_foo :: "'a foo itself \<Rightarrow> defl"
-where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
+where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
+
+definition
+  "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
 
 instance
 apply (rule typedef_rep_class)
@@ -112,6 +122,9 @@
 apply (rule emb_foo_def)
 apply (rule prj_foo_def)
 apply (rule defl_foo_def)
+apply (rule liftemb_foo_def)
+apply (rule liftprj_foo_def)
+apply (rule liftdefl_foo_def)
 done
 
 end
@@ -123,10 +136,19 @@
 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
 
 definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
 definition defl_bar :: "'a bar itself \<Rightarrow> defl"
-where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
+where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
+
+definition
+  "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
 
 instance
 apply (rule typedef_rep_class)
@@ -135,6 +157,9 @@
 apply (rule emb_bar_def)
 apply (rule prj_bar_def)
 apply (rule defl_bar_def)
+apply (rule liftemb_bar_def)
+apply (rule liftprj_bar_def)
+apply (rule liftdefl_bar_def)
 done
 
 end
@@ -146,10 +171,19 @@
 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
 
 definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
 definition defl_baz :: "'a baz itself \<Rightarrow> defl"
-where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
+where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
+
+definition
+  "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
 
 instance
 apply (rule typedef_rep_class)
@@ -158,42 +192,60 @@
 apply (rule emb_baz_def)
 apply (rule prj_baz_def)
 apply (rule defl_baz_def)
+apply (rule liftemb_baz_def)
+apply (rule liftprj_baz_def)
+apply (rule liftdefl_baz_def)
 done
 
 end
 
 text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
 
-lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
+lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
 apply (rule typedef_DEFL)
 apply (rule defl_foo_def)
 done
 
-lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
+lemma LIFTDEFL_foo [domain_defl_simps]:
+  "LIFTDEFL('a foo) = u_defl\<cdot>DEFL('a foo)"
+apply (rule typedef_LIFTDEFL)
+apply (rule liftdefl_foo_def)
+done
+
+lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
 apply (rule typedef_DEFL)
 apply (rule defl_bar_def)
 done
 
-lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
+lemma LIFTDEFL_bar [domain_defl_simps]:
+  "LIFTDEFL('a bar) = u_defl\<cdot>DEFL('a bar)"
+apply (rule typedef_LIFTDEFL)
+apply (rule liftdefl_bar_def)
+done
+
+lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
 apply (rule typedef_DEFL)
 apply (rule defl_baz_def)
 done
 
+lemma LIFTDEFL_baz [domain_defl_simps]:
+  "LIFTDEFL('a baz) = u_defl\<cdot>DEFL('a baz)"
+apply (rule typedef_LIFTDEFL)
+apply (rule liftdefl_baz_def)
+done
+
 text {* Prove DEFL equations using type combinator unfold lemmas. *}
 
-lemmas DEFL_simps =
-  DEFL_ssum DEFL_sprod DEFL_u DEFL_cfun
-
 lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
+unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
 by (rule foo_defl_unfold)
 
 lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
+unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
 by (rule bar_defl_unfold)
 
 lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps DEFL_convex
+unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
 by (rule baz_defl_unfold)
 
 (********************************************************************)
@@ -254,6 +306,24 @@
   "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
 by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
 
+lemma isodefl_foo_u [domain_isodefl]:
+  "isodefl (d :: 'a foo \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
+using liftemb_foo_def [THEN meta_eq_to_obj_eq]
+using liftprj_foo_def [THEN meta_eq_to_obj_eq]
+by (rule isodefl_u)
+
+lemma isodefl_bar_u [domain_isodefl]:
+  "isodefl (d :: 'a bar \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
+using liftemb_bar_def [THEN meta_eq_to_obj_eq]
+using liftprj_bar_def [THEN meta_eq_to_obj_eq]
+by (rule isodefl_u)
+
+lemma isodefl_baz_u [domain_isodefl]:
+  "isodefl (d :: 'a baz \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
+using liftemb_baz_def [THEN meta_eq_to_obj_eq]
+using liftprj_baz_def [THEN meta_eq_to_obj_eq]
+by (rule isodefl_u)
+
 (********************************************************************)
 
 subsection {* Step 4: Define map functions, prove isodefl property *}
@@ -314,7 +384,7 @@
 text {* Prove isodefl rules for all map functions simultaneously. *}
 
 lemma isodefl_foo_bar_baz:
-  assumes isodefl_d: "isodefl d t"
+  assumes isodefl_d: "isodefl (u_map\<cdot>d) t"
   shows
   "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
   isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
@@ -332,8 +402,8 @@
   isodefl_foo_abs
   isodefl_bar_abs
   isodefl_baz_abs
-  isodefl_ssum isodefl_sprod isodefl_ID_DEFL
-  isodefl_u isodefl_convex isodefl_cfun
+  domain_isodefl
+  isodefl_ID_DEFL isodefl_LIFTDEFL
   isodefl_d
  )
  apply assumption+
@@ -349,21 +419,21 @@
 apply (rule isodefl_DEFL_imp_ID)
 apply (subst DEFL_foo)
 apply (rule isodefl_foo)
-apply (rule isodefl_ID_DEFL)
+apply (rule isodefl_LIFTDEFL)
 done
 
 lemma bar_map_ID: "bar_map\<cdot>ID = ID"
 apply (rule isodefl_DEFL_imp_ID)
 apply (subst DEFL_bar)
 apply (rule isodefl_bar)
-apply (rule isodefl_ID_DEFL)
+apply (rule isodefl_LIFTDEFL)
 done
 
 lemma baz_map_ID: "baz_map\<cdot>ID = ID"
 apply (rule isodefl_DEFL_imp_ID)
 apply (subst DEFL_baz)
 apply (rule isodefl_baz)
-apply (rule isodefl_ID_DEFL)
+apply (rule isodefl_LIFTDEFL)
 done
 
 (********************************************************************)