--- a/src/HOLCF/Algebraic.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Algebraic.thy Mon Oct 11 08:32:09 2010 -0700
@@ -72,36 +72,29 @@
subsection {* Defining algebraic deflations by ideal completion *}
-text {*
- An SFP domain is one that can be represented as the limit of a
- sequence of finite posets. Here we use omega-algebraic deflations
- (i.e. countable ideals of finite deflations) to model sequences of
- finite posets.
-*}
-
-typedef (open) sfp = "{S::fin_defl set. below.ideal S}"
+typedef (open) defl = "{S::fin_defl set. below.ideal S}"
by (fast intro: below.ideal_principal)
-instantiation sfp :: below
+instantiation defl :: below
begin
definition
- "x \<sqsubseteq> y \<longleftrightarrow> Rep_sfp x \<subseteq> Rep_sfp y"
+ "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
instance ..
end
-instance sfp :: po
-using type_definition_sfp below_sfp_def
+instance defl :: po
+using type_definition_defl below_defl_def
by (rule below.typedef_ideal_po)
-instance sfp :: cpo
-using type_definition_sfp below_sfp_def
+instance defl :: cpo
+using type_definition_defl below_defl_def
by (rule below.typedef_ideal_cpo)
definition
- sfp_principal :: "fin_defl \<Rightarrow> sfp" where
- "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
+ defl_principal :: "fin_defl \<Rightarrow> defl" where
+ "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
proof
@@ -130,52 +123,52 @@
done
qed
-interpretation sfp: ideal_completion below sfp_principal Rep_sfp
-using type_definition_sfp below_sfp_def
-using sfp_principal_def fin_defl_countable
+interpretation defl: ideal_completion below defl_principal Rep_defl
+using type_definition_defl below_defl_def
+using defl_principal_def fin_defl_countable
by (rule below.typedef_ideal_completion)
text {* Algebraic deflations are pointed *}
-lemma sfp_minimal: "sfp_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
-apply (induct x rule: sfp.principal_induct, simp)
-apply (rule sfp.principal_mono)
+lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
+apply (induct x rule: defl.principal_induct, simp)
+apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def)
apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
done
-instance sfp :: pcpo
-by intro_classes (fast intro: sfp_minimal)
+instance defl :: pcpo
+by intro_classes (fast intro: defl_minimal)
-lemma inst_sfp_pcpo: "\<bottom> = sfp_principal (Abs_fin_defl \<bottom>)"
-by (rule sfp_minimal [THEN UU_I, symmetric])
+lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
+by (rule defl_minimal [THEN UU_I, symmetric])
subsection {* Applying algebraic deflations *}
definition
- cast :: "sfp \<rightarrow> udom \<rightarrow> udom"
+ cast :: "defl \<rightarrow> udom \<rightarrow> udom"
where
- "cast = sfp.basis_fun Rep_fin_defl"
+ "cast = defl.basis_fun Rep_fin_defl"
-lemma cast_sfp_principal:
- "cast\<cdot>(sfp_principal a) = Rep_fin_defl a"
+lemma cast_defl_principal:
+ "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
unfolding cast_def
-apply (rule sfp.basis_fun_principal)
+apply (rule defl.basis_fun_principal)
apply (simp only: below_fin_defl_def)
done
lemma deflation_cast: "deflation (cast\<cdot>d)"
-apply (induct d rule: sfp.principal_induct)
+apply (induct d rule: defl.principal_induct)
apply (rule adm_subst [OF _ adm_deflation], simp)
-apply (simp add: cast_sfp_principal)
+apply (simp add: cast_defl_principal)
apply (rule finite_deflation_imp_deflation)
apply (rule finite_deflation_Rep_fin_defl)
done
lemma finite_deflation_cast:
"compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
-apply (drule sfp.compact_imp_principal, clarify)
-apply (simp add: cast_sfp_principal)
+apply (drule defl.compact_imp_principal, clarify)
+apply (simp add: cast_defl_principal)
apply (rule finite_deflation_Rep_fin_defl)
done
@@ -190,9 +183,9 @@
done
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
-apply (induct A rule: sfp.principal_induct, simp)
-apply (induct B rule: sfp.principal_induct, simp)
-apply (simp add: cast_sfp_principal below_fin_defl_def)
+apply (induct A rule: defl.principal_induct, simp)
+apply (induct B rule: defl.principal_induct, simp)
+apply (simp add: cast_defl_principal below_fin_defl_def)
done
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
@@ -209,8 +202,8 @@
by (simp add: below_antisym cast_below_imp_below)
lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
-apply (subst inst_sfp_pcpo)
-apply (subst cast_sfp_principal)
+apply (subst inst_defl_pcpo)
+apply (subst cast_defl_principal)
apply (rule Abs_fin_defl_inverse)
apply (simp add: finite_deflation_UU)
done
@@ -221,40 +214,40 @@
subsection {* Deflation membership relation *}
definition
- in_sfp :: "udom \<Rightarrow> sfp \<Rightarrow> bool" (infixl ":::" 50)
+ in_defl :: "udom \<Rightarrow> defl \<Rightarrow> bool" (infixl ":::" 50)
where
"x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
-lemma adm_in_sfp: "adm (\<lambda>x. x ::: A)"
-unfolding in_sfp_def by simp
+lemma adm_in_defl: "adm (\<lambda>x. x ::: A)"
+unfolding in_defl_def by simp
-lemma in_sfpI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
-unfolding in_sfp_def .
+lemma in_deflI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
+unfolding in_defl_def .
lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
-unfolding in_sfp_def .
+unfolding in_defl_def .
-lemma cast_in_sfp [simp]: "cast\<cdot>A\<cdot>x ::: A"
-unfolding in_sfp_def by (rule cast.idem)
+lemma cast_in_defl [simp]: "cast\<cdot>A\<cdot>x ::: A"
+unfolding in_defl_def by (rule cast.idem)
-lemma bottom_in_sfp [simp]: "\<bottom> ::: A"
-unfolding in_sfp_def by (rule cast_strict2)
+lemma bottom_in_defl [simp]: "\<bottom> ::: A"
+unfolding in_defl_def by (rule cast_strict2)
-lemma sfp_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
-unfolding in_sfp_def
+lemma defl_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
+unfolding in_defl_def
apply (rule deflation.belowD)
apply (rule deflation_cast)
apply (erule monofun_cfun_arg)
apply assumption
done
-lemma rev_sfp_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
-by (rule sfp_belowD)
+lemma rev_defl_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
+by (rule defl_belowD)
-lemma sfp_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
+lemma defl_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
apply (rule cast_below_imp_below)
apply (rule cast.belowI)
-apply (simp add: in_sfp_def)
+apply (simp add: in_defl_def)
done
end
--- a/src/HOLCF/Bifinite.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Bifinite.thy Mon Oct 11 08:32:09 2010 -0700
@@ -18,12 +18,12 @@
class bifinite = pcpo +
fixes emb :: "'a::pcpo \<rightarrow> udom"
fixes prj :: "udom \<rightarrow> 'a::pcpo"
- fixes sfp :: "'a itself \<Rightarrow> sfp"
+ fixes defl :: "'a itself \<Rightarrow> defl"
assumes ep_pair_emb_prj: "ep_pair emb prj"
- assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
+ assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
-syntax "_SFP" :: "type \<Rightarrow> sfp" ("(1SFP/(1'(_')))")
-translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
+syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))")
+translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
interpretation bifinite:
pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
@@ -47,24 +47,24 @@
ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
proof -
obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
- and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
- by (rule sfp.obtain_principal_chain)
- def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
- interpret sfp_approx: approx_chain approx
+ and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))"
+ by (rule defl.obtain_principal_chain)
+ def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
+ interpret defl_approx: approx_chain approx
proof (rule approx_chain.intro)
show "chain (\<lambda>i. approx i)"
unfolding approx_def by (simp add: Y)
show "(\<Squnion>i. approx i) = ID"
unfolding approx_def
- by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
+ by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq)
show "\<And>i. finite_deflation (approx i)"
unfolding approx_def
apply (rule bifinite.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
- apply (rule sfp.compact_principal)
+ apply (rule defl.compact_principal)
apply (rule below_trans [OF monofun_cfun_fun])
apply (rule is_ub_thelub, simp add: Y)
- apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
+ apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL)
done
qed
(* FIXME: why does show ?thesis fail here? *)
@@ -74,30 +74,30 @@
subsection {* Type combinators *}
definition
- sfp_fun1 ::
- "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
+ defl_fun1 ::
+ "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
where
- "sfp_fun1 approx f =
- sfp.basis_fun (\<lambda>a.
- sfp_principal (Abs_fin_defl
+ "defl_fun1 approx f =
+ defl.basis_fun (\<lambda>a.
+ defl_principal (Abs_fin_defl
(udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
definition
- sfp_fun2 ::
+ defl_fun2 ::
"(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
- \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
+ \<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)"
where
- "sfp_fun2 approx f =
- sfp.basis_fun (\<lambda>a.
- sfp.basis_fun (\<lambda>b.
- sfp_principal (Abs_fin_defl
+ "defl_fun2 approx f =
+ defl.basis_fun (\<lambda>a.
+ defl.basis_fun (\<lambda>b.
+ defl_principal (Abs_fin_defl
(udom_emb approx oo
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
-lemma cast_sfp_fun1:
+lemma cast_defl_fun1:
assumes approx: "approx_chain approx"
assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
- shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
+ shows "cast\<cdot>(defl_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
proof -
have 1: "\<And>a. finite_deflation
(udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
@@ -106,23 +106,23 @@
apply (rule f, rule finite_deflation_Rep_fin_defl)
done
show ?thesis
- by (induct A rule: sfp.principal_induct, simp)
- (simp only: sfp_fun1_def
- sfp.basis_fun_principal
- sfp.basis_fun_mono
- sfp.principal_mono
+ by (induct A rule: defl.principal_induct, simp)
+ (simp only: defl_fun1_def
+ defl.basis_fun_principal
+ defl.basis_fun_mono
+ defl.principal_mono
Abs_fin_defl_mono [OF 1 1]
monofun_cfun below_refl
Rep_fin_defl_mono
- cast_sfp_principal
+ cast_defl_principal
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed
-lemma cast_sfp_fun2:
+lemma cast_defl_fun2:
assumes approx: "approx_chain approx"
assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
finite_deflation (f\<cdot>a\<cdot>b)"
- shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
+ shows "cast\<cdot>(defl_fun2 approx f\<cdot>A\<cdot>B) =
udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
proof -
have 1: "\<And>a b. finite_deflation (udom_emb approx oo
@@ -132,15 +132,15 @@
apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
done
show ?thesis
- by (induct A B rule: sfp.principal_induct2, simp, simp)
- (simp only: sfp_fun2_def
- sfp.basis_fun_principal
- sfp.basis_fun_mono
- sfp.principal_mono
+ by (induct A B rule: defl.principal_induct2, simp, simp)
+ (simp only: defl_fun2_def
+ defl.basis_fun_principal
+ defl.basis_fun_mono
+ defl.principal_mono
Abs_fin_defl_mono [OF 1 1]
monofun_cfun below_refl
Rep_fin_defl_mono
- cast_sfp_principal
+ cast_defl_principal
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed
@@ -156,22 +156,22 @@
"prj = (ID :: udom \<rightarrow> udom)"
definition
- "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
+ "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> udom)"
by (simp add: ep_pair.intro)
next
- show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
- unfolding sfp_udom_def
+ show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
+ unfolding defl_udom_def
apply (subst contlub_cfun_arg)
apply (rule chainI)
- apply (rule sfp.principal_mono)
+ apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def)
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
apply (rule chainE)
apply (rule chain_udom_approx)
- apply (subst cast_sfp_principal)
+ apply (subst cast_defl_principal)
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
done
qed
@@ -197,14 +197,14 @@
by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
qed
-definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
+definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "cfun_defl = defl_fun2 cfun_approx cfun_map"
-lemma cast_cfun_sfp:
- "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
+lemma cast_cfun_defl:
+ "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
-unfolding cfun_sfp_def
-apply (rule cast_sfp_fun2 [OF cfun_approx])
+unfolding cfun_defl_def
+apply (rule cast_defl_fun2 [OF cfun_approx])
apply (erule (1) finite_deflation_cfun_map)
done
@@ -218,7 +218,7 @@
"prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
definition
- "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+ "defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
@@ -226,16 +226,16 @@
using ep_pair_udom [OF cfun_approx]
by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
- unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
+ show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+ unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
+ by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map)
qed
end
-lemma SFP_cfun:
- "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_cfun_def)
+lemma DEFL_cfun:
+ "DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_cfun_def)
subsection {* Cartesian product is a bifinite domain *}
@@ -256,14 +256,14 @@
by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
qed
-definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "prod_sfp = sfp_fun2 prod_approx cprod_map"
+definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "prod_defl = defl_fun2 prod_approx cprod_map"
-lemma cast_prod_sfp:
- "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
+lemma cast_prod_defl:
+ "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
-unfolding prod_sfp_def
-apply (rule cast_sfp_fun2 [OF prod_approx])
+unfolding prod_defl_def
+apply (rule cast_defl_fun2 [OF prod_approx])
apply (erule (1) finite_deflation_cprod_map)
done
@@ -277,7 +277,7 @@
"prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
definition
- "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+ "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
@@ -285,16 +285,16 @@
using ep_pair_udom [OF prod_approx]
by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
+ show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
+ by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map)
qed
end
-lemma SFP_prod:
- "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_prod_def)
+lemma DEFL_prod:
+ "DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_prod_def)
subsection {* Strict product is a bifinite domain *}
@@ -315,16 +315,16 @@
by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
qed
-definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
+definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "sprod_defl = defl_fun2 sprod_approx sprod_map"
-lemma cast_sprod_sfp:
- "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
+lemma cast_sprod_defl:
+ "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
udom_emb sprod_approx oo
sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
udom_prj sprod_approx"
-unfolding sprod_sfp_def
-apply (rule cast_sfp_fun2 [OF sprod_approx])
+unfolding sprod_defl_def
+apply (rule cast_defl_fun2 [OF sprod_approx])
apply (erule (1) finite_deflation_sprod_map)
done
@@ -338,7 +338,7 @@
"prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
definition
- "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+ "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
@@ -346,16 +346,16 @@
using ep_pair_udom [OF sprod_approx]
by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
- unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
+ show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
+ unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
+ by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map)
qed
end
-lemma SFP_sprod:
- "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_sprod_def)
+lemma DEFL_sprod:
+ "DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sprod_def)
subsection {* Lifted cpo is a bifinite domain *}
@@ -374,14 +374,14 @@
by (intro finite_deflation_u_map finite_deflation_udom_approx)
qed
-definition u_sfp :: "sfp \<rightarrow> sfp"
-where "u_sfp = sfp_fun1 u_approx u_map"
+definition u_defl :: "defl \<rightarrow> defl"
+where "u_defl = defl_fun1 u_approx u_map"
-lemma cast_u_sfp:
- "cast\<cdot>(u_sfp\<cdot>A) =
+lemma cast_u_defl:
+ "cast\<cdot>(u_defl\<cdot>A) =
udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
-unfolding u_sfp_def
-apply (rule cast_sfp_fun1 [OF u_approx])
+unfolding u_defl_def
+apply (rule cast_defl_fun1 [OF u_approx])
apply (erule finite_deflation_u_map)
done
@@ -395,7 +395,7 @@
"prj = u_map\<cdot>prj oo udom_prj u_approx"
definition
- "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
+ "defl (t::'a u itself) = u_defl\<cdot>DEFL('a)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
@@ -403,15 +403,15 @@
using ep_pair_udom [OF u_approx]
by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
- unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
+ show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def defl_u_def cast_u_defl
+ by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map)
qed
end
-lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
-by (rule sfp_u_def)
+lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\<cdot>DEFL('a)"
+by (rule defl_u_def)
subsection {* Lifted countable types are bifinite domains *}
@@ -472,25 +472,25 @@
"prj = udom_prj lift_approx"
definition
- "sfp (t::'a lift itself) =
- (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
+ "defl (t::'a lift itself) =
+ (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
instance proof
show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
unfolding emb_lift_def prj_lift_def
by (rule ep_pair_udom [OF lift_approx])
- show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
- unfolding sfp_lift_def
+ show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
+ unfolding defl_lift_def
apply (subst contlub_cfun_arg)
apply (rule chainI)
- apply (rule sfp.principal_mono)
+ apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def)
apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
ep_pair.finite_deflation_e_d_p [OF ep])
apply (intro monofun_cfun below_refl)
apply (rule chainE)
apply (rule chain_lift_approx)
- apply (subst cast_sfp_principal)
+ apply (subst cast_defl_principal)
apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
done
@@ -517,14 +517,14 @@
by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
qed
-definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
+definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "ssum_defl = defl_fun2 ssum_approx ssum_map"
-lemma cast_ssum_sfp:
- "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
+lemma cast_ssum_defl:
+ "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
-unfolding ssum_sfp_def
-apply (rule cast_sfp_fun2 [OF ssum_approx])
+unfolding ssum_defl_def
+apply (rule cast_defl_fun2 [OF ssum_approx])
apply (erule (1) finite_deflation_ssum_map)
done
@@ -538,7 +538,7 @@
"prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
definition
- "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+ "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
@@ -546,15 +546,15 @@
using ep_pair_udom [OF ssum_approx]
by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
- unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
+ show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+ unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
+ by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map)
qed
end
-lemma SFP_ssum:
- "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_ssum_def)
+lemma DEFL_ssum:
+ "DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_ssum_def)
end
--- a/src/HOLCF/ConvexPD.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy Mon Oct 11 08:32:09 2010 -0700
@@ -463,14 +463,14 @@
by (intro finite_deflation_convex_map finite_deflation_udom_approx)
qed
-definition convex_sfp :: "sfp \<rightarrow> sfp"
-where "convex_sfp = sfp_fun1 convex_approx convex_map"
+definition convex_defl :: "defl \<rightarrow> defl"
+where "convex_defl = defl_fun1 convex_approx convex_map"
-lemma cast_convex_sfp:
- "cast\<cdot>(convex_sfp\<cdot>A) =
+lemma cast_convex_defl:
+ "cast\<cdot>(convex_defl\<cdot>A) =
udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
-unfolding convex_sfp_def
-apply (rule cast_sfp_fun1 [OF convex_approx])
+unfolding convex_defl_def
+apply (rule cast_defl_fun1 [OF convex_approx])
apply (erule finite_deflation_convex_map)
done
@@ -484,7 +484,7 @@
"prj = convex_map\<cdot>prj oo udom_prj convex_approx"
definition
- "sfp (t::'a convex_pd itself) = convex_sfp\<cdot>SFP('a)"
+ "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
@@ -492,17 +492,17 @@
using ep_pair_udom [OF convex_approx]
by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
- unfolding emb_convex_pd_def prj_convex_pd_def sfp_convex_pd_def cast_convex_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq convex_map_map)
+ show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> '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 expand_cfun_eq convex_map_map)
qed
end
-text {* SFP of type constructor = type combinator *}
+text {* DEFL of type constructor = type combinator *}
-lemma SFP_convex: "SFP('a convex_pd) = convex_sfp\<cdot>SFP('a)"
-by (rule sfp_convex_pd_def)
+lemma DEFL_convex: "DEFL('a convex_pd) = convex_defl\<cdot>DEFL('a)"
+by (rule defl_convex_pd_def)
subsection {* Join *}
--- a/src/HOLCF/Library/Strict_Fun.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Library/Strict_Fun.thy Mon Oct 11 08:32:09 2010 -0700
@@ -162,14 +162,14 @@
by (intro finite_deflation_sfun_map finite_deflation_udom_approx)
qed
-definition sfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "sfun_sfp = sfp_fun2 sfun_approx sfun_map"
+definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "sfun_defl = defl_fun2 sfun_approx sfun_map"
-lemma cast_sfun_sfp:
- "cast\<cdot>(sfun_sfp\<cdot>A\<cdot>B) =
+lemma cast_sfun_defl:
+ "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
-unfolding sfun_sfp_def
-apply (rule cast_sfp_fun2 [OF sfun_approx])
+unfolding sfun_defl_def
+apply (rule cast_defl_fun2 [OF sfun_approx])
apply (erule (1) finite_deflation_sfun_map)
done
@@ -183,7 +183,7 @@
"prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
definition
- "sfp (t::('a \<rightarrow>! 'b) itself) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+ "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
@@ -191,29 +191,29 @@
using ep_pair_udom [OF sfun_approx]
by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
- unfolding emb_sfun_def prj_sfun_def sfp_sfun_def cast_sfun_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq sfun_map_map)
+ show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+ unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
+ by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map)
qed
end
-lemma SFP_sfun:
- "SFP('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_sfun_def)
+lemma DEFL_sfun:
+ "DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sfun_def)
lemma isodefl_sfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_sfp\<cdot>t1\<cdot>t2)"
+ isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_sfun_sfp cast_isodefl)
+apply (simp add: cast_sfun_defl cast_isodefl)
apply (simp add: emb_sfun_def prj_sfun_def)
apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
done
setup {*
Domain_Isomorphism.add_type_constructor
- (@{type_name "sfun"}, @{term sfun_sfp}, @{const_name sfun_map}, @{thm SFP_sfun},
+ (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm DEFL_sfun},
@{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
*}
--- a/src/HOLCF/LowerPD.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/LowerPD.thy Mon Oct 11 08:32:09 2010 -0700
@@ -452,14 +452,14 @@
by (intro finite_deflation_lower_map finite_deflation_udom_approx)
qed
-definition lower_sfp :: "sfp \<rightarrow> sfp"
-where "lower_sfp = sfp_fun1 lower_approx lower_map"
+definition lower_defl :: "defl \<rightarrow> defl"
+where "lower_defl = defl_fun1 lower_approx lower_map"
-lemma cast_lower_sfp:
- "cast\<cdot>(lower_sfp\<cdot>A) =
+lemma cast_lower_defl:
+ "cast\<cdot>(lower_defl\<cdot>A) =
udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
-unfolding lower_sfp_def
-apply (rule cast_sfp_fun1 [OF lower_approx])
+unfolding lower_defl_def
+apply (rule cast_defl_fun1 [OF lower_approx])
apply (erule finite_deflation_lower_map)
done
@@ -473,7 +473,7 @@
"prj = lower_map\<cdot>prj oo udom_prj lower_approx"
definition
- "sfp (t::'a lower_pd itself) = lower_sfp\<cdot>SFP('a)"
+ "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
@@ -481,15 +481,15 @@
using ep_pair_udom [OF lower_approx]
by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
- unfolding emb_lower_pd_def prj_lower_pd_def sfp_lower_pd_def cast_lower_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq lower_map_map)
+ show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> '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 expand_cfun_eq lower_map_map)
qed
end
-lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\<cdot>SFP('a)"
-by (rule sfp_lower_pd_def)
+lemma DEFL_lower: "DEFL('a lower_pd) = lower_defl\<cdot>DEFL('a)"
+by (rule defl_lower_pd_def)
subsection {* Join *}
--- a/src/HOLCF/Powerdomains.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Powerdomains.thy Mon Oct 11 08:32:09 2010 -0700
@@ -9,25 +9,25 @@
begin
lemma isodefl_upper:
- "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_sfp\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_upper_sfp cast_isodefl)
+apply (simp add: cast_upper_defl cast_isodefl)
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
apply (simp add: upper_map_map)
done
lemma isodefl_lower:
- "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_sfp\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_lower_sfp cast_isodefl)
+apply (simp add: cast_lower_defl cast_isodefl)
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
apply (simp add: lower_map_map)
done
lemma isodefl_convex:
- "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_sfp\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_convex_sfp cast_isodefl)
+apply (simp add: cast_convex_defl cast_isodefl)
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
apply (simp add: convex_map_map)
done
@@ -36,16 +36,16 @@
setup {*
fold Domain_Isomorphism.add_type_constructor
- [(@{type_name "upper_pd"}, @{term upper_sfp}, @{const_name upper_map},
- @{thm SFP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
+ [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
+ @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
@{thm deflation_upper_map}),
- (@{type_name "lower_pd"}, @{term lower_sfp}, @{const_name lower_map},
- @{thm SFP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
+ (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
+ @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
@{thm deflation_lower_map}),
- (@{type_name "convex_pd"}, @{term convex_sfp}, @{const_name convex_map},
- @{thm SFP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
+ (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
+ @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
@{thm deflation_convex_map})]
*}
--- a/src/HOLCF/Representable.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Representable.thy Mon Oct 11 08:32:09 2010 -0700
@@ -15,20 +15,20 @@
subsection {* Representations of types *}
-lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>SFP('a)\<cdot>x"
-by (simp add: cast_SFP)
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
+by (simp add: cast_DEFL)
-lemma in_SFP_iff:
- "x ::: SFP('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
-by (simp add: in_sfp_def cast_SFP)
+lemma in_DEFL_iff:
+ "x ::: DEFL('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+by (simp add: in_defl_def cast_DEFL)
lemma prj_inverse:
- "x ::: SFP('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
-by (simp only: in_SFP_iff)
+ "x ::: DEFL('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+by (simp only: in_DEFL_iff)
-lemma emb_in_SFP [simp]:
- "emb\<cdot>(x::'a) ::: SFP('a)"
-by (simp add: in_SFP_iff)
+lemma emb_in_DEFL [simp]:
+ "emb\<cdot>(x::'a) ::: DEFL('a)"
+by (simp add: in_DEFL_iff)
subsection {* Coerce operator *}
@@ -48,16 +48,16 @@
by (rule ext_cfun, simp add: beta_coerce)
lemma emb_coerce:
- "SFP('a) \<sqsubseteq> SFP('b)
+ "DEFL('a) \<sqsubseteq> DEFL('b)
\<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
apply (simp add: beta_coerce)
apply (rule prj_inverse)
- apply (erule sfp_belowD)
- apply (rule emb_in_SFP)
+ apply (erule defl_belowD)
+ apply (rule emb_in_DEFL)
done
lemma coerce_prj:
- "SFP('a) \<sqsubseteq> SFP('b)
+ "DEFL('a) \<sqsubseteq> DEFL('b)
\<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
apply (simp add: coerce_def)
apply (rule emb_eq_iff [THEN iffD1])
@@ -69,21 +69,21 @@
done
lemma coerce_coerce [simp]:
- "SFP('a) \<sqsubseteq> SFP('b)
+ "DEFL('a) \<sqsubseteq> DEFL('b)
\<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
-by (simp add: beta_coerce prj_inverse sfp_belowD)
+by (simp add: beta_coerce prj_inverse defl_belowD)
lemma coerce_inverse:
- "emb\<cdot>(x::'a) ::: SFP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
+ "emb\<cdot>(x::'a) ::: DEFL('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
by (simp only: beta_coerce prj_inverse emb_inverse)
lemma coerce_type:
- "SFP('a) \<sqsubseteq> SFP('b)
- \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: SFP('a)"
-by (simp add: beta_coerce prj_inverse sfp_belowD)
+ "DEFL('a) \<sqsubseteq> DEFL('b)
+ \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: DEFL('a)"
+by (simp add: beta_coerce prj_inverse defl_belowD)
lemma ep_pair_coerce:
- "SFP('a) \<sqsubseteq> SFP('b)
+ "DEFL('a) \<sqsubseteq> DEFL('b)
\<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
apply (rule ep_pair.intro)
apply simp
@@ -98,19 +98,19 @@
lemma domain_abs_iso:
fixes abs and rep
- assumes SFP: "SFP('b) = SFP('a)"
+ assumes DEFL: "DEFL('b) = DEFL('a)"
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
shows "rep\<cdot>(abs\<cdot>x) = x"
-unfolding abs_def rep_def by (simp add: SFP)
+unfolding abs_def rep_def by (simp add: DEFL)
lemma domain_rep_iso:
fixes abs and rep
- assumes SFP: "SFP('b) = SFP('a)"
+ assumes DEFL: "DEFL('b) = DEFL('a)"
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
shows "abs\<cdot>(rep\<cdot>x) = x"
-unfolding abs_def rep_def by (simp add: SFP [symmetric])
+unfolding abs_def rep_def by (simp add: DEFL [symmetric])
subsection {* Proving a subtype is representable *}
@@ -120,7 +120,7 @@
*}
setup {* Sign.add_const_constraint
- (@{const_name sfp}, SOME @{typ "'a::pcpo itself \<Rightarrow> sfp"}) *}
+ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) *}
setup {* Sign.add_const_constraint
(@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
@@ -131,16 +131,16 @@
lemma typedef_rep_class:
fixes Rep :: "'a::pcpo \<Rightarrow> udom"
fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
- fixes t :: sfp
+ fixes t :: defl
assumes type: "type_definition Rep Abs {x. x ::: t}"
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
- assumes sfp: "sfp \<equiv> (\<lambda> a::'a itself. t)"
+ assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
shows "OFCLASS('a, bifinite_class)"
proof
have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
- by (simp add: adm_in_sfp)
+ by (simp add: adm_in_defl)
have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
unfolding emb
apply (rule beta_cfun)
@@ -152,12 +152,12 @@
apply (rule typedef_cont_Abs [OF type below adm])
apply simp_all
done
- have emb_in_sfp: "\<And>x::'a. emb\<cdot>x ::: t"
+ have emb_in_defl: "\<And>x::'a. emb\<cdot>x ::: t"
using type_definition.Rep [OF type]
by (simp add: emb_beta)
have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
unfolding prj_beta
- apply (simp add: cast_fixed [OF emb_in_sfp])
+ apply (simp add: cast_fixed [OF emb_in_defl])
apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
done
have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
@@ -168,19 +168,19 @@
apply (simp add: prj_emb)
apply (simp add: emb_prj cast.below)
done
- show "cast\<cdot>SFP('a) = emb oo (prj :: udom \<rightarrow> 'a)"
- by (rule ext_cfun, simp add: sfp emb_prj)
+ show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
+ by (rule ext_cfun, simp add: defl emb_prj)
qed
-lemma typedef_SFP:
- assumes "sfp \<equiv> (\<lambda>a::'a::pcpo itself. t)"
- shows "SFP('a::pcpo) = t"
+lemma typedef_DEFL:
+ assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
+ shows "DEFL('a::pcpo) = t"
unfolding assms ..
text {* Restore original typing constraints *}
setup {* Sign.add_const_constraint
- (@{const_name sfp}, SOME @{typ "'a::bifinite itself \<Rightarrow> sfp"}) *}
+ (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"}) *}
setup {* Sign.add_const_constraint
(@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
@@ -188,15 +188,15 @@
setup {* Sign.add_const_constraint
(@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
-lemma adm_mem_Collect_in_sfp: "adm (\<lambda>x. x \<in> {x. x ::: A})"
-unfolding mem_Collect_eq by (rule adm_in_sfp)
+lemma adm_mem_Collect_in_defl: "adm (\<lambda>x. x \<in> {x. x ::: A})"
+unfolding mem_Collect_eq by (rule adm_in_defl)
use "Tools/repdef.ML"
subsection {* Isomorphic deflations *}
definition
- isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
+ isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
where
"isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
@@ -222,12 +222,12 @@
using cast.below [of t "emb\<cdot>x"] by simp
qed
-lemma isodefl_ID_SFP: "isodefl (ID :: 'a \<rightarrow> 'a) SFP('a)"
-unfolding isodefl_def by (simp add: cast_SFP)
+lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
+unfolding isodefl_def by (simp add: cast_DEFL)
-lemma isodefl_SFP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) SFP('a) \<Longrightarrow> d = ID"
+lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
unfolding isodefl_def
-apply (simp add: cast_SFP)
+apply (simp add: cast_DEFL)
apply (simp add: expand_cfun_eq)
apply (rule allI)
apply (drule_tac x="emb\<cdot>x" in spec)
@@ -260,61 +260,61 @@
lemma isodefl_coerce:
fixes d :: "'a \<rightarrow> 'a"
- assumes SFP: "SFP('b) = SFP('a)"
+ assumes DEFL: "DEFL('b) = DEFL('a)"
shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
unfolding isodefl_def
apply (simp add: expand_cfun_eq)
-apply (simp add: emb_coerce coerce_prj SFP)
+apply (simp add: emb_coerce coerce_prj DEFL)
done
lemma isodefl_abs_rep:
fixes abs and rep and d
- assumes SFP: "SFP('b) = SFP('a)"
+ assumes DEFL: "DEFL('b) = DEFL('a)"
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
-unfolding abs_def rep_def using SFP by (rule isodefl_coerce)
+unfolding abs_def rep_def using DEFL by (rule isodefl_coerce)
lemma isodefl_cfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_sfp\<cdot>t1\<cdot>t2)"
+ isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_cfun_sfp cast_isodefl)
+apply (simp add: cast_cfun_defl cast_isodefl)
apply (simp add: emb_cfun_def prj_cfun_def)
apply (simp add: cfun_map_map cfcomp1)
done
lemma isodefl_ssum:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_sfp\<cdot>t1\<cdot>t2)"
+ isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_ssum_sfp cast_isodefl)
+apply (simp add: cast_ssum_defl cast_isodefl)
apply (simp add: emb_ssum_def prj_ssum_def)
apply (simp add: ssum_map_map isodefl_strict)
done
lemma isodefl_sprod:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_sfp\<cdot>t1\<cdot>t2)"
+ isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_sprod_sfp cast_isodefl)
+apply (simp add: cast_sprod_defl cast_isodefl)
apply (simp add: emb_sprod_def prj_sprod_def)
apply (simp add: sprod_map_map isodefl_strict)
done
lemma isodefl_cprod:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_sfp\<cdot>t1\<cdot>t2)"
+ isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_prod_sfp cast_isodefl)
+apply (simp add: cast_prod_defl cast_isodefl)
apply (simp add: emb_prod_def prj_prod_def)
apply (simp add: cprod_map_map cfcomp1)
done
lemma isodefl_u:
- "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_sfp\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_u_sfp cast_isodefl)
+apply (simp add: cast_u_defl cast_isodefl)
apply (simp add: emb_u_def prj_u_def)
apply (simp add: u_map_map)
done
@@ -325,19 +325,19 @@
setup {*
fold Domain_Isomorphism.add_type_constructor
- [(@{type_name cfun}, @{term cfun_sfp}, @{const_name cfun_map}, @{thm SFP_cfun},
+ [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun},
@{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
- (@{type_name ssum}, @{term ssum_sfp}, @{const_name ssum_map}, @{thm SFP_ssum},
+ (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum},
@{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
- (@{type_name sprod}, @{term sprod_sfp}, @{const_name sprod_map}, @{thm SFP_sprod},
+ (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod},
@{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
- (@{type_name prod}, @{term cprod_sfp}, @{const_name cprod_map}, @{thm SFP_prod},
+ (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod},
@{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
- (@{type_name "u"}, @{term u_sfp}, @{const_name u_map}, @{thm SFP_u},
+ (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u},
@{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
*}
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Oct 11 08:32:09 2010 -0700
@@ -48,7 +48,7 @@
structure DeflData = Theory_Data
(
- (* terms like "foo_sfp" *)
+ (* terms like "foo_defl" *)
type T = term Symtab.table;
val empty = Symtab.empty;
val extend = I;
@@ -57,7 +57,7 @@
structure RepData = Theory_Data
(
- (* theorems like "SFP('a foo) = foo_sfp$SFP('a)" *)
+ (* theorems like "DEFL('a foo) = foo_defl$DEFL('a)" *)
type T = thm list;
val empty = [];
val extend = I;
@@ -83,11 +83,11 @@
);
fun add_type_constructor
- (tname, defl_const, map_name, SFP_thm,
+ (tname, defl_const, map_name, DEFL_thm,
isodefl_thm, map_ID_thm, defl_map_thm) =
DeflData.map (Symtab.insert (K true) (tname, defl_const))
#> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
- #> RepData.map (Thm.add_thm SFP_thm)
+ #> RepData.map (Thm.add_thm DEFL_thm)
#> IsodeflData.map (Thm.add_thm isodefl_thm)
#> MapIdData.map (Thm.add_thm map_ID_thm);
@@ -104,19 +104,19 @@
infixr 6 ->>;
infix -->>;
-val sfpT = @{typ "sfp"};
+val deflT = @{typ "defl"};
fun mapT (T as Type (_, Ts)) =
(map (fn T => T ->> T) Ts) -->> (T ->> T)
| mapT T = T ->> T;
-fun mk_SFP T =
- Const (@{const_name sfp}, Term.itselfT T --> sfpT) $ Logic.mk_type T;
+fun mk_DEFL T =
+ Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T;
fun coerce_const T = Const (@{const_name coerce}, T);
fun isodefl_const T =
- Const (@{const_name isodefl}, (T ->> T) --> sfpT --> HOLogic.boolT);
+ Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
@@ -218,13 +218,13 @@
let
fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
| is_closed_typ _ = false;
- fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, sfpT)
+ fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
| defl_of (TVar _) = error ("defl_of_typ: TVar")
| defl_of (T as Type (c, Ts)) =
case Symtab.lookup tab c of
SOME t => list_ccomb (t, map defl_of Ts)
| NONE => if is_closed_typ T
- then mk_SFP T
+ then mk_DEFL T
else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
in defl_of T end;
@@ -443,7 +443,7 @@
(* declare deflation combinator constants *)
fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
let
- val defl_type = map (K sfpT) vs -->> sfpT;
+ val defl_type = map (K deflT) vs -->> deflT;
val defl_bind = Binding.suffix_name "_defl" tbind;
in
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
@@ -470,34 +470,34 @@
fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
let
fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
- val reps = map (mk_SFP o tfree) vs;
+ val reps = map (mk_DEFL o tfree) vs;
val defl = list_ccomb (defl_const, reps);
- val ((_, _, _, {SFP, ...}), thy) =
+ val ((_, _, _, {DEFL, ...}), thy) =
Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
in
- (SFP, thy)
+ (DEFL, thy)
end;
- val (SFP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
- val thy = RepData.map (fold Thm.add_thm SFP_thms) thy;
+ val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
+ val thy = RepData.map (fold Thm.add_thm DEFL_thms) thy;
- (* prove SFP equations *)
- fun mk_SFP_eq_thm (lhsT, rhsT) =
+ (* prove DEFL equations *)
+ fun mk_DEFL_eq_thm (lhsT, rhsT) =
let
- val goal = mk_eqs (mk_SFP lhsT, mk_SFP rhsT);
- val SFP_simps = RepData.get thy;
+ val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT);
+ val DEFL_simps = RepData.get thy;
val tac =
- rewrite_goals_tac (map mk_meta_eq SFP_simps)
+ rewrite_goals_tac (map mk_meta_eq DEFL_simps)
THEN resolve_tac defl_unfold_thms 1;
in
Goal.prove_global thy [] [] goal (K tac)
end;
- val SFP_eq_thms = map mk_SFP_eq_thm dom_eqns;
+ val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns;
- (* register SFP equations *)
- val SFP_eq_binds = map (Binding.prefix_name "SFP_eq_") dbinds;
+ (* register DEFL equations *)
+ val DEFL_eq_binds = map (Binding.prefix_name "DEFL_eq_") dbinds;
val (_, thy) = thy |>
(Global_Theory.add_thms o map Thm.no_attributes)
- (SFP_eq_binds ~~ SFP_eq_thms);
+ (DEFL_eq_binds ~~ DEFL_eq_thms);
(* define rep/abs functions *)
fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
@@ -516,10 +516,10 @@
|>> ListPair.unzip;
(* prove isomorphism and isodefl rules *)
- fun mk_iso_thms ((tbind, SFP_eq), (rep_def, abs_def)) thy =
+ fun mk_iso_thms ((tbind, DEFL_eq), (rep_def, abs_def)) thy =
let
fun make thm =
- Drule.zero_var_indexes (thm OF [SFP_eq, abs_def, rep_def]);
+ Drule.zero_var_indexes (thm OF [DEFL_eq, abs_def, rep_def]);
val rep_iso_thm = make @{thm domain_rep_iso};
val abs_iso_thm = make @{thm domain_abs_iso};
val isodefl_thm = make @{thm isodefl_abs_rep};
@@ -532,7 +532,7 @@
end;
val ((iso_thms, isodefl_abs_rep_thms), thy) =
thy
- |> fold_map mk_iso_thms (dbinds ~~ SFP_eq_thms ~~ rep_abs_defs)
+ |> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs)
|>> ListPair.unzip;
(* collect info about rep/abs *)
@@ -561,7 +561,7 @@
val isodefl_thm =
let
fun unprime a = Library.unprefix "'" a;
- fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), sfpT);
+ fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT);
fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T);
fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
fun mk_goal ((map_const, defl_const), (T, rhsT)) =
@@ -579,9 +579,9 @@
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
val bottom_rules =
@{thms fst_strict snd_strict isodefl_bottom simp_thms};
- val SFP_simps = map (fn th => th RS sym) (RepData.get thy);
+ val DEFL_simps = map (fn th => th RS sym) (RepData.get thy);
val isodefl_rules =
- @{thms conjI isodefl_ID_SFP}
+ @{thms conjI isodefl_ID_DEFL}
@ isodefl_abs_rep_thms
@ IsodeflData.get thy;
in
@@ -595,7 +595,7 @@
simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
simp_tac beta_ss 1,
simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
- simp_tac (HOL_basic_ss addsimps SFP_simps) 1,
+ simp_tac (HOL_basic_ss addsimps DEFL_simps) 1,
REPEAT (etac @{thm conjE} 1),
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
end;
@@ -613,23 +613,23 @@
(* prove map_ID theorems *)
fun prove_map_ID_thm
- (((map_const, (lhsT, _)), SFP_thm), isodefl_thm) =
+ (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) =
let
val Ts = snd (dest_Type lhsT);
val lhs = list_ccomb (map_const, map mk_ID Ts);
val goal = mk_eqs (lhs, mk_ID lhsT);
val tac = EVERY
- [rtac @{thm isodefl_SFP_imp_ID} 1,
- stac SFP_thm 1,
+ [rtac @{thm isodefl_DEFL_imp_ID} 1,
+ stac DEFL_thm 1,
rtac isodefl_thm 1,
- REPEAT (rtac @{thm isodefl_ID_SFP} 1)];
+ REPEAT (rtac @{thm isodefl_ID_DEFL} 1)];
in
Goal.prove_global thy [] [] goal (K tac)
end;
val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds;
val map_ID_thms =
map prove_map_ID_thm
- (map_consts ~~ dom_eqns ~~ SFP_thms ~~ isodefl_thms);
+ (map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms);
val (_, thy) = thy |>
(Global_Theory.add_thms o map Thm.no_attributes)
(map_ID_binds ~~ map_ID_thms);
--- a/src/HOLCF/Tools/repdef.ML Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML Mon Oct 11 08:32:09 2010 -0700
@@ -7,7 +7,7 @@
signature REPDEF =
sig
type rep_info =
- { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm }
+ { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm }
val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
term -> (binding * binding) option -> theory ->
@@ -28,19 +28,19 @@
(** type definitions **)
type rep_info =
- { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm };
+ { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm };
(* building types and terms *)
val udomT = @{typ udom};
-val sfpT = @{typ sfp};
+val deflT = @{typ defl};
fun emb_const T = Const (@{const_name emb}, T ->> udomT);
fun prj_const T = Const (@{const_name prj}, udomT ->> T);
-fun sfp_const T = Const (@{const_name sfp}, Term.itselfT T --> sfpT);
+fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT);
fun mk_cast (t, x) =
capply_const (udomT, udomT)
- $ (capply_const (sfpT, udomT ->> udomT) $ @{const cast} $ t)
+ $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
$ x;
(* manipulating theorems *)
@@ -70,8 +70,8 @@
val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
val deflT = Term.fastype_of defl;
- val _ = if deflT = @{typ "sfp"} then ()
- else error ("Not type sfp: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
+ val _ = if deflT = @{typ "defl"} then ()
+ else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
(*lhs*)
val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
@@ -84,12 +84,12 @@
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
(*set*)
- val in_defl = @{term "in_sfp :: udom => sfp => bool"};
+ val in_defl = @{term "in_defl :: udom => defl => bool"};
val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl);
(*pcpodef*)
- val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_sfp} 1;
- val tac2 = rtac @{thm adm_mem_Collect_in_sfp} 1;
+ val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_defl} 1;
+ val tac2 = rtac @{thm adm_mem_Collect_in_defl} 1;
val ((info, cpo_info, pcpo_info), thy) = thy
|> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
@@ -99,12 +99,12 @@
val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
- val sfp_eqn = Logic.mk_equals (sfp_const newT,
+ val defl_eqn = Logic.mk_equals (defl_const newT,
Abs ("x", Term.itselfT newT, defl));
val name_def = Binding.suffix_name "_def" name;
val emb_bind = (Binding.prefix_name "emb_" name_def, []);
val prj_bind = (Binding.prefix_name "prj_" name_def, []);
- val sfp_bind = (Binding.prefix_name "sfp_" name_def, []);
+ val defl_bind = (Binding.prefix_name "defl_" name_def, []);
(*instantiate class rep*)
val lthy = thy
@@ -113,34 +113,34 @@
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
val ((_, (_, prj_ldef)), lthy) =
Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
- val ((_, (_, sfp_ldef)), lthy) =
- Specification.definition (NONE, (sfp_bind, sfp_eqn)) lthy;
+ val ((_, (_, defl_ldef)), lthy) =
+ Specification.definition (NONE, (defl_bind, defl_eqn)) lthy;
val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
- val sfp_def = singleton (ProofContext.export lthy ctxt_thy) sfp_ldef;
+ val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef;
val type_definition_thm =
MetaSimplifier.rewrite_rule
(the_list (#set_def (#2 info)))
(#type_definition (#2 info));
val typedef_thms =
- [type_definition_thm, #below_def cpo_info, emb_def, prj_def, sfp_def];
+ [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def];
val thy = lthy
|> Class.prove_instantiation_instance
(K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
|> Local_Theory.exit_global;
(*other theorems*)
- val sfp_thm' = Thm.transfer thy sfp_def;
- val (SFP_thm, thy) = thy
+ val defl_thm' = Thm.transfer thy defl_def;
+ val (DEFL_thm, thy) = thy
|> Sign.add_path (Binding.name_of name)
|> Global_Theory.add_thm
- ((Binding.prefix_name "SFP_" name,
- Drule.zero_var_indexes (@{thm typedef_SFP} OF [sfp_thm'])), [])
+ ((Binding.prefix_name "DEFL_" name,
+ Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
||> Sign.restore_naming thy;
val rep_info =
- { emb_def = emb_def, prj_def = prj_def, sfp_def = sfp_def, SFP = SFP_thm };
+ { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, DEFL = DEFL_thm };
in
((info, cpo_info, pcpo_info, rep_info), thy)
end
--- a/src/HOLCF/UpperPD.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/UpperPD.thy Mon Oct 11 08:32:09 2010 -0700
@@ -447,14 +447,14 @@
by (intro finite_deflation_upper_map finite_deflation_udom_approx)
qed
-definition upper_sfp :: "sfp \<rightarrow> sfp"
-where "upper_sfp = sfp_fun1 upper_approx upper_map"
+definition upper_defl :: "defl \<rightarrow> defl"
+where "upper_defl = defl_fun1 upper_approx upper_map"
-lemma cast_upper_sfp:
- "cast\<cdot>(upper_sfp\<cdot>A) =
+lemma cast_upper_defl:
+ "cast\<cdot>(upper_defl\<cdot>A) =
udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
-unfolding upper_sfp_def
-apply (rule cast_sfp_fun1 [OF upper_approx])
+unfolding upper_defl_def
+apply (rule cast_defl_fun1 [OF upper_approx])
apply (erule finite_deflation_upper_map)
done
@@ -468,7 +468,7 @@
"prj = upper_map\<cdot>prj oo udom_prj upper_approx"
definition
- "sfp (t::'a upper_pd itself) = upper_sfp\<cdot>SFP('a)"
+ "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
@@ -476,15 +476,15 @@
using ep_pair_udom [OF upper_approx]
by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
next
- show "cast\<cdot>SFP('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
- unfolding emb_upper_pd_def prj_upper_pd_def sfp_upper_pd_def cast_upper_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq upper_map_map)
+ show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> '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 expand_cfun_eq upper_map_map)
qed
end
-lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\<cdot>SFP('a)"
-by (rule sfp_upper_pd_def)
+lemma DEFL_upper: "DEFL('a upper_pd) = upper_defl\<cdot>DEFL('a)"
+by (rule defl_upper_pd_def)
subsection {* Join *}
--- a/src/HOLCF/ex/Domain_Proofs.thy Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy Mon Oct 11 08:32:09 2010 -0700
@@ -28,50 +28,50 @@
text {* Start with the one-step non-recursive version *}
definition
- foo_bar_baz_sfpF ::
- "sfp \<rightarrow> sfp \<times> sfp \<times> sfp \<rightarrow> sfp \<times> sfp \<times> sfp"
+ foo_bar_baz_deflF ::
+ "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
where
- "foo_bar_baz_sfpF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3).
- ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>t2))
- , u_sfp\<cdot>(cfun_sfp\<cdot>t3\<cdot>SFP(tr))
- , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>t1)\<cdot>SFP(tr)))))"
+ "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))
+ , 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_sfpF_beta:
- "foo_bar_baz_sfpF\<cdot>a\<cdot>t =
- ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>(fst (snd t))))
- , u_sfp\<cdot>(cfun_sfp\<cdot>(snd (snd t))\<cdot>SFP(tr))
- , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(fst t))\<cdot>SFP(tr)))"
-unfolding foo_bar_baz_sfpF_def
+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))))
+ , 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
by (simp add: split_def)
text {* Individual type combinators are projected from the fixed point. *}
-definition foo_sfp :: "sfp \<rightarrow> sfp"
-where "foo_sfp = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
+definition foo_defl :: "defl \<rightarrow> defl"
+where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
-definition bar_sfp :: "sfp \<rightarrow> sfp"
-where "bar_sfp = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
+definition bar_defl :: "defl \<rightarrow> defl"
+where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
-definition baz_sfp :: "sfp \<rightarrow> sfp"
-where "baz_sfp = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
+definition baz_defl :: "defl \<rightarrow> defl"
+where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
lemma defl_apply_thms:
- "foo_sfp\<cdot>a = fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))"
- "bar_sfp\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
- "baz_sfp\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
-unfolding foo_sfp_def bar_sfp_def baz_sfp_def by simp_all
+ "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_sfp_unfold:
- "foo_sfp\<cdot>a = ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>(bar_sfp\<cdot>a)))"
-unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
+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)))"
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma bar_sfp_unfold: "bar_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(baz_sfp\<cdot>a)\<cdot>SFP(tr))"
-unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))"
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma baz_sfp_unfold: "baz_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(foo_sfp\<cdot>a))\<cdot>SFP(tr))"
-unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>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
how the fixrec package works."
@@ -82,14 +82,14 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "{x. x ::: foo_sfp\<cdot>SFP('a)}"
-by (simp_all add: adm_in_sfp)
+pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>DEFL('a)}"
+by (simp_all add: adm_in_defl)
-pcpodef (open) 'a bar = "{x. x ::: bar_sfp\<cdot>SFP('a)}"
-by (simp_all add: adm_in_sfp)
+pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>DEFL('a)}"
+by (simp_all add: adm_in_defl)
-pcpodef (open) 'a baz = "{x. x ::: baz_sfp\<cdot>SFP('a)}"
-by (simp_all add: adm_in_sfp)
+pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>DEFL('a)}"
+by (simp_all add: adm_in_defl)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
@@ -100,10 +100,10 @@
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_sfp\<cdot>SFP('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
-definition sfp_foo :: "'a foo itself \<Rightarrow> sfp"
-where "sfp_foo \<equiv> \<lambda>a. foo_sfp\<cdot>SFP('a)"
+definition defl_foo :: "'a foo itself \<Rightarrow> defl"
+where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
instance
apply (rule typedef_rep_class)
@@ -111,7 +111,7 @@
apply (rule below_foo_def)
apply (rule emb_foo_def)
apply (rule prj_foo_def)
-apply (rule sfp_foo_def)
+apply (rule defl_foo_def)
done
end
@@ -123,10 +123,10 @@
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_sfp\<cdot>SFP('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
-definition sfp_bar :: "'a bar itself \<Rightarrow> sfp"
-where "sfp_bar \<equiv> \<lambda>a. bar_sfp\<cdot>SFP('a)"
+definition defl_bar :: "'a bar itself \<Rightarrow> defl"
+where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
instance
apply (rule typedef_rep_class)
@@ -134,7 +134,7 @@
apply (rule below_bar_def)
apply (rule emb_bar_def)
apply (rule prj_bar_def)
-apply (rule sfp_bar_def)
+apply (rule defl_bar_def)
done
end
@@ -146,10 +146,10 @@
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_sfp\<cdot>SFP('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
-definition sfp_baz :: "'a baz itself \<Rightarrow> sfp"
-where "sfp_baz \<equiv> \<lambda>a. baz_sfp\<cdot>SFP('a)"
+definition defl_baz :: "'a baz itself \<Rightarrow> defl"
+where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
instance
apply (rule typedef_rep_class)
@@ -157,44 +157,44 @@
apply (rule below_baz_def)
apply (rule emb_baz_def)
apply (rule prj_baz_def)
-apply (rule sfp_baz_def)
+apply (rule defl_baz_def)
done
end
-text {* Prove SFP rules using lemma @{text typedef_SFP}. *}
+text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
-lemma SFP_foo: "SFP('a foo) = foo_sfp\<cdot>SFP('a)"
-apply (rule typedef_SFP)
-apply (rule sfp_foo_def)
+lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
+apply (rule typedef_DEFL)
+apply (rule defl_foo_def)
done
-lemma SFP_bar: "SFP('a bar) = bar_sfp\<cdot>SFP('a)"
-apply (rule typedef_SFP)
-apply (rule sfp_bar_def)
+lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
+apply (rule typedef_DEFL)
+apply (rule defl_bar_def)
done
-lemma SFP_baz: "SFP('a baz) = baz_sfp\<cdot>SFP('a)"
-apply (rule typedef_SFP)
-apply (rule sfp_baz_def)
+lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
+apply (rule typedef_DEFL)
+apply (rule defl_baz_def)
done
-text {* Prove SFP equations using type combinator unfold lemmas. *}
+text {* Prove DEFL equations using type combinator unfold lemmas. *}
-lemmas SFP_simps =
- SFP_ssum SFP_sprod SFP_u SFP_cfun
+lemmas DEFL_simps =
+ DEFL_ssum DEFL_sprod DEFL_u DEFL_cfun
-lemma SFP_foo': "SFP('a foo) = SFP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-unfolding SFP_foo SFP_bar SFP_baz SFP_simps
-by (rule foo_sfp_unfold)
+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
+by (rule foo_defl_unfold)
-lemma SFP_bar': "SFP('a bar) = SFP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding SFP_foo SFP_bar SFP_baz SFP_simps
-by (rule bar_sfp_unfold)
+lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
+unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
+by (rule bar_defl_unfold)
-lemma SFP_baz': "SFP('a baz) = SFP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding SFP_foo SFP_bar SFP_baz SFP_simps SFP_convex
-by (rule baz_sfp_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
+by (rule baz_defl_unfold)
(********************************************************************)
@@ -223,36 +223,36 @@
text {* Prove isomorphism rules. *}
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
-by (rule domain_abs_iso [OF SFP_foo' foo_abs_def foo_rep_def])
+by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
-by (rule domain_rep_iso [OF SFP_foo' foo_abs_def foo_rep_def])
+by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
-by (rule domain_abs_iso [OF SFP_bar' bar_abs_def bar_rep_def])
+by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
-by (rule domain_rep_iso [OF SFP_bar' bar_abs_def bar_rep_def])
+by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
-by (rule domain_abs_iso [OF SFP_baz' baz_abs_def baz_rep_def])
+by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
-by (rule domain_rep_iso [OF SFP_baz' baz_abs_def baz_rep_def])
+by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
text {* Prove isodefl rules using @{text isodefl_coerce}. *}
lemma isodefl_foo_abs:
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
-by (rule isodefl_abs_rep [OF SFP_foo' foo_abs_def foo_rep_def])
+by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
lemma isodefl_bar_abs:
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
-by (rule isodefl_abs_rep [OF SFP_bar' bar_abs_def bar_rep_def])
+by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
lemma isodefl_baz_abs:
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
-by (rule isodefl_abs_rep [OF SFP_baz' baz_abs_def baz_rep_def])
+by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
(********************************************************************)
@@ -316,15 +316,15 @@
lemma isodefl_foo_bar_baz:
assumes isodefl_d: "isodefl d t"
shows
- "isodefl (foo_map\<cdot>d) (foo_sfp\<cdot>t) \<and>
- isodefl (bar_map\<cdot>d) (bar_sfp\<cdot>t) \<and>
- isodefl (baz_map\<cdot>d) (baz_sfp\<cdot>t)"
+ "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)"
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)
apply (simp only: foo_bar_baz_mapF_beta
- foo_bar_baz_sfpF_beta
+ foo_bar_baz_deflF_beta
fst_conv snd_conv)
apply (elim conjE)
apply (intro
@@ -332,7 +332,7 @@
isodefl_foo_abs
isodefl_bar_abs
isodefl_baz_abs
- isodefl_ssum isodefl_sprod isodefl_ID_SFP
+ isodefl_ssum isodefl_sprod isodefl_ID_DEFL
isodefl_u isodefl_convex isodefl_cfun
isodefl_d
)
@@ -343,27 +343,27 @@
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
-text {* Prove map ID lemmas, using isodefl_SFP_imp_ID *}
+text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
lemma foo_map_ID: "foo_map\<cdot>ID = ID"
-apply (rule isodefl_SFP_imp_ID)
-apply (subst SFP_foo)
+apply (rule isodefl_DEFL_imp_ID)
+apply (subst DEFL_foo)
apply (rule isodefl_foo)
-apply (rule isodefl_ID_SFP)
+apply (rule isodefl_ID_DEFL)
done
lemma bar_map_ID: "bar_map\<cdot>ID = ID"
-apply (rule isodefl_SFP_imp_ID)
-apply (subst SFP_bar)
+apply (rule isodefl_DEFL_imp_ID)
+apply (subst DEFL_bar)
apply (rule isodefl_bar)
-apply (rule isodefl_ID_SFP)
+apply (rule isodefl_ID_DEFL)
done
lemma baz_map_ID: "baz_map\<cdot>ID = ID"
-apply (rule isodefl_SFP_imp_ID)
-apply (subst SFP_baz)
+apply (rule isodefl_DEFL_imp_ID)
+apply (subst DEFL_baz)
apply (rule isodefl_baz)
-apply (rule isodefl_ID_SFP)
+apply (rule isodefl_ID_DEFL)
done
(********************************************************************)