# HG changeset patch
# User huffman
# Date 1199401262 -3600
# Node ID c2adeb1bae5cec25aa912eb92aa5f5fa26ce451f
# Parent  f9aa43287e42d3d9a5da8484825e01881ab74154
new instance proofs for classes finite_po, chfin, flat

diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -103,6 +103,12 @@
 lemma UU_CFun: "\<bottom> \<in> CFun"
 by (simp add: CFun_def inst_fun_pcpo cont_const)
 
+instance "->" :: (finite_po, finite_po) finite_po
+by (rule typedef_finite_po [OF type_definition_CFun])
+
+instance "->" :: (finite_po, chfin) chfin
+by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
+
 instance "->" :: (cpo, pcpo) pcpo
 by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
 
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -161,6 +161,31 @@
   thus "\<exists>x. S <<| x" ..
 qed
 
+instance "*" :: (finite_po, finite_po) finite_po ..
+
+instance "*" :: (chfin, chfin) chfin
+proof (intro_classes, clarify)
+  fix Y :: "nat \<Rightarrow> 'a \<times> 'b"
+  assume Y: "chain Y"
+  from Y have "chain (\<lambda>i. fst (Y i))"
+    by (rule ch2ch_monofun [OF monofun_fst])
+  hence "\<exists>m. max_in_chain m (\<lambda>i. fst (Y i))"
+    by (rule chfin [rule_format])
+  then obtain m where m: "max_in_chain m (\<lambda>i. fst (Y i))" ..
+  from Y have "chain (\<lambda>i. snd (Y i))"
+    by (rule ch2ch_monofun [OF monofun_snd])
+  hence "\<exists>n. max_in_chain n (\<lambda>i. snd (Y i))"
+    by (rule chfin [rule_format])
+  then obtain n where n: "max_in_chain n (\<lambda>i. snd (Y i))" ..
+  from m have m': "max_in_chain (max m n) (\<lambda>i. fst (Y i))"
+    by (rule maxinch_mono [OF _ le_maxI1])
+  from n have n': "max_in_chain (max m n) (\<lambda>i. snd (Y i))"
+    by (rule maxinch_mono [OF _ le_maxI2])
+  from m' n' have "max_in_chain (max m n) Y"
+    unfolding max_in_chain_def Pair_fst_snd_eq by fast
+  thus "\<exists>n. max_in_chain n Y" ..
+qed
+
 subsection {* Product type is pointed *}
 
 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Discrete.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -72,6 +72,22 @@
   thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
 qed
 
+instance discr :: (finite) finite_po
+proof
+  have "finite (Discr ` (UNIV :: 'a set))"
+    by (rule finite_imageI [OF finite])
+  also have "(Discr ` (UNIV :: 'a set)) = UNIV"
+    by (auto, case_tac x, auto)
+  finally show "finite (UNIV :: 'a discr set)" .
+qed
+
+instance discr :: (type) chfin
+apply (intro_classes, clarify)
+apply (rule_tac x=0 in exI)
+apply (unfold max_in_chain_def)
+apply (clarify, erule discr_chain0 [symmetric])
+done
+
 subsection {* @{term undiscr} *}
 
 definition
@@ -85,9 +101,9 @@
  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
 by (fast dest: discr_chain0 elim: arg_cong)
 
-lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
-apply (unfold cont_def is_lub_def is_ub_def)
-apply (simp add: discr_chain_f_range0)
+lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
+apply (rule chfindom_monofun2cont)
+apply (rule monofunI, simp)
 done
 
 end
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -62,7 +62,6 @@
 lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
 by (simp add: chain_def less_fun_def)
 
-
 text {* upper bounds of function chains yield upper bound in the po range *}
 
 lemma ub2ub_fun:
@@ -125,6 +124,46 @@
 instance "fun" :: (type, dcpo) dcpo
 by intro_classes (rule dcpo_fun)
 
+instance "fun" :: (finite, finite_po) finite_po ..
+
+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 expand_fun_eq 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 (intro_classes, clarify)
+  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 [rule_format])
+  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"
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Lift.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -14,6 +14,9 @@
 pcpodef 'a lift = "UNIV :: 'a discr u set"
 by simp
 
+instance lift :: (finite) finite_po
+by (rule typedef_finite_po [OF type_definition_lift])
+
 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
 
 definition
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -30,6 +30,41 @@
 done
 
 
+subsection {* Proving a subtype is finite *}
+
+context type_definition
+begin
+
+lemma Abs_image:
+  shows "Abs ` A = UNIV"
+proof
+  show "Abs ` A <= UNIV" by simp
+  show "UNIV <= Abs ` A"
+  proof
+    fix x
+    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
+    thus "x : Abs ` A" using Rep by (rule image_eqI)
+  qed
+qed
+
+lemma finite_UNIV: "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
+proof -
+  assume "finite A"
+  hence "finite (Abs ` A)" by (rule finite_imageI)
+  thus "finite (UNIV :: 'b set)" by (simp only: Abs_image)
+qed
+
+end
+
+theorem typedef_finite_po:
+  fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po"
+  assumes type: "type_definition Rep Abs A"
+  shows "OFCLASS('b, finite_po_class)"
+ apply (intro_classes)
+ apply (rule type_definition.finite_UNIV [OF type])
+ apply (rule finite)
+done
+
 subsection {* Proving a subtype is chain-finite *}
 
 lemma monofun_Rep:
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Sprod.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -19,6 +19,12 @@
         "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
 by simp
 
+instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+by (rule typedef_finite_po [OF type_definition_Sprod])
+
+instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+by (rule typedef_chfin [OF type_definition_Sprod less_Sprod_def])
+
 syntax (xsymbols)
   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 syntax (HTML output)
@@ -174,7 +180,6 @@
 apply (simp add: less_sprod)
 done
 
-
 subsection {* Properties of @{term ssplit} *}
 
 lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
@@ -186,4 +191,13 @@
 lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
 by (cases z, simp_all)
 
+subsection {* Strict product preserves flatness *}
+
+instance "**" :: (flat, flat) flat
+apply (intro_classes, clarify)
+apply (rule_tac p=x in sprodE, simp)
+apply (rule_tac p=y in sprodE, simp)
+apply (simp add: flat_less_iff spair_less)
+done
+
 end
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -21,6 +21,12 @@
     (cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
 by simp
 
+instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+by (rule typedef_finite_po [OF type_definition_Ssum])
+
+instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def])
+
 syntax (xsymbols)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 syntax (HTML output)
@@ -186,4 +192,18 @@
 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
 by (cases z, simp_all)
 
+subsection {* Strict sum preserves flatness *}
+
+lemma flat_less_iff:
+  fixes x y :: "'a::flat"
+  shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
+by (safe dest!: ax_flat [rule_format])
+
+instance "++" :: (flat, flat) flat
+apply (intro_classes, clarify)
+apply (rule_tac p=x in ssumE, simp)
+apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
+apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
+done
+
 end
diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Up.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -68,6 +68,13 @@
     by (auto split: u.split_asm intro: trans_less)
 qed
 
+lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
+by (auto, case_tac x, auto)
+
+instance u :: (finite_po) finite_po
+by (intro_classes, simp add: u_UNIV)
+
+
 subsection {* Lifted cpo is a cpo *}
 
 lemma is_lub_Iup:
@@ -310,12 +317,27 @@
 lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
 by (cases x, simp_all)
 
+text {* lifting preserves chain-finiteness *}
+
 lemma up_chain_cases:
   "chain Y \<Longrightarrow>
   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
   (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
 by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
 
+instance u :: (chfin) chfin
+apply (intro_classes, clarify)
+apply (drule up_chain_cases, safe)
+apply (drule chfin [rule_format])
+apply (erule exE, rename_tac n)
+apply (rule_tac x="n + j" in exI)
+apply (simp only: max_in_chain_def)
+apply (clarify, rename_tac k)
+apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
+apply (rule_tac x="k - j" in exI, simp)
+apply (simp add: max_in_chain_def)
+done
+
 lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
 apply (unfold compact_def)
 apply (rule admI)