new instance proofs for classes finite_po, chfin, flat
authorhuffman
Fri Jan 04 00:01:02 2008 +0100 (2008-01-04)
changeset 25827c2adeb1bae5c
parent 25826 f9aa43287e42
child 25828 228c53fdb3b4
new instance proofs for classes finite_po, chfin, flat
src/HOLCF/Cfun.thy
src/HOLCF/Cprod.thy
src/HOLCF/Discrete.thy
src/HOLCF/Ffun.thy
src/HOLCF/Lift.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Thu Jan 03 23:59:51 2008 +0100
     1.2 +++ b/src/HOLCF/Cfun.thy	Fri Jan 04 00:01:02 2008 +0100
     1.3 @@ -103,6 +103,12 @@
     1.4  lemma UU_CFun: "\<bottom> \<in> CFun"
     1.5  by (simp add: CFun_def inst_fun_pcpo cont_const)
     1.6  
     1.7 +instance "->" :: (finite_po, finite_po) finite_po
     1.8 +by (rule typedef_finite_po [OF type_definition_CFun])
     1.9 +
    1.10 +instance "->" :: (finite_po, chfin) chfin
    1.11 +by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
    1.12 +
    1.13  instance "->" :: (cpo, pcpo) pcpo
    1.14  by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
    1.15  
     2.1 --- a/src/HOLCF/Cprod.thy	Thu Jan 03 23:59:51 2008 +0100
     2.2 +++ b/src/HOLCF/Cprod.thy	Fri Jan 04 00:01:02 2008 +0100
     2.3 @@ -161,6 +161,31 @@
     2.4    thus "\<exists>x. S <<| x" ..
     2.5  qed
     2.6  
     2.7 +instance "*" :: (finite_po, finite_po) finite_po ..
     2.8 +
     2.9 +instance "*" :: (chfin, chfin) chfin
    2.10 +proof (intro_classes, clarify)
    2.11 +  fix Y :: "nat \<Rightarrow> 'a \<times> 'b"
    2.12 +  assume Y: "chain Y"
    2.13 +  from Y have "chain (\<lambda>i. fst (Y i))"
    2.14 +    by (rule ch2ch_monofun [OF monofun_fst])
    2.15 +  hence "\<exists>m. max_in_chain m (\<lambda>i. fst (Y i))"
    2.16 +    by (rule chfin [rule_format])
    2.17 +  then obtain m where m: "max_in_chain m (\<lambda>i. fst (Y i))" ..
    2.18 +  from Y have "chain (\<lambda>i. snd (Y i))"
    2.19 +    by (rule ch2ch_monofun [OF monofun_snd])
    2.20 +  hence "\<exists>n. max_in_chain n (\<lambda>i. snd (Y i))"
    2.21 +    by (rule chfin [rule_format])
    2.22 +  then obtain n where n: "max_in_chain n (\<lambda>i. snd (Y i))" ..
    2.23 +  from m have m': "max_in_chain (max m n) (\<lambda>i. fst (Y i))"
    2.24 +    by (rule maxinch_mono [OF _ le_maxI1])
    2.25 +  from n have n': "max_in_chain (max m n) (\<lambda>i. snd (Y i))"
    2.26 +    by (rule maxinch_mono [OF _ le_maxI2])
    2.27 +  from m' n' have "max_in_chain (max m n) Y"
    2.28 +    unfolding max_in_chain_def Pair_fst_snd_eq by fast
    2.29 +  thus "\<exists>n. max_in_chain n Y" ..
    2.30 +qed
    2.31 +
    2.32  subsection {* Product type is pointed *}
    2.33  
    2.34  lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
     3.1 --- a/src/HOLCF/Discrete.thy	Thu Jan 03 23:59:51 2008 +0100
     3.2 +++ b/src/HOLCF/Discrete.thy	Fri Jan 04 00:01:02 2008 +0100
     3.3 @@ -72,6 +72,22 @@
     3.4    thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
     3.5  qed
     3.6  
     3.7 +instance discr :: (finite) finite_po
     3.8 +proof
     3.9 +  have "finite (Discr ` (UNIV :: 'a set))"
    3.10 +    by (rule finite_imageI [OF finite])
    3.11 +  also have "(Discr ` (UNIV :: 'a set)) = UNIV"
    3.12 +    by (auto, case_tac x, auto)
    3.13 +  finally show "finite (UNIV :: 'a discr set)" .
    3.14 +qed
    3.15 +
    3.16 +instance discr :: (type) chfin
    3.17 +apply (intro_classes, clarify)
    3.18 +apply (rule_tac x=0 in exI)
    3.19 +apply (unfold max_in_chain_def)
    3.20 +apply (clarify, erule discr_chain0 [symmetric])
    3.21 +done
    3.22 +
    3.23  subsection {* @{term undiscr} *}
    3.24  
    3.25  definition
    3.26 @@ -85,9 +101,9 @@
    3.27   "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
    3.28  by (fast dest: discr_chain0 elim: arg_cong)
    3.29  
    3.30 -lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
    3.31 -apply (unfold cont_def is_lub_def is_ub_def)
    3.32 -apply (simp add: discr_chain_f_range0)
    3.33 +lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
    3.34 +apply (rule chfindom_monofun2cont)
    3.35 +apply (rule monofunI, simp)
    3.36  done
    3.37  
    3.38  end
     4.1 --- a/src/HOLCF/Ffun.thy	Thu Jan 03 23:59:51 2008 +0100
     4.2 +++ b/src/HOLCF/Ffun.thy	Fri Jan 04 00:01:02 2008 +0100
     4.3 @@ -62,7 +62,6 @@
     4.4  lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
     4.5  by (simp add: chain_def less_fun_def)
     4.6  
     4.7 -
     4.8  text {* upper bounds of function chains yield upper bound in the po range *}
     4.9  
    4.10  lemma ub2ub_fun:
    4.11 @@ -125,6 +124,46 @@
    4.12  instance "fun" :: (type, dcpo) dcpo
    4.13  by intro_classes (rule dcpo_fun)
    4.14  
    4.15 +instance "fun" :: (finite, finite_po) finite_po ..
    4.16 +
    4.17 +text {* chain-finite function spaces *}
    4.18 +
    4.19 +lemma maxinch2maxinch_lambda:
    4.20 +  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
    4.21 +unfolding max_in_chain_def expand_fun_eq by simp
    4.22 +
    4.23 +lemma maxinch_mono:
    4.24 +  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
    4.25 +unfolding max_in_chain_def
    4.26 +proof (intro allI impI)
    4.27 +  fix k
    4.28 +  assume Y: "\<forall>n\<ge>i. Y i = Y n"
    4.29 +  assume ij: "i \<le> j"
    4.30 +  assume jk: "j \<le> k"
    4.31 +  from ij jk have ik: "i \<le> k" by simp
    4.32 +  from Y ij have Yij: "Y i = Y j" by simp
    4.33 +  from Y ik have Yik: "Y i = Y k" by simp
    4.34 +  from Yij Yik show "Y j = Y k" by auto
    4.35 +qed
    4.36 +
    4.37 +instance "fun" :: (finite, chfin) chfin
    4.38 +proof (intro_classes, clarify)
    4.39 +  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
    4.40 +  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
    4.41 +  assume "chain Y"
    4.42 +  hence "\<And>x. chain (\<lambda>i. Y i x)"
    4.43 +    by (rule ch2ch_fun)
    4.44 +  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
    4.45 +    by (rule chfin [rule_format])
    4.46 +  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
    4.47 +    by (rule LeastI_ex)
    4.48 +  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
    4.49 +    by (rule maxinch_mono [OF _ Max_ge], simp_all)
    4.50 +  hence "max_in_chain (Max (range ?n)) Y"
    4.51 +    by (rule maxinch2maxinch_lambda)
    4.52 +  thus "\<exists>n. max_in_chain n Y" ..
    4.53 +qed
    4.54 +
    4.55  subsection {* Full function space is pointed *}
    4.56  
    4.57  lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
     5.1 --- a/src/HOLCF/Lift.thy	Thu Jan 03 23:59:51 2008 +0100
     5.2 +++ b/src/HOLCF/Lift.thy	Fri Jan 04 00:01:02 2008 +0100
     5.3 @@ -14,6 +14,9 @@
     5.4  pcpodef 'a lift = "UNIV :: 'a discr u set"
     5.5  by simp
     5.6  
     5.7 +instance lift :: (finite) finite_po
     5.8 +by (rule typedef_finite_po [OF type_definition_lift])
     5.9 +
    5.10  lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
    5.11  
    5.12  definition
     6.1 --- a/src/HOLCF/Pcpodef.thy	Thu Jan 03 23:59:51 2008 +0100
     6.2 +++ b/src/HOLCF/Pcpodef.thy	Fri Jan 04 00:01:02 2008 +0100
     6.3 @@ -30,6 +30,41 @@
     6.4  done
     6.5  
     6.6  
     6.7 +subsection {* Proving a subtype is finite *}
     6.8 +
     6.9 +context type_definition
    6.10 +begin
    6.11 +
    6.12 +lemma Abs_image:
    6.13 +  shows "Abs ` A = UNIV"
    6.14 +proof
    6.15 +  show "Abs ` A <= UNIV" by simp
    6.16 +  show "UNIV <= Abs ` A"
    6.17 +  proof
    6.18 +    fix x
    6.19 +    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
    6.20 +    thus "x : Abs ` A" using Rep by (rule image_eqI)
    6.21 +  qed
    6.22 +qed
    6.23 +
    6.24 +lemma finite_UNIV: "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
    6.25 +proof -
    6.26 +  assume "finite A"
    6.27 +  hence "finite (Abs ` A)" by (rule finite_imageI)
    6.28 +  thus "finite (UNIV :: 'b set)" by (simp only: Abs_image)
    6.29 +qed
    6.30 +
    6.31 +end
    6.32 +
    6.33 +theorem typedef_finite_po:
    6.34 +  fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po"
    6.35 +  assumes type: "type_definition Rep Abs A"
    6.36 +  shows "OFCLASS('b, finite_po_class)"
    6.37 + apply (intro_classes)
    6.38 + apply (rule type_definition.finite_UNIV [OF type])
    6.39 + apply (rule finite)
    6.40 +done
    6.41 +
    6.42  subsection {* Proving a subtype is chain-finite *}
    6.43  
    6.44  lemma monofun_Rep:
     7.1 --- a/src/HOLCF/Sprod.thy	Thu Jan 03 23:59:51 2008 +0100
     7.2 +++ b/src/HOLCF/Sprod.thy	Fri Jan 04 00:01:02 2008 +0100
     7.3 @@ -19,6 +19,12 @@
     7.4          "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
     7.5  by simp
     7.6  
     7.7 +instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
     7.8 +by (rule typedef_finite_po [OF type_definition_Sprod])
     7.9 +
    7.10 +instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    7.11 +by (rule typedef_chfin [OF type_definition_Sprod less_Sprod_def])
    7.12 +
    7.13  syntax (xsymbols)
    7.14    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    7.15  syntax (HTML output)
    7.16 @@ -174,7 +180,6 @@
    7.17  apply (simp add: less_sprod)
    7.18  done
    7.19  
    7.20 -
    7.21  subsection {* Properties of @{term ssplit} *}
    7.22  
    7.23  lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
    7.24 @@ -186,4 +191,13 @@
    7.25  lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
    7.26  by (cases z, simp_all)
    7.27  
    7.28 +subsection {* Strict product preserves flatness *}
    7.29 +
    7.30 +instance "**" :: (flat, flat) flat
    7.31 +apply (intro_classes, clarify)
    7.32 +apply (rule_tac p=x in sprodE, simp)
    7.33 +apply (rule_tac p=y in sprodE, simp)
    7.34 +apply (simp add: flat_less_iff spair_less)
    7.35 +done
    7.36 +
    7.37  end
     8.1 --- a/src/HOLCF/Ssum.thy	Thu Jan 03 23:59:51 2008 +0100
     8.2 +++ b/src/HOLCF/Ssum.thy	Fri Jan 04 00:01:02 2008 +0100
     8.3 @@ -21,6 +21,12 @@
     8.4      (cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
     8.5  by simp
     8.6  
     8.7 +instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
     8.8 +by (rule typedef_finite_po [OF type_definition_Ssum])
     8.9 +
    8.10 +instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    8.11 +by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def])
    8.12 +
    8.13  syntax (xsymbols)
    8.14    "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
    8.15  syntax (HTML output)
    8.16 @@ -186,4 +192,18 @@
    8.17  lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
    8.18  by (cases z, simp_all)
    8.19  
    8.20 +subsection {* Strict sum preserves flatness *}
    8.21 +
    8.22 +lemma flat_less_iff:
    8.23 +  fixes x y :: "'a::flat"
    8.24 +  shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
    8.25 +by (safe dest!: ax_flat [rule_format])
    8.26 +
    8.27 +instance "++" :: (flat, flat) flat
    8.28 +apply (intro_classes, clarify)
    8.29 +apply (rule_tac p=x in ssumE, simp)
    8.30 +apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
    8.31 +apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
    8.32 +done
    8.33 +
    8.34  end
     9.1 --- a/src/HOLCF/Up.thy	Thu Jan 03 23:59:51 2008 +0100
     9.2 +++ b/src/HOLCF/Up.thy	Fri Jan 04 00:01:02 2008 +0100
     9.3 @@ -68,6 +68,13 @@
     9.4      by (auto split: u.split_asm intro: trans_less)
     9.5  qed
     9.6  
     9.7 +lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
     9.8 +by (auto, case_tac x, auto)
     9.9 +
    9.10 +instance u :: (finite_po) finite_po
    9.11 +by (intro_classes, simp add: u_UNIV)
    9.12 +
    9.13 +
    9.14  subsection {* Lifted cpo is a cpo *}
    9.15  
    9.16  lemma is_lub_Iup:
    9.17 @@ -310,12 +317,27 @@
    9.18  lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
    9.19  by (cases x, simp_all)
    9.20  
    9.21 +text {* lifting preserves chain-finiteness *}
    9.22 +
    9.23  lemma up_chain_cases:
    9.24    "chain Y \<Longrightarrow>
    9.25    (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
    9.26    (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
    9.27  by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
    9.28  
    9.29 +instance u :: (chfin) chfin
    9.30 +apply (intro_classes, clarify)
    9.31 +apply (drule up_chain_cases, safe)
    9.32 +apply (drule chfin [rule_format])
    9.33 +apply (erule exE, rename_tac n)
    9.34 +apply (rule_tac x="n + j" in exI)
    9.35 +apply (simp only: max_in_chain_def)
    9.36 +apply (clarify, rename_tac k)
    9.37 +apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
    9.38 +apply (rule_tac x="k - j" in exI, simp)
    9.39 +apply (simp add: max_in_chain_def)
    9.40 +done
    9.41 +
    9.42  lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
    9.43  apply (unfold compact_def)
    9.44  apply (rule admI)