# HG changeset patch # User huffman # Date 1110236449 -3600 # Node ID 14e3228f18cc8c7bc3d285de809c5f82d28ca65a # Parent f363e6e080e7482a96f13bfd0ecc172338e4b0b4 arranged for document generation, cleaned up some proofs diff -r f363e6e080e7 -r 14e3228f18cc src/HOLCF/Cont.thy --- a/src/HOLCF/Cont.thy Mon Mar 07 23:54:01 2005 +0100 +++ b/src/HOLCF/Cont.thy Tue Mar 08 00:00:49 2005 +0100 @@ -12,20 +12,17 @@ imports FunCpo begin -(* - - Now we change the default class! Form now on all untyped typevariables are +text {* + Now we change the default class! Form now on all untyped type variables are of default class po - -*) - +*} defaultsort po consts - monofun :: "('a => 'b) => bool" (* monotonicity *) - contlub :: "('a::cpo => 'b::cpo) => bool" (* first cont. def *) - cont :: "('a::cpo => 'b::cpo) => bool" (* secnd cont. def *) + monofun :: "('a => 'b) => bool" -- "monotonicity" + contlub :: "('a::cpo => 'b::cpo) => bool" -- "first cont. def" + cont :: "('a::cpo => 'b::cpo) => bool" -- "secnd cont. def" defs @@ -37,147 +34,100 @@ cont: "cont(f) == ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))" -(* ------------------------------------------------------------------------ *) -(* the main purpose of cont.thy is to show: *) -(* monofun(f) & contlub(f) <==> cont(f) *) -(* ------------------------------------------------------------------------ *) +text {* + the main purpose of cont.thy is to show: + @{prop "monofun(f) & contlub(f) == cont(f)"} +*} -(* Title: HOLCF/Cont.ML - ID: $Id$ - Author: Franz Regensburger - License: GPL (GNU GENERAL PUBLIC LICENSE) - -Results about continuity and monotonicity -*) - -(* ------------------------------------------------------------------------ *) -(* access to definition *) -(* ------------------------------------------------------------------------ *) +text {* access to definition *} lemma contlubI: "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==> contlub(f)" -apply (unfold contlub) -apply assumption -done +by (unfold contlub) lemma contlubE: " contlub(f)==> ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))" -apply (unfold contlub) -apply assumption -done - +by (unfold contlub) lemma contI: "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)" - -apply (unfold cont) -apply assumption -done +by (unfold cont) lemma contE: "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))" -apply (unfold cont) -apply assumption -done - +by (unfold cont) lemma monofunI: "! x y. x << y --> f(x) << f(y) ==> monofun(f)" -apply (unfold monofun) -apply assumption -done +by (unfold monofun) lemma monofunE: "monofun(f) ==> ! x y. x << y --> f(x) << f(y)" -apply (unfold monofun) -apply assumption -done +by (unfold monofun) -(* ------------------------------------------------------------------------ *) -(* the main purpose of cont.thy is to show: *) -(* monofun(f) & contlub(f) <==> cont(f) *) -(* ------------------------------------------------------------------------ *) - -(* ------------------------------------------------------------------------ *) -(* monotone functions map chains to chains *) -(* ------------------------------------------------------------------------ *) +text {* monotone functions map chains to chains *} lemma ch2ch_monofun: "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))" apply (rule chainI) -apply (erule monofunE [THEN spec, THEN spec, THEN mp]) +apply (erule monofunE [rule_format]) apply (erule chainE) done -(* ------------------------------------------------------------------------ *) -(* monotone functions map upper bound to upper bounds *) -(* ------------------------------------------------------------------------ *) +text {* monotone functions map upper bound to upper bounds *} lemma ub2ub_monofun: "[| monofun(f); range(Y) <| u|] ==> range(%i. f(Y(i))) <| f(u)" apply (rule ub_rangeI) -apply (erule monofunE [THEN spec, THEN spec, THEN mp]) +apply (erule monofunE [rule_format]) apply (erule ub_rangeD) done -(* ------------------------------------------------------------------------ *) -(* left to right: monofun(f) & contlub(f) ==> cont(f) *) -(* ------------------------------------------------------------------------ *) +text {* left to right: @{prop "monofun(f) & contlub(f) ==> cont(f)"} *} lemma monocontlub2cont: "[|monofun(f);contlub(f)|] ==> cont(f)" -apply (unfold cont) -apply (intro strip) +apply (rule contI [rule_format]) apply (rule thelubE) apply (erule ch2ch_monofun) apply assumption -apply (erule contlubE [THEN spec, THEN mp, symmetric]) +apply (erule contlubE [rule_format, symmetric]) apply assumption done -(* ------------------------------------------------------------------------ *) -(* first a lemma about binary chains *) -(* ------------------------------------------------------------------------ *) +text {* first a lemma about binary chains *} lemma binchain_cont: "[| cont(f); x << y |] ==> range(%i::nat. f(if i = 0 then x else y)) <<| f(y)" apply (rule subst) -prefer 2 apply (erule contE [THEN spec, THEN mp]) +prefer 2 apply (erule contE [rule_format]) apply (erule bin_chain) apply (rule_tac y = "y" in arg_cong) apply (erule lub_bin_chain [THEN thelubI]) done -(* ------------------------------------------------------------------------ *) -(* right to left: cont(f) ==> monofun(f) & contlub(f) *) -(* part1: cont(f) ==> monofun(f *) -(* ------------------------------------------------------------------------ *) +text {* right to left: @{prop "cont(f) ==> monofun(f) & contlub(f)"} *} +text {* part1: @{prop "cont(f) ==> monofun(f)"} *} lemma cont2mono: "cont(f) ==> monofun(f)" -apply (unfold monofun) -apply (intro strip) +apply (rule monofunI [rule_format]) apply (drule binchain_cont [THEN is_ub_lub]) apply (auto split add: split_if_asm) done -(* ------------------------------------------------------------------------ *) -(* right to left: cont(f) ==> monofun(f) & contlub(f) *) -(* part2: cont(f) ==> contlub(f) *) -(* ------------------------------------------------------------------------ *) +text {* right to left: @{prop "cont(f) ==> monofun(f) & contlub(f)"} *} +text {* part2: @{prop "cont(f) ==> contlub(f)"} *} lemma cont2contlub: "cont(f) ==> contlub(f)" -apply (unfold contlub) -apply (intro strip) +apply (rule contlubI [rule_format]) apply (rule thelubI [symmetric]) -apply (erule contE [THEN spec, THEN mp]) +apply (erule contE [rule_format]) apply assumption done -(* ------------------------------------------------------------------------ *) -(* monotone functions map finite chains to finite chains *) -(* ------------------------------------------------------------------------ *) +text {* monotone functions map finite chains to finite chains *} lemma monofun_finch2finch: "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))" @@ -185,31 +135,23 @@ apply (force elim!: ch2ch_monofun simp add: max_in_chain_def) done -(* ------------------------------------------------------------------------ *) -(* The same holds for continuous functions *) -(* ------------------------------------------------------------------------ *) +text {* The same holds for continuous functions *} lemmas cont_finch2finch = cont2mono [THEN monofun_finch2finch, standard] (* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *) - -(* ------------------------------------------------------------------------ *) -(* The following results are about a curried function that is monotone *) -(* in both arguments *) -(* ------------------------------------------------------------------------ *) +text {* + The following results are about a curried function that is monotone + in both arguments +*} lemma ch2ch_MF2L: "[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)" -apply (erule ch2ch_monofun [THEN ch2ch_fun]) -apply assumption -done - +by (erule ch2ch_monofun [THEN ch2ch_fun]) lemma ch2ch_MF2R: "[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))" -apply (erule ch2ch_monofun) -apply assumption -done +by (erule ch2ch_monofun) lemma ch2ch_MF2LR: "[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> @@ -218,11 +160,10 @@ apply (rule trans_less) apply (erule ch2ch_MF2L [THEN chainE]) apply assumption -apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec) +apply (rule monofunE [rule_format], erule spec) apply (erule chainE) done - lemma ch2ch_lubMF2R: "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); !f. monofun(MF2(f)::('b::po=>'c::cpo)); @@ -233,13 +174,12 @@ apply assumption apply (rule ch2ch_MF2R, erule spec) apply assumption -apply (intro strip) +apply (rule allI) apply (rule chainE) apply (erule ch2ch_MF2L) apply assumption done - lemma ch2ch_lubMF2L: "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); !f. monofun(MF2(f)::('b::po=>'c::cpo)); @@ -250,27 +190,25 @@ apply assumption apply (erule ch2ch_MF2L) apply assumption -apply (intro strip) +apply (rule allI) apply (rule chainE) apply (rule ch2ch_MF2R, erule spec) apply assumption done - lemma lub_MF2_mono: "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); !f. monofun(MF2(f)::('b::po=>'c::cpo)); chain(F)|] ==> monofun(% x. lub(range(% j. MF2 (F j) (x))))" -apply (rule monofunI) -apply (intro strip) +apply (rule monofunI [rule_format]) apply (rule lub_mono) apply (erule ch2ch_MF2L) apply assumption apply (erule ch2ch_MF2L) apply assumption -apply (intro strip) -apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec) +apply (rule allI) +apply (rule monofunE [rule_format], erule spec) apply assumption done @@ -289,7 +227,7 @@ apply assumption apply (erule ch2ch_lubMF2L) apply (assumption+) -apply (intro strip) +apply (rule allI) apply (rule is_ub_thelub) apply (erule ch2ch_MF2L) apply assumption @@ -301,13 +239,12 @@ apply assumption apply (erule ch2ch_lubMF2R) apply (assumption+) -apply (intro strip) +apply (rule allI) apply (rule is_ub_thelub) apply (rule ch2ch_MF2R, erule spec) apply assumption done - lemma diag_lubMF2_1: "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); !f. monofun(MF2(f)::('b::po=>'c::cpo)); @@ -342,7 +279,7 @@ apply (assumption+) apply (erule ch2ch_lubMF2L) apply (assumption+) -apply (intro strip) +apply (rule allI) apply (rule is_ub_thelub) apply (erule ch2ch_MF2L) apply assumption @@ -361,11 +298,10 @@ apply (assumption+) done - -(* ------------------------------------------------------------------------ *) -(* The following results are about a curried function that is continuous *) -(* in both arguments *) -(* ------------------------------------------------------------------------ *) +text {* + The following results are about a curried function that is continuous + in both arguments +*} lemma contlub_CF2: assumes prem1: "cont(CF2)" @@ -385,18 +321,15 @@ apply (auto simp add: cont2mono prems) done -(* ------------------------------------------------------------------------ *) -(* The following results are about application for functions in 'a=>'b *) -(* ------------------------------------------------------------------------ *) +text {* + The following results are about application for functions in @{typ "'a=>'b"} +*} lemma monofun_fun_fun: "f1 << f2 ==> f1(x) << f2(x)" -apply (erule less_fun [THEN iffD1, THEN spec]) -done +by (erule less_fun [THEN iffD1, THEN spec]) lemma monofun_fun_arg: "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)" -apply (erule monofunE [THEN spec, THEN spec, THEN mp]) -apply assumption -done +by (erule monofunE [THEN spec, THEN spec, THEN mp]) lemma monofun_fun: "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)" apply (rule trans_less) @@ -405,15 +338,13 @@ apply (erule monofun_fun_fun) done - -(* ------------------------------------------------------------------------ *) -(* The following results are about the propagation of monotonicity and *) -(* continuity *) -(* ------------------------------------------------------------------------ *) +text {* + The following results are about the propagation of monotonicity and + continuity +*} lemma mono2mono_MF1L: "[|monofun(c1)|] ==> monofun(%x. c1 x y)" -apply (rule monofunI) -apply (intro strip) +apply (rule monofunI [rule_format]) apply (erule monofun_fun_arg [THEN monofun_fun_fun]) apply assumption done @@ -421,8 +352,7 @@ lemma cont2cont_CF1L: "[|cont(c1)|] ==> cont(%x. c1 x y)" apply (rule monocontlub2cont) apply (erule cont2mono [THEN mono2mono_MF1L]) -apply (rule contlubI) -apply (intro strip) +apply (rule contlubI [rule_format]) apply (frule asm_rl) apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst]) apply assumption @@ -436,8 +366,7 @@ (********* Note "(%x.%y.c1 x y) = c1" ***********) lemma mono2mono_MF1L_rev: "!y. monofun(%x. c1 x y) ==> monofun(c1)" -apply (rule monofunI) -apply (intro strip) +apply (rule monofunI [rule_format]) apply (rule less_fun [THEN iffD2]) apply (blast dest: monofunE) done @@ -446,8 +375,7 @@ apply (rule monocontlub2cont) apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev]) apply (erule spec) -apply (rule contlubI) -apply (intro strip) +apply (rule contlubI [rule_format]) apply (rule ext) apply (subst thelub_fun) apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev, THEN ch2ch_monofun]) @@ -456,10 +384,10 @@ apply (blast dest: cont2contlub [THEN contlubE]) done -(* ------------------------------------------------------------------------ *) -(* What D.A.Schmidt calls continuity of abstraction *) -(* never used here *) -(* ------------------------------------------------------------------------ *) +text {* + What D.A.Schmidt calls continuity of abstraction + never used here +*} lemma contlub_abstraction: "[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==> @@ -476,21 +404,18 @@ lemma mono2mono_app: "[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==> monofun(%x.(ft(x))(tt(x)))" -apply (rule monofunI) -apply (intro strip) +apply (rule monofunI [rule_format]) apply (rule_tac ?f1.0 = "ft(x)" and ?f2.0 = "ft(y)" in monofun_fun) apply (erule spec) apply (erule spec) -apply (erule monofunE [THEN spec, THEN spec, THEN mp]) +apply (erule monofunE [rule_format]) apply assumption -apply (erule monofunE [THEN spec, THEN spec, THEN mp]) +apply (erule monofunE [rule_format]) apply assumption done - lemma cont2contlub_app: "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))" -apply (rule contlubI) -apply (intro strip) +apply (rule contlubI [rule_format]) apply (rule_tac f3 = "tt" in contlubE [THEN spec, THEN mp, THEN ssubst]) apply (erule cont2contlub) apply assumption @@ -500,70 +425,54 @@ apply assumption done - lemma cont2cont_app: "[|cont(ft); !x. cont(ft(x)); cont(tt)|] ==> cont(%x.(ft(x))(tt(x)))" apply (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) done - lemmas cont2cont_app2 = cont2cont_app[OF _ allI] (* [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *) (* cont (%x. ?ft x (?tt x)) *) -(* ------------------------------------------------------------------------ *) -(* The identity function is continuous *) -(* ------------------------------------------------------------------------ *) +text {* The identity function is continuous *} lemma cont_id: "cont(% x. x)" -apply (rule contI) -apply (intro strip) +apply (rule contI [rule_format]) apply (erule thelubE) apply (rule refl) done -(* ------------------------------------------------------------------------ *) -(* constant functions are continuous *) -(* ------------------------------------------------------------------------ *) +text {* constant functions are continuous *} lemma cont_const: "cont(%x. c)" -apply (unfold cont) -apply (intro strip) +apply (rule contI [rule_format]) apply (blast intro: is_lubI ub_rangeI dest: ub_rangeD) done +lemma cont2cont_app3: "[|cont(f); cont(t) |] ==> cont(%x. f(t(x)))" +by (best intro: cont2cont_app2 cont_const) -lemma cont2cont_app3: "[|cont(f); cont(t) |] ==> cont(%x. f(t(x)))" -apply (best intro: cont2cont_app2 cont_const) -done - -(* ------------------------------------------------------------------------ *) -(* A non-emptyness result for Cfun *) -(* ------------------------------------------------------------------------ *) +text {* A non-emptiness result for Cfun *} lemma CfunI: "?x:Collect cont" apply (rule CollectI) apply (rule cont_const) done -(* ------------------------------------------------------------------------ *) -(* some properties of flat *) -(* ------------------------------------------------------------------------ *) +text {* some properties of flat *} lemma flatdom2monofun: "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)" - -apply (unfold monofun) -apply (intro strip) -apply (drule ax_flat [THEN spec, THEN spec, THEN mp]) +apply (rule monofunI [rule_format]) +apply (drule ax_flat [rule_format]) apply auto done declare range_composition [simp del] + lemma chfindom_monofun2cont: "monofun f ==> cont(f::'a::chfin=>'b::pcpo)" apply (rule monocontlub2cont) apply assumption -apply (rule contlubI) -apply (intro strip) +apply (rule contlubI [rule_format]) apply (frule chfin2finch) apply (rule antisym_less) apply (clarsimp simp add: finite_chain_def maxinch_is_thelub) diff -r f363e6e080e7 -r 14e3228f18cc src/HOLCF/FunCpo.thy --- a/src/HOLCF/FunCpo.thy Mon Mar 07 23:54:01 2005 +0100 +++ b/src/HOLCF/FunCpo.thy Tue Mar 08 00:00:49 2005 +0100 @@ -16,17 +16,13 @@ imports Pcpo begin -(* to make << defineable: *) +subsection {* Type @{typ "'a => 'b"} is a partial order *} instance fun :: (type, sq_ord) sq_ord .. defs (overloaded) less_fun_def: "(op <<) == (%f1 f2.!x. f1 x << f2 x)" -(* ------------------------------------------------------------------------ *) -(* less_fun is a partial order on 'a => 'b *) -(* ------------------------------------------------------------------------ *) - lemma refl_less_fun: "(f::'a::type =>'b::po) << f" apply (unfold less_fun_def) apply (fast intro!: refl_less) @@ -35,40 +31,39 @@ lemma antisym_less_fun: "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2" apply (unfold less_fun_def) -(* apply (cut_tac prems) *) -apply (subst expand_fun_eq) +apply (rule ext) apply (fast intro!: antisym_less) done lemma trans_less_fun: "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3" apply (unfold less_fun_def) -(* apply (cut_tac prems) *) apply clarify apply (rule trans_less) -apply (erule allE) -apply assumption +apply (erule allE, assumption) apply (erule allE, assumption) done -(* default class is still type!*) +text {* default class is still type! *} instance fun :: (type, po) po -apply (intro_classes) -apply (rule refl_less_fun) -apply (rule antisym_less_fun, assumption+) -apply (rule trans_less_fun, assumption+) -done +by intro_classes + (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+ -(* for compatibility with old HOLCF-Version *) +text {* for compatibility with old HOLCF-Version *} lemma inst_fun_po: "(op <<)=(%f g.!x. f x << g x)" apply (fold less_fun_def) apply (rule refl) done -(* ------------------------------------------------------------------------ *) -(* Type 'a::type => 'b::pcpo is pointed *) -(* ------------------------------------------------------------------------ *) +text {* make the symbol @{text "<<"} accessible for type fun *} + +lemma less_fun: "(f1 << f2) = (! x. f1(x) << f2(x))" +apply (subst inst_fun_po) +apply (rule refl) +done + +subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *} lemma minimal_fun: "(%z. UU) << x" apply (simp (no_asm) add: inst_fun_po minimal) @@ -81,27 +76,16 @@ apply (rule minimal_fun [THEN allI]) done -(* ------------------------------------------------------------------------ *) -(* make the symbol << accessible for type fun *) -(* ------------------------------------------------------------------------ *) +subsection {* Type @{typ "'a::type => 'b::pcpo"} is chain complete *} -lemma less_fun: "(f1 << f2) = (! x. f1(x) << f2(x))" -apply (subst inst_fun_po) -apply (rule refl) -done - -(* ------------------------------------------------------------------------ *) -(* chains of functions yield chains in the po range *) -(* ------------------------------------------------------------------------ *) +text {* chains of functions yield chains in the po range *} lemma ch2ch_fun: "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)" apply (unfold chain_def) apply (simp add: less_fun) done -(* ------------------------------------------------------------------------ *) -(* upper bounds of function chains yield upper bound in the po range *) -(* ------------------------------------------------------------------------ *) +text {* upper bounds of function chains yield upper bound in the po range *} lemma ub2ub_fun: "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)" apply (rule ub_rangeI) @@ -110,9 +94,7 @@ apply auto done -(* ------------------------------------------------------------------------ *) -(* Type 'a::type => 'b::pcpo is chain complete *) -(* ------------------------------------------------------------------------ *) +text {* Type @{typ "'a::type => 'b::pcpo"} is chain complete *} lemma lub_fun: "chain(S::nat=>('a::type => 'b::cpo)) ==> range(S) <<| (% x. lub(range(% i. S(i)(x))))" @@ -122,7 +104,6 @@ apply (rule allI) apply (rule is_ub_thelub) apply (erule ch2ch_fun) -(* apply (intro strip) *) apply (subst less_fun) apply (rule allI) apply (rule is_lub_thelub) @@ -138,22 +119,17 @@ apply (erule lub_fun) done -(* default class is still type *) +text {* default class is still type *} instance fun :: (type, cpo) cpo -apply (intro_classes) -apply (erule cpo_fun) -done +by intro_classes (rule cpo_fun) -instance fun :: (type, pcpo)pcpo -apply (intro_classes) -apply (rule least_fun) -done +instance fun :: (type, pcpo) pcpo +by intro_classes (rule least_fun) -(* for compatibility with old HOLCF-Version *) +text {* for compatibility with old HOLCF-Version *} lemma inst_fun_pcpo: "UU = (%x. UU)" -apply (simp add: UU_def UU_fun_def) -done +by (simp add: UU_def UU_fun_def) end diff -r f363e6e080e7 -r 14e3228f18cc src/HOLCF/Pcpo.thy --- a/src/HOLCF/Pcpo.thy Mon Mar 07 23:54:01 2005 +0100 +++ b/src/HOLCF/Pcpo.thy Tue Mar 08 00:00:49 2005 +0100 @@ -12,80 +12,26 @@ imports Porder begin -(* The class cpo of chain complete partial orders *) -(* ********************************************** *) +subsection {* Complete partial orders *} + +text {* The class cpo of chain complete partial orders *} + axclass cpo < po - (* class axiom: *) + -- {* class axiom: *} cpo: "chain S ==> ? x. range S <<| x" -(* The class pcpo of pointed cpos *) -(* ****************************** *) -axclass pcpo < cpo - - least: "? x.!y. x<") - -defs - UU_def: "UU == @x.!y. x<(? n. max_in_chain n Y)" - -axclass flat (x = UU) | (x=y)" - -(* Title: HOLCF/Pcpo.ML - ID: $Id$ - Author: Franz Regensburger - License: GPL (GNU GENERAL PUBLIC LICENSE) +text {* in cpo's everthing equal to THE lub has lub properties for every chain *} -introduction of the classes cpo and pcpo -*) - - -(* ------------------------------------------------------------------------ *) -(* derive the old rule minimal *) -(* ------------------------------------------------------------------------ *) - -lemma UU_least: "ALL z. UU << z" -apply (unfold UU_def) -apply (rule some_eq_ex [THEN iffD2]) -apply (rule least) -done +lemma thelubE: "[| chain(S); lub(range(S)) = (l::'a::cpo) |] ==> range(S) <<| l" +by (blast dest: cpo intro: lubI) -lemmas minimal = UU_least [THEN spec, standard] - -declare minimal [iff] - -(* ------------------------------------------------------------------------ *) -(* in cpo's everthing equal to THE lub has lub properties for every chain *) -(* ------------------------------------------------------------------------ *) - -lemma thelubE: "[| chain(S); lub(range(S)) = (l::'a::cpo) |] ==> range(S) <<| l " -apply (blast dest: cpo intro: lubI) -done - -(* ------------------------------------------------------------------------ *) -(* Properties of the lub *) -(* ------------------------------------------------------------------------ *) - +text {* Properties of the lub *} lemma is_ub_thelub: "chain (S::nat => 'a::cpo) ==> S(x) << lub(range(S))" -apply (blast dest: cpo intro: lubI [THEN is_ub_lub]) -done +by (blast dest: cpo intro: lubI [THEN is_ub_lub]) lemma is_lub_thelub: "[| chain (S::nat => 'a::cpo); range(S) <| x |] ==> lub(range S) << x" -apply (blast dest: cpo intro: lubI [THEN is_lub_lub]) -done +by (blast dest: cpo intro: lubI [THEN is_lub_lub]) lemma lub_range_mono: "[| range X <= range Y; chain Y; chain (X::nat=>'a::cpo) |] ==> lub(range X) << lub(range Y)" apply (erule is_lub_thelub) @@ -122,10 +68,7 @@ apply (force elim!: is_ub_thelub) done - -(* ------------------------------------------------------------------------ *) -(* the << relation between two chains is preserved by their lubs *) -(* ------------------------------------------------------------------------ *) +text {* the @{text "<<"} relation between two chains is preserved by their lubs *} lemma lub_mono: "[|chain(C1::(nat=>'a::cpo));chain(C2); ALL k. C1(k) << C2(k)|] ==> lub(range(C1)) << lub(range(C2))" @@ -136,38 +79,20 @@ apply (erule is_ub_thelub) done -(* ------------------------------------------------------------------------ *) -(* the = relation between two chains is preserved by their lubs *) -(* ------------------------------------------------------------------------ *) +text {* the = relation between two chains is preserved by their lubs *} lemma lub_equal: "[| chain(C1::(nat=>'a::cpo));chain(C2);ALL k. C1(k)=C2(k)|] ==> lub(range(C1))=lub(range(C2))" -apply (rule antisym_less) -apply (rule lub_mono) -apply assumption -apply assumption -apply (intro strip) -apply (rule antisym_less_inverse [THEN conjunct1]) -apply (erule spec) -apply (rule lub_mono) -apply assumption -apply assumption -apply (intro strip) -apply (rule antisym_less_inverse [THEN conjunct2]) -apply (erule spec) -done +by (simp only: expand_fun_eq [symmetric]) -(* ------------------------------------------------------------------------ *) -(* more results about mono and = of lubs of chains *) -(* ------------------------------------------------------------------------ *) +text {* more results about mono and = of lubs of chains *} lemma lub_mono2: "[|EX j. ALL i. j X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|] - ==> lub(range(X))< lub(range(X))< X(i)=Y(i); chain(X::nat=>'a::cpo); chain(Y)|] ==> lub(range(X))=lub(range(Y))" -apply (blast intro: antisym_less lub_mono2 sym) -done +by (blast intro: antisym_less lub_mono2 sym) lemma lub_mono3: "[|chain(Y::nat=>'a::cpo);chain(X); ALL i. EX j. Y(i)<< X(j)|]==> lub(range(Y))<") + +defs + UU_def: "UU == @x.!y. x< x = UU" -apply (subst eq_UU_iff) -apply assumption -done +by (subst eq_UU_iff) lemma not_less2not_eq: "~(x::'a::po)< ~x=y" -apply auto -done +by auto lemma chain_UU_I: "[|chain(Y);lub(range(Y))=UU|] ==> ALL i. Y(i)=UU" apply (rule allI) @@ -233,74 +179,70 @@ apply (erule is_ub_thelub) done - lemma chain_UU_I_inverse: "ALL i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU" apply (rule lub_chain_maxelem) apply (erule spec) -apply (rule allI) -apply (rule antisym_less_inverse [THEN conjunct1]) -apply (erule spec) +apply simp done lemma chain_UU_I_inverse2: "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> EX i.~ Y(i)=UU" -apply (blast intro: chain_UU_I_inverse) -done +by (blast intro: chain_UU_I_inverse) lemma notUU_I: "[| x< ~y=UU" -apply (blast intro: UU_I) -done +by (blast intro: UU_I) lemma chain_mono2: "[|EX j. ~Y(j)=UU;chain(Y::nat=>'a::pcpo)|] ==> EX j. ALL i. j~Y(i)=UU" -apply (blast dest: notUU_I chain_mono) -done +by (blast dest: notUU_I chain_mono) + +subsection {* Chain-finite and flat cpos *} -(**************************************) -(* some properties for chfin and flat *) -(**************************************) +text {* further useful classes for HOLCF domains *} + +axclass chfin < cpo + chfin: "!Y. chain Y-->(? n. max_in_chain n Y)" -(* ------------------------------------------------------------------------ *) -(* flat types are chfin *) -(* ------------------------------------------------------------------------ *) +axclass flat < pcpo + ax_flat: "! x y. x << y --> (x = UU) | (x=y)" + +text {* some properties for chfin and flat *} -(*Used only in an "instance" declaration (Fun1.thy)*) +text {* flat types are chfin *} + lemma flat_imp_chfin: + -- {*Used only in an "instance" declaration (Fun1.thy)*} "ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)" apply (unfold max_in_chain_def) apply clarify apply (case_tac "ALL i. Y (i) =UU") apply (rule_tac x = "0" in exI) -apply (simp (no_asm_simp)) +apply simp apply simp apply (erule exE) apply (rule_tac x = "i" in exI) -apply (intro strip) +apply clarify apply (erule le_imp_less_or_eq [THEN disjE]) apply safe -apply (blast dest: chain_mono ax_flat [THEN spec, THEN spec, THEN mp]) +apply (blast dest: chain_mono ax_flat [rule_format]) done -(* flat subclass of chfin --> adm_flat not needed *) +instance flat < chfin +by intro_classes (rule flat_imp_chfin) + +text {* flat subclass of chfin @{text "-->"} @{text adm_flat} not needed *} lemma flat_eq: "(a::'a::flat) ~= UU ==> a << b = (a = b)" -apply (safe intro!: refl_less) -apply (drule ax_flat [THEN spec, THEN spec, THEN mp]) -apply (fast intro!: refl_less ax_flat [THEN spec, THEN spec, THEN mp]) -done +by (safe dest!: ax_flat [rule_format]) lemma chfin2finch: "chain (Y::nat=>'a::chfin) ==> finite_chain Y" -apply (force simp add: chfin finite_chain_def) -done +by (simp add: chfin finite_chain_def) -(* ------------------------------------------------------------------------ *) -(* lemmata for improved admissibility introdution rule *) -(* ------------------------------------------------------------------------ *) +text {* lemmata for improved admissibility introdution rule *} lemma infinite_chain_adm_lemma: "[|chain Y; ALL i. P (Y i); (!!Y. [| chain Y; ALL i. P (Y i); ~ finite_chain Y |] ==> P (lub(range Y))) |] ==> P (lub (range Y))" -(* apply (cut_tac prems) *) apply (case_tac "finite_chain Y") prefer 2 apply fast apply (unfold finite_chain_def) @@ -315,7 +257,6 @@ (!!Y. [| chain Y; ALL i. P (Y i); ALL i. EX j. i < j & Y i ~= Y j & Y i << Y j|] ==> P (lub (range Y))) |] ==> P (lub (range Y))" -(* apply (cut_tac prems) *) apply (erule infinite_chain_adm_lemma) apply assumption apply (erule thin_rl) @@ -324,9 +265,4 @@ apply (fast dest: le_imp_less_or_eq elim: chain_mono) done -instance flat