--- a/src/HOLCF/Adm.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Adm.thy Sat Oct 16 16:39:06 2010 -0700
@@ -48,52 +48,52 @@
subsection {* Admissibility of special formulae and propagation *}
-lemma adm_not_free: "adm (\<lambda>x. t)"
+lemma adm_const [simp]: "adm (\<lambda>x. t)"
by (rule admI, simp)
-lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
+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_all: "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
+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: "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
+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 {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *}
-
-lemma adm_disj_lemma1:
- "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk>
- \<Longrightarrow> chain (\<lambda>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
-apply (rule chainI)
-apply (erule chain_mono)
-apply (rule Least_le)
-apply (rule LeastI2_ex)
-apply simp_all
-done
-
-lemmas adm_disj_lemma2 = LeastI_ex [of "\<lambda>j. i \<le> j \<and> P (Y j)", standard]
+text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
-lemma adm_disj_lemma3:
- "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow>
- (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
- apply (frule (1) adm_disj_lemma1)
- apply (rule below_antisym)
- apply (rule lub_mono, assumption+)
- apply (erule chain_mono)
- apply (simp add: adm_disj_lemma2)
- apply (rule lub_range_mono, fast, assumption+)
-done
+lemma adm_disj_lemma1:
+ assumes adm: "adm P"
+ assumes chain: "chain Y"
+ assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
+ shows "P (\<Squnion>i. Y i)"
+proof -
+ def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)"
+ have chain': "chain (\<lambda>i. Y (f i))"
+ unfolding f_def
+ apply (rule chainI)
+ apply (rule chain_mono [OF chain])
+ apply (rule Least_le)
+ apply (rule LeastI2_ex)
+ 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_range_mono [OF _ chain chain'])
+ apply clarsimp
+ done
+ show "P (\<Squnion>i. Y i)"
+ unfolding lub_eq using adm chain' f2 by (rule admD)
+qed
-lemma adm_disj_lemma4:
- "\<lbrakk>adm P; chain Y; \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
-apply (subst adm_disj_lemma3, assumption+)
-apply (erule admD)
-apply (simp add: adm_disj_lemma1)
-apply (simp add: adm_disj_lemma2)
-done
-
-lemma adm_disj_lemma5:
+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)
@@ -101,28 +101,27 @@
apply simp
done
-lemma adm_disj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
+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_lemma5 [THEN disjE])
-apply (erule (2) adm_disj_lemma4 [THEN disjI1])
-apply (erule (2) adm_disj_lemma4 [THEN disjI2])
+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: "\<lbrakk>adm (\<lambda>x. \<not> P x); adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
+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_iff:
+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_not_conj:
- "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. \<not> Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> (P x \<and> Q x))"
-by (simp add: adm_imp)
-
text {* admissibility and continuity *}
-lemma adm_below: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
+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)"
apply (rule admI)
apply (simp add: cont2contlubE)
apply (rule lub_mono)
@@ -131,10 +130,11 @@
apply (erule spec)
done
-lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
-by (simp add: po_eq_conv adm_conj adm_below)
+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_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
+lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
apply (rule admI)
apply (simp add: cont2contlubE)
apply (erule admD)
@@ -142,14 +142,8 @@
apply (erule spec)
done
-lemma adm_not_below: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
-apply (rule admI)
-apply (drule_tac x=0 in spec)
-apply (erule contrapos_nn)
-apply (erule rev_below_trans)
-apply (erule cont2mono [THEN monofunE])
-apply (erule is_ub_thelub)
-done
+lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
+by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
subsection {* Compactness *}
@@ -190,20 +184,20 @@
text {* admissibility and compactness *}
-lemma adm_compact_not_below: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
+lemma adm_compact_not_below [simp]:
+ "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
unfolding compact_def by (rule adm_subst)
-lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
-by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
+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_compact_neq: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
-by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
+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 compact_UU [simp, intro]: "compact \<bottom>"
-by (rule compactI, simp add: adm_not_free)
-
-lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. t x \<noteq> \<bottom>)"
-by (simp add: adm_neq_compact)
+by (rule compactI, simp)
text {* Any upward-closed predicate is admissible. *}
@@ -212,9 +206,9 @@
shows "adm P"
by (rule admI, drule spec, erule P, erule is_ub_thelub)
-lemmas adm_lemmas [simp] =
- adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
+lemmas adm_lemmas =
+ adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
adm_below adm_eq adm_not_below
- adm_compact_not_below adm_compact_neq adm_neq_compact adm_not_UU
+ adm_compact_not_below adm_compact_neq adm_neq_compact
end
--- a/src/HOLCF/Bifinite.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Bifinite.thy Sat Oct 16 16:39:06 2010 -0700
@@ -56,7 +56,7 @@
unfolding approx_def by (simp add: Y)
show "(\<Squnion>i. approx i) = ID"
unfolding approx_def
- by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq)
+ by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff)
show "\<And>i. finite_deflation (approx i)"
unfolding approx_def
apply (rule bifinite.finite_deflation_p_d_e)
@@ -228,7 +228,7 @@
next
show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map)
qed
end
@@ -287,7 +287,7 @@
next
show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
qed
end
@@ -348,7 +348,7 @@
next
show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
qed
end
@@ -405,7 +405,7 @@
next
show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
unfolding emb_u_def prj_u_def defl_u_def cast_u_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff u_map_map)
qed
end
@@ -425,7 +425,7 @@
by (rule chainI, simp add: FLIFT_mono)
lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
apply (simp add: contlub_cfun_fun)
apply (simp add: lift_approx_def)
apply (case_tac x, simp)
@@ -440,7 +440,7 @@
lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
proof
- fix x
+ fix x :: "'a lift"
show "lift_approx i\<cdot>x \<sqsubseteq> x"
unfolding lift_approx_def
by (cases x, simp, simp)
@@ -548,7 +548,7 @@
next
show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
qed
end
--- a/src/HOLCF/Cfun.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Cfun.thy Sat Oct 16 16:39:06 2010 -0700
@@ -6,21 +6,15 @@
header {* The type of continuous functions *}
theory Cfun
-imports Pcpodef Ffun Product_Cpo
+imports Pcpodef Fun_Cpo Product_Cpo
begin
default_sort cpo
subsection {* Definition of continuous function type *}
-lemma Ex_cont: "\<exists>f. cont f"
-by (rule exI, rule cont_const)
-
-lemma adm_cont: "adm cont"
-by (rule admI, rule cont_lub_fun)
-
cpodef (CFun) ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
-by (simp_all add: Ex_cont adm_cont)
+by (auto intro: cont_const adm_cont)
type_notation (xsymbols)
cfun ("(_ \<rightarrow>/ _)" [1, 0] 0)
@@ -176,19 +170,19 @@
text {* Extensionality for continuous functions *}
-lemma expand_cfun_eq: "(f = g) = (\<forall>x. f\<cdot>x = g\<cdot>x)"
+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)
-lemma ext_cfun: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
-by (simp add: expand_cfun_eq)
+lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
+by (simp add: cfun_eq_iff)
text {* Extensionality wrt. ordering for continuous functions *}
-lemma expand_cfun_below: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)"
-by (simp add: below_CFun_def expand_fun_below)
+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 below_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: expand_cfun_below)
+lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: cfun_below_iff)
text {* Congruence for continuous function application *}
@@ -233,7 +227,7 @@
text {* monotonicity of application *}
lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
-by (simp add: expand_cfun_below)
+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])
@@ -258,7 +252,7 @@
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 expand_cfun_below)
+by (simp add: chain_def cfun_below_iff)
text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
@@ -293,29 +287,6 @@
apply (rule minimal [THEN monofun_cfun_arg])
done
-text {* the lub of a chain of continous functions is monotone *}
-
-lemma lub_cfun_mono: "chain F \<Longrightarrow> monofun (\<lambda>x. \<Squnion>i. F i\<cdot>x)"
-apply (drule ch2ch_monofun [OF monofun_Rep_CFun])
-apply (simp add: thelub_fun [symmetric])
-apply (erule monofun_lub_fun)
-apply (simp add: monofun_Rep_CFun2)
-done
-
-text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"} *}
-
-lemma ex_lub_cfun:
- "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>j. \<Squnion>i. F j\<cdot>(Y i)) = (\<Squnion>i. \<Squnion>j. F j\<cdot>(Y i))"
-by (simp add: diag_lub)
-
-text {* the lub of a chain of cont. functions is continuous *}
-
-lemma cont_lub_cfun: "chain F \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i\<cdot>x)"
-apply (rule cont2cont_lub)
-apply (erule monofun_Rep_CFun [THEN ch2ch_monofun])
-apply (rule cont_Rep_CFun2)
-done
-
text {* type @{typ "'a -> 'b"} is chain complete *}
lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
@@ -333,18 +304,30 @@
assumes t: "cont (\<lambda>x. t x)"
shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
proof -
- have "cont (\<lambda>x. Rep_CFun (f x))"
- using cont_Rep_CFun f by (rule cont2cont_app3)
- thus "cont (\<lambda>x. (f x)\<cdot>(t x))"
- using cont_Rep_CFun2 t by (rule cont2cont_app2)
+ 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)
qed
+text {*
+ Two specific lemmas for the combination of LCF and HOL terms.
+ These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
+*}
+
+lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
+by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
+
+lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
+by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
+
+
text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
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 expand_cfun_below by simp
+ unfolding monofun_def cfun_below_iff by simp
text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
@@ -509,7 +492,7 @@
by (simp add: cfcomp1)
lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>"
-by (simp add: expand_cfun_eq)
+by (simp add: cfun_eq_iff)
text {*
Show that interpretation of (pcpo,@{text "_->_"}) is a category.
@@ -520,13 +503,13 @@
*}
lemma ID2 [simp]: "f oo ID = f"
-by (rule ext_cfun, simp)
+by (rule cfun_eqI, simp)
lemma ID3 [simp]: "ID oo f = f"
-by (rule ext_cfun, simp)
+by (rule cfun_eqI, simp)
lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
-by (rule ext_cfun, simp)
+by (rule cfun_eqI, simp)
subsection {* Map operator for continuous function space *}
@@ -539,12 +522,12 @@
unfolding cfun_map_def by simp
lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
-unfolding expand_cfun_eq by simp
+unfolding cfun_eq_iff by 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 ext_cfun) simp
+by (rule cfun_eqI) simp
subsection {* Strictified functions *}
@@ -600,10 +583,10 @@
using f
proof (rule cont2cont_Let)
fix x show "cont (\<lambda>y. g x y)"
- using g by (rule cont_fst_snd_D2)
+ using g by (simp add: prod_cont_iff)
next
fix y show "cont (\<lambda>x. g x y)"
- using g by (rule cont_fst_snd_D1)
+ using g by (simp add: prod_cont_iff)
qed
text {* The simple version (suggested by Joachim Breitner) is needed if
--- a/src/HOLCF/Completion.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Completion.thy Sat Oct 16 16:39:06 2010 -0700
@@ -397,7 +397,7 @@
assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
assumes below: "\<And>a. f a \<sqsubseteq> g a"
shows "basis_fun f \<sqsubseteq> basis_fun g"
- apply (rule below_cfun_ext)
+ apply (rule cfun_belowI)
apply (simp only: basis_fun_beta f_mono g_mono)
apply (rule is_lub_thelub_ex)
apply (rule basis_fun_lemma, erule f_mono)
--- a/src/HOLCF/Cont.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Cont.thy Sat Oct 16 16:39:06 2010 -0700
@@ -22,12 +22,6 @@
monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity" where
"monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
-(*
-definition
- contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def" where
- "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
-*)
-
definition
cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
where
@@ -176,6 +170,17 @@
"\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
by (rule cont_apply [OF _ _ cont_const])
+text {* Least upper bounds preserve continuity *}
+
+lemma cont2cont_lub [simp]:
+ 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
+
text {* if-then-else is continuous *}
lemma cont_if [simp, cont2cont]:
@@ -184,7 +189,7 @@
subsection {* Finite chains and flat pcpos *}
-text {* monotone functions map finite chains to finite chains *}
+text {* Monotone functions map finite chains to finite chains. *}
lemma monofun_finch2finch:
"\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
@@ -193,12 +198,14 @@
apply (force simp add: max_in_chain_def)
done
-text {* The same holds for continuous functions *}
+text {* The same holds for continuous functions. *}
lemma cont_finch2finch:
"\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
by (rule cont2mono [THEN monofun_finch2finch])
+text {* All monotone functions with chain-finite domain are continuous. *}
+
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
apply (erule contI2)
apply (frule chfin2finch)
@@ -208,7 +215,7 @@
apply (force simp add: max_in_chain_def)
done
-text {* some properties of flat *}
+text {* All strict functions with flat domain are continuous. *}
lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
apply (rule monofunI)
@@ -219,7 +226,7 @@
lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)"
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
-text {* functions with discrete domain *}
+text {* All functions with discrete domain are continuous. *}
lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
apply (rule contI)
--- a/src/HOLCF/ConvexPD.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy Sat Oct 16 16:39:06 2010 -0700
@@ -331,7 +331,7 @@
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: expand_cfun_below)
+by (simp add: cfun_below_iff)
lemma convex_bind_basis_mono:
"t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
@@ -382,7 +382,7 @@
by (induct xs rule: convex_pd_induct, simp_all)
lemma convex_map_ID: "convex_map\<cdot>ID = ID"
-by (simp add: expand_cfun_eq ID_def convex_map_ident)
+by (simp add: cfun_eq_iff ID_def convex_map_ident)
lemma convex_map_map:
"convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
@@ -494,7 +494,7 @@
next
show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq convex_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
qed
end
--- a/src/HOLCF/Cprod.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Cprod.thy Sat Oct 16 16:39:06 2010 -0700
@@ -51,7 +51,7 @@
unfolding cprod_map_def by simp
lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
-unfolding expand_cfun_eq by auto
+unfolding cfun_eq_iff by auto
lemma cprod_map_map:
"cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
--- a/src/HOLCF/Deflation.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Deflation.thy Sat Oct 16 16:39:06 2010 -0700
@@ -19,7 +19,7 @@
begin
lemma below_ID: "d \<sqsubseteq> ID"
-by (rule below_cfun_ext, simp add: below)
+by (rule cfun_belowI, simp add: below)
text {* The set of fixed points is the same as the range. *}
@@ -36,7 +36,7 @@
lemma belowI:
assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
-proof (rule below_cfun_ext)
+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)
@@ -326,7 +326,7 @@
lemma ep_pair_unique_e_lemma:
assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
shows "e1 \<sqsubseteq> e2"
-proof (rule below_cfun_ext)
+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])
@@ -341,7 +341,7 @@
lemma ep_pair_unique_p_lemma:
assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
shows "p1 \<sqsubseteq> p2"
-proof (rule below_cfun_ext)
+proof (rule cfun_belowI)
fix x
have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
by (rule ep_pair.e_p_below [OF 1])
@@ -414,9 +414,9 @@
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"
- by (simp add: expand_cfun_eq)
+ 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"
- apply (rule below_cfun_ext, simp)
+ apply (rule cfun_belowI, simp)
apply (rule below_trans [OF e2p2.e_p_below])
apply (rule monofun_cfun_arg)
apply (rule e1p1.e_p_below)
@@ -431,9 +431,9 @@
interpret d2: deflation d2 by fact
fix f
show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
- by (simp add: expand_cfun_eq d1.idem d2.idem)
+ by (simp add: cfun_eq_iff d1.idem d2.idem)
show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
- apply (rule below_cfun_ext, simp)
+ apply (rule cfun_belowI, simp)
apply (rule below_trans [OF d2.below])
apply (rule monofun_cfun_arg)
apply (rule d1.below)
@@ -455,7 +455,7 @@
by (simp add: a b)
qed
show "inj_on ?f (range ?h)"
- proof (rule inj_onI, rule ext_cfun, clarsimp)
+ 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))))"
--- a/src/HOLCF/Domain.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Domain.thy Sat Oct 16 16:39:06 2010 -0700
@@ -10,7 +10,6 @@
("Tools/cont_consts.ML")
("Tools/cont_proc.ML")
("Tools/Domain/domain_constructors.ML")
- ("Tools/Domain/domain_library.ML")
("Tools/Domain/domain_axioms.ML")
("Tools/Domain/domain_theorems.ML")
("Tools/Domain/domain_extender.ML")
@@ -154,7 +153,6 @@
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
-use "Tools/Domain/domain_library.ML"
use "Tools/Domain/domain_axioms.ML"
use "Tools/Domain/domain_constructors.ML"
use "Tools/Domain/domain_theorems.ML"
--- a/src/HOLCF/FOCUS/Buffer.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/FOCUS/Buffer.thy Sat Oct 16 16:39:06 2010 -0700
@@ -200,7 +200,7 @@
apply ( rule_tac [2] P="(%x. x:B)" in ssubst)
prefer 3
apply ( assumption)
-apply ( rule_tac [2] ext_cfun)
+apply ( rule_tac [2] cfun_eqI)
apply ( drule_tac [2] spec)
apply ( drule_tac [2] f="rt" in cfun_arg_cong)
prefer 2
--- a/src/HOLCF/FOCUS/Fstream.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Sat Oct 16 16:39:06 2010 -0700
@@ -95,7 +95,7 @@
apply (safe)
apply (erule_tac [!] contrapos_np)
prefer 2 apply (fast elim: DefE)
-apply (rule Lift_cases)
+apply (rule lift.exhaust)
apply (erule (1) notE)
apply (safe)
apply (drule Def_inject_less_eq [THEN iffD1])
--- a/src/HOLCF/Ffun.thy Fri Oct 15 17:21:37 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,273 +0,0 @@
-(* Title: HOLCF/FunCpo.thy
- Author: Franz Regensburger
-*)
-
-header {* Class instances for the full function space *}
-
-theory Ffun
-imports Cont
-begin
-
-subsection {* Full function space is a partial order *}
-
-instantiation "fun" :: (type, below) below
-begin
-
-definition
- below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
-
-instance ..
-end
-
-instance "fun" :: (type, po) po
-proof
- fix f :: "'a \<Rightarrow> 'b"
- show "f \<sqsubseteq> f"
- by (simp add: below_fun_def)
-next
- fix f g :: "'a \<Rightarrow> 'b"
- assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "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"
- unfolding below_fun_def by (fast elim: below_trans)
-qed
-
-text {* make the symbol @{text "<<"} accessible for type fun *}
-
-lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
-by (simp add: below_fun_def)
-
-lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: below_fun_def)
-
-subsection {* Full function space is chain complete *}
-
-text {* function application is monotone *}
-
-lemma monofun_app: "monofun (\<lambda>f. f x)"
-by (rule monofunI, simp add: below_fun_def)
-
-text {* chains of functions yield chains in the po range *}
-
-lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
-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 {* upper bounds of function chains yield upper bound in the po range *}
-
-lemma ub2ub_fun:
- "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
-by (auto simp add: is_ub_def below_fun_def)
-
-text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
-
-lemma is_lub_lambda:
- assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
- shows "range Y <<| f"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (rule below_fun_ext)
-apply (rule is_ub_lub [OF f])
-apply (rule below_fun_ext)
-apply (rule is_lub_lub [OF f])
-apply (erule ub2ub_fun)
-done
-
-lemma 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 thelub_fun:
- "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
- \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-by (rule lub_fun [THEN thelubI])
-
-lemma cpo_fun:
- "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
-by (rule exI, erule lub_fun)
-
-instance "fun" :: (type, cpo) cpo
-by intro_classes (rule cpo_fun)
-
-instance "fun" :: (finite, finite_po) finite_po ..
-
-instance "fun" :: (type, discrete_cpo) discrete_cpo
-proof
- fix f g :: "'a \<Rightarrow> 'b"
- show "f \<sqsubseteq> g \<longleftrightarrow> f = g"
- unfolding expand_fun_below fun_eq_iff
- by simp
-qed
-
-text {* chain-finite function spaces *}
-
-lemma maxinch2maxinch_lambda:
- "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
-unfolding max_in_chain_def fun_eq_iff by simp
-
-lemma maxinch_mono:
- "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
-unfolding max_in_chain_def
-proof (intro allI impI)
- fix k
- assume Y: "\<forall>n\<ge>i. Y i = Y n"
- assume ij: "i \<le> j"
- assume jk: "j \<le> k"
- from ij jk have ik: "i \<le> k" by simp
- from Y ij have Yij: "Y i = Y j" by simp
- from Y ik have Yik: "Y i = Y k" by simp
- from Yij Yik show "Y j = Y k" by auto
-qed
-
-instance "fun" :: (finite, chfin) chfin
-proof
- fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
- let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
- assume "chain Y"
- hence "\<And>x. chain (\<lambda>i. Y i x)"
- by (rule ch2ch_fun)
- hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
- by (rule chfin)
- hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
- by (rule LeastI_ex)
- hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
- by (rule maxinch_mono [OF _ Max_ge], simp_all)
- hence "max_in_chain (Max (range ?n)) Y"
- by (rule maxinch2maxinch_lambda)
- thus "\<exists>n. max_in_chain n Y" ..
-qed
-
-subsection {* Full function space is pointed *}
-
-lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
-by (simp add: below_fun_def)
-
-lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
-apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
-apply (rule minimal_fun [THEN allI])
-done
-
-instance "fun" :: (type, pcpo) pcpo
-by intro_classes (rule least_fun)
-
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
-by (rule minimal_fun [THEN UU_I, symmetric])
-
-text {* function application is strict in the left argument *}
-lemma app_strict [simp]: "\<bottom> x = \<bottom>"
-by (simp add: inst_fun_pcpo)
-
-text {*
- The following results are about application for functions in @{typ "'a=>'b"}
-*}
-
-lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
-by (simp add: below_fun_def)
-
-lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
-by (rule monofunE)
-
-lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
-by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
-
-subsection {* Propagation of monotonicity and continuity *}
-
-text {* the lub of a chain of monotone functions is monotone *}
-
-lemma monofun_lub_fun:
- "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
- \<Longrightarrow> monofun (\<Squnion>i. F i)"
-apply (rule monofunI)
-apply (simp add: thelub_fun)
-apply (rule lub_mono)
-apply (erule ch2ch_fun)
-apply (erule ch2ch_fun)
-apply (simp add: monofunE)
-done
-
-text {* the lub of a chain of continuous functions is continuous *}
-
-lemma cont_lub_fun:
- "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
-apply (rule contI2)
-apply (erule monofun_lub_fun)
-apply (simp add: cont2mono)
-apply (simp add: thelub_fun cont2contlubE)
-apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
-done
-
-lemma cont2cont_lub:
- "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
-by (simp add: thelub_fun [symmetric] cont_lub_fun)
-
-lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
-apply (rule monofunI)
-apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
-done
-
-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)
-apply (simp add: thelub_fun ch2ch_cont)
-done
-
-text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
-
-lemma mono2mono_lambda:
- assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
-apply (rule monofunI)
-apply (rule below_fun_ext)
-apply (erule monofunE [OF f])
-done
-
-lemma cont2cont_lambda [simp]:
- assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
-apply (rule contI2)
-apply (simp add: mono2mono_lambda cont2mono f)
-apply (rule below_fun_ext)
-apply (simp add: thelub_fun cont2contlubE [OF f])
-done
-
-text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
-
-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: thelub_fun ch2ch_lambda)
-
-lemma contlub_abstraction:
- "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
- (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
-apply (rule thelub_fun [symmetric])
-apply (simp add: ch2ch_cont)
-done
-
-lemma mono2mono_app:
- "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
-apply (rule monofunI)
-apply (simp add: monofun_fun monofunE)
-done
-
-lemma cont2cont_app:
- "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
-apply (erule cont_apply [where t=t])
-apply (erule spec)
-apply (erule cont2cont_fun)
-done
-
-lemmas cont2cont_app2 = cont2cont_app [rule_format]
-
-lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
-by (rule cont2cont_app2 [OF cont_const])
-
-end
--- a/src/HOLCF/Fix.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Fix.thy Sat Oct 16 16:39:06 2010 -0700
@@ -60,13 +60,7 @@
text {* direct connection between @{term fix} and iteration *}
lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
-apply (unfold fix_def)
-apply (rule beta_cfun)
-apply (rule cont2cont_lub)
-apply (rule ch2ch_lambda)
-apply (rule chain_iterate)
-apply simp
-done
+unfolding fix_def by simp
lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
unfolding fix_def2
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Fun_Cpo.thy Sat Oct 16 16:39:06 2010 -0700
@@ -0,0 +1,201 @@
+(* Title: HOLCF/Fun_Cpo.thy
+ Author: Franz Regensburger
+ Author: Brian Huffman
+*)
+
+header {* Class instances for the full function space *}
+
+theory Fun_Cpo
+imports Adm
+begin
+
+subsection {* Full function space is a partial order *}
+
+instantiation "fun" :: (type, below) below
+begin
+
+definition
+ below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
+
+instance ..
+end
+
+instance "fun" :: (type, po) po
+proof
+ fix f :: "'a \<Rightarrow> 'b"
+ show "f \<sqsubseteq> f"
+ by (simp add: below_fun_def)
+next
+ fix f g :: "'a \<Rightarrow> 'b"
+ assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "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"
+ 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)
+
+lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: below_fun_def)
+
+lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
+by (simp add: below_fun_def)
+
+subsection {* Full function space is chain complete *}
+
+text {* Function application is monotone. *}
+
+lemma monofun_app: "monofun (\<lambda>f. f x)"
+by (rule monofunI, simp add: below_fun_def)
+
+text {* Properties of chains of functions. *}
+
+lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
+unfolding chain_def fun_below_iff by auto
+
+lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
+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 {* upper bounds of function chains yield upper bound in the po range *}
+
+lemma ub2ub_fun:
+ "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
+by (auto simp add: is_ub_def below_fun_def)
+
+text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
+
+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
+
+lemma 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 thelub_fun:
+ "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
+ \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
+by (rule lub_fun [THEN thelubI])
+
+instance "fun" :: (type, cpo) cpo
+by intro_classes (rule exI, erule lub_fun)
+
+subsection {* Chain-finiteness of function space *}
+
+lemma maxinch2maxinch_lambda:
+ "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
+unfolding max_in_chain_def fun_eq_iff by simp
+
+lemma maxinch_mono:
+ "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
+unfolding max_in_chain_def
+proof (intro allI impI)
+ fix k
+ assume Y: "\<forall>n\<ge>i. Y i = Y n"
+ assume ij: "i \<le> j"
+ assume jk: "j \<le> k"
+ from ij jk have ik: "i \<le> k" by simp
+ from Y ij have Yij: "Y i = Y j" by simp
+ from Y ik have Yik: "Y i = Y k" by simp
+ from Yij Yik show "Y j = Y k" by auto
+qed
+
+instance "fun" :: (finite, chfin) chfin
+proof
+ fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
+ let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
+ assume "chain Y"
+ hence "\<And>x. chain (\<lambda>i. Y i x)"
+ by (rule ch2ch_fun)
+ hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
+ by (rule chfin)
+ hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
+ by (rule LeastI_ex)
+ hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
+ by (rule maxinch_mono [OF _ Max_ge], simp_all)
+ hence "max_in_chain (Max (range ?n)) Y"
+ by (rule maxinch2maxinch_lambda)
+ thus "\<exists>n. max_in_chain n Y" ..
+qed
+
+instance "fun" :: (finite, finite_po) finite_po ..
+
+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
+qed
+
+subsection {* Full function space is pointed *}
+
+lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
+by (simp add: below_fun_def)
+
+instance "fun" :: (type, pcpo) pcpo
+by default (fast intro: minimal_fun)
+
+lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
+by (rule minimal_fun [THEN UU_I, symmetric])
+
+lemma app_strict [simp]: "\<bottom> x = \<bottom>"
+by (simp add: inst_fun_pcpo)
+
+lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
+by (rule UU_I, rule minimal_fun)
+
+subsection {* Propagation of monotonicity and continuity *}
+
+text {* The lub of a chain of monotone functions is monotone. *}
+
+lemma adm_monofun: "adm monofun"
+by (rule admI, simp add: thelub_fun fun_chain_iff monofun_def lub_mono)
+
+text {* The lub of a chain of continuous functions is continuous. *}
+
+lemma adm_cont: "adm cont"
+by (rule admI, simp add: thelub_fun fun_chain_iff)
+
+text {* Function application preserves monotonicity and continuity. *}
+
+lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
+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 thelub_fun ch2ch_cont)
+done
+
+text {*
+ Lambda abstraction preserves monotonicity and continuity.
+ (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)
+*}
+
+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 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])
+
+text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
+
+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: thelub_fun ch2ch_lambda)
+
+end
--- a/src/HOLCF/HOLCF.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/HOLCF.thy Sat Oct 16 16:39:06 2010 -0700
@@ -15,7 +15,20 @@
ML {* path_add "~~/src/HOLCF/Library" *}
-text {* Legacy theorem names *}
+text {* Legacy theorem names deprecated after Isabelle2009-2: *}
+
+lemmas expand_fun_below = fun_below_iff
+lemmas below_fun_ext = fun_belowI
+lemmas expand_cfun_eq = cfun_eq_iff
+lemmas ext_cfun = cfun_eqI
+lemmas expand_cfun_below = cfun_below_iff
+lemmas below_cfun_ext = cfun_belowI
+lemmas monofun_fun_fun = fun_belowD
+lemmas monofun_fun_arg = monofunE
+lemmas monofun_lub_fun = adm_monofun [THEN admD]
+lemmas cont_lub_fun = adm_cont [THEN admD]
+
+text {* Older legacy theorem names: *}
lemmas sq_ord_less_eq_trans = below_eq_trans
lemmas sq_ord_eq_less_trans = eq_below_trans
--- a/src/HOLCF/IsaMakefile Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/IsaMakefile Sat Oct 16 16:39:06 2010 -0700
@@ -48,9 +48,9 @@
Deflation.thy \
Domain.thy \
Domain_Aux.thy \
- Ffun.thy \
Fixrec.thy \
Fix.thy \
+ Fun_Cpo.thy \
HOLCF.thy \
Lift.thy \
LowerPD.thy \
@@ -74,7 +74,6 @@
Tools/Domain/domain_axioms.ML \
Tools/Domain/domain_constructors.ML \
Tools/Domain/domain_isomorphism.ML \
- Tools/Domain/domain_library.ML \
Tools/Domain/domain_take_proofs.ML \
Tools/Domain/domain_theorems.ML \
Tools/fixrec.ML \
@@ -102,6 +101,7 @@
HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
+ Library/Defl_Bifinite.thy \
Library/List_Cpo.thy \
Library/Stream.thy \
Library/Strict_Fun.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Library/Defl_Bifinite.thy Sat Oct 16 16:39:06 2010 -0700
@@ -0,0 +1,650 @@
+(* Title: HOLCF/Library/Defl_Bifinite.thy
+ Author: Brian Huffman
+*)
+
+header {* Algebraic deflations are a bifinite domain *}
+
+theory Defl_Bifinite
+imports HOLCF Infinite_Set
+begin
+
+subsection {* Lemmas about MOST *}
+
+default_sort type
+
+lemma MOST_INFM:
+ assumes inf: "infinite (UNIV::'a set)"
+ shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
+ unfolding Alm_all_def Inf_many_def
+ apply (auto simp add: Collect_neg_eq)
+ apply (drule (1) finite_UnI)
+ apply (simp add: Compl_partition2 inf)
+ done
+
+lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
+by (rule MOST_inj [OF _ inj_Suc])
+
+lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
+unfolding MOST_nat
+apply (clarify, rule_tac x="Suc m" in exI, clarify)
+apply (erule Suc_lessE, simp)
+done
+
+lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
+by (rule iffI [OF MOST_SucD MOST_SucI])
+
+lemma INFM_finite_Bex_distrib:
+ "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
+by (induct set: finite, simp, simp add: INFM_disj_distrib)
+
+lemma MOST_finite_Ball_distrib:
+ "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
+by (induct set: finite, simp, simp add: MOST_conj_distrib)
+
+lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
+unfolding MOST_nat_le by fast
+
+subsection {* Eventually constant sequences *}
+
+definition
+ eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
+where
+ "eventually_constant S = (\<exists>x. MOST i. S i = x)"
+
+lemma eventually_constant_MOST_MOST:
+ "eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)"
+unfolding eventually_constant_def MOST_nat
+apply safe
+apply (rule_tac x=m in exI, clarify)
+apply (rule_tac x=m in exI, clarify)
+apply simp
+apply fast
+done
+
+lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S"
+unfolding eventually_constant_def by fast
+
+lemma eventually_constant_comp:
+ "eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))"
+unfolding eventually_constant_def
+apply (erule exE, rule_tac x="f x" in exI)
+apply (erule MOST_mono, simp)
+done
+
+lemma eventually_constant_Suc_iff:
+ "eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)"
+unfolding eventually_constant_def
+by (subst MOST_Suc_iff, rule refl)
+
+lemma eventually_constant_SucD:
+ "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)"
+by (rule eventually_constant_Suc_iff [THEN iffD1])
+
+subsection {* Limits of eventually constant sequences *}
+
+definition
+ eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "eventual S = (THE x. MOST i. S i = x)"
+
+lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x"
+unfolding eventual_def
+apply (rule the_equality, assumption)
+apply (rename_tac y)
+apply (subgoal_tac "MOST i::nat. y = x", simp)
+apply (erule MOST_rev_mp)
+apply (erule MOST_rev_mp)
+apply simp
+done
+
+lemma MOST_eq_eventual:
+ "eventually_constant S \<Longrightarrow> MOST i. S i = eventual S"
+unfolding eventually_constant_def
+by (erule exE, simp add: eventual_eqI)
+
+lemma eventual_mem_range:
+ "eventually_constant S \<Longrightarrow> eventual S \<in> range S"
+apply (drule MOST_eq_eventual)
+apply (simp only: MOST_nat_le, clarify)
+apply (drule spec, drule mp, rule order_refl)
+apply (erule range_eqI [OF sym])
+done
+
+lemma eventually_constant_MOST_iff:
+ assumes S: "eventually_constant S"
+ shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)"
+apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))")
+apply simp
+apply (rule iffI)
+apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
+apply (erule MOST_mono, force)
+apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
+apply (erule MOST_mono, simp)
+done
+
+lemma MOST_eventual:
+ "\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)"
+proof -
+ assume "eventually_constant S"
+ hence "MOST n. S n = eventual S"
+ by (rule MOST_eq_eventual)
+ moreover assume "MOST n. P (S n)"
+ ultimately have "MOST n. S n = eventual S \<and> P (S n)"
+ by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
+ hence "MOST n::nat. P (eventual S)"
+ by (rule MOST_mono) auto
+ thus ?thesis by simp
+qed
+
+lemma eventually_constant_MOST_Suc_eq:
+ "eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n"
+apply (drule MOST_eq_eventual)
+apply (frule MOST_Suc_iff [THEN iffD2])
+apply (erule MOST_rev_mp)
+apply (erule MOST_rev_mp)
+apply simp
+done
+
+lemma eventual_comp:
+ "eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))"
+apply (rule eventual_eqI)
+apply (rule MOST_mono)
+apply (erule MOST_eq_eventual)
+apply simp
+done
+
+subsection {* Constructing finite deflations by iteration *}
+
+default_sort cpo
+
+lemma le_Suc_induct:
+ assumes le: "i \<le> j"
+ assumes step: "\<And>i. P i (Suc i)"
+ assumes refl: "\<And>i. P i i"
+ assumes trans: "\<And>i j k. \<lbrakk>P i j; P j k\<rbrakk> \<Longrightarrow> P i k"
+ shows "P i j"
+proof (cases "i = j")
+ assume "i = j"
+ thus "P i j" by (simp add: refl)
+next
+ assume "i \<noteq> j"
+ with le have "i < j" by simp
+ thus "P i j" using step trans by (rule less_Suc_induct)
+qed
+
+definition
+ eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)"
+where
+ "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
+
+text {* A pre-deflation is like a deflation, but not idempotent. *}
+
+locale pre_deflation =
+ fixes f :: "'a \<rightarrow> 'a::cpo"
+ assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
+ assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
+begin
+
+lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
+by (induct i, simp_all add: below_trans [OF below])
+
+lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
+by (induct i, simp_all)
+
+lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
+apply (erule le_Suc_induct)
+apply (simp add: below)
+apply (rule below_refl)
+apply (erule (1) below_trans)
+done
+
+lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
+proof (rule finite_subset)
+ show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))"
+ by (clarify, case_tac i, simp_all)
+ show "finite (insert x (range (\<lambda>x. f\<cdot>x)))"
+ by (simp add: finite_range)
+qed
+
+lemma eventually_constant_iterate_app:
+ "eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)"
+unfolding eventually_constant_def MOST_nat_le
+proof -
+ let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x"
+ have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k"
+ apply (rule finite_range_has_max)
+ apply (erule antichain_iterate_app)
+ apply (rule finite_range_iterate_app)
+ done
+ then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast
+ show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z"
+ proof (intro exI allI impI)
+ fix k
+ assume "j \<le> k"
+ hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app)
+ also have "?Y j \<sqsubseteq> ?Y k" by (rule j)
+ finally show "?Y k = ?Y j" .
+ qed
+qed
+
+lemma eventually_constant_iterate:
+ "eventually_constant (\<lambda>n. iterate n\<cdot>f)"
+proof -
+ have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)"
+ by (simp add: eventually_constant_iterate_app)
+ hence "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). MOST i. MOST j. iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y"
+ unfolding eventually_constant_MOST_MOST .
+ hence "MOST i. MOST j. \<forall>y\<in>range (\<lambda>x. f\<cdot>x). iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y"
+ by (simp only: MOST_finite_Ball_distrib [OF finite_range])
+ hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)"
+ by simp
+ hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
+ by (simp only: iterate_Suc2)
+ hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
+ by (simp only: cfun_eq_iff)
+ hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
+ unfolding eventually_constant_MOST_MOST .
+ thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
+ by (rule eventually_constant_SucD)
+qed
+
+abbreviation
+ d :: "'a \<rightarrow> 'a"
+where
+ "d \<equiv> eventual_iterate f"
+
+lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
+unfolding eventual_iterate_def
+using eventually_constant_iterate by (rule MOST_eventual)
+
+lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
+apply (rule MOST_d)
+apply (subst iterate_Suc [symmetric])
+apply (rule eventually_constant_MOST_Suc_eq)
+apply (rule eventually_constant_iterate_app)
+done
+
+lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x"
+proof
+ assume "d\<cdot>x = x"
+ with f_d [where x=x]
+ show "f\<cdot>x = x" by simp
+next
+ assume f: "f\<cdot>x = x"
+ have "\<forall>n. iterate n\<cdot>f\<cdot>x = x"
+ by (rule allI, rule nat.induct, simp, simp add: f)
+ hence "MOST n. iterate n\<cdot>f\<cdot>x = x"
+ by (rule ALL_MOST)
+ thus "d\<cdot>x = x"
+ by (rule MOST_d)
+qed
+
+lemma finite_deflation_d: "finite_deflation d"
+proof
+ fix x :: 'a
+ have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
+ unfolding eventual_iterate_def
+ using eventually_constant_iterate
+ by (rule eventual_mem_range)
+ then obtain n where n: "d = iterate n\<cdot>f" ..
+ have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x"
+ using f_d by (rule iterate_fixed)
+ thus "d\<cdot>(d\<cdot>x) = d\<cdot>x"
+ by (simp add: n)
+next
+ fix x :: 'a
+ show "d\<cdot>x \<sqsubseteq> x"
+ by (rule MOST_d, simp add: iterate_below)
+next
+ from finite_range
+ have "finite {x. f\<cdot>x = x}"
+ by (rule finite_range_imp_finite_fixes)
+ thus "finite {x. d\<cdot>x = x}"
+ by (simp add: d_fixed_iff)
+qed
+
+lemma deflation_d: "deflation d"
+using finite_deflation_d
+by (rule finite_deflation_imp_deflation)
+
+end
+
+lemma finite_deflation_eventual_iterate:
+ "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)"
+by (rule pre_deflation.finite_deflation_d)
+
+lemma pre_deflation_oo:
+ assumes "finite_deflation d"
+ assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
+ shows "pre_deflation (d oo f)"
+proof
+ interpret d: finite_deflation d by fact
+ fix x
+ show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
+ by (simp, rule below_trans [OF d.below f])
+ show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
+ by (rule finite_subset [OF _ d.finite_range], auto)
+qed
+
+lemma eventual_iterate_oo_fixed_iff:
+ assumes "finite_deflation d"
+ assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
+ shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
+proof -
+ interpret d: finite_deflation d by fact
+ let ?e = "d oo f"
+ interpret e: pre_deflation "d oo f"
+ using `finite_deflation d` f
+ by (rule pre_deflation_oo)
+ let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
+ show ?thesis
+ apply (subst e.d_fixed_iff)
+ apply simp
+ apply safe
+ apply (erule subst)
+ apply (rule d.idem)
+ apply (rule below_antisym)
+ apply (rule f)
+ apply (erule subst, rule d.below)
+ apply simp
+ done
+qed
+
+lemma eventual_mono:
+ assumes A: "eventually_constant A"
+ assumes B: "eventually_constant B"
+ assumes below: "\<And>n. A n \<sqsubseteq> B n"
+ shows "eventual A \<sqsubseteq> eventual B"
+proof -
+ from A have "MOST n. A n = eventual A"
+ by (rule MOST_eq_eventual)
+ then have "MOST n. eventual A \<sqsubseteq> B n"
+ by (rule MOST_mono) (erule subst, rule below)
+ with B show "eventual A \<sqsubseteq> eventual B"
+ by (rule MOST_eventual)
+qed
+
+lemma eventual_iterate_mono:
+ assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g"
+ shows "eventual_iterate f \<sqsubseteq> eventual_iterate g"
+unfolding eventual_iterate_def
+apply (rule eventual_mono)
+apply (rule pre_deflation.eventually_constant_iterate [OF f])
+apply (rule pre_deflation.eventually_constant_iterate [OF g])
+apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
+done
+
+lemma cont2cont_eventual_iterate_oo:
+ assumes d: "finite_deflation d"
+ assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
+ shows "cont (\<lambda>x. eventual_iterate (d oo f x))"
+ (is "cont ?e")
+proof (rule contI2)
+ show "monofun ?e"
+ apply (rule monofunI)
+ apply (rule eventual_iterate_mono)
+ apply (rule pre_deflation_oo [OF d below])
+ apply (rule pre_deflation_oo [OF d below])
+ apply (rule monofun_cfun_arg)
+ apply (erule cont2monofunE [OF cont])
+ done
+next
+ fix Y :: "nat \<Rightarrow> 'b"
+ assume Y: "chain Y"
+ with cont have fY: "chain (\<lambda>i. f (Y i))"
+ by (rule ch2ch_cont)
+ assume eY: "chain (\<lambda>i. ?e (Y i))"
+ have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x"
+ by (rule admD [OF _ Y], simp add: cont, rule below)
+ have "deflation (?e (\<Squnion>i. Y i))"
+ apply (rule pre_deflation.deflation_d)
+ apply (rule pre_deflation_oo [OF d lub_below])
+ done
+ then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))"
+ proof (rule deflation.belowI)
+ fix x :: 'a
+ assume "?e (\<Squnion>i. Y i)\<cdot>x = x"
+ hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x"
+ by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
+ hence "(\<Squnion>i. f (Y i)\<cdot>x) = x"
+ apply (simp only: cont2contlubE [OF cont Y])
+ apply (simp only: contlub_cfun_fun [OF fY])
+ done
+ have "compact (d\<cdot>x)"
+ using d by (rule finite_deflation.compact)
+ then have "compact x"
+ using `d\<cdot>x = x` by simp
+ then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
+ using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
+ then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
+ by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
+ then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
+ then have "f (Y n)\<cdot>x = x"
+ using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
+ with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
+ by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
+ moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
+ by (rule is_ub_thelub, simp add: eY)
+ ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x"
+ by (simp add: contlub_cfun_fun eY)
+ also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x"
+ apply (rule deflation.below)
+ apply (rule admD [OF adm_deflation eY])
+ apply (rule pre_deflation.deflation_d)
+ apply (rule pre_deflation_oo [OF d below])
+ done
+ finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" ..
+ qed
+qed
+
+subsection {* Take function for finite deflations *}
+
+definition
+ defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)"
+where
+ "defl_take i d = eventual_iterate (udom_approx i oo d)"
+
+lemma finite_deflation_defl_take:
+ "deflation d \<Longrightarrow> finite_deflation (defl_take i d)"
+unfolding defl_take_def
+apply (rule pre_deflation.finite_deflation_d)
+apply (rule pre_deflation_oo)
+apply (rule finite_deflation_udom_approx)
+apply (erule deflation.below)
+done
+
+lemma deflation_defl_take:
+ "deflation d \<Longrightarrow> deflation (defl_take i d)"
+apply (rule finite_deflation_imp_deflation)
+apply (erule finite_deflation_defl_take)
+done
+
+lemma defl_take_fixed_iff:
+ "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x"
+unfolding defl_take_def
+apply (rule eventual_iterate_oo_fixed_iff)
+apply (rule finite_deflation_udom_approx)
+apply (erule deflation.below)
+done
+
+lemma defl_take_below:
+ "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_take i a \<sqsubseteq> defl_take i b"
+apply (rule deflation.belowI)
+apply (erule deflation_defl_take)
+apply (simp add: defl_take_fixed_iff)
+apply (erule (1) deflation.belowD)
+apply (erule conjunct2)
+done
+
+lemma cont2cont_defl_take:
+ assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
+ shows "cont (\<lambda>x. defl_take i (f x))"
+unfolding defl_take_def
+using finite_deflation_udom_approx assms
+by (rule cont2cont_eventual_iterate_oo)
+
+definition
+ fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl"
+where
+ "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))"
+
+lemma Rep_fin_defl_fd_take:
+ "Rep_fin_defl (fd_take i d) = defl_take i (Rep_fin_defl d)"
+unfolding fd_take_def
+apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
+apply (rule finite_deflation_defl_take)
+apply (rule deflation_Rep_fin_defl)
+done
+
+lemma fd_take_fixed_iff:
+ "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
+ udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
+unfolding Rep_fin_defl_fd_take
+apply (rule defl_take_fixed_iff)
+apply (rule deflation_Rep_fin_defl)
+done
+
+lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
+apply (rule fin_defl_belowI)
+apply (simp add: fd_take_fixed_iff)
+done
+
+lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d"
+apply (rule fin_defl_eqI)
+apply (simp add: fd_take_fixed_iff)
+done
+
+lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
+apply (rule fin_defl_belowI)
+apply (simp add: fd_take_fixed_iff)
+apply (simp add: fin_defl_belowD)
+done
+
+lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x"
+apply (rule deflation.belowD)
+apply (rule finite_deflation_imp_deflation)
+apply (rule finite_deflation_udom_approx)
+apply (erule chain_mono [OF chain_udom_approx])
+apply assumption
+done
+
+lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
+apply (rule fin_defl_belowI)
+apply (simp add: fd_take_fixed_iff)
+apply (simp add: approx_fixed_le_lemma)
+done
+
+lemma finite_range_fd_take: "finite (range (fd_take n))"
+apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
+apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"])
+apply (clarify, simp add: fd_take_fixed_iff)
+apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx])
+apply (rule inj_onI, clarify)
+apply (simp add: set_eq_iff fin_defl_eqI)
+done
+
+lemma fd_take_covers: "\<exists>n. fd_take n a = a"
+apply (rule_tac x=
+ "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
+apply (rule below_antisym)
+apply (rule fd_take_below)
+apply (rule fin_defl_belowI)
+apply (simp add: fd_take_fixed_iff)
+apply (rule approx_fixed_le_lemma)
+apply (rule Max_ge)
+apply (rule finite_imageI)
+apply (rule Rep_fin_defl.finite_fixes)
+apply (rule imageI)
+apply (erule CollectI)
+apply (rule LeastI_ex)
+apply (rule approx_chain.compact_eq_approx [OF udom_approx])
+apply (erule subst)
+apply (rule Rep_fin_defl.compact)
+done
+
+subsection {* Chain of approx functions on algebraic deflations *}
+
+definition
+ defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl"
+where
+ "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
+
+lemma defl_approx_principal:
+ "defl_approx i\<cdot>(defl_principal d) = defl_principal (fd_take i d)"
+unfolding defl_approx_def
+by (simp add: defl.basis_fun_principal fd_take_mono)
+
+lemma defl_approx: "approx_chain defl_approx"
+proof
+ show chain: "chain defl_approx"
+ unfolding defl_approx_def
+ by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain)
+ show idem: "\<And>i x. defl_approx i\<cdot>(defl_approx i\<cdot>x) = defl_approx i\<cdot>x"
+ apply (induct_tac x rule: defl.principal_induct, simp)
+ apply (simp add: defl_approx_principal fd_take_idem)
+ done
+ show below: "\<And>i x. defl_approx i\<cdot>x \<sqsubseteq> x"
+ apply (induct_tac x rule: defl.principal_induct, simp)
+ apply (simp add: defl_approx_principal fd_take_below)
+ done
+ show lub: "(\<Squnion>i. defl_approx i) = ID"
+ apply (rule cfun_eqI, rule below_antisym)
+ apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
+ apply (induct_tac x rule: defl.principal_induct, simp)
+ apply (simp add: contlub_cfun_fun chain)
+ apply (simp add: compact_below_lub_iff defl.compact_principal chain)
+ apply (simp add: defl_approx_principal)
+ apply (subgoal_tac "\<exists>i. fd_take i a = a", metis below_refl)
+ apply (rule fd_take_covers)
+ done
+ show "\<And>i. finite {x. defl_approx i\<cdot>x = x}"
+ apply (rule finite_range_imp_finite_fixes)
+ apply (rule_tac B="defl_principal ` range (fd_take i)" in rev_finite_subset)
+ apply (simp add: finite_range_fd_take)
+ apply (clarsimp, rename_tac x)
+ apply (induct_tac x rule: defl.principal_induct)
+ apply (simp add: adm_mem_finite finite_range_fd_take)
+ apply (simp add: defl_approx_principal)
+ done
+qed
+
+subsection {* Algebraic deflations are a bifinite domain *}
+
+instantiation defl :: bifinite
+begin
+
+definition
+ "emb = udom_emb defl_approx"
+
+definition
+ "prj = udom_prj defl_approx"
+
+definition
+ "defl (t::defl itself) =
+ (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
+
+instance proof
+ show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
+ unfolding emb_defl_def prj_defl_def
+ by (rule ep_pair_udom [OF defl_approx])
+ show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)"
+ unfolding defl_defl_def
+ apply (subst contlub_cfun_arg)
+ apply (rule chainI)
+ apply (rule defl.principal_mono)
+ apply (simp add: below_fin_defl_def)
+ apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
+ ep_pair.finite_deflation_e_d_p [OF ep])
+ apply (intro monofun_cfun below_refl)
+ apply (rule chainE)
+ apply (rule approx_chain.chain_approx [OF defl_approx])
+ apply (subst cast_defl_principal)
+ apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
+ ep_pair.finite_deflation_e_d_p [OF ep])
+ apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx]
+ approx_chain.lub_approx [OF defl_approx])
+ done
+qed
+
+end
+
+end
--- a/src/HOLCF/Library/HOLCF_Library.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Library/HOLCF_Library.thy Sat Oct 16 16:39:06 2010 -0700
@@ -1,5 +1,6 @@
theory HOLCF_Library
imports
+ Defl_Bifinite
List_Cpo
Stream
Strict_Fun
--- a/src/HOLCF/Library/Stream.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Library/Stream.thy Sat Oct 16 16:39:06 2010 -0700
@@ -265,7 +265,7 @@
apply (simp add: stream.bisim_def,clarsimp)
apply (drule spec, drule spec, drule (1) mp)
apply (case_tac "x", simp)
- apply (case_tac "x'", simp)
+ apply (case_tac "y", simp)
by auto
@@ -508,7 +508,7 @@
by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
apply (subst sfilter_unfold, auto)
apply (case_tac "x=UU", auto)
by (drule stream_exhaust_eq [THEN iffD1], auto)
--- a/src/HOLCF/Library/Strict_Fun.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Library/Strict_Fun.thy Sat Oct 16 16:39:06 2010 -0700
@@ -37,13 +37,13 @@
unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
- by (simp add: expand_cfun_eq strictify_conv_if)
+ by (simp add: cfun_eq_iff strictify_conv_if)
lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
unfolding sfun_abs_def sfun_rep_def
apply (simp add: cont_Abs_sfun cont_Rep_sfun)
apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
- apply (simp add: expand_cfun_eq strictify_conv_if)
+ apply (simp add: cfun_eq_iff strictify_conv_if)
apply (simp add: Rep_sfun [simplified])
done
@@ -56,7 +56,7 @@
lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
apply default
apply (rule sfun_abs_sfun_rep)
-apply (simp add: expand_cfun_below strictify_conv_if)
+apply (simp add: cfun_below_iff strictify_conv_if)
done
interpretation sfun: ep_pair sfun_rep sfun_abs
@@ -71,14 +71,14 @@
lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
unfolding sfun_map_def
- by (simp add: cfun_map_ID expand_cfun_eq)
+ by (simp add: 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) =
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: expand_cfun_eq strictify_cancel assms cfun_map_map)
+by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
lemma ep_pair_sfun_map:
assumes 1: "ep_pair e1 p1"
@@ -193,7 +193,7 @@
next
show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
qed
end
--- a/src/HOLCF/Lift.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Lift.thy Sat Oct 16 16:39:06 2010 -0700
@@ -43,12 +43,6 @@
text {* @{term UU} and @{term Def} *}
-lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)"
- by (induct x) simp_all
-
-lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
- by (insert Lift_exhaust) blast
-
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
by (cases x) simp_all
@@ -86,17 +80,6 @@
by (induct x) auto
qed
-text {*
- \medskip Two specific lemmas for the combination of LCF and HOL
- terms.
-*}
-
-lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
-
-lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
-by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
-
subsection {* Further operations *}
definition
@@ -134,12 +117,12 @@
"(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
apply (rule monofunE [where f=flift1])
apply (rule cont2mono [OF cont_flift1])
-apply (simp add: below_fun_ext)
+apply (simp add: fun_below_iff)
done
lemma cont2cont_flift1 [simp, cont2cont]:
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
-apply (rule cont_flift1 [THEN cont2cont_app3])
+apply (rule cont_flift1 [THEN cont_compose])
apply simp
done
--- a/src/HOLCF/LowerPD.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Sat Oct 16 16:39:06 2010 -0700
@@ -323,7 +323,7 @@
lemma lower_bind_basis_mono:
"t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
-unfolding expand_cfun_below
+unfolding cfun_below_iff
apply (erule lower_le_induct, safe)
apply (simp add: monofun_cfun)
apply (simp add: rev_below_trans [OF lower_plus_below1])
@@ -371,7 +371,7 @@
by (induct xs rule: lower_pd_induct, simp_all)
lemma lower_map_ID: "lower_map\<cdot>ID = ID"
-by (simp add: expand_cfun_eq ID_def lower_map_ident)
+by (simp add: cfun_eq_iff ID_def lower_map_ident)
lemma lower_map_map:
"lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
@@ -483,7 +483,7 @@
next
show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq lower_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
qed
end
--- a/src/HOLCF/Porder.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Porder.thy Sat Oct 16 16:39:06 2010 -0700
@@ -344,87 +344,6 @@
lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
-subsection {* Directed sets *}
-
-definition directed :: "'a set \<Rightarrow> bool" where
- "directed S \<longleftrightarrow> (\<exists>x. x \<in> S) \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
-
-lemma directedI:
- assumes 1: "\<exists>z. z \<in> S"
- assumes 2: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
- shows "directed S"
- unfolding directed_def using prems by fast
-
-lemma directedD1: "directed S \<Longrightarrow> \<exists>z. z \<in> S"
- unfolding directed_def by fast
-
-lemma directedD2: "\<lbrakk>directed S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
- unfolding directed_def by fast
-
-lemma directedE1:
- assumes S: "directed S"
- obtains z where "z \<in> S"
- by (insert directedD1 [OF S], fast)
-
-lemma directedE2:
- assumes S: "directed S"
- assumes x: "x \<in> S" and y: "y \<in> S"
- obtains z where "z \<in> S" "x \<sqsubseteq> z" "y \<sqsubseteq> z"
- by (insert directedD2 [OF S x y], fast)
-
-lemma directed_finiteI:
- assumes U: "\<And>U. \<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. U <| z"
- shows "directed S"
-proof (rule directedI)
- have "finite {}" and "{} \<subseteq> S" by simp_all
- hence "\<exists>z\<in>S. {} <| z" by (rule U)
- thus "\<exists>z. z \<in> S" by simp
-next
- fix x y
- assume "x \<in> S" and "y \<in> S"
- hence "finite {x, y}" and "{x, y} \<subseteq> S" by simp_all
- hence "\<exists>z\<in>S. {x, y} <| z" by (rule U)
- thus "\<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" by simp
-qed
-
-lemma directed_finiteD:
- assumes S: "directed S"
- shows "\<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. U <| z"
-proof (induct U set: finite)
- case empty
- from S have "\<exists>z. z \<in> S" by (rule directedD1)
- thus "\<exists>z\<in>S. {} <| z" by simp
-next
- case (insert x F)
- from `insert x F \<subseteq> S`
- have xS: "x \<in> S" and FS: "F \<subseteq> S" by simp_all
- from FS have "\<exists>y\<in>S. F <| y" by fact
- then obtain y where yS: "y \<in> S" and Fy: "F <| y" ..
- obtain z where zS: "z \<in> S" and xz: "x \<sqsubseteq> z" and yz: "y \<sqsubseteq> z"
- using S xS yS by (rule directedE2)
- from Fy yz have "F <| z" by (rule is_ub_upward)
- with xz have "insert x F <| z" by simp
- with zS show "\<exists>z\<in>S. insert x F <| z" ..
-qed
-
-lemma not_directed_empty [simp]: "\<not> directed {}"
- by (rule notI, drule directedD1, simp)
-
-lemma directed_singleton: "directed {x}"
- by (rule directedI, auto)
-
-lemma directed_bin: "x \<sqsubseteq> y \<Longrightarrow> directed {x, y}"
- by (rule directedI, auto)
-
-lemma directed_chain: "chain S \<Longrightarrow> directed (range S)"
-apply (rule directedI)
-apply (rule_tac x="S 0" in exI, simp)
-apply (clarify, rename_tac m n)
-apply (rule_tac x="S (max m n)" in bexI)
-apply (simp add: chain_mono)
-apply simp
-done
-
text {* lemmata for improved admissibility introdution rule *}
lemma infinite_chain_adm_lemma:
--- a/src/HOLCF/Product_Cpo.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Product_Cpo.thy Sat Oct 16 16:39:06 2010 -0700
@@ -267,14 +267,6 @@
apply (simp only: prod_contI)
done
-lemma cont_fst_snd_D1:
- "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
-by (drule cont_compose [OF _ cont_pair1], simp)
-
-lemma cont_fst_snd_D2:
- "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
-by (drule cont_compose [OF _ cont_pair2], simp)
-
lemma cont2cont_prod_case' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
assumes g: "cont (\<lambda>x. g x)"
--- a/src/HOLCF/Representable.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Representable.thy Sat Oct 16 16:39:06 2010 -0700
@@ -45,7 +45,7 @@
by (simp add: coerce_def)
lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
-by (rule ext_cfun, simp add: beta_coerce)
+by (rule cfun_eqI, simp add: beta_coerce)
lemma emb_coerce:
"DEFL('a) \<sqsubseteq> DEFL('b)
@@ -169,7 +169,7 @@
apply (simp add: emb_prj cast.below)
done
show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
- by (rule ext_cfun, simp add: defl emb_prj)
+ by (rule cfun_eqI, simp add: defl emb_prj)
qed
lemma typedef_DEFL:
@@ -201,10 +201,10 @@
"isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
-unfolding isodefl_def by (simp add: ext_cfun)
+unfolding isodefl_def by (simp add: cfun_eqI)
lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
-unfolding isodefl_def by (simp add: ext_cfun)
+unfolding isodefl_def by (simp add: cfun_eqI)
lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
unfolding isodefl_def
@@ -228,14 +228,14 @@
lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
unfolding isodefl_def
apply (simp add: cast_DEFL)
-apply (simp add: expand_cfun_eq)
+apply (simp add: cfun_eq_iff)
apply (rule allI)
apply (drule_tac x="emb\<cdot>x" in spec)
apply simp
done
lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
-unfolding isodefl_def by (simp add: expand_cfun_eq)
+unfolding isodefl_def by (simp add: cfun_eq_iff)
lemma adm_isodefl:
"cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
@@ -263,7 +263,7 @@
assumes DEFL: "DEFL('b) = DEFL('a)"
shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
unfolding isodefl_def
-apply (simp add: expand_cfun_eq)
+apply (simp add: cfun_eq_iff)
apply (simp add: emb_coerce coerce_prj DEFL)
done
--- a/src/HOLCF/Sprod.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Sprod.thy Sat Oct 16 16:39:06 2010 -0700
@@ -250,7 +250,7 @@
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: expand_cfun_eq eta_cfun)
+unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
lemma sprod_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
--- a/src/HOLCF/Ssum.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Ssum.thy Sat Oct 16 16:39:06 2010 -0700
@@ -234,7 +234,7 @@
by (cases "x = \<bottom>") simp_all
lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
-unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
+unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
lemma ssum_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Oct 16 16:39:06 2010 -0700
@@ -7,26 +7,30 @@
signature DOMAIN_CONSTRUCTORS =
sig
+ type constr_info =
+ {
+ iso_info : Domain_Take_Proofs.iso_info,
+ con_specs : (term * (bool * typ) list) list,
+ con_betas : thm list,
+ nchotomy : thm,
+ exhaust : thm,
+ compacts : thm list,
+ con_rews : thm list,
+ inverts : thm list,
+ injects : thm list,
+ dist_les : thm list,
+ dist_eqs : thm list,
+ cases : thm list,
+ sel_rews : thm list,
+ dis_rews : thm list,
+ match_rews : thm list
+ }
val add_domain_constructors :
binding
-> (binding * (bool * binding option * typ) list * mixfix) list
-> Domain_Take_Proofs.iso_info
-> theory
- -> { con_consts : term list,
- con_betas : thm list,
- nchotomy : thm,
- exhaust : thm,
- compacts : thm list,
- con_rews : thm list,
- inverts : thm list,
- injects : thm list,
- dist_les : thm list,
- dist_eqs : thm list,
- cases : thm list,
- sel_rews : thm list,
- dis_rews : thm list,
- match_rews : thm list
- } * theory;
+ -> constr_info * theory;
end;
@@ -39,6 +43,25 @@
infix -->>;
infix 9 `;
+type constr_info =
+ {
+ iso_info : Domain_Take_Proofs.iso_info,
+ con_specs : (term * (bool * typ) list) list,
+ con_betas : thm list,
+ nchotomy : thm,
+ exhaust : thm,
+ compacts : thm list,
+ con_rews : thm list,
+ inverts : thm list,
+ injects : thm list,
+ dist_les : thm list,
+ dist_eqs : thm list,
+ cases : thm list,
+ sel_rews : thm list,
+ dis_rews : thm list,
+ match_rews : thm list
+ }
+
(************************** miscellaneous functions ***************************)
val simple_ss = HOL_basic_ss addsimps simp_thms;
@@ -833,6 +856,9 @@
(thy : theory) =
let
val dname = Binding.name_of dbind;
+ val _ = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+
+ val bindings = map #1 spec;
(* retrieve facts about rep/abs *)
val lhsT = #absT iso_info;
@@ -844,6 +870,7 @@
val abs_strict = iso_locale RS @{thm iso.abs_strict};
val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
+ val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict];
(* qualify constants and theorems with domain name *)
val thy = Sign.add_path dname thy;
@@ -857,18 +884,22 @@
in
add_constructors con_spec abs_const iso_locale thy
end;
- val {con_consts, con_betas, exhaust, ...} = con_result;
+ val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews,
+ inverts, injects, dist_les, dist_eqs} = con_result;
+
+ (* prepare constructor spec *)
+ val con_specs : (term * (bool * typ) list) list =
+ let
+ fun prep_arg (lazy, sel, T) = (lazy, T);
+ fun prep_con c (b, args, mx) = (c, map prep_arg args);
+ in
+ map2 prep_con con_consts spec
+ end;
(* define case combinator *)
val ((case_const : typ -> term, cases : thm list), thy) =
- let
- fun prep_arg (lazy, sel, T) = (lazy, T);
- fun prep_con c (b, args, mx) = (c, map prep_arg args);
- val case_spec = map2 prep_con con_consts spec;
- in
- add_case_combinator case_spec lhsT dbind
+ add_case_combinator con_specs lhsT dbind
con_betas exhaust iso_locale rep_const thy
- end;
(* define and prove theorems for selector functions *)
val (sel_thms : thm list, thy : theory) =
@@ -882,46 +913,61 @@
(* define and prove theorems for discriminator functions *)
val (dis_thms : thm list, thy : theory) =
- let
- val bindings = map #1 spec;
- fun prep_arg (lazy, sel, T) = (lazy, T);
- fun prep_con c (b, args, mx) = (c, map prep_arg args);
- val dis_spec = map2 prep_con con_consts spec;
- in
- add_discriminators bindings dis_spec lhsT
- exhaust case_const cases thy
- end
+ add_discriminators bindings con_specs lhsT
+ exhaust case_const cases thy;
(* define and prove theorems for match combinators *)
val (match_thms : thm list, thy : theory) =
- let
- val bindings = map #1 spec;
- fun prep_arg (lazy, sel, T) = (lazy, T);
- fun prep_con c (b, args, mx) = (c, map prep_arg args);
- val mat_spec = map2 prep_con con_consts spec;
- in
- add_match_combinators bindings mat_spec lhsT
- exhaust case_const cases thy
- end
+ add_match_combinators bindings con_specs lhsT
+ exhaust case_const cases thy;
(* restore original signature path *)
val thy = Sign.parent_path thy;
+ (* bind theorem names in global theory *)
+ val (_, thy) =
+ let
+ fun qualified name = Binding.qualified true name dbind;
+ val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
+ val dname = fst (dest_Type lhsT);
+ val simp = Simplifier.simp_add;
+ val case_names = Rule_Cases.case_names names;
+ val cases_type = Induct.cases_type dname;
+ in
+ Global_Theory.add_thmss [
+ ((qualified "iso_rews" , iso_rews ), [simp]),
+ ((qualified "nchotomy" , [nchotomy] ), []),
+ ((qualified "exhaust" , [exhaust] ), [case_names, cases_type]),
+ ((qualified "when_rews" , cases ), [simp]),
+ ((qualified "compacts" , compacts ), [simp]),
+ ((qualified "con_rews" , con_rews ), [simp]),
+ ((qualified "sel_rews" , sel_thms ), [simp]),
+ ((qualified "dis_rews" , dis_thms ), [simp]),
+ ((qualified "dist_les" , dist_les ), [simp]),
+ ((qualified "dist_eqs" , dist_eqs ), [simp]),
+ ((qualified "inverts" , inverts ), [simp]),
+ ((qualified "injects" , injects ), [simp]),
+ ((qualified "match_rews", match_thms ), [simp])] thy
+ end;
+
val result =
- { con_consts = con_consts,
+ {
+ iso_info = iso_info,
+ con_specs = con_specs,
con_betas = con_betas,
- nchotomy = #nchotomy con_result,
+ nchotomy = nchotomy,
exhaust = exhaust,
- compacts = #compacts con_result,
- con_rews = #con_rews con_result,
- inverts = #inverts con_result,
- injects = #injects con_result,
- dist_les = #dist_les con_result,
- dist_eqs = #dist_eqs con_result,
+ compacts = compacts,
+ con_rews = con_rews,
+ inverts = inverts,
+ injects = injects,
+ dist_les = dist_les,
+ dist_eqs = dist_eqs,
cases = cases,
sel_rews = sel_thms,
dis_rews = dis_thms,
- match_rews = match_thms };
+ match_rews = match_thms
+ };
in
(result, thy)
end;
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Sat Oct 16 16:39:06 2010 -0700
@@ -35,7 +35,15 @@
structure Domain_Extender :> DOMAIN_EXTENDER =
struct
-open Domain_Library;
+open HOLCF_Library;
+
+fun first (x,_,_) = x;
+fun second (_,x,_) = x;
+fun third (_,_,x) = x;
+
+fun upd_first f (x,y,z) = (f x, y, z);
+fun upd_second f (x,y,z) = ( x, f y, z);
+fun upd_third f (x,y,z) = ( x, y, f z);
(* ----- general testing and preprocessing of constructor list -------------- *)
fun check_and_sort_domain
@@ -94,22 +102,22 @@
| SOME typevars =>
if indirect
then error ("Indirect recursion of type " ^
- quote (string_of_typ thy t))
+ quote (Syntax.string_of_typ_global thy t))
else if dname <> s orelse
(** BUG OR FEATURE?:
mutual recursion may use different arguments **)
remove_sorts typevars = remove_sorts typl
then Type(s,map (analyse true) typl)
else error ("Direct recursion of type " ^
- quote (string_of_typ thy t) ^
+ quote (Syntax.string_of_typ_global thy t) ^
" with different arguments"))
- | analyse indirect (TVar _) = Imposs "extender:analyse";
+ | analyse indirect (TVar _) = error "extender:analyse";
fun check_pcpo lazy T =
let val sort = arg_sort lazy in
if Sign.of_sort thy (T, sort) then T
else error ("Constructor argument type is not of sort " ^
Syntax.string_of_sort_global thy sort ^ ": " ^
- string_of_typ thy T)
+ Syntax.string_of_typ_global thy T)
end;
fun analyse_arg (lazy, sel, T) =
(lazy, sel, check_pcpo lazy (analyse false T));
@@ -167,7 +175,7 @@
check_and_sort_domain arg_sort dtnvs' cons'' tmp_thy;
val dts : typ list = map (Type o fst) eqs';
- fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
+ fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T;
fun mk_con_typ (bind, args, mx) =
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
@@ -179,28 +187,17 @@
val ((iso_infos, take_info), thy) = add_isos iso_spec thy;
- val new_dts : (string * string list) list =
- map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun one_con (con,args,mx) : cons =
- (Binding.name_of con, (* FIXME preverse binding (!?) *)
- ListPair.map (fn ((lazy,sel,tp),vn) =>
- mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
- (args, Datatype_Prop.make_tnames (map third args)));
- val eqs : eq list =
- map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+ val (constr_infos, thy) =
+ thy
+ |> fold_map (fn ((dbind, (_,cs)), info) =>
+ Domain_Constructors.add_domain_constructors dbind cs info)
+ (dbinds ~~ eqs' ~~ iso_infos);
- val ((rewss, take_rews), theorems_thy) =
- thy
- |> fold_map (fn (((dbind, eq), (_,cs)), info) =>
- Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
- (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
- ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
+ val (take_rews, thy) =
+ Domain_Theorems.comp_theorems comp_dbind
+ dbinds take_info constr_infos thy;
in
- theorems_thy
- |> Global_Theory.add_thmss
- [((Binding.qualified true "rews" comp_dbind,
- flat rewss @ take_rews), [])]
- |> snd
+ thy
end;
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Oct 16 16:39:06 2010 -0700
@@ -639,9 +639,8 @@
val (take_info, thy) =
Domain_Take_Proofs.define_take_functions
(dbinds ~~ iso_infos) thy;
- val { take_consts, take_defs, chain_take_thms, take_0_thms,
- take_Suc_thms, deflation_take_thms,
- finite_consts, finite_defs } = take_info;
+ val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} =
+ take_info;
(* least-upper-bound lemma for take functions *)
val lub_take_lemma =
--- a/src/HOLCF/Tools/Domain/domain_library.ML Fri Oct 15 17:21:37 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,239 +0,0 @@
-(* Title: HOLCF/Tools/Domain/domain_library.ML
- Author: David von Oheimb
-
-Library for domain command.
-*)
-
-
-(* infix syntax *)
-
-infixr 5 -->;
-infixr 6 ->>;
-infixr 0 ===>;
-infixr 0 ==>;
-infix 0 ==;
-infix 1 ===;
-infix 1 ~=;
-
-infix 9 ` ;
-infix 9 `% ;
-infix 9 `%%;
-
-
-(* ----- specific support for domain ---------------------------------------- *)
-
-signature DOMAIN_LIBRARY =
-sig
- val first : 'a * 'b * 'c -> 'a
- val second : 'a * 'b * 'c -> 'b
- val third : 'a * 'b * 'c -> 'c
- val upd_second : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
- val upd_third : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
- val mapn : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
- val atomize : Proof.context -> thm -> thm list
-
- val Imposs : string -> 'a;
- val cpo_type : theory -> typ -> bool;
- val pcpo_type : theory -> typ -> bool;
- val string_of_typ : theory -> typ -> string;
-
- (* Creating HOLCF types *)
- val mk_ssumT : typ * typ -> typ;
- val mk_sprodT : typ * typ -> typ;
- val mk_uT : typ -> typ;
- val oneT : typ;
- val pcpoS : sort;
-
- (* Creating HOLCF terms *)
- val %: : string -> term;
- val %%: : string -> term;
- val ` : term * term -> term;
- val `% : term * string -> term;
- val UU : term;
- val ID : term;
- val list_ccomb : term * term list -> term;
- val con_app2 : string -> ('a -> term) -> 'a list -> term;
- val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a
- val proj : term -> 'a list -> int -> term;
-
- (* Creating propositions *)
- val mk_conj : term * term -> term;
- val mk_disj : term * term -> term;
- val mk_imp : term * term -> term;
- val mk_lam : string * term -> term;
- val mk_all : string * term -> term;
- val mk_ex : string * term -> term;
- val mk_constrainall : string * typ * term -> term;
- val === : term * term -> term;
- val defined : term -> term;
- val mk_adm : term -> term;
- val lift : ('a -> term) -> 'a list * term -> term;
- val lift_defined : ('a -> term) -> 'a list * term -> term;
-
- (* Creating meta-propositions *)
- val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
- val == : term * term -> term;
- val ===> : term * term -> term;
- val mk_All : string * term -> term;
-
- (* Domain specifications *)
- eqtype arg;
- type cons = string * arg list;
- type eq = (string * typ list) * cons list;
- val mk_arg : (bool * Datatype.dtyp) * string -> arg;
- val is_lazy : arg -> bool;
- val rec_of : arg -> int;
- val dtyp_of : arg -> Datatype.dtyp;
- val vname : arg -> string;
- val upd_vname : (string -> string) -> arg -> arg;
- val is_rec : arg -> bool;
- val is_nonlazy_rec : arg -> bool;
- val nonlazy : arg list -> string list;
- val nonlazy_rec : arg list -> string list;
- val %# : arg -> term;
- val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
- val idx_name : 'a list -> string -> int -> string;
- val con_app : string -> arg list -> term;
-end;
-
-structure Domain_Library :> DOMAIN_LIBRARY =
-struct
-
-fun first (x,_,_) = x;
-fun second (_,x,_) = x;
-fun third (_,_,x) = x;
-
-fun upd_first f (x,y,z) = (f x, y, z);
-fun upd_second f (x,y,z) = ( x, f y, z);
-fun upd_third f (x,y,z) = ( x, y, f z);
-
-fun mapn f n [] = []
- | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
-
-fun foldr'' f (l,f2) =
- let fun itr [] = raise Fail "foldr''"
- | itr [a] = f2 a
- | itr (a::l) = f(a, itr l)
- in itr l end;
-
-fun atomize ctxt thm =
- let
- val r_inst = read_instantiate ctxt;
- fun at thm =
- case concl_of thm of
- _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
- | _ => [thm];
- in map zero_var_indexes (at thm) end;
-
-exception Impossible of string;
-fun Imposs msg = raise Impossible ("Domain:"^msg);
-
-fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
-fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
-fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
-
-(* ----- constructor list handling ----- *)
-
-type arg =
- (bool * Datatype.dtyp) * (* (lazy, recursive element) *)
- string; (* argument name *)
-
-type cons =
- string * (* operator name of constr *)
- arg list; (* argument list *)
-
-type eq =
- (string * (* name of abstracted type *)
- typ list) * (* arguments of abstracted type *)
- cons list; (* represented type, as a constructor list *)
-
-val mk_arg = I;
-
-fun rec_of ((_,dtyp),_) =
- case dtyp of Datatype_Aux.DtRec i => i | _ => ~1;
-(* FIXME: what about indirect recursion? *)
-
-fun is_lazy arg = fst (fst arg);
-fun dtyp_of arg = snd (fst arg);
-val vname = snd;
-val upd_vname = apsnd;
-fun is_rec arg = rec_of arg >=0;
-fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
-fun nonlazy args = map vname (filter_out is_lazy args);
-fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
-
-
-(* ----- support for type and mixfix expressions ----- *)
-
-fun mk_uT T = Type(@{type_name "u"}, [T]);
-fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
-fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
-val oneT = @{typ one};
-
-(* ----- support for term expressions ----- *)
-
-fun %: s = Free(s,dummyT);
-fun %# arg = %:(vname arg);
-fun %%: s = Const(s,dummyT);
-
-local open HOLogic in
-val mk_trp = mk_Trueprop;
-fun mk_conj (S,T) = conj $ S $ T;
-fun mk_disj (S,T) = disj $ S $ T;
-fun mk_imp (S,T) = imp $ S $ T;
-fun mk_lam (x,T) = Abs(x,dummyT,T);
-fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
-fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type.constraint (typ --> boolT) (mk_lam(x,P)));
-end
-
-fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
-
-infixr 0 ===>; fun S ===> T = %%: "==>" $ S $ T;
-infix 0 ==; fun S == T = %%: "==" $ S $ T;
-infix 1 ===; fun S === T = %%: @{const_name HOL.eq} $ S $ T;
-infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
-
-infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
-infix 9 `% ; fun f`% s = f` %: s;
-infix 9 `%%; fun f`%%s = f` %%:s;
-
-fun mk_adm t = %%: @{const_name adm} $ t;
-val ID = %%: @{const_name ID};
-fun mk_strictify t = %%: @{const_name strictify}`t;
-fun mk_ssplit t = %%: @{const_name ssplit}`t;
-fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
-fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
-
-val pcpoS = @{sort pcpo};
-
-val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
-fun con_app2 con f args = list_ccomb(%%:con,map f args);
-fun con_app con = con_app2 con %#;
-fun prj _ _ x ( _::[]) _ = x
- | prj _ _ _ [] _ = raise Fail "Domain_Library.prj: empty list"
- | prj f1 _ x (_::y::ys) 0 = f1 x y
- | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun proj x = prj (fn S => K (%%: @{const_name fst} $ S)) (fn S => K (%%: @{const_name snd} $ S)) x;
-fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
-
-val UU = %%: @{const_name UU};
-fun defined t = t ~= UU;
-fun cpair (t,u) = %%: @{const_name Pair} $ t $ u;
-fun spair (t,u) = %%: @{const_name spair}`t`u;
-fun lift_defined f = lift (fn x => defined (f x));
-fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
-
-fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
- (case cont_eta_contract body of
- body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) =>
- if not (member (op =) (loose_bnos f) 0) then incr_boundvars ~1 f
- else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
- | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body'))
- | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
- | cont_eta_contract t = t;
-
-fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
-
-end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Oct 16 16:39:06 2010 -0700
@@ -24,6 +24,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list
}
@@ -35,6 +36,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list,
lub_take_thms : thm list,
@@ -80,6 +82,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list
};
@@ -92,6 +95,7 @@
take_0_thms : thm list,
take_Suc_thms : thm list,
deflation_take_thms : thm list,
+ take_strict_thms : thm list,
finite_consts : term list,
finite_defs : thm list,
lub_take_thms : thm list,
@@ -299,7 +303,7 @@
val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
in
- add_qualified_thm "take_0" (dbind, take_0_thm) thy
+ add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy
end;
val (take_0_thms, thy) =
fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy;
@@ -369,7 +373,7 @@
Drule.zero_var_indexes
(@{thm deflation_strict} OF [deflation_take]);
in
- add_qualified_thm "take_strict" (dbind, take_strict_thm) thy
+ add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy
end;
val (take_strict_thms, thy) =
fold_map prove_take_strict
@@ -429,6 +433,7 @@
take_0_thms = take_0_thms,
take_Suc_thms = take_Suc_thms,
deflation_take_thms = deflation_take_thms,
+ take_strict_thms = take_strict_thms,
finite_consts = finite_consts,
finite_defs = finite_defs
};
@@ -593,6 +598,7 @@
take_0_thms = #take_0_thms take_info,
take_Suc_thms = #take_Suc_thms take_info,
deflation_take_thms = #deflation_take_thms take_info,
+ take_strict_thms = #take_strict_thms take_info,
finite_consts = #finite_consts take_info,
finite_defs = #finite_defs take_info,
lub_take_thms = lub_take_thms,
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Oct 16 16:39:06 2010 -0700
@@ -9,17 +9,10 @@
signature DOMAIN_THEOREMS =
sig
- val theorems:
- Domain_Library.eq * Domain_Library.eq list ->
- binding ->
- (binding * (bool * binding option * typ) list * mixfix) list ->
- Domain_Take_Proofs.iso_info ->
+ val comp_theorems :
+ binding -> binding list ->
Domain_Take_Proofs.take_induct_info ->
- theory -> thm list * theory;
-
- val comp_theorems :
- binding * Domain_Library.eq list ->
- Domain_Take_Proofs.take_induct_info ->
+ Domain_Constructors.constr_info list ->
theory -> thm list * theory
val quiet_mode: bool Unsynchronized.ref;
@@ -35,18 +28,11 @@
fun message s = if !quiet_mode then () else writeln s;
fun trace s = if !trace_domain then tracing s else ();
-open Domain_Library;
+open HOLCF_Library;
infixr 0 ===>;
-infixr 0 ==>;
infix 0 == ;
infix 1 ===;
-infix 1 ~= ;
-infix 1 <<;
-infix 1 ~<<;
infix 9 ` ;
-infix 9 `% ;
-infix 9 `%%;
-infixr 9 oo;
(* ----- general proof facilities ------------------------------------------- *)
@@ -91,340 +77,218 @@
else cut_facts_tac prems 1 :: tacsf context;
in pg'' thy defs t tacs end;
-(* FIXME!!!!!!!!! *)
-(* We should NEVER re-parse variable names as strings! *)
-(* The names can conflict with existing constants or other syntax! *)
-fun case_UU_tac ctxt rews i v =
- InductTacs.case_tac ctxt (v^"=UU") i THEN
- asm_simp_tac (HOLCF_ss addsimps rews) i;
+(******************************************************************************)
+(***************************** proofs about take ******************************)
+(******************************************************************************)
+
+fun take_theorems
+ (dbinds : binding list)
+ (take_info : Domain_Take_Proofs.take_induct_info)
+ (constr_infos : Domain_Constructors.constr_info list)
+ (thy : theory) : thm list list * theory =
+let
+ val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info;
+ val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
+
+ val n = Free ("n", @{typ nat});
+ val n' = @{const Suc} $ n;
+
+ local
+ val newTs = map (#absT o #iso_info) constr_infos;
+ val subs = newTs ~~ map (fn t => t $ n) take_consts;
+ fun is_ID (Const (c, _)) = (c = @{const_name ID})
+ | is_ID _ = false;
+ in
+ fun map_of_arg v T =
+ let val m = Domain_Take_Proofs.map_of_typ thy subs T;
+ in if is_ID m then v else mk_capply (m, v) end;
+ end
+
+ fun prove_take_apps
+ ((dbind, take_const), constr_info) thy =
+ let
+ val {iso_info, con_specs, con_betas, ...} = constr_info;
+ val {abs_inverse, ...} = iso_info;
+ fun prove_take_app (con_const, args) =
+ let
+ val Ts = map snd args;
+ val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
+ val vs = map Free (ns ~~ Ts);
+ val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
+ val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts);
+ val goal = mk_trp (mk_eq (lhs, rhs));
+ val rules =
+ [abs_inverse] @ con_betas @ @{thms take_con_rules}
+ @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
+ val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+ val take_apps = map prove_take_app con_specs;
+ in
+ yield_singleton Global_Theory.add_thmss
+ ((Binding.qualified true "take_rews" dbind, take_apps),
+ [Simplifier.simp_add]) thy
+ end;
+in
+ fold_map prove_take_apps
+ (dbinds ~~ take_consts ~~ constr_infos) thy
+end;
(* ----- general proofs ----------------------------------------------------- *)
val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
-fun theorems
- (((dname, _), cons) : eq, eqs : eq list)
- (dbind : binding)
- (spec : (binding * (bool * binding option * typ) list * mixfix) list)
- (iso_info : Domain_Take_Proofs.iso_info)
- (take_info : Domain_Take_Proofs.take_induct_info)
- (thy : theory) =
-let
-
-val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
-val map_tab = Domain_Take_Proofs.get_map_tab thy;
-
-
-(* ----- getting the axioms and definitions --------------------------------- *)
-
-val ax_abs_iso = #abs_inverse iso_info;
-val ax_rep_iso = #rep_inverse iso_info;
-
-val abs_const = #abs_const iso_info;
-val rep_const = #rep_const iso_info;
-
-local
- fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
-in
- val ax_take_0 = ga "take_0" dname;
- val ax_take_strict = ga "take_strict" dname;
-end; (* local *)
-
-val {take_Suc_thms, deflation_take_thms, ...} = take_info;
-
-(* ----- define constructors ------------------------------------------------ *)
-
-val (result, thy) =
- Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
-
-val con_appls = #con_betas result;
-val {nchotomy, exhaust, ...} = result;
-val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
-val {sel_rews, ...} = result;
-val when_rews = #cases result;
-val when_strict = hd when_rews;
-val dis_rews = #dis_rews result;
-val mat_rews = #match_rews result;
-
-(* ----- theorems concerning the isomorphism -------------------------------- *)
-
-val pg = pg' thy;
-
-val retraction_strict = @{thm retraction_strict};
-val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
-val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
-
-(* ----- theorems concerning one induction step ----------------------------- *)
-
-local
- fun dc_take dn = %%:(dn^"_take");
- val dnames = map (fst o fst) eqs;
- val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
-
- fun copy_of_dtyp tab r dt =
- if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
- and copy tab r (Datatype_Aux.DtRec i) = r i
- | copy tab r (Datatype_Aux.DtTFree a) = ID
- | copy tab r (Datatype_Aux.DtType (c, ds)) =
- case Symtab.lookup tab c of
- SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
- | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
-
- fun one_take_app (con, args) =
- let
- fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
- fun one_rhs arg =
- if Datatype_Aux.is_rec_type (dtyp_of arg)
- then copy_of_dtyp map_tab
- mk_take (dtyp_of arg) ` (%# arg)
- else (%# arg);
- val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args);
- val rhs = con_app2 con one_rhs args;
- val goal = mk_trp (lhs === rhs);
- val rules =
- [ax_abs_iso] @ @{thms take_con_rules}
- @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
- val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
- in pg con_appls goal (K tacs) end;
- val take_apps = map one_take_app cons;
-in
- val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
-end;
-
-val case_ns =
- "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
-
-fun qualified name = Binding.qualified true name dbind;
-val simp = Simplifier.simp_add;
-
-in
- thy
- |> Global_Theory.add_thmss [
- ((qualified "iso_rews" , iso_rews ), [simp]),
- ((qualified "nchotomy" , [nchotomy] ), []),
- ((qualified "exhaust" , [exhaust] ),
- [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
- ((qualified "when_rews" , when_rews ), [simp]),
- ((qualified "compacts" , compacts ), [simp]),
- ((qualified "con_rews" , con_rews ), [simp]),
- ((qualified "sel_rews" , sel_rews ), [simp]),
- ((qualified "dis_rews" , dis_rews ), [simp]),
- ((qualified "dist_les" , dist_les ), [simp]),
- ((qualified "dist_eqs" , dist_eqs ), [simp]),
- ((qualified "inverts" , inverts ), [simp]),
- ((qualified "injects" , injects ), [simp]),
- ((qualified "take_rews" , take_rews ), [simp]),
- ((qualified "match_rews", mat_rews ), [simp])]
- |> snd
- |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- dist_les @ dist_eqs)
-end; (* let *)
+val case_UU_allI =
+ @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis};
(******************************************************************************)
(****************************** induction rules *******************************)
(******************************************************************************)
fun prove_induction
- (comp_dbind : binding, eqs : eq list)
+ (comp_dbind : binding)
+ (constr_infos : Domain_Constructors.constr_info list)
+ (take_info : Domain_Take_Proofs.take_induct_info)
(take_rews : thm list)
- (take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
- val comp_dname = Sign.full_name thy comp_dbind;
- val dnames = map (fst o fst) eqs;
- val conss = map snd eqs;
- fun dc_take dn = %%:(dn^"_take");
- val x_name = idx_name dnames "x";
- val P_name = idx_name dnames "P";
- val pg = pg' thy;
+ val comp_dname = Binding.name_of comp_dbind;
+
+ val iso_infos = map #iso_info constr_infos;
+ val exhausts = map #exhaust constr_infos;
+ val con_rews = maps #con_rews constr_infos;
+ val {take_consts, take_induct_thms, ...} = take_info;
- local
- fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
- fun gts s dn = Global_Theory.get_thms thy (dn ^ "." ^ s);
- in
- val axs_rep_iso = map (ga "rep_iso") dnames;
- val axs_abs_iso = map (ga "abs_iso") dnames;
- val exhausts = map (ga "exhaust" ) dnames;
- val con_rews = maps (gts "con_rews" ) dnames;
- end;
+ val newTs = map #absT iso_infos;
+ val P_names = Datatype_Prop.indexify_names (map (K "P") newTs);
+ val x_names = Datatype_Prop.indexify_names (map (K "x") newTs);
+ val P_types = map (fn T => T --> HOLogic.boolT) newTs;
+ val Ps = map Free (P_names ~~ P_types);
+ val xs = map Free (x_names ~~ newTs);
+ val n = Free ("n", HOLogic.natT);
- val {take_consts, ...} = take_info;
- val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
- val {lub_take_thms, finite_defs, reach_thms, ...} = take_info;
- val {take_induct_thms, ...} = take_info;
-
- fun one_con p (con, args) =
+ fun con_assm defined p (con, args) =
let
- val P_names = map P_name (1 upto (length dnames));
- val vns = Name.variant_list P_names (map vname args);
- val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
- fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
- val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
- val t2 = lift ind_hyp (filter is_rec args, t1);
- val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
- in Library.foldr mk_All (vns, t3) end;
+ val Ts = map snd args;
+ val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts);
+ val vs = map Free (ns ~~ Ts);
+ val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
+ fun ind_hyp (v, T) t =
+ case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t
+ | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t);
+ val t1 = mk_trp (p $ list_ccomb (con, vs));
+ val t2 = fold_rev ind_hyp (vs ~~ Ts) t1;
+ val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2);
+ in fold_rev Logic.all vs (if defined then t3 else t2) end;
+ fun eq_assms ((p, T), cons) =
+ mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons;
+ val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos);
- fun one_eq ((p, cons), concl) =
- mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
-
- fun ind_term concf = Library.foldr one_eq
- (mapn (fn n => fn x => (P_name n, x)) 1 conss,
- mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
fun quant_tac ctxt i = EVERY
- (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
+ (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names);
- fun ind_prems_tac prems = EVERY
- (maps (fn cons =>
- (resolve_tac prems 1 ::
- maps (fn (_,args) =>
- resolve_tac prems 1 ::
- map (K(atac 1)) (nonlazy args) @
- map (K(atac 1)) (filter is_rec args))
- cons))
- conss);
- local
- fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg =>
- is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
- ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse
- rec_of arg <> n andalso rec_to (rec_of arg::ns)
- (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
- ) o snd) cons;
- fun warn (n,cons) =
- if rec_to [] false (n,cons)
- then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
- else false;
+ (* FIXME: move this message to domain_take_proofs.ML *)
+ val is_finite = #is_finite take_info;
+ val _ = if is_finite
+ then message ("Proving finiteness rule for domain "^comp_dname^" ...")
+ else ();
- in
- val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
- val is_emptys = map warn n__eqs;
- val is_finite = #is_finite take_info;
- val _ = if is_finite
- then message ("Proving finiteness rule for domain "^comp_dname^" ...")
- else ();
- end;
val _ = trace " Proving finite_ind...";
val finite_ind =
let
- fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
- val goal = ind_term concf;
+ val concls =
+ map (fn ((P, t), x) => P $ mk_capply (t $ n, x))
+ (Ps ~~ take_consts ~~ xs);
+ val goal = mk_trp (foldr1 mk_conj concls);
fun tacf {prems, context} =
let
+ (* Prove stronger prems, without definedness side conditions *)
+ fun con_thm p (con, args) =
+ let
+ val subgoal = con_assm false p (con, args);
+ val rules = prems @ con_rews @ simp_thms;
+ val simplify = asm_simp_tac (HOL_basic_ss addsimps rules);
+ fun arg_tac (lazy, _) =
+ rtac (if lazy then allI else case_UU_allI) 1;
+ val tacs =
+ rewrite_goals_tac @{thms atomize_all atomize_imp} ::
+ map arg_tac args @
+ [REPEAT (rtac impI 1), ALLGOALS simplify];
+ in
+ Goal.prove context [] [] subgoal (K (EVERY tacs))
+ end;
+ fun eq_thms (p, cons) = map (con_thm p) cons;
+ val conss = map #con_specs constr_infos;
+ val prems' = maps eq_thms (Ps ~~ conss);
+
val tacs1 = [
quant_tac context 1,
simp_tac HOL_ss 1,
InductTacs.induct_tac context [[SOME "n"]] 1,
simp_tac (take_ss addsimps prems) 1,
TRY (safe_tac HOL_cs)];
- fun arg_tac arg =
- (* FIXME! case_UU_tac *)
- case_UU_tac context (prems @ con_rews) 1
- (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
- fun con_tacs (con, args) =
- asm_simp_tac take_ss 1 ::
- map arg_tac (filter is_nonlazy_rec args) @
- [resolve_tac prems 1] @
- map (K (atac 1)) (nonlazy args) @
- map (K (etac spec 1)) (filter is_rec args);
+ fun con_tac _ =
+ asm_simp_tac take_ss 1 THEN
+ (resolve_tac prems' THEN_ALL_NEW etac spec) 1;
fun cases_tacs (cons, exhaust) =
res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
- maps con_tacs cons;
+ map con_tac cons;
+ val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
in
- tacs1 @ maps cases_tacs (conss ~~ exhausts)
+ EVERY (map DETERM tacs)
end;
- in pg'' thy [] goal tacf end;
-
-(* ----- theorems concerning finiteness and induction ----------------------- *)
-
- val global_ctxt = ProofContext.init_global thy;
+ in Goal.prove_global thy [] assms goal tacf end;
val _ = trace " Proving ind...";
val ind =
- if is_finite
- then (* finite case *)
- let
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- fun tacf {prems, context} =
- let
- fun finite_tacs (take_induct, fin_ind) = [
- rtac take_induct 1,
- rtac fin_ind 1,
- ind_prems_tac prems];
- in
- TRY (safe_tac HOL_cs) ::
- maps finite_tacs (take_induct_thms ~~ atomize global_ctxt finite_ind)
- end;
- in pg'' thy [] (ind_term concf) tacf end
+ let
+ val concls = map (op $) (Ps ~~ xs);
+ val goal = mk_trp (foldr1 mk_conj concls);
+ val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps;
+ fun tacf {prems, context} =
+ let
+ fun finite_tac (take_induct, fin_ind) =
+ rtac take_induct 1 THEN
+ (if is_finite then all_tac else resolve_tac prems 1) THEN
+ (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1;
+ val fin_inds = Project_Rule.projections context finite_ind;
+ in
+ TRY (safe_tac HOL_cs) THEN
+ EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
+ end;
+ in Goal.prove_global thy [] (adms @ assms) goal tacf end
- else (* infinite case *)
- let
- val goal =
- let
- fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
- val cont_rules =
- @{thms cont_id cont_const cont2cont_Rep_CFun
- cont2cont_fst cont2cont_snd};
- val subgoal =
- let
- val Ts = map (Type o fst) eqs;
- val P_names = Datatype_Prop.indexify_names (map (K "P") dnames);
- val x_names = Datatype_Prop.indexify_names (map (K "x") dnames);
- val P_types = map (fn T => T --> HOLogic.boolT) Ts;
- val Ps = map Free (P_names ~~ P_types);
- val xs = map Free (x_names ~~ Ts);
- val n = Free ("n", HOLogic.natT);
- val goals =
- map (fn ((P,t),x) => P $ HOLCF_Library.mk_capply (t $ n, x))
- (Ps ~~ take_consts ~~ xs);
- in
- HOLogic.mk_Trueprop
- (HOLogic.mk_all ("n", HOLogic.natT, foldr1 HOLogic.mk_conj goals))
- end;
- fun tacf {prems, context} =
- let
- val subtac =
- EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
- val subthm = Goal.prove context [] [] subgoal (K subtac);
- in
- map (fn ax_reach => rtac (ax_reach RS subst) 1) reach_thms @ [
- cut_facts_tac (subthm :: take (length dnames) prems) 1,
- REPEAT (rtac @{thm conjI} 1 ORELSE
- EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
- resolve_tac chain_take_thms 1,
- asm_simp_tac HOL_basic_ss 1])
- ]
- end;
- in pg'' thy [] goal tacf end;
+ (* case names for induction rules *)
+ val dnames = map (fst o dest_Type) newTs;
+ val case_ns =
+ let
+ val adms =
+ if is_finite then [] else
+ if length dnames = 1 then ["adm"] else
+ map (fn s => "adm_" ^ Long_Name.base_name s) dnames;
+ val bottoms =
+ if length dnames = 1 then ["bottom"] else
+ map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
+ fun one_eq bot constr_info =
+ let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c));
+ in bot :: map name_of (#con_specs constr_info) end;
+ in adms @ flat (map2 one_eq bottoms constr_infos) end;
-val case_ns =
- let
- val adms =
- if is_finite then [] else
- if length dnames = 1 then ["adm"] else
- map (fn s => "adm_" ^ Long_Name.base_name s) dnames;
- val bottoms =
- if length dnames = 1 then ["bottom"] else
- map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
- fun one_eq bot (_,cons) =
- bot :: map (fn (c,_) => Long_Name.base_name c) cons;
- in adms @ flat (map2 one_eq bottoms eqs) end;
-
-val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
-fun ind_rule (dname, rule) =
- ((Binding.empty, [rule]),
- [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
+ val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
+ fun ind_rule (dname, rule) =
+ ((Binding.empty, rule),
+ [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
in
thy
- |> snd o Global_Theory.add_thmss [
- ((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []),
- ((Binding.qualified true "induct" comp_dbind, [ind] ), [])]
- |> (snd o Global_Theory.add_thmss (map ind_rule (dnames ~~ inducts)))
+ |> snd o Global_Theory.add_thms [
+ ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []),
+ ((Binding.qualified true "induct" comp_dbind, ind ), [])]
+ |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts)))
end; (* prove_induction *)
(******************************************************************************)
@@ -432,166 +296,171 @@
(******************************************************************************)
fun prove_coinduction
- (comp_dbind : binding, eqs : eq list)
- (take_lemmas : thm list)
+ (comp_dbind : binding, dbinds : binding list)
+ (constr_infos : Domain_Constructors.constr_info list)
+ (take_info : Domain_Take_Proofs.take_induct_info)
+ (take_rews : thm list list)
(thy : theory) : theory =
let
+ val iso_infos = map #iso_info constr_infos;
+ val newTs = map #absT iso_infos;
-val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_name thy comp_dbind;
-fun dc_take dn = %%:(dn^"_take");
-val x_name = idx_name dnames "x";
-val n_eqs = length eqs;
-
-val take_rews =
- maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
+ val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info;
-(* ----- define bisimulation predicate -------------------------------------- *)
+ val R_names = Datatype_Prop.indexify_names (map (K "R") newTs);
+ val R_types = map (fn T => T --> T --> boolT) newTs;
+ val Rs = map Free (R_names ~~ R_types);
+ val n = Free ("n", natT);
+ val reserved = "x" :: "y" :: R_names;
-local
- open HOLCF_Library
- val dtypes = map (Type o fst) eqs;
- val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
+ (* declare bisimulation predicate *)
val bisim_bind = Binding.suffix_name "_bisim" comp_dbind;
- val bisim_type = relprod --> boolT;
-in
+ val bisim_type = R_types ---> boolT;
val (bisim_const, thy) =
Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy;
-end;
-
-local
- fun legacy_infer_term thy t =
- singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
- fun legacy_infer_prop thy t = legacy_infer_term thy (Type.constraint propT t);
- fun infer_props thy = map (apsnd (legacy_infer_prop thy));
- fun add_defs_i x = Global_Theory.add_defs false (map Thm.no_attributes x);
- fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
+ (* define bisimulation predicate *)
+ local
+ fun one_con T (con, args) =
+ let
+ val Ts = map snd args;
+ val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts);
+ val ns2 = map (fn n => n^"'") ns1;
+ val vs1 = map Free (ns1 ~~ Ts);
+ val vs2 = map Free (ns2 ~~ Ts);
+ val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1));
+ val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2));
+ fun rel ((v1, v2), T) =
+ case AList.lookup (op =) (newTs ~~ Rs) T of
+ NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2;
+ val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]);
+ in
+ Library.foldr mk_ex (vs1 @ vs2, eqs)
+ end;
+ fun one_eq ((T, R), cons) =
+ let
+ val x = Free ("x", T);
+ val y = Free ("y", T);
+ val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T));
+ val disjs = disj1 :: map (one_con T) cons;
+ in
+ mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs)))
+ end;
+ val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos);
+ val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs);
+ val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs);
+ in
+ val (bisim_def_thm, thy) = thy |>
+ yield_singleton (Global_Theory.add_defs false)
+ ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []);
+ end (* local *)
- fun one_con (con, args) =
+ (* prove coinduction lemma *)
+ val coind_lemma =
let
- val nonrec_args = filter_out is_rec args;
- val rec_args = filter is_rec args;
- val recs_cnt = length rec_args;
- val allargs = nonrec_args @ rec_args
- @ map (upd_vname (fn s=> s^"'")) rec_args;
- val allvns = map vname allargs;
- fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
- val vns1 = map (vname_arg "" ) args;
- val vns2 = map (vname_arg "'") args;
- val allargs_cnt = length nonrec_args + 2*recs_cnt;
- val rec_idxs = (recs_cnt-1) downto 0;
- val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
- (allargs~~((allargs_cnt-1) downto 0)));
- fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $
- Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
- val capps =
- List.foldr
- mk_conj
- (mk_conj(
- Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
- Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
- (mapn rel_app 1 rec_args);
+ val assm = mk_trp (list_comb (bisim_const, Rs));
+ fun one ((T, R), take_const) =
+ let
+ val x = Free ("x", T);
+ val y = Free ("y", T);
+ val lhs = mk_capply (take_const $ n, x);
+ val rhs = mk_capply (take_const $ n, y);
+ in
+ mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs))))
+ end;
+ val goal =
+ mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)));
+ val rules = @{thm Rep_CFun_strict1} :: take_0_thms;
+ fun tacf {prems, context} =
+ let
+ val prem' = rewrite_rule [bisim_def_thm] (hd prems);
+ val prems' = Project_Rule.projections context prem';
+ val dests = map (fn th => th RS spec RS spec RS mp) prems';
+ fun one_tac (dest, rews) =
+ dtac dest 1 THEN safe_tac HOL_cs THEN
+ ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews));
+ in
+ rtac @{thm nat.induct} 1 THEN
+ simp_tac (HOL_ss addsimps rules) 1 THEN
+ safe_tac HOL_cs THEN
+ EVERY (map one_tac (dests ~~ take_rews))
+ end
in
- List.foldr
- mk_ex
- (Library.foldr mk_conj
- (map (defined o Bound) nonlazy_idxs,capps)) allvns
+ Goal.prove_global thy [] [assm] goal tacf
end;
- fun one_comp n (_,cons) =
- mk_all (x_name(n+1),
- mk_all (x_name(n+1)^"'",
- mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
- foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
- ::map one_con cons))));
- val bisim_eqn =
- %%:(comp_dname^"_bisim") ==
- mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
+
+ (* prove individual coinduction rules *)
+ fun prove_coind ((T, R), take_lemma) =
+ let
+ val x = Free ("x", T);
+ val y = Free ("y", T);
+ val assm1 = mk_trp (list_comb (bisim_const, Rs));
+ val assm2 = mk_trp (R $ x $ y);
+ val goal = mk_trp (mk_eq (x, y));
+ fun tacf {prems, context} =
+ let
+ val rule = hd prems RS coind_lemma;
+ in
+ rtac take_lemma 1 THEN
+ asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1
+ end;
+ in
+ Goal.prove_global thy [] [assm1, assm2] goal tacf
+ end;
+ val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms);
+ val coind_binds = map (Binding.qualified true "coinduct") dbinds;
in
- val (ax_bisim_def, thy) =
- yield_singleton add_defs_infer
- (Binding.qualified true "bisim_def" comp_dbind, bisim_eqn) thy;
-end; (* local *)
-
-(* ----- theorem concerning coinduction ------------------------------------- *)
-
-local
- val pg = pg' thy;
- val xs = mapn (fn n => K (x_name n)) 1 dnames;
- fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
- val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
- val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
- val _ = trace " Proving coind_lemma...";
- val coind_lemma =
- let
- fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
- fun mk_eqn n dn =
- (dc_take dn $ %:"n" ` bnd_arg n 0) ===
- (dc_take dn $ %:"n" ` bnd_arg n 1);
- fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
- val goal =
- mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
- Library.foldr mk_all2 (xs,
- Library.foldr mk_imp (mapn mk_prj 0 dnames,
- foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
- fun x_tacs ctxt n x = [
- rotate_tac (n+1) 1,
- etac all2E 1,
- eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
- TRY (safe_tac HOL_cs),
- REPEAT (CHANGED (asm_simp_tac take_ss 1))];
- fun tacs ctxt = [
- rtac impI 1,
- InductTacs.induct_tac ctxt [[SOME "n"]] 1,
- simp_tac take_ss 1,
- safe_tac HOL_cs] @
- flat (mapn (x_tacs ctxt) 0 xs);
- in pg [ax_bisim_def] goal tacs end;
-in
- val _ = trace " Proving coind...";
- val coind =
- let
- fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
- fun mk_eqn x = %:x === %:(x^"'");
- val goal =
- mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
- Logic.list_implies (mapn mk_prj 0 xs,
- mk_trp (foldr1 mk_conj (map mk_eqn xs)));
- val tacs =
- TRY (safe_tac HOL_cs) ::
- maps (fn take_lemma => [
- rtac take_lemma 1,
- cut_facts_tac [coind_lemma] 1,
- fast_tac HOL_cs 1])
- take_lemmas;
- in pg [] goal (K tacs) end;
-end; (* local *)
-
-in thy |> snd o Global_Theory.add_thmss
- [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])]
+ thy |> snd o Global_Theory.add_thms
+ (map Thm.no_attributes (coind_binds ~~ coinds))
end; (* let *)
+(******************************************************************************)
+(******************************* main function ********************************)
+(******************************************************************************)
+
fun comp_theorems
- (comp_dbind : binding, eqs : eq list)
+ (comp_dbind : binding)
+ (dbinds : binding list)
(take_info : Domain_Take_Proofs.take_induct_info)
+ (constr_infos : Domain_Constructors.constr_info list)
(thy : theory) =
let
-val map_tab = Domain_Take_Proofs.get_map_tab thy;
+val comp_dname = Binding.name_of comp_dbind;
-val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_name thy comp_dbind;
-
-(* ----- getting the composite axiom and definitions ------------------------ *)
+(* Test for emptiness *)
+(* FIXME: reimplement emptiness test
+local
+ open Domain_Library;
+ val dnames = map (fst o fst) eqs;
+ val conss = map snd eqs;
+ fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg =>
+ is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
+ ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse
+ rec_of arg <> n andalso rec_to (rec_of arg::ns)
+ (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
+ ) o snd) cons;
+ fun warn (n,cons) =
+ if rec_to [] false (n,cons)
+ then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
+ else false;
+in
+ val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
+ val is_emptys = map warn n__eqs;
+end;
+*)
(* Test for indirect recursion *)
local
- fun indirect_arg arg =
- rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg);
+ val newTs = map (#absT o #iso_info) constr_infos;
+ fun indirect_typ (Type (_, Ts)) =
+ exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts
+ | indirect_typ _ = false;
+ fun indirect_arg (_, T) = indirect_typ T;
fun indirect_con (_, args) = exists indirect_arg args;
- fun indirect_eq (_, cons) = exists indirect_con cons;
+ fun indirect_eq cons = exists indirect_con cons;
in
- val is_indirect = exists indirect_eq eqs;
+ val is_indirect = exists indirect_eq (map #con_specs constr_infos);
val _ =
if is_indirect
then message "Indirect recursion detected, skipping proofs of (co)induction rules"
@@ -600,19 +469,21 @@
(* theorems about take *)
-val take_lemmas = #take_lemma_thms take_info;
+val (take_rewss, thy) =
+ take_theorems dbinds take_info constr_infos thy;
-val take_rews =
- maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
+val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
+
+val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss;
(* prove induction rules, unless definition is indirect recursive *)
val thy =
if is_indirect then thy else
- prove_induction (comp_dbind, eqs) take_rews take_info thy;
+ prove_induction comp_dbind constr_infos take_info take_rews thy;
val thy =
if is_indirect then thy else
- prove_coinduction (comp_dbind, eqs) take_lemmas thy;
+ prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy;
in
(take_rews, thy)
--- a/src/HOLCF/Tools/holcf_library.ML Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Tools/holcf_library.ML Sat Oct 16 16:39:06 2010 -0700
@@ -24,8 +24,10 @@
val mk_not = HOLogic.mk_not;
val mk_conj = HOLogic.mk_conj;
val mk_disj = HOLogic.mk_disj;
+val mk_imp = HOLogic.mk_imp;
fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t;
+fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t;
(*** Basic HOLCF concepts ***)
@@ -39,6 +41,9 @@
fun mk_defined t = mk_not (mk_undef t);
+fun mk_adm t =
+ Const (@{const_name adm}, fastype_of t --> boolT) $ t;
+
fun mk_compact t =
Const (@{const_name compact}, fastype_of t --> boolT) $ t;
--- a/src/HOLCF/Universal.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Universal.thy Sat Oct 16 16:39:06 2010 -0700
@@ -988,7 +988,7 @@
done
lemma lub_udom_approx [simp]: "(\<Squnion>i. udom_approx i) = ID"
-apply (rule ext_cfun, simp add: contlub_cfun_fun)
+apply (rule cfun_eqI, simp add: contlub_cfun_fun)
apply (rule below_antisym)
apply (rule is_lub_thelub)
apply (simp)
--- a/src/HOLCF/Up.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/Up.thy Sat Oct 16 16:39:06 2010 -0700
@@ -303,7 +303,7 @@
unfolding u_map_def by simp
lemma u_map_ID: "u_map\<cdot>ID = ID"
-unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun)
+unfolding u_map_def by (simp add: 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
--- a/src/HOLCF/UpperPD.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Sat Oct 16 16:39:06 2010 -0700
@@ -318,7 +318,7 @@
lemma upper_bind_basis_mono:
"t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
-unfolding expand_cfun_below
+unfolding cfun_below_iff
apply (erule upper_le_induct, safe)
apply (simp add: monofun_cfun)
apply (simp add: below_trans [OF upper_plus_below1])
@@ -366,7 +366,7 @@
by (induct xs rule: upper_pd_induct, simp_all)
lemma upper_map_ID: "upper_map\<cdot>ID = ID"
-by (simp add: expand_cfun_eq ID_def upper_map_ident)
+by (simp add: cfun_eq_iff ID_def upper_map_ident)
lemma upper_map_map:
"upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
@@ -478,7 +478,7 @@
next
show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
- by (simp add: cast_DEFL oo_def expand_cfun_eq upper_map_map)
+ by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
qed
end
--- a/src/HOLCF/ex/Fix2.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/ex/Fix2.thy Sat Oct 16 16:39:06 2010 -0700
@@ -16,7 +16,7 @@
lemma lemma1: "fix = gix"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
apply (rule antisym_less)
apply (rule fix_least)
apply (rule gix1_def)
--- a/src/HOLCF/ex/Focus_ex.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/ex/Focus_ex.thy Sat Oct 16 16:39:06 2010 -0700
@@ -211,7 +211,7 @@
apply (rule_tac x = "f" in exI)
apply (erule conjE)+
apply (erule conjI)
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
apply (erule_tac x = "x" in allE)
apply (erule exE)
apply (erule conjE)+
--- a/src/HOLCF/ex/Hoare.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/ex/Hoare.thy Sat Oct 16 16:39:06 2010 -0700
@@ -417,7 +417,7 @@
(* ------ the main proof q o p = q ------ *)
theorem hoare_main: "q oo p = q"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
apply (subst cfcomp2)
apply (rule hoare_lemma3 [THEN disjE])
apply (erule hoare_lemma23)
--- a/src/HOLCF/ex/Pattern_Match.thy Fri Oct 15 17:21:37 2010 +0100
+++ b/src/HOLCF/ex/Pattern_Match.thy Sat Oct 16 16:39:06 2010 -0700
@@ -359,6 +359,9 @@
ML {*
local open HOLCF_Library in
+infixr 6 ->>;
+infix 9 ` ;
+
val beta_rules =
@{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair};