--- a/src/HOLCF/Cprod.thy Tue Mar 08 00:28:46 2005 +0100
+++ b/src/HOLCF/Cprod.thy Tue Mar 08 00:32:10 2005 +0100
@@ -14,15 +14,14 @@
defaultsort cpo
-instance "*"::(sq_ord,sq_ord)sq_ord ..
+subsection {* Ordering on @{typ "'a * 'b"} *}
+
+instance "*" :: (sq_ord, sq_ord) sq_ord ..
defs (overloaded)
-
less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
-(* ------------------------------------------------------------------------ *)
-(* less_cprod is a partial order on 'a * 'b *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Type @{typ "'a * 'b"} is a partial order *}
lemma refl_less_cprod: "(p::'a*'b) << p"
apply (unfold less_cprod_def)
@@ -44,18 +43,13 @@
apply (fast intro: trans_less)
done
-(* Class Instance *::(pcpo,pcpo)po *)
-
defaultsort pcpo
-instance "*"::(cpo,cpo)po
-apply (intro_classes)
-apply (rule refl_less_cprod)
-apply (rule antisym_less_cprod, assumption+)
-apply (rule trans_less_cprod, assumption+)
-done
+instance "*" :: (cpo, cpo) po
+by intro_classes
+ (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+
-(* for compatibility with old HOLCF-Version *)
+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)
@@ -65,70 +59,28 @@
apply (simp add: inst_cprod_po)
done
-(* ------------------------------------------------------------------------ *)
-(* type cprod is pointed *)
-(* ------------------------------------------------------------------------ *)
-
-lemma minimal_cprod: "(UU,UU)<<p"
-apply (simp (no_asm) add: inst_cprod_po)
-done
+subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-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)
-apply (rule minimal_cprod [THEN allI])
-done
-
-(* ------------------------------------------------------------------------ *)
-(* Pair <_,_> is monotone in both arguments *)
-(* ------------------------------------------------------------------------ *)
+text {* Pair @{text "(_,_)"} is monotone in both arguments *}
lemma monofun_pair1: "monofun Pair"
-
-apply (unfold monofun)
-apply (intro strip)
-apply (rule less_fun [THEN iffD2])
-apply (intro strip)
-apply (simp (no_asm_simp) add: inst_cprod_po)
-done
+by (simp add: monofun less_fun inst_cprod_po)
lemma monofun_pair2: "monofun(Pair x)"
-apply (unfold monofun)
-apply (simp (no_asm_simp) add: inst_cprod_po)
-done
+by (simp add: monofun inst_cprod_po)
lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
-apply (rule trans_less)
-apply (erule monofun_pair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
-apply (erule monofun_pair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
-done
+by (simp add: inst_cprod_po)
-(* ------------------------------------------------------------------------ *)
-(* fst and snd are monotone *)
-(* ------------------------------------------------------------------------ *)
+text {* @{term fst} and @{term snd} are monotone *}
lemma monofun_fst: "monofun fst"
-apply (unfold monofun)
-apply (intro strip)
-apply (rule_tac p = "x" in PairE)
-apply (rule_tac p = "y" in PairE)
-apply simp
-apply (erule less_cprod4c [THEN conjunct1])
-done
+by (simp add: monofun inst_cprod_po)
lemma monofun_snd: "monofun snd"
-apply (unfold monofun)
-apply (intro strip)
-apply (rule_tac p = "x" in PairE)
-apply (rule_tac p = "y" in PairE)
-apply simp
-apply (erule less_cprod4c [THEN conjunct2])
-done
+by (simp add: monofun inst_cprod_po)
-(* ------------------------------------------------------------------------ *)
-(* the type 'a * 'b is a cpo *)
-(* ------------------------------------------------------------------------ *)
+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))))"
@@ -159,17 +111,86 @@
*)
lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
-apply (rule exI)
-apply (erule lub_cprod)
+by (rule exI, erule lub_cprod)
+
+instance "*" :: (cpo,cpo)cpo
+by intro_classes (rule cpo_cprod)
+
+subsection {* Type @{typ "'a * 'b"} is pointed *}
+
+lemma minimal_cprod: "(UU,UU)<<p"
+by (simp add: inst_cprod_po)
+
+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)
+apply (rule minimal_cprod [THEN allI])
+done
+
+instance "*" :: (pcpo,pcpo)pcpo
+by intro_classes (rule least_cprod)
+
+text {* for compatibility with old HOLCF-Version *}
+lemma inst_cprod_pcpo: "UU = (UU,UU)"
+apply (simp add: UU_cprod_def[folded UU_def])
+done
+
+subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
+
+lemma contlub_pair1: "contlub(Pair)"
+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
-(* Class instance of * for class pcpo and cpo. *)
+lemma contlub_pair2: "contlub(Pair(x))"
+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)"
+apply (rule monocontlub2cont)
+apply (rule monofun_pair1)
+apply (rule contlub_pair1)
+done
+
+lemma cont_pair2: "cont(Pair(x))"
+apply (rule monocontlub2cont)
+apply (rule monofun_pair2)
+apply (rule contlub_pair2)
+done
-instance "*" :: (cpo,cpo)cpo
-by (intro_classes, rule cpo_cprod)
+lemma contlub_fst: "contlub(fst)"
+apply (rule contlubI [rule_format])
+apply (simp add: lub_cprod [THEN thelubI])
+done
+
+lemma contlub_snd: "contlub(snd)"
+apply (rule contlubI [rule_format])
+apply (simp add: lub_cprod [THEN thelubI])
+done
-instance "*" :: (pcpo,pcpo)pcpo
-by (intro_classes, rule least_cprod)
+lemma cont_fst: "cont(fst)"
+apply (rule monocontlub2cont)
+apply (rule monofun_fst)
+apply (rule contlub_fst)
+done
+
+lemma cont_snd: "cont(snd)"
+apply (rule monocontlub2cont)
+apply (rule monofun_snd)
+apply (rule contlub_snd)
+done
+
+subsection {* Continuous versions of constants *}
consts
cpair :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
@@ -235,128 +256,12 @@
syntax (xsymbols)
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
-(* for compatibility with old HOLCF-Version *)
-lemma inst_cprod_pcpo: "UU = (UU,UU)"
-apply (simp add: UU_cprod_def[folded UU_def])
-done
-
-(* ------------------------------------------------------------------------ *)
-(* continuity of (_,_) , fst, snd *)
-(* ------------------------------------------------------------------------ *)
-
-lemma Cprod3_lemma1:
-"chain(Y::(nat=>'a::cpo)) ==>
- (lub(range(Y)),(x::'b::cpo)) =
- (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
-apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
-apply (rule lub_equal)
-apply assumption
-apply (rule monofun_fst [THEN ch2ch_monofun])
-apply (rule ch2ch_fun)
-apply (rule monofun_pair1 [THEN ch2ch_monofun])
-apply assumption
-apply (rule allI)
-apply (simp (no_asm))
-apply (rule sym)
-apply (simp (no_asm))
-apply (rule lub_const [THEN thelubI])
-done
-
-lemma contlub_pair1: "contlub(Pair)"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule expand_fun_eq [THEN iffD2])
-apply (intro strip)
-apply (subst lub_fun [THEN thelubI])
-apply (erule monofun_pair1 [THEN ch2ch_monofun])
-apply (rule trans)
-apply (rule_tac [2] thelub_cprod [symmetric])
-apply (rule_tac [2] ch2ch_fun)
-apply (erule_tac [2] monofun_pair1 [THEN ch2ch_monofun])
-apply (erule Cprod3_lemma1)
-done
-
-lemma Cprod3_lemma2:
-"chain(Y::(nat=>'a::cpo)) ==>
- ((x::'b::cpo),lub(range Y)) =
- (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
-apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
-apply (rule sym)
-apply (simp (no_asm))
-apply (rule lub_const [THEN thelubI])
-apply (rule lub_equal)
-apply assumption
-apply (rule monofun_snd [THEN ch2ch_monofun])
-apply (rule monofun_pair2 [THEN ch2ch_monofun])
-apply assumption
-apply (rule allI)
-apply (simp (no_asm))
-done
-
-lemma contlub_pair2: "contlub(Pair(x))"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule trans)
-apply (rule_tac [2] thelub_cprod [symmetric])
-apply (erule_tac [2] monofun_pair2 [THEN ch2ch_monofun])
-apply (erule Cprod3_lemma2)
-done
-
-lemma cont_pair1: "cont(Pair)"
-apply (rule monocontlub2cont)
-apply (rule monofun_pair1)
-apply (rule contlub_pair1)
-done
-
-lemma cont_pair2: "cont(Pair(x))"
-apply (rule monocontlub2cont)
-apply (rule monofun_pair2)
-apply (rule contlub_pair2)
-done
-
-lemma contlub_fst: "contlub(fst)"
-apply (rule contlubI)
-apply (intro strip)
-apply (subst lub_cprod [THEN thelubI])
-apply assumption
-apply (simp (no_asm))
-done
-
-lemma contlub_snd: "contlub(snd)"
-apply (rule contlubI)
-apply (intro strip)
-apply (subst lub_cprod [THEN thelubI])
-apply assumption
-apply (simp (no_asm))
-done
-
-lemma cont_fst: "cont(fst)"
-apply (rule monocontlub2cont)
-apply (rule monofun_fst)
-apply (rule contlub_fst)
-done
-
-lemma cont_snd: "cont(snd)"
-apply (rule monocontlub2cont)
-apply (rule monofun_snd)
-apply (rule contlub_snd)
-done
-
-(*
- --------------------------------------------------------------------------
- more lemmas for Cprod3.thy
-
- --------------------------------------------------------------------------
-*)
-
-(* ------------------------------------------------------------------------ *)
-(* convert all lemmas to the continuous versions *)
-(* ------------------------------------------------------------------------ *)
+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 (no_asm) add: cont_pair1 cont_pair2 cont2cont_CF1L)
+apply (simp add: cont_pair1 cont_pair2 cont2cont_CF1L)
apply (subst beta_cfun)
apply (rule cont_pair2)
apply (rule refl)
@@ -364,21 +269,10 @@
lemma inject_cpair:
"<a,b> = <aa,ba> ==> a=aa & b=ba"
-apply (unfold cpair_def)
-apply (drule beta_cfun_cprod [THEN subst])
-apply (drule beta_cfun_cprod [THEN subst])
-apply (erule Pair_inject)
-apply fast
-done
+by (simp add: cpair_def beta_cfun_cprod)
lemma inst_cprod_pcpo2: "UU = <UU,UU>"
-apply (unfold cpair_def)
-apply (rule sym)
-apply (rule trans)
-apply (rule beta_cfun_cprod)
-apply (rule sym)
-apply (rule inst_cprod_pcpo)
-done
+by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo)
lemma defined_cpair_rev:
"<a,b> = UU ==> a = UU & b = UU"
@@ -386,8 +280,7 @@
apply (erule inject_cpair)
done
-lemma Exh_Cprod2:
- "? a b. z=<a,b>"
+lemma Exh_Cprod2: "? a b. z=<a,b>"
apply (unfold cpair_def)
apply (rule PairE)
apply (rule exI)
@@ -400,66 +293,36 @@
shows "Q"
apply (rule PairE)
apply (rule prems)
-apply (unfold cpair_def)
-apply (erule beta_cfun_cprod [THEN ssubst])
-done
-
-lemma cfst2:
- "cfst$<x,y> = x"
-apply (unfold cfst_def cpair_def)
-apply (subst beta_cfun_cprod)
-apply (subst beta_cfun)
-apply (rule cont_fst)
-apply (simp (no_asm))
+apply (simp add: cpair_def beta_cfun_cprod)
done
-lemma csnd2:
- "csnd$<x,y> = y"
-apply (unfold csnd_def cpair_def)
-apply (subst beta_cfun_cprod)
-apply (subst beta_cfun)
-apply (rule cont_snd)
-apply (simp (no_asm))
-done
+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: "cfst$UU = UU"
-apply (simp add: inst_cprod_pcpo2 cfst2)
-done
+by (simp add: inst_cprod_pcpo2)
lemma csnd_strict: "csnd$UU = UU"
-apply (simp add: inst_cprod_pcpo2 csnd2)
-done
+by (simp add: inst_cprod_pcpo2)
-lemma surjective_pairing_Cprod2: "<cfst$p , csnd$p> = p"
+lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p"
apply (unfold cfst_def csnd_def cpair_def)
-apply (subst beta_cfun_cprod)
-apply (simplesubst beta_cfun)
-apply (rule cont_snd)
-apply (subst beta_cfun)
-apply (rule cont_fst)
-apply (rule surjective_pairing [symmetric])
+apply (simp add: cont_fst cont_snd beta_cfun_cprod)
done
lemma less_cprod5c:
"<xa,ya> << <x,y> ==> xa<<x & ya << y"
-apply (unfold cfst_def csnd_def cpair_def)
-apply (rule less_cprod4c)
-apply (drule beta_cfun_cprod [THEN subst])
-apply (drule beta_cfun_cprod [THEN subst])
-apply assumption
-done
+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 (unfold cfst_def csnd_def cpair_def)
-apply (subst beta_cfun_cprod)
-apply (simplesubst beta_cfun [THEN ext])
-apply (rule cont_snd)
-apply (subst beta_cfun [THEN ext])
-apply (rule cont_fst)
-apply (rule lub_cprod)
-apply assumption
+apply (simp add: cpair_def beta_cfun_cprod)
+apply (simp add: cfst_def csnd_def cont_fst cont_snd)
+apply (erule lub_cprod)
done
lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
@@ -468,27 +331,12 @@
lub (range ?S1) =
<lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>"
*)
-lemma csplit2:
- "csplit$f$<x,y> = f$x$y"
-apply (unfold csplit_def)
-apply (subst beta_cfun)
-apply (simp (no_asm))
-apply (simp (no_asm) add: cfst2 csnd2)
-done
-lemma csplit3:
- "csplit$cpair$z=z"
-apply (unfold csplit_def)
-apply (subst beta_cfun)
-apply (simp (no_asm))
-apply (simp (no_asm) add: surjective_pairing_Cprod2)
-done
+lemma csplit2 [simp]: "csplit$f$<x,y> = f$x$y"
+by (simp add: csplit_def)
-(* ------------------------------------------------------------------------ *)
-(* install simplifier for Cprod *)
-(* ------------------------------------------------------------------------ *)
-
-declare cfst2 [simp] csnd2 [simp] csplit2 [simp]
+lemma csplit3: "csplit$cpair$z=z"
+by (simp add: csplit_def surjective_pairing_Cprod2)
lemmas Cprod_rews = cfst2 csnd2 csplit2
--- a/src/HOLCF/Ssum.thy Tue Mar 08 00:28:46 2005 +0100
+++ b/src/HOLCF/Ssum.thy Tue Mar 08 00:32:10 2005 +0100
@@ -12,6 +12,8 @@
imports Cfun
begin
+subsection {* Definition of strict sum type *}
+
constdefs
Sinl_Rep :: "['a,'a,'b,bool]=>bool"
"Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))"
@@ -32,7 +34,7 @@
Isinr :: "'b => ('a ++ 'b)"
Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
-defs (*defining the abstract constants*)
+defs -- {*defining the abstract constants*}
Isinl_def: "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
Isinr_def: "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
@@ -41,48 +43,34 @@
&(!a. a~=UU & s=Isinl(a) --> z=f$a)
&(!b. b~=UU & s=Isinr(b) --> z=g$b)"
-(* ------------------------------------------------------------------------ *)
-(* A non-emptyness result for Sssum *)
-(* ------------------------------------------------------------------------ *)
+text {* A non-emptiness result for Ssum *}
lemma SsumIl: "Sinl_Rep(a):Ssum"
-apply (unfold Ssum_def)
-apply blast
-done
+by (unfold Ssum_def) blast
lemma SsumIr: "Sinr_Rep(a):Ssum"
-apply (unfold Ssum_def)
-apply blast
-done
+by (unfold Ssum_def) blast
lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum"
apply (rule inj_on_inverseI)
apply (erule Abs_Ssum_inverse)
done
-(* ------------------------------------------------------------------------ *)
-(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *)
-(* ------------------------------------------------------------------------ *)
+text {* Strictness of @{term Sinr_Rep}, @{term Sinl_Rep} and @{term Isinl}, @{term Isinr} *}
lemma strict_SinlSinr_Rep:
"Sinl_Rep(UU) = Sinr_Rep(UU)"
apply (unfold Sinr_Rep_def Sinl_Rep_def)
-apply (rule ext)
-apply (rule ext)
-apply (rule ext)
+apply (rule ext)+
apply fast
done
-lemma strict_IsinlIsinr:
- "Isinl(UU) = Isinr(UU)"
+lemma strict_IsinlIsinr: "Isinl(UU) = Isinr(UU)"
apply (unfold Isinl_def Isinr_def)
apply (rule strict_SinlSinr_Rep [THEN arg_cong])
done
-
-(* ------------------------------------------------------------------------ *)
-(* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
-(* ------------------------------------------------------------------------ *)
+text {* distinctness of @{term Sinl_Rep}, @{term Sinr_Rep} and @{term Isinl}, @{term Isinr} *}
lemma noteq_SinlSinr_Rep:
"(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
@@ -90,7 +78,6 @@
apply (blast dest!: fun_cong)
done
-
lemma noteq_IsinlIsinr:
"Isinl(a)=Isinr(b) ==> a=UU & b=UU"
apply (unfold Isinl_def Isinr_def)
@@ -100,11 +87,7 @@
apply (rule SsumIr)
done
-
-
-(* ------------------------------------------------------------------------ *)
-(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
-(* ------------------------------------------------------------------------ *)
+text {* injectivity of @{term Sinl_Rep}, @{term Sinr_Rep} and @{term Isinl}, @{term Isinr} *}
lemma inject_Sinl_Rep1: "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
apply (unfold Sinl_Rep_def)
@@ -173,19 +156,17 @@
done
declare inject_Isinl [dest!] inject_Isinr [dest!]
+declare noteq_IsinlIsinr [dest!]
+declare noteq_IsinlIsinr [OF sym, dest!]
lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
-apply blast
-done
+by blast
lemma inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
-apply blast
-done
+by blast
-(* ------------------------------------------------------------------------ *)
-(* Exhaustion of the strict sum ++ *)
-(* choice of the bottom representation is arbitrary *)
-(* ------------------------------------------------------------------------ *)
+text {* Exhaustion of the strict sum @{typ "'a ++ 'b"} *}
+text {* choice of the bottom representation is arbitrary *}
lemma Exh_Ssum:
"z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"
@@ -227,9 +208,7 @@
apply (erule arg_cong)
done
-(* ------------------------------------------------------------------------ *)
-(* elimination rules for the strict sum ++ *)
-(* ------------------------------------------------------------------------ *)
+text {* elimination rules for the strict sum @{typ "'a ++ 'b"} *}
lemma IssumE:
"[|p=Isinl(UU) ==> Q ;
@@ -245,12 +224,7 @@
apply auto
done
-
-
-
-(* ------------------------------------------------------------------------ *)
-(* rewrites for Iwhen *)
-(* ------------------------------------------------------------------------ *)
+text {* rewrites for @{term Iwhen} *}
lemma Iwhen1:
"Iwhen f g (Isinl UU) = UU"
@@ -325,17 +299,15 @@
apply fast
done
-(* ------------------------------------------------------------------------ *)
-(* instantiate the simplifier *)
-(* ------------------------------------------------------------------------ *)
+text {* instantiate the simplifier *}
lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3
declare Ssum0_ss [simp]
-(* Partial ordering for the strict sum ++ *)
+subsection {* Ordering for type @{typ "'a ++ 'b"} *}
-instance "++"::(pcpo,pcpo)sq_ord ..
+instance "++"::(pcpo, pcpo) sq_ord ..
defs (overloaded)
less_ssum_def: "(op <<) == (%s1 s2.@z.
@@ -348,113 +320,23 @@
"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
apply (unfold less_ssum_def)
apply (rule some_equality)
-apply (drule_tac [2] conjunct1)
-apply (drule_tac [2] spec)
-apply (drule_tac [2] spec)
-apply (erule_tac [2] mp)
-prefer 2 apply fast
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule inject_Isinl)
-apply (drule inject_Isinl)
-apply simp
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr[OF sym])
-apply simp
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule inject_Isinl)
-apply (drule noteq_IsinlIsinr[OF sym])
-apply simp
-apply (rule eq_UU_iff[symmetric])
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr[OF sym])
-apply simp
+prefer 2 apply simp
+apply (safe elim!: UU_I)
done
-
lemma less_ssum1b:
"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
apply (unfold less_ssum_def)
apply (rule some_equality)
-apply (drule_tac [2] conjunct2)
-apply (drule_tac [2] conjunct1)
-apply (drule_tac [2] spec)
-apply (drule_tac [2] spec)
-apply (erule_tac [2] mp)
-prefer 2 apply fast
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr)
-apply (drule noteq_IsinlIsinr)
-apply simp
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule inject_Isinr)
-apply (drule inject_Isinr)
-apply simp
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr)
-apply (drule inject_Isinr)
-apply simp
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule inject_Isinr)
-apply (drule noteq_IsinlIsinr)
-apply simp
-apply (rule eq_UU_iff[symmetric])
+prefer 2 apply simp
+apply (safe elim!: UU_I)
done
-
lemma less_ssum1c:
"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
apply (unfold less_ssum_def)
apply (rule some_equality)
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule inject_Isinl)
-apply (drule noteq_IsinlIsinr)
-apply simp
-apply (rule eq_UU_iff)
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr[OF sym])
-apply (drule inject_Isinr)
-apply simp
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule inject_Isinl)
-apply (drule inject_Isinr)
-apply simp
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr[OF sym])
-apply (drule noteq_IsinlIsinr)
-apply simp
+prefer 2
apply (drule conjunct2)
apply (drule conjunct2)
apply (drule conjunct1)
@@ -462,53 +344,25 @@
apply (drule spec)
apply (erule mp)
apply fast
+apply (safe elim!: UU_I)
done
-
lemma less_ssum1d:
"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
apply (unfold less_ssum_def)
apply (rule some_equality)
-apply (drule_tac [2] conjunct2)
-apply (drule_tac [2] conjunct2)
-apply (drule_tac [2] conjunct2)
-apply (drule_tac [2] spec)
-apply (drule_tac [2] spec)
-apply (erule_tac [2] mp)
-prefer 2 apply fast
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr)
-apply (drule inject_Isinl)
-apply simp
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr[OF sym])
-apply (drule inject_Isinr)
-apply simp
-apply (rule eq_UU_iff)
-apply (rule conjI)
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule noteq_IsinlIsinr)
-apply (drule noteq_IsinlIsinr[OF sym])
-apply simp
-apply (intro strip)
-apply (erule conjE)
-apply simp
-apply (drule inject_Isinr)
-apply simp
+prefer 2
+apply (drule conjunct2)
+apply (drule conjunct2)
+apply (drule conjunct2)
+apply (drule spec)
+apply (drule spec)
+apply (erule mp)
+apply fast
+apply (safe elim!: UU_I)
done
-
-(* ------------------------------------------------------------------------ *)
-(* optimize lemmas about less_ssum *)
-(* ------------------------------------------------------------------------ *)
+text {* optimize lemmas about @{term less_ssum} *}
lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)"
apply (rule less_ssum1a)
@@ -534,19 +388,12 @@
apply (rule refl)
done
-
-(* ------------------------------------------------------------------------ *)
-(* less_ssum is a partial order on ++ *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Type @{typ "'a ++ 'b"} is a partial order *}
lemma refl_less_ssum: "(p::'a++'b) << p"
apply (rule_tac p = "p" in IssumE2)
-apply (erule ssubst)
-apply (rule less_ssum2a [THEN iffD2])
-apply (rule refl_less)
-apply (erule ssubst)
-apply (rule less_ssum2b [THEN iffD2])
-apply (rule refl_less)
+apply (simp add: less_ssum2a)
+apply (simp add: less_ssum2b)
done
lemma antisym_less_ssum: "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
@@ -625,16 +472,11 @@
apply (erule less_ssum2b [THEN iffD1])
done
-(* Class Instance ++::(pcpo,pcpo)po *)
+instance "++" :: (pcpo, pcpo) po
+by intro_classes
+ (assumption | rule refl_less_ssum antisym_less_ssum trans_less_ssum)+
-instance "++"::(pcpo,pcpo)po
-apply (intro_classes)
-apply (rule refl_less_ssum)
-apply (rule antisym_less_ssum, assumption+)
-apply (rule trans_less_ssum, assumption+)
-done
-
-(* for compatibility with old HOLCF-Version *)
+text {* for compatibility with old HOLCF-Version *}
lemma inst_ssum_po: "(op <<)=(%s1 s2.@z.
(! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
&(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
@@ -644,38 +486,16 @@
apply (rule refl)
done
-(* ------------------------------------------------------------------------ *)
-(* access to less_ssum in class po *)
-(* ------------------------------------------------------------------------ *)
-
-lemma less_ssum3a: "Isinl x << Isinl y = x << y"
-apply (simp (no_asm) add: less_ssum2a)
-done
-
-lemma less_ssum3b: "Isinr x << Isinr y = x << y"
-apply (simp (no_asm) add: less_ssum2b)
-done
-
-lemma less_ssum3c: "Isinl x << Isinr y = (x = UU)"
-apply (simp (no_asm) add: less_ssum2c)
-done
-
-lemma less_ssum3d: "Isinr x << Isinl y = (x = UU)"
-apply (simp (no_asm) add: less_ssum2d)
-done
-
-(* ------------------------------------------------------------------------ *)
-(* type ssum ++ is pointed *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Type @{typ "'a ++ 'b"} is pointed *}
lemma minimal_ssum: "Isinl UU << s"
apply (rule_tac p = "s" in IssumE2)
apply simp
-apply (rule less_ssum3a [THEN iffD2])
+apply (rule less_ssum2a [THEN iffD2])
apply (rule minimal)
apply simp
apply (subst strict_IsinlIsinr)
-apply (rule less_ssum3b [THEN iffD2])
+apply (rule less_ssum2b [THEN iffD2])
apply (rule minimal)
done
@@ -686,35 +506,22 @@
apply (rule minimal_ssum [THEN allI])
done
-(* ------------------------------------------------------------------------ *)
-(* Isinl, Isinr are monotone *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Monotonicity of @{term Isinl}, @{term Isinr}, @{term Iwhen} *}
+
+text {* @{term Isinl} and @{term Isinr} are monotone *}
lemma monofun_Isinl: "monofun(Isinl)"
-apply (unfold monofun)
-apply (intro strip)
-apply (erule less_ssum3a [THEN iffD2])
-done
+by (simp add: monofun less_ssum2a)
lemma monofun_Isinr: "monofun(Isinr)"
-apply (unfold monofun)
-apply (intro strip)
-apply (erule less_ssum3b [THEN iffD2])
-done
+by (simp add: monofun less_ssum2b)
-
-(* ------------------------------------------------------------------------ *)
-(* Iwhen is monotone in all arguments *)
-(* ------------------------------------------------------------------------ *)
-
+text {* @{term Iwhen} is monotone in all arguments *}
lemma monofun_Iwhen1: "monofun(Iwhen)"
-apply (unfold monofun)
-apply (intro strip)
-apply (rule less_fun [THEN iffD2])
-apply (intro strip)
-apply (rule less_fun [THEN iffD2])
-apply (intro strip)
+apply (rule monofunI [rule_format])
+apply (rule less_fun [THEN iffD2, rule_format])
+apply (rule less_fun [THEN iffD2, rule_format])
apply (rule_tac p = "xb" in IssumE)
apply simp
apply simp
@@ -723,10 +530,8 @@
done
lemma monofun_Iwhen2: "monofun(Iwhen(f))"
-apply (unfold monofun)
-apply (intro strip)
-apply (rule less_fun [THEN iffD2])
-apply (intro strip)
+apply (rule monofunI [rule_format])
+apply (rule less_fun [THEN iffD2, rule_format])
apply (rule_tac p = "xa" in IssumE)
apply simp
apply simp
@@ -735,8 +540,7 @@
done
lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))"
-apply (unfold monofun)
-apply (intro strip)
+apply (rule monofunI [rule_format])
apply (rule_tac p = "x" in IssumE)
apply simp
apply (rule_tac p = "y" in IssumE)
@@ -744,32 +548,28 @@
apply (rule_tac P = "xa=UU" in notE)
apply assumption
apply (rule UU_I)
-apply (rule less_ssum3a [THEN iffD1])
+apply (rule less_ssum2a [THEN iffD1])
apply assumption
apply simp
apply (rule monofun_cfun_arg)
-apply (erule less_ssum3a [THEN iffD1])
+apply (erule less_ssum2a [THEN iffD1])
apply (simp del: Iwhen2)
apply (rule_tac s = "UU" and t = "xa" in subst)
-apply (erule less_ssum3c [THEN iffD1, symmetric])
+apply (erule less_ssum2c [THEN iffD1, symmetric])
apply simp
apply (rule_tac p = "y" in IssumE)
apply simp
-apply (simp only: less_ssum3d)
-apply (simp only: less_ssum3d)
+apply (simp only: less_ssum2d)
+apply (simp only: less_ssum2d)
apply simp
apply (rule monofun_cfun_arg)
-apply (erule less_ssum3b [THEN iffD1])
+apply (erule less_ssum2b [THEN iffD1])
done
-
-(* ------------------------------------------------------------------------ *)
-(* some kind of exhaustion rules for chains in 'a ++ 'b *)
-(* ------------------------------------------------------------------------ *)
+text {* some kind of exhaustion rules for chains in @{typ "'a ++ 'b"} *}
lemma ssum_lemma1: "[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))"
-apply fast
-done
+by fast
lemma ssum_lemma2: "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|]
==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)"
@@ -782,7 +582,6 @@
apply fast
done
-
lemma ssum_lemma3: "[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|]
==> (!i.? y. Y(i)=Isinr(y))"
apply (erule exE)
@@ -799,13 +598,13 @@
prefer 2 apply simp
apply (rule exI, rule refl)
apply (erule_tac P = "x=UU" in notE)
-apply (rule less_ssum3d [THEN iffD1])
+apply (rule less_ssum2d [THEN iffD1])
apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
apply (erule chain_mono)
apply assumption
apply (erule_tac P = "xa=UU" in notE)
-apply (rule less_ssum3c [THEN iffD1])
+apply (rule less_ssum2c [THEN iffD1])
apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
apply (erule chain_mono)
@@ -821,10 +620,7 @@
apply (erule ssum_lemma1)
done
-
-(* ------------------------------------------------------------------------ *)
-(* restricted surjectivity of Isinl *)
-(* ------------------------------------------------------------------------ *)
+text {* restricted surjectivity of @{term Isinl} *}
lemma ssum_lemma5: "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"
apply simp
@@ -833,9 +629,7 @@
apply simp
done
-(* ------------------------------------------------------------------------ *)
-(* restricted surjectivity of Isinr *)
-(* ------------------------------------------------------------------------ *)
+text {* restricted surjectivity of @{term Isinr} *}
lemma ssum_lemma6: "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"
apply simp
@@ -844,21 +638,19 @@
apply simp
done
-(* ------------------------------------------------------------------------ *)
-(* technical lemmas *)
-(* ------------------------------------------------------------------------ *)
+text {* technical lemmas *}
lemma ssum_lemma7: "[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU"
apply (rule_tac p = "z" in IssumE)
apply simp
apply (erule notE)
apply (rule antisym_less)
-apply (erule less_ssum3a [THEN iffD1])
+apply (erule less_ssum2a [THEN iffD1])
apply (rule minimal)
apply fast
apply simp
apply (rule notE)
-apply (erule_tac [2] less_ssum3c [THEN iffD1])
+apply (erule_tac [2] less_ssum2c [THEN iffD1])
apply assumption
done
@@ -866,17 +658,15 @@
apply (rule_tac p = "z" in IssumE)
apply simp
apply (erule notE)
-apply (erule less_ssum3d [THEN iffD1])
+apply (erule less_ssum2d [THEN iffD1])
apply simp
apply (rule notE)
-apply (erule_tac [2] less_ssum3d [THEN iffD1])
+apply (erule_tac [2] less_ssum2d [THEN iffD1])
apply assumption
apply fast
done
-(* ------------------------------------------------------------------------ *)
-(* the type 'a ++ 'b is a cpo in three steps *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Type @{typ "'a ++ 'b"} is a cpo in three steps *}
lemma lub_ssum1a: "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>
range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
@@ -897,21 +687,20 @@
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
apply simp
-apply (rule less_ssum3c [THEN iffD2])
+apply (rule less_ssum2c [THEN iffD2])
apply (rule chain_UU_I_inverse)
apply (rule allI)
apply (rule_tac p = "Y (i) " in IssumE)
apply simp
apply simp
apply (erule notE)
-apply (rule less_ssum3c [THEN iffD1])
+apply (rule less_ssum2c [THEN iffD1])
apply (rule_tac t = "Isinl (x) " in subst)
apply assumption
apply (erule ub_rangeD)
apply simp
done
-
lemma lub_ssum1b: "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>
range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
apply (rule is_lubI)
@@ -925,14 +714,14 @@
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
apply (rule_tac p = "u" in IssumE2)
apply simp
-apply (rule less_ssum3d [THEN iffD2])
+apply (rule less_ssum2d [THEN iffD2])
apply (rule chain_UU_I_inverse)
apply (rule allI)
apply (rule_tac p = "Y (i) " in IssumE)
apply simp
apply simp
apply (erule notE)
-apply (rule less_ssum3d [THEN iffD1])
+apply (rule less_ssum2d [THEN iffD1])
apply (rule_tac t = "Isinr (y) " in subst)
apply assumption
apply (erule ub_rangeD)
@@ -944,7 +733,6 @@
apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
done
-
lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard]
(*
[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
@@ -970,14 +758,21 @@
apply assumption
done
-(* Class instance of ++ for class pcpo *)
+instance "++" :: (pcpo, pcpo) cpo
+by intro_classes (rule cpo_ssum)
+
+instance "++" :: (pcpo, pcpo) pcpo
+by intro_classes (rule least_ssum)
-instance "++" :: (pcpo,pcpo)pcpo
-apply (intro_classes)
-apply (erule cpo_ssum)
-apply (rule least_ssum)
+text {* for compatibility with old HOLCF-Version *}
+lemma inst_ssum_pcpo: "UU = Isinl UU"
+apply (simp add: UU_def UU_ssum_def)
done
+declare inst_ssum_pcpo [symmetric, simp]
+
+subsection {* Continuous versions of constants *}
+
consts
sinl :: "'a -> ('a++'b)"
sinr :: "'b -> ('a++'b)"
@@ -992,16 +787,7 @@
translations
"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
-(* for compatibility with old HOLCF-Version *)
-lemma inst_ssum_pcpo: "UU = Isinl UU"
-apply (simp add: UU_def UU_ssum_def)
-done
-
-declare inst_ssum_pcpo [symmetric, simp]
-
-(* ------------------------------------------------------------------------ *)
-(* continuity for Isinl and Isinr *)
-(* ------------------------------------------------------------------------ *)
+text {* continuity for @{term Isinl} and @{term Isinr} *}
lemma contlub_Isinl: "contlub(Isinl)"
apply (rule contlubI)
@@ -1063,24 +849,19 @@
apply simp
done
-lemma cont_Isinl: "cont(Isinl)"
+lemma cont_Isinl [iff]: "cont(Isinl)"
apply (rule monocontlub2cont)
apply (rule monofun_Isinl)
apply (rule contlub_Isinl)
done
-lemma cont_Isinr: "cont(Isinr)"
+lemma cont_Isinr [iff]: "cont(Isinr)"
apply (rule monocontlub2cont)
apply (rule monofun_Isinr)
apply (rule contlub_Isinr)
done
-declare cont_Isinl [iff] cont_Isinr [iff]
-
-
-(* ------------------------------------------------------------------------ *)
-(* continuity for Iwhen in the firts two arguments *)
-(* ------------------------------------------------------------------------ *)
+text {* continuity for @{term Iwhen} in the first two arguments *}
lemma contlub_Iwhen1: "contlub(Iwhen)"
apply (rule contlubI)
@@ -1122,13 +903,9 @@
apply (erule contlub_cfun_fun)
done
-(* ------------------------------------------------------------------------ *)
-(* continuity for Iwhen in its third argument *)
-(* ------------------------------------------------------------------------ *)
+text {* continuity for @{term Iwhen} in its third argument *}
-(* ------------------------------------------------------------------------ *)
-(* first 5 ugly lemmas *)
-(* ------------------------------------------------------------------------ *)
+text {* first 5 ugly lemmas *}
lemma ssum_lemma9: "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
apply (intro strip)
@@ -1137,13 +914,12 @@
apply (erule exI)
apply (rule_tac P = "y=UU" in notE)
apply assumption
-apply (rule less_ssum3d [THEN iffD1])
+apply (rule less_ssum2d [THEN iffD1])
apply (erule subst)
apply (erule subst)
apply (erule is_ub_thelub)
done
-
lemma ssum_lemma10: "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
apply (intro strip)
apply (rule_tac p = "Y (i) " in IssumE)
@@ -1153,7 +929,7 @@
apply (erule_tac [2] exI)
apply (rule_tac P = "xa=UU" in notE)
apply assumption
-apply (rule less_ssum3c [THEN iffD1])
+apply (rule less_ssum2c [THEN iffD1])
apply (erule subst)
apply (erule subst)
apply (erule is_ub_thelub)
@@ -1219,7 +995,6 @@
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
done
-
lemma ssum_lemma13: "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>
Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
apply simp
@@ -1269,7 +1044,6 @@
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
done
-
lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))"
apply (rule contlubI)
apply (intro strip)
@@ -1302,9 +1076,7 @@
apply (rule contlub_Iwhen3)
done
-(* ------------------------------------------------------------------------ *)
-(* continuous versions of lemmas for 'a ++ 'b *)
-(* ------------------------------------------------------------------------ *)
+text {* continuous versions of lemmas for @{typ "'a ++ 'b"} *}
lemma strict_sinl [simp]: "sinl$UU =UU"
apply (unfold sinl_def)
@@ -1356,7 +1128,6 @@
apply (rule Exh_Ssum)
done
-
lemma ssumE:
assumes major: "p=UU ==> Q"
assumes prem2: "!!x.[|p=sinl$x; x~=UU |] ==> Q"
@@ -1436,7 +1207,7 @@
apply (rule cont_Isinl)
apply (subst beta_cfun)
apply (rule cont_Isinl)
-apply (rule less_ssum3a)
+apply (rule less_ssum2a)
done
lemma less_ssum4b:
@@ -1446,7 +1217,7 @@
apply (rule cont_Isinr)
apply (subst beta_cfun)
apply (rule cont_Isinr)
-apply (rule less_ssum3b)
+apply (rule less_ssum2b)
done
lemma less_ssum4c:
@@ -1456,7 +1227,7 @@
apply (rule cont_Isinr)
apply (subst beta_cfun)
apply (rule cont_Isinl)
-apply (rule less_ssum3c)
+apply (rule less_ssum2c)
done
lemma less_ssum4d:
@@ -1466,7 +1237,7 @@
apply (rule cont_Isinl)
apply (subst beta_cfun)
apply (rule cont_Isinr)
-apply (rule less_ssum3d)
+apply (rule less_ssum2d)
done
lemma ssum_chainE:
@@ -1556,12 +1327,16 @@
apply auto
done
-
-(* ------------------------------------------------------------------------ *)
-(* install simplifier for Ssum *)
-(* ------------------------------------------------------------------------ *)
+text {* install simplifier for Ssum *}
lemmas Ssum_rews = strict_sinl strict_sinr defined_sinl defined_sinr
sscase1 sscase2 sscase3
+text {* for backward compatibility *}
+
+lemmas less_ssum3a = less_ssum2a
+lemmas less_ssum3b = less_ssum2b
+lemmas less_ssum3c = less_ssum2c
+lemmas less_ssum3d = less_ssum2d
+
end
--- a/src/HOLCF/Up.thy Tue Mar 08 00:28:46 2005 +0100
+++ b/src/HOLCF/Up.thy Tue Mar 08 00:32:10 2005 +0100
@@ -12,12 +12,9 @@
imports Cfun Sum_Type Datatype
begin
-(* new type for lifting *)
+subsection {* Definition of new type for lifting *}
-typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
-by auto
-
-instance u :: (sq_ord)sq_ord ..
+typedef (Up) ('a) "u" = "UNIV :: (unit + 'a) set" ..
consts
Iup :: "'a => ('a)u"
@@ -27,15 +24,8 @@
Iup_def: "Iup x == Abs_Up(Inr(x))"
Ifup_def: "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
-defs (overloaded)
- less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of
- Inl(y1) => True
- | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
- | Inr(z2) => y2<<z2))"
-
lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
-apply (simp (no_asm) add: Up_def Abs_Up_inverse)
-done
+by (simp add: Up_def Abs_Up_inverse)
lemma Exh_Up: "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
apply (unfold Iup_def)
@@ -61,15 +51,13 @@
apply (rule Rep_Up_inverse)
done
-lemma inject_Iup: "Iup x=Iup y ==> x=y"
+lemma inject_Iup [dest!]: "Iup x=Iup y ==> x=y"
apply (unfold Iup_def)
apply (rule inj_Inr [THEN injD])
apply (rule inj_Abs_Up [THEN injD])
apply assumption
done
-declare inject_Iup [dest!]
-
lemma defined_Iup: "Iup x~=Abs_Up(Inl ())"
apply (unfold Iup_def)
apply (rule notI)
@@ -79,7 +67,6 @@
apply (erule inj_Abs_Up [THEN injD])
done
-
lemma upE: "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
apply (rule Exh_Up [THEN disjE])
apply fast
@@ -87,57 +74,43 @@
apply fast
done
-lemma Ifup1: "Ifup(f)(Abs_Up(Inl ()))=UU"
+lemma Ifup1 [simp]: "Ifup(f)(Abs_Up(Inl ()))=UU"
apply (unfold Ifup_def)
apply (subst Abs_Up_inverse2)
apply (subst sum_case_Inl)
apply (rule refl)
done
-lemma Ifup2:
- "Ifup(f)(Iup(x))=f$x"
+lemma Ifup2 [simp]: "Ifup(f)(Iup(x))=f$x"
apply (unfold Ifup_def Iup_def)
apply (subst Abs_Up_inverse2)
apply (subst sum_case_Inr)
apply (rule refl)
done
-lemmas Up0_ss = Ifup1 Ifup2
+subsection {* Ordering on type @{typ "'a u"} *}
+
+instance u :: (sq_ord) sq_ord ..
-declare Ifup1 [simp] Ifup2 [simp]
+defs (overloaded)
+ less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of
+ Inl(y1) => True
+ | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
+ | Inr(z2) => y2<<z2))"
-lemma less_up1a:
+lemma less_up1a [iff]:
"Abs_Up(Inl ())<< z"
-apply (unfold less_up_def)
-apply (subst Abs_Up_inverse2)
-apply (subst sum_case_Inl)
-apply (rule TrueI)
-done
+by (simp add: less_up_def Abs_Up_inverse2)
-lemma less_up1b:
+lemma less_up1b [iff]:
"~(Iup x) << (Abs_Up(Inl ()))"
-apply (unfold Iup_def less_up_def)
-apply (rule notI)
-apply (rule iffD1)
-prefer 2 apply (assumption)
-apply (subst Abs_Up_inverse2)
-apply (subst Abs_Up_inverse2)
-apply (subst sum_case_Inr)
-apply (subst sum_case_Inl)
-apply (rule refl)
-done
+by (simp add: Iup_def less_up_def Abs_Up_inverse2)
-lemma less_up1c:
+lemma less_up1c [iff]:
"(Iup x) << (Iup y)=(x<<y)"
-apply (unfold Iup_def less_up_def)
-apply (subst Abs_Up_inverse2)
-apply (subst Abs_Up_inverse2)
-apply (subst sum_case_Inr)
-apply (subst sum_case_Inr)
-apply (rule refl)
-done
+by (simp add: Iup_def less_up_def Abs_Up_inverse2)
-declare less_up1a [iff] less_up1b [iff] less_up1c [iff]
+subsection {* Type @{typ "'a u"} is a partial order *}
lemma refl_less_up: "(p::'a u) << p"
apply (rule_tac p = "p" in upE)
@@ -167,16 +140,11 @@
apply (blast intro: trans_less)
done
-(* Class Instance u::(pcpo)po *)
+instance u :: (pcpo) po
+by intro_classes
+ (assumption | rule refl_less_up antisym_less_up trans_less_up)+
-instance u :: (pcpo)po
-apply (intro_classes)
-apply (rule refl_less_up)
-apply (rule antisym_less_up, assumption+)
-apply (rule trans_less_up, assumption+)
-done
-
-(* for compatibility with old HOLCF-Version *)
+text {* for compatibility with old HOLCF-Version *}
lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of
Inl(y1) => True
| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
@@ -185,49 +153,14 @@
apply (rule refl)
done
-(* -------------------------------------------------------------------------*)
-(* type ('a)u is pointed *)
-(* ------------------------------------------------------------------------ *)
-
-lemma minimal_up: "Abs_Up(Inl ()) << z"
-apply (simp (no_asm) add: less_up1a)
-done
-
-lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
-
-lemma least_up: "EX x::'a u. ALL y. x<<y"
-apply (rule_tac x = "Abs_Up (Inl ())" in exI)
-apply (rule minimal_up [THEN allI])
-done
-
-(* -------------------------------------------------------------------------*)
-(* access to less_up in class po *)
-(* ------------------------------------------------------------------------ *)
-
-lemma less_up2b: "~ Iup(x) << Abs_Up(Inl ())"
-apply (simp (no_asm) add: less_up1b)
-done
-
-lemma less_up2c: "(Iup(x)<<Iup(y)) = (x<<y)"
-apply (simp (no_asm) add: less_up1c)
-done
-
-(* ------------------------------------------------------------------------ *)
-(* Iup and Ifup are monotone *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Monotonicity of @{term Iup} and @{term Ifup} *}
lemma monofun_Iup: "monofun(Iup)"
-
-apply (unfold monofun)
-apply (intro strip)
-apply (erule less_up2c [THEN iffD2])
-done
+by (simp add: monofun)
lemma monofun_Ifup1: "monofun(Ifup)"
-apply (unfold monofun)
-apply (intro strip)
-apply (rule less_fun [THEN iffD2])
-apply (intro strip)
+apply (rule monofunI [rule_format])
+apply (rule less_fun [THEN iffD2, rule_format])
apply (rule_tac p = "xa" in upE)
apply simp
apply simp
@@ -235,8 +168,7 @@
done
lemma monofun_Ifup2: "monofun(Ifup(f))"
-apply (unfold monofun)
-apply (intro strip)
+apply (rule monofunI [rule_format])
apply (rule_tac p = "x" in upE)
apply simp
apply simp
@@ -246,17 +178,12 @@
apply (erule monofun_cfun_arg)
done
-(* ------------------------------------------------------------------------ *)
-(* Some kind of surjectivity lemma *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Type @{typ "'a u"} is a cpo *}
+
+text {* Some kind of surjectivity lemma *}
lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
-apply simp
-done
-
-(* ------------------------------------------------------------------------ *)
-(* ('a)u is a cpo *)
-(* ------------------------------------------------------------------------ *)
+by simp
lemma lub_up1a: "[|chain(Y);EX i x. Y(i)=Iup(x)|]
==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
@@ -265,10 +192,10 @@
apply (rule_tac p = "Y (i) " in upE)
apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst)
apply (erule sym)
-apply (rule minimal_up)
+apply (rule less_up1a)
apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst])
apply assumption
-apply (rule less_up2c [THEN iffD2])
+apply (rule less_up1c [THEN iffD2])
apply (rule is_ub_thelub)
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
apply (rule_tac p = "u" in upE)
@@ -277,12 +204,12 @@
apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE)
apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
apply assumption
-apply (rule less_up2b)
+apply (rule less_up1b)
apply (erule subst)
apply (erule ub_rangeD)
apply (rule_tac t = "u" in up_lemma1 [THEN subst])
apply assumption
-apply (rule less_up2c [THEN iffD2])
+apply (rule less_up1c [THEN iffD2])
apply (rule is_lub_thelub)
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
apply (erule monofun_Ifup2 [THEN ub2ub_monofun])
@@ -295,12 +222,8 @@
apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst)
apply assumption
apply (rule refl_less)
-apply (rule notE)
-apply (drule spec)
-apply (drule spec)
-apply assumption
-apply assumption
-apply (rule minimal_up)
+apply simp
+apply (rule less_up1a)
done
lemmas thelub_up1a = lub_up1a [THEN thelubI, standard]
@@ -316,60 +239,55 @@
*)
lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"
-apply (rule disjE)
-apply (rule_tac [2] exI)
-apply (erule_tac [2] lub_up1a)
-prefer 2 apply (assumption)
-apply (rule_tac [2] exI)
-apply (erule_tac [2] lub_up1b)
-prefer 2 apply (assumption)
-apply fast
-done
-
-(* Class instance of ('a)u for class pcpo *)
-
-instance u :: (pcpo)pcpo
-apply (intro_classes)
-apply (erule cpo_up)
-apply (rule least_up)
+apply (case_tac "\<exists> i x. Y i = Iup x")
+apply (rule exI)
+apply (erule lub_up1a)
+apply assumption
+apply (rule exI)
+apply (erule lub_up1b)
+apply simp
done
-constdefs
- up :: "'a -> ('a)u"
- "up == (LAM x. Iup(x))"
- fup :: "('a->'c)-> ('a)u -> 'c"
- "fup == (LAM f p. Ifup(f)(p))"
+instance u :: (pcpo) cpo
+by intro_classes (rule cpo_up)
+
+subsection {* Type @{typ "'a u"} is pointed *}
-translations
-"case l of up$x => t1" == "fup$(LAM x. t1)$l"
+lemma minimal_up: "Abs_Up(Inl ()) << z"
+by (rule less_up1a)
-(* for compatibility with old HOLCF-Version *)
-lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
-apply (simp add: UU_def UU_up_def)
+lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
+
+lemma least_up: "EX x::'a u. ALL y. x<<y"
+apply (rule_tac x = "Abs_Up (Inl ())" in exI)
+apply (rule minimal_up [THEN allI])
done
-(* -------------------------------------------------------------------------*)
-(* some lemmas restated for class pcpo *)
-(* ------------------------------------------------------------------------ *)
+instance u :: (pcpo) pcpo
+by intro_classes (rule least_up)
+
+text {* for compatibility with old HOLCF-Version *}
+lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
+by (simp add: UU_def UU_up_def)
+
+text {* some lemmas restated for class pcpo *}
lemma less_up3b: "~ Iup(x) << UU"
apply (subst inst_up_pcpo)
-apply (rule less_up2b)
+apply (rule less_up1b)
done
-lemma defined_Iup2: "Iup(x) ~= UU"
+lemma defined_Iup2 [iff]: "Iup(x) ~= UU"
apply (subst inst_up_pcpo)
apply (rule defined_Iup)
done
-declare defined_Iup2 [iff]
-(* ------------------------------------------------------------------------ *)
-(* continuity for Iup *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Continuity of @{term Iup} and @{term Ifup} *}
+
+text {* continuity for @{term Iup} *}
lemma contlub_Iup: "contlub(Iup)"
-apply (rule contlubI)
-apply (intro strip)
+apply (rule contlubI [rule_format])
apply (rule trans)
apply (rule_tac [2] thelub_up1a [symmetric])
prefer 3 apply fast
@@ -382,20 +300,16 @@
apply simp
done
-lemma cont_Iup: "cont(Iup)"
+lemma cont_Iup [iff]: "cont(Iup)"
apply (rule monocontlub2cont)
apply (rule monofun_Iup)
apply (rule contlub_Iup)
done
-declare cont_Iup [iff]
-(* ------------------------------------------------------------------------ *)
-(* continuity for Ifup *)
-(* ------------------------------------------------------------------------ *)
+text {* continuity for @{term Ifup} *}
lemma contlub_Ifup1: "contlub(Ifup)"
-apply (rule contlubI)
-apply (intro strip)
+apply (rule contlubI [rule_format])
apply (rule trans)
apply (rule_tac [2] thelub_fun [symmetric])
apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
@@ -407,10 +321,8 @@
apply (erule contlub_cfun_fun)
done
-
lemma contlub_Ifup2: "contlub(Ifup(f))"
-apply (rule contlubI)
-apply (intro strip)
+apply (rule contlubI [rule_format])
apply (rule disjE)
defer 1
apply (subst thelub_up1a)
@@ -464,13 +376,20 @@
apply (rule contlub_Ifup2)
done
+subsection {* Continuous versions of constants *}
-(* ------------------------------------------------------------------------ *)
-(* continuous versions of lemmas for ('a)u *)
-(* ------------------------------------------------------------------------ *)
+constdefs
+ up :: "'a -> ('a)u"
+ "up == (LAM x. Iup(x))"
+ fup :: "('a->'c)-> ('a)u -> 'c"
+ "fup == (LAM f p. Ifup(f)(p))"
+
+translations
+"case l of up$x => t1" == "fup$(LAM x. t1)$l"
+
+text {* continuous versions of lemmas for @{typ "('a)u"} *}
lemma Exh_Up1: "z = UU | (EX x. z = up$x)"
-
apply (unfold up_def)
apply simp
apply (subst inst_up_pcpo)
@@ -483,10 +402,8 @@
apply auto
done
-lemma defined_up: " up$x ~= UU"
-apply (unfold up_def)
-apply auto
-done
+lemma defined_up [simp]: " up$x ~= UU"
+by (simp add: up_def)
lemma upE1:
"[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q"
@@ -499,7 +416,7 @@
lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L
-lemma fup1: "fup$f$UU=UU"
+lemma fup1 [simp]: "fup$f$UU=UU"
apply (unfold up_def fup_def)
apply (subst inst_up_pcpo)
apply (subst beta_cfun)
@@ -509,7 +426,7 @@
apply simp
done
-lemma fup2: "fup$f$(up$x)=f$x"
+lemma fup2 [simp]: "fup$f$(up$x)=f$x"
apply (unfold up_def fup_def)
apply (simplesubst beta_cfun)
apply (rule cont_Iup)
@@ -521,16 +438,10 @@
done
lemma less_up4b: "~ up$x << UU"
-apply (unfold up_def fup_def)
-apply simp
-apply (rule less_up3b)
-done
+by (simp add: up_def fup_def less_up3b)
-lemma less_up4c:
- "(up$x << up$y) = (x<<y)"
-apply (unfold up_def fup_def)
-apply simp
-done
+lemma less_up4c: "(up$x << up$y) = (x<<y)"
+by (simp add: up_def fup_def)
lemma thelub_up2a:
"[| chain(Y); EX i x. Y(i) = up$x |] ==>
@@ -553,34 +464,25 @@
apply simp
done
-
-
lemma thelub_up2b:
"[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU"
apply (unfold up_def fup_def)
apply (subst inst_up_pcpo)
-apply (rule thelub_up1b)
-apply assumption
-apply (intro strip)
-apply (drule spec)
-apply (drule spec)
+apply (erule thelub_up1b)
apply simp
done
-
lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)"
apply (rule iffI)
apply (erule exE)
apply simp
-apply (rule defined_up)
apply (rule_tac p = "z" in upE1)
-apply (erule notE)
-apply assumption
+apply simp
apply (erule exI)
done
-
-lemma thelub_up2a_rev: "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
+lemma thelub_up2a_rev:
+ "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
apply (rule exE)
apply (rule chain_UU_I_inverse2)
apply (rule up_lemma2 [THEN iffD1])
@@ -590,10 +492,9 @@
apply assumption
done
-lemma thelub_up2b_rev: "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up$x"
-apply (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
-done
-
+lemma thelub_up2b_rev:
+ "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up$x"
+by (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU |
lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
@@ -611,17 +512,13 @@
lemma fup3: "fup$up$x=x"
apply (rule_tac p = "x" in upE1)
-apply (simp add: fup1 fup2)
-apply (simp add: fup1 fup2)
+apply simp
+apply simp
done
-(* ------------------------------------------------------------------------ *)
-(* install simplifier for ('a)u *)
-(* ------------------------------------------------------------------------ *)
+text {* for backward compatibility *}
-declare fup1 [simp] fup2 [simp] defined_up [simp]
+lemmas less_up2b = less_up1b
+lemmas less_up2c = less_up1c
end
-
-
-