--- 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