# HG changeset patch # User huffman # Date 1287958284 25200 # Node ID 0fb7891f0c7c8458043d1b6fbb6fac1257cb974f # Parent 9dbb01456031f41641c2813316c89708c4064a32# Parent 07445603208a6919079227b2c9de0ced33f62930 merged diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Bifinite.thy Sun Oct 24 15:11:24 2010 -0700 @@ -5,7 +5,7 @@ header {* Bifinite domains *} theory Bifinite -imports Algebraic Cprod Sprod Ssum Up Lift One Tr +imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable begin subsection {* Class of bifinite domains *} diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Cfun.thy Sun Oct 24 15:11:24 2010 -0700 @@ -95,12 +95,6 @@ lemma UU_CFun: "\ \ CFun" by (simp add: CFun_def inst_fun_pcpo) -instance cfun :: (finite_po, finite_po) finite_po -by (rule typedef_finite_po [OF type_definition_CFun]) - -instance cfun :: (finite_po, chfin) chfin -by (rule typedef_chfin [OF type_definition_CFun below_CFun_def]) - instance cfun :: (cpo, discrete_cpo) discrete_cpo by intro_classes (simp add: below_CFun_def Rep_CFun_inject) @@ -550,7 +544,10 @@ lemma strict2 [simp]: "x \ \ \ strict\x = ID" by (simp add: strict_conv_if) - definition +lemma strict3 [simp]: "strict\x\\ = \" +by (simp add: strict_conv_if) + +definition strictify :: "('a \ 'b) \ 'a \ 'b" where "strictify = (\ f x. strict\x\(f\x))" diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Discrete.thy --- a/src/HOLCF/Discrete.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Discrete.thy Sun Oct 24 15:11:24 2010 -0700 @@ -44,22 +44,6 @@ "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}" by (fast elim: discr_chain0) -instance discr :: (finite) finite_po -proof - have "finite (Discr ` (UNIV :: 'a set))" - by (rule finite_imageI [OF finite]) - also have "(Discr ` (UNIV :: 'a set)) = UNIV" - by (auto, case_tac x, auto) - finally show "finite (UNIV :: 'a discr set)" . -qed - -instance discr :: (type) chfin -apply intro_classes -apply (rule_tac x=0 in exI) -apply (unfold max_in_chain_def) -apply (clarify, erule discr_chain0 [symmetric]) -done - subsection {* \emph{undiscr} *} definition diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/FOCUS/Fstream.thy Sun Oct 24 15:11:24 2010 -0700 @@ -42,11 +42,7 @@ lemma Def_maximal: "a = Def d \ a\b \ b = Def d" -apply (rule flat_eq [THEN iffD1, symmetric]) -apply (rule Def_not_UU) -apply (drule antisym_less_inverse) -apply (erule (1) conjunct2 [THEN trans_less]) -done +by simp section "fscons" diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Fun_Cpo.thy --- a/src/HOLCF/Fun_Cpo.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Fun_Cpo.thy Sun Oct 24 15:11:24 2010 -0700 @@ -110,26 +110,6 @@ from Yij Yik show "Y j = Y k" by auto qed -instance "fun" :: (finite, chfin) chfin -proof - fix Y :: "nat \ 'a \ 'b" - let ?n = "\x. LEAST n. max_in_chain n (\i. Y i x)" - assume "chain Y" - hence "\x. chain (\i. Y i x)" - by (rule ch2ch_fun) - hence "\x. \n. max_in_chain n (\i. Y i x)" - by (rule chfin) - hence "\x. max_in_chain (?n x) (\i. Y i x)" - by (rule LeastI_ex) - hence "\x. max_in_chain (Max (range ?n)) (\i. Y i x)" - by (rule maxinch_mono [OF _ Max_ge], simp_all) - hence "max_in_chain (Max (range ?n)) Y" - by (rule maxinch2maxinch_lambda) - thus "\n. max_in_chain n Y" .. -qed - -instance "fun" :: (finite, finite_po) finite_po .. - instance "fun" :: (type, discrete_cpo) discrete_cpo proof fix f g :: "'a \ 'b" diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Library/Sum_Cpo.thy --- a/src/HOLCF/Library/Sum_Cpo.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Library/Sum_Cpo.thy Sun Oct 24 15:11:24 2010 -0700 @@ -213,8 +213,6 @@ apply (case_tac "\i. Y i", simp_all) done -instance sum :: (finite_po, finite_po) finite_po .. - instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo by intro_classes (simp add: below_sum_def split: sum.split) diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Lift.thy Sun Oct 24 15:11:24 2010 -0700 @@ -5,17 +5,14 @@ header {* Lifting types of class type to flat pcpo's *} theory Lift -imports Discrete Up Countable +imports Discrete Up begin default_sort type -pcpodef 'a lift = "UNIV :: 'a discr u set" +pcpodef (open) 'a lift = "UNIV :: 'a discr u set" by simp_all -instance lift :: (finite) finite_po -by (rule typedef_finite_po [OF type_definition_lift]) - lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] definition @@ -33,7 +30,7 @@ done rep_datatype "\\'a lift" Def - by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) + by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo) lemmas lift_distinct1 = lift.distinct(1) lemmas lift_distinct2 = lift.distinct(2) @@ -65,7 +62,7 @@ by simp lemma Def_below_Def: "Def x \ Def y \ x = y" -by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def) +by (simp add: below_lift_def Def_def Abs_lift_inverse) lemma Def_below_iff [simp]: "Def x \ y \ Def x = y" by (induct y, simp, simp add: Def_below_Def) @@ -80,6 +77,18 @@ by (induct x) auto qed +subsection {* Continuity of @{const lift_case} *} + +lemma lift_case_eq: "lift_case \ f x = fup\(\ y. f (undiscr y))\(Rep_lift x)" +apply (induct x, unfold lift.cases) +apply (simp add: Rep_lift_strict) +apply (simp add: Def_def Abs_lift_inverse) +done + +lemma cont2cont_lift_case [simp]: + "\\y. cont (\x. f x y); cont g\ \ cont (\x. lift_case \ (f x) (g x))" +unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose]) + subsection {* Further operations *} definition @@ -90,59 +99,14 @@ flift2 :: "('a \ 'b) \ ('a lift \ 'b lift)" where "flift2 f = (FLIFT x. Def (f x))" -subsection {* Continuity Proofs for flift1, flift2 *} - -text {* Need the instance of @{text flat}. *} - -lemma cont_lift_case1: "cont (\f. lift_case a f x)" -apply (induct x) -apply simp -apply simp -apply (rule cont_id [THEN cont2cont_fun]) -done - -lemma cont_lift_case2: "cont (\x. lift_case \ f x)" -apply (rule flatdom_strict2cont) -apply simp -done - -lemma cont_flift1: "cont flift1" -unfolding flift1_def -apply (rule cont2cont_LAM) -apply (rule cont_lift_case2) -apply (rule cont_lift_case1) -done - -lemma FLIFT_mono: - "(\x. f x \ g x) \ (FLIFT x. f x) \ (FLIFT x. g x)" -apply (rule monofunE [where f=flift1]) -apply (rule cont2mono [OF cont_flift1]) -apply (simp add: fun_below_iff) -done - -lemma cont2cont_flift1 [simp, cont2cont]: - "\\y. cont (\x. f x y)\ \ cont (\x. FLIFT y. f x y)" -apply (rule cont_flift1 [THEN cont_compose]) -apply simp -done - -lemma cont2cont_lift_case [simp]: - "\\y. cont (\x. f x y); cont g\ \ cont (\x. lift_case UU (f x) (g x))" -apply (subgoal_tac "cont (\x. (FLIFT y. f x y)\(g x))") -apply (simp add: flift1_def cont_lift_case2) -apply simp -done - -text {* rewrites for @{term flift1}, @{term flift2} *} - lemma flift1_Def [simp]: "flift1 f\(Def x) = (f x)" -by (simp add: flift1_def cont_lift_case2) +by (simp add: flift1_def) lemma flift2_Def [simp]: "flift2 f\(Def x) = Def (f x)" by (simp add: flift2_def) lemma flift1_strict [simp]: "flift1 f\\ = \" -by (simp add: flift1_def cont_lift_case2) +by (simp add: flift1_def) lemma flift2_strict [simp]: "flift2 f\\ = \" by (simp add: flift2_def) @@ -153,4 +117,12 @@ lemma flift2_defined_iff [simp]: "(flift2 f\x = \) = (x = \)" by (cases x, simp_all) +lemma FLIFT_mono: + "(\x. f x \ g x) \ (FLIFT x. f x) \ (FLIFT x. g x)" +by (rule cfun_belowI, case_tac x, simp_all) + +lemma cont2cont_flift1 [simp, cont2cont]: + "\\y. cont (\x. f x y)\ \ cont (\x. FLIFT y. f x y)" +by (simp add: flift1_def cont2cont_LAM) + end diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Pcpo.thy --- a/src/HOLCF/Pcpo.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Pcpo.thy Sun Oct 24 15:11:24 2010 -0700 @@ -262,18 +262,6 @@ end -class finite_po = finite + po -begin - -subclass chfin -apply default -apply (drule finite_range_imp_finch) -apply (rule finite) -apply (simp add: finite_chain_def) -done - -end - class flat = pcpo + assumes ax_flat: "x \ y \ x = \ \ x = y" begin @@ -299,7 +287,7 @@ end -text {* Discrete cpos *} +subsection {* Discrete cpos *} class discrete_cpo = below + assumes discrete_cpo [simp]: "x \ y \ x = y" @@ -320,14 +308,14 @@ thus "S i = S 0" by (rule sym) qed -subclass cpo +subclass chfin proof fix S :: "nat \ 'a" assume S: "chain S" - hence "\x. S = (\i. x)" - by (rule discrete_chain_const) - thus "\x. range S <<| x" - by (fast intro: lub_const) + hence "\x. S = (\i. x)" by (rule discrete_chain_const) + hence "max_in_chain 0 S" + unfolding max_in_chain_def by auto + thus "\i. max_in_chain i S" .. qed end diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Pcpodef.thy --- a/src/HOLCF/Pcpodef.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Pcpodef.thy Sun Oct 24 15:11:24 2010 -0700 @@ -46,15 +46,6 @@ by (simp only: type_definition.Abs_image [OF type]) qed -theorem typedef_finite_po: - fixes Abs :: "'a::finite_po \ 'b::po" - assumes type: "type_definition Rep Abs A" - shows "OFCLASS('b, finite_po_class)" - apply (intro_classes) - apply (rule typedef_finite_UNIV [OF type]) - apply (rule finite) -done - subsection {* Proving a subtype is chain-finite *} lemma ch2ch_Rep: diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Product_Cpo.thy --- a/src/HOLCF/Product_Cpo.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Product_Cpo.thy Sun Oct 24 15:11:24 2010 -0700 @@ -12,19 +12,16 @@ subsection {* Unit type is a pcpo *} -instantiation unit :: below +instantiation unit :: discrete_cpo begin definition below_unit_def [simp]: "x \ (y::unit) \ True" -instance .. -end +instance proof +qed simp -instance unit :: discrete_cpo -by intro_classes simp - -instance unit :: finite_po .. +end instance unit :: pcpo by intro_classes simp @@ -157,8 +154,6 @@ thus "\x. range S <<| x" .. qed -instance prod :: (finite_po, finite_po) finite_po .. - instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo proof fix x y :: "'a \ 'b" diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Sprod.thy Sun Oct 24 15:11:24 2010 -0700 @@ -12,37 +12,31 @@ subsection {* Definition of strict product type *} -pcpodef (Sprod) ('a, 'b) sprod (infixr "**" 20) = +pcpodef ('a, 'b) sprod (infixr "**" 20) = "{p::'a \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" by simp_all -instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po -by (rule typedef_finite_po [OF type_definition_Sprod]) - instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin -by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def]) +by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) type_notation (xsymbols) sprod ("(_ \/ _)" [21,20] 20) type_notation (HTML output) sprod ("(_ \/ _)" [21,20] 20) -lemma spair_lemma: "(strict\b\a, strict\a\b) \ Sprod" -by (simp add: Sprod_def strict_conv_if) - subsection {* Definitions of constants *} definition sfst :: "('a ** 'b) \ 'a" where - "sfst = (\ p. fst (Rep_Sprod p))" + "sfst = (\ p. fst (Rep_sprod p))" definition ssnd :: "('a ** 'b) \ 'b" where - "ssnd = (\ p. snd (Rep_Sprod p))" + "ssnd = (\ p. snd (Rep_sprod p))" definition spair :: "'a \ 'b \ ('a ** 'b)" where - "spair = (\ a b. Abs_Sprod (strict\b\a, strict\a\b))" + "spair = (\ a b. Abs_sprod (strict\b\a, strict\a\b))" definition ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" where @@ -59,28 +53,20 @@ subsection {* Case analysis *} -lemma Rep_Sprod_spair: - "Rep_Sprod (:a, b:) = (strict\b\a, strict\a\b)" -unfolding spair_def -by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma) - -lemmas Rep_Sprod_simps = - Rep_Sprod_inject [symmetric] below_Sprod_def - Rep_Sprod_strict Rep_Sprod_spair +lemma spair_sprod: "(strict\b\a, strict\a\b) \ sprod" +by (simp add: sprod_def strict_conv_if) -lemma Exh_Sprod: - "z = \ \ (\a b. z = (:a, b:) \ a \ \ \ b \ \)" -apply (insert Rep_Sprod [of z]) -apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq) -apply (simp add: Sprod_def) -apply (erule disjE, simp) -apply (simp add: strict_conv_if) -apply fast -done +lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\b\a, strict\a\b)" +by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) + +lemmas Rep_sprod_simps = + Rep_sprod_inject [symmetric] below_sprod_def + Pair_fst_snd_eq below_prod_def + Rep_sprod_strict Rep_sprod_spair lemma sprodE [case_names bottom spair, cases type: sprod]: - "\p = \ \ Q; \x y. \p = (:x, y:); x \ \; y \ \\ \ Q\ \ Q" -using Exh_Sprod [of p] by auto + obtains "p = \" | x y where "p = (:x, y:)" and "x \ \" and "y \ \" +using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps) lemma sprod_induct [case_names bottom spair, induct type: sprod]: "\P \; \x y. \x \ \; y \ \\ \ P (:x, y:)\ \ P x" @@ -89,22 +75,22 @@ subsection {* Properties of \emph{spair} *} lemma spair_strict1 [simp]: "(:\, y:) = \" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps) lemma spair_strict2 [simp]: "(:x, \:) = \" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps) lemma spair_strict_iff [simp]: "((:x, y:) = \) = (x = \ \ y = \)" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps strict_conv_if) lemma spair_below_iff: "((:a, b:) \ (:c, d:)) = (a = \ \ b = \ \ (a \ c \ b \ d))" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps strict_conv_if) lemma spair_eq_iff: "((:a, b:) = (:c, d:)) = (a = c \ b = d \ (a = \ \ b = \) \ (c = \ \ d = \))" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps strict_conv_if) lemma spair_strict: "x = \ \ y = \ \ (:x, y:) = \" by simp @@ -118,6 +104,10 @@ lemma spair_defined_rev: "(:x, y:) = \ \ x = \ \ y = \" by simp +lemma spair_below: + "\x \ \; y \ \\ \ (:x, y:) \ (:a, b:) = (x \ a \ y \ b)" +by (simp add: spair_below_iff) + lemma spair_eq: "\x \ \; y \ \\ \ ((:x, y:) = (:a, b:)) = (x = a \ y = b)" by (simp add: spair_eq_iff) @@ -135,16 +125,16 @@ subsection {* Properties of \emph{sfst} and \emph{ssnd} *} lemma sfst_strict [simp]: "sfst\\ = \" -by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict) +by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict) lemma ssnd_strict [simp]: "ssnd\\ = \" -by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict) +by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict) lemma sfst_spair [simp]: "y \ \ \ sfst\(:x, y:) = x" -by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair) +by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair) lemma ssnd_spair [simp]: "x \ \ \ ssnd\(:x, y:) = y" -by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair) +by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair) lemma sfst_defined_iff [simp]: "(sfst\p = \) = (p = \)" by (cases p, simp_all) @@ -158,24 +148,15 @@ lemma ssnd_defined: "p \ \ \ ssnd\p \ \" by simp -lemma surjective_pairing_Sprod2: "(:sfst\p, ssnd\p:) = p" +lemma spair_sfst_ssnd: "(:sfst\p, ssnd\p:) = p" by (cases p, simp_all) lemma below_sprod: "x \ y = (sfst\x \ sfst\y \ ssnd\x \ ssnd\y)" -apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod) -apply (simp only: below_prod_def) -done +by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod) lemma eq_sprod: "(x = y) = (sfst\x = sfst\y \ ssnd\x = ssnd\y)" by (auto simp add: po_eq_conv below_sprod) -lemma spair_below: - "\x \ \; y \ \\ \ (:x, y:) \ (:a, b:) = (x \ a \ y \ b)" -apply (cases "a = \", simp) -apply (cases "b = \", simp) -apply (simp add: below_sprod) -done - lemma sfst_below_iff: "sfst\x \ y = x \ (:y, ssnd\x:)" apply (cases "x = \", simp, cases "y = \", simp) apply (simp add: below_sprod) @@ -195,7 +176,7 @@ by (rule compactI, simp add: ssnd_below_iff) lemma compact_spair: "\compact x; compact y\ \ compact (:x, y:)" -by (rule compact_Sprod, simp add: Rep_Sprod_spair strict_conv_if) +by (rule compact_sprod, simp add: Rep_sprod_spair strict_conv_if) lemma compact_spair_iff: "compact (:x, y:) = (x = \ \ y = \ \ (compact x \ compact y))" diff -r 07445603208a -r 0fb7891f0c7c src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Sun Oct 24 21:25:13 2010 +0200 +++ b/src/HOLCF/Ssum.thy Sun Oct 24 15:11:24 2010 -0700 @@ -12,17 +12,14 @@ subsection {* Definition of strict sum type *} -pcpodef (Ssum) ('a, 'b) ssum (infixr "++" 10) = - "{p :: tr \ ('a \ 'b). - (fst p \ TT \ snd (snd p) = \) \ - (fst p \ FF \ fst (snd p) = \)}" +pcpodef ('a, 'b) ssum (infixr "++" 10) = + "{p :: tr \ ('a \ 'b). p = \ \ + (fst p = TT \ fst (snd p) \ \ \ snd (snd p) = \) \ + (fst p = FF \ fst (snd p) = \ \ snd (snd p) \ \) }" by simp_all -instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po -by (rule typedef_finite_po [OF type_definition_Ssum]) - instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin -by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def]) +by (rule typedef_chfin [OF type_definition_ssum below_ssum_def]) type_notation (xsymbols) ssum ("(_ \/ _)" [21, 20] 20) @@ -34,45 +31,44 @@ definition sinl :: "'a \ ('a ++ 'b)" where - "sinl = (\ a. Abs_Ssum (strict\a\TT, a, \))" + "sinl = (\ a. Abs_ssum (strict\a\TT, a, \))" definition sinr :: "'b \ ('a ++ 'b)" where - "sinr = (\ b. Abs_Ssum (strict\b\FF, \, b))" + "sinr = (\ b. Abs_ssum (strict\b\FF, \, b))" -lemma sinl_Ssum: "(strict\a\TT, a, \) \ Ssum" -by (simp add: Ssum_def strict_conv_if) +lemma sinl_ssum: "(strict\a\TT, a, \) \ ssum" +by (simp add: ssum_def strict_conv_if) -lemma sinr_Ssum: "(strict\b\FF, \, b) \ Ssum" -by (simp add: Ssum_def strict_conv_if) +lemma sinr_ssum: "(strict\b\FF, \, b) \ ssum" +by (simp add: ssum_def strict_conv_if) -lemma sinl_Abs_Ssum: "sinl\a = Abs_Ssum (strict\a\TT, a, \)" -by (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum) - -lemma sinr_Abs_Ssum: "sinr\b = Abs_Ssum (strict\b\FF, \, b)" -by (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum) +lemma Rep_ssum_sinl: "Rep_ssum (sinl\a) = (strict\a\TT, a, \)" +by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum) -lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\a) = (strict\a\TT, a, \