# HG changeset patch # User huffman # Date 1292809039 28800 # Node ID 2b7bc8d9fd6e9913ef2c377647fa24e48ea7ee0a # Parent 752d81c2ce2596a128d60dd3dd59fdf203717955 use deflations over type 'udom u' to represent predomains; removed now-unnecessary class liftdomain; diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Domain.thy --- a/src/HOL/HOLCF/Domain.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Domain.thy Sun Dec 19 17:37:19 2010 -0800 @@ -89,12 +89,12 @@ [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \ udom defl"}) , (@{const_name emb}, SOME @{typ "'a::pcpo \ udom"}) , (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) - , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \ udom defl"}) - , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \ udom"}) - , (@{const_name liftprj}, SOME @{typ "udom \ 'a::pcpo u"}) ] + , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \ udom u defl"}) + , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \ udom u"}) + , (@{const_name liftprj}, SOME @{typ "udom u \ 'a::pcpo u"}) ] *} -lemma typedef_liftdomain_class: +lemma typedef_domain_class: fixes Rep :: "'a::pcpo \ udom" fixes Abs :: "udom \ 'a::pcpo" fixes t :: "udom defl" @@ -103,13 +103,11 @@ assumes emb: "emb \ (\ x. Rep x)" assumes prj: "prj \ (\ x. Abs (cast\t\x))" assumes defl: "defl \ (\ a::'a itself. t)" - assumes liftemb: "(liftemb :: 'a u \ udom) \ u_emb oo u_map\emb" - assumes liftprj: "(liftprj :: udom \ 'a u) \ u_map\prj oo u_prj" - assumes liftdefl: "(liftdefl :: 'a itself \ _) \ (\t. u_defl\DEFL('a))" - shows "OFCLASS('a, liftdomain_class)" -using liftemb [THEN meta_eq_to_obj_eq] -using liftprj [THEN meta_eq_to_obj_eq] -proof (rule liftdomain_class_intro) + assumes liftemb: "(liftemb :: 'a u \ udom u) \ u_map\emb" + assumes liftprj: "(liftprj :: udom u \ 'a u) \ u_map\prj" + assumes liftdefl: "(liftdefl :: 'a itself \ _) \ (\t. pdefl\DEFL('a))" + shows "OFCLASS('a, domain_class)" +proof have emb_beta: "\x. emb\x = Rep x" unfolding emb apply (rule beta_cfun) @@ -135,9 +133,7 @@ done show "cast\DEFL('a) = emb oo (prj :: udom \ 'a)" by (rule cfun_eqI, simp add: defl emb_prj) - show "LIFTDEFL('a) = u_defl\DEFL('a)" - unfolding liftdefl .. -qed +qed (simp_all only: liftemb liftprj liftdefl) lemma typedef_DEFL: assumes "defl \ (\a::'a::pcpo itself. t)" @@ -151,19 +147,20 @@ [ (@{const_name defl}, SOME @{typ "'a::domain itself \ udom defl"}) , (@{const_name emb}, SOME @{typ "'a::domain \ udom"}) , (@{const_name prj}, SOME @{typ "udom \ 'a::domain"}) - , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \ udom defl"}) - , (@{const_name liftemb}, SOME @{typ "'a::predomain u \ udom"}) - , (@{const_name liftprj}, SOME @{typ "udom \ 'a::predomain u"}) ] + , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \ udom u defl"}) + , (@{const_name liftemb}, SOME @{typ "'a::predomain u \ udom u"}) + , (@{const_name liftprj}, SOME @{typ "udom u \ 'a::predomain u"}) ] *} use "Tools/domaindef.ML" subsection {* Isomorphic deflations *} -definition - isodefl :: "('a \ 'a) \ udom defl \ bool" -where - "isodefl d t \ cast\t = emb oo d oo prj" +definition isodefl :: "('a \ 'a) \ udom defl \ bool" + where "isodefl d t \ cast\t = emb oo d oo prj" + +definition isodefl' :: "('a::predomain \ 'a) \ udom u defl \ bool" + where "isodefl' d t \ cast\t = liftemb oo u_map\d oo liftprj" lemma isodeflI: "(\x. cast\t\x = emb\(d\(prj\x))) \ isodefl d t" unfolding isodefl_def by (simp add: cfun_eqI) @@ -191,9 +188,8 @@ unfolding isodefl_def by (simp add: cast_DEFL) lemma isodefl_LIFTDEFL: - "isodefl (u_map\(ID :: 'a \ 'a)) LIFTDEFL('a::predomain)" -unfolding u_map_ID DEFL_u [symmetric] -by (rule isodefl_ID_DEFL) + "isodefl' (ID :: 'a \ 'a) LIFTDEFL('a::predomain)" +unfolding isodefl'_def by (simp add: cast_liftdefl u_map_ID) lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \ 'a) DEFL('a) \ d = ID" unfolding isodefl_def @@ -237,6 +233,10 @@ unfolding isodefl_def by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb) +lemma isodefl'_pdefl: "isodefl d t \ isodefl' d (pdefl\t)" +unfolding isodefl_def isodefl'_def +by (simp add: cast_pdefl u_map_oo liftemb_eq liftprj_eq) + lemma isodefl_sfun: "isodefl d1 t1 \ isodefl d2 t2 \ isodefl (sfun_map\d1\d2) (sfun_defl\t1\t2)" @@ -274,12 +274,10 @@ done lemma isodefl_u: - fixes d :: "'a::liftdomain \ 'a" - shows "isodefl (d :: 'a \ 'a) t \ isodefl (u_map\d) (u_defl\t)" + "isodefl' d t \ isodefl (u_map\d) (u_defl\t)" apply (rule isodeflI) -apply (simp add: cast_u_defl cast_isodefl) +apply (simp add: cast_u_defl isodefl'_def) apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq) -apply (simp add: u_map_map) done lemma encode_prod_u_map: @@ -291,11 +289,11 @@ done lemma isodefl_cprod_u: - assumes "isodefl (u_map\d1) t1" and "isodefl (u_map\d2) t2" - shows "isodefl (u_map\(cprod_map\d1\d2)) (sprod_defl\t1\t2)" -using isodefl_sprod [OF assms] unfolding isodefl_def -unfolding emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def -by (simp add: cfcomp1 encode_prod_u_map) + assumes "isodefl' d1 t1" and "isodefl' d2 t2" + shows "isodefl' (cprod_map\d1\d2) (prod_liftdefl\t1\t2)" +using assms unfolding isodefl'_def +unfolding liftemb_prod_def liftprj_prod_def +by (simp add: cast_prod_liftdefl cfcomp1 encode_prod_u_map sprod_map_map) lemma encode_cfun_map: "encode_cfun\(cfun_map\f\g\(decode_cfun\x)) @@ -328,7 +326,7 @@ lemmas [domain_isodefl] = isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod - isodefl_cfun isodefl_cprod isodefl_cprod_u + isodefl_cfun isodefl_cprod isodefl_cprod_u isodefl'_pdefl lemmas [domain_deflation] = deflation_cfun_map deflation_sfun_map deflation_ssum_map diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/Bool_Discrete.thy --- a/src/HOL/HOLCF/Library/Bool_Discrete.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy Sun Dec 19 17:37:19 2010 -0800 @@ -29,23 +29,23 @@ begin definition - "(liftemb :: bool u \ udom) \ liftemb oo u_map\(\ x. Discr x)" + "(liftemb :: bool u \ udom u) \ liftemb oo u_map\(\ x. Discr x)" definition - "(liftprj :: udom \ bool u) \ u_map\(\ y. undiscr y) oo liftprj" + "(liftprj :: udom u \ bool u) \ u_map\(\ y. undiscr y) oo liftprj" definition "liftdefl \ (\(t::bool itself). LIFTDEFL(bool discr))" instance proof - show "ep_pair liftemb (liftprj :: udom \ bool u)" + show "ep_pair liftemb (liftprj :: udom u \ bool u)" unfolding liftemb_bool_def liftprj_bool_def apply (rule ep_pair_comp) apply (rule ep_pair_u_map) apply (simp add: ep_pair.intro) apply (rule predomain_ep) done - show "cast\LIFTDEFL(bool) = liftemb oo (liftprj :: udom \ bool u)" + show "cast\LIFTDEFL(bool) = liftemb oo (liftprj :: udom u \ bool u)" unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_def apply (simp add: cast_liftdefl cfcomp1 u_map_map) apply (simp add: ID_def [symmetric] u_map_ID) diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/Char_Discrete.thy --- a/src/HOL/HOLCF/Library/Char_Discrete.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/Char_Discrete.thy Sun Dec 19 17:37:19 2010 -0800 @@ -29,23 +29,23 @@ begin definition - "(liftemb :: nibble u \ udom) \ liftemb oo u_map\(\ x. Discr x)" + "(liftemb :: nibble u \ udom u) \ liftemb oo u_map\(\ x. Discr x)" definition - "(liftprj :: udom \ nibble u) \ u_map\(\ y. undiscr y) oo liftprj" + "(liftprj :: udom u \ nibble u) \ u_map\(\ y. undiscr y) oo liftprj" definition "liftdefl \ (\(t::nibble itself). LIFTDEFL(nibble discr))" instance proof - show "ep_pair liftemb (liftprj :: udom \ nibble u)" + show "ep_pair liftemb (liftprj :: udom u \ nibble u)" unfolding liftemb_nibble_def liftprj_nibble_def apply (rule ep_pair_comp) apply (rule ep_pair_u_map) apply (simp add: ep_pair.intro) apply (rule predomain_ep) done - show "cast\LIFTDEFL(nibble) = liftemb oo (liftprj :: udom \ nibble u)" + show "cast\LIFTDEFL(nibble) = liftemb oo (liftprj :: udom u \ nibble u)" unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def apply (simp add: cast_liftdefl cfcomp1 u_map_map) apply (simp add: ID_def [symmetric] u_map_ID) @@ -75,23 +75,23 @@ begin definition - "(liftemb :: char u \ udom) \ liftemb oo u_map\(\ x. Discr x)" + "(liftemb :: char u \ udom u) \ liftemb oo u_map\(\ x. Discr x)" definition - "(liftprj :: udom \ char u) \ u_map\(\ y. undiscr y) oo liftprj" + "(liftprj :: udom u \ char u) \ u_map\(\ y. undiscr y) oo liftprj" definition "liftdefl \ (\(t::char itself). LIFTDEFL(char discr))" instance proof - show "ep_pair liftemb (liftprj :: udom \ char u)" + show "ep_pair liftemb (liftprj :: udom u \ char u)" unfolding liftemb_char_def liftprj_char_def apply (rule ep_pair_comp) apply (rule ep_pair_u_map) apply (simp add: ep_pair.intro) apply (rule predomain_ep) done - show "cast\LIFTDEFL(char) = liftemb oo (liftprj :: udom \ char u)" + show "cast\LIFTDEFL(char) = liftemb oo (liftprj :: udom u \ char u)" unfolding liftemb_char_def liftprj_char_def liftdefl_char_def apply (simp add: cast_liftdefl cfcomp1 u_map_map) apply (simp add: ID_def [symmetric] u_map_ID) diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/Defl_Bifinite.thy --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 17:37:19 2010 -0800 @@ -637,7 +637,7 @@ apply (rule someI_ex [OF bifinite]) done -instantiation defl :: (bifinite) liftdomain +instantiation defl :: (bifinite) "domain" begin definition @@ -651,17 +651,15 @@ (\i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))" definition - "(liftemb :: 'a defl u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ 'a defl u) = u_map\prj oo u_prj" + "(liftemb :: 'a defl u \ udom u) = u_map\emb" definition - "liftdefl (t::'a defl itself) = u_defl\DEFL('a defl)" + "(liftprj :: udom u \ 'a defl u) = u_map\prj" -instance -using liftemb_defl_def liftprj_defl_def liftdefl_defl_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::'a defl itself) = pdefl\DEFL('a defl)" + +instance proof show ep: "ep_pair emb (prj :: udom \ 'a defl)" unfolding emb_defl_def prj_defl_def by (rule ep_pair_udom [OF defl_approx]) @@ -682,7 +680,7 @@ apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx] approx_chain.lub_approx [OF defl_approx]) done -qed +qed (fact liftemb_defl_def liftprj_defl_def liftdefl_defl_def)+ end diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/Int_Discrete.thy --- a/src/HOL/HOLCF/Library/Int_Discrete.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/Int_Discrete.thy Sun Dec 19 17:37:19 2010 -0800 @@ -29,23 +29,23 @@ begin definition - "(liftemb :: int u \ udom) \ liftemb oo u_map\(\ x. Discr x)" + "(liftemb :: int u \ udom u) \ liftemb oo u_map\(\ x. Discr x)" definition - "(liftprj :: udom \ int u) \ u_map\(\ y. undiscr y) oo liftprj" + "(liftprj :: udom u \ int u) \ u_map\(\ y. undiscr y) oo liftprj" definition "liftdefl \ (\(t::int itself). LIFTDEFL(int discr))" instance proof - show "ep_pair liftemb (liftprj :: udom \ int u)" + show "ep_pair liftemb (liftprj :: udom u \ int u)" unfolding liftemb_int_def liftprj_int_def apply (rule ep_pair_comp) apply (rule ep_pair_u_map) apply (simp add: ep_pair.intro) apply (rule predomain_ep) done - show "cast\LIFTDEFL(int) = liftemb oo (liftprj :: udom \ int u)" + show "cast\LIFTDEFL(int) = liftemb oo (liftprj :: udom u \ int u)" unfolding liftemb_int_def liftprj_int_def liftdefl_int_def apply (simp add: cast_liftdefl cfcomp1 u_map_map) apply (simp add: ID_def [symmetric] u_map_ID) diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/List_Predomain.thy --- a/src/HOL/HOLCF/Library/List_Predomain.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy Sun Dec 19 17:37:19 2010 -0800 @@ -5,13 +5,61 @@ header {* Predomain class instance for HOL list type *} theory List_Predomain -imports List_Cpo +imports List_Cpo Sum_Cpo begin subsection {* Strict list type *} domain 'a slist = SNil | SCons "'a" "'a slist" +text {* Polymorphic map function for strict lists. *} + +text {* FIXME: The domain package should generate this! *} + +fixrec slist_map' :: "('a \ 'b) \ 'a slist \ 'b slist" + where "slist_map'\f\SNil = SNil" + | "\x \ \; xs \ \\ \ + slist_map'\f\(SCons\x\xs) = SCons\(f\x)\(slist_map'\f\xs)" + +lemma slist_map'_strict [simp]: "slist_map'\f\\ = \" +by fixrec_simp + +lemma slist_map_conv [simp]: "slist_map = slist_map'" +apply (rule cfun_eqI, rule cfun_eqI, rename_tac f xs) +apply (induct_tac xs, simp_all) +apply (subst slist_map_unfold, simp) +apply (subst slist_map_unfold, simp add: SNil_def) +apply (subst slist_map_unfold, simp add: SCons_def) +done + +lemma slist_map'_slist_map': + "f\\ = \ \ slist_map'\f\(slist_map'\g\xs) = slist_map'\(\ x. f\(g\x))\xs" +apply (induct xs, simp, simp) +apply (case_tac "g\a = \", simp, simp) +apply (case_tac "slist_map'\g\xs = \", simp, simp) +done + +lemma slist_map'_oo: + "f\\ = \ \ slist_map'\(f oo g) = slist_map'\f oo slist_map'\g" +by (simp add: cfcomp1 slist_map'_slist_map' eta_cfun) + +lemma slist_map'_ID: "slist_map'\ID = ID" +by (rule cfun_eqI, induct_tac x, simp_all) + +lemma ep_pair_slist_map': + "ep_pair e p \ ep_pair (slist_map'\e) (slist_map'\p)" +apply (rule ep_pair.intro) +apply (subst slist_map'_slist_map') +apply (erule pcpo_ep_pair.p_strict [unfolded pcpo_ep_pair_def]) +apply (simp add: ep_pair.e_inverse ID_def [symmetric] slist_map'_ID) +apply (subst slist_map'_slist_map') +apply (erule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def]) +apply (rule below_eq_trans [OF _ ID1]) +apply (subst slist_map'_ID [symmetric]) +apply (intro monofun_cfun below_refl) +apply (simp add: cfun_below_iff ep_pair.e_p_below) +done + text {* Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic. *} @@ -48,34 +96,52 @@ subsection {* Lists are a predomain *} +definition udefl :: "udom defl \ udom u defl" + where "udefl = defl_fun1 (strictify\up) (fup\ID) ID" + +lemma cast_udefl: + "cast\(udefl\t) = strictify\up oo cast\t oo fup\ID" +unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up) + +definition list_liftdefl :: "udom u defl \ udom u defl" + where "list_liftdefl = (\ a. udefl\(slist_defl\(u_defl\a)))" + +lemma cast_slist_defl: "cast\(slist_defl\a) = emb oo slist_map\(cast\a) oo prj" +using isodefl_slist [where fa="cast\a" and da="a"] +unfolding isodefl_def by simp + +lemma u_emb_bottom: "u_emb\\ = \" +by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u]) + instantiation list :: (predomain) predomain begin definition - "liftemb = emb oo encode_list_u" + "liftemb = (strictify\up oo emb oo slist_map'\u_emb) oo slist_map'\liftemb oo encode_list_u" definition - "liftprj = decode_list_u oo prj" + "liftprj = (decode_list_u oo slist_map'\liftprj) oo (slist_map'\u_prj oo prj) oo fup\ID" definition - "liftdefl (t::('a list) itself) = DEFL(('a\<^sub>\) slist)" + "liftdefl (t::('a list) itself) = list_liftdefl\LIFTDEFL('a)" instance proof - have "ep_pair encode_list_u decode_list_u" - by (rule ep_pair.intro, simp_all) - thus "ep_pair liftemb (liftprj :: udom \ ('a list) u)" + show "ep_pair liftemb (liftprj :: udom u \ ('a list) u)" unfolding liftemb_list_def liftprj_list_def - using ep_pair_emb_prj by (rule ep_pair_comp) - show "cast\LIFTDEFL('a list) = liftemb oo (liftprj :: udom \ ('a list) u)" + by (intro ep_pair_comp ep_pair_slist_map' ep_pair_strictify_up + ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro) + show "cast\LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \ ('a list) u)" unfolding liftemb_list_def liftprj_list_def liftdefl_list_def - by (simp add: cfcomp1 cast_DEFL) + apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl cast_liftdefl) + apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff) + done qed end lemma liftdefl_list [domain_defl_simps]: - "LIFTDEFL('a::predomain list) = slist_defl\LIFTDEFL('a)" -unfolding liftdefl_list_def by (simp add: domain_defl_simps) + "LIFTDEFL('a::predomain list) = list_liftdefl\LIFTDEFL('a)" +by (rule liftdefl_list_def) subsection {* Continuous map operation for lists *} @@ -105,21 +171,21 @@ lemma encode_list_u_map: "encode_list_u\(u_map\(list_map\f)\(decode_list_u\xs)) = slist_map\(u_map\f)\xs" -apply (induct xs) -apply (simp, subst slist_map_unfold, simp) -apply (simp, subst slist_map_unfold, simp add: SNil_def) +apply (induct xs, simp, simp) apply (case_tac a, simp, rename_tac b) apply (case_tac "decode_list_u\xs") -apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp) -by (simp, subst slist_map_unfold, simp add: SCons_def) +apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp, simp) +done lemma isodefl_list_u [domain_isodefl]: fixes d :: "'a::predomain \ 'a" - assumes "isodefl (u_map\d) t" - shows "isodefl (u_map\(list_map\d)) (slist_defl\t)" -using assms [THEN isodefl_slist] unfolding isodefl_def -unfolding emb_u_def prj_u_def liftemb_list_def liftprj_list_def -by (simp add: cfcomp1 encode_list_u_map) + assumes "isodefl' d t" + shows "isodefl' (list_map\d) (list_liftdefl\t)" +using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def +apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl) +apply (simp add: cfcomp1 encode_list_u_map) +apply (simp add: slist_map'_slist_map' u_emb_bottom) +done setup {* Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true]) diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/Nat_Discrete.thy --- a/src/HOL/HOLCF/Library/Nat_Discrete.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy Sun Dec 19 17:37:19 2010 -0800 @@ -29,23 +29,23 @@ begin definition - "(liftemb :: nat u \ udom) \ liftemb oo u_map\(\ x. Discr x)" + "(liftemb :: nat u \ udom u) \ liftemb oo u_map\(\ x. Discr x)" definition - "(liftprj :: udom \ nat u) \ u_map\(\ y. undiscr y) oo liftprj" + "(liftprj :: udom u \ nat u) \ u_map\(\ y. undiscr y) oo liftprj" definition "liftdefl \ (\(t::nat itself). LIFTDEFL(nat discr))" instance proof - show "ep_pair liftemb (liftprj :: udom \ nat u)" + show "ep_pair liftemb (liftprj :: udom u \ nat u)" unfolding liftemb_nat_def liftprj_nat_def apply (rule ep_pair_comp) apply (rule ep_pair_u_map) apply (simp add: ep_pair.intro) apply (rule predomain_ep) done - show "cast\LIFTDEFL(nat) = liftemb oo (liftprj :: udom \ nat u)" + show "cast\LIFTDEFL(nat) = liftemb oo (liftprj :: udom u \ nat u)" unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_def apply (simp add: cast_liftdefl cfcomp1 u_map_map) apply (simp add: ID_def [symmetric] u_map_ID) diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/Option_Cpo.thy --- a/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Dec 19 17:37:19 2010 -0800 @@ -5,7 +5,7 @@ header {* Cpo class instance for HOL option type *} theory Option_Cpo -imports HOLCF +imports HOLCF Sum_Cpo begin subsection {* Ordering on option type *} @@ -209,45 +209,40 @@ subsection {* Option type is a predomain *} definition - "encode_option_u = - (\(up\x). case x of None \ sinl\ONE | Some a \ sinr\(up\a))" + "encode_option = (\ x. case x of None \ Inl () | Some a \ Inr a)" definition - "decode_option_u = sscase\(\ ONE. up\None)\(\(up\a). up\(Some a))" - -lemma decode_encode_option_u [simp]: "decode_option_u\(encode_option_u\x) = x" -unfolding decode_option_u_def encode_option_u_def -by (case_tac x, simp, rename_tac y, case_tac y, simp_all) + "decode_option = (\ x. case x of Inl (u::unit) \ None | Inr a \ Some a)" -lemma encode_decode_option_u [simp]: "encode_option_u\(decode_option_u\x) = x" -unfolding decode_option_u_def encode_option_u_def -apply (case_tac x, simp) -apply (rename_tac a, case_tac a rule: oneE, simp, simp) -apply (rename_tac b, case_tac b, simp, simp) -done +lemma decode_encode_option [simp]: "decode_option\(encode_option\x) = x" +unfolding decode_option_def encode_option_def +by (cases x, simp_all) + +lemma encode_decode_option [simp]: "encode_option\(decode_option\x) = x" +unfolding decode_option_def encode_option_def +by (cases x, simp_all) instantiation option :: (predomain) predomain begin definition - "liftemb = emb oo encode_option_u" + "liftemb = liftemb oo u_map\encode_option" definition - "liftprj = decode_option_u oo prj" + "liftprj = u_map\decode_option oo liftprj" definition - "liftdefl (t::('a option) itself) = DEFL(one \ 'a u)" + "liftdefl (t::('a option) itself) = LIFTDEFL(unit + 'a)" instance proof - show "ep_pair liftemb (liftprj :: udom \ ('a option) u)" + show "ep_pair liftemb (liftprj :: udom u \ ('a option) u)" unfolding liftemb_option_def liftprj_option_def - apply (rule ep_pair_comp) + apply (intro ep_pair_comp ep_pair_u_map predomain_ep) apply (rule ep_pair.intro, simp, simp) - apply (rule ep_pair_emb_prj) done - show "cast\LIFTDEFL('a option) = liftemb oo (liftprj :: udom \ ('a option) u)" + show "cast\LIFTDEFL('a option) = liftemb oo (liftprj :: udom u \ ('a option) u)" unfolding liftemb_option_def liftprj_option_def liftdefl_option_def - by (simp add: cast_DEFL cfcomp1) + by (simp add: cast_liftdefl cfcomp1 u_map_map ID_def [symmetric] u_map_ID) qed end diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Library/Sum_Cpo.thy --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Dec 19 17:37:19 2010 -0800 @@ -260,28 +260,43 @@ apply (rename_tac b, case_tac b, simp, simp) done +lemma ep_pair_strictify_up: + "ep_pair (strictify\up) (fup\ID)" +apply (rule ep_pair.intro) +apply (simp add: strictify_conv_if) +apply (case_tac y, simp, simp add: strictify_conv_if) +done + +definition sum_liftdefl :: "udom u defl \ udom u defl \ udom u defl" + where "sum_liftdefl = defl_fun2 (u_map\emb oo strictify\up) + (fup\ID oo u_map\prj) ssum_map" + instantiation sum :: (predomain, predomain) predomain begin definition - "liftemb = emb oo encode_sum_u" + "liftemb = (u_map\emb oo strictify\up) oo + (ssum_map\liftemb\liftemb oo encode_sum_u)" definition - "liftprj = decode_sum_u oo prj" + "liftprj = (decode_sum_u oo ssum_map\liftprj\liftprj) oo + (fup\ID oo u_map\prj)" definition - "liftdefl (t::('a + 'b) itself) = DEFL('a u \ 'b u)" + "liftdefl (t::('a + 'b) itself) = sum_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" instance proof - show "ep_pair liftemb (liftprj :: udom \ ('a + 'b) u)" + show "ep_pair liftemb (liftprj :: udom u \ ('a + 'b) u)" unfolding liftemb_sum_def liftprj_sum_def - apply (rule ep_pair_comp) - apply (rule ep_pair.intro, simp, simp) - apply (rule ep_pair_emb_prj) - done - show "cast\LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom \ ('a + 'b) u)" + by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u_map ep_pair_emb_prj + ep_pair_strictify_up predomain_ep, simp add: ep_pair.intro) + show "cast\LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \ ('a + 'b) u)" unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def - by (simp add: cast_DEFL cfcomp1) + apply (subst sum_liftdefl_def, subst cast_defl_fun2) + apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj + ep_pair_strictify_up) + apply (erule (1) finite_deflation_ssum_map) + by (simp add: cast_liftdefl cfcomp1 ssum_map_map) qed end diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Powerdomains.thy --- a/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 17:37:19 2010 -0800 @@ -59,7 +59,7 @@ subsection {* Domain class instances *} -instantiation upper_pd :: ("domain") liftdomain +instantiation upper_pd :: ("domain") "domain" begin definition @@ -72,17 +72,15 @@ "defl (t::'a upper_pd itself) = upper_defl\DEFL('a)" definition - "(liftemb :: 'a upper_pd u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ 'a upper_pd u) = u_map\prj oo u_prj" + "(liftemb :: 'a upper_pd u \ udom u) = u_map\emb" definition - "liftdefl (t::'a upper_pd itself) = u_defl\DEFL('a upper_pd)" + "(liftprj :: udom u \ 'a upper_pd u) = u_map\prj" -instance -using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::'a upper_pd itself) = pdefl\DEFL('a upper_pd)" + +instance proof show "ep_pair emb (prj :: udom \ 'a upper_pd)" unfolding emb_upper_pd_def prj_upper_pd_def by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj) @@ -90,11 +88,11 @@ show "cast\DEFL('a upper_pd) = emb oo (prj :: udom \ 'a upper_pd)" unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map) -qed +qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+ end -instantiation lower_pd :: ("domain") liftdomain +instantiation lower_pd :: ("domain") "domain" begin definition @@ -107,17 +105,15 @@ "defl (t::'a lower_pd itself) = lower_defl\DEFL('a)" definition - "(liftemb :: 'a lower_pd u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ 'a lower_pd u) = u_map\prj oo u_prj" + "(liftemb :: 'a lower_pd u \ udom u) = u_map\emb" definition - "liftdefl (t::'a lower_pd itself) = u_defl\DEFL('a lower_pd)" + "(liftprj :: udom u \ 'a lower_pd u) = u_map\prj" -instance -using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::'a lower_pd itself) = pdefl\DEFL('a lower_pd)" + +instance proof show "ep_pair emb (prj :: udom \ 'a lower_pd)" unfolding emb_lower_pd_def prj_lower_pd_def by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj) @@ -125,11 +121,11 @@ show "cast\DEFL('a lower_pd) = emb oo (prj :: udom \ 'a lower_pd)" unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) -qed +qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+ end -instantiation convex_pd :: ("domain") liftdomain +instantiation convex_pd :: ("domain") "domain" begin definition @@ -142,17 +138,15 @@ "defl (t::'a convex_pd itself) = convex_defl\DEFL('a)" definition - "(liftemb :: 'a convex_pd u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ 'a convex_pd u) = u_map\prj oo u_prj" + "(liftemb :: 'a convex_pd u \ udom u) = u_map\emb" definition - "liftdefl (t::'a convex_pd itself) = u_defl\DEFL('a convex_pd)" + "(liftprj :: udom u \ 'a convex_pd u) = u_map\prj" -instance -using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::'a convex_pd itself) = pdefl\DEFL('a convex_pd)" + +instance proof show "ep_pair emb (prj :: udom \ 'a convex_pd)" unfolding emb_convex_pd_def prj_convex_pd_def by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj) @@ -160,7 +154,7 @@ show "cast\DEFL('a convex_pd) = emb oo (prj :: udom \ 'a convex_pd)" unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map) -qed +qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+ end diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Representable.thy --- a/src/HOL/HOLCF/Representable.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Representable.thy Sun Dec 19 17:37:19 2010 -0800 @@ -8,6 +8,8 @@ imports Algebraic Map_Functions Countable begin +default_sort cpo + subsection {* Class of representable domains *} text {* @@ -16,31 +18,67 @@ to being omega-bifinite. A predomain is a cpo that, when lifted, becomes a domain. + Predomains are represented by deflations over a lifted universal + domain type. *} -class predomain = cpo + - fixes liftdefl :: "('a::cpo) itself \ udom defl" - fixes liftemb :: "'a\<^sub>\ \ udom" - fixes liftprj :: "udom \ 'a\<^sub>\" +class predomain_syn = cpo + + fixes liftemb :: "'a\<^sub>\ \ udom\<^sub>\" + fixes liftprj :: "udom\<^sub>\ \ 'a\<^sub>\" + fixes liftdefl :: "'a itself \ udom u defl" + +class predomain = predomain_syn + assumes predomain_ep: "ep_pair liftemb liftprj" - assumes cast_liftdefl: "cast\(liftdefl TYPE('a::cpo)) = liftemb oo liftprj" + assumes cast_liftdefl: "cast\(liftdefl TYPE('a)) = liftemb oo liftprj" syntax "_LIFTDEFL" :: "type \ logic" ("(1LIFTDEFL/(1'(_')))") translations "LIFTDEFL('t)" \ "CONST liftdefl TYPE('t)" -class "domain" = predomain + pcpo + - fixes emb :: "'a::cpo \ udom" - fixes prj :: "udom \ 'a::cpo" +definition pdefl :: "udom defl \ udom u defl" + where "pdefl = defl_fun1 ID ID u_map" + +lemma cast_pdefl: "cast\(pdefl\t) = u_map\(cast\t)" +by (simp add: pdefl_def cast_defl_fun1 ep_pair_def finite_deflation_u_map) + +class "domain" = predomain_syn + pcpo + + fixes emb :: "'a \ udom" + fixes prj :: "udom \ 'a" fixes defl :: "'a itself \ udom defl" assumes ep_pair_emb_prj: "ep_pair emb prj" assumes cast_DEFL: "cast\(defl TYPE('a)) = emb oo prj" + assumes liftemb_eq: "liftemb = u_map\emb" + assumes liftprj_eq: "liftprj = u_map\prj" + assumes liftdefl_eq: "liftdefl TYPE('a) = pdefl\(defl TYPE('a))" syntax "_DEFL" :: "type \ logic" ("(1DEFL/(1'(_')))") translations "DEFL('t)" \ "CONST defl TYPE('t)" +instance "domain" \ predomain +proof + show "ep_pair liftemb (liftprj::udom\<^sub>\ \ 'a\<^sub>\)" + unfolding liftemb_eq liftprj_eq + by (intro ep_pair_u_map ep_pair_emb_prj) + show "cast\LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\ \ 'a\<^sub>\)" + unfolding liftemb_eq liftprj_eq liftdefl_eq + by (simp add: cast_pdefl cast_DEFL u_map_oo) +qed + +text {* + Constants @{const liftemb} and @{const liftprj} imply class predomain. +*} + +setup {* + fold Sign.add_const_constraint + [(@{const_name liftemb}, SOME @{typ "'a::predomain u \ udom u"}), + (@{const_name liftprj}, SOME @{typ "udom u \ 'a::predomain u"}), + (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \ udom u defl"})] +*} + +interpretation predomain: pcpo_ep_pair liftemb liftprj + unfolding pcpo_ep_pair_def by (rule predomain_ep) + interpretation "domain": pcpo_ep_pair emb prj - unfolding pcpo_ep_pair_def - by (rule ep_pair_emb_prj) + unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj) lemmas emb_inverse = domain.e_inverse lemmas emb_prj_below = domain.e_p_below @@ -51,7 +89,7 @@ subsection {* Domains are bifinite *} lemma approx_chain_ep_cast: - assumes ep: "ep_pair (e::'a::pcpo \ udom) (p::udom \ 'a)" + assumes ep: "ep_pair (e::'a::pcpo \ 'b::bifinite) (p::'b \ 'a)" assumes cast_t: "cast\t = e oo p" shows "\(a::nat \ 'a::pcpo \ 'a). approx_chain a" proof - @@ -125,8 +163,8 @@ subsection {* Type combinators *} -definition u_defl :: "udom defl \ udom defl" - where "u_defl = defl_fun1 u_emb u_prj u_map" +definition u_defl :: "udom u defl \ udom defl" + where "u_defl = defl_fun1 u_emb u_prj ID" definition prod_defl :: "udom defl \ udom defl \ udom defl" where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map" @@ -141,9 +179,8 @@ where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map" lemma cast_u_defl: - "cast\(u_defl\A) = u_emb oo u_map\(cast\A) oo u_prj" -using ep_pair_u finite_deflation_u_map -unfolding u_defl_def by (rule cast_defl_fun1) + "cast\(u_defl\A) = u_emb oo cast\A oo u_prj" +unfolding u_defl_def by (simp add: cast_defl_fun1 ep_pair_u) lemma cast_prod_defl: "cast\(prod_defl\A\B) = @@ -169,66 +206,11 @@ using ep_pair_sfun finite_deflation_sfun_map unfolding sfun_defl_def by (rule cast_defl_fun2) -subsection {* Lemma for proving domain instances *} - -text {* - A class of domains where @{const liftemb}, @{const liftprj}, - and @{const liftdefl} are all defined in the standard way. -*} - -class liftdomain = "domain" + - assumes liftemb_eq: "liftemb = u_emb oo u_map\emb" - assumes liftprj_eq: "liftprj = u_map\prj oo u_prj" - assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\DEFL('a)" - -text {* Temporarily relax type constraints. *} - -setup {* - fold Sign.add_const_constraint - [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \ udom defl"}) - , (@{const_name emb}, SOME @{typ "'a::pcpo \ udom"}) - , (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) - , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \ udom defl"}) - , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \ udom"}) - , (@{const_name liftprj}, SOME @{typ "udom \ 'a::pcpo u"}) ] -*} - -default_sort pcpo - -lemma liftdomain_class_intro: - assumes liftemb: "(liftemb :: 'a u \ udom) = u_emb oo u_map\emb" - assumes liftprj: "(liftprj :: udom \ 'a u) = u_map\prj oo u_prj" - assumes liftdefl: "liftdefl TYPE('a) = u_defl\DEFL('a)" - assumes ep_pair: "ep_pair emb (prj :: udom \ 'a)" - assumes cast_defl: "cast\DEFL('a) = emb oo (prj :: udom \ 'a)" - shows "OFCLASS('a, liftdomain_class)" -proof - show "ep_pair liftemb (liftprj :: udom \ 'a u)" - unfolding liftemb liftprj - by (intro ep_pair_comp ep_pair_u_map ep_pair ep_pair_u) - show "cast\LIFTDEFL('a) = liftemb oo (liftprj :: udom \ 'a u)" - unfolding liftemb liftprj liftdefl - by (simp add: cfcomp1 cast_u_defl cast_defl u_map_map) -next -qed fact+ - -text {* Restore original type constraints. *} - -setup {* - fold Sign.add_const_constraint - [ (@{const_name defl}, SOME @{typ "'a::domain itself \ udom defl"}) - , (@{const_name emb}, SOME @{typ "'a::domain \ udom"}) - , (@{const_name prj}, SOME @{typ "udom \ 'a::domain"}) - , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \ udom defl"}) - , (@{const_name liftemb}, SOME @{typ "'a::predomain u \ udom"}) - , (@{const_name liftprj}, SOME @{typ "udom \ 'a::predomain u"}) ] -*} - subsection {* Class instance proofs *} subsubsection {* Universal domain *} -instantiation udom :: liftdomain +instantiation udom :: "domain" begin definition [simp]: @@ -241,17 +223,15 @@ "defl (t::udom itself) = (\i. defl_principal (Abs_fin_defl (udom_approx i)))" definition - "(liftemb :: udom u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ udom u) = u_map\prj oo u_prj" + "(liftemb :: udom u \ udom u) = u_map\emb" definition - "liftdefl (t::udom itself) = u_defl\DEFL(udom)" + "(liftprj :: udom u \ udom u) = u_map\prj" -instance -using liftemb_udom_def liftprj_udom_def liftdefl_udom_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::udom itself) = pdefl\DEFL(udom)" + +instance proof show "ep_pair emb (prj :: udom \ udom)" by (simp add: ep_pair.intro) show "cast\DEFL(udom) = emb oo (prj :: udom \ udom)" @@ -266,52 +246,50 @@ apply (subst cast_defl_principal) apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) done -qed +qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+ end subsubsection {* Lifted cpo *} -instantiation u :: (predomain) liftdomain +instantiation u :: (predomain) "domain" begin definition - "emb = liftemb" + "emb = u_emb oo liftemb" definition - "prj = liftprj" + "prj = liftprj oo u_prj" definition - "defl (t::'a u itself) = LIFTDEFL('a)" + "defl (t::'a u itself) = u_defl\LIFTDEFL('a)" definition - "(liftemb :: 'a u u \ udom) = u_emb oo u_map\emb" + "(liftemb :: 'a u u \ udom u) = u_map\emb" definition - "(liftprj :: udom \ 'a u u) = u_map\prj oo u_prj" + "(liftprj :: udom u \ 'a u u) = u_map\prj" definition - "liftdefl (t::'a u itself) = u_defl\DEFL('a u)" + "liftdefl (t::'a u itself) = pdefl\DEFL('a u)" -instance -using liftemb_u_def liftprj_u_def liftdefl_u_def -proof (rule liftdomain_class_intro) +instance proof show "ep_pair emb (prj :: udom \ 'a u)" unfolding emb_u_def prj_u_def - by (rule predomain_ep) + by (intro ep_pair_comp ep_pair_u predomain_ep) show "cast\DEFL('a u) = emb oo (prj :: udom \ 'a u)" unfolding emb_u_def prj_u_def defl_u_def - by (rule cast_liftdefl) -qed + by (simp add: cast_u_defl cast_liftdefl assoc_oo) +qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+ end -lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)" +lemma DEFL_u: "DEFL('a::predomain u) = u_defl\LIFTDEFL('a)" by (rule defl_u_def) subsubsection {* Strict function space *} -instantiation sfun :: ("domain", "domain") liftdomain +instantiation sfun :: ("domain", "domain") "domain" begin definition @@ -324,24 +302,22 @@ "defl (t::('a \! 'b) itself) = sfun_defl\DEFL('a)\DEFL('b)" definition - "(liftemb :: ('a \! 'b) u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ ('a \! 'b) u) = u_map\prj oo u_prj" + "(liftemb :: ('a \! 'b) u \ udom u) = u_map\emb" definition - "liftdefl (t::('a \! 'b) itself) = u_defl\DEFL('a \! 'b)" + "(liftprj :: udom u \ ('a \! 'b) u) = u_map\prj" -instance -using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::('a \! 'b) itself) = pdefl\DEFL('a \! 'b)" + +instance proof show "ep_pair emb (prj :: udom \ 'a \! 'b)" unfolding emb_sfun_def prj_sfun_def by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj) show "cast\DEFL('a \! 'b) = emb oo (prj :: udom \ 'a \! 'b)" unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map) -qed +qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+ end @@ -351,7 +327,7 @@ subsubsection {* Continuous function space *} -instantiation cfun :: (predomain, "domain") liftdomain +instantiation cfun :: (predomain, "domain") "domain" begin definition @@ -364,17 +340,15 @@ "defl (t::('a \ 'b) itself) = DEFL('a u \! 'b)" definition - "(liftemb :: ('a \ 'b) u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ ('a \ 'b) u) = u_map\prj oo u_prj" + "(liftemb :: ('a \ 'b) u \ udom u) = u_map\emb" definition - "liftdefl (t::('a \ 'b) itself) = u_defl\DEFL('a \ 'b)" + "(liftprj :: udom u \ ('a \ 'b) u) = u_map\prj" -instance -using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::('a \ 'b) itself) = pdefl\DEFL('a \ 'b)" + +instance proof have "ep_pair encode_cfun decode_cfun" by (rule ep_pair.intro, simp_all) thus "ep_pair emb (prj :: udom \ 'a \ 'b)" @@ -383,7 +357,7 @@ show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_cfun_def prj_cfun_def defl_cfun_def by (simp add: cast_DEFL cfcomp1) -qed +qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+ end @@ -393,7 +367,7 @@ subsubsection {* Strict product *} -instantiation sprod :: ("domain", "domain") liftdomain +instantiation sprod :: ("domain", "domain") "domain" begin definition @@ -406,25 +380,22 @@ "defl (t::('a \ 'b) itself) = sprod_defl\DEFL('a)\DEFL('b)" definition - "(liftemb :: ('a \ 'b) u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ ('a \ 'b) u) = u_map\prj oo u_prj" + "(liftemb :: ('a \ 'b) u \ udom u) = u_map\emb" definition - "liftdefl (t::('a \ 'b) itself) = u_defl\DEFL('a \ 'b)" + "(liftprj :: udom u \ ('a \ 'b) u) = u_map\prj" -instance -using liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::('a \ 'b) itself) = pdefl\DEFL('a \ 'b)" + +instance proof show "ep_pair emb (prj :: udom \ 'a \ 'b)" unfolding emb_sprod_def prj_sprod_def by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj) -next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map) -qed +qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+ end @@ -434,27 +405,43 @@ subsubsection {* Cartesian product *} +definition prod_liftdefl :: "udom u defl \ udom u defl \ udom u defl" + where "prod_liftdefl = defl_fun2 (u_map\prod_emb oo decode_prod_u) + (encode_prod_u oo u_map\prod_prj) sprod_map" + +lemma cast_prod_liftdefl: + "cast\(prod_liftdefl\a\b) = + (u_map\prod_emb oo decode_prod_u) oo sprod_map\(cast\a)\(cast\b) oo + (encode_prod_u oo u_map\prod_prj)" +unfolding prod_liftdefl_def +apply (rule cast_defl_fun2) +apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod) +apply (simp add: ep_pair.intro) +apply (erule (1) finite_deflation_sprod_map) +done + instantiation prod :: (predomain, predomain) predomain begin definition - "liftemb = emb oo encode_prod_u" + "liftemb = (u_map\prod_emb oo decode_prod_u) oo + (sprod_map\liftemb\liftemb oo encode_prod_u)" definition - "liftprj = decode_prod_u oo prj" + "liftprj = (decode_prod_u oo sprod_map\liftprj\liftprj) oo + (encode_prod_u oo u_map\prod_prj)" definition - "liftdefl (t::('a \ 'b) itself) = DEFL('a\<^sub>\ \ 'b\<^sub>\)" + "liftdefl (t::('a \ 'b) itself) = prod_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" instance proof - have "ep_pair encode_prod_u decode_prod_u" - by (rule ep_pair.intro, simp_all) - thus "ep_pair liftemb (liftprj :: udom \ ('a \ 'b) u)" + show "ep_pair liftemb (liftprj :: udom u \ ('a \ 'b) u)" unfolding liftemb_prod_def liftprj_prod_def - using ep_pair_emb_prj by (rule ep_pair_comp) - show "cast\LIFTDEFL('a \ 'b) = liftemb oo (liftprj :: udom \ ('a \ 'b) u)" + by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map + ep_pair_prod predomain_ep, simp_all add: ep_pair.intro) + show "cast\LIFTDEFL('a \ 'b) = liftemb oo (liftprj :: udom u \ ('a \ 'b) u)" unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def - by (simp add: cast_DEFL cfcomp1) + by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map) qed end @@ -472,13 +459,25 @@ "defl (t::('a \ 'b) itself) = prod_defl\DEFL('a)\DEFL('b)" instance proof - show "ep_pair emb (prj :: udom \ 'a \ 'b)" + show 1: "ep_pair emb (prj :: udom \ 'a \ 'b)" unfolding emb_prod_def prj_prod_def by (intro ep_pair_comp ep_pair_prod ep_pair_cprod_map ep_pair_emb_prj) -next - show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" + show 2: "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map) + show 3: "liftemb = u_map\(emb :: 'a \ 'b \ udom)" + unfolding emb_prod_def liftemb_prod_def liftemb_eq + unfolding encode_prod_u_def decode_prod_u_def + by (rule cfun_eqI, case_tac x, simp, clarsimp) + show 4: "liftprj = u_map\(prj :: udom \ 'a \ 'b)" + unfolding prj_prod_def liftprj_prod_def liftprj_eq + unfolding encode_prod_u_def decode_prod_u_def + apply (rule cfun_eqI, case_tac x, simp) + apply (rename_tac y, case_tac "prod_prj\y", simp) + done + show 5: "LIFTDEFL('a \ 'b) = pdefl\DEFL('a \ 'b)" + by (rule cast_eq_imp_eq) + (simp add: cast_liftdefl cast_pdefl cast_DEFL 2 3 4 u_map_oo) qed end @@ -488,12 +487,13 @@ by (rule defl_prod_def) lemma LIFTDEFL_prod: - "LIFTDEFL('a::predomain \ 'b::predomain) = DEFL('a u \ 'b u)" + "LIFTDEFL('a::predomain \ 'b::predomain) = + prod_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" by (rule liftdefl_prod_def) subsubsection {* Unit type *} -instantiation unit :: liftdomain +instantiation unit :: "domain" begin definition @@ -506,24 +506,21 @@ "defl (t::unit itself) = \" definition - "(liftemb :: unit u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ unit u) = u_map\prj oo u_prj" + "(liftemb :: unit u \ udom u) = u_map\emb" definition - "liftdefl (t::unit itself) = u_defl\DEFL(unit)" + "(liftprj :: udom u \ unit u) = u_map\prj" -instance -using liftemb_unit_def liftprj_unit_def liftdefl_unit_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::unit itself) = pdefl\DEFL(unit)" + +instance proof show "ep_pair emb (prj :: udom \ unit)" unfolding emb_unit_def prj_unit_def by (simp add: ep_pair.intro) -next show "cast\DEFL(unit) = emb oo (prj :: udom \ unit)" unfolding emb_unit_def prj_unit_def defl_unit_def by simp -qed +qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+ end @@ -533,34 +530,38 @@ begin definition - "(liftemb :: 'a discr u \ udom) = udom_emb discr_approx" + "(liftemb :: 'a discr u \ udom u) = strictify\up oo udom_emb discr_approx" definition - "(liftprj :: udom \ 'a discr u) = udom_prj discr_approx" + "(liftprj :: udom u \ 'a discr u) = udom_prj discr_approx oo fup\ID" definition "liftdefl (t::'a discr itself) = - (\i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom \ 'a discr u))))" + (\i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \ 'a discr u))))" instance proof - show "ep_pair liftemb (liftprj :: udom \ 'a discr u)" + show 1: "ep_pair liftemb (liftprj :: udom u \ 'a discr u)" unfolding liftemb_discr_def liftprj_discr_def - by (rule ep_pair_udom [OF discr_approx]) - show "cast\LIFTDEFL('a discr) = liftemb oo (liftprj :: udom \ 'a discr u)" - unfolding liftemb_discr_def liftprj_discr_def liftdefl_discr_def + apply (intro ep_pair_comp ep_pair_udom [OF discr_approx]) + apply (rule ep_pair.intro) + apply (simp add: strictify_conv_if) + apply (case_tac y, simp, simp add: strictify_conv_if) + done + show "cast\LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \ 'a discr u)" + unfolding liftdefl_discr_def apply (subst contlub_cfun_arg) apply (rule chainI) apply (rule defl.principal_mono) apply (simp add: below_fin_defl_def) apply (simp add: Abs_fin_defl_inverse - ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]] + ep_pair.finite_deflation_e_d_p [OF 1] approx_chain.finite_deflation_approx [OF discr_approx]) apply (intro monofun_cfun below_refl) apply (rule chainE) apply (rule chain_discr_approx) apply (subst cast_defl_principal) apply (simp add: Abs_fin_defl_inverse - ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]] + ep_pair.finite_deflation_e_d_p [OF 1] approx_chain.finite_deflation_approx [OF discr_approx]) apply (simp add: lub_distribs) done @@ -570,7 +571,7 @@ subsubsection {* Strict sum *} -instantiation ssum :: ("domain", "domain") liftdomain +instantiation ssum :: ("domain", "domain") "domain" begin definition @@ -583,24 +584,22 @@ "defl (t::('a \ 'b) itself) = ssum_defl\DEFL('a)\DEFL('b)" definition - "(liftemb :: ('a \ 'b) u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ ('a \ 'b) u) = u_map\prj oo u_prj" + "(liftemb :: ('a \ 'b) u \ udom u) = u_map\emb" definition - "liftdefl (t::('a \ 'b) itself) = u_defl\DEFL('a \ 'b)" + "(liftprj :: udom u \ ('a \ 'b) u) = u_map\prj" -instance -using liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::('a \ 'b) itself) = pdefl\DEFL('a \ 'b)" + +instance proof show "ep_pair emb (prj :: udom \ 'a \ 'b)" unfolding emb_ssum_def prj_ssum_def by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj) show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map) -qed +qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+ end @@ -610,7 +609,7 @@ subsubsection {* Lifted HOL type *} -instantiation lift :: (countable) liftdomain +instantiation lift :: (countable) "domain" begin definition @@ -623,17 +622,15 @@ "defl (t::'a lift itself) = DEFL('a discr u)" definition - "(liftemb :: 'a lift u \ udom) = u_emb oo u_map\emb" - -definition - "(liftprj :: udom \ 'a lift u) = u_map\prj oo u_prj" + "(liftemb :: 'a lift u \ udom u) = u_map\emb" definition - "liftdefl (t::'a lift itself) = u_defl\DEFL('a lift)" + "(liftprj :: udom u \ 'a lift u) = u_map\prj" -instance -using liftemb_lift_def liftprj_lift_def liftdefl_lift_def -proof (rule liftdomain_class_intro) +definition + "liftdefl (t::'a lift itself) = pdefl\DEFL('a lift)" + +instance proof note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse have "ep_pair (\(x::'a lift). Rep_lift x) (\ y. Abs_lift y)" by (simp add: ep_pair_def) @@ -643,7 +640,7 @@ show "cast\DEFL('a lift) = emb oo (prj :: udom \ 'a lift)" unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL by (simp add: cfcomp1) -qed +qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+ end diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Dec 19 17:37:19 2010 -0800 @@ -69,6 +69,7 @@ val udomT = @{typ udom} val deflT = @{typ "udom defl"} +val udeflT = @{typ "udom u defl"} fun mk_DEFL T = Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T @@ -77,7 +78,7 @@ | dest_DEFL t = raise TERM ("dest_DEFL", [t]) fun mk_LIFTDEFL T = - Const (@{const_name liftdefl}, Term.itselfT T --> deflT) $ Logic.mk_type T + Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) $ Logic.mk_type T fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t]) @@ -100,6 +101,9 @@ fun isodefl_const T = Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT) +fun isodefl'_const T = + Const (@{const_name isodefl'}, (T ->> T) --> udeflT --> HOLogic.boolT) + fun mk_deflation t = Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t @@ -218,7 +222,7 @@ | _ => NONE) handle TERM _ => NONE fun proc2 t = (case dest_LIFTDEFL t of - TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, deflT)) + TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, udeflT)) | _ => NONE) handle TERM _ => NONE in Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T) @@ -492,7 +496,7 @@ let val defl_bind = Binding.suffix_name "_defl" tbind val defl_type = - map Term.itselfT typeTs ---> map (K deflT) defl_args -->> deflT + map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT in Sign.declare_const ((defl_bind, defl_type), NoSyn) thy end @@ -614,11 +618,11 @@ let fun unprime a = Library.unprefix "'" a fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT) - fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), deflT) + fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), udeflT) fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T) fun mk_assm t = case try dest_LIFTDEFL t of - SOME T => mk_trp (isodefl_const (mk_upT T) $ mk_u_map (mk_f T) $ mk_p T) + SOME T => mk_trp (isodefl'_const T $ mk_f T $ mk_p T) | NONE => let val T = dest_DEFL t in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun Dec 19 17:37:19 2010 -0800 @@ -50,12 +50,13 @@ val udomT = @{typ udom} val deflT = @{typ "udom defl"} +val udeflT = @{typ "udom u defl"} fun emb_const T = Const (@{const_name emb}, T ->> udomT) fun prj_const T = Const (@{const_name prj}, udomT ->> T) fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT) -fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> udomT) -fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T) -fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT) +fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> mk_upT udomT) +fun liftprj_const T = Const (@{const_name liftprj}, mk_upT udomT ->> mk_upT T) +fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) fun mk_u_map t = let @@ -129,15 +130,13 @@ val defl_eqn = Logic.mk_equals (defl_const newT, Abs ("x", Term.itselfT newT, defl)) val liftemb_eqn = - Logic.mk_equals (liftemb_const newT, - mk_cfcomp (@{const u_emb}, mk_u_map (emb_const newT))) + Logic.mk_equals (liftemb_const newT, mk_u_map (emb_const newT)) val liftprj_eqn = - Logic.mk_equals (liftprj_const newT, - mk_cfcomp (mk_u_map (prj_const newT), @{const u_prj})) + Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT)) val liftdefl_eqn = Logic.mk_equals (liftdefl_const newT, Abs ("t", Term.itselfT newT, - mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT))) + mk_capply (@{const pdefl}, defl_const newT $ Logic.mk_type newT))) val name_def = Binding.suffix_name "_def" name val emb_bind = (Binding.prefix_name "emb_" name_def, []) @@ -149,7 +148,7 @@ (*instantiate class rep*) val lthy = thy - |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain}) + |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain}) val ((_, (_, emb_ldef)), lthy) = Specification.definition (NONE, (emb_bind, emb_eqn)) lthy val ((_, (_, prj_ldef)), lthy) = @@ -178,7 +177,7 @@ liftemb_def, liftprj_def, liftdefl_def] val thy = lthy |> Class.prove_instantiation_instance - (K (Tactic.rtac (@{thm typedef_liftdomain_class} OF typedef_thms) 1)) + (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1)) |> Local_Theory.exit_global (*other theorems*) diff -r 752d81c2ce25 -r 2b7bc8d9fd6e src/HOL/HOLCF/ex/Domain_Proofs.thy --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Sun Dec 19 10:33:46 2010 -0800 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Sun Dec 19 17:37:19 2010 -0800 @@ -17,9 +17,6 @@ and 'a bar = Bar (lazy "'a baz \ tr") and 'a baz = Baz (lazy "'a foo convex_pd \ tr") -TODO: add another type parameter that is strict, -to show the different handling of LIFTDEFL vs. DEFL. - *) (********************************************************************) @@ -33,15 +30,15 @@ "udom defl \ udom defl \ udom defl \ udom defl \ udom defl \ udom defl \ udom defl" where "foo_bar_baz_deflF = (\ a. Abs_cfun (\(t1, t2, t3). - ( ssum_defl\DEFL(one)\(sprod_defl\a\(u_defl\t2)) - , u_defl\(sfun_defl\(u_defl\t3)\DEFL(tr)) - , u_defl\(sfun_defl\(u_defl\(convex_defl\t1))\DEFL(tr)))))" + ( ssum_defl\DEFL(one)\(sprod_defl\(u_defl\(pdefl\a))\(u_defl\(pdefl\t2))) + , u_defl\(pdefl\(sfun_defl\(u_defl\(pdefl\t3))\DEFL(tr))) + , u_defl\(pdefl\(sfun_defl\(u_defl\(pdefl\(convex_defl\t1)))\DEFL(tr))))))" lemma foo_bar_baz_deflF_beta: "foo_bar_baz_deflF\a\t = - ( ssum_defl\DEFL(one)\(sprod_defl\a\(u_defl\(fst (snd t)))) - , u_defl\(sfun_defl\(u_defl\(snd (snd t)))\DEFL(tr)) - , u_defl\(sfun_defl\(u_defl\(convex_defl\(fst t)))\DEFL(tr)))" + ( ssum_defl\DEFL(one)\(sprod_defl\(u_defl\(pdefl\a))\(u_defl\(pdefl\(fst (snd t))))) + , u_defl\(pdefl\(sfun_defl\(u_defl\(pdefl\(snd (snd t))))\DEFL(tr))) + , u_defl\(pdefl\(sfun_defl\(u_defl\(pdefl\(convex_defl\(fst t))))\DEFL(tr))))" unfolding foo_bar_baz_deflF_def by (simp add: split_def) @@ -65,13 +62,13 @@ text {* Unfold rules for each combinator. *} lemma foo_defl_unfold: - "foo_defl\a = ssum_defl\DEFL(one)\(sprod_defl\a\(u_defl\(bar_defl\a)))" + "foo_defl\a = ssum_defl\DEFL(one)\(sprod_defl\(u_defl\(pdefl\a))\(u_defl\(pdefl\(bar_defl\a))))" unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) -lemma bar_defl_unfold: "bar_defl\a = u_defl\(sfun_defl\(u_defl\(baz_defl\a))\DEFL(tr))" +lemma bar_defl_unfold: "bar_defl\a = u_defl\(pdefl\(sfun_defl\(u_defl\(pdefl\(baz_defl\a)))\DEFL(tr)))" unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) -lemma baz_defl_unfold: "baz_defl\a = u_defl\(sfun_defl\(u_defl\(convex_defl\(foo_defl\a)))\DEFL(tr))" +lemma baz_defl_unfold: "baz_defl\a = u_defl\(pdefl\(sfun_defl\(u_defl\(pdefl\(convex_defl\(foo_defl\a))))\DEFL(tr)))" 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 @@ -83,40 +80,40 @@ text {* Use @{text pcpodef} with the appropriate type combinator. *} -pcpodef (open) 'a foo = "defl_set (foo_defl\LIFTDEFL('a))" +pcpodef (open) 'a foo = "defl_set (foo_defl\DEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a bar = "defl_set (bar_defl\LIFTDEFL('a))" +pcpodef (open) 'a bar = "defl_set (bar_defl\DEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a baz = "defl_set (baz_defl\LIFTDEFL('a))" +pcpodef (open) 'a baz = "defl_set (baz_defl\DEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) text {* Prove rep instance using lemma @{text typedef_rep_class}. *} -instantiation foo :: ("domain") liftdomain +instantiation foo :: ("domain") "domain" begin definition emb_foo :: "'a foo \ udom" where "emb_foo \ (\ x. Rep_foo x)" definition prj_foo :: "udom \ 'a foo" -where "prj_foo \ (\ y. Abs_foo (cast\(foo_defl\LIFTDEFL('a))\y))" +where "prj_foo \ (\ y. Abs_foo (cast\(foo_defl\DEFL('a))\y))" definition defl_foo :: "'a foo itself \ udom defl" -where "defl_foo \ \a. foo_defl\LIFTDEFL('a)" +where "defl_foo \ \a. foo_defl\DEFL('a)" definition - "(liftemb :: 'a foo u \ udom) \ u_emb oo u_map\emb" + "(liftemb :: 'a foo u \ udom u) \ u_map\emb" definition - "(liftprj :: udom \ 'a foo u) \ u_map\prj oo u_prj" + "(liftprj :: udom u \ 'a foo u) \ u_map\prj" definition - "liftdefl \ \(t::'a foo itself). u_defl\DEFL('a foo)" + "liftdefl \ \(t::'a foo itself). pdefl\DEFL('a foo)" instance -apply (rule typedef_liftdomain_class) +apply (rule typedef_domain_class) apply (rule type_definition_foo) apply (rule below_foo_def) apply (rule emb_foo_def) @@ -129,29 +126,29 @@ end -instantiation bar :: ("domain") liftdomain +instantiation bar :: ("domain") "domain" begin definition emb_bar :: "'a bar \ udom" where "emb_bar \ (\ x. Rep_bar x)" definition prj_bar :: "udom \ 'a bar" -where "prj_bar \ (\ y. Abs_bar (cast\(bar_defl\LIFTDEFL('a))\y))" +where "prj_bar \ (\ y. Abs_bar (cast\(bar_defl\DEFL('a))\y))" definition defl_bar :: "'a bar itself \ udom defl" -where "defl_bar \ \a. bar_defl\LIFTDEFL('a)" +where "defl_bar \ \a. bar_defl\DEFL('a)" definition - "(liftemb :: 'a bar u \ udom) \ u_emb oo u_map\emb" + "(liftemb :: 'a bar u \ udom u) \ u_map\emb" definition - "(liftprj :: udom \ 'a bar u) \ u_map\prj oo u_prj" + "(liftprj :: udom u \ 'a bar u) \ u_map\prj" definition - "liftdefl \ \(t::'a bar itself). u_defl\DEFL('a bar)" + "liftdefl \ \(t::'a bar itself). pdefl\DEFL('a bar)" instance -apply (rule typedef_liftdomain_class) +apply (rule typedef_domain_class) apply (rule type_definition_bar) apply (rule below_bar_def) apply (rule emb_bar_def) @@ -164,29 +161,29 @@ end -instantiation baz :: ("domain") liftdomain +instantiation baz :: ("domain") "domain" begin definition emb_baz :: "'a baz \ udom" where "emb_baz \ (\ x. Rep_baz x)" definition prj_baz :: "udom \ 'a baz" -where "prj_baz \ (\ y. Abs_baz (cast\(baz_defl\LIFTDEFL('a))\y))" +where "prj_baz \ (\ y. Abs_baz (cast\(baz_defl\DEFL('a))\y))" definition defl_baz :: "'a baz itself \ udom defl" -where "defl_baz \ \a. baz_defl\LIFTDEFL('a)" +where "defl_baz \ \a. baz_defl\DEFL('a)" definition - "(liftemb :: 'a baz u \ udom) \ u_emb oo u_map\emb" + "(liftemb :: 'a baz u \ udom u) \ u_map\emb" definition - "(liftprj :: udom \ 'a baz u) \ u_map\prj oo u_prj" + "(liftprj :: udom u \ 'a baz u) \ u_map\prj" definition - "liftdefl \ \(t::'a baz itself). u_defl\DEFL('a baz)" + "liftdefl \ \(t::'a baz itself). pdefl\DEFL('a baz)" instance -apply (rule typedef_liftdomain_class) +apply (rule typedef_domain_class) apply (rule type_definition_baz) apply (rule below_baz_def) apply (rule emb_baz_def) @@ -201,17 +198,17 @@ text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *} -lemma DEFL_foo: "DEFL('a foo) = foo_defl\LIFTDEFL('a)" +lemma DEFL_foo: "DEFL('a foo) = foo_defl\DEFL('a)" apply (rule typedef_DEFL) apply (rule defl_foo_def) done -lemma DEFL_bar: "DEFL('a bar) = bar_defl\LIFTDEFL('a)" +lemma DEFL_bar: "DEFL('a bar) = bar_defl\DEFL('a)" apply (rule typedef_DEFL) apply (rule defl_bar_def) done -lemma DEFL_baz: "DEFL('a baz) = baz_defl\LIFTDEFL('a)" +lemma DEFL_baz: "DEFL('a baz) = baz_defl\DEFL('a)" apply (rule typedef_DEFL) apply (rule defl_baz_def) done @@ -348,7 +345,7 @@ text {* Prove isodefl rules for all map functions simultaneously. *} lemma isodefl_foo_bar_baz: - assumes isodefl_d: "isodefl (u_map\d) t" + assumes isodefl_d: "isodefl d t" shows "isodefl (foo_map\d) (foo_defl\t) \ isodefl (bar_map\d) (bar_defl\t) \ @@ -383,21 +380,21 @@ apply (rule isodefl_DEFL_imp_ID) apply (subst DEFL_foo) apply (rule isodefl_foo) -apply (rule isodefl_LIFTDEFL) +apply (rule isodefl_ID_DEFL) done lemma bar_map_ID: "bar_map\ID = ID" apply (rule isodefl_DEFL_imp_ID) apply (subst DEFL_bar) apply (rule isodefl_bar) -apply (rule isodefl_LIFTDEFL) +apply (rule isodefl_ID_DEFL) done lemma baz_map_ID: "baz_map\ID = ID" apply (rule isodefl_DEFL_imp_ID) apply (subst DEFL_baz) apply (rule isodefl_baz) -apply (rule isodefl_LIFTDEFL) +apply (rule isodefl_ID_DEFL) done (********************************************************************)