--- a/src/HOL/HOLCF/Adm.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Adm.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,53 +5,51 @@
section \<open>Admissibility and compactness\<close>
theory Adm
-imports Cont
+ imports Cont
begin
default_sort cpo
subsection \<open>Definitions\<close>
-definition
- adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
- "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
+definition adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
+ where "adm P \<longleftrightarrow> (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
+
+lemma admI: "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
+ unfolding adm_def by fast
-lemma admI:
- "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
-unfolding adm_def by fast
+lemma admD: "adm P \<Longrightarrow> chain Y \<Longrightarrow> (\<And>i. P (Y i)) \<Longrightarrow> P (\<Squnion>i. Y i)"
+ unfolding adm_def by fast
-lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
-unfolding adm_def by fast
-
-lemma admD2: "\<lbrakk>adm (\<lambda>x. \<not> P x); chain Y; P (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. P (Y i)"
-unfolding adm_def by fast
+lemma admD2: "adm (\<lambda>x. \<not> P x) \<Longrightarrow> chain Y \<Longrightarrow> P (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. P (Y i)"
+ unfolding adm_def by fast
lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
-by (rule admI, erule spec)
+ by (rule admI) (erule spec)
+
subsection \<open>Admissibility on chain-finite types\<close>
text \<open>For chain-finite (easy) types every formula is admissible.\<close>
-lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
-by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
+lemma adm_chfin [simp]: "adm P"
+ for P :: "'a::chfin \<Rightarrow> bool"
+ by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
+
subsection \<open>Admissibility of special formulae and propagation\<close>
lemma adm_const [simp]: "adm (\<lambda>x. t)"
-by (rule admI, simp)
+ by (rule admI, simp)
-lemma adm_conj [simp]:
- "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
-by (fast intro: admI elim: admD)
+lemma adm_conj [simp]: "adm (\<lambda>x. P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
+ by (fast intro: admI elim: admD)
-lemma adm_all [simp]:
- "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
-by (fast intro: admI elim: admD)
+lemma adm_all [simp]: "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
+ by (fast intro: admI elim: admD)
-lemma adm_ball [simp]:
- "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
-by (fast intro: admI elim: admD)
+lemma adm_ball [simp]: "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
+ by (fast intro: admI elim: admD)
text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>
@@ -68,14 +66,14 @@
apply (rule chain_mono [OF chain])
apply (rule Least_le)
apply (rule LeastI2_ex)
- apply (simp_all add: P)
+ apply (simp_all add: P)
done
have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))"
using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))"
apply (rule below_antisym)
- apply (rule lub_mono [OF chain chain'])
- apply (rule chain_mono [OF chain f1])
+ apply (rule lub_mono [OF chain chain'])
+ apply (rule chain_mono [OF chain f1])
apply (rule lub_range_mono [OF _ chain chain'])
apply clarsimp
done
@@ -83,107 +81,95 @@
unfolding lub_eq using adm chain' f2 by (rule admD)
qed
-lemma adm_disj_lemma2:
- "\<forall>n::nat. P n \<or> Q n \<Longrightarrow> (\<forall>i. \<exists>j\<ge>i. P j) \<or> (\<forall>i. \<exists>j\<ge>i. Q j)"
-apply (erule contrapos_pp)
-apply (clarsimp, rename_tac a b)
-apply (rule_tac x="max a b" in exI)
-apply simp
-done
+lemma adm_disj_lemma2: "\<forall>n::nat. P n \<or> Q n \<Longrightarrow> (\<forall>i. \<exists>j\<ge>i. P j) \<or> (\<forall>i. \<exists>j\<ge>i. Q j)"
+ apply (erule contrapos_pp)
+ apply (clarsimp, rename_tac a b)
+ apply (rule_tac x="max a b" in exI)
+ apply simp
+ done
-lemma adm_disj [simp]:
- "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
-apply (rule admI)
-apply (erule adm_disj_lemma2 [THEN disjE])
-apply (erule (2) adm_disj_lemma1 [THEN disjI1])
-apply (erule (2) adm_disj_lemma1 [THEN disjI2])
-done
+lemma adm_disj [simp]: "adm (\<lambda>x. P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
+ apply (rule admI)
+ apply (erule adm_disj_lemma2 [THEN disjE])
+ apply (erule (2) adm_disj_lemma1 [THEN disjI1])
+ apply (erule (2) adm_disj_lemma1 [THEN disjI2])
+ done
-lemma adm_imp [simp]:
- "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
-by (subst imp_conv_disj, rule adm_disj)
+lemma adm_imp [simp]: "adm (\<lambda>x. \<not> P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
+ by (subst imp_conv_disj) (rule adm_disj)
-lemma adm_iff [simp]:
- "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>
- \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
-by (subst iff_conv_conj_imp, rule adm_conj)
+lemma adm_iff [simp]: "adm (\<lambda>x. P x \<longrightarrow> Q x) \<Longrightarrow> adm (\<lambda>x. Q x \<longrightarrow> P x) \<Longrightarrow> adm (\<lambda>x. P x \<longleftrightarrow> Q x)"
+ by (subst iff_conv_conj_imp) (rule adm_conj)
text \<open>admissibility and continuity\<close>
-lemma adm_below [simp]:
- "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
-by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
+lemma adm_below [simp]: "cont (\<lambda>x. u x) \<Longrightarrow> cont (\<lambda>x. v x) \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
+ by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
-lemma adm_eq [simp]:
- "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
-by (simp add: po_eq_conv)
+lemma adm_eq [simp]: "cont (\<lambda>x. u x) \<Longrightarrow> cont (\<lambda>x. v x) \<Longrightarrow> adm (\<lambda>x. u x = v x)"
+ by (simp add: po_eq_conv)
-lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
-by (simp add: adm_def cont2contlubE ch2ch_cont)
+lemma adm_subst: "cont (\<lambda>x. t x) \<Longrightarrow> adm P \<Longrightarrow> adm (\<lambda>x. P (t x))"
+ by (simp add: adm_def cont2contlubE ch2ch_cont)
lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
-by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
+ by (rule admI) (simp add: cont2contlubE ch2ch_cont lub_below_iff)
+
subsection \<open>Compactness\<close>
-definition
- compact :: "'a::cpo \<Rightarrow> bool" where
- "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
+definition compact :: "'a::cpo \<Rightarrow> bool"
+ where "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
-unfolding compact_def .
+ unfolding compact_def .
lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)"
-unfolding compact_def .
+ unfolding compact_def .
+
+lemma compactI2: "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
+ unfolding compact_def adm_def by fast
-lemma compactI2:
- "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
-unfolding compact_def adm_def by fast
+lemma compactD2: "compact x \<Longrightarrow> chain Y \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
+ unfolding compact_def adm_def by fast
-lemma compactD2:
- "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
-unfolding compact_def adm_def by fast
+lemma compact_below_lub_iff: "compact x \<Longrightarrow> chain Y \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
+ by (fast intro: compactD2 elim: below_lub)
-lemma compact_below_lub_iff:
- "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
-by (fast intro: compactD2 elim: below_lub)
-
-lemma compact_chfin [simp]: "compact (x::'a::chfin)"
-by (rule compactI [OF adm_chfin])
+lemma compact_chfin [simp]: "compact x"
+ for x :: "'a::chfin"
+ by (rule compactI [OF adm_chfin])
-lemma compact_imp_max_in_chain:
- "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
-apply (drule (1) compactD2, simp)
-apply (erule exE, rule_tac x=i in exI)
-apply (rule max_in_chainI)
-apply (rule below_antisym)
-apply (erule (1) chain_mono)
-apply (erule (1) below_trans [OF is_ub_thelub])
-done
+lemma compact_imp_max_in_chain: "chain Y \<Longrightarrow> compact (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. max_in_chain i Y"
+ apply (drule (1) compactD2, simp)
+ apply (erule exE, rule_tac x=i in exI)
+ apply (rule max_in_chainI)
+ apply (rule below_antisym)
+ apply (erule (1) chain_mono)
+ apply (erule (1) below_trans [OF is_ub_thelub])
+ done
text \<open>admissibility and compactness\<close>
lemma adm_compact_not_below [simp]:
- "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
-unfolding compact_def by (rule adm_subst)
+ "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
+ unfolding compact_def by (rule adm_subst)
-lemma adm_neq_compact [simp]:
- "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
-by (simp add: po_eq_conv)
+lemma adm_neq_compact [simp]: "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
+ by (simp add: po_eq_conv)
-lemma adm_compact_neq [simp]:
- "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
-by (simp add: po_eq_conv)
+lemma adm_compact_neq [simp]: "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
+ by (simp add: po_eq_conv)
lemma compact_bottom [simp, intro]: "compact \<bottom>"
-by (rule compactI, simp)
+ by (rule compactI) simp
text \<open>Any upward-closed predicate is admissible.\<close>
lemma adm_upward:
assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
shows "adm P"
-by (rule admI, drule spec, erule P, erule is_ub_thelub)
+ by (rule admI, drule spec, erule P, erule is_ub_thelub)
lemmas adm_lemmas =
adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
--- a/src/HOL/HOLCF/Bifinite.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,7 +5,7 @@
section \<open>Profinite and bifinite cpos\<close>
theory Bifinite
-imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
+ imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
begin
default_sort cpo
--- a/src/HOL/HOLCF/Cfun.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Mon Jan 01 23:07:24 2018 +0100
@@ -6,17 +6,18 @@
section \<open>The type of continuous functions\<close>
theory Cfun
-imports Cpodef Fun_Cpo Product_Cpo
+ imports Cpodef Fun_Cpo Product_Cpo
begin
default_sort cpo
+
subsection \<open>Definition of continuous function type\<close>
-definition "cfun = {f::'a => 'b. cont f}"
+definition "cfun = {f::'a \<Rightarrow> 'b. cont f}"
-cpodef ('a, 'b) cfun ("(_ \<rightarrow>/ _)" [1, 0] 0) = "cfun :: ('a => 'b) set"
- unfolding cfun_def by (auto intro: cont_const adm_cont)
+cpodef ('a, 'b) cfun ("(_ \<rightarrow>/ _)" [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set"
+ by (auto simp: cfun_def intro: cont_const adm_cont)
type_notation (ASCII)
cfun (infixr "->" 0)
@@ -78,18 +79,19 @@
text \<open>Dummy patterns for continuous abstraction\<close>
translations
- "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
+ "\<Lambda> _. t" \<rightharpoonup> "CONST Abs_cfun (\<lambda>_. t)"
+
subsection \<open>Continuous function space is pointed\<close>
lemma bottom_cfun: "\<bottom> \<in> cfun"
-by (simp add: cfun_def inst_fun_pcpo)
+ by (simp add: cfun_def inst_fun_pcpo)
instance cfun :: (cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
+ by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
instance cfun :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun])
+ by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun])
lemmas Rep_cfun_strict =
typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
@@ -100,30 +102,32 @@
text \<open>function application is strict in its first argument\<close>
lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
-by (simp add: Rep_cfun_strict)
+ by (simp add: Rep_cfun_strict)
lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
-by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)
+ by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)
text \<open>for compatibility with old HOLCF-Version\<close>
lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
-by simp
+ by simp
+
subsection \<open>Basic properties of continuous functions\<close>
text \<open>Beta-equality for continuous functions\<close>
lemma Abs_cfun_inverse2: "cont f \<Longrightarrow> Rep_cfun (Abs_cfun f) = f"
-by (simp add: Abs_cfun_inverse cfun_def)
+ by (simp add: Abs_cfun_inverse cfun_def)
lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
-by (simp add: Abs_cfun_inverse2)
+ by (simp add: Abs_cfun_inverse2)
-text \<open>Beta-reduction simproc\<close>
+
+subsubsection \<open>Beta-reduction simproc\<close>
text \<open>
Given the term @{term "(\<Lambda> x. f x)\<cdot>y"}, the procedure tries to
- construct the theorem @{term "(\<Lambda> x. f x)\<cdot>y == f y"}. If this
+ construct the theorem @{term "(\<Lambda> x. f x)\<cdot>y \<equiv> f y"}. If this
theorem cannot be completely solved by the cont2cont rules, then
the procedure returns the ordinary conditional \<open>beta_cfun\<close>
rule.
@@ -140,12 +144,10 @@
simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open>
fn phi => fn ctxt => fn ct =>
let
- val dest = Thm.dest_comb;
- val f = (snd o dest o snd o dest) ct;
+ val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct)));
val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
- val tr = Thm.instantiate' [SOME T, SOME U] [SOME f]
- (mk_meta_eq @{thm Abs_cfun_inverse2});
- val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
+ val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2});
+ val rules = Named_Theorems.get ctxt \<^named_theorems>\<open>cont2cont\<close>;
val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
in SOME (perhaps (SINGLE (tac 1)) tr) end
\<close>
@@ -153,44 +155,43 @@
text \<open>Eta-equality for continuous functions\<close>
lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"
-by (rule Rep_cfun_inverse)
+ by (rule Rep_cfun_inverse)
text \<open>Extensionality for continuous functions\<close>
lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
-by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)
+ by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)
lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
-by (simp add: cfun_eq_iff)
+ by (simp add: cfun_eq_iff)
text \<open>Extensionality wrt. ordering for continuous functions\<close>
-lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)"
-by (simp add: below_cfun_def fun_below_iff)
+lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)"
+ by (simp add: below_cfun_def fun_below_iff)
lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: cfun_below_iff)
+ by (simp add: cfun_below_iff)
text \<open>Congruence for continuous function application\<close>
-lemma cfun_cong: "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f\<cdot>x = g\<cdot>y"
-by simp
+lemma cfun_cong: "f = g \<Longrightarrow> x = y \<Longrightarrow> f\<cdot>x = g\<cdot>y"
+ by simp
lemma cfun_fun_cong: "f = g \<Longrightarrow> f\<cdot>x = g\<cdot>x"
-by simp
+ by simp
lemma cfun_arg_cong: "x = y \<Longrightarrow> f\<cdot>x = f\<cdot>y"
-by simp
+ by simp
+
subsection \<open>Continuity of application\<close>
lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
-by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun])
+ by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun])
lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
-apply (cut_tac x=f in Rep_cfun)
-apply (simp add: cfun_def)
-done
+ using Rep_cfun [where x = f] by (simp add: cfun_def)
lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
@@ -200,66 +201,66 @@
text \<open>contlub, cont properties of @{term Rep_cfun} in each argument\<close>
lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
-by (rule cont_Rep_cfun2 [THEN cont2contlubE])
+ by (rule cont_Rep_cfun2 [THEN cont2contlubE])
lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
-by (rule cont_Rep_cfun1 [THEN cont2contlubE])
+ by (rule cont_Rep_cfun1 [THEN cont2contlubE])
text \<open>monotonicity of application\<close>
lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
-by (simp add: cfun_below_iff)
+ by (simp add: cfun_below_iff)
lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
-by (rule monofun_Rep_cfun2 [THEN monofunE])
+ by (rule monofun_Rep_cfun2 [THEN monofunE])
-lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
-by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
+lemma monofun_cfun: "f \<sqsubseteq> g \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
+ by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
-text \<open>ch2ch - rules for the type @{typ "'a -> 'b"}\<close>
+text \<open>ch2ch - rules for the type @{typ "'a \<rightarrow> 'b"}\<close>
lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])
+ by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])
lemma ch2ch_Rep_cfunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun])
+ by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun])
lemma ch2ch_Rep_cfunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
-by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun])
+ by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun])
-lemma ch2ch_Rep_cfun [simp]:
- "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
-by (simp add: chain_def monofun_cfun)
+lemma ch2ch_Rep_cfun [simp]: "chain F \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
+ by (simp add: chain_def monofun_cfun)
lemma ch2ch_LAM [simp]:
- "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
-by (simp add: chain_def cfun_below_iff)
+ "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> (\<And>i. cont (\<lambda>x. S i x)) \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
+ by (simp add: chain_def cfun_below_iff)
text \<open>contlub, cont properties of @{term Rep_cfun} in both arguments\<close>
-lemma lub_APP:
- "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
-by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
+lemma lub_APP: "chain F \<Longrightarrow> chain Y \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
+ by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
lemma lub_LAM:
- "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
-by (simp add: lub_cfun lub_fun ch2ch_lambda)
+ assumes "\<And>x. chain (\<lambda>i. F i x)"
+ and "\<And>i. cont (\<lambda>x. F i x)"
+ shows "(\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
+ using assms by (simp add: lub_cfun lub_fun ch2ch_lambda)
lemmas lub_distribs = lub_APP lub_LAM
text \<open>strictness\<close>
lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
-apply (rule bottomI)
-apply (erule subst)
-apply (rule minimal [THEN monofun_cfun_arg])
-done
+ apply (rule bottomI)
+ apply (erule subst)
+ apply (rule minimal [THEN monofun_cfun_arg])
+ done
-text \<open>type @{typ "'a -> 'b"} is chain complete\<close>
+text \<open>type @{typ "'a \<rightarrow> 'b"} is chain complete\<close>
lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
-by (simp add: lub_cfun lub_fun ch2ch_lambda)
+ by (simp add: lub_cfun lub_fun ch2ch_lambda)
+
subsection \<open>Continuity simplification procedure\<close>
@@ -270,10 +271,10 @@
assumes t: "cont (\<lambda>x. t x)"
shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
proof -
- have 1: "\<And>y. cont (\<lambda>x. (f x)\<cdot>y)"
- using cont_Rep_cfun1 f by (rule cont_compose)
- show "cont (\<lambda>x. (f x)\<cdot>(t x))"
- using t cont_Rep_cfun2 1 by (rule cont_apply)
+ from cont_Rep_cfun1 f have "cont (\<lambda>x. (f x)\<cdot>y)" for y
+ by (rule cont_compose)
+ with t cont_Rep_cfun2 show "cont (\<lambda>x. (f x)\<cdot>(t x))"
+ by (rule cont_apply)
qed
text \<open>
@@ -281,21 +282,21 @@
These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
\<close>
-lemma cont_APP_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_APP [THEN cont2cont_fun])
+lemma cont_APP_app [simp]: "cont f \<Longrightarrow> cont g \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
+ by (rule cont2cont_APP [THEN cont2cont_fun])
-lemma cont_APP_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
-by (rule cont_APP_app [THEN cont2cont_fun])
+lemma cont_APP_app_app [simp]: "cont f \<Longrightarrow> cont g \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
+ by (rule cont_APP_app [THEN cont2cont_fun])
-text \<open>cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"}\<close>
+text \<open>cont2mono Lemma for @{term "\<lambda>x. LAM y. c1(x)(y)"}\<close>
lemma cont2mono_LAM:
"\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
\<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
- unfolding monofun_def cfun_below_iff by simp
+ by (simp add: monofun_def cfun_below_iff)
-text \<open>cont2cont Lemma for @{term "%x. LAM y. f x y"}\<close>
+text \<open>cont2cont Lemma for @{term "\<lambda>x. LAM y. f x y"}\<close>
text \<open>
Not suitable as a cont2cont rule, because on nested lambdas
@@ -307,9 +308,10 @@
assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
proof (rule cont_Abs_cfun)
- fix x
- from f1 show "f x \<in> cfun" by (simp add: cfun_def)
- from f2 show "cont f" by (rule cont2cont_lambda)
+ from f1 show "f x \<in> cfun" for x
+ by (simp add: cfun_def)
+ from f2 show "cont f"
+ by (rule cont2cont_lambda)
qed
text \<open>
@@ -321,176 +323,173 @@
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
-using assms by (simp add: cont2cont_LAM prod_cont_iff)
+ using assms by (simp add: cont2cont_LAM prod_cont_iff)
lemma cont2cont_LAM_discrete [simp, cont2cont]:
"(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
-by (simp add: cont2cont_LAM)
+ by (simp add: cont2cont_LAM)
+
subsection \<open>Miscellaneous\<close>
text \<open>Monotonicity of @{term Abs_cfun}\<close>
-lemma monofun_LAM:
- "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
-by (simp add: cfun_below_iff)
+lemma monofun_LAM: "cont f \<Longrightarrow> cont g \<Longrightarrow> (\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
+ by (simp add: cfun_below_iff)
text \<open>some lemmata for functions with flat/chfin domain/range types\<close>
-lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)
- ==> !s. ? n. (LUB i. Y i)\<cdot>s = Y n\<cdot>s"
-apply (rule allI)
-apply (subst contlub_cfun_fun)
-apply assumption
-apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
-done
+lemma chfin_Rep_cfunR: "chain Y \<Longrightarrow> \<forall>s. \<exists>n. (LUB i. Y i)\<cdot>s = Y n\<cdot>s"
+ for Y :: "nat \<Rightarrow> 'a::cpo \<rightarrow> 'b::chfin"
+ apply (rule allI)
+ apply (subst contlub_cfun_fun)
+ apply assumption
+ apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
+ done
lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
-by (rule adm_subst, simp, rule adm_chfin)
+ by (rule adm_subst, simp, rule adm_chfin)
+
subsection \<open>Continuous injection-retraction pairs\<close>
text \<open>Continuous retractions are strict.\<close>
-lemma retraction_strict:
- "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
-apply (rule bottomI)
-apply (drule_tac x="\<bottom>" in spec)
-apply (erule subst)
-apply (rule monofun_cfun_arg)
-apply (rule minimal)
-done
+lemma retraction_strict: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
+ apply (rule bottomI)
+ apply (drule_tac x="\<bottom>" in spec)
+ apply (erule subst)
+ apply (rule monofun_cfun_arg)
+ apply (rule minimal)
+ done
-lemma injection_eq:
- "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x = g\<cdot>y) = (x = y)"
-apply (rule iffI)
-apply (drule_tac f=f in cfun_arg_cong)
-apply simp
-apply simp
-done
+lemma injection_eq: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x = g\<cdot>y) = (x = y)"
+ apply (rule iffI)
+ apply (drule_tac f=f in cfun_arg_cong)
+ apply simp
+ apply simp
+ done
-lemma injection_below:
- "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)"
-apply (rule iffI)
-apply (drule_tac f=f in monofun_cfun_arg)
-apply simp
-apply (erule monofun_cfun_arg)
-done
+lemma injection_below: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)"
+ apply (rule iffI)
+ apply (drule_tac f=f in monofun_cfun_arg)
+ apply simp
+ apply (erule monofun_cfun_arg)
+ done
-lemma injection_defined_rev:
- "\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; g\<cdot>z = \<bottom>\<rbrakk> \<Longrightarrow> z = \<bottom>"
-apply (drule_tac f=f in cfun_arg_cong)
-apply (simp add: retraction_strict)
-done
+lemma injection_defined_rev: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> g\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
+ apply (drule_tac f=f in cfun_arg_cong)
+ apply (simp add: retraction_strict)
+ done
-lemma injection_defined:
- "\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; z \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> g\<cdot>z \<noteq> \<bottom>"
-by (erule contrapos_nn, rule injection_defined_rev)
+lemma injection_defined: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> z \<noteq> \<bottom> \<Longrightarrow> g\<cdot>z \<noteq> \<bottom>"
+ by (erule contrapos_nn, rule injection_defined_rev)
+
text \<open>a result about functions with flat codomain\<close>
-lemma flat_eqI: "\<lbrakk>(x::'a::flat) \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> x = y"
-by (drule ax_flat, simp)
+lemma flat_eqI: "x \<sqsubseteq> y \<Longrightarrow> x \<noteq> \<bottom> \<Longrightarrow> x = y"
+ for x y :: "'a::flat"
+ by (drule ax_flat) simp
-lemma flat_codom:
- "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
-apply (case_tac "f\<cdot>x = \<bottom>")
-apply (rule disjI1)
-apply (rule bottomI)
-apply (erule_tac t="\<bottom>" in subst)
-apply (rule minimal [THEN monofun_cfun_arg])
-apply clarify
-apply (rule_tac a = "f\<cdot>\<bottom>" in refl [THEN box_equals])
-apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
-apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
-done
+lemma flat_codom: "f\<cdot>x = c \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
+ for c :: "'b::flat"
+ apply (case_tac "f\<cdot>x = \<bottom>")
+ apply (rule disjI1)
+ apply (rule bottomI)
+ apply (erule_tac t="\<bottom>" in subst)
+ apply (rule minimal [THEN monofun_cfun_arg])
+ apply clarify
+ apply (rule_tac a = "f\<cdot>\<bottom>" in refl [THEN box_equals])
+ apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
+ apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
+ done
+
subsection \<open>Identity and composition\<close>
-definition
- ID :: "'a \<rightarrow> 'a" where
- "ID = (\<Lambda> x. x)"
+definition ID :: "'a \<rightarrow> 'a"
+ where "ID = (\<Lambda> x. x)"
-definition
- cfcomp :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c" where
- oo_def: "cfcomp = (\<Lambda> f g x. f\<cdot>(g\<cdot>x))"
+definition cfcomp :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"
+ where oo_def: "cfcomp = (\<Lambda> f g x. f\<cdot>(g\<cdot>x))"
-abbreviation
- cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100) where
- "f oo g == cfcomp\<cdot>f\<cdot>g"
+abbreviation cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100)
+ where "f oo g == cfcomp\<cdot>f\<cdot>g"
lemma ID1 [simp]: "ID\<cdot>x = x"
-by (simp add: ID_def)
+ by (simp add: ID_def)
lemma cfcomp1: "(f oo g) = (\<Lambda> x. f\<cdot>(g\<cdot>x))"
-by (simp add: oo_def)
+ by (simp add: oo_def)
lemma cfcomp2 [simp]: "(f oo g)\<cdot>x = f\<cdot>(g\<cdot>x)"
-by (simp add: cfcomp1)
+ by (simp add: cfcomp1)
lemma cfcomp_LAM: "cont g \<Longrightarrow> f oo (\<Lambda> x. g x) = (\<Lambda> x. f\<cdot>(g x))"
-by (simp add: cfcomp1)
+ by (simp add: cfcomp1)
lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>"
-by (simp add: cfun_eq_iff)
+ by (simp add: cfun_eq_iff)
text \<open>
- Show that interpretation of (pcpo,\<open>_->_\<close>) is a category.
- The class of objects is interpretation of syntactical class pcpo.
- The class of arrows between objects @{typ 'a} and @{typ 'b} is interpret. of @{typ "'a -> 'b"}.
- The identity arrow is interpretation of @{term ID}.
- The composition of f and g is interpretation of \<open>oo\<close>.
+ Show that interpretation of (pcpo, \<open>_\<rightarrow>_\<close>) is a category.
+ \<^item> The class of objects is interpretation of syntactical class pcpo.
+ \<^item> The class of arrows between objects @{typ 'a} and @{typ 'b} is interpret. of @{typ "'a \<rightarrow> 'b"}.
+ \<^item> The identity arrow is interpretation of @{term ID}.
+ \<^item> The composition of f and g is interpretation of \<open>oo\<close>.
\<close>
lemma ID2 [simp]: "f oo ID = f"
-by (rule cfun_eqI, simp)
+ by (rule cfun_eqI, simp)
lemma ID3 [simp]: "ID oo f = f"
-by (rule cfun_eqI, simp)
+ by (rule cfun_eqI) simp
lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
-by (rule cfun_eqI, simp)
+ by (rule cfun_eqI) simp
+
subsection \<open>Strictified functions\<close>
default_sort pcpo
-definition
- seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
- "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
+definition seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
+ where "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
lemma cont2cont_if_bottom [cont2cont, simp]:
- assumes f: "cont (\<lambda>x. f x)" and g: "cont (\<lambda>x. g x)"
+ assumes f: "cont (\<lambda>x. f x)"
+ and g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. if f x = \<bottom> then \<bottom> else g x)"
proof (rule cont_apply [OF f])
- show "\<And>x. cont (\<lambda>y. if y = \<bottom> then \<bottom> else g x)"
+ show "cont (\<lambda>y. if y = \<bottom> then \<bottom> else g x)" for x
unfolding cont_def is_lub_def is_ub_def ball_simps
by (simp add: lub_eq_bottom_iff)
- show "\<And>y. cont (\<lambda>x. if y = \<bottom> then \<bottom> else g x)"
+ show "cont (\<lambda>x. if y = \<bottom> then \<bottom> else g x)" for y
by (simp add: g)
qed
lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
-unfolding seq_def by simp
+ by (simp add: seq_def)
lemma seq_simps [simp]:
"seq\<cdot>\<bottom> = \<bottom>"
"seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
"x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
-by (simp_all add: seq_conv_if)
+ by (simp_all add: seq_conv_if)
-definition
- strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
- "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))"
+definition strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b"
+ where "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))"
lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
-unfolding strictify_def by simp
+ by (simp add: strictify_def)
lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by (simp add: strictify_conv_if)
+ by (simp add: strictify_conv_if)
lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
-by (simp add: strictify_conv_if)
+ by (simp add: strictify_conv_if)
+
subsection \<open>Continuity of let-bindings\<close>
@@ -499,19 +498,18 @@
assumes g1: "\<And>y. cont (\<lambda>x. g x y)"
assumes g2: "\<And>x. cont (\<lambda>y. g x y)"
shows "cont (\<lambda>x. let y = f x in g x y)"
-unfolding Let_def using f g2 g1 by (rule cont_apply)
+ unfolding Let_def using f g2 g1 by (rule cont_apply)
lemma cont2cont_Let' [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
shows "cont (\<lambda>x. let y = f x in g x y)"
-using f
+ using f
proof (rule cont2cont_Let)
- fix x show "cont (\<lambda>y. g x y)"
- using g by (simp add: prod_cont_iff)
-next
- fix y show "cont (\<lambda>x. g x y)"
- using g by (simp add: prod_cont_iff)
+ from g show "cont (\<lambda>y. g x y)" for x
+ by (simp add: prod_cont_iff)
+ from g show "cont (\<lambda>x. g x y)" for y
+ by (simp add: prod_cont_iff)
qed
text \<open>The simple version (suggested by Joachim Breitner) is needed if
@@ -520,6 +518,6 @@
lemma cont2cont_Let_simple [simp, cont2cont]:
assumes "\<And>y. cont (\<lambda>x. g x y)"
shows "cont (\<lambda>x. let y = t in g x y)"
-unfolding Let_def using assms .
+ unfolding Let_def using assms .
end
--- a/src/HOL/HOLCF/Cont.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Cont.thy Mon Jan 01 23:07:24 2018 +0100
@@ -6,7 +6,7 @@
section \<open>Continuity and monotonicity\<close>
theory Cont
-imports Pcpo
+ imports Pcpo
begin
text \<open>
@@ -18,71 +18,62 @@
subsection \<open>Definitions\<close>
-definition
- monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" \<comment> "monotonicity" where
- "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+definition monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" \<comment> "monotonicity"
+ where "monofun f \<longleftrightarrow> (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
-definition
- cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
-where
- "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
+definition cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
+ where "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
+
+lemma contI: "(\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)) \<Longrightarrow> cont f"
+ by (simp add: cont_def)
-lemma contI:
- "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> cont f"
-by (simp add: cont_def)
-
-lemma contE:
- "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
-by (simp add: cont_def)
+lemma contE: "cont f \<Longrightarrow> chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
+ by (simp add: cont_def)
-lemma monofunI:
- "\<lbrakk>\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y\<rbrakk> \<Longrightarrow> monofun f"
-by (simp add: monofun_def)
+lemma monofunI: "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> monofun f"
+ by (simp add: monofun_def)
-lemma monofunE:
- "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
-by (simp add: monofun_def)
+lemma monofunE: "monofun f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+ by (simp add: monofun_def)
subsection \<open>Equivalence of alternate definition\<close>
text \<open>monotone functions map chains to chains\<close>
-lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))"
-apply (rule chainI)
-apply (erule monofunE)
-apply (erule chainE)
-done
+lemma ch2ch_monofun: "monofun f \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. f (Y i))"
+ apply (rule chainI)
+ apply (erule monofunE)
+ apply (erule chainE)
+ done
text \<open>monotone functions map upper bound to upper bounds\<close>
-lemma ub2ub_monofun:
- "\<lbrakk>monofun f; range Y <| u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u"
-apply (rule ub_rangeI)
-apply (erule monofunE)
-apply (erule ub_rangeD)
-done
+lemma ub2ub_monofun: "monofun f \<Longrightarrow> range Y <| u \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u"
+ apply (rule ub_rangeI)
+ apply (erule monofunE)
+ apply (erule ub_rangeD)
+ done
text \<open>a lemma about binary chains\<close>
-lemma binchain_cont:
- "\<lbrakk>cont f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y"
-apply (subgoal_tac "f (\<Squnion>i::nat. if i = 0 then x else y) = f y")
-apply (erule subst)
-apply (erule contE)
-apply (erule bin_chain)
-apply (rule_tac f=f in arg_cong)
-apply (erule is_lub_bin_chain [THEN lub_eqI])
-done
+lemma binchain_cont: "cont f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y"
+ apply (subgoal_tac "f (\<Squnion>i::nat. if i = 0 then x else y) = f y")
+ apply (erule subst)
+ apply (erule contE)
+ apply (erule bin_chain)
+ apply (rule_tac f=f in arg_cong)
+ apply (erule is_lub_bin_chain [THEN lub_eqI])
+ done
text \<open>continuity implies monotonicity\<close>
lemma cont2mono: "cont f \<Longrightarrow> monofun f"
-apply (rule monofunI)
-apply (drule (1) binchain_cont)
-apply (drule_tac i=0 in is_lub_rangeD1)
-apply simp
-done
+ apply (rule monofunI)
+ apply (drule (1) binchain_cont)
+ apply (drule_tac i=0 in is_lub_rangeD1)
+ apply simp
+ done
lemmas cont2monofunE = cont2mono [THEN monofunE]
@@ -90,17 +81,15 @@
text \<open>continuity implies preservation of lubs\<close>
-lemma cont2contlubE:
- "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
-apply (rule lub_eqI [symmetric])
-apply (erule (1) contE)
-done
+lemma cont2contlubE: "cont f \<Longrightarrow> chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
+ apply (rule lub_eqI [symmetric])
+ apply (erule (1) contE)
+ done
lemma contI2:
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes mono: "monofun f"
- assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
- \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
+ assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
shows "cont f"
proof (rule contI)
fix Y :: "nat \<Rightarrow> 'a"
@@ -109,15 +98,16 @@
by (rule ch2ch_monofun)
have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)"
apply (rule below_antisym)
- apply (rule lub_below [OF fY])
- apply (rule monofunE [OF mono])
- apply (rule is_ub_thelub [OF Y])
+ apply (rule lub_below [OF fY])
+ apply (rule monofunE [OF mono])
+ apply (rule is_ub_thelub [OF Y])
apply (rule below [OF Y fY])
done
with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
by (rule thelubE)
qed
+
subsection \<open>Collection of continuity rules\<close>
named_theorems cont2cont "continuity intro rule"
@@ -128,9 +118,9 @@
text \<open>The identity function is continuous\<close>
lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)"
-apply (rule contI)
-apply (erule cpo_lubI)
-done
+ apply (rule contI)
+ apply (erule cpo_lubI)
+ done
text \<open>constant functions are continuous\<close>
@@ -146,87 +136,88 @@
assumes 3: "\<And>y. cont (\<lambda>x. f x y)"
shows "cont (\<lambda>x. (f x) (t x))"
proof (rule contI2 [OF monofunI])
- fix x y :: "'a" assume "x \<sqsubseteq> y"
+ fix x y :: "'a"
+ assume "x \<sqsubseteq> y"
then show "f x (t x) \<sqsubseteq> f y (t y)"
by (auto intro: cont2monofunE [OF 1]
- cont2monofunE [OF 2]
- cont2monofunE [OF 3]
- below_trans)
+ cont2monofunE [OF 2]
+ cont2monofunE [OF 3]
+ below_trans)
next
- fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
+ fix Y :: "nat \<Rightarrow> 'a"
+ assume "chain Y"
then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) \<sqsubseteq> (\<Squnion>i. f (Y i) (t (Y i)))"
by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1]
- cont2contlubE [OF 2] ch2ch_cont [OF 2]
- cont2contlubE [OF 3] ch2ch_cont [OF 3]
- diag_lub below_refl)
+ cont2contlubE [OF 2] ch2ch_cont [OF 2]
+ cont2contlubE [OF 3] ch2ch_cont [OF 3]
+ diag_lub below_refl)
qed
-lemma cont_compose:
- "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
-by (rule cont_apply [OF _ _ cont_const])
+lemma cont_compose: "cont c \<Longrightarrow> cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. c (f x))"
+ by (rule cont_apply [OF _ _ cont_const])
text \<open>Least upper bounds preserve continuity\<close>
lemma cont2cont_lub [simp]:
- assumes chain: "\<And>x. chain (\<lambda>i. F i x)" and cont: "\<And>i. cont (\<lambda>x. F i x)"
+ assumes chain: "\<And>x. chain (\<lambda>i. F i x)"
+ and cont: "\<And>i. cont (\<lambda>x. F i x)"
shows "cont (\<lambda>x. \<Squnion>i. F i x)"
-apply (rule contI2)
-apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain)
-apply (simp add: cont2contlubE [OF cont])
-apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
-done
+ apply (rule contI2)
+ apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain)
+ apply (simp add: cont2contlubE [OF cont])
+ apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
+ done
text \<open>if-then-else is continuous\<close>
-lemma cont_if [simp, cont2cont]:
- "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
-by (induct b) simp_all
+lemma cont_if [simp, cont2cont]: "cont f \<Longrightarrow> cont g \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
+ by (induct b) simp_all
+
subsection \<open>Finite chains and flat pcpos\<close>
text \<open>Monotone functions map finite chains to finite chains.\<close>
-lemma monofun_finch2finch:
- "\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
-apply (unfold finite_chain_def)
-apply (simp add: ch2ch_monofun)
-apply (force simp add: max_in_chain_def)
-done
+lemma monofun_finch2finch: "monofun f \<Longrightarrow> finite_chain Y \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
+ by (force simp add: finite_chain_def ch2ch_monofun max_in_chain_def)
text \<open>The same holds for continuous functions.\<close>
-lemma cont_finch2finch:
- "\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
-by (rule cont2mono [THEN monofun_finch2finch])
+lemma cont_finch2finch: "cont f \<Longrightarrow> finite_chain Y \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
+ by (rule cont2mono [THEN monofun_finch2finch])
text \<open>All monotone functions with chain-finite domain are continuous.\<close>
-lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
-apply (erule contI2)
-apply (frule chfin2finch)
-apply (clarsimp simp add: finite_chain_def)
-apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))")
-apply (simp add: maxinch_is_thelub ch2ch_monofun)
-apply (force simp add: max_in_chain_def)
-done
+lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont f"
+ for f :: "'a::chfin \<Rightarrow> 'b::cpo"
+ apply (erule contI2)
+ apply (frule chfin2finch)
+ apply (clarsimp simp add: finite_chain_def)
+ apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))")
+ apply (simp add: maxinch_is_thelub ch2ch_monofun)
+ apply (force simp add: max_in_chain_def)
+ done
text \<open>All strict functions with flat domain are continuous.\<close>
-lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
-apply (rule monofunI)
-apply (drule ax_flat)
-apply auto
-done
+lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun f"
+ for f :: "'a::flat \<Rightarrow> 'b::pcpo"
+ apply (rule monofunI)
+ apply (drule ax_flat)
+ apply auto
+ done
-lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)"
-by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
+lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont f"
+ for f :: "'a::flat \<Rightarrow> 'b::pcpo"
+ by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
text \<open>All functions with discrete domain are continuous.\<close>
-lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
-apply (rule contI)
-apply (drule discrete_chain_const, clarify)
-apply (simp add: is_lub_const)
-done
+lemma cont_discrete_cpo [simp, cont2cont]: "cont f"
+ for f :: "'a::discrete_cpo \<Rightarrow> 'b::cpo"
+ apply (rule contI)
+ apply (drule discrete_chain_const, clarify)
+ apply (simp add: is_lub_const)
+ done
end
--- a/src/HOL/HOLCF/Cpodef.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,8 +5,8 @@
section \<open>Subtypes of pcpos\<close>
theory Cpodef
-imports Adm
-keywords "pcpodef" "cpodef" :: thy_goal
+ imports Adm
+ keywords "pcpodef" "cpodef" :: thy_goal
begin
subsection \<open>Proving a subtype is a partial order\<close>
@@ -16,22 +16,22 @@
if the ordering is defined in the standard way.
\<close>
-setup \<open>Sign.add_const_constraint (@{const_name Porder.below}, NONE)\<close>
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>Porder.below\<close>, NONE)\<close>
theorem typedef_po:
fixes Abs :: "'a::po \<Rightarrow> 'b::type"
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "OFCLASS('b, po_class)"
- apply (intro_classes, unfold below)
- apply (rule below_refl)
- apply (erule (1) below_trans)
- apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
- apply (erule (1) below_antisym)
-done
+ apply (intro_classes, unfold below)
+ apply (rule below_refl)
+ apply (erule (1) below_trans)
+ apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
+ apply (erule (1) below_antisym)
+ done
-setup \<open>Sign.add_const_constraint (@{const_name Porder.below},
- SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"})\<close>
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>Porder.below\<close>, SOME \<^typ>\<open>'a::below \<Rightarrow> 'a::below \<Rightarrow> bool\<close>)\<close>
+
subsection \<open>Proving a subtype is finite\<close>
@@ -41,29 +41,32 @@
shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
proof -
assume "finite A"
- hence "finite (Abs ` A)" by (rule finite_imageI)
- thus "finite (UNIV :: 'b set)"
+ then have "finite (Abs ` A)"
+ by (rule finite_imageI)
+ then show "finite (UNIV :: 'b set)"
by (simp only: type_definition.Abs_image [OF type])
qed
+
subsection \<open>Proving a subtype is chain-finite\<close>
lemma ch2ch_Rep:
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
-unfolding chain_def below .
+ unfolding chain_def below .
theorem typedef_chfin:
fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "OFCLASS('b, chfin_class)"
- apply intro_classes
- apply (drule ch2ch_Rep [OF below])
- apply (drule chfin)
- apply (unfold max_in_chain_def)
- apply (simp add: type_definition.Rep_inject [OF type])
-done
+ apply intro_classes
+ apply (drule ch2ch_Rep [OF below])
+ apply (drule chfin)
+ apply (unfold max_in_chain_def)
+ apply (simp add: type_definition.Rep_inject [OF type])
+ done
+
subsection \<open>Proving a subtype is complete\<close>
@@ -78,7 +81,7 @@
lemma typedef_is_lubI:
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
-unfolding is_lub_def is_ub_def below by simp
+ by (simp add: is_lub_def is_ub_def below)
lemma Abs_inverse_lub_Rep:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
@@ -86,24 +89,26 @@
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
- apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF below]])
- apply (rule type_definition.Rep [OF type])
-done
+ apply (rule type_definition.Abs_inverse [OF type])
+ apply (erule admD [OF adm ch2ch_Rep [OF below]])
+ apply (rule type_definition.Rep [OF type])
+ done
theorem typedef_is_lub:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
- shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
+ assumes S: "chain S"
+ shows "range S <<| Abs (\<Squnion>i. Rep (S i))"
proof -
- assume S: "chain S"
- hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
- hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
- hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
+ from S have "chain (\<lambda>i. Rep (S i))"
+ by (rule ch2ch_Rep [OF below])
+ then have "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))"
+ by (rule cpo_lubI)
+ then have "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
- thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
+ then show "range S <<| Abs (\<Squnion>i. Rep (S i))"
by (rule typedef_is_lubI [OF below])
qed
@@ -116,12 +121,14 @@
and adm: "adm (\<lambda>x. x \<in> A)"
shows "OFCLASS('b, cpo_class)"
proof
- fix S::"nat \<Rightarrow> 'b" assume "chain S"
- hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
+ fix S :: "nat \<Rightarrow> 'b"
+ assume "chain S"
+ then have "range S <<| Abs (\<Squnion>i. Rep (S i))"
by (rule typedef_is_lub [OF type below adm])
- thus "\<exists>x. range S <<| x" ..
+ then show "\<exists>x. range S <<| x" ..
qed
+
subsubsection \<open>Continuity of \emph{Rep} and \emph{Abs}\<close>
text \<open>For any sub-cpo, the @{term Rep} function is continuous.\<close>
@@ -132,13 +139,13 @@
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
- apply (erule cont_apply [OF _ _ cont_const])
- apply (rule contI)
- apply (simp only: typedef_lub [OF type below adm])
- apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
- apply (rule cpo_lubI)
- apply (erule ch2ch_Rep [OF below])
-done
+ apply (erule cont_apply [OF _ _ cont_const])
+ apply (rule contI)
+ apply (simp only: typedef_lub [OF type below adm])
+ apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
+ apply (rule cpo_lubI)
+ apply (erule ch2ch_Rep [OF below])
+ done
text \<open>
For a sub-cpo, we can make the @{term Abs} function continuous
@@ -154,8 +161,9 @@
and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
and f_in_A: "\<And>x. f x \<in> A"
shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
-unfolding cont_def is_lub_def is_ub_def ball_simps below
-by (simp add: type_definition.Abs_inverse [OF type f_in_A])
+ unfolding cont_def is_lub_def is_ub_def ball_simps below
+ by (simp add: type_definition.Abs_inverse [OF type f_in_A])
+
subsection \<open>Proving subtype elements are compact\<close>
@@ -170,9 +178,10 @@
by (rule typedef_cont_Rep [OF type below adm cont_id])
assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)"
with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst)
- thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
+ then show "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
qed
+
subsection \<open>Proving a subtype is pointed\<close>
text \<open>
@@ -187,12 +196,12 @@
and z_in_A: "z \<in> A"
and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
shows "OFCLASS('b, pcpo_class)"
- apply (intro_classes)
- apply (rule_tac x="Abs z" in exI, rule allI)
- apply (unfold below)
- apply (subst type_definition.Abs_inverse [OF type z_in_A])
- apply (rule z_least [OF type_definition.Rep [OF type]])
-done
+ apply (intro_classes)
+ apply (rule_tac x="Abs z" in exI, rule allI)
+ apply (unfold below)
+ apply (subst type_definition.Abs_inverse [OF type z_in_A])
+ apply (rule z_least [OF type_definition.Rep [OF type]])
+ done
text \<open>
As a special case, a subtype of a pcpo has a least element
@@ -205,7 +214,8 @@
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, pcpo_class)"
-by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
+ by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
+
subsubsection \<open>Strictness of \emph{Rep} and \emph{Abs}\<close>
@@ -219,36 +229,37 @@
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "Abs \<bottom> = \<bottom>"
- apply (rule bottomI, unfold below)
- apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
-done
+ apply (rule bottomI, unfold below)
+ apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
+ done
theorem typedef_Rep_strict:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "Rep \<bottom> = \<bottom>"
- apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
- apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
-done
+ apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
+ apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
+ done
theorem typedef_Abs_bottom_iff:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
- apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
-done
+ apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
+ apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
+ done
theorem typedef_Rep_bottom_iff:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "(Rep x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
- apply (simp add: type_definition.Rep_inject [OF type])
-done
+ apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
+ apply (simp add: type_definition.Rep_inject [OF type])
+ done
+
subsection \<open>Proving a subtype is flat\<close>
@@ -258,12 +269,13 @@
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and bottom_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, flat_class)"
- apply (intro_classes)
- apply (unfold below)
- apply (simp add: type_definition.Rep_inject [OF type, symmetric])
- apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
- apply (simp add: ax_flat)
-done
+ apply (intro_classes)
+ apply (unfold below)
+ apply (simp add: type_definition.Rep_inject [OF type, symmetric])
+ apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
+ apply (simp add: ax_flat)
+ done
+
subsection \<open>HOLCF type definition package\<close>
--- a/src/HOL/HOLCF/Cprod.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Cprod.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,46 +5,45 @@
section \<open>The cpo of cartesian products\<close>
theory Cprod
-imports Cfun
+ imports Cfun
begin
default_sort cpo
+
subsection \<open>Continuous case function for unit type\<close>
-definition
- unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
- "unit_when = (\<Lambda> a _. a)"
+definition unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
+ where "unit_when = (\<Lambda> a _. a)"
translations
- "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
+ "\<Lambda>(). t" \<rightleftharpoons> "CONST unit_when\<cdot>t"
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
-by (simp add: unit_when_def)
+ by (simp add: unit_when_def)
+
subsection \<open>Continuous version of split function\<close>
-definition
- csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
- "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
+definition csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a \<times> 'b) \<rightarrow> 'c"
+ where "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
translations
- "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
+ "\<Lambda>(CONST Pair x y). t" \<rightleftharpoons> "CONST csplit\<cdot>(\<Lambda> x y. t)"
-abbreviation
- cfst :: "'a \<times> 'b \<rightarrow> 'a" where
- "cfst \<equiv> Abs_cfun fst"
+abbreviation cfst :: "'a \<times> 'b \<rightarrow> 'a"
+ where "cfst \<equiv> Abs_cfun fst"
-abbreviation
- csnd :: "'a \<times> 'b \<rightarrow> 'b" where
- "csnd \<equiv> Abs_cfun snd"
+abbreviation csnd :: "'a \<times> 'b \<rightarrow> 'b"
+ where "csnd \<equiv> Abs_cfun snd"
+
subsection \<open>Convert all lemmas to the continuous versions\<close>
lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
-by (simp add: csplit_def)
+ by (simp add: csplit_def)
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
-by (simp add: csplit_def)
+ by (simp add: csplit_def)
end
--- a/src/HOL/HOLCF/Deflation.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Deflation.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,11 +5,12 @@
section \<open>Continuous deflations and ep-pairs\<close>
theory Deflation
-imports Cfun
+ imports Cfun
begin
default_sort cpo
+
subsection \<open>Continuous deflations\<close>
locale deflation =
@@ -19,15 +20,15 @@
begin
lemma below_ID: "d \<sqsubseteq> ID"
-by (rule cfun_belowI, simp add: below)
+ by (rule cfun_belowI) (simp add: below)
text \<open>The set of fixed points is the same as the range.\<close>
lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
-by (auto simp add: eq_sym_conv idem)
+ by (auto simp add: eq_sym_conv idem)
lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
-by (auto simp add: eq_sym_conv idem)
+ by (auto simp add: eq_sym_conv idem)
text \<open>
The pointwise ordering on deflation functions coincides with
@@ -35,20 +36,22 @@
\<close>
lemma belowI:
- assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
+ assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x"
+ shows "d \<sqsubseteq> f"
proof (rule cfun_belowI)
fix x
- from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
- also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
+ from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x"
+ by (rule monofun_cfun_arg)
+ also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x"
+ by (rule f)
finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
qed
lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
proof (rule below_antisym)
from below show "d\<cdot>x \<sqsubseteq> x" .
-next
assume "f \<sqsubseteq> d"
- hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
+ then have "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
also assume "f\<cdot>x = x"
finally show "x \<sqsubseteq> d\<cdot>x" .
qed
@@ -56,23 +59,22 @@
end
lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
-by (rule deflation.below [THEN bottomI])
+ by (rule deflation.below [THEN bottomI])
lemma adm_deflation: "adm (\<lambda>d. deflation d)"
-by (simp add: deflation_def)
+ by (simp add: deflation_def)
lemma deflation_ID: "deflation ID"
-by (simp add: deflation.intro)
+ by (simp add: deflation.intro)
lemma deflation_bottom: "deflation \<bottom>"
-by (simp add: deflation.intro)
+ by (simp add: deflation.intro)
-lemma deflation_below_iff:
- "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
- apply safe
- apply (simp add: deflation.belowD)
- apply (simp add: deflation.belowI)
-done
+lemma deflation_below_iff: "deflation p \<Longrightarrow> deflation q \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
+ apply safe
+ apply (simp add: deflation.belowD)
+ apply (simp add: deflation.belowI)
+ done
text \<open>
The composition of two deflations is equal to
@@ -88,26 +90,26 @@
from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
next
interpret f: deflation f by fact
- assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
- hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
+ assume "f \<sqsubseteq> g"
+ then have "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
+ then have "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
qed
-lemma deflation_below_comp2:
- "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
-by (simp only: deflation.belowD deflation.idem)
+lemma deflation_below_comp2: "deflation f \<Longrightarrow> deflation g \<Longrightarrow> f \<sqsubseteq> g \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
+ by (simp only: deflation.belowD deflation.idem)
subsection \<open>Deflations with finite range\<close>
lemma finite_range_imp_finite_fixes:
- "finite (range f) \<Longrightarrow> finite {x. f x = x}"
+ assumes "finite (range f)"
+ shows "finite {x. f x = x}"
proof -
have "{x. f x = x} \<subseteq> range f"
by (clarify, erule subst, rule rangeI)
- moreover assume "finite (range f)"
- ultimately show "finite {x. f x = x}"
+ from this assms show "finite {x. f x = x}"
by (rule finite_subset)
qed
@@ -116,10 +118,10 @@
begin
lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
-by (simp add: range_eq_fixes finite_fixes)
+ by (simp add: range_eq_fixes finite_fixes)
lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
-by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
+ by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
lemma compact: "compact (d\<cdot>x)"
proof (rule compactI2)
@@ -127,41 +129,36 @@
assume Y: "chain Y"
have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
proof (rule finite_range_imp_finch)
- show "chain (\<lambda>i. d\<cdot>(Y i))"
- using Y by simp
- have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
- by clarsimp
- thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
+ from Y show "chain (\<lambda>i. d\<cdot>(Y i))" by simp
+ have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)" by auto
+ then show "finite (range (\<lambda>i. d\<cdot>(Y i)))"
using finite_range by (rule finite_subset)
qed
- hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
+ then have "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
by (simp add: finite_chain_def maxinch_is_thelub Y)
then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
- hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
+ then have "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
by (rule monofun_cfun_arg)
- hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
+ then have "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
by (simp add: contlub_cfun_arg Y idem)
- hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
- using j by simp
- hence "d\<cdot>x \<sqsubseteq> Y j"
+ with j have "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)" by simp
+ then have "d\<cdot>x \<sqsubseteq> Y j"
using below by (rule below_trans)
- thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
+ then show "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
qed
end
-lemma finite_deflation_intro:
- "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
-by (intro finite_deflation.intro finite_deflation_axioms.intro)
+lemma finite_deflation_intro: "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
+ by (intro finite_deflation.intro finite_deflation_axioms.intro)
-lemma finite_deflation_imp_deflation:
- "finite_deflation d \<Longrightarrow> deflation d"
-unfolding finite_deflation_def by simp
+lemma finite_deflation_imp_deflation: "finite_deflation d \<Longrightarrow> deflation d"
+ by (simp add: finite_deflation_def)
lemma finite_deflation_bottom: "finite_deflation \<bottom>"
-by standard simp_all
+ by standard simp_all
subsection \<open>Continuous embedding-projection pairs\<close>
@@ -175,22 +172,21 @@
lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
proof
assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
- hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
- thus "x \<sqsubseteq> y" by simp
+ then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
+ then show "x \<sqsubseteq> y" by simp
next
assume "x \<sqsubseteq> y"
- thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
+ then show "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
qed
lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
-unfolding po_eq_conv e_below_iff ..
+ unfolding po_eq_conv e_below_iff ..
-lemma p_eq_iff:
- "\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
-by (safe, erule subst, erule subst, simp)
+lemma p_eq_iff: "e\<cdot>(p\<cdot>x) = x \<Longrightarrow> e\<cdot>(p\<cdot>y) = y \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
+ by (safe, erule subst, erule subst, simp)
-lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
-by (auto, rule exI, erule sym)
+lemma p_inverse: "(\<exists>x. y = e\<cdot>x) \<longleftrightarrow> e\<cdot>(p\<cdot>y) = y"
+ by (auto, rule exI, erule sym)
lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
proof
@@ -206,28 +202,29 @@
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
proof -
assume "compact (e\<cdot>x)"
- hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD)
- hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
- hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp
- thus "compact x" by (rule compactI)
+ then have "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD)
+ then have "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
+ then have "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp
+ then show "compact x" by (rule compactI)
qed
-lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
+lemma compact_e:
+ assumes "compact x"
+ shows "compact (e\<cdot>x)"
proof -
- assume "compact x"
- hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD)
- hence "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
- hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
- thus "compact (e\<cdot>x)" by (rule compactI)
+ from assms have "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD)
+ then have "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
+ then have "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
+ then show "compact (e\<cdot>x)" by (rule compactI)
qed
lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
-by (rule iffI [OF compact_e_rev compact_e])
+ by (rule iffI [OF compact_e_rev compact_e])
text \<open>Deflations from ep-pairs\<close>
lemma deflation_e_p: "deflation (e oo p)"
-by (simp add: deflation.intro e_p_below)
+ by (simp add: deflation.intro e_p_below)
lemma deflation_e_d_p:
assumes "deflation d"
@@ -253,9 +250,9 @@
by (simp add: e_below_iff_below_p below)
have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
by (simp add: finite_image)
- hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
+ then have "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
by (simp add: image_image)
- thus "finite {x. (e oo d oo p)\<cdot>x = x}"
+ then show "finite {x. (e oo d oo p)\<cdot>x = x}"
by (rule finite_range_imp_finite_fixes)
qed
@@ -265,32 +262,27 @@
shows "deflation (p oo d oo e)"
proof -
interpret d: deflation d by fact
- {
- fix x
+ have p_d_e_below: "(p oo d oo e)\<cdot>x \<sqsubseteq> x" for x
+ proof -
have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
by (rule d.below)
- hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
+ then have "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
by (rule monofun_cfun_arg)
- hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
- by simp
- }
- note p_d_e_below = this
+ then show ?thesis by simp
+ qed
show ?thesis
proof
- fix x
- show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
+ show "(p oo d oo e)\<cdot>x \<sqsubseteq> x" for x
by (rule p_d_e_below)
- next
- fix x
- show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
+ show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x" for x
proof (rule below_antisym)
show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
by (rule p_d_e_below)
have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
by (intro monofun_cfun_arg d)
- hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
+ then have "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
by (simp only: d.idem)
- thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
+ then show "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
by simp
qed
qed
@@ -305,16 +297,16 @@
show ?thesis
proof (rule finite_deflation_intro)
have "deflation d" ..
- thus "deflation (p oo d oo e)"
+ then show "deflation (p oo d oo e)"
using d by (rule deflation_p_d_e)
next
have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
by (rule d.finite_image)
- hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
+ then have "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
by (rule finite_imageI)
- hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
+ then have "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
by (simp add: image_image)
- thus "finite {x. (p oo d oo e)\<cdot>x = x}"
+ then show "finite {x. (p oo d oo e)\<cdot>x = x}"
by (rule finite_range_imp_finite_fixes)
qed
qed
@@ -324,41 +316,42 @@
subsection \<open>Uniqueness of ep-pairs\<close>
lemma ep_pair_unique_e_lemma:
- assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
+ assumes 1: "ep_pair e1 p"
+ and 2: "ep_pair e2 p"
shows "e1 \<sqsubseteq> e2"
proof (rule cfun_belowI)
fix x
have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
by (rule ep_pair.e_p_below [OF 1])
- thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
+ then show "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
by (simp only: ep_pair.e_inverse [OF 2])
qed
-lemma ep_pair_unique_e:
- "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
-by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
+lemma ep_pair_unique_e: "ep_pair e1 p \<Longrightarrow> ep_pair e2 p \<Longrightarrow> e1 = e2"
+ by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
lemma ep_pair_unique_p_lemma:
- assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
+ assumes 1: "ep_pair e p1"
+ and 2: "ep_pair e p2"
shows "p1 \<sqsubseteq> p2"
proof (rule cfun_belowI)
fix x
have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
by (rule ep_pair.e_p_below [OF 1])
- hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
+ then have "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
by (rule monofun_cfun_arg)
- thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
+ then show "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
by (simp only: ep_pair.e_inverse [OF 2])
qed
-lemma ep_pair_unique_p:
- "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
-by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
+lemma ep_pair_unique_p: "ep_pair e p1 \<Longrightarrow> ep_pair e p2 \<Longrightarrow> p1 = p2"
+ by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
+
subsection \<open>Composing ep-pairs\<close>
lemma ep_pair_ID_ID: "ep_pair ID ID"
-by standard simp_all
+ by standard simp_all
lemma ep_pair_comp:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -371,7 +364,7 @@
by simp
have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
by (rule ep1.e_p_below)
- hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
+ then have "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
by (rule monofun_cfun_arg)
also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
by (rule ep2.e_p_below)
@@ -387,19 +380,19 @@
lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
proof -
have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
- hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
+ then have "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
finally show "e\<cdot>\<bottom> = \<bottom>" by simp
qed
lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
-by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
+ by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
-by simp
+ by simp
lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
-by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
+ by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
lemmas stricts = e_strict p_strict
--- a/src/HOL/HOLCF/Discrete.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Discrete.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,7 +5,7 @@
section \<open>Discrete cpo types\<close>
theory Discrete
-imports Cont
+ imports Cont
begin
datatype 'a discr = Discr "'a :: type"
@@ -15,24 +15,23 @@
instantiation discr :: (type) discrete_cpo
begin
-definition
- "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
+definition "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
instance
by standard (simp add: below_discr_def)
end
+
subsection \<open>\emph{undiscr}\<close>
-definition
- undiscr :: "('a::type)discr => 'a" where
- "undiscr x = (case x of Discr y => y)"
+definition undiscr :: "('a::type)discr \<Rightarrow> 'a"
+ where "undiscr x = (case x of Discr y \<Rightarrow> y)"
lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
-by (simp add: undiscr_def)
+ by (simp add: undiscr_def)
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
-by (induct y) simp
+ by (induct y) simp
end
--- a/src/HOL/HOLCF/Fix.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Fix.thy Mon Jan 01 23:07:24 2018 +0100
@@ -6,51 +6,50 @@
section \<open>Fixed point operator and admissibility\<close>
theory Fix
-imports Cfun
+ imports Cfun
begin
default_sort pcpo
+
subsection \<open>Iteration\<close>
-primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
+primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)"
+ where
"iterate 0 = (\<Lambda> F x. x)"
| "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
text \<open>Derive inductive properties of iterate from primitive recursion\<close>
lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x"
-by simp
+ by simp
lemma iterate_Suc [simp]: "iterate (Suc n)\<cdot>F\<cdot>x = F\<cdot>(iterate n\<cdot>F\<cdot>x)"
-by simp
+ by simp
declare iterate.simps [simp del]
lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
-by (induct n) simp_all
+ by (induct n) simp_all
-lemma iterate_iterate:
- "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"
-by (induct m) simp_all
+lemma iterate_iterate: "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"
+ by (induct m) simp_all
text \<open>The sequence of function iterations is a chain.\<close>
lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)"
-by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)
+ by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)
subsection \<open>Least fixed point operator\<close>
-definition
- "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
- "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
+definition "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a"
+ where "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
text \<open>Binder syntax for @{term fix}\<close>
-abbreviation
- fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "\<mu> " 10) where
- "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
+abbreviation fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "\<mu> " 10)
+ where "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
notation (ASCII)
fix_syn (binder "FIX " 10)
@@ -60,7 +59,7 @@
text \<open>direct connection between @{term fix} and iteration\<close>
lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
-unfolding fix_def by simp
+ by (simp add: fix_def)
lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
unfolding fix_def2
@@ -72,105 +71,103 @@
\<close>
lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)"
-apply (simp add: fix_def2)
-apply (subst lub_range_shift [of _ 1, symmetric])
-apply (rule chain_iterate)
-apply (subst contlub_cfun_arg)
-apply (rule chain_iterate)
-apply simp
-done
+ apply (simp add: fix_def2)
+ apply (subst lub_range_shift [of _ 1, symmetric])
+ apply (rule chain_iterate)
+ apply (subst contlub_cfun_arg)
+ apply (rule chain_iterate)
+ apply simp
+ done
lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
-apply (simp add: fix_def2)
-apply (rule lub_below)
-apply (rule chain_iterate)
-apply (induct_tac i)
-apply simp
-apply simp
-apply (erule rev_below_trans)
-apply (erule monofun_cfun_arg)
-done
+ apply (simp add: fix_def2)
+ apply (rule lub_below)
+ apply (rule chain_iterate)
+ apply (induct_tac i)
+ apply simp
+ apply simp
+ apply (erule rev_below_trans)
+ apply (erule monofun_cfun_arg)
+ done
lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
-by (rule fix_least_below, simp)
+ by (rule fix_least_below) simp
lemma fix_eqI:
- assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
+ assumes fixed: "F\<cdot>x = x"
+ and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
shows "fix\<cdot>F = x"
-apply (rule below_antisym)
-apply (rule fix_least [OF fixed])
-apply (rule least [OF fix_eq [symmetric]])
-done
+ apply (rule below_antisym)
+ apply (rule fix_least [OF fixed])
+ apply (rule least [OF fix_eq [symmetric]])
+ done
lemma fix_eq2: "f \<equiv> fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
-by (simp add: fix_eq [symmetric])
+ by (simp add: fix_eq [symmetric])
lemma fix_eq3: "f \<equiv> fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
-by (erule fix_eq2 [THEN cfun_fun_cong])
+ by (erule fix_eq2 [THEN cfun_fun_cong])
lemma fix_eq4: "f = fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
-apply (erule ssubst)
-apply (rule fix_eq)
-done
+ by (erule ssubst) (rule fix_eq)
lemma fix_eq5: "f = fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
-by (erule fix_eq4 [THEN cfun_fun_cong])
+ by (erule fix_eq4 [THEN cfun_fun_cong])
text \<open>strictness of @{term fix}\<close>
-lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
-apply (rule iffI)
-apply (erule subst)
-apply (rule fix_eq [symmetric])
-apply (erule fix_least [THEN bottomI])
-done
+lemma fix_bottom_iff: "fix\<cdot>F = \<bottom> \<longleftrightarrow> F\<cdot>\<bottom> = \<bottom>"
+ apply (rule iffI)
+ apply (erule subst)
+ apply (rule fix_eq [symmetric])
+ apply (erule fix_least [THEN bottomI])
+ done
lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
-by (simp add: fix_bottom_iff)
+ by (simp add: fix_bottom_iff)
lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
-by (simp add: fix_bottom_iff)
+ by (simp add: fix_bottom_iff)
text \<open>@{term fix} applied to identity and constant functions\<close>
lemma fix_id: "(\<mu> x. x) = \<bottom>"
-by (simp add: fix_strict)
+ by (simp add: fix_strict)
lemma fix_const: "(\<mu> x. c) = c"
-by (subst fix_eq, simp)
+ by (subst fix_eq) simp
+
subsection \<open>Fixed point induction\<close>
-lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
-unfolding fix_def2
-apply (erule admD)
-apply (rule chain_iterate)
-apply (rule nat_induct, simp_all)
-done
+lemma fix_ind: "adm P \<Longrightarrow> P \<bottom> \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P (F\<cdot>x)) \<Longrightarrow> P (fix\<cdot>F)"
+ unfolding fix_def2
+ apply (erule admD)
+ apply (rule chain_iterate)
+ apply (rule nat_induct, simp_all)
+ done
-lemma cont_fix_ind:
- "\<lbrakk>cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>(Abs_cfun F))"
-by (simp add: fix_ind)
+lemma cont_fix_ind: "cont F \<Longrightarrow> adm P \<Longrightarrow> P \<bottom> \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P (F x)) \<Longrightarrow> P (fix\<cdot>(Abs_cfun F))"
+ by (simp add: fix_ind)
-lemma def_fix_ind:
- "\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
-by (simp add: fix_ind)
+lemma def_fix_ind: "\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
+ by (simp add: fix_ind)
lemma fix_ind2:
assumes adm: "adm P"
assumes 0: "P \<bottom>" and 1: "P (F\<cdot>\<bottom>)"
assumes step: "\<And>x. \<lbrakk>P x; P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (F\<cdot>(F\<cdot>x))"
shows "P (fix\<cdot>F)"
-unfolding fix_def2
-apply (rule admD [OF adm chain_iterate])
-apply (rule nat_less_induct)
-apply (case_tac n)
-apply (simp add: 0)
-apply (case_tac nat)
-apply (simp add: 1)
-apply (frule_tac x=nat in spec)
-apply (simp add: step)
-done
+ unfolding fix_def2
+ apply (rule admD [OF adm chain_iterate])
+ apply (rule nat_less_induct)
+ apply (case_tac n)
+ apply (simp add: 0)
+ apply (case_tac nat)
+ apply (simp add: 1)
+ apply (frule_tac x=nat in spec)
+ apply (simp add: step)
+ done
lemma parallel_fix_ind:
assumes adm: "adm (\<lambda>x. P (fst x) (snd x))"
@@ -180,17 +177,17 @@
proof -
from adm have adm': "adm (case_prod P)"
unfolding split_def .
- have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
- by (induct_tac i, simp add: base, simp add: step)
- hence "\<And>i. case_prod P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
+ have "P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)" for i
+ by (induct i) (simp add: base, simp add: step)
+ then have "\<And>i. case_prod P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
by simp
- hence "case_prod P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
+ then have "case_prod P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
by - (rule admD [OF adm'], simp, assumption)
- hence "case_prod P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
+ then have "case_prod P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
by (simp add: lub_Pair)
- hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
+ then have "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
by simp
- thus "P (fix\<cdot>F) (fix\<cdot>G)"
+ then show "P (fix\<cdot>F) (fix\<cdot>G)"
by (simp add: fix_def2)
qed
@@ -200,7 +197,8 @@
assumes "P \<bottom> \<bottom>"
assumes "\<And>x y. P x y \<Longrightarrow> P (F x) (G y)"
shows "P (fix\<cdot>(Abs_cfun F)) (fix\<cdot>(Abs_cfun G))"
-by (rule parallel_fix_ind, simp_all add: assms)
+ by (rule parallel_fix_ind) (simp_all add: assms)
+
subsection \<open>Fixed-points on product types\<close>
@@ -215,27 +213,35 @@
\<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
(is "fix\<cdot>F = (?x, ?y)")
proof (rule fix_eqI)
- have 1: "fst (F\<cdot>(?x, ?y)) = ?x"
+ have *: "fst (F\<cdot>(?x, ?y)) = ?x"
by (rule trans [symmetric, OF fix_eq], simp)
- have 2: "snd (F\<cdot>(?x, ?y)) = ?y"
+ have "snd (F\<cdot>(?x, ?y)) = ?y"
by (rule trans [symmetric, OF fix_eq], simp)
- from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
+ with * show "F\<cdot>(?x, ?y) = (?x, ?y)"
+ by (simp add: prod_eq_iff)
next
- fix z assume F_z: "F\<cdot>z = z"
- obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
+ fix z
+ assume F_z: "F\<cdot>z = z"
+ obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
from F_z z have F_x: "fst (F\<cdot>(x, y)) = x" by simp
from F_z z have F_y: "snd (F\<cdot>(x, y)) = y" by simp
let ?y1 = "\<mu> y. snd (F\<cdot>(x, y))"
- have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
- hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> fst (F\<cdot>(x, y))"
+ have "?y1 \<sqsubseteq> y"
+ by (rule fix_least) (simp add: F_y)
+ then have "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> fst (F\<cdot>(x, y))"
by (simp add: fst_monofun monofun_cfun)
- hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> x" using F_x by simp
- hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
- hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> snd (F\<cdot>(x, y))"
+ with F_x have "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> x"
+ by simp
+ then have *: "?x \<sqsubseteq> x"
+ by (simp add: fix_least_below)
+ then have "snd (F\<cdot>(?x, y)) \<sqsubseteq> snd (F\<cdot>(x, y))"
by (simp add: snd_monofun monofun_cfun)
- hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> y" using F_y by simp
- hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
- show "(?x, ?y) \<sqsubseteq> z" using z 1 2 by simp
+ with F_y have "snd (F\<cdot>(?x, y)) \<sqsubseteq> y"
+ by simp
+ then have "?y \<sqsubseteq> y"
+ by (simp add: fix_least_below)
+ with z * show "(?x, ?y) \<sqsubseteq> z"
+ by simp
qed
end
--- a/src/HOL/HOLCF/Fun_Cpo.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Fun_Cpo.thy Mon Jan 01 23:07:24 2018 +0100
@@ -6,7 +6,7 @@
section \<open>Class instances for the full function space\<close>
theory Fun_Cpo
-imports Adm
+ imports Adm
begin
subsection \<open>Full function space is a partial order\<close>
@@ -14,8 +14,7 @@
instantiation "fun" :: (type, below) below
begin
-definition
- below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
+definition below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
instance ..
end
@@ -27,127 +26,125 @@
by (simp add: below_fun_def)
next
fix f g :: "'a \<Rightarrow> 'b"
- assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
+ assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" then show "f = g"
by (simp add: below_fun_def fun_eq_iff below_antisym)
next
fix f g h :: "'a \<Rightarrow> 'b"
- assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
+ assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" then show "f \<sqsubseteq> h"
unfolding below_fun_def by (fast elim: below_trans)
qed
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)"
-by (simp add: below_fun_def)
+ by (simp add: below_fun_def)
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: below_fun_def)
+ by (simp add: below_fun_def)
lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
-by (simp add: below_fun_def)
+ by (simp add: below_fun_def)
+
subsection \<open>Full function space is chain complete\<close>
text \<open>Properties of chains of functions.\<close>
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
-unfolding chain_def fun_below_iff by auto
+ by (auto simp: chain_def fun_below_iff)
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
-by (simp add: chain_def below_fun_def)
+ by (simp add: chain_def below_fun_def)
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
-by (simp add: chain_def below_fun_def)
-
-text \<open>Type @{typ "'a::type => 'b::cpo"} is chain complete\<close>
+ by (simp add: chain_def below_fun_def)
-lemma is_lub_lambda:
- "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
-unfolding is_lub_def is_ub_def below_fun_def by simp
+text \<open>Type @{typ "'a::type \<Rightarrow> 'b::cpo"} is chain complete\<close>
+
+lemma is_lub_lambda: "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
+ by (simp add: is_lub_def is_ub_def below_fun_def)
-lemma is_lub_fun:
- "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
- \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
-apply (rule is_lub_lambda)
-apply (rule cpo_lubI)
-apply (erule ch2ch_fun)
-done
+lemma is_lub_fun: "chain S \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
+ for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
+ apply (rule is_lub_lambda)
+ apply (rule cpo_lubI)
+ apply (erule ch2ch_fun)
+ done
-lemma lub_fun:
- "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
- \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-by (rule is_lub_fun [THEN lub_eqI])
+lemma lub_fun: "chain S \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
+ for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
+ by (rule is_lub_fun [THEN lub_eqI])
instance "fun" :: (type, cpo) cpo
-by intro_classes (rule exI, erule is_lub_fun)
+ by intro_classes (rule exI, erule is_lub_fun)
instance "fun" :: (type, discrete_cpo) discrete_cpo
proof
fix f g :: "'a \<Rightarrow> 'b"
- show "f \<sqsubseteq> g \<longleftrightarrow> f = g"
- unfolding fun_below_iff fun_eq_iff
- by simp
+ show "f \<sqsubseteq> g \<longleftrightarrow> f = g"
+ by (simp add: fun_below_iff fun_eq_iff)
qed
+
subsection \<open>Full function space is pointed\<close>
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
-by (simp add: below_fun_def)
+ by (simp add: below_fun_def)
instance "fun" :: (type, pcpo) pcpo
-by standard (fast intro: minimal_fun)
+ by standard (fast intro: minimal_fun)
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
-by (rule minimal_fun [THEN bottomI, symmetric])
+ by (rule minimal_fun [THEN bottomI, symmetric])
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
-by (simp add: inst_fun_pcpo)
+ by (simp add: inst_fun_pcpo)
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
-by (rule bottomI, rule minimal_fun)
+ by (rule bottomI, rule minimal_fun)
+
subsection \<open>Propagation of monotonicity and continuity\<close>
text \<open>The lub of a chain of monotone functions is monotone.\<close>
lemma adm_monofun: "adm monofun"
-by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono)
+ by (rule admI) (simp add: lub_fun fun_chain_iff monofun_def lub_mono)
text \<open>The lub of a chain of continuous functions is continuous.\<close>
lemma adm_cont: "adm cont"
-by (rule admI, simp add: lub_fun fun_chain_iff)
+ by (rule admI) (simp add: lub_fun fun_chain_iff)
text \<open>Function application preserves monotonicity and continuity.\<close>
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
-by (simp add: monofun_def fun_below_iff)
+ by (simp add: monofun_def fun_below_iff)
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
-apply (rule contI2)
-apply (erule cont2mono [THEN mono2mono_fun])
-apply (simp add: cont2contlubE lub_fun ch2ch_cont)
-done
+ apply (rule contI2)
+ apply (erule cont2mono [THEN mono2mono_fun])
+ apply (simp add: cont2contlubE lub_fun ch2ch_cont)
+ done
lemma cont_fun: "cont (\<lambda>f. f x)"
-using cont_id by (rule cont2cont_fun)
+ using cont_id by (rule cont2cont_fun)
text \<open>
Lambda abstraction preserves monotonicity and continuity.
(Note \<open>(\<lambda>x. \<lambda>y. f x y) = f\<close>.)
\<close>
-lemma mono2mono_lambda:
- assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
-using f by (simp add: monofun_def fun_below_iff)
+lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f"
+ by (simp add: monofun_def fun_below_iff)
lemma cont2cont_lambda [simp]:
- assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
-by (rule contI, rule is_lub_lambda, rule contE [OF f])
+ assumes f: "\<And>y. cont (\<lambda>x. f x y)"
+ shows "cont f"
+ by (rule contI, rule is_lub_lambda, rule contE [OF f])
text \<open>What D.A.Schmidt calls continuity of abstraction; never used here\<close>
-lemma contlub_lambda:
- "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
- \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
-by (simp add: lub_fun ch2ch_lambda)
+lemma contlub_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
+ for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
+ by (simp add: lub_fun ch2ch_lambda)
end
--- a/src/HOL/HOLCF/Map_Functions.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,28 +5,24 @@
section \<open>Map functions for various types\<close>
theory Map_Functions
-imports Deflation Sprod Ssum Sfun Up
+ imports Deflation Sprod Ssum Sfun Up
begin
subsection \<open>Map operator for continuous function space\<close>
default_sort cpo
-definition
- cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
-where
- "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
+definition cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
+ where "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
-unfolding cfun_map_def by simp
+ by (simp add: cfun_map_def)
lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
-unfolding cfun_eq_iff by simp
+ by (simp add: cfun_eq_iff)
-lemma cfun_map_map:
- "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
- cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-by (rule cfun_eqI) simp
+lemma cfun_map_map: "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) = cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+ by (rule cfun_eqI) simp
lemma ep_pair_cfun_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -34,9 +30,9 @@
proof
interpret e1p1: ep_pair e1 p1 by fact
interpret e2p2: ep_pair e2 p2 by fact
- fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
+ show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" for f
by (simp add: cfun_eq_iff)
- fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
+ show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" for g
apply (rule cfun_belowI, simp)
apply (rule below_trans [OF e2p2.e_p_below])
apply (rule monofun_cfun_arg)
@@ -79,13 +75,13 @@
proof (rule inj_onI, rule cfun_eqI, clarsimp)
fix x f g
assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
- hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ then have "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
by (rule equalityD1)
- hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ then have "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
by (simp add: subset_eq)
then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
by (rule rangeE)
- thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
+ then show "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
by clarsimp
qed
qed
@@ -97,41 +93,39 @@
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
- thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
+ then show "deflation (cfun_map\<cdot>d1\<cdot>d2)"
+ by (rule deflation_cfun_map)
have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
using d1.finite_range d2.finite_range
by (rule finite_range_cfun_map)
- thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ then show "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
by (rule finite_range_imp_finite_fixes)
qed
text \<open>Finite deflations are compact elements of the function space\<close>
lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
-apply (frule finite_deflation_imp_deflation)
-apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
-apply (simp add: cfun_map_def deflation.idem eta_cfun)
-apply (rule finite_deflation.compact)
-apply (simp only: finite_deflation_cfun_map)
-done
+ apply (frule finite_deflation_imp_deflation)
+ apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
+ apply (simp add: cfun_map_def deflation.idem eta_cfun)
+ apply (rule finite_deflation.compact)
+ apply (simp only: finite_deflation_cfun_map)
+ done
+
subsection \<open>Map operator for product type\<close>
-definition
- prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
-where
- "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
+definition prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
+ where "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
lemma prod_map_Pair [simp]: "prod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
-unfolding prod_map_def by simp
+ by (simp add: prod_map_def)
lemma prod_map_ID: "prod_map\<cdot>ID\<cdot>ID = ID"
-unfolding cfun_eq_iff by auto
+ by (auto simp: cfun_eq_iff)
-lemma prod_map_map:
- "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) =
- prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-by (induct p) simp
+lemma prod_map_map: "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) = prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+ by (induct p) simp
lemma ep_pair_prod_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -139,9 +133,9 @@
proof
interpret e1p1: ep_pair e1 p1 by fact
interpret e2p2: ep_pair e2 p2 by fact
- fix x show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
by (induct x) simp
- fix y show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
qed
@@ -165,91 +159,90 @@
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
- thus "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map)
+ then show "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map)
have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
- by clarsimp
- thus "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
+ by auto
+ then show "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
+
subsection \<open>Map function for lifted cpo\<close>
-definition
- u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
-where
- "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
+definition u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
+ where "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
-unfolding u_map_def by simp
+ by (simp add: u_map_def)
lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
-unfolding u_map_def by simp
+ by (simp add: u_map_def)
lemma u_map_ID: "u_map\<cdot>ID = ID"
-unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
+ by (simp add: u_map_def cfun_eq_iff eta_cfun)
lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
-by (induct p) simp_all
+ by (induct p) simp_all
lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g"
-by (simp add: cfcomp1 u_map_map eta_cfun)
+ by (simp add: cfcomp1 u_map_map eta_cfun)
lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
-apply standard
-apply (case_tac x, simp, simp add: ep_pair.e_inverse)
-apply (case_tac y, simp, simp add: ep_pair.e_p_below)
-done
+ apply standard
+ subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse)
+ subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below)
+ done
lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
-apply standard
-apply (case_tac x, simp, simp add: deflation.idem)
-apply (case_tac x, simp, simp add: deflation.below)
-done
+ apply standard
+ subgoal for x by (cases x, simp, simp add: deflation.idem)
+ subgoal for x by (cases x, simp, simp add: deflation.below)
+ done
lemma finite_deflation_u_map:
- assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
+ assumes "finite_deflation d"
+ shows "finite_deflation (u_map\<cdot>d)"
proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
have "deflation d" by fact
- thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
+ then show "deflation (u_map\<cdot>d)"
+ by (rule deflation_u_map)
have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
by (rule subsetI, case_tac x, simp_all)
- thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
- by (rule finite_subset, simp add: d.finite_fixes)
+ then show "finite {x. u_map\<cdot>d\<cdot>x = x}"
+ by (rule finite_subset) (simp add: d.finite_fixes)
qed
+
subsection \<open>Map function for strict products\<close>
default_sort pcpo
-definition
- sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
-where
- "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
+definition sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
+ where "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding sprod_map_def by simp
+ by (simp add: sprod_map_def)
-lemma sprod_map_spair [simp]:
- "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
-by (simp add: sprod_map_def)
+lemma sprod_map_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+ by (simp add: sprod_map_def)
-lemma sprod_map_spair':
- "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
-by (cases "x = \<bottom> \<or> y = \<bottom>") auto
+lemma sprod_map_spair': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+ by (cases "x = \<bottom> \<or> y = \<bottom>") auto
lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
-unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
+ by (simp add: sprod_map_def cfun_eq_iff eta_cfun)
lemma sprod_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-apply (induct p, simp)
-apply (case_tac "f2\<cdot>x = \<bottom>", simp)
-apply (case_tac "g2\<cdot>y = \<bottom>", simp)
-apply simp
-done
+ apply (induct p)
+ apply simp
+ apply (case_tac "f2\<cdot>x = \<bottom>", simp)
+ apply (case_tac "g2\<cdot>y = \<bottom>", simp)
+ apply simp
+ done
lemma ep_pair_sprod_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -257,10 +250,11 @@
proof
interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
- fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
by (induct x) simp_all
- fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
- apply (induct y, simp)
+ show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
+ apply (induct y)
+ apply simp
apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
done
@@ -291,47 +285,48 @@
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
- thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
- have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
- ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
+ then show "deflation (sprod_map\<cdot>d1\<cdot>d2)"
+ by (rule deflation_sprod_map)
+ have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
+ insert \<bottom> ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
- thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
- by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+ then show "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+ by (rule finite_subset) (simp add: d1.finite_fixes d2.finite_fixes)
qed
+
subsection \<open>Map function for strict sums\<close>
-definition
- ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
-where
- "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
+definition ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
+ where "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
-unfolding ssum_map_def by simp
+ by (simp add: ssum_map_def)
lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
-unfolding ssum_map_def by simp
+ by (simp add: ssum_map_def)
lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
-unfolding ssum_map_def by simp
+ by (simp add: ssum_map_def)
lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
-by (cases "x = \<bottom>") simp_all
+ by (cases "x = \<bottom>") simp_all
lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
-by (cases "x = \<bottom>") simp_all
+ by (cases "x = \<bottom>") simp_all
lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
-unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
+ by (simp add: ssum_map_def cfun_eq_iff eta_cfun)
lemma ssum_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-apply (induct p, simp)
-apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
-apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
-done
+ apply (induct p)
+ apply simp
+ apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
+ apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
+ done
lemma ep_pair_ssum_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -339,11 +334,12 @@
proof
interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
- fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
by (induct x) simp_all
- fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
- apply (induct y, simp)
- apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
+ show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
+ apply (induct y)
+ apply simp
+ apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
done
qed
@@ -374,32 +370,30 @@
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
- thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
+ then show "deflation (ssum_map\<cdot>d1\<cdot>d2)"
+ by (rule deflation_ssum_map)
have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
(\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
(\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
by (rule subsetI, case_tac x, simp_all)
- thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+ then show "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
+
subsection \<open>Map operator for strict function space\<close>
-definition
- sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
-where
- "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
+definition sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
+ where "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
- unfolding sfun_map_def
- by (simp add: cfun_map_ID cfun_eq_iff)
+ by (simp add: sfun_map_def cfun_map_ID cfun_eq_iff)
lemma sfun_map_map:
- assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
- "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>"
+ shows "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-unfolding sfun_map_def
-by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
+ by (simp add: sfun_map_def cfun_eq_iff strictify_cancel assms cfun_map_map)
lemma ep_pair_sfun_map:
assumes 1: "ep_pair e1 p1"
@@ -410,13 +404,13 @@
unfolding pcpo_ep_pair_def by fact
interpret e2p2: pcpo_ep_pair e2 p2
unfolding pcpo_ep_pair_def by fact
- fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
+ show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" for f
unfolding sfun_map_def
apply (simp add: sfun_eq_iff strictify_cancel)
apply (rule ep_pair.e_inverse)
apply (rule ep_pair_cfun_map [OF 1 2])
done
- fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
+ show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" for g
unfolding sfun_map_def
apply (simp add: sfun_below_iff strictify_cancel)
apply (rule ep_pair.e_p_below)
@@ -428,40 +422,39 @@
assumes 1: "deflation d1"
assumes 2: "deflation d2"
shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
-apply (simp add: sfun_map_def)
-apply (rule deflation.intro)
-apply simp
-apply (subst strictify_cancel)
-apply (simp add: cfun_map_def deflation_strict 1 2)
-apply (simp add: cfun_map_def deflation.idem 1 2)
-apply (simp add: sfun_below_iff)
-apply (subst strictify_cancel)
-apply (simp add: cfun_map_def deflation_strict 1 2)
-apply (rule deflation.below)
-apply (rule deflation_cfun_map [OF 1 2])
-done
+ apply (simp add: sfun_map_def)
+ apply (rule deflation.intro)
+ apply simp
+ apply (subst strictify_cancel)
+ apply (simp add: cfun_map_def deflation_strict 1 2)
+ apply (simp add: cfun_map_def deflation.idem 1 2)
+ apply (simp add: sfun_below_iff)
+ apply (subst strictify_cancel)
+ apply (simp add: cfun_map_def deflation_strict 1 2)
+ apply (rule deflation.below)
+ apply (rule deflation_cfun_map [OF 1 2])
+ done
lemma finite_deflation_sfun_map:
- assumes 1: "finite_deflation d1"
- assumes 2: "finite_deflation d2"
+ assumes "finite_deflation d1"
+ and "finite_deflation d2"
shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
proof (intro finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
- thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
- from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
+ then show "deflation (sfun_map\<cdot>d1\<cdot>d2)"
+ by (rule deflation_sfun_map)
+ from assms have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
by (rule finite_deflation_cfun_map)
then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
by (rule finite_deflation.finite_fixes)
moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
- by (rule inj_onI, simp add: sfun_eq_iff)
+ by (rule inj_onI) (simp add: sfun_eq_iff)
ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
by (rule finite_vimageI)
- then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
- unfolding sfun_map_def sfun_eq_iff
- by (simp add: strictify_cancel
- deflation_strict \<open>deflation d1\<close> \<open>deflation d2\<close>)
+ with \<open>deflation d1\<close> \<open>deflation d2\<close> show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ by (simp add: sfun_map_def sfun_eq_iff strictify_cancel deflation_strict)
qed
end
--- a/src/HOL/HOLCF/One.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/One.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,69 +5,67 @@
section \<open>The unit domain\<close>
theory One
-imports Lift
+ imports Lift
begin
-type_synonym
- one = "unit lift"
+type_synonym one = "unit lift"
translations
- (type) "one" <= (type) "unit lift"
+ (type) "one" \<leftharpoondown> (type) "unit lift"
definition ONE :: "one"
- where "ONE == Def ()"
+ where "ONE \<equiv> Def ()"
text \<open>Exhaustion and Elimination for type @{typ one}\<close>
lemma Exh_one: "t = \<bottom> \<or> t = ONE"
-unfolding ONE_def by (induct t) simp_all
+ by (induct t) (simp_all add: ONE_def)
lemma oneE [case_names bottom ONE]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-unfolding ONE_def by (induct p) simp_all
+ by (induct p) (simp_all add: ONE_def)
-lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
-by (cases x rule: oneE) simp_all
+lemma one_induct [case_names bottom ONE]: "P \<bottom> \<Longrightarrow> P ONE \<Longrightarrow> P x"
+ by (cases x rule: oneE) simp_all
lemma dist_below_one [simp]: "ONE \<notsqsubseteq> \<bottom>"
-unfolding ONE_def by simp
+ by (simp add: ONE_def)
lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
-by (induct x rule: one_induct) simp_all
+ by (induct x rule: one_induct) simp_all
lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
-by (induct x rule: one_induct) simp_all
+ by (induct x rule: one_induct) simp_all
lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
-unfolding ONE_def by simp
+ by (simp add: ONE_def)
lemma one_neq_iffs [simp]:
"x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
"ONE \<noteq> x \<longleftrightarrow> x = \<bottom>"
"x \<noteq> \<bottom> \<longleftrightarrow> x = ONE"
"\<bottom> \<noteq> x \<longleftrightarrow> x = ONE"
-by (induct x rule: one_induct) simp_all
+ by (induct x rule: one_induct) simp_all
lemma compact_ONE: "compact ONE"
-by (rule compact_chfin)
+ by (rule compact_chfin)
text \<open>Case analysis function for type @{typ one}\<close>
-definition
- one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
- "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
+definition one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a"
+ where "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
translations
- "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
- "case x of XCONST ONE :: 'a \<Rightarrow> t" => "CONST one_case\<cdot>t\<cdot>x"
- "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t"
+ "case x of XCONST ONE \<Rightarrow> t" \<rightleftharpoons> "CONST one_case\<cdot>t\<cdot>x"
+ "case x of XCONST ONE :: 'a \<Rightarrow> t" \<rightharpoonup> "CONST one_case\<cdot>t\<cdot>x"
+ "\<Lambda> (XCONST ONE). t" \<rightleftharpoons> "CONST one_case\<cdot>t"
lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
-by (simp add: one_case_def)
+ by (simp add: one_case_def)
lemma one_case2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
-by (simp add: one_case_def)
+ by (simp add: one_case_def)
lemma one_case3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
-by (induct x rule: one_induct) simp_all
+ by (induct x rule: one_induct) simp_all
end
--- a/src/HOL/HOLCF/Pcpo.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,7 +5,7 @@
section \<open>Classes cpo and pcpo\<close>
theory Pcpo
-imports Porder
+ imports Porder
begin
subsection \<open>Complete partial orders\<close>
@@ -29,8 +29,7 @@
lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
-lemma is_lub_thelub:
- "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
+lemma is_lub_thelub: "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])
lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
@@ -42,63 +41,56 @@
lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)"
by (erule below_trans, erule is_ub_thelub)
-lemma lub_range_mono:
- "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule lub_below)
-apply (subgoal_tac "\<exists>j. X i = Y j")
-apply clarsimp
-apply (erule is_ub_thelub)
-apply auto
-done
+lemma lub_range_mono: "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk> \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
+ apply (erule lub_below)
+ apply (subgoal_tac "\<exists>j. X i = Y j")
+ apply clarsimp
+ apply (erule is_ub_thelub)
+ apply auto
+ done
-lemma lub_range_shift:
- "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
-apply (rule below_antisym)
-apply (rule lub_range_mono)
-apply fast
-apply assumption
-apply (erule chain_shift)
-apply (rule lub_below)
-apply assumption
-apply (rule_tac i="i" in below_lub)
-apply (erule chain_shift)
-apply (erule chain_mono)
-apply (rule le_add1)
-done
+lemma lub_range_shift: "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
+ apply (rule below_antisym)
+ apply (rule lub_range_mono)
+ apply fast
+ apply assumption
+ apply (erule chain_shift)
+ apply (rule lub_below)
+ apply assumption
+ apply (rule_tac i="i" in below_lub)
+ apply (erule chain_shift)
+ apply (erule chain_mono)
+ apply (rule le_add1)
+ done
-lemma maxinch_is_thelub:
- "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
-apply (rule iffI)
-apply (fast intro!: lub_eqI lub_finch1)
-apply (unfold max_in_chain_def)
-apply (safe intro!: below_antisym)
-apply (fast elim!: chain_mono)
-apply (drule sym)
-apply (force elim!: is_ub_thelub)
-done
+lemma maxinch_is_thelub: "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
+ apply (rule iffI)
+ apply (fast intro!: lub_eqI lub_finch1)
+ apply (unfold max_in_chain_def)
+ apply (safe intro!: below_antisym)
+ apply (fast elim!: chain_mono)
+ apply (drule sym)
+ apply (force elim!: is_ub_thelub)
+ done
text \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close>
-lemma lub_mono:
- "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-by (fast elim: lub_below below_lub)
+lemma lub_mono: "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
+ by (fast elim: lub_below below_lub)
text \<open>the = relation between two chains is preserved by their lubs\<close>
-lemma lub_eq:
- "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
+lemma lub_eq: "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
by simp
lemma ch2ch_lub:
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
-apply (rule chainI)
-apply (rule lub_mono [OF 2 2])
-apply (rule chainE [OF 1])
-done
+ apply (rule chainI)
+ apply (rule lub_mono [OF 2 2])
+ apply (rule chainE [OF 1])
+ done
lemma diag_lub:
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
@@ -108,7 +100,7 @@
have 3: "chain (\<lambda>i. Y i i)"
apply (rule chainI)
apply (rule below_trans)
- apply (rule chainE [OF 1])
+ apply (rule chainE [OF 1])
apply (rule chainE [OF 2])
done
have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
@@ -118,7 +110,7 @@
apply (rule lub_below [OF 2])
apply (rule below_lub [OF 3])
apply (rule below_trans)
- apply (rule chain_mono [OF 1 max.cobounded1])
+ apply (rule chain_mono [OF 1 max.cobounded1])
apply (rule chain_mono [OF 2 max.cobounded2])
done
show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
@@ -135,6 +127,7 @@
end
+
subsection \<open>Pointed cpos\<close>
text \<open>The class pcpo of pointed cpos\<close>
@@ -147,44 +140,39 @@
where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)"
lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
-unfolding bottom_def
-apply (rule the1I2)
-apply (rule ex_ex1I)
-apply (rule least)
-apply (blast intro: below_antisym)
-apply simp
-done
+ unfolding bottom_def
+ apply (rule the1I2)
+ apply (rule ex_ex1I)
+ apply (rule least)
+ apply (blast intro: below_antisym)
+ apply simp
+ done
end
text \<open>Old "UU" syntax:\<close>
syntax UU :: logic
-
-translations "UU" => "CONST bottom"
+translations "UU" \<rightharpoonup> "CONST bottom"
text \<open>Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}.\<close>
-
-setup \<open>
- Reorient_Proc.add
- (fn Const(@{const_name bottom}, _) => true | _ => false)
-\<close>
-
+setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close>
simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
text \<open>useful lemmas about @{term \<bottom>}\<close>
-lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
-by (simp add: po_eq_conv)
+lemma below_bottom_iff [simp]: "x \<sqsubseteq> \<bottom> \<longleftrightarrow> x = \<bottom>"
+ by (simp add: po_eq_conv)
-lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
-by simp
+lemma eq_bottom_iff: "x = \<bottom> \<longleftrightarrow> x \<sqsubseteq> \<bottom>"
+ by simp
lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
-by (subst eq_bottom_iff)
+ by (subst eq_bottom_iff)
lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
-by (simp only: eq_bottom_iff lub_below_iff)
+ by (simp only: eq_bottom_iff lub_below_iff)
+
subsection \<open>Chain-finite and flat cpos\<close>
@@ -195,10 +183,10 @@
begin
subclass cpo
-apply standard
-apply (frule chfin)
-apply (blast intro: lub_finch1)
-done
+ apply standard
+ apply (frule chfin)
+ apply (blast intro: lub_finch1)
+ done
lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y"
by (simp add: chfin finite_chain_def)
@@ -210,19 +198,18 @@
begin
subclass chfin
-apply standard
-apply (unfold max_in_chain_def)
-apply (case_tac "\<forall>i. Y i = \<bottom>")
-apply simp
-apply simp
-apply (erule exE)
-apply (rule_tac x="i" in exI)
-apply clarify
-apply (blast dest: chain_mono ax_flat)
-done
+ apply standard
+ apply (unfold max_in_chain_def)
+ apply (case_tac "\<forall>i. Y i = \<bottom>")
+ apply simp
+ apply simp
+ apply (erule exE)
+ apply (rule_tac x="i" in exI)
+ apply clarify
+ apply (blast dest: chain_mono ax_flat)
+ done
-lemma flat_below_iff:
- shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
+lemma flat_below_iff: "x \<sqsubseteq> y \<longleftrightarrow> x = \<bottom> \<or> x = y"
by (safe dest!: ax_flat)
lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
@@ -237,7 +224,7 @@
begin
subclass po
-proof qed simp_all
+ by standard simp_all
text \<open>In a discrete cpo, every chain is constant\<close>
@@ -246,19 +233,20 @@
shows "\<exists>x. S = (\<lambda>i. x)"
proof (intro exI ext)
fix i :: nat
- have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono)
- hence "S 0 = S i" by simp
- thus "S i = S 0" by (rule sym)
+ from S le0 have "S 0 \<sqsubseteq> S i" by (rule chain_mono)
+ then have "S 0 = S i" by simp
+ then show "S i = S 0" by (rule sym)
qed
subclass chfin
proof
fix S :: "nat \<Rightarrow> 'a"
assume S: "chain S"
- hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const)
- hence "max_in_chain 0 S"
- unfolding max_in_chain_def by auto
- thus "\<exists>i. max_in_chain i S" ..
+ then have "\<exists>x. S = (\<lambda>i. x)"
+ by (rule discrete_chain_const)
+ then have "max_in_chain 0 S"
+ by (auto simp: max_in_chain_def)
+ then show "\<exists>i. max_in_chain i S" ..
qed
end
--- a/src/HOL/HOLCF/Porder.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Porder.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,7 +5,7 @@
section \<open>Partial orders\<close>
theory Porder
-imports Main
+ imports Main
begin
declare [[typedef_overloaded]]
@@ -23,17 +23,16 @@
notation
below (infix "\<sqsubseteq>" 50)
-abbreviation
- not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<notsqsubseteq>" 50)
+abbreviation not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<notsqsubseteq>" 50)
where "not_below x y \<equiv> \<not> below x y"
notation (ASCII)
not_below (infix "~<<" 50)
-lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+lemma below_eq_trans: "a \<sqsubseteq> b \<Longrightarrow> b = c \<Longrightarrow> a \<sqsubseteq> c"
by (rule subst)
-lemma eq_below_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+lemma eq_below_trans: "a = b \<Longrightarrow> b \<sqsubseteq> c \<Longrightarrow> a \<sqsubseteq> c"
by (rule ssubst)
end
@@ -72,8 +71,8 @@
subsection \<open>Upper bounds\<close>
-definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55) where
- "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)"
+definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55)
+ where "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)"
lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u"
by (simp add: is_ub_def)
@@ -102,13 +101,14 @@
lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y"
unfolding is_ub_def by (fast intro: below_trans)
+
subsection \<open>Least upper bounds\<close>
-definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55) where
- "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
+definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55)
+ where "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
-definition lub :: "'a set \<Rightarrow> 'a" where
- "lub S = (THE x. S <<| x)"
+definition lub :: "'a set \<Rightarrow> 'a"
+ where "lub S = (THE x. S <<| x)"
end
@@ -119,14 +119,13 @@
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10)
translations
- "LUB x:A. t" == "CONST lub ((%x. t) ` A)"
+ "LUB x:A. t" \<rightleftharpoons> "CONST lub ((\<lambda>x. t) ` A)"
context po
begin
-abbreviation
- Lub (binder "\<Squnion>" 10) where
- "\<Squnion>n. t n == lub (range t)"
+abbreviation Lub (binder "\<Squnion>" 10)
+ where "\<Squnion>n. t n \<equiv> lub (range t)"
notation (ASCII)
Lub (binder "LUB " 10)
@@ -147,7 +146,7 @@
text \<open>lubs are unique\<close>
-lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
+lemma is_lub_unique: "S <<| x \<Longrightarrow> S <<| y \<Longrightarrow> x = y"
unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
text \<open>technical lemmas about @{term lub} and @{term is_lub}\<close>
@@ -170,16 +169,17 @@
lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
by (rule is_lub_bin [THEN lub_eqI])
-lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
+lemma is_lub_maximal: "S <| x \<Longrightarrow> x \<in> S \<Longrightarrow> S <<| x"
by (erule is_lubI, erule (1) is_ubD)
-lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
+lemma lub_maximal: "S <| x \<Longrightarrow> x \<in> S \<Longrightarrow> lub S = x"
by (rule is_lub_maximal [THEN lub_eqI])
+
subsection \<open>Countable chains\<close>
-definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
- \<comment> \<open>Here we use countable chains and I prefer to code them as functions!\<close>
+definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
+ where \<comment> \<open>Here we use countable chains and I prefer to code them as functions!\<close>
"chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))"
lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y"
@@ -190,11 +190,11 @@
text \<open>chains are monotone functions\<close>
-lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
+lemma chain_mono_less: "chain Y \<Longrightarrow> i < j \<Longrightarrow> Y i \<sqsubseteq> Y j"
by (erule less_Suc_induct, erule chainE, erule below_trans)
-lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
- by (cases "i = j", simp, simp add: chain_mono_less)
+lemma chain_mono: "chain Y \<Longrightarrow> i \<le> j \<Longrightarrow> Y i \<sqsubseteq> Y j"
+ by (cases "i = j") (simp_all add: chain_mono_less)
lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
by (rule chainI, simp, erule chainE)
@@ -204,20 +204,18 @@
lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
by (rule is_lubD1 [THEN ub_rangeD])
-lemma is_ub_range_shift:
- "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
-apply (rule iffI)
-apply (rule ub_rangeI)
-apply (rule_tac y="S (i + j)" in below_trans)
-apply (erule chain_mono)
-apply (rule le_add1)
-apply (erule ub_rangeD)
-apply (rule ub_rangeI)
-apply (erule ub_rangeD)
-done
+lemma is_ub_range_shift: "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
+ apply (rule iffI)
+ apply (rule ub_rangeI)
+ apply (rule_tac y="S (i + j)" in below_trans)
+ apply (erule chain_mono)
+ apply (rule le_add1)
+ apply (erule ub_rangeD)
+ apply (rule ub_rangeI)
+ apply (erule ub_rangeD)
+ done
-lemma is_lub_range_shift:
- "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
+lemma is_lub_range_shift: "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
by (simp add: is_lub_def is_ub_range_shift)
text \<open>the lub of a constant chain is the constant\<close>
@@ -231,61 +229,60 @@
lemma lub_const [simp]: "(\<Squnion>i. c) = c"
by (rule is_lub_const [THEN lub_eqI])
+
subsection \<open>Finite chains\<close>
-definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" where
- \<comment> \<open>finite chains, needed for monotony of continuous functions\<close>
+definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
+ where \<comment> \<open>finite chains, needed for monotony of continuous functions\<close>
"max_in_chain i C \<longleftrightarrow> (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
-definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
- "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
+definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
+ where "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
text \<open>results about finite chains\<close>
lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y"
unfolding max_in_chain_def by fast
-lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j"
+lemma max_in_chainD: "max_in_chain i Y \<Longrightarrow> i \<le> j \<Longrightarrow> Y i = Y j"
unfolding max_in_chain_def by fast
-lemma finite_chainI:
- "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> finite_chain C"
+lemma finite_chainI: "chain C \<Longrightarrow> max_in_chain i C \<Longrightarrow> finite_chain C"
unfolding finite_chain_def by fast
-lemma finite_chainE:
- "\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+lemma finite_chainE: "\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
unfolding finite_chain_def by fast
-lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i"
-apply (rule is_lubI)
-apply (rule ub_rangeI, rename_tac j)
-apply (rule_tac x=i and y=j in linorder_le_cases)
-apply (drule (1) max_in_chainD, simp)
-apply (erule (1) chain_mono)
-apply (erule ub_rangeD)
-done
+lemma lub_finch1: "chain C \<Longrightarrow> max_in_chain i C \<Longrightarrow> range C <<| C i"
+ apply (rule is_lubI)
+ apply (rule ub_rangeI, rename_tac j)
+ apply (rule_tac x=i and y=j in linorder_le_cases)
+ apply (drule (1) max_in_chainD, simp)
+ apply (erule (1) chain_mono)
+ apply (erule ub_rangeD)
+ done
-lemma lub_finch2:
- "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
-apply (erule finite_chainE)
-apply (erule LeastI2 [where Q="\<lambda>i. range C <<| C i"])
-apply (erule (1) lub_finch1)
-done
+lemma lub_finch2: "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
+ apply (erule finite_chainE)
+ apply (erule LeastI2 [where Q="\<lambda>i. range C <<| C i"])
+ apply (erule (1) lub_finch1)
+ done
lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)"
- apply (erule finite_chainE)
- apply (rule_tac B="Y ` {..i}" in finite_subset)
- apply (rule subsetI)
- apply (erule rangeE, rename_tac j)
- apply (rule_tac x=i and y=j in linorder_le_cases)
- apply (subgoal_tac "Y j = Y i", simp)
- apply (simp add: max_in_chain_def)
+ apply (erule finite_chainE)
+ apply (rule_tac B="Y ` {..i}" in finite_subset)
+ apply (rule subsetI)
+ apply (erule rangeE, rename_tac j)
+ apply (rule_tac x=i and y=j in linorder_le_cases)
+ apply (subgoal_tac "Y j = Y i", simp)
+ apply (simp add: max_in_chain_def)
+ apply simp
apply simp
- apply simp
-done
+ done
lemma finite_range_has_max:
- fixes f :: "nat \<Rightarrow> 'a" and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes f :: "nat \<Rightarrow> 'a"
+ and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
assumes mono: "\<And>i j. i \<le> j \<Longrightarrow> r (f i) (f j)"
assumes finite_range: "finite (range f)"
shows "\<exists>k. \<forall>i. r (f i) (f k)"
@@ -307,38 +304,35 @@
finally show "r (f i) (f ?k)" .
qed
-lemma finite_range_imp_finch:
- "\<lbrakk>chain Y; finite (range Y)\<rbrakk> \<Longrightarrow> finite_chain Y"
- apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k")
- apply (erule exE)
- apply (rule finite_chainI, assumption)
- apply (rule max_in_chainI)
- apply (rule below_antisym)
+lemma finite_range_imp_finch: "chain Y \<Longrightarrow> finite (range Y) \<Longrightarrow> finite_chain Y"
+ apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k")
+ apply (erule exE)
+ apply (rule finite_chainI, assumption)
+ apply (rule max_in_chainI)
+ apply (rule below_antisym)
+ apply (erule (1) chain_mono)
+ apply (erule spec)
+ apply (rule finite_range_has_max)
apply (erule (1) chain_mono)
- apply (erule spec)
- apply (rule finite_range_has_max)
- apply (erule (1) chain_mono)
- apply assumption
-done
+ apply assumption
+ done
lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)"
- by (rule chainI, simp)
+ by (rule chainI) simp
-lemma bin_chainmax:
- "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
- unfolding max_in_chain_def by simp
+lemma bin_chainmax: "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
+ by (simp add: max_in_chain_def)
-lemma is_lub_bin_chain:
- "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
-apply (frule bin_chain)
-apply (drule bin_chainmax)
-apply (drule (1) lub_finch1)
-apply simp
-done
+lemma is_lub_bin_chain: "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
+ apply (frule bin_chain)
+ apply (drule bin_chainmax)
+ apply (drule (1) lub_finch1)
+ apply simp
+ done
text \<open>the maximal element in a chain is its lub\<close>
-lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
+lemma lub_chain_maxelem: "Y i = c \<Longrightarrow> \<forall>i. Y i \<sqsubseteq> c \<Longrightarrow> lub (range Y) = c"
by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)
end
--- a/src/HOL/HOLCF/Product_Cpo.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Product_Cpo.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,26 +5,26 @@
section \<open>The cpo of cartesian products\<close>
theory Product_Cpo
-imports Adm
+ imports Adm
begin
default_sort cpo
+
subsection \<open>Unit type is a pcpo\<close>
instantiation unit :: discrete_cpo
begin
-definition
- below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
+definition below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
-instance proof
-qed simp
+instance
+ by standard simp
end
instance unit :: pcpo
-by intro_classes simp
+ by standard simp
subsection \<open>Product type is a partial order\<close>
@@ -32,182 +32,185 @@
instantiation prod :: (below, below) below
begin
-definition
- below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
+definition below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
instance ..
+
end
instance prod :: (po, po) po
proof
fix x :: "'a \<times> 'b"
show "x \<sqsubseteq> x"
- unfolding below_prod_def by simp
+ by (simp add: below_prod_def)
next
fix x y :: "'a \<times> 'b"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
+ assume "x \<sqsubseteq> y" "y \<sqsubseteq> x"
+ then show "x = y"
unfolding below_prod_def prod_eq_iff
by (fast intro: below_antisym)
next
fix x y z :: "'a \<times> 'b"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+ assume "x \<sqsubseteq> y" "y \<sqsubseteq> z"
+ then show "x \<sqsubseteq> z"
unfolding below_prod_def
by (fast intro: below_trans)
qed
+
subsection \<open>Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
-lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
-unfolding below_prod_def by simp
+lemma prod_belowI: "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
+ by (simp add: below_prod_def)
lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
-unfolding below_prod_def by simp
+ by (simp add: below_prod_def)
text \<open>Pair \<open>(_,_)\<close> is monotone in both arguments\<close>
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
-by (simp add: monofun_def)
+ by (simp add: monofun_def)
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
-by (simp add: monofun_def)
+ by (simp add: monofun_def)
-lemma monofun_pair:
- "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
-by simp
+lemma monofun_pair: "x1 \<sqsubseteq> x2 \<Longrightarrow> y1 \<sqsubseteq> y2 \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
+ by simp
-lemma ch2ch_Pair [simp]:
- "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
-by (rule chainI, simp add: chainE)
+lemma ch2ch_Pair [simp]: "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
+ by (rule chainI, simp add: chainE)
text \<open>@{term fst} and @{term snd} are monotone\<close>
lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
-unfolding below_prod_def by simp
+ by (simp add: below_prod_def)
lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y"
-unfolding below_prod_def by simp
+ by (simp add: below_prod_def)
lemma monofun_fst: "monofun fst"
-by (simp add: monofun_def below_prod_def)
+ by (simp add: monofun_def below_prod_def)
lemma monofun_snd: "monofun snd"
-by (simp add: monofun_def below_prod_def)
+ by (simp add: monofun_def below_prod_def)
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
lemma prod_chain_cases:
- assumes "chain Y"
+ assumes chain: "chain Y"
obtains A B
where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
proof
- from \<open>chain Y\<close> show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
- from \<open>chain Y\<close> show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
- show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
+ from chain show "chain (\<lambda>i. fst (Y i))"
+ by (rule ch2ch_fst)
+ from chain show "chain (\<lambda>i. snd (Y i))"
+ by (rule ch2ch_snd)
+ show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))"
+ by simp
qed
+
subsection \<open>Product type is a cpo\<close>
-lemma is_lub_Pair:
- "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
-unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
+lemma is_lub_Pair: "range A <<| x \<Longrightarrow> range B <<| y \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
+ by (simp add: is_lub_def is_ub_def below_prod_def)
-lemma lub_Pair:
- "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
-by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
+lemma lub_Pair: "chain A \<Longrightarrow> chain B \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
+ for A :: "nat \<Rightarrow> 'a::cpo" and B :: "nat \<Rightarrow> 'b::cpo"
+ by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
lemma is_lub_prod:
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
- assumes S: "chain S"
+ assumes "chain S"
shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
+ using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI)
-lemma lub_prod:
- "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
- \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-by (rule is_lub_prod [THEN lub_eqI])
+lemma lub_prod: "chain S \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
+ for S :: "nat \<Rightarrow> 'a::cpo \<times> 'b::cpo"
+ by (rule is_lub_prod [THEN lub_eqI])
instance prod :: (cpo, cpo) cpo
proof
fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
assume "chain S"
- hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
+ then have "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
by (rule is_lub_prod)
- thus "\<exists>x. range S <<| x" ..
+ then show "\<exists>x. range S <<| x" ..
qed
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
proof
fix x y :: "'a \<times> 'b"
show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
- unfolding below_prod_def prod_eq_iff
- by simp
+ by (simp add: below_prod_def prod_eq_iff)
qed
+
subsection \<open>Product type is pointed\<close>
lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
-by (simp add: below_prod_def)
+ by (simp add: below_prod_def)
instance prod :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_prod)
+ by intro_classes (fast intro: minimal_prod)
lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_prod [THEN bottomI, symmetric])
+ by (rule minimal_prod [THEN bottomI, symmetric])
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-unfolding inst_prod_pcpo by simp
+ by (simp add: inst_prod_pcpo)
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
-unfolding inst_prod_pcpo by (rule fst_conv)
+ unfolding inst_prod_pcpo by (rule fst_conv)
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
-unfolding inst_prod_pcpo by (rule snd_conv)
+ unfolding inst_prod_pcpo by (rule snd_conv)
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
-by simp
+ by simp
lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
-unfolding split_def by simp
+ by (simp add: split_def)
+
subsection \<open>Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (erule cpo_lubI)
-apply (rule is_lub_const)
-done
+ apply (rule contI)
+ apply (rule is_lub_Pair)
+ apply (erule cpo_lubI)
+ apply (rule is_lub_const)
+ done
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (rule is_lub_const)
-apply (erule cpo_lubI)
-done
+ apply (rule contI)
+ apply (rule is_lub_Pair)
+ apply (rule is_lub_const)
+ apply (erule cpo_lubI)
+ done
lemma cont_fst: "cont fst"
-apply (rule contI)
-apply (simp add: lub_prod)
-apply (erule cpo_lubI [OF ch2ch_fst])
-done
+ apply (rule contI)
+ apply (simp add: lub_prod)
+ apply (erule cpo_lubI [OF ch2ch_fst])
+ done
lemma cont_snd: "cont snd"
-apply (rule contI)
-apply (simp add: lub_prod)
-apply (erule cpo_lubI [OF ch2ch_snd])
-done
+ apply (rule contI)
+ apply (simp add: lub_prod)
+ apply (erule cpo_lubI [OF ch2ch_snd])
+ done
lemma cont2cont_Pair [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. (f x, g x))"
-apply (rule cont_apply [OF f cont_pair1])
-apply (rule cont_apply [OF g cont_pair2])
-apply (rule cont_const)
-done
+ apply (rule cont_apply [OF f cont_pair1])
+ apply (rule cont_apply [OF g cont_pair2])
+ apply (rule cont_const)
+ done
lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
@@ -219,13 +222,13 @@
assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
-unfolding split_def
-apply (rule cont_apply [OF g])
-apply (rule cont_apply [OF cont_fst f2])
-apply (rule cont_apply [OF cont_snd f3])
-apply (rule cont_const)
-apply (rule f1)
-done
+ unfolding split_def
+ apply (rule cont_apply [OF g])
+ apply (rule cont_apply [OF cont_fst f2])
+ apply (rule cont_apply [OF cont_snd f3])
+ apply (rule cont_const)
+ apply (rule f1)
+ done
lemma prod_contI:
assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
@@ -234,66 +237,68 @@
proof -
have "cont (\<lambda>(x, y). f (x, y))"
by (intro cont2cont_case_prod f1 f2 cont2cont)
- thus "cont f"
+ then show "cont f"
by (simp only: case_prod_eta)
qed
-lemma prod_cont_iff:
- "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
-apply safe
-apply (erule cont_compose [OF _ cont_pair1])
-apply (erule cont_compose [OF _ cont_pair2])
-apply (simp only: prod_contI)
-done
+lemma prod_cont_iff: "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
+ apply safe
+ apply (erule cont_compose [OF _ cont_pair1])
+ apply (erule cont_compose [OF _ cont_pair2])
+ apply (simp only: prod_contI)
+ done
lemma cont2cont_case_prod' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. case_prod (f x) (g x))"
-using assms by (simp add: cont2cont_case_prod prod_cont_iff)
+ using assms by (simp add: cont2cont_case_prod prod_cont_iff)
text \<open>The simple version (due to Joachim Breitner) is needed if
either element type of the pair is not a cpo.\<close>
lemma cont2cont_split_simple [simp, cont2cont]:
- assumes "\<And>a b. cont (\<lambda>x. f x a b)"
- shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
-using assms by (cases p) auto
+ assumes "\<And>a b. cont (\<lambda>x. f x a b)"
+ shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
+ using assms by (cases p) auto
text \<open>Admissibility of predicates on product types.\<close>
lemma adm_case_prod [simp]:
assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
-unfolding case_prod_beta using assms .
+ unfolding case_prod_beta using assms .
+
subsection \<open>Compactness and chain-finiteness\<close>
-lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
-unfolding below_prod_def by simp
+lemma fst_below_iff: "fst x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
+ for x :: "'a \<times> 'b"
+ by (simp add: below_prod_def)
-lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
-unfolding below_prod_def by simp
+lemma snd_below_iff: "snd x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
+ for x :: "'a \<times> 'b"
+ by (simp add: below_prod_def)
lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
-by (rule compactI, simp add: fst_below_iff)
+ by (rule compactI) (simp add: fst_below_iff)
lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
-by (rule compactI, simp add: snd_below_iff)
+ by (rule compactI) (simp add: snd_below_iff)
-lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
-by (rule compactI, simp add: below_prod_def)
+lemma compact_Pair: "compact x \<Longrightarrow> compact y \<Longrightarrow> compact (x, y)"
+ by (rule compactI) (simp add: below_prod_def)
lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
-apply (safe intro!: compact_Pair)
-apply (drule compact_fst, simp)
-apply (drule compact_snd, simp)
-done
+ apply (safe intro!: compact_Pair)
+ apply (drule compact_fst, simp)
+ apply (drule compact_snd, simp)
+ done
instance prod :: (chfin, chfin) chfin
-apply intro_classes
-apply (erule compact_imp_max_in_chain)
-apply (case_tac "\<Squnion>i. Y i", simp)
-done
+ apply intro_classes
+ apply (erule compact_imp_max_in_chain)
+ apply (case_tac "\<Squnion>i. Y i", simp)
+ done
end
--- a/src/HOL/HOLCF/Sfun.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Sfun.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,30 +5,25 @@
section \<open>The Strict Function Type\<close>
theory Sfun
-imports Cfun
+ imports Cfun
begin
-pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0)
- = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
-by simp_all
+pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
+ by simp_all
type_notation (ASCII)
sfun (infixr "->!" 0)
text \<open>TODO: Define nice syntax for abstraction, application.\<close>
-definition
- sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
-where
- "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
+definition sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
+ where "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
-definition
- sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
-where
- "sfun_rep = (\<Lambda> f. Rep_sfun f)"
+definition sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
+ where "sfun_rep = (\<Lambda> f. Rep_sfun f)"
lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
- unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
+ by (simp add: sfun_rep_def cont_Rep_sfun)
lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
unfolding sfun_rep_beta by (rule Rep_sfun_strict)
@@ -54,9 +49,9 @@
done
lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g"
-by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)
+ by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)
lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g"
-by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)
+ by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)
end
--- a/src/HOL/HOLCF/Sprod.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Sprod.thy Mon Jan 01 23:07:24 2018 +0100
@@ -6,20 +6,21 @@
section \<open>The type of strict products\<close>
theory Sprod
-imports Cfun
+ imports Cfun
begin
default_sort pcpo
+
subsection \<open>Definition of strict product type\<close>
definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
pcpodef ('a, 'b) sprod ("(_ \<otimes>/ _)" [21,20] 20) = "sprod :: ('a \<times> 'b) set"
- unfolding sprod_def by simp_all
+ by (simp_all add: sprod_def)
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])
+ by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])
type_notation (ASCII)
sprod (infixr "**" 20)
@@ -27,39 +28,34 @@
subsection \<open>Definitions of constants\<close>
-definition
- sfst :: "('a ** 'b) \<rightarrow> 'a" where
- "sfst = (\<Lambda> p. fst (Rep_sprod p))"
+definition sfst :: "('a ** 'b) \<rightarrow> 'a"
+ where "sfst = (\<Lambda> p. fst (Rep_sprod p))"
-definition
- ssnd :: "('a ** 'b) \<rightarrow> 'b" where
- "ssnd = (\<Lambda> p. snd (Rep_sprod p))"
+definition ssnd :: "('a ** 'b) \<rightarrow> 'b"
+ where "ssnd = (\<Lambda> p. snd (Rep_sprod p))"
-definition
- spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
- "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))"
+definition spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)"
+ where "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))"
-definition
- ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
- "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
+definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
+ where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
-syntax
- "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))")
+syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))")
+translations
+ "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
+ "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
translations
- "(:x, y, z:)" == "(:x, (:y, z:):)"
- "(:x, y:)" == "CONST spair\<cdot>x\<cdot>y"
+ "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" \<rightleftharpoons> "CONST ssplit\<cdot>(\<Lambda> x y. t)"
-translations
- "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
subsection \<open>Case analysis\<close>
lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod"
-by (simp add: sprod_def seq_conv_if)
+ by (simp add: sprod_def seq_conv_if)
lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)"
-by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
+ by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
lemmas Rep_sprod_simps =
Rep_sprod_inject [symmetric] below_sprod_def
@@ -68,144 +64,139 @@
lemma sprodE [case_names bottom spair, cases type: sprod]:
obtains "p = \<bottom>" | x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>"
-using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps)
+ using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps)
lemma sprod_induct [case_names bottom spair, induct type: sprod]:
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
-by (cases x, simp_all)
+ by (cases x) simp_all
+
subsection \<open>Properties of \emph{spair}\<close>
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
-by (simp add: Rep_sprod_simps)
+ by (simp add: Rep_sprod_simps)
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
-by (simp add: Rep_sprod_simps)
+ by (simp add: Rep_sprod_simps)
-lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
-by (simp add: Rep_sprod_simps seq_conv_if)
+lemma spair_bottom_iff [simp]: "(:x, y:) = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>"
+ by (simp add: Rep_sprod_simps seq_conv_if)
-lemma spair_below_iff:
- "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
-by (simp add: Rep_sprod_simps seq_conv_if)
+lemma spair_below_iff: "(:a, b:) \<sqsubseteq> (:c, d:) \<longleftrightarrow> a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
+ by (simp add: Rep_sprod_simps seq_conv_if)
-lemma spair_eq_iff:
- "((:a, b:) = (:c, d:)) =
- (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
-by (simp add: Rep_sprod_simps seq_conv_if)
+lemma spair_eq_iff: "(:a, b:) = (:c, d:) \<longleftrightarrow> a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>)"
+ by (simp add: Rep_sprod_simps seq_conv_if)
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
-by simp
+ by simp
lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
-by simp
+ by simp
lemma spair_defined: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
-by simp
+ by simp
lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
-by simp
+ by simp
-lemma spair_below:
- "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
-by (simp add: spair_below_iff)
+lemma spair_below: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) \<longleftrightarrow> x \<sqsubseteq> a \<and> y \<sqsubseteq> b"
+ by (simp add: spair_below_iff)
-lemma spair_eq:
- "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)"
-by (simp add: spair_eq_iff)
+lemma spair_eq: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> (:x, y:) = (:a, b:) \<longleftrightarrow> x = a \<and> y = b"
+ by (simp add: spair_eq_iff)
-lemma spair_inject:
- "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b"
-by (rule spair_eq [THEN iffD1])
+lemma spair_inject: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> (:x, y:) = (:a, b:) \<Longrightarrow> x = a \<and> y = b"
+ by (rule spair_eq [THEN iffD1])
lemma inst_sprod_pcpo2: "\<bottom> = (:\<bottom>, \<bottom>:)"
-by simp
+ by simp
lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
-by (cases p, simp only: inst_sprod_pcpo2, simp)
+ by (cases p) (simp only: inst_sprod_pcpo2, simp)
+
subsection \<open>Properties of \emph{sfst} and \emph{ssnd}\<close>
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
-by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict)
+ by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict)
lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
-by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict)
+ by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict)
lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
-by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair)
+ by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair)
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
-by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
+ by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
-lemma sfst_bottom_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
-by (cases p, simp_all)
+lemma sfst_bottom_iff [simp]: "sfst\<cdot>p = \<bottom> \<longleftrightarrow> p = \<bottom>"
+ by (cases p) simp_all
-lemma ssnd_bottom_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
-by (cases p, simp_all)
+lemma ssnd_bottom_iff [simp]: "ssnd\<cdot>p = \<bottom> \<longleftrightarrow> p = \<bottom>"
+ by (cases p) simp_all
lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
-by simp
+ by simp
lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
-by simp
+ by simp
lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
-by (cases p, simp_all)
+ by (cases p) simp_all
-lemma below_sprod: "(x \<sqsubseteq> y) = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
-by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)
+lemma below_sprod: "x \<sqsubseteq> y \<longleftrightarrow> sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y"
+ by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)
-lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
-by (auto simp add: po_eq_conv below_sprod)
+lemma eq_sprod: "x = y \<longleftrightarrow> sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y"
+ by (auto simp add: po_eq_conv below_sprod)
lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
-apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
-apply (simp add: below_sprod)
-done
+ by (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp, simp add: below_sprod)
lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:sfst\<cdot>x, y:)"
-apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
-apply (simp add: below_sprod)
-done
+ by (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp, simp add: below_sprod)
+
subsection \<open>Compactness\<close>
lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)"
-by (rule compactI, simp add: sfst_below_iff)
+ by (rule compactI) (simp add: sfst_below_iff)
lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)"
-by (rule compactI, simp add: ssnd_below_iff)
+ by (rule compactI) (simp add: ssnd_below_iff)
-lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
-by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if)
+lemma compact_spair: "compact x \<Longrightarrow> compact y \<Longrightarrow> compact (:x, y:)"
+ by (rule compact_sprod) (simp add: Rep_sprod_spair seq_conv_if)
-lemma compact_spair_iff:
- "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"
-apply (safe elim!: compact_spair)
-apply (drule compact_sfst, simp)
-apply (drule compact_ssnd, simp)
-apply simp
-apply simp
-done
+lemma compact_spair_iff: "compact (:x, y:) \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y)"
+ apply (safe elim!: compact_spair)
+ apply (drule compact_sfst, simp)
+ apply (drule compact_ssnd, simp)
+ apply simp
+ apply simp
+ done
+
subsection \<open>Properties of \emph{ssplit}\<close>
lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by (simp add: ssplit_def)
+ by (simp add: ssplit_def)
-lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y"
-by (simp add: ssplit_def)
+lemma ssplit2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y"
+ by (simp add: ssplit_def)
lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
-by (cases z, simp_all)
+ by (cases z) simp_all
+
subsection \<open>Strict product preserves flatness\<close>
instance sprod :: (flat, flat) flat
proof
fix x y :: "'a \<otimes> 'b"
- assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
+ assume "x \<sqsubseteq> y"
+ then show "x = \<bottom> \<or> x = y"
apply (induct x, simp)
apply (induct y, simp)
apply (simp add: spair_below_iff flat_below_iff)
--- a/src/HOL/HOLCF/Ssum.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Ssum.thy Mon Jan 01 23:07:24 2018 +0100
@@ -6,24 +6,24 @@
section \<open>The type of strict sums\<close>
theory Ssum
-imports Tr
+ imports Tr
begin
default_sort pcpo
+
subsection \<open>Definition of strict sum type\<close>
-definition
- "ssum =
- {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
- (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
- (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
+definition "ssum =
+ {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
+ (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
+ (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
pcpodef ('a, 'b) ssum ("(_ \<oplus>/ _)" [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
- unfolding ssum_def by simp_all
+ by (simp_all add: ssum_def)
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
+ by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
type_notation (ASCII)
ssum (infixr "++" 10)
@@ -31,108 +31,108 @@
subsection \<open>Definitions of constructors\<close>
-definition
- sinl :: "'a \<rightarrow> ('a ++ 'b)" where
- "sinl = (\<Lambda> a. Abs_ssum (seq\<cdot>a\<cdot>TT, a, \<bottom>))"
+definition sinl :: "'a \<rightarrow> ('a ++ 'b)"
+ where "sinl = (\<Lambda> a. Abs_ssum (seq\<cdot>a\<cdot>TT, a, \<bottom>))"
-definition
- sinr :: "'b \<rightarrow> ('a ++ 'b)" where
- "sinr = (\<Lambda> b. Abs_ssum (seq\<cdot>b\<cdot>FF, \<bottom>, b))"
+definition sinr :: "'b \<rightarrow> ('a ++ 'b)"
+ where "sinr = (\<Lambda> b. Abs_ssum (seq\<cdot>b\<cdot>FF, \<bottom>, b))"
lemma sinl_ssum: "(seq\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
-by (simp add: ssum_def seq_conv_if)
+ by (simp add: ssum_def seq_conv_if)
lemma sinr_ssum: "(seq\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
-by (simp add: ssum_def seq_conv_if)
+ by (simp add: ssum_def seq_conv_if)
lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (seq\<cdot>a\<cdot>TT, a, \<bottom>)"
-by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
+ by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (seq\<cdot>b\<cdot>FF, \<bottom>, b)"
-by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
+ by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
lemmas Rep_ssum_simps =
Rep_ssum_inject [symmetric] below_ssum_def
prod_eq_iff below_prod_def
Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
+
subsection \<open>Properties of \emph{sinl} and \emph{sinr}\<close>
text \<open>Ordering\<close>
-lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps seq_conv_if)
+lemma sinl_below [simp]: "sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
+ by (simp add: Rep_ssum_simps seq_conv_if)
-lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps seq_conv_if)
+lemma sinr_below [simp]: "sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
+ by (simp add: Rep_ssum_simps seq_conv_if)
-lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps seq_conv_if)
+lemma sinl_below_sinr [simp]: "sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y \<longleftrightarrow> x = \<bottom>"
+ by (simp add: Rep_ssum_simps seq_conv_if)
-lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps seq_conv_if)
+lemma sinr_below_sinl [simp]: "sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y \<longleftrightarrow> x = \<bottom>"
+ by (simp add: Rep_ssum_simps seq_conv_if)
text \<open>Equality\<close>
-lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
-by (simp add: po_eq_conv)
+lemma sinl_eq [simp]: "sinl\<cdot>x = sinl\<cdot>y \<longleftrightarrow> x = y"
+ by (simp add: po_eq_conv)
-lemma sinr_eq [simp]: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
-by (simp add: po_eq_conv)
+lemma sinr_eq [simp]: "sinr\<cdot>x = sinr\<cdot>y \<longleftrightarrow> x = y"
+ by (simp add: po_eq_conv)
-lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
-by (subst po_eq_conv, simp)
+lemma sinl_eq_sinr [simp]: "sinl\<cdot>x = sinr\<cdot>y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+ by (subst po_eq_conv) simp
-lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
-by (subst po_eq_conv, simp)
+lemma sinr_eq_sinl [simp]: "sinr\<cdot>x = sinl\<cdot>y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+ by (subst po_eq_conv) simp
lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
-by (rule sinl_eq [THEN iffD1])
+ by (rule sinl_eq [THEN iffD1])
lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
-by (rule sinr_eq [THEN iffD1])
+ by (rule sinr_eq [THEN iffD1])
text \<open>Strictness\<close>
lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
-by (simp add: Rep_ssum_simps)
+ by (simp add: Rep_ssum_simps)
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
-by (simp add: Rep_ssum_simps)
+ by (simp add: Rep_ssum_simps)
-lemma sinl_bottom_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
-using sinl_eq [of "x" "\<bottom>"] by simp
+lemma sinl_bottom_iff [simp]: "sinl\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
+ using sinl_eq [of "x" "\<bottom>"] by simp
-lemma sinr_bottom_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
-using sinr_eq [of "x" "\<bottom>"] by simp
+lemma sinr_bottom_iff [simp]: "sinr\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
+ using sinr_eq [of "x" "\<bottom>"] by simp
lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
-by simp
+ by simp
lemma sinr_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
-by simp
+ by simp
text \<open>Compactness\<close>
lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
-by (rule compact_ssum, simp add: Rep_ssum_sinl)
+ by (rule compact_ssum) (simp add: Rep_ssum_sinl)
lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
-by (rule compact_ssum, simp add: Rep_ssum_sinr)
+ by (rule compact_ssum) (simp add: Rep_ssum_sinr)
lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
-unfolding compact_def
-by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)
+ unfolding compact_def
+ by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)
lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x"
-unfolding compact_def
-by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)
+ unfolding compact_def
+ by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)
lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x"
-by (safe elim!: compact_sinl compact_sinlD)
+ by (safe elim!: compact_sinl compact_sinlD)
lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x"
-by (safe elim!: compact_sinr compact_sinrD)
+ by (safe elim!: compact_sinr compact_sinrD)
+
subsection \<open>Case analysis\<close>
@@ -140,61 +140,61 @@
obtains "p = \<bottom>"
| x where "p = sinl\<cdot>x" and "x \<noteq> \<bottom>"
| y where "p = sinr\<cdot>y" and "y \<noteq> \<bottom>"
-using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps)
+ using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps)
lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
"\<lbrakk>P \<bottom>;
\<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
\<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
-by (cases x, simp_all)
+ by (cases x) simp_all
lemma ssumE2 [case_names sinl sinr]:
"\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-by (cases p, simp only: sinl_strict [symmetric], simp, simp)
+ by (cases p, simp only: sinl_strict [symmetric], simp, simp)
lemma below_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
-by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
+ by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
-by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
+ by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
+
subsection \<open>Case analysis combinator\<close>
-definition
- sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
- "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))"
+definition sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
+ where "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))"
translations
- "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
- "case s of (XCONST sinl :: 'a)\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" => "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+ "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" \<rightleftharpoons> "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+ "case s of (XCONST sinl :: 'a)\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" \<rightharpoonup> "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
translations
- "\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
- "\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
+ "\<Lambda>(XCONST sinl\<cdot>x). t" \<rightleftharpoons> "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
+ "\<Lambda>(XCONST sinr\<cdot>y). t" \<rightleftharpoons> "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
-lemma beta_sscase:
- "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
-unfolding sscase_def by (simp add: cont_Rep_ssum)
+lemma beta_sscase: "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
+ by (simp add: sscase_def cont_Rep_ssum)
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
-unfolding beta_sscase by (simp add: Rep_ssum_strict)
+ by (simp add: beta_sscase Rep_ssum_strict)
lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x"
-unfolding beta_sscase by (simp add: Rep_ssum_sinl)
+ by (simp add: beta_sscase Rep_ssum_sinl)
lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y"
-unfolding beta_sscase by (simp add: Rep_ssum_sinr)
+ by (simp add: beta_sscase Rep_ssum_sinr)
lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
-by (cases z, simp_all)
+ by (cases z) simp_all
+
subsection \<open>Strict sum preserves flatness\<close>
instance ssum :: (flat, flat) flat
-apply (intro_classes, clarify)
-apply (case_tac x, simp)
-apply (case_tac y, simp_all add: flat_below_iff)
-apply (case_tac y, simp_all add: flat_below_iff)
-done
+ apply (intro_classes, clarify)
+ apply (case_tac x, simp)
+ apply (case_tac y, simp_all add: flat_below_iff)
+ apply (case_tac y, simp_all add: flat_below_iff)
+ done
end
--- a/src/HOL/HOLCF/Tr.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Tr.thy Mon Jan 01 23:07:24 2018 +0100
@@ -5,107 +5,97 @@
section \<open>The type of lifted booleans\<close>
theory Tr
-imports Lift
+ imports Lift
begin
subsection \<open>Type definition and constructors\<close>
-type_synonym
- tr = "bool lift"
+type_synonym tr = "bool lift"
translations
- (type) "tr" <= (type) "bool lift"
+ (type) "tr" \<leftharpoondown> (type) "bool lift"
-definition
- TT :: "tr" where
- "TT = Def True"
+definition TT :: "tr"
+ where "TT = Def True"
-definition
- FF :: "tr" where
- "FF = Def False"
+definition FF :: "tr"
+ where "FF = Def False"
text \<open>Exhaustion and Elimination for type @{typ tr}\<close>
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
-unfolding FF_def TT_def by (induct t) auto
+ by (induct t) (auto simp: FF_def TT_def)
lemma trE [case_names bottom TT FF, cases type: tr]:
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-unfolding FF_def TT_def by (induct p) auto
+ by (induct p) (auto simp: FF_def TT_def)
lemma tr_induct [case_names bottom TT FF, induct type: tr]:
- "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
-by (cases x) simp_all
+ "P \<bottom> \<Longrightarrow> P TT \<Longrightarrow> P FF \<Longrightarrow> P x"
+ by (cases x) simp_all
text \<open>distinctness for type @{typ tr}\<close>
lemma dist_below_tr [simp]:
"TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
-unfolding TT_def FF_def by simp_all
+ by (simp_all add: TT_def FF_def)
-lemma dist_eq_tr [simp]:
- "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
-unfolding TT_def FF_def by simp_all
+lemma dist_eq_tr [simp]: "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
+ by (simp_all add: TT_def FF_def)
lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
-by (induct x) simp_all
+ by (induct x) simp_all
lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
-by (induct x) simp_all
+ by (induct x) simp_all
lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
-by (induct x) simp_all
+ by (induct x) simp_all
lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
-by (induct x) simp_all
+ by (induct x) simp_all
subsection \<open>Case analysis\<close>
default_sort pcpo
-definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" where
- "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
+definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a"
+ where "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
-abbreviation
- cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
-where
- "If b then e1 else e2 == tr_case\<cdot>e1\<cdot>e2\<cdot>b"
+abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
+ where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b"
translations
- "\<Lambda> (XCONST TT). t" == "CONST tr_case\<cdot>t\<cdot>\<bottom>"
- "\<Lambda> (XCONST FF). t" == "CONST tr_case\<cdot>\<bottom>\<cdot>t"
+ "\<Lambda> (XCONST TT). t" \<rightleftharpoons> "CONST tr_case\<cdot>t\<cdot>\<bottom>"
+ "\<Lambda> (XCONST FF). t" \<rightleftharpoons> "CONST tr_case\<cdot>\<bottom>\<cdot>t"
lemma ifte_thms [simp]:
"If \<bottom> then e1 else e2 = \<bottom>"
"If FF then e1 else e2 = e2"
"If TT then e1 else e2 = e1"
-by (simp_all add: tr_case_def TT_def FF_def)
+ by (simp_all add: tr_case_def TT_def FF_def)
subsection \<open>Boolean connectives\<close>
-definition
- trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
- andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
-abbreviation
- andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where
- "x andalso y == trand\<cdot>x\<cdot>y"
+definition trand :: "tr \<rightarrow> tr \<rightarrow> tr"
+ where andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
+
+abbreviation andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35)
+ where "x andalso y \<equiv> trand\<cdot>x\<cdot>y"
+
+definition tror :: "tr \<rightarrow> tr \<rightarrow> tr"
+ where orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
-definition
- tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
- orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
-abbreviation
- orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where
- "x orelse y == tror\<cdot>x\<cdot>y"
+abbreviation orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30)
+ where "x orelse y \<equiv> tror\<cdot>x\<cdot>y"
-definition
- neg :: "tr \<rightarrow> tr" where
- "neg = flift2 Not"
+definition neg :: "tr \<rightarrow> tr"
+ where "neg = flift2 Not"
-definition
- If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
- "If2 Q x y = (If Q then x else y)"
+definition If2 :: "tr \<Rightarrow> 'c \<Rightarrow> 'c \<Rightarrow> 'c"
+ where "If2 Q x y = (If Q then x else y)"
text \<open>tactic for tr-thms with case split\<close>
@@ -119,10 +109,10 @@
"(\<bottom> andalso y) = \<bottom>"
"(y andalso TT) = y"
"(y andalso y) = y"
-apply (unfold andalso_def, simp_all)
-apply (cases y, simp_all)
-apply (cases y, simp_all)
-done
+ apply (unfold andalso_def, simp_all)
+ apply (cases y, simp_all)
+ apply (cases y, simp_all)
+ done
lemma orelse_thms [simp]:
"(TT orelse y) = TT"
@@ -130,25 +120,21 @@
"(\<bottom> orelse y) = \<bottom>"
"(y orelse FF) = y"
"(y orelse y) = y"
-apply (unfold orelse_def, simp_all)
-apply (cases y, simp_all)
-apply (cases y, simp_all)
-done
+ apply (unfold orelse_def, simp_all)
+ apply (cases y, simp_all)
+ apply (cases y, simp_all)
+ done
lemma neg_thms [simp]:
"neg\<cdot>TT = FF"
"neg\<cdot>FF = TT"
"neg\<cdot>\<bottom> = \<bottom>"
-by (simp_all add: neg_def TT_def FF_def)
+ by (simp_all add: neg_def TT_def FF_def)
text \<open>split-tac for If via If2 because the constant has to be a constant\<close>
-lemma split_If2:
- "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
-apply (unfold If2_def)
-apply (cases Q)
-apply (simp_all)
-done
+lemma split_If2: "P (If2 Q x y) \<longleftrightarrow> ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
+ by (cases Q) (simp_all add: If2_def)
(* FIXME unused!? *)
ML \<open>
@@ -159,42 +145,34 @@
subsection "Rewriting of HOLCF operations to HOL functions"
-lemma andalso_or:
- "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
-apply (cases t)
-apply simp_all
-done
+lemma andalso_or: "t \<noteq> \<bottom> \<Longrightarrow> (t andalso s) = FF \<longleftrightarrow> t = FF \<or> s = FF"
+ by (cases t) simp_all
-lemma andalso_and:
- "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
-apply (cases t)
-apply simp_all
-done
+lemma andalso_and: "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) \<longleftrightarrow> t \<noteq> FF \<and> s \<noteq> FF"
+ by (cases t) simp_all
-lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
-by (simp add: FF_def)
+lemma Def_bool1 [simp]: "Def x \<noteq> FF \<longleftrightarrow> x"
+ by (simp add: FF_def)
-lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
-by (simp add: FF_def)
+lemma Def_bool2 [simp]: "Def x = FF \<longleftrightarrow> \<not> x"
+ by (simp add: FF_def)
-lemma Def_bool3 [simp]: "(Def x = TT) = x"
-by (simp add: TT_def)
+lemma Def_bool3 [simp]: "Def x = TT \<longleftrightarrow> x"
+ by (simp add: TT_def)
-lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
-by (simp add: TT_def)
+lemma Def_bool4 [simp]: "Def x \<noteq> TT \<longleftrightarrow> \<not> x"
+ by (simp add: TT_def)
-lemma If_and_if:
- "(If Def P then A else B) = (if P then A else B)"
-apply (cases "Def P")
-apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
-done
+lemma If_and_if: "(If Def P then A else B) = (if P then A else B)"
+ by (cases "Def P") (auto simp add: TT_def[symmetric] FF_def[symmetric])
+
subsection \<open>Compactness\<close>
lemma compact_TT: "compact TT"
-by (rule compact_chfin)
+ by (rule compact_chfin)
lemma compact_FF: "compact FF"
-by (rule compact_chfin)
+ by (rule compact_chfin)
end
--- a/src/HOL/HOLCF/Up.thy Mon Jan 01 21:17:28 2018 +0100
+++ b/src/HOL/HOLCF/Up.thy Mon Jan 01 23:07:24 2018 +0100
@@ -6,40 +6,47 @@
section \<open>The type of lifted values\<close>
theory Up
-imports Cfun
+ imports Cfun
begin
default_sort cpo
+
subsection \<open>Definition of new type for lifting\<close>
datatype 'a u ("(_\<^sub>\<bottom>)" [1000] 999) = Ibottom | Iup 'a
-primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
+primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
+ where
"Ifup f Ibottom = \<bottom>"
- | "Ifup f (Iup x) = f\<cdot>x"
+ | "Ifup f (Iup x) = f\<cdot>x"
+
subsection \<open>Ordering on lifted cpo\<close>
instantiation u :: (cpo) below
begin
-definition
- below_up_def:
- "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
- (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
+definition below_up_def:
+ "(op \<sqsubseteq>) \<equiv>
+ (\<lambda>x y.
+ (case x of
+ Ibottom \<Rightarrow> True
+ | Iup a \<Rightarrow> (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b)))"
instance ..
+
end
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
-by (simp add: below_up_def)
+ by (simp add: below_up_def)
lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"
-by (simp add: below_up_def)
+ by (simp add: below_up_def)
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
-by (simp add: below_up_def)
+ by (simp add: below_up_def)
+
subsection \<open>Lifted cpo is a partial order\<close>
@@ -47,28 +54,28 @@
proof
fix x :: "'a u"
show "x \<sqsubseteq> x"
- unfolding below_up_def by (simp split: u.split)
+ by (simp add: below_up_def split: u.split)
next
fix x y :: "'a u"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
- unfolding below_up_def
- by (auto split: u.split_asm intro: below_antisym)
+ assume "x \<sqsubseteq> y" "y \<sqsubseteq> x"
+ then show "x = y"
+ by (auto simp: below_up_def split: u.split_asm intro: below_antisym)
next
fix x y z :: "'a u"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- unfolding below_up_def
- by (auto split: u.split_asm intro: below_trans)
+ assume "x \<sqsubseteq> y" "y \<sqsubseteq> z"
+ then show "x \<sqsubseteq> z"
+ by (auto simp: below_up_def split: u.split_asm intro: below_trans)
qed
+
subsection \<open>Lifted cpo is a cpo\<close>
-lemma is_lub_Iup:
- "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
-unfolding is_lub_def is_ub_def ball_simps
-by (auto simp add: below_up_def split: u.split)
+lemma is_lub_Iup: "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
+ by (auto simp: is_lub_def is_ub_def ball_simps below_up_def split: u.split)
lemma up_chain_lemma:
- assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom"
+ assumes Y: "chain Y"
+ obtains "\<forall>i. Y i = Ibottom"
| A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
proof (cases "\<exists>k. Y k \<noteq> Ibottom")
case True
@@ -78,20 +85,19 @@
proof
fix i :: nat
from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)
- with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto)
- thus "Iup (A i) = Y (i + k)"
+ with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k") auto
+ then show "Iup (A i) = Y (i + k)"
by (cases "Y (i + k)", simp_all add: A_def)
qed
from Y have chain_A: "chain A"
- unfolding chain_def Iup_below [symmetric]
- by (simp add: Iup_A)
- hence "range A <<| (\<Squnion>i. A i)"
+ by (simp add: chain_def Iup_below [symmetric] Iup_A)
+ then have "range A <<| (\<Squnion>i. A i)"
by (rule cpo_lubI)
- hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
+ then have "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
by (rule is_lub_Iup)
- hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
+ then have "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
by (simp only: Iup_A)
- hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
+ then have "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
by (simp only: is_lub_range_shift [OF Y])
with Iup_A chain_A show ?thesis ..
next
@@ -104,59 +110,62 @@
proof
fix S :: "nat \<Rightarrow> 'a u"
assume S: "chain S"
- thus "\<exists>x. range (\<lambda>i. S i) <<| x"
+ then show "\<exists>x. range (\<lambda>i. S i) <<| x"
proof (rule up_chain_lemma)
assume "\<forall>i. S i = Ibottom"
- hence "range (\<lambda>i. S i) <<| Ibottom"
+ then have "range (\<lambda>i. S i) <<| Ibottom"
by (simp add: is_lub_const)
- thus ?thesis ..
+ then show ?thesis ..
next
fix A :: "nat \<Rightarrow> 'a"
assume "range S <<| Iup (\<Squnion>i. A i)"
- thus ?thesis ..
+ then show ?thesis ..
qed
qed
+
subsection \<open>Lifted cpo is pointed\<close>
instance u :: (cpo) pcpo
-by intro_classes fast
+ by intro_classes fast
text \<open>for compatibility with old HOLCF-Version\<close>
lemma inst_up_pcpo: "\<bottom> = Ibottom"
-by (rule minimal_up [THEN bottomI, symmetric])
+ by (rule minimal_up [THEN bottomI, symmetric])
+
subsection \<open>Continuity of \emph{Iup} and \emph{Ifup}\<close>
text \<open>continuity for @{term Iup}\<close>
lemma cont_Iup: "cont Iup"
-apply (rule contI)
-apply (rule is_lub_Iup)
-apply (erule cpo_lubI)
-done
+ apply (rule contI)
+ apply (rule is_lub_Iup)
+ apply (erule cpo_lubI)
+ done
text \<open>continuity for @{term Ifup}\<close>
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
-by (induct x, simp_all)
+ by (induct x) simp_all
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
-apply (rule monofunI)
-apply (case_tac x, simp)
-apply (case_tac y, simp)
-apply (simp add: monofun_cfun_arg)
-done
+ apply (rule monofunI)
+ apply (case_tac x, simp)
+ apply (case_tac y, simp)
+ apply (simp add: monofun_cfun_arg)
+ done
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
proof (rule contI2)
- fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
+ fix Y
+ assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"
proof (rule up_chain_lemma)
fix A and k
assume A: "\<forall>i. Iup (A i) = Y (i + k)"
assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
- hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
+ then have "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
by (simp add: lub_eqI contlub_cfun_arg)
also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
by (simp add: A)
@@ -166,96 +175,86 @@
qed simp
qed (rule monofun_Ifup2)
+
subsection \<open>Continuous versions of constants\<close>
-definition
- up :: "'a \<rightarrow> 'a u" where
- "up = (\<Lambda> x. Iup x)"
+definition up :: "'a \<rightarrow> 'a u"
+ where "up = (\<Lambda> x. Iup x)"
-definition
- fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
- "fup = (\<Lambda> f p. Ifup f p)"
+definition fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
+ where "fup = (\<Lambda> f p. Ifup f p)"
translations
- "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
- "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
- "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
+ "case l of XCONST up\<cdot>x \<Rightarrow> t" \<rightleftharpoons> "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+ "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" \<rightharpoonup> "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+ "\<Lambda>(XCONST up\<cdot>x). t" \<rightleftharpoons> "CONST fup\<cdot>(\<Lambda> x. t)"
text \<open>continuous versions of lemmas for @{typ "('a)u"}\<close>
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
-apply (induct z)
-apply (simp add: inst_up_pcpo)
-apply (simp add: up_def cont_Iup)
-done
+ by (induct z) (simp add: inst_up_pcpo, simp add: up_def cont_Iup)
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
-by (simp add: up_def cont_Iup)
+ by (simp add: up_def cont_Iup)
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
-by simp
+ by simp
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
-by (simp add: up_def cont_Iup inst_up_pcpo)
+ by (simp add: up_def cont_Iup inst_up_pcpo)
lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>"
-by simp (* FIXME: remove? *)
+ by simp (* FIXME: remove? *)
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
-by (simp add: up_def cont_Iup)
+ by (simp add: up_def cont_Iup)
-lemma upE [case_names bottom up, cases type: u]:
- "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-apply (cases p)
-apply (simp add: inst_up_pcpo)
-apply (simp add: up_def cont_Iup)
-done
+lemma upE [case_names bottom up, cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+ by (cases p) (simp add: inst_up_pcpo, simp add: up_def cont_Iup)
-lemma up_induct [case_names bottom up, induct type: u]:
- "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
-by (cases x, simp_all)
+lemma up_induct [case_names bottom up, induct type: u]: "P \<bottom> \<Longrightarrow> (\<And>x. P (up\<cdot>x)) \<Longrightarrow> P x"
+ by (cases x) simp_all
text \<open>lifting preserves chain-finiteness\<close>
lemma up_chain_cases:
- assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
+ assumes Y: "chain Y"
+ obtains "\<forall>i. Y i = \<bottom>"
| A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
-apply (rule up_chain_lemma [OF Y])
-apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
-done
+ by (rule up_chain_lemma [OF Y]) (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
-apply (rule compactI2)
-apply (erule up_chain_cases)
-apply simp
-apply (drule (1) compactD2, simp)
-apply (erule exE)
-apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
-apply (simp, erule exI)
-done
+ apply (rule compactI2)
+ apply (erule up_chain_cases)
+ apply simp
+ apply (drule (1) compactD2, simp)
+ apply (erule exE)
+ apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
+ apply (simp, erule exI)
+ done
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
-unfolding compact_def
-by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
+ unfolding compact_def
+ by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
-by (safe elim!: compact_up compact_upD)
+ by (safe elim!: compact_up compact_upD)
instance u :: (chfin) chfin
-apply intro_classes
-apply (erule compact_imp_max_in_chain)
-apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
-done
+ apply intro_classes
+ apply (erule compact_imp_max_in_chain)
+ apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
+ done
text \<open>properties of fup\<close>
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
+ by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
-by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
+ by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
-by (cases x, simp_all)
+ by (cases x) simp_all
end