--- a/src/HOLCF/LowerPD.thy Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/LowerPD.thy Fri May 16 23:25:37 2008 +0200
@@ -103,13 +103,7 @@
done
lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
-by (rule Rep_lower_pd [simplified])
-
-lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
-unfolding less_lower_pd_def less_set_eq .
-
-
-subsection {* Principal ideals *}
+by (rule Rep_lower_pd [unfolded mem_Collect_eq])
definition
lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
@@ -123,7 +117,7 @@
done
interpretation lower_pd:
- bifinite_basis [lower_le approx_pd lower_principal Rep_lower_pd]
+ ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
apply unfold_locales
apply (rule approx_pd_lower_le)
apply (rule approx_pd_idem)
@@ -138,32 +132,25 @@
done
lemma lower_principal_less_iff [simp]:
- "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
-unfolding less_lower_pd_def Rep_lower_principal less_set_eq
-by (fast intro: lower_le_refl elim: lower_le_trans)
+ "lower_principal t \<sqsubseteq> lower_principal u \<longleftrightarrow> t \<le>\<flat> u"
+by (rule lower_pd.principal_less_iff)
+
+lemma lower_principal_eq_iff:
+ "lower_principal t = lower_principal u \<longleftrightarrow> t \<le>\<flat> u \<and> u \<le>\<flat> t"
+by (rule lower_pd.principal_eq_iff)
lemma lower_principal_mono:
"t \<le>\<flat> u \<Longrightarrow> lower_principal t \<sqsubseteq> lower_principal u"
-by (rule lower_principal_less_iff [THEN iffD2])
+by (rule lower_pd.principal_mono)
lemma compact_lower_principal: "compact (lower_principal t)"
-apply (rule compactI2)
-apply (simp add: less_lower_pd_def)
-apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
-apply (simp add: Rep_lower_principal set_cpo_simps)
-apply (simp add: subset_eq)
-apply (drule spec, drule mp, rule lower_le_refl)
-apply (erule exE, rename_tac i)
-apply (rule_tac x=i in exI)
-apply clarify
-apply (erule (1) lower_le.idealD3 [OF ideal_Rep_lower_pd])
-done
+by (rule lower_pd.compact_principal)
lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: lower_pd.principal_induct, simp, simp)
instance lower_pd :: (bifinite) pcpo
-by (intro_classes, fast intro: lower_pd_minimal)
+by intro_classes (fast intro: lower_pd_minimal)
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
by (rule lower_pd_minimal [THEN UU_I, symmetric])
@@ -174,51 +161,27 @@
instance lower_pd :: (profinite) approx ..
defs (overloaded)
- approx_lower_pd_def:
- "approx \<equiv> (\<lambda>n. lower_pd.basis_fun (\<lambda>t. lower_principal (approx_pd n t)))"
+ approx_lower_pd_def: "approx \<equiv> lower_pd.completion_approx"
+
+instance lower_pd :: (profinite) profinite
+apply (intro_classes, unfold approx_lower_pd_def)
+apply (simp add: lower_pd.chain_completion_approx)
+apply (rule lower_pd.lub_completion_approx)
+apply (rule lower_pd.completion_approx_idem)
+apply (rule lower_pd.finite_fixes_completion_approx)
+done
+
+instance lower_pd :: (bifinite) bifinite ..
lemma approx_lower_principal [simp]:
"approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)"
unfolding approx_lower_pd_def
-apply (rule lower_pd.basis_fun_principal)
-apply (erule lower_principal_mono [OF approx_pd_lower_mono])
-done
-
-lemma chain_approx_lower_pd:
- "chain (approx :: nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd)"
-unfolding approx_lower_pd_def
-by (rule lower_pd.chain_basis_fun_take)
-
-lemma lub_approx_lower_pd:
- "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a lower_pd)"
-unfolding approx_lower_pd_def
-by (rule lower_pd.lub_basis_fun_take)
-
-lemma approx_lower_pd_idem:
- "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, simp)
-apply (simp add: approx_pd_idem)
-done
+by (rule lower_pd.completion_approx_principal)
lemma approx_eq_lower_principal:
"\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
unfolding approx_lower_pd_def
-by (rule lower_pd.basis_fun_take_eq_principal)
-
-lemma finite_fixes_approx_lower_pd:
- "finite {xs::'a lower_pd. approx n\<cdot>xs = xs}"
-unfolding approx_lower_pd_def
-by (rule lower_pd.finite_fixes_basis_fun_take)
-
-instance lower_pd :: (profinite) profinite
-apply intro_classes
-apply (simp add: chain_approx_lower_pd)
-apply (rule lub_approx_lower_pd)
-apply (rule approx_lower_pd_idem)
-apply (rule finite_fixes_approx_lower_pd)
-done
-
-instance lower_pd :: (bifinite) bifinite ..
+by (rule lower_pd.completion_approx_eq_principal)
lemma compact_imp_lower_principal:
"compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
@@ -231,10 +194,7 @@
lemma lower_principal_induct:
"\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
-apply (erule approx_induct, rename_tac xs)
-apply (cut_tac n=n and xs=xs in approx_eq_lower_principal)
-apply (clarify, simp)
-done
+by (rule lower_pd.principal_induct)
lemma lower_principal_induct2:
"\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
@@ -247,54 +207,12 @@
done
-subsection {* Monadic unit *}
+subsection {* Monadic unit and plus *}
definition
lower_unit :: "'a \<rightarrow> 'a lower_pd" where
"lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
-lemma lower_unit_Rep_compact_basis [simp]:
- "lower_unit\<cdot>(Rep_compact_basis a) = lower_principal (PDUnit a)"
-unfolding lower_unit_def
-apply (rule compact_basis.basis_fun_principal)
-apply (rule lower_principal_mono)
-apply (erule PDUnit_lower_mono)
-done
-
-lemma lower_unit_strict [simp]: "lower_unit\<cdot>\<bottom> = \<bottom>"
-unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
-
-lemma approx_lower_unit [simp]:
- "approx n\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(approx n\<cdot>x)"
-apply (induct x rule: compact_basis_induct, simp)
-apply (simp add: approx_Rep_compact_basis)
-done
-
-lemma lower_unit_less_iff [simp]:
- "(lower_unit\<cdot>x \<sqsubseteq> lower_unit\<cdot>y) = (x \<sqsubseteq> y)"
- apply (rule iffI)
- apply (rule bifinite_less_ext)
- apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
- apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
- apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
- apply (clarify, simp add: compact_le_def)
- apply (erule monofun_cfun_arg)
-done
-
-lemma lower_unit_eq_iff [simp]:
- "(lower_unit\<cdot>x = lower_unit\<cdot>y) = (x = y)"
-unfolding po_eq_conv by simp
-
-lemma lower_unit_strict_iff [simp]: "(lower_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
-unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
-
-lemma compact_lower_unit_iff [simp]:
- "compact (lower_unit\<cdot>x) = compact x"
-unfolding bifinite_compact_iff by simp
-
-
-subsection {* Monadic plus *}
-
definition
lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
"lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
@@ -305,79 +223,89 @@
(infixl "+\<flat>" 65) where
"xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
+syntax
+ "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
+
+translations
+ "{x,xs}\<flat>" == "{x}\<flat> +\<flat> {xs}\<flat>"
+ "{x}\<flat>" == "CONST lower_unit\<cdot>x"
+
+lemma lower_unit_Rep_compact_basis [simp]:
+ "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
+unfolding lower_unit_def
+by (simp add: compact_basis.basis_fun_principal
+ lower_principal_mono PDUnit_lower_mono)
+
lemma lower_plus_principal [simp]:
- "lower_plus\<cdot>(lower_principal t)\<cdot>(lower_principal u) =
- lower_principal (PDPlus t u)"
+ "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
unfolding lower_plus_def
by (simp add: lower_pd.basis_fun_principal
lower_pd.basis_fun_mono PDPlus_lower_mono)
+lemma approx_lower_unit [simp]:
+ "approx n\<cdot>{x}\<flat> = {approx n\<cdot>x}\<flat>"
+apply (induct x rule: compact_basis_induct, simp)
+apply (simp add: approx_Rep_compact_basis)
+done
+
lemma approx_lower_plus [simp]:
- "approx n\<cdot>(lower_plus\<cdot>xs\<cdot>ys) = lower_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
+ "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
-lemma lower_plus_commute: "lower_plus\<cdot>xs\<cdot>ys = lower_plus\<cdot>ys\<cdot>xs"
-apply (induct xs ys rule: lower_principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
-
-lemma lower_plus_assoc:
- "lower_plus\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>zs = lower_plus\<cdot>xs\<cdot>(lower_plus\<cdot>ys\<cdot>zs)"
+lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
apply (induct xs ys arbitrary: zs rule: lower_principal_induct2, simp, simp)
apply (rule_tac xs=zs in lower_principal_induct, simp)
apply (simp add: PDPlus_assoc)
done
-lemma lower_plus_absorb: "lower_plus\<cdot>xs\<cdot>xs = xs"
+lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
+apply (induct xs ys rule: lower_principal_induct2, simp, simp)
+apply (simp add: PDPlus_commute)
+done
+
+lemma lower_plus_absorb: "xs +\<flat> xs = xs"
apply (induct xs rule: lower_principal_induct, simp)
apply (simp add: PDPlus_absorb)
done
-lemma lower_plus_less1: "xs \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
+interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
+ by unfold_locales
+ (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
+
+lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
+by (rule aci_lower_plus.mult_left_commute)
+
+lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
+by (rule aci_lower_plus.mult_left_idem)
+
+lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
+
+lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
apply (induct xs ys rule: lower_principal_induct2, simp, simp)
apply (simp add: PDPlus_lower_less)
done
-lemma lower_plus_less2: "ys \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
+lemma lower_plus_less2: "ys \<sqsubseteq> xs +\<flat> ys"
by (subst lower_plus_commute, rule lower_plus_less1)
-lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs"
+lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
apply (subst lower_plus_absorb [of zs, symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
lemma lower_plus_less_iff:
- "(lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs) = (xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs)"
+ "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
apply safe
apply (erule trans_less [OF lower_plus_less1])
apply (erule trans_less [OF lower_plus_less2])
apply (erule (1) lower_plus_least)
done
-lemma lower_plus_strict_iff [simp]:
- "(lower_plus\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<and> ys = \<bottom>)"
-apply safe
-apply (rule UU_I, erule subst, rule lower_plus_less1)
-apply (rule UU_I, erule subst, rule lower_plus_less2)
-apply (rule lower_plus_absorb)
-done
-
-lemma lower_plus_strict1 [simp]: "lower_plus\<cdot>\<bottom>\<cdot>ys = ys"
-apply (rule antisym_less [OF _ lower_plus_less2])
-apply (simp add: lower_plus_least)
-done
-
-lemma lower_plus_strict2 [simp]: "lower_plus\<cdot>xs\<cdot>\<bottom> = xs"
-apply (rule antisym_less [OF _ lower_plus_less1])
-apply (simp add: lower_plus_least)
-done
-
lemma lower_unit_less_plus_iff:
- "(lower_unit\<cdot>x \<sqsubseteq> lower_plus\<cdot>ys\<cdot>zs) =
- (lower_unit\<cdot>x \<sqsubseteq> ys \<or> lower_unit\<cdot>x \<sqsubseteq> zs)"
+ "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
apply (rule iffI)
apply (subgoal_tac
- "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
+ "adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)")
apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
@@ -391,19 +319,65 @@
apply (erule trans_less [OF _ lower_plus_less2])
done
+lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
+ apply (rule iffI)
+ apply (rule bifinite_less_ext)
+ apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
+ apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
+ apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
+ apply (clarify, simp add: compact_le_def)
+ apply (erule monofun_cfun_arg)
+done
+
lemmas lower_pd_less_simps =
lower_unit_less_iff
lower_plus_less_iff
lower_unit_less_plus_iff
+lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
+unfolding po_eq_conv by simp
+
+lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
+unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
+
+lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
+
+lemma lower_plus_strict_iff [simp]:
+ "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
+apply safe
+apply (rule UU_I, erule subst, rule lower_plus_less1)
+apply (rule UU_I, erule subst, rule lower_plus_less2)
+apply (rule lower_plus_absorb)
+done
+
+lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
+apply (rule antisym_less [OF _ lower_plus_less2])
+apply (simp add: lower_plus_least)
+done
+
+lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
+apply (rule antisym_less [OF _ lower_plus_less1])
+apply (simp add: lower_plus_least)
+done
+
+lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
+unfolding bifinite_compact_iff by simp
+
+lemma compact_lower_plus [simp]:
+ "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
+apply (drule compact_imp_lower_principal)+
+apply (auto simp add: compact_lower_principal)
+done
+
subsection {* Induction rules *}
lemma lower_pd_induct1:
assumes P: "adm P"
- assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
+ assumes unit: "\<And>x. P {x}\<flat>"
assumes insert:
- "\<And>x ys. \<lbrakk>P (lower_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>(lower_unit\<cdot>x)\<cdot>ys)"
+ "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
shows "P (xs::'a lower_pd)"
apply (induct xs rule: lower_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct1)
@@ -416,8 +390,8 @@
lemma lower_pd_induct:
assumes P: "adm P"
- assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
- assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>xs\<cdot>ys)"
+ assumes unit: "\<And>x. P {x}\<flat>"
+ assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
shows "P (xs::'a lower_pd)"
apply (induct xs rule: lower_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct)
@@ -433,9 +407,10 @@
"'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
"lower_bind_basis = fold_pd
(\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
- (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+ (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
-lemma ACI_lower_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_lower_bind:
+ "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
apply unfold_locales
apply (simp add: lower_plus_assoc)
apply (simp add: lower_plus_commute)
@@ -446,11 +421,11 @@
"lower_bind_basis (PDUnit a) =
(\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
"lower_bind_basis (PDPlus t u) =
- (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
+ (\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)"
unfolding lower_bind_basis_def
apply -
-apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_lower_bind])
-apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_lower_bind])
+apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
+apply (rule fold_pd_PDPlus [OF ACI_lower_bind])
done
lemma lower_bind_basis_mono:
@@ -474,12 +449,11 @@
done
lemma lower_bind_unit [simp]:
- "lower_bind\<cdot>(lower_unit\<cdot>x)\<cdot>f = f\<cdot>x"
+ "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x"
by (induct x rule: compact_basis_induct, simp, simp)
lemma lower_bind_plus [simp]:
- "lower_bind\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>f =
- lower_plus\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>(lower_bind\<cdot>ys\<cdot>f)"
+ "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -490,28 +464,26 @@
definition
lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
- "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_unit\<cdot>(f\<cdot>x)))"
+ "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<flat>))"
definition
lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where
"lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
lemma lower_map_unit [simp]:
- "lower_map\<cdot>f\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(f\<cdot>x)"
+ "lower_map\<cdot>f\<cdot>{x}\<flat> = {f\<cdot>x}\<flat>"
unfolding lower_map_def by simp
lemma lower_map_plus [simp]:
- "lower_map\<cdot>f\<cdot>(lower_plus\<cdot>xs\<cdot>ys) =
- lower_plus\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>(lower_map\<cdot>f\<cdot>ys)"
+ "lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
unfolding lower_map_def by simp
lemma lower_join_unit [simp]:
- "lower_join\<cdot>(lower_unit\<cdot>xs) = xs"
+ "lower_join\<cdot>{xs}\<flat> = xs"
unfolding lower_join_def by simp
lemma lower_join_plus [simp]:
- "lower_join\<cdot>(lower_plus\<cdot>xss\<cdot>yss) =
- lower_plus\<cdot>(lower_join\<cdot>xss)\<cdot>(lower_join\<cdot>yss)"
+ "lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
unfolding lower_join_def by simp
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"