--- 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)
--- 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
--- 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<<y"
-
-consts
- UU :: "'a::pcpo"
-
-syntax (xsymbols)
- UU :: "'a::pcpo" ("\<bottom>")
-
-defs
- UU_def: "UU == @x.!y. x<<y"
-
-(* further useful classes for HOLCF domains *)
-
-axclass chfin<cpo
-
-chfin: "!Y. chain Y-->(? n. max_in_chain n Y)"
-
-axclass flat<pcpo
-
-ax_flat: "! x y. x << y --> (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<i --> X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]
- ==> lub(range(X))<<lub(range(Y))"
+ ==> lub(range(X))<<lub(range(Y))"
apply (erule exE)
apply (rule is_lub_thelub)
apply assumption
apply (rule ub_rangeI)
-(* apply (intro strip) *)
apply (case_tac "j<i")
apply (rule_tac s = "Y (i) " and t = "X (i) " in subst)
apply (rule sym)
@@ -180,21 +105,19 @@
apply (rule not_less_eq [THEN subst])
apply assumption
apply (rule_tac s = "Y (Suc (j))" and t = "X (Suc (j))" in subst)
-apply (simp (no_asm_simp))
+apply (simp)
apply (erule is_ub_thelub)
done
lemma lub_equal2: "[|EX j. ALL i. j<i --> 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))<<lub(range(X))"
apply (rule is_lub_thelub)
apply assumption
apply (rule ub_rangeI)
-(* apply (intro strip) *)
apply (erule allE)
apply (erule exE)
apply (rule trans_less)
@@ -203,9 +126,35 @@
apply assumption
done
-(* ------------------------------------------------------------------------ *)
-(* usefull lemmas about UU *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Pointed cpos *}
+
+text {* The class pcpo of pointed cpos *}
+
+axclass pcpo < cpo
+ least: "? x.!y. x<<y"
+
+consts
+ UU :: "'a::pcpo"
+
+syntax (xsymbols)
+ UU :: "'a::pcpo" ("\<bottom>")
+
+defs
+ UU_def: "UU == @x.!y. x<<y"
+
+text {* 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
+
+lemmas minimal = UU_least [THEN spec, standard]
+
+declare minimal [iff]
+
+text {* useful lemmas about @{term UU} *}
lemma eq_UU_iff: "(x=UU)=(x<<UU)"
apply (rule iffI)
@@ -217,13 +166,10 @@
done
lemma UU_I: "x << UU ==> x = UU"
-apply (subst eq_UU_iff)
-apply assumption
-done
+by (subst eq_UU_iff)
lemma not_less2not_eq: "~(x::'a::po)<<y ==> ~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; ~x=UU |] ==> ~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<i-->~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<chfin
-apply (intro_classes)
-apply (rule flat_imp_chfin)
-done
-
end