# HG changeset patch # User huffman # Date 1117067007 -7200 # Node ID 81a4b4a245b0691ac100b1a5d38482cd2c934879 # Parent defa6fa5fd29e54e6bc4fcbfa31931e498568f2b cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff diff -r defa6fa5fd29 -r 81a4b4a245b0 src/HOLCF/Cprod.ML --- a/src/HOLCF/Cprod.ML Thu May 26 00:31:48 2005 +0200 +++ b/src/HOLCF/Cprod.ML Thu May 26 02:23:27 2005 +0200 @@ -5,10 +5,7 @@ val refl_less_cprod = thm "refl_less_cprod"; val antisym_less_cprod = thm "antisym_less_cprod"; val trans_less_cprod = thm "trans_less_cprod"; -val inst_cprod_po = thm "inst_cprod_po"; -val less_cprod4c = thm "less_cprod4c"; val minimal_cprod = thm "minimal_cprod"; -val UU_cprod_def = thm "UU_cprod_def"; val least_cprod = thm "least_cprod"; val monofun_pair1 = thm "monofun_pair1"; val monofun_pair2 = thm "monofun_pair2"; @@ -32,7 +29,6 @@ val contlub_snd = thm "contlub_snd"; val cont_fst = thm "cont_fst"; val cont_snd = thm "cont_snd"; -val beta_cfun_cprod = thm "beta_cfun_cprod"; val inject_cpair = thm "inject_cpair"; val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; val defined_cpair_rev = thm "defined_cpair_rev"; @@ -43,7 +39,6 @@ val cfst_strict = thm "cfst_strict"; val csnd_strict = thm "csnd_strict"; val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; -val less_cprod5c = thm "less_cprod5c"; val lub_cprod2 = thm "lub_cprod2"; val thelub_cprod2 = thm "thelub_cprod2"; val csplit2 = thm "csplit2"; diff -r defa6fa5fd29 -r 81a4b4a245b0 src/HOLCF/Cprod.thy --- 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<) \ \p1 p2. (fst p1 \ fst p2 \ snd p1 \ snd p2)" -lemma refl_less_cprod: "(p::'a*'b) << p" -apply (unfold less_cprod_def) -apply simp -done +lemma refl_less_cprod: "(p::'a * 'b) \ p" +by (simp add: less_cprod_def) -lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2" +lemma antisym_less_cprod: "\(p1::'a * 'b) \ p2; p2 \ p1\ \ 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: - "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3" +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 -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< x1 << x2 & y1 << y2" -apply (simp add: inst_cprod_po) -done 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 (\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 (\y. (x, y))" +by (simp add: monofun less_cprod_def) -lemma monofun_pair: "[|x1< (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)" -by (simp add: inst_cprod_po) +lemma monofun_pair: + "\x1 \ x2; y1 \ y2\ \ (x1, y1) \ (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 \ 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]) @@ -118,15 +103,12 @@ apply (erule monofun_snd [THEN ub2ub_monofun]) done -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 \ lub (range S) = (\i. fst (S i), \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 \ 'a::cpo * 'b::cpo) \ \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: 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 = "(\, \)" in exI) apply (rule minimal_cprod [THEN allI]) done @@ -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]) -done +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 (\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]) done -lemma contlub_pair2: "contlub(Pair(x))" +lemma contlub_pair2: "contlub (\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]) done -lemma cont_pair1: "cont(Pair)" +lemma cont_pair1: "cont (\x. (x, y))" apply (rule monocontlub2cont) apply (rule monofun_pair1) apply (rule contlub_pair1) done -lemma cont_pair2: "cont(Pair(x))" +lemma cont_pair2: "cont (\y. (x, y))" apply (rule monocontlub2cont) apply (rule monofun_pair2) apply (rule contlub_pair2) done -lemma contlub_fst: "contlub(fst)" +lemma contlub_fst: "contlub fst" apply (rule contlubI [rule_format]) apply (simp add: lub_cprod [THEN thelubI]) done -lemma contlub_snd: "contlub(snd)" +lemma contlub_snd: "contlub snd" apply (rule contlubI [rule_format]) apply (simp add: lub_cprod [THEN thelubI]) done -lemma cont_fst: "cont(fst)" +lemma cont_fst: "cont fst" apply (rule monocontlub2cont) apply (rule monofun_fst) apply (rule contlub_fst) done -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 *} consts - 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 \ 'b \ ('a * 'b)" (* continuous pairing *) + cfst :: "('a * 'b) \ 'a" + csnd :: "('a * 'b) \ 'b" + csplit :: "('a \ 'b \ 'c) \ ('a * 'b) \ 'c" syntax - "@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)") + "@ctuple" :: "['a, args] \ 'a * 'b" ("(1<_,/ _>)") translations - "" == ">" - "" == "cpair$x$y" + "" == ">" + "" == "cpair$x$y" defs -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 \ (\ x y. (x, y))" + cfst_def: "cfst \ (\ p. fst p)" + csnd_def: "csnd \ (\ p. snd p)" + csplit_def: "csplit \ (\ f p. f\(cfst\p)\(csnd\p))" subsection {* Syntax *} text {* syntax for @{text "LAM .e"} *} syntax - "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) + "_LAM" :: "[patterns, 'a \ 'b] \ ('a \ 'b)" ("(3LAM <_>./ _)" [0, 10] 10) translations - "LAM .b" == "csplit$(LAM x. LAM .b)" + "LAM . b" == "csplit$(LAM x. LAM . b)" "LAM . LAM zs. b" <= "csplit$(LAM x y zs. b)" "LAM .b" == "csplit$(LAM x y. b)" syntax (xsymbols) - "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\()<_>./ _)" [0, 10] 10) + "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\()<_>./ _)" [0, 10] 10) text {* syntax for Let *} constdefs - CLet :: "'a::cpo -> ('a -> 'b::cpo) -> 'b" - "CLet == LAM s f. f$s" + CLet :: "'a \ ('a \ 'b) \ 'b" + "CLet \ \ s f. f\s" nonterminals 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) -done +lemma cpair_eq_pair: " = (x, y)" +by (simp add: cpair_def cont_pair1 cont_pair2) + +lemma inject_cpair: " = \ a = aa \ b = ba" +by (simp add: cpair_eq_pair) -lemma inject_cpair: - " = ==> a=aa & b=ba" -by (simp add: cpair_def beta_cfun_cprod) +lemma cpair_eq [iff]: "( = ) = (a = a' \ b = b')" +by (simp add: cpair_eq_pair) -lemma cpair_eq [iff]: "( = ) = (a = a' & b = b')" -by (blast dest!: inject_cpair) +lemma cpair_less: "( \ ) = (a \ a' \ b \ b')" +by (simp add: cpair_eq_pair less_cprod_def) -lemma inst_cprod_pcpo2: "UU = " -by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo) +lemma inst_cprod_pcpo2: "\ = <\, \>" +by (simp add: cpair_eq_pair inst_cprod_pcpo) lemma defined_cpair_rev: - " = UU ==> a = UU & b = UU" -apply (drule inst_cprod_pcpo2 [THEN subst]) -apply (erule inject_cpair) -done + " = \ \ a = \ \ b = \" +by (simp add: inst_cprod_pcpo cpair_eq_pair) + +lemma Exh_Cprod2: "\a b. z = " +by (simp add: cpair_eq_pair) + +lemma cprodE: "\\x y. p = \ Q\ \ Q" +by (cut_tac Exh_Cprod2, auto) + +lemma cfst2 [simp]: "cfst\ = x" +by (simp add: cpair_eq_pair cfst_def cont_fst) -lemma Exh_Cprod2: "? a b. z=" -apply (unfold cpair_def) -apply (rule PairE) -apply (rule exI) -apply (rule exI) -apply (erule beta_cfun_cprod [THEN ssubst]) +lemma csnd2 [simp]: "csnd\ = y" +by (simp add: cpair_eq_pair csnd_def cont_snd) + +lemma cfst_strict [simp]: "cfst\\ = \" +by (simp add: inst_cprod_pcpo2) + +lemma csnd_strict [simp]: "csnd\\ = \" +by (simp add: inst_cprod_pcpo2) + +lemma surjective_pairing_Cprod2: "p, csnd\p> = p" +apply (unfold cfst_def csnd_def) +apply (simp add: cont_fst cont_snd cpair_eq_pair) done -lemma cprodE: -assumes prems: "!!x y. [| p = |] ==> Q" -shows "Q" -apply (rule PairE) -apply (rule prems) -apply (simp add: cpair_def beta_cfun_cprod) -done - -lemma cfst2 [simp]: "cfst$ = x" -by (simp add: cpair_def cfst_def beta_cfun_cprod cont_fst) - -lemma csnd2 [simp]: "csnd$ = 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: " = p" -apply (unfold cfst_def csnd_def cpair_def) -apply (simp add: cont_fst cont_snd beta_cfun_cprod) -done - -lemma less_cprod5c: - " << ==> xa< 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 \ range S <<| <\i. cfst\(S i), \i. csnd\(S i)>" +apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd) apply (erule lub_cprod) done -lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard] -(* -chain ?S1 ==> - lub (range ?S1) = - " -*) +lemma thelub_cprod2: + "chain S \ lub (range S) = <\i. cfst\(S i), \i. csnd\(S i)>" +by (rule lub_cprod2 [THEN thelubI]) -lemma csplit2 [simp]: "csplit$f$ = f$x$y" +lemma csplit2 [simp]: "csplit\f\ = f\x\y" by (simp add: csplit_def) -lemma csplit3: "csplit$cpair$z=z" +lemma csplit3: "csplit\cpair\z = z" by (simp add: csplit_def surjective_pairing_Cprod2) lemmas Cprod_rews = cfst2 csnd2 csplit2