# HG changeset patch
# User huffman
# Date 1199294943 -3600
# Node ID 71157f7e671e9e794027fba204984a346434514e
# Parent  b2874ee9081aa5df495bd0983fc4c4a2d16aae34
update instance proofs for sq_ord, po; new instance proofs for dcpo

diff -r b2874ee9081a -r 71157f7e671e src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Wed Jan 02 18:28:15 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Wed Jan 02 18:29:03 2008 +0100
@@ -15,15 +15,19 @@
 
 subsection {* Type @{typ unit} is a pcpo *}
 
-instance unit :: sq_ord ..
+instantiation unit :: sq_ord
+begin
 
-defs (overloaded)
+definition
   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
 
+instance ..
+end
+
 instance unit :: po
 by intro_classes simp_all
 
-instance unit :: cpo
+instance unit :: dcpo
 by intro_classes (simp add: is_lub_def is_ub_def)
 
 instance unit :: pcpo
@@ -42,29 +46,31 @@
 
 subsection {* Product type is a partial order *}
 
-instance "*" :: (sq_ord, sq_ord) sq_ord ..
+instantiation "*" :: (sq_ord, sq_ord) sq_ord
+begin
 
-defs (overloaded)
+definition
   less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
 
-lemma refl_less_cprod: "(p::'a * 'b) \<sqsubseteq> p"
-by (simp add: less_cprod_def)
+instance ..
+end
 
-lemma antisym_less_cprod: "\<lbrakk>(p1::'a * 'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p1\<rbrakk> \<Longrightarrow> p1 = p2"
-apply (unfold less_cprod_def)
-apply (rule injective_fst_snd)
-apply (fast intro: antisym_less)
-apply (fast intro: antisym_less)
-done
-
-lemma trans_less_cprod: "\<lbrakk>(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3"
-apply (unfold less_cprod_def)
-apply (fast intro: trans_less)
-done
-
-instance "*" :: (cpo, cpo) po
-by intro_classes
-  (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+
+instance "*" :: (po, po) po
+proof
+  fix x :: "'a \<times> 'b"
+  show "x \<sqsubseteq> x"
+    unfolding less_cprod_def by simp
+next
+  fix x y :: "'a \<times> 'b"
+  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
+    unfolding less_cprod_def Pair_fst_snd_eq
+    by (fast intro: antisym_less)
+next
+  fix x y z :: "'a \<times> 'b"
+  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+    unfolding less_cprod_def
+    by (fast intro: trans_less)
+qed
 
 
 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
@@ -91,36 +97,70 @@
 
 subsection {* Product type is a cpo *}
 
-lemma lub_cprod: 
-  "chain S \<Longrightarrow> range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
+lemma lub_cprod:
+  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
+  assumes S: "chain S"
+  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
 apply (rule is_lubI)
 apply (rule ub_rangeI)
 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
 apply (rule monofun_pair)
 apply (rule is_ub_thelub)
-apply (erule monofun_fst [THEN ch2ch_monofun])
+apply (rule ch2ch_monofun [OF monofun_fst S])
 apply (rule is_ub_thelub)
-apply (erule monofun_snd [THEN ch2ch_monofun])
+apply (rule ch2ch_monofun [OF monofun_snd S])
 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
 apply (rule monofun_pair)
 apply (rule is_lub_thelub)
-apply (erule monofun_fst [THEN ch2ch_monofun])
+apply (rule ch2ch_monofun [OF monofun_fst S])
 apply (erule monofun_fst [THEN ub2ub_monofun])
 apply (rule is_lub_thelub)
-apply (erule monofun_snd [THEN ch2ch_monofun])
+apply (rule ch2ch_monofun [OF monofun_snd S])
 apply (erule monofun_snd [THEN ub2ub_monofun])
 done
 
+lemma directed_lub_cprod:
+  fixes S :: "('a::dcpo \<times> 'b::dcpo) set"
+  assumes S: "directed S"
+  shows "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
+apply (rule is_lubI)
+apply (rule is_ubI)
+apply (rule_tac t=x in surjective_pairing [THEN ssubst])
+apply (rule monofun_pair)
+apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_fst S] imageI])
+apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_snd S] imageI])
+apply (rule_tac t=u in surjective_pairing [THEN ssubst])
+apply (rule monofun_pair)
+apply (rule is_lub_thelub')
+apply (rule dir2dir_monofun [OF monofun_fst S])
+apply (erule ub2ub_monofun' [OF monofun_fst])
+apply (rule is_lub_thelub')
+apply (rule dir2dir_monofun [OF monofun_snd S])
+apply (erule ub2ub_monofun' [OF monofun_snd])
+done
+
 lemma thelub_cprod:
-  "chain S \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
+  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
+    \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
 by (rule lub_cprod [THEN thelubI])
 
-lemma cpo_cprod:
-  "chain (S::nat \<Rightarrow> 'a::cpo * 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
-by (rule exI, erule lub_cprod)
+instance "*" :: (cpo, cpo) cpo
+proof
+  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
+  assume "chain S"
+  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
+    by (rule lub_cprod)
+  thus "\<exists>x. range S <<| x" ..
+qed
 
-instance "*" :: (cpo, cpo) cpo
-by intro_classes (rule cpo_cprod)
+instance "*" :: (dcpo, dcpo) dcpo
+proof
+  fix S :: "('a \<times> 'b) set"
+  assume "directed S"
+  hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
+    by (rule directed_lub_cprod)
+  thus "\<exists>x. S <<| x" ..
+qed
 
 subsection {* Product type is pointed *}