changeset 16081 81a4b4a245b0
parent 16070 4a83dd540b88
child 16093 cdcbf5a7f38d
--- a/src/HOLCF/Cprod.thy	Thu May 26 00:31:48 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Thu May 26 02:23:27 2005 +0200
@@ -30,76 +30,61 @@
 by intro_classes simp
-subsection {* Ordering on @{typ "'a * 'b"} *}
+subsection {* Type @{typ "'a * 'b"} is a partial order *}
 instance "*" :: (sq_ord, sq_ord) sq_ord ..
 defs (overloaded)
-  less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
-subsection {* Type @{typ "'a * 'b"} is a partial order *}
+  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) << p"
-apply (unfold less_cprod_def)
-apply simp
+lemma refl_less_cprod: "(p::'a * 'b) \<sqsubseteq> p"
+by (simp add: less_cprod_def)
-lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
+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)
-lemma trans_less_cprod: 
-        "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
+lemma trans_less_cprod: "\<lbrakk>(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3"
 apply (unfold less_cprod_def)
 apply (rule conjI)
 apply (fast intro: trans_less)
 apply (fast intro: trans_less)
-defaultsort pcpo
 instance "*" :: (cpo, cpo) po
 by intro_classes
   (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
-apply (fold less_cprod_def)
-apply (rule refl)
-lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
-apply (simp add: inst_cprod_po)
 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
-lemma monofun_pair1: "monofun Pair"
-by (simp add: monofun less_fun inst_cprod_po)
+lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
+by (simp add: monofun less_cprod_def)
-lemma monofun_pair2: "monofun(Pair x)"
-by (simp add: monofun inst_cprod_po)
+lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
+by (simp add: monofun less_cprod_def)
-lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
-by (simp add: inst_cprod_po)
+lemma monofun_pair:
+  "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
+by (simp add: less_cprod_def)
 text {* @{term fst} and @{term snd} are monotone *}
 lemma monofun_fst: "monofun fst"
-by (simp add: monofun inst_cprod_po)
+by (simp add: monofun less_cprod_def)
 lemma monofun_snd: "monofun snd"
-by (simp add: monofun inst_cprod_po)
+by (simp add: monofun less_cprod_def)
 subsection {* Type @{typ "'a * 'b"} is a cpo *}
 lemma lub_cprod: 
-"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
+"chain S \<Longrightarrow> 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])
@@ -118,15 +103,12 @@
 apply (erule monofun_snd [THEN ub2ub_monofun])
-lemmas thelub_cprod = lub_cprod [THEN thelubI, standard]
-"chain ?S1 ==>
- lub (range ?S1) =
- (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
+lemma thelub_cprod:
+  "chain S \<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=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
+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
@@ -134,13 +116,11 @@
 subsection {* Type @{typ "'a * 'b"} is pointed *}
-lemma minimal_cprod: "(UU,UU)<<p"
-by (simp add: inst_cprod_po)
+lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
+by (simp add: less_cprod_def)
-lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard]
-lemma least_cprod: "EX x::'a*'b. ALL y. x<<y"
-apply (rule_tac x = " (UU,UU) " in exI)
+lemma least_cprod: "EX x::'a::pcpo * 'b::pcpo. ALL y. x \<sqsubseteq> y"
+apply (rule_tac x = "(\<bottom>, \<bottom>)" in exI)
 apply (rule minimal_cprod [THEN allI])
@@ -149,58 +129,54 @@
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_cprod_pcpo: "UU = (UU,UU)"
-apply (simp add: UU_cprod_def[folded UU_def])
+by (rule minimal_cprod [THEN UU_I, symmetric])
 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-lemma contlub_pair1: "contlub(Pair)"
+lemma contlub_pair1: "contlub (\<lambda>x. (x,y))"
 apply (rule contlubI [rule_format])
-apply (rule ext)
-apply (subst lub_fun [THEN thelubI])
-apply (erule monofun_pair1 [THEN ch2ch_monofun])
 apply (subst thelub_cprod)
-apply (rule ch2ch_fun)
 apply (erule monofun_pair1 [THEN ch2ch_monofun])
 apply (simp add: lub_const [THEN thelubI])
-lemma contlub_pair2: "contlub(Pair(x))"
+lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
 apply (rule contlubI [rule_format])
 apply (subst thelub_cprod)
 apply (erule monofun_pair2 [THEN ch2ch_monofun])
 apply (simp add: lub_const [THEN thelubI])
-lemma cont_pair1: "cont(Pair)"
+lemma cont_pair1: "cont (\<lambda>x. (x, y))"
 apply (rule monocontlub2cont)
 apply (rule monofun_pair1)
 apply (rule contlub_pair1)
-lemma cont_pair2: "cont(Pair(x))"
+lemma cont_pair2: "cont (\<lambda>y. (x, y))"
 apply (rule monocontlub2cont)
 apply (rule monofun_pair2)
 apply (rule contlub_pair2)
-lemma contlub_fst: "contlub(fst)"
+lemma contlub_fst: "contlub fst"
 apply (rule contlubI [rule_format])
 apply (simp add: lub_cprod [THEN thelubI])
-lemma contlub_snd: "contlub(snd)"
+lemma contlub_snd: "contlub snd"
 apply (rule contlubI [rule_format])
 apply (simp add: lub_cprod [THEN thelubI])
-lemma cont_fst: "cont(fst)"
+lemma cont_fst: "cont fst"
 apply (rule monocontlub2cont)
 apply (rule monofun_fst)
 apply (rule contlub_fst)
-lemma cont_snd: "cont(snd)"
+lemma cont_snd: "cont snd"
 apply (rule monocontlub2cont)
 apply (rule monofun_snd)
 apply (rule contlub_snd)
@@ -209,44 +185,44 @@
 subsection {* Continuous versions of constants *}
-        cpair        :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
-        cfst         :: "('a::cpo*'b::cpo)->'a"
-        csnd         :: "('a::cpo*'b::cpo)->'b"
-        csplit       :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c"
+  cpair  :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *)
+  cfst   :: "('a * 'b) \<rightarrow> 'a"
+  csnd   :: "('a * 'b) \<rightarrow> 'b"
+  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c"
-        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
+  "@ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
-        "<x, y, z>"   == "<x, <y, z>>"
-        "<x, y>"      == "cpair$x$y"
+  "<x, y, z>" == "<x, <y, z>>"
+  "<x, y>"    == "cpair$x$y"
-cpair_def:       "cpair  == (LAM x y.(x,y))"
-cfst_def:        "cfst   == (LAM p. fst(p))"
-csnd_def:        "csnd   == (LAM p. snd(p))"      
-csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
+  cpair_def:  "cpair  \<equiv> (\<Lambda> x y. (x, y))"
+  cfst_def:   "cfst   \<equiv> (\<Lambda> p. fst p)"
+  csnd_def:   "csnd   \<equiv> (\<Lambda> p. snd p)"      
+  csplit_def: "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
 subsection {* Syntax *}
 text {* syntax for @{text "LAM <x,y,z>.e"} *}
-  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
+  "_LAM" :: "[patterns, 'a \<Rightarrow> 'b] \<Rightarrow> ('a \<rightarrow> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
-  "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
+  "LAM <x,y,zs>. b"       == "csplit$(LAM x. LAM <y,zs>. b)"
   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
 syntax (xsymbols)
-  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
+  "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
 text {* syntax for Let *}
-  CLet           :: "'a::cpo -> ('a -> 'b::cpo) -> 'b"
-  "CLet == LAM s f. f$s"
+  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
+  "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
   Cletbinds  Cletbind
@@ -266,87 +242,62 @@
 subsection {* Convert all lemmas to the continuous versions *}
-lemma beta_cfun_cprod: 
-        "(LAM x y.(x,y))$a$b = (a,b)"
-apply (subst beta_cfun)
-apply (simp add: cont_pair1 cont_pair2 cont2cont_CF1L)
-apply (subst beta_cfun)
-apply (rule cont_pair2)
-apply (rule refl)
+lemma cpair_eq_pair: "<x, y> = (x, y)"
+by (simp add: cpair_def cont_pair1 cont_pair2)
+lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba"
+by (simp add: cpair_eq_pair)
-lemma inject_cpair: 
-        "<a,b> = <aa,ba>  ==> a=aa & b=ba"
-by (simp add: cpair_def beta_cfun_cprod)
+lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
+by (simp add: cpair_eq_pair)
-lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' & b = b')"
-by (blast dest!: inject_cpair)
+lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
+by (simp add: cpair_eq_pair less_cprod_def)
-lemma inst_cprod_pcpo2: "UU = <UU,UU>"
-by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo)
+lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
+by (simp add: cpair_eq_pair inst_cprod_pcpo)
 lemma defined_cpair_rev: 
- "<a,b> = UU ==> a = UU & b = UU"
-apply (drule inst_cprod_pcpo2 [THEN subst])
-apply (erule inject_cpair)
+ "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
+by (simp add: inst_cprod_pcpo cpair_eq_pair)
+lemma Exh_Cprod2: "\<exists>a b. z = <a, b>"
+by (simp add: cpair_eq_pair)
+lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+by (cut_tac Exh_Cprod2, auto)
+lemma cfst2 [simp]: "cfst\<cdot><x, y> = x"
+by (simp add: cpair_eq_pair cfst_def cont_fst)
-lemma Exh_Cprod2: "? a b. z=<a,b>"
-apply (unfold cpair_def)
-apply (rule PairE)
-apply (rule exI)
-apply (rule exI)
-apply (erule beta_cfun_cprod [THEN ssubst])
+lemma csnd2 [simp]: "csnd\<cdot><x, y> = y"
+by (simp add: cpair_eq_pair csnd_def cont_snd)
+lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
+by (simp add: inst_cprod_pcpo2)
+lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
+by (simp add: inst_cprod_pcpo2)
+lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p"
+apply (unfold cfst_def csnd_def)
+apply (simp add: cont_fst cont_snd cpair_eq_pair)
-lemma cprodE:
-assumes prems: "!!x y. [| p = <x,y> |] ==> Q"
-shows "Q"
-apply (rule PairE)
-apply (rule prems)
-apply (simp add: cpair_def beta_cfun_cprod)
-lemma cfst2 [simp]: "cfst$<x,y> = x"
-by (simp add: cpair_def cfst_def beta_cfun_cprod cont_fst)
-lemma csnd2 [simp]: "csnd$<x,y> = y"
-by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd)
-lemma cfst_strict [simp]: "cfst$UU = UU"
-by (simp add: inst_cprod_pcpo2)
-lemma csnd_strict [simp]: "csnd$UU = UU"
-by (simp add: inst_cprod_pcpo2)
-lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p"
-apply (unfold cfst_def csnd_def cpair_def)
-apply (simp add: cont_fst cont_snd beta_cfun_cprod)
-lemma less_cprod5c: 
- "<xa,ya> << <x,y> ==> xa<<x & ya << y"
-by (simp add: cpair_def beta_cfun_cprod inst_cprod_po)
 lemma lub_cprod2: 
-"[|chain(S)|] ==> range(S) <<|  
-  <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"
-apply (simp add: cpair_def beta_cfun_cprod)
-apply (simp add: cfst_def csnd_def cont_fst cont_snd)
+  "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
+apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
 apply (erule lub_cprod)
-lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
-chain ?S1 ==>
- lub (range ?S1) =
- <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
+lemma thelub_cprod2:
+  "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
+by (rule lub_cprod2 [THEN thelubI])
-lemma csplit2 [simp]: "csplit$f$<x,y> = f$x$y"
+lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
 by (simp add: csplit_def)
-lemma csplit3: "csplit$cpair$z=z"
+lemma csplit3: "csplit\<cdot>cpair\<cdot>z = z"
 by (simp add: csplit_def surjective_pairing_Cprod2)
 lemmas Cprod_rews = cfst2 csnd2 csplit2