--- a/src/HOLCF/Sprod.ML Tue May 24 05:51:06 2005 +0200
+++ b/src/HOLCF/Sprod.ML Tue May 24 05:52:48 2005 +0200
@@ -1,75 +1,11 @@
(* legacy ML bindings *)
-val Ispair_def = thm "Ispair_def";
-val Isfst_def = thm "Isfst_def";
-val Issnd_def = thm "Issnd_def";
-val SprodI = thm "SprodI";
-val inj_on_Abs_Sprod = thm "inj_on_Abs_Sprod";
-val strict_Spair_Rep = thm "strict_Spair_Rep";
-val defined_Spair_Rep_rev = thm "defined_Spair_Rep_rev";
-val inject_Spair_Rep = thm "inject_Spair_Rep";
-val inject_Ispair = thm "inject_Ispair";
-val strict_Ispair = thm "strict_Ispair";
-val strict_Ispair1 = thm "strict_Ispair1";
-val strict_Ispair2 = thm "strict_Ispair2";
-val strict_Ispair_rev = thm "strict_Ispair_rev";
-val defined_Ispair_rev = thm "defined_Ispair_rev";
-val defined_Ispair = thm "defined_Ispair";
-val Exh_Sprod = thm "Exh_Sprod";
-val IsprodE = thm "IsprodE";
-val strict_Isfst = thm "strict_Isfst";
-val strict_Isfst1 = thm "strict_Isfst1";
-val strict_Isfst2 = thm "strict_Isfst2";
-val strict_Issnd = thm "strict_Issnd";
-val strict_Issnd1 = thm "strict_Issnd1";
-val strict_Issnd2 = thm "strict_Issnd2";
-val Isfst = thm "Isfst";
-val Issnd = thm "Issnd";
-val Isfst2 = thm "Isfst2";
-val Issnd2 = thm "Issnd2";
-val Sprod0_ss = [strict_Isfst1, strict_Isfst2, strict_Issnd1, strict_Issnd2,
- Isfst2, Issnd2]
-val defined_IsfstIssnd = thm "defined_IsfstIssnd";
-val surjective_pairing_Sprod = thm "surjective_pairing_Sprod";
-val Sel_injective_Sprod = thm "Sel_injective_Sprod";
val less_sprod_def = thm "less_sprod_def";
-val refl_less_sprod = thm "refl_less_sprod";
-val antisym_less_sprod = thm "antisym_less_sprod";
-val trans_less_sprod = thm "trans_less_sprod";
-val inst_sprod_po = thm "inst_sprod_po";
-val minimal_sprod = thm "minimal_sprod";
-val UU_sprod_def = thm "UU_sprod_def";
-val least_sprod = thm "least_sprod";
-val monofun_Ispair1 = thm "monofun_Ispair1";
-val monofun_Ispair2 = thm "monofun_Ispair2";
-val monofun_Ispair = thm "monofun_Ispair";
-val monofun_Isfst = thm "monofun_Isfst";
-val monofun_Issnd = thm "monofun_Issnd";
-val lub_sprod = thm "lub_sprod";
-val thelub_sprod = thm "thelub_sprod";
-val cpo_sprod = thm "cpo_sprod";
val spair_def = thm "spair_def";
val sfst_def = thm "sfst_def";
val ssnd_def = thm "ssnd_def";
val ssplit_def = thm "ssplit_def";
-val inst_sprod_pcpo = thm "inst_sprod_pcpo";
-val sprod3_lemma1 = thm "sprod3_lemma1";
-val sprod3_lemma2 = thm "sprod3_lemma2";
-val sprod3_lemma3 = thm "sprod3_lemma3";
-val contlub_Ispair1 = thm "contlub_Ispair1";
-val sprod3_lemma4 = thm "sprod3_lemma4";
-val sprod3_lemma5 = thm "sprod3_lemma5";
-val sprod3_lemma6 = thm "sprod3_lemma6";
-val contlub_Ispair2 = thm "contlub_Ispair2";
-val cont_Ispair1 = thm "cont_Ispair1";
-val cont_Ispair2 = thm "cont_Ispair2";
-val contlub_Isfst = thm "contlub_Isfst";
-val contlub_Issnd = thm "contlub_Issnd";
-val cont_Isfst = thm "cont_Isfst";
-val cont_Issnd = thm "cont_Issnd";
-val spair_eq = thm "spair_eq";
-val beta_cfun_sprod = thm "beta_cfun_sprod";
val inject_spair = thm "inject_spair";
val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
val strict_spair = thm "strict_spair";
@@ -81,21 +17,12 @@
val Exh_Sprod2 = thm "Exh_Sprod2";
val sprodE = thm "sprodE";
val strict_sfst = thm "strict_sfst";
-val strict_sfst1 = thm "strict_sfst1";
-val strict_sfst2 = thm "strict_sfst2";
val strict_ssnd = thm "strict_ssnd";
-val strict_ssnd1 = thm "strict_ssnd1";
-val strict_ssnd2 = thm "strict_ssnd2";
val sfst2 = thm "sfst2";
val ssnd2 = thm "ssnd2";
val defined_sfstssnd = thm "defined_sfstssnd";
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
-val lub_sprod2 = thm "lub_sprod2";
-val thelub_sprod2 = thm "thelub_sprod2";
val ssplit1 = thm "ssplit1";
val ssplit2 = thm "ssplit2";
val ssplit3 = thm "ssplit3";
-val Sprod_rews = [strict_sfst1, strict_sfst2,
- strict_ssnd1, strict_ssnd2, sfst2, ssnd2, defined_spair,
- ssplit1, ssplit2]
--- a/src/HOLCF/Sprod.thy Tue May 24 05:51:06 2005 +0200
+++ b/src/HOLCF/Sprod.thy Tue May 24 05:52:48 2005 +0200
@@ -1,6 +1,6 @@
(* Title: HOLCF/Sprod.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger and Brian Huffman
License: GPL (GNU GENERAL PUBLIC LICENSE)
Strict product with typedef.
@@ -9,452 +9,76 @@
header {* The type of strict products *}
theory Sprod
-imports Cfun
+imports Cprod TypedefPcpo
begin
subsection {* Definition of strict product type *}
-constdefs
- Spair_Rep :: "['a,'b] => ['a,'b] => bool"
- "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))"
-
-typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
-by auto
+typedef (Sprod) ('a, 'b) "**" (infixr 20) =
+ "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
+by (auto simp add: inst_cprod_pcpo)
syntax (xsymbols)
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
syntax (HTML output)
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
-consts
- Ispair :: "['a,'b] => ('a ** 'b)"
- Isfst :: "('a ** 'b) => 'a"
- Issnd :: "('a ** 'b) => 'b"
-
-defs
- (*defining the abstract constants*)
-
- Ispair_def: "Ispair a b == Abs_Sprod(Spair_Rep a b)"
-
- Isfst_def: "Isfst(p) == THE z. (p=Ispair UU UU --> z=UU)
- &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)"
-
- Issnd_def: "Issnd(p) == THE z. (p=Ispair UU UU --> z=UU)
- &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"
-
-text {* A non-emptiness result for Sprod *}
-
-lemma SprodI: "(Spair_Rep a b):Sprod"
-apply (unfold Sprod_def)
-apply (rule CollectI, rule exI, rule exI, rule refl)
-done
+subsection {* Class instances *}
-lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
-apply (rule inj_on_inverseI)
-apply (erule Abs_Sprod_inverse)
-done
-
-text {* Strictness and definedness of @{term Spair_Rep} *}
+instance "**" :: (pcpo, pcpo) sq_ord ..
+defs (overloaded)
+ less_sprod_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Sprod x \<sqsubseteq> Rep_Sprod y"
-lemma strict_Spair_Rep:
- "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
-apply (unfold Spair_Rep_def)
-apply (rule ext)
-apply (rule ext)
-apply (rule iffI)
-apply fast
-apply fast
-done
-
-lemma defined_Spair_Rep_rev:
- "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
-apply (unfold Spair_Rep_def)
-apply (case_tac "a=UU|b=UU")
-apply assumption
-apply (fast dest: fun_cong)
-done
-
-text {* injectivity of @{term Spair_Rep} and @{term Ispair} *}
+lemma adm_Sprod: "adm (\<lambda>x. x \<in> Sprod)"
+by (simp add: Sprod_def)
-lemma inject_Spair_Rep:
-"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
-
-apply (unfold Spair_Rep_def)
-apply (drule fun_cong)
-apply (drule fun_cong)
-apply (erule iffD1 [THEN mp])
-apply auto
-done
-
-lemma inject_Ispair:
- "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
-apply (unfold Ispair_def)
-apply (erule inject_Spair_Rep)
-apply assumption
-apply (erule inj_on_Abs_Sprod [THEN inj_onD])
-apply (rule SprodI)
-apply (rule SprodI)
-done
-
-text {* strictness and definedness of @{term Ispair} *}
+lemma UU_Sprod: "\<bottom> \<in> Sprod"
+by (simp add: Sprod_def)
-lemma strict_Ispair:
- "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
-apply (unfold Ispair_def)
-apply (erule strict_Spair_Rep [THEN arg_cong])
-done
-
-lemma strict_Ispair1:
- "Ispair UU b = Ispair UU UU"
-apply (unfold Ispair_def)
-apply (rule strict_Spair_Rep [THEN arg_cong])
-apply (rule disjI1)
-apply (rule refl)
-done
+instance "**" :: (pcpo, pcpo) po
+by (rule typedef_po [OF type_definition_Sprod less_sprod_def])
-lemma strict_Ispair2:
- "Ispair a UU = Ispair UU UU"
-apply (unfold Ispair_def)
-apply (rule strict_Spair_Rep [THEN arg_cong])
-apply (rule disjI2)
-apply (rule refl)
-done
-
-lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
-apply (rule de_Morgan_disj [THEN subst])
-apply (erule contrapos_nn)
-apply (erule strict_Ispair)
-done
+instance "**" :: (pcpo, pcpo) cpo
+by (rule typedef_cpo [OF type_definition_Sprod less_sprod_def adm_Sprod])
-lemma defined_Ispair_rev:
- "Ispair a b = Ispair UU UU ==> (a = UU | b = UU)"
-apply (unfold Ispair_def)
-apply (rule defined_Spair_Rep_rev)
-apply (rule inj_on_Abs_Sprod [THEN inj_onD])
-apply assumption
-apply (rule SprodI)
-apply (rule SprodI)
-done
-
-lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"
-apply (rule contrapos_nn)
-apply (erule_tac [2] defined_Ispair_rev)
-apply (rule de_Morgan_disj [THEN iffD2])
-apply (erule conjI)
-apply assumption
-done
-
-text {* Exhaustion of the strict product @{typ "'a ** 'b"} *}
+instance "**" :: (pcpo, pcpo) pcpo
+by (rule typedef_pcpo_UU [OF type_definition_Sprod less_sprod_def UU_Sprod])
-lemma Exh_Sprod:
- "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
-apply (unfold Ispair_def)
-apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
-apply (erule exE)
-apply (erule exE)
-apply (rule excluded_middle [THEN disjE])
-apply (rule disjI2)
-apply (rule exI)
-apply (rule exI)
-apply (rule conjI)
-apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
-apply (erule arg_cong)
-apply (rule de_Morgan_disj [THEN subst])
-apply assumption
-apply (rule disjI1)
-apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
-apply (rule_tac f = "Abs_Sprod" in arg_cong)
-apply (erule trans)
-apply (erule strict_Spair_Rep)
-done
+lemmas cont_Rep_Sprod =
+ typedef_cont_Rep [OF type_definition_Sprod less_sprod_def adm_Sprod]
-text {* general elimination rule for strict product *}
+lemmas cont_Abs_Sprod =
+ typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod]
-lemma IsprodE:
-assumes prem1: "p=Ispair UU UU ==> Q"
-assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q"
-shows "Q"
-apply (rule Exh_Sprod [THEN disjE])
-apply (erule prem1)
-apply (erule exE)
-apply (erule exE)
-apply (erule conjE)
-apply (erule conjE)
-apply (erule prem2)
-apply assumption
-apply assumption
-done
+lemmas strict_Rep_Sprod =
+ typedef_strict_Rep [OF type_definition_Sprod less_sprod_def UU_Sprod]
-text {* some results about the selectors @{term Isfst}, @{term Issnd} *}
-
-lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
-apply (unfold Isfst_def)
-apply (rule the_equality)
-apply (rule conjI)
-apply fast
-apply (intro strip)
-apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
-apply (rule not_sym)
-apply (rule defined_Ispair)
-apply (fast+)
-done
+lemmas strict_Abs_Sprod =
+ typedef_strict_Abs [OF type_definition_Sprod less_sprod_def UU_Sprod]
-lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU"
-apply (subst strict_Ispair1)
-apply (rule strict_Isfst)
-apply (rule refl)
-done
-
-lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU"
-apply (subst strict_Ispair2)
-apply (rule strict_Isfst)
-apply (rule refl)
-done
+lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
+by (simp add: strict_Abs_Sprod inst_cprod_pcpo2 [symmetric])
-lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
-apply (unfold Issnd_def)
-apply (rule the_equality)
-apply (rule conjI)
-apply fast
-apply (intro strip)
-apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
-apply (rule not_sym)
-apply (rule defined_Ispair)
-apply (fast+)
-done
-
-lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU"
-apply (subst strict_Ispair1)
-apply (rule strict_Issnd)
-apply (rule refl)
-done
-
-lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU"
-apply (subst strict_Ispair2)
-apply (rule strict_Issnd)
-apply (rule refl)
+lemma spair_lemma:
+ "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
+apply (simp add: Sprod_def inst_cprod_pcpo2)
+apply (case_tac "a = \<bottom>", case_tac [!] "b = \<bottom>", simp_all)
done
-lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
-apply (unfold Isfst_def)
-apply (rule the_equality)
-apply (rule conjI)
-apply (intro strip)
-apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
-apply (erule defined_Ispair)
-apply assumption
-apply assumption
-apply (intro strip)
-apply (rule inject_Ispair [THEN conjunct1])
-prefer 3 apply fast
-apply (fast+)
-done
-
-lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
-apply (unfold Issnd_def)
-apply (rule the_equality)
-apply (rule conjI)
-apply (intro strip)
-apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
-apply (erule defined_Ispair)
-apply assumption
-apply assumption
-apply (intro strip)
-apply (rule inject_Ispair [THEN conjunct2])
-prefer 3 apply fast
-apply (fast+)
-done
-
-lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
-apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
-apply (erule Isfst)
-apply assumption
-apply (erule ssubst)
-apply (rule strict_Isfst1)
-done
-
-lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
-apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
-apply (erule Issnd)
-apply assumption
-apply (erule ssubst)
-apply (rule strict_Issnd2)
-done
-
-
-text {* instantiate the simplifier *}
-
-lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
- Isfst2 Issnd2
-
-declare Isfst2 [simp] Issnd2 [simp]
-
-lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
-apply (rule_tac p = "p" in IsprodE)
-apply simp
-apply (erule ssubst)
-apply (rule conjI)
-apply (simp add: Sprod0_ss)
-apply (simp add: Sprod0_ss)
-done
-
-
-text {* Surjective pairing: equivalent to @{thm [source] Exh_Sprod} *}
-
-lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
-apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
-apply (simp add: Sprod0_ss)
-apply (erule exE)
-apply (erule exE)
-apply (simp add: Sprod0_ss)
-done
-
-lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
-apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
-apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
-apply simp
-done
-
-subsection {* Type @{typ "'a ** 'b"} is a partial order *}
-
-instance "**" :: (sq_ord, sq_ord) sq_ord ..
-
-defs (overloaded)
- less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
-
-lemma refl_less_sprod: "(p::'a ** 'b) << p"
-apply (unfold less_sprod_def)
-apply (fast intro: refl_less)
-done
-
-lemma antisym_less_sprod:
- "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
-apply (unfold less_sprod_def)
-apply (rule Sel_injective_Sprod)
-apply (fast intro: antisym_less)
-apply (fast intro: antisym_less)
-done
-
-lemma trans_less_sprod:
- "[|(p1::'a ** 'b) << p2;p2 << p3|] ==> p1 << p3"
-apply (unfold less_sprod_def)
-apply (blast intro: trans_less)
-done
-
-instance "**" :: (pcpo, pcpo) po
-by intro_classes
- (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
+subsection {* Definitions of constants *}
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
-apply (fold less_sprod_def)
-apply (rule refl)
-done
-
-subsection {* Monotonicity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
-
-text {* @{term Ispair} is monotone in both arguments *}
-
-lemma monofun_Ispair1: "monofun(Ispair)"
-apply (unfold monofun)
-apply (intro strip)
-apply (rule less_fun [THEN iffD2])
-apply (intro strip)
-apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
-apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
-apply (frule notUU_I)
-apply assumption
-apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
-done
-
-lemma monofun_Ispair2: "monofun(Ispair(x))"
-apply (unfold monofun)
-apply (intro strip)
-apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
-apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
-apply (frule notUU_I)
-apply assumption
-apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
-done
-
-lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
-apply (rule trans_less)
-apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
-prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
-apply assumption
-apply assumption
-done
-
-text {* @{term Isfst} and @{term Issnd} are monotone *}
-
-lemma monofun_Isfst: "monofun(Isfst)"
-by (simp add: monofun inst_sprod_po)
-
-lemma monofun_Issnd: "monofun(Issnd)"
-by (simp add: monofun inst_sprod_po)
-
-subsection {* Type @{typ "'a ** 'b"} is a cpo *}
+consts
+ sfst :: "('a ** 'b) \<rightarrow> 'a"
+ ssnd :: "('a ** 'b) \<rightarrow> 'b"
+ spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)"
+ ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
-lemma lub_sprod:
-"[|chain(S)|] ==> range(S) <<|
- Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
-apply (rule monofun_Ispair)
-apply (rule is_ub_thelub)
-apply (erule monofun_Isfst [THEN ch2ch_monofun])
-apply (rule is_ub_thelub)
-apply (erule monofun_Issnd [THEN ch2ch_monofun])
-apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
-apply (rule monofun_Ispair)
-apply (rule is_lub_thelub)
-apply (erule monofun_Isfst [THEN ch2ch_monofun])
-apply (erule monofun_Isfst [THEN ub2ub_monofun])
-apply (rule is_lub_thelub)
-apply (erule monofun_Issnd [THEN ch2ch_monofun])
-apply (erule monofun_Issnd [THEN ub2ub_monofun])
-done
-
-lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
-
-lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
-apply (rule exI)
-apply (erule lub_sprod)
-done
-
-instance "**" :: (pcpo, pcpo) cpo
-by intro_classes (rule cpo_sprod)
-
-subsection {* Type @{typ "'a ** 'b"} is pointed *}
-
-lemma minimal_sprod: "Ispair UU UU << p"
-apply (simp add: inst_sprod_po minimal)
-done
-
-lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
-
-lemma least_sprod: "? x::'a**'b.!y. x<<y"
-apply (rule_tac x = "Ispair UU UU" in exI)
-apply (rule minimal_sprod [THEN allI])
-done
-
-instance "**" :: (pcpo, pcpo) pcpo
-by intro_classes (rule least_sprod)
-
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_sprod_pcpo: "UU = Ispair UU UU"
-by (simp add: UU_def UU_sprod_def)
-
-declare inst_sprod_pcpo [symmetric, simp]
-
-subsection {* Continuous versions of constants *}
-
-consts
- spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
- sfst :: "('a**'b)->'a"
- ssnd :: "('a**'b)->'b"
- ssplit :: "('a->'b->'c)->('a**'b)->'c"
+defs
+ sfst_def: "sfst \<equiv> \<Lambda> p. cfst\<cdot>(Rep_Sprod p)"
+ ssnd_def: "ssnd \<equiv> \<Lambda> p. csnd\<cdot>(Rep_Sprod p)"
+ spair_def: "spair \<equiv> \<Lambda> a b. Abs_Sprod
+ <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
+ ssplit_def: "ssplit \<equiv> \<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p))"
syntax
"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
@@ -463,467 +87,107 @@
"(:x, y, z:)" == "(:x, (:y, z:):)"
"(:x, y:)" == "spair$x$y"
-defs
-spair_def: "spair == (LAM x y. Ispair x y)"
-sfst_def: "sfst == (LAM p. Isfst p)"
-ssnd_def: "ssnd == (LAM p. Issnd p)"
-ssplit_def: "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
-
-subsection {* Continuity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
+subsection {* Case analysis *}
-lemma sprod3_lemma1:
-"[| chain(Y); x~= UU; lub(range(Y))~= UU |] ==>
- Ispair (lub(range Y)) x =
- Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))
- (lub(range(%i. Issnd(Ispair(Y i) x))))"
-apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
-apply (rule lub_equal)
-apply assumption
-apply (rule monofun_Isfst [THEN ch2ch_monofun])
-apply (rule ch2ch_fun)
-apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
-apply assumption
-apply (rule allI)
-apply (simp (no_asm_simp))
-apply (rule sym)
-apply (drule chain_UU_I_inverse2)
-apply (erule exE)
-apply (rule lub_chain_maxelem)
-apply (erule Issnd2)
-apply (rule allI)
-apply (rename_tac "j")
-apply (case_tac "Y (j) =UU")
-apply auto
-done
-
-lemma sprod3_lemma2:
-"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>
- Ispair (lub(range Y)) x =
- Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))
- (lub(range(%i. Issnd(Ispair(Y i) x))))"
-apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
-apply assumption
-apply (rule trans)
-apply (rule strict_Ispair1)
-apply (rule strict_Ispair [symmetric])
-apply (rule disjI1)
-apply (rule chain_UU_I_inverse)
-apply auto
-apply (erule chain_UU_I [THEN spec])
-apply assumption
+lemma spair_Abs_Sprod:
+ "(:a, b:) = Abs_Sprod <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
+apply (unfold spair_def)
+apply (simp add: cont_Abs_Sprod spair_lemma)
done
-
-lemma sprod3_lemma3:
-"[| chain(Y); x = UU |] ==>
- Ispair (lub(range Y)) x =
- Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))
- (lub(range(%i. Issnd(Ispair (Y i) x))))"
-apply (erule ssubst)
-apply (rule trans)
-apply (rule strict_Ispair2)
-apply (rule strict_Ispair [symmetric])
-apply (rule disjI1)
-apply (rule chain_UU_I_inverse)
-apply (rule allI)
-apply (simp add: Sprod0_ss)
-done
-
-lemma contlub_Ispair1: "contlub(Ispair)"
-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_Ispair1 [THEN ch2ch_monofun])
-apply (rule trans)
-apply (rule_tac [2] thelub_sprod [symmetric])
-apply (rule_tac [2] ch2ch_fun)
-apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
-apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
-apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
-apply (erule sprod3_lemma1)
-apply assumption
-apply assumption
-apply (erule sprod3_lemma2)
-apply assumption
-apply assumption
-apply (erule sprod3_lemma3)
-apply assumption
-done
-
-lemma sprod3_lemma4:
-"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>
- Ispair x (lub(range Y)) =
- Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))
- (lub(range(%i. Issnd (Ispair x (Y i)))))"
-apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
-apply (rule sym)
-apply (drule chain_UU_I_inverse2)
-apply (erule exE)
-apply (rule lub_chain_maxelem)
-apply (erule Isfst2)
-apply (rule allI)
-apply (rename_tac "j")
-apply (case_tac "Y (j) =UU")
-apply auto
+lemma Exh_Sprod2:
+ "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
+apply (rule_tac x=z in Abs_Sprod_cases)
+apply (simp add: Sprod_def)
+apply (erule disjE)
+apply (simp add: strict_Abs_Sprod)
+apply (rule disjI2)
+apply (rule_tac x="cfst\<cdot>y" in exI)
+apply (rule_tac x="csnd\<cdot>y" in exI)
+apply (simp add: spair_Abs_Sprod Abs_Sprod_inject spair_lemma)
+apply (simp add: surjective_pairing_Cprod2)
done
-lemma sprod3_lemma5:
-"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>
- Ispair x (lub(range Y)) =
- Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))
- (lub(range(%i. Issnd(Ispair x (Y i)))))"
-apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
-apply assumption
-apply (rule trans)
-apply (rule strict_Ispair2)
-apply (rule strict_Ispair [symmetric])
-apply (rule disjI2)
-apply (rule chain_UU_I_inverse)
-apply (rule allI)
-apply (simp add: Sprod0_ss)
-apply (erule chain_UU_I [THEN spec])
-apply assumption
+lemma sprodE:
+ "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+by (cut_tac z=p in Exh_Sprod2, auto)
+
+subsection {* Properties of @{term spair} *}
+
+lemma strict_spair1 [simp]: "(:\<bottom>, b:) = \<bottom>"
+apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
+apply (case_tac "b = \<bottom>", simp_all)
done
-lemma sprod3_lemma6:
-"[| chain(Y); x = UU |] ==>
- Ispair x (lub(range Y)) =
- Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))
- (lub(range(%i. Issnd (Ispair x (Y i)))))"
-apply (rule_tac s = "UU" and t = "x" in ssubst)
-apply assumption
-apply (rule trans)
-apply (rule strict_Ispair1)
-apply (rule strict_Ispair [symmetric])
-apply (rule disjI1)
-apply (rule chain_UU_I_inverse)
-apply (rule allI)
-apply (simp add: Sprod0_ss)
-done
-
-lemma contlub_Ispair2: "contlub(Ispair(x))"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule trans)
-apply (rule_tac [2] thelub_sprod [symmetric])
-apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
-apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
-apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
-apply (erule sprod3_lemma4)
-apply assumption
-apply assumption
-apply (erule sprod3_lemma5)
-apply assumption
-apply assumption
-apply (erule sprod3_lemma6)
-apply assumption
-done
-
-lemma cont_Ispair1: "cont(Ispair)"
-apply (rule monocontlub2cont)
-apply (rule monofun_Ispair1)
-apply (rule contlub_Ispair1)
-done
-
-lemma cont_Ispair2: "cont(Ispair(x))"
-apply (rule monocontlub2cont)
-apply (rule monofun_Ispair2)
-apply (rule contlub_Ispair2)
+lemma strict_spair2 [simp]: "(:a, \<bottom>:) = \<bottom>"
+apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
+apply (case_tac "a = \<bottom>", simp_all)
done
-lemma contlub_Isfst: "contlub(Isfst)"
-apply (rule contlubI)
-apply (intro strip)
-apply (subst lub_sprod [THEN thelubI])
-apply assumption
-apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
-apply (simp add: Sprod0_ss)
-apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
-apply assumption
-apply (rule trans)
-apply (simp add: Sprod0_ss)
-apply (rule sym)
-apply (rule chain_UU_I_inverse)
-apply (rule allI)
-apply (rule strict_Isfst)
-apply (rule contrapos_np)
-apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
-apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
+lemma strict_spair: "a = \<bottom> \<or> b = \<bottom> \<Longrightarrow> (:a, b:) = \<bottom>"
+by auto
+
+lemma strict_spair_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
+by (erule contrapos_np, auto)
+
+lemma defined_spair [simp]:
+ "\<lbrakk>a \<noteq> \<bottom>; b \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:a, b:) \<noteq> \<bottom>"
+apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
+apply (subst Abs_Sprod_inject)
+apply (simp add: Sprod_def)
+apply (simp add: Sprod_def inst_cprod_pcpo2)
+apply simp
done
-lemma contlub_Issnd: "contlub(Issnd)"
-apply (rule contlubI)
-apply (intro strip)
-apply (subst lub_sprod [THEN thelubI])
-apply assumption
-apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
-apply (simp add: Sprod0_ss)
-apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
-apply assumption
-apply (simp add: Sprod0_ss)
-apply (rule sym)
-apply (rule chain_UU_I_inverse)
-apply (rule allI)
-apply (rule strict_Issnd)
-apply (rule contrapos_np)
-apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
-apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
-done
-
-lemma cont_Isfst: "cont(Isfst)"
-apply (rule monocontlub2cont)
-apply (rule monofun_Isfst)
-apply (rule contlub_Isfst)
-done
-
-lemma cont_Issnd: "cont(Issnd)"
-apply (rule monocontlub2cont)
-apply (rule monofun_Issnd)
-apply (rule contlub_Issnd)
-done
-
-lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
-apply fast
-done
-
-text {* convert all lemmas to the continuous versions *}
-
-lemma beta_cfun_sprod [simp]:
- "(LAM x y. Ispair x y)$a$b = Ispair a b"
-apply (subst beta_cfun)
-apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
-apply (subst beta_cfun)
-apply (rule cont_Ispair2)
-apply (rule refl)
-done
+lemma defined_spair_rev: "(:a, b:) = \<bottom> \<Longrightarrow> a = \<bottom> \<or> b = \<bottom>"
+by (erule contrapos_pp, simp)
lemma inject_spair:
- "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
-apply (unfold spair_def)
-apply (erule inject_Ispair)
-apply assumption
-apply (erule box_equals)
-apply (rule beta_cfun_sprod)
-apply (rule beta_cfun_sprod)
+ "\<lbrakk>aa \<noteq> \<bottom>; ba \<noteq> \<bottom>; (:a,b:) = (:aa,ba:)\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba"
+apply (simp add: spair_Abs_Sprod)
+apply (simp add: Abs_Sprod_inject [OF spair_lemma] Sprod_def)
+apply (case_tac "a = \<bottom>", simp_all)
+apply (case_tac "b = \<bottom>", simp_all)
done
lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
-apply (unfold spair_def)
-apply (rule sym)
-apply (rule trans)
-apply (rule beta_cfun_sprod)
-apply (rule sym)
-apply (rule inst_sprod_pcpo)
-done
+by simp
-lemma strict_spair:
- "(a=UU | b=UU) ==> (:a,b:)=UU"
-apply (unfold spair_def)
-apply (rule trans)
-apply (rule beta_cfun_sprod)
-apply (rule trans)
-apply (rule_tac [2] inst_sprod_pcpo [symmetric])
-apply (erule strict_Ispair)
-done
+subsection {* Properties of @{term sfst} and @{term ssnd} *}
-lemma strict_spair1: "(:UU,b:) = UU"
-apply (unfold spair_def)
-apply (subst beta_cfun_sprod)
-apply (rule trans)
-apply (rule_tac [2] inst_sprod_pcpo [symmetric])
-apply (rule strict_Ispair1)
-done
-
-lemma strict_spair2: "(:a,UU:) = UU"
-apply (unfold spair_def)
-apply (subst beta_cfun_sprod)
-apply (rule trans)
-apply (rule_tac [2] inst_sprod_pcpo [symmetric])
-apply (rule strict_Ispair2)
-done
+lemma strict_sfst [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
+by (simp add: sfst_def cont_Rep_Sprod strict_Rep_Sprod)
-declare strict_spair1 [simp] strict_spair2 [simp]
-
-lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
-apply (unfold spair_def)
-apply (rule strict_Ispair_rev)
-apply auto
-done
+lemma strict_ssnd [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
+by (simp add: ssnd_def cont_Rep_Sprod strict_Rep_Sprod)
-lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)"
-apply (unfold spair_def)
-apply (rule defined_Ispair_rev)
-apply auto
-done
-
-lemma defined_spair [simp]:
- "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
+lemma Rep_Sprod_spair:
+ "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
apply (unfold spair_def)
-apply (subst beta_cfun_sprod)
-apply (subst inst_sprod_pcpo)
-apply (erule defined_Ispair)
-apply assumption
-done
-
-lemma Exh_Sprod2:
- "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
-apply (unfold spair_def)
-apply (rule Exh_Sprod [THEN disjE])
-apply (rule disjI1)
-apply (subst inst_sprod_pcpo)
-apply assumption
-apply (rule disjI2)
-apply (erule exE)
-apply (erule exE)
-apply (rule exI)
-apply (rule exI)
-apply (rule conjI)
-apply (subst beta_cfun_sprod)
-apply fast
-apply fast
-done
-
-lemma sprodE:
-assumes prem1: "p=UU ==> Q"
-assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
-shows "Q"
-apply (rule IsprodE)
-apply (rule prem1)
-apply (subst inst_sprod_pcpo)
-apply assumption
-apply (rule prem2)
-prefer 2 apply (assumption)
-prefer 2 apply (assumption)
-apply (unfold spair_def)
-apply (subst beta_cfun_sprod)
-apply assumption
-done
-
-lemma strict_sfst: "p=UU==>sfst$p=UU"
-apply (unfold sfst_def)
-apply (subst beta_cfun)
-apply (rule cont_Isfst)
-apply (rule strict_Isfst)
-apply (rule inst_sprod_pcpo [THEN subst])
-apply assumption
-done
-
-lemma strict_sfst1 [simp]: "sfst$(:UU,y:) = UU"
-apply (unfold sfst_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (subst beta_cfun)
-apply (rule cont_Isfst)
-apply (rule strict_Isfst1)
+apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
done
-lemma strict_sfst2 [simp]: "sfst$(:x,UU:) = UU"
-apply (unfold sfst_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (subst beta_cfun)
-apply (rule cont_Isfst)
-apply (rule strict_Isfst2)
-done
-
-lemma strict_ssnd: "p=UU==>ssnd$p=UU"
-apply (unfold ssnd_def)
-apply (subst beta_cfun)
-apply (rule cont_Issnd)
-apply (rule strict_Issnd)
-apply (rule inst_sprod_pcpo [THEN subst])
-apply assumption
-done
+lemma sfst2 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
+by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
-lemma strict_ssnd1 [simp]: "ssnd$(:UU,y:) = UU"
-apply (unfold ssnd_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (subst beta_cfun)
-apply (rule cont_Issnd)
-apply (rule strict_Issnd1)
-done
-
-lemma strict_ssnd2 [simp]: "ssnd$(:x,UU:) = UU"
-apply (unfold ssnd_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (subst beta_cfun)
-apply (rule cont_Issnd)
-apply (rule strict_Issnd2)
-done
-
-lemma sfst2 [simp]: "y~=UU ==>sfst$(:x,y:)=x"
-apply (unfold sfst_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (subst beta_cfun)
-apply (rule cont_Isfst)
-apply (erule Isfst2)
-done
+lemma ssnd2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
+by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
-lemma ssnd2 [simp]: "x~=UU ==>ssnd$(:x,y:)=y"
-apply (unfold ssnd_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (subst beta_cfun)
-apply (rule cont_Issnd)
-apply (erule Issnd2)
-done
-
-
-lemma defined_sfstssnd: "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
-apply (unfold sfst_def ssnd_def spair_def)
-apply (simplesubst beta_cfun)
-apply (rule cont_Issnd)
-apply (subst beta_cfun)
-apply (rule cont_Isfst)
-apply (rule defined_IsfstIssnd)
-apply (rule inst_sprod_pcpo [THEN subst])
-apply assumption
-done
+lemma defined_sfstssnd: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
+by (rule_tac p=p in sprodE, simp_all)
-lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
-apply (unfold sfst_def ssnd_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (simplesubst beta_cfun)
-apply (rule cont_Issnd)
-apply (subst beta_cfun)
-apply (rule cont_Isfst)
-apply (rule surjective_pairing_Sprod [symmetric])
-done
+lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
+by (rule_tac p=p in sprodE, simp_all)
-lemma lub_sprod2:
-"chain(S) ==> range(S) <<|
- (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
-apply (unfold sfst_def ssnd_def spair_def)
-apply (subst beta_cfun_sprod)
-apply (simplesubst beta_cfun [THEN ext])
-apply (rule cont_Issnd)
-apply (subst beta_cfun [THEN ext])
-apply (rule cont_Isfst)
-apply (erule lub_sprod)
-done
+subsection {* Properties of @{term ssplit} *}
-lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
-(*
- "chain ?S1 ==>
- lub (range ?S1) =
- (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
-*)
-
-lemma ssplit1 [simp]: "ssplit$f$UU=UU"
+lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
by (simp add: ssplit_def)
-lemma ssplit2 [simp]: "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
+lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:)= f\<cdot>x\<cdot>y"
by (simp add: ssplit_def)
-lemma ssplit3: "ssplit$spair$z=z"
-apply (simp add: ssplit_def)
-apply (simp add: surjective_pairing_Sprod2)
-apply (case_tac "z=UU", simp_all)
-done
-
-text {* install simplifier for Sprod *}
-
-lemmas Sprod_rews = strict_sfst1 strict_sfst2
- strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
- ssplit1 ssplit2
+lemma ssplit3: "ssplit\<cdot>spair\<cdot>z = z"
+by (rule_tac p=z in sprodE, simp_all)
end