# HG changeset patch # User huffman # Date 1117833992 -7200 # Node ID 5d1b752cacc13fda1bbded369ef62e80f8a4bc69 # Parent 36ee7f6af79fef7c6b3ea0f2532f77bf6bbdd473 changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict diff -r 36ee7f6af79f -r 5d1b752cacc1 src/HOLCF/Cprod.ML --- a/src/HOLCF/Cprod.ML Fri Jun 03 23:23:55 2005 +0200 +++ b/src/HOLCF/Cprod.ML Fri Jun 03 23:26:32 2005 +0200 @@ -34,8 +34,8 @@ val defined_cpair_rev = thm "defined_cpair_rev"; val Exh_Cprod2 = thm "Exh_Cprod2"; val cprodE = thm "cprodE"; -val cfst2 = thm "cfst2"; -val csnd2 = thm "csnd2"; +val cfst_cpair = thm "cfst_cpair"; +val csnd_cpair = thm "csnd_cpair"; val cfst_strict = thm "cfst_strict"; val csnd_strict = thm "csnd_strict"; val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; @@ -43,4 +43,4 @@ val thelub_cprod2 = thm "thelub_cprod2"; val csplit2 = thm "csplit2"; val csplit3 = thm "csplit3"; -val Cprod_rews = [cfst2, csnd2, csplit2] +val Cprod_rews = [cfst_cpair, csnd_cpair, csplit2]; diff -r 36ee7f6af79f -r 5d1b752cacc1 src/HOLCF/Cprod.thy --- a/src/HOLCF/Cprod.thy Fri Jun 03 23:23:55 2005 +0200 +++ b/src/HOLCF/Cprod.thy Fri Jun 03 23:26:32 2005 +0200 @@ -49,8 +49,6 @@ lemma trans_less_cprod: "\(p1::'a*'b) \ p2; p2 \ p3\ \ p1 \ p3" apply (unfold less_cprod_def) -apply (rule conjI) -apply (fast intro: trans_less) apply (fast intro: trans_less) done @@ -64,10 +62,10 @@ text {* Pair @{text "(_,_)"} is monotone in both arguments *} lemma monofun_pair1: "monofun (\x. (x, y))" -by (simp add: monofun less_cprod_def) +by (simp add: monofun_def less_cprod_def) lemma monofun_pair2: "monofun (\y. (x, y))" -by (simp add: monofun less_cprod_def) +by (simp add: monofun_def less_cprod_def) lemma monofun_pair: "\x1 \ x2; y1 \ y2\ \ (x1, y1) \ (x2, y2)" @@ -76,15 +74,15 @@ text {* @{term fst} and @{term snd} are monotone *} lemma monofun_fst: "monofun fst" -by (simp add: monofun less_cprod_def) +by (simp add: monofun_def less_cprod_def) lemma monofun_snd: "monofun snd" -by (simp add: monofun less_cprod_def) +by (simp add: monofun_def less_cprod_def) subsection {* Type @{typ "'a * 'b"} is a cpo *} lemma lub_cprod: -"chain S \ range S <<| (\i. fst (S i), \i. snd (S i))" + "chain S \ range S <<| (\i. fst (S i), \i. snd (S i))" apply (rule is_lubI) apply (rule ub_rangeI) apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst]) @@ -135,14 +133,14 @@ subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} lemma contlub_pair1: "contlub (\x. (x,y))" -apply (rule contlubI [rule_format]) +apply (rule contlubI) apply (subst thelub_cprod) apply (erule monofun_pair1 [THEN ch2ch_monofun]) apply (simp add: thelub_const) done lemma contlub_pair2: "contlub (\y. (x, y))" -apply (rule contlubI [rule_format]) +apply (rule contlubI) apply (subst thelub_cprod) apply (erule monofun_pair2 [THEN ch2ch_monofun]) apply (simp add: thelub_const) @@ -161,13 +159,13 @@ done lemma contlub_fst: "contlub fst" -apply (rule contlubI [rule_format]) -apply (simp add: lub_cprod [THEN thelubI]) +apply (rule contlubI) +apply (simp add: thelub_cprod) done lemma contlub_snd: "contlub snd" -apply (rule contlubI [rule_format]) -apply (simp add: lub_cprod [THEN thelubI]) +apply (rule contlubI) +apply (simp add: thelub_cprod) done lemma cont_fst: "cont fst" @@ -254,6 +252,9 @@ lemma cpair_less: "( \ ) = (a \ a' \ b \ b')" by (simp add: cpair_eq_pair less_cprod_def) +lemma cpair_strict: "<\, \> = \" +by (simp add: cpair_eq_pair inst_cprod_pcpo) + lemma inst_cprod_pcpo2: "\ = <\, \>" by (simp add: cpair_eq_pair inst_cprod_pcpo) @@ -267,10 +268,10 @@ lemma cprodE: "\\x y. p = \ Q\ \ Q" by (cut_tac Exh_Cprod2, auto) -lemma cfst2 [simp]: "cfst\ = x" +lemma cfst_cpair [simp]: "cfst\ = x" by (simp add: cpair_eq_pair cfst_def cont_fst) -lemma csnd2 [simp]: "csnd\ = y" +lemma csnd_cpair [simp]: "csnd\ = y" by (simp add: cpair_eq_pair csnd_def cont_snd) lemma cfst_strict [simp]: "cfst\\ = \" @@ -300,6 +301,6 @@ lemma csplit3: "csplit\cpair\z = z" by (simp add: csplit_def surjective_pairing_Cprod2) -lemmas Cprod_rews = cfst2 csnd2 csplit2 +lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2 end