(*<*) theory Theory_Of_Lists imports HOLCF_ROOT begin (*>*) section‹ Strict lists \label{sec:theory_of_lists} › text‹ Head- and tail-strict lists. Many technical Isabelle details are lifted from ‹HOLCF-Prelude.Data_List›; names follow HOL, prefixed with ‹s›. › domain 'a slist ("[:_:]") = snil ("[::]") | scons (shead :: "'a") (stail :: "'a slist") (infixr ":#" 65) lemma scons_strict[simp]: "scons⋅⊥ = ⊥" by (clarsimp simp: cfun_eq_iff) lemma shead_bottom_iff[simp]: "(shead⋅xs = ⊥) ⟷ (xs = ⊥ ∨ xs = [::])" by (cases xs) simp_all lemma stail_bottom_iff[simp]: "(stail⋅xs = ⊥) ⟷ (xs = ⊥ ∨ xs = [::])" by (cases xs) simp_all lemma match_snil_match_scons_slist_case: "match_snil⋅xs⋅k1 +++ match_scons⋅xs⋅k2 = slist_case⋅k1⋅k2⋅xs" by (cases xs) simp_all lemma slist_bottom': "slist_case⋅⊥⋅⊥⋅xs = ⊥" by (cases xs; simp) lemma slist_bottom[simp]: "slist_case⋅⊥⋅⊥ = ⊥" by (simp add: cfun_eq_iff slist_bottom') lemma slist_case_distr: "f⋅⊥ = ⊥ ⟹ f⋅(slist_case⋅g⋅h⋅xs) = slist_case⋅(f⋅g)⋅(Λ x xs. f⋅(h⋅x⋅xs))⋅xs" "slist_case⋅g'⋅h'⋅xs⋅z = slist_case⋅(g'⋅z)⋅(Λ x xs. h'⋅x⋅xs⋅z)⋅xs" by (case_tac [!] xs) simp_all lemma slist_case_cong: assumes "xs = xs'" assumes "xs' = [::] ⟹ n = n'" assumes "⋀y ys. ⟦xs' = y :# ys; y ≠ ⊥; ys ≠ ⊥⟧ ⟹ c y ys = c' y ys" assumes "cont (λ(x, y). c x y)" assumes "cont (λ(x, y). c' x y)" shows "slist_case⋅n⋅(Λ x xs. c x xs)⋅xs = slist_case⋅n'⋅(Λ x xs. c' x xs)⋅xs'" using assms by (cases xs; cases xs'; clarsimp simp: prod_cont_iff) text‹ Section syntax for @{const ‹scons›} ala Haskell. › syntax "_scons_section" :: "'a → [:'a:] → [:'a:]" ("'(:#')") "_scons_section_left" :: "'a ⇒ [:'a:] → [:'a:]" ("'(_:#')") translations "(x:#)" == "(CONST Rep_cfun) (CONST scons) x" abbreviation scons_section_right :: "[:'a:] ⇒ 'a → [:'a:]" ("'(:#_')") where "(:#xs) ≡ Λ x. x :# xs" syntax "_strict_list" :: "args ⇒ [:'a:]" ("[:(_):]") translations "[:x, xs:]" == "x :# [:xs:]" "[:x:]" == "x :# [::]" text‹ Class instances. › instantiation slist :: (Eq) Eq_strict begin fixrec eq_slist :: "[:'a:] → [:'a:] → tr" where "eq_slist⋅[::]⋅[::] = TT" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ eq_slist⋅(x :# xs)⋅[::] = FF" | "⟦y ≠ ⊥; ys ≠ ⊥⟧ ⟹ eq_slist⋅[::]⋅(y :# ys) = FF" | "⟦x ≠ ⊥; xs ≠ ⊥; y ≠ ⊥; ys ≠ ⊥⟧ ⟹ eq_slist⋅(x :# xs)⋅(y :# ys) = (eq⋅x⋅y andalso eq_slist⋅xs⋅ys)" instance proof fix xs :: "[:'a:]" show "eq⋅xs⋅⊥ = ⊥" by (cases xs) (subst eq_slist.unfold; simp)+ show "eq⋅⊥⋅xs = ⊥" by (cases xs) (subst eq_slist.unfold; simp)+ qed end instance slist :: (Eq_sym) Eq_sym proof fix xs ys :: "[:'a:]" show "eq⋅xs⋅ys = eq⋅ys⋅xs" proof (induct xs arbitrary: ys) case snil show ?case by (cases ys; simp) next case scons then show ?case by (cases ys; simp add: eq_sym) qed simp_all qed instance slist :: (Eq_equiv) Eq_equiv proof fix xs ys zs :: "[:'a:]" show "eq⋅xs⋅xs ≠ FF" by (induct xs) simp_all assume "eq⋅xs⋅ys = TT" and "eq⋅ys⋅zs = TT" then show "eq⋅xs⋅zs = TT" proof (induct xs arbitrary: ys zs) case (snil ys zs) then show ?case by (cases ys, simp_all) next case (scons x xs ys zs) with eq_trans show ?case by (cases ys; cases zs) auto qed simp_all qed instance slist :: (Eq_eq) Eq_eq proof fix xs ys :: "[:'a:]" show "eq⋅xs⋅xs ≠ FF" by (induct xs) simp_all assume "eq⋅xs⋅ys = TT" then show "xs = ys" proof (induct xs arbitrary: ys) case (snil ys) then show ?case by (cases ys) simp_all next case (scons x xs ys) then show ?case by (cases ys) auto qed simp qed instance slist :: (Eq_def) Eq_def proof fix xs ys :: "[:'a:]" assume "xs ≠ ⊥" and "ys ≠ ⊥" then show "eq⋅xs⋅ys ≠ ⊥" proof(induct xs arbitrary: ys) case (snil ys) then show ?case by (cases ys) simp_all next case (scons a xs) then show ?case by (cases ys) simp_all qed simp qed lemma slist_eq_TT_snil[simp]: fixes xs :: "[:'a::Eq:]" shows "(eq⋅xs⋅[::] = TT) ⟷ (xs = [::])" "(eq⋅[::]⋅xs = TT) ⟷ (xs = [::])" by (cases xs; simp)+ lemma slist_eq_FF_snil[simp]: fixes xs :: "[:'a::Eq:]" shows "(eq⋅xs⋅[::] = FF) ⟷ (∃y ys. y ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs = y :# ys)" "(eq⋅[::]⋅xs = FF) ⟷ (∃y ys. y ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs = y :# ys)" by (cases xs; force)+ subsection‹ Some of the usual reasoning infrastructure › inductive slistmem :: "'a ⇒ [:'a:] ⇒ bool" where "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ slistmem x (x :# xs)" | "⟦slistmem x xs; y ≠ ⊥⟧ ⟹ slistmem x (y :# xs)" lemma slistmem_bottom1[iff]: fixes x :: "'a" shows "¬ slistmem x ⊥" by rule (induct x "⊥::[:'a:]" rule: slistmem.induct; fastforce) lemma slistmem_bottom2[iff]: fixes xs :: "[:'a:]" shows "¬ slistmem ⊥ xs" by rule (induct "⊥::'a" xs rule: slistmem.induct; fastforce) lemma slistmem_nil[iff]: shows "¬ slistmem x [::]" by (fastforce elim: slistmem.cases) lemma slistmem_scons[simp]: shows "slistmem x (y :# ys) ⟷ (x = y ∧ x ≠ ⊥ ∧ ys ≠ ⊥) ∨ (slistmem x ys ∧ y ≠ ⊥)" proof - have "x = y ∨ slistmem x ys" if "slistmem x (y :# ys)" using that by (induct "x" "y :# ys" arbitrary: y ys rule: slistmem.induct; force) then show ?thesis by (auto elim: slistmem.cases intro: slistmem.intros) qed definition sset :: "[:'a:] ⇒ 'a set" where "sset xs = {x. slistmem x xs}" lemma sset_simp[simp]: shows "sset ⊥ = {}" and "sset [::] = {}" and "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sset (x :# xs) = insert x (sset xs)" unfolding sset_def by (auto elim: slistmem.cases intro: slistmem.intros) lemma sset_defined[simp]: assumes "x ∈ sset xs" shows "x ≠ ⊥" using assms sset_def by force lemma sset_below: assumes "y ∈ sset ys" assumes "xs ⊑ ys" assumes "xs ≠ ⊥" obtains x where "x ∈ sset xs" and "x ⊑ y" using assms proof(induct ys arbitrary: xs) case (scons y ys xs) then show ?case by (cases xs) auto qed simp_all subsection‹ Some of the usual operations › text‹ A variety of functions on lists. Drawn from \<^citet>‹"Bird:1987"›, @{theory ‹HOL.List›} and @{theory ‹HOLCF-Prelude.Data_List›}. The definitions vary because, for instance, the strictness of some of those in @{theory ‹HOLCF-Prelude.Data_List›} correspond neither to those in Haskell nor Bird's expectations (specifically ‹stails›, ‹inits›, ‹sscanl›). › fixrec snull :: "[:'a:] → tr" where "snull⋅[::] = TT" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ snull⋅(x :# xs) = FF" lemma snull_strict[simp]: "snull⋅⊥ = ⊥" by fixrec_simp lemma snull_bottom_iff[simp]: "(snull⋅xs = ⊥) ⟷ (xs = ⊥)" by (cases xs) simp_all lemma snull_FF_conv: "(snull⋅xxs = FF) ⟷ (∃x xs. xxs ≠ ⊥ ∧ xxs = x :# xs)" by (cases xxs) simp_all lemma snull_TT_conv[simp]: "(snull⋅xs = TT) ⟷ (xs = [::])" by (cases xs) simp_all lemma snull_eq_snil: "snull⋅xs = eq⋅xs⋅[::]" by (cases xs) simp_all fixrec smap :: "('a → 'b) → [:'a:] → [:'b:]" where "smap⋅f⋅[::] = [::]" | "⟦x ≠⊥; xs ≠ ⊥⟧ ⟹ smap⋅f⋅(x :# xs) = f⋅x :# smap⋅f⋅xs" lemma smap_strict[simp]: "smap⋅f⋅⊥ = ⊥" by fixrec_simp lemma smap_bottom_iff[simp]: "(smap⋅f⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (∃x∈sset xs. f⋅x = ⊥))" by (induct xs) simp_all lemma smap_is_snil_conv[simp]: "(smap⋅f⋅xs = [::]) ⟷ (xs = [::])" "( [::] = smap⋅f⋅xs) ⟷ (xs = [::])" by (cases xs; simp)+ lemma smap_strict_scons[simp]: assumes "f⋅⊥ = ⊥" shows "smap⋅f⋅(x :# xs) = f⋅x :# smap⋅f⋅xs" using assms by (cases "x :# xs = ⊥"; fastforce) lemma smap_ID': "smap⋅ID⋅xs = xs" by (induct xs) simp_all lemma smap_ID[simp]: "smap⋅ID = ID" by (clarsimp simp: cfun_eq_iff smap_ID') lemma smap_cong: assumes "xs = xs'" assumes "⋀x. x ∈ sset xs ⟹ f⋅x = f'⋅x" shows "smap⋅f⋅xs = smap⋅f'⋅xs'" using assms by (induct xs arbitrary: xs') auto lemma smap_smap'[simp]: assumes "f⋅⊥ = ⊥" shows "smap⋅f⋅(smap⋅g⋅xs) = smap⋅(f oo g)⋅xs" using assms by (induct xs) simp_all lemma smap_smap[simp]: assumes "f⋅⊥ = ⊥" shows "smap⋅f oo smap⋅g = smap⋅(f oo g)" using assms by (clarsimp simp: cfun_eq_iff) lemma sset_smap[simp]: assumes "⋀x. x ∈ sset xs ⟹ f⋅x ≠ ⊥" shows "sset (smap⋅f⋅xs) = { f⋅x | x. x ∈ sset xs }" using assms by (induct xs) auto lemma shead_smap_distr: assumes "f⋅⊥ = ⊥" assumes "⋀x. x∈sset xs ⟹ f⋅x ≠ ⊥" shows "shead⋅(smap⋅f⋅xs) = f⋅(shead⋅xs)" using assms by (induct xs) simp_all fixrec sappend :: "[:'a:] → [:'a:] → [:'a:]" where "sappend⋅[::]⋅ys = ys" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sappend⋅(x :# xs)⋅ys = x :# sappend⋅xs⋅ys" abbreviation sappend_syn :: "'a slist ⇒ 'a slist ⇒ 'a slist" (infixr ":@" 65) where "xs :@ ys ≡ sappend⋅xs⋅ys" lemma sappend_strict[simp]: "sappend⋅⊥ = ⊥" by fixrec_simp lemma sappend_strict2[simp]: "xs :@ ⊥ = ⊥" by (induct xs) simp_all lemma sappend_bottom_iff[simp]: "(xs :@ ys = ⊥) ⟷ (xs = ⊥ ∨ ys = ⊥)" by (induct xs) simp_all lemma sappend_scons[simp]: "(x :# xs) :@ ys = x :# xs :@ ys" by (cases "x :# xs = ⊥"; fastforce) lemma sappend_assoc[simp]: "(xs :@ ys) :@ zs = xs :@ (ys :@ zs)" by (induct xs) simp_all lemma sappend_snil_id_left[simp]: "sappend⋅[::] = ID" by (simp add: cfun_eq_iff) lemma sappend_snil_id_right[iff]: "xs :@ [::] = xs" by (induct xs) simp_all lemma snil_append_iff[iff]: "xs :@ ys = [::] ⟷ xs = [::] ∧ ys = [::]" by (induct xs) simp_all lemma smap_sappend[simp]: "smap⋅f⋅(xs :@ ys) = smap⋅f⋅xs :@ smap⋅f⋅ys" by (induct xs; cases "ys = ⊥"; simp) lemma stail_sappend: "stail⋅(xs :@ ys) = (case xs of [::] ⇒ stail⋅ys | z :# zs ⇒ zs :@ ys)" by (induct xs) simp_all lemma stail_append2[simp]: "xs ≠ [::] ⟹ stail⋅(xs :@ ys) = stail⋅xs :@ ys" by (induct xs) simp_all lemma slist_case_snoc: "g⋅⊥⋅⊥ = ⊥ ⟹ slist_case⋅f⋅g⋅(xs :@ [:x:]) = g⋅(shead⋅(xs :@ [:x:]))⋅(stail⋅(xs :@ [:x:]))" by (cases "x = ⊥"; cases xs; clarsimp) fixrec sall :: "('a → tr) → [:'a:] → tr" where "sall⋅p⋅[::] = TT" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sall⋅p⋅(x :# xs) = (p⋅x andalso sall⋅p⋅xs)" lemma sall_strict[simp]: "sall⋅p⋅⊥ = ⊥" by fixrec_simp lemma sall_const_TT[simp]: assumes "xs ≠ ⊥" shows "sall⋅(Λ x. TT)⋅xs = TT" using assms by (induct xs) simp_all lemma sall_const_TT_conv[simp]: "(sall⋅(Λ x. TT)⋅xs = TT) ⟷ (xs ≠ ⊥)" by auto lemma sall_TT[simp]: "(sall⋅p⋅xs = TT) ⟷ (xs ≠ ⊥ ∧ (∀x∈sset xs. p⋅x = TT))" by (induct xs) simp_all fixrec sfilter :: "('a → tr) → [:'a:] → [:'a:]" where "sfilter⋅p⋅[::] = [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sfilter⋅p⋅(x :# xs) = If p⋅x then x :# sfilter⋅p⋅xs else sfilter⋅p⋅xs" lemma sfilter_strict[simp]: "sfilter⋅p⋅⊥ = ⊥" by fixrec_simp lemma sfilter_bottom_iff[simp]: "(sfilter⋅p⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (∃x∈sset xs. p⋅x = ⊥))" by (induct xs) (use trE in auto) lemma sset_sfilter[simp]: assumes "⋀x. x ∈ sset xs ⟹ p⋅x ≠ ⊥" shows "sset (sfilter⋅p⋅xs) = {x |x. x ∈ sset xs ∧ p⋅x = TT}" using assms by (induct xs) (fastforce simp: If2_def[symmetric] split: If2_splits)+ lemma sfilter_strict_scons[simp]: assumes "p⋅⊥ = ⊥" shows "sfilter⋅p⋅(x :# xs) = If p⋅x then x :# sfilter⋅p⋅xs else sfilter⋅p⋅xs" using assms by (cases "x = ⊥"; cases "xs = ⊥"; simp) lemma sfilter_scons_let: assumes "p⋅⊥ = ⊥" shows "sfilter⋅p⋅(x :# xs) = (let xs' = sfilter⋅p⋅xs in If p⋅x then x :# xs' else xs')" unfolding Let_def using assms by simp lemma sfilter_sappend[simp]: "sfilter⋅p⋅(xs :@ ys) = sfilter⋅p⋅xs :@ sfilter⋅p⋅ys" by (cases "ys"; clarsimp) (induct xs; fastforce simp: If2_def[symmetric] split: If2_splits) lemma sfilter_const_FF[simp]: assumes "xs ≠ ⊥" shows "sfilter⋅(Λ x. FF)⋅xs = [::]" using assms by (induct xs) simp_all lemma sfilter_const_FF_conv[simp]: "(sfilter⋅(Λ x. FF)⋅xs = [::]) ⟷ (xs ≠ ⊥)" by auto lemma sfilter_const_TT[simp]: "sfilter⋅(Λ x. TT)⋅xs = xs" by (induct xs) simp_all lemma sfilter_cong: assumes "xs = xs'" assumes "⋀x. x ∈ sset xs ⟹ p⋅x = p'⋅x" shows "sfilter⋅p⋅xs = sfilter⋅p'⋅xs'" using assms by (induct xs arbitrary: xs') auto lemma sfilter_snil_conv[simp]: "sfilter⋅p⋅xs = [::] ⟷ sall⋅(neg oo p)⋅xs = TT" by (induct xs; force simp: If2_def[symmetric] split: If2_splits) lemma sfilter_sfilter': "sfilter⋅p⋅(sfilter⋅q⋅xs) = sfilter⋅(Λ x. q⋅x andalso p⋅x)⋅xs" proof(induct xs) case (scons x xs) from scons(1, 2) show ?case by (cases "sfilter⋅q⋅xs = ⊥") (simp_all add: If_distr If_andalso scons(3)[symmetric] del: sfilter_bottom_iff) qed simp_all lemma sfilter_sfilter: "sfilter⋅p oo sfilter⋅q = sfilter⋅(Λ x. q⋅x andalso p⋅x)" by (clarsimp simp: cfun_eq_iff sfilter_sfilter') lemma sfilter_smap': assumes "p⋅⊥ = ⊥" shows "sfilter⋅p⋅(smap⋅f⋅xs) = smap⋅f⋅(sfilter⋅(p oo f)⋅xs)" using assms by (induct xs; simp add: If2_def[symmetric] split: If2_splits) (metis slist.con_rews(2) smap.simps(2) smap_strict) lemma sfilter_smap: assumes "p⋅⊥ = ⊥" shows "sfilter⋅p oo smap⋅f = smap⋅f oo sfilter⋅(p oo f)" using assms by (clarsimp simp: cfun_eq_iff sfilter_smap') fixrec sfoldl :: "('a::pcpo → 'b::domain → 'a) → 'a → [:'b:] → 'a" where "sfoldl⋅f⋅z⋅[::] = z" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sfoldl⋅f⋅z⋅(x :# xs) = sfoldl⋅f⋅(f⋅z⋅x)⋅xs" lemma sfoldl_strict[simp]: "sfoldl⋅f⋅z⋅⊥ = ⊥" by fixrec_simp lemma sfoldl_strict_f[simp]: assumes "f⋅⊥ = ⊥" shows "sfoldl⋅f⋅⊥⋅xs = ⊥" using assms by (induct xs) simp_all lemma sfoldl_cong: assumes "xs = xs'" assumes "z = z'" assumes "⋀x z. x ∈ sset xs ⟹ f⋅z⋅x = f'⋅z⋅x" shows "sfoldl⋅f⋅z⋅xs = sfoldl⋅f'⋅z'⋅xs'" using assms by (induct xs arbitrary: xs' z z') auto lemma sfoldl_sappend[simp]: assumes "f⋅⊥ = ⊥" shows "sfoldl⋅f⋅z⋅(xs :@ ys) = sfoldl⋅f⋅(sfoldl⋅f⋅z⋅xs)⋅ys" using assms by (cases "ys = ⊥", force) (induct xs arbitrary: z; simp) fixrec sfoldr :: "('b → 'a::pcpo → 'a) → 'a → [:'b:] → 'a" where "sfoldr⋅f⋅z⋅[::] = z" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sfoldr⋅f⋅z⋅(x :# xs) = f⋅x⋅(sfoldr⋅f⋅z⋅xs)" lemma sfoldr_strict[simp]: "sfoldr⋅f⋅z⋅⊥ = ⊥" by fixrec_simp fixrec sconcat :: "[:[:'a:]:] → [:'a:]" where "sconcat⋅[::] = [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sconcat⋅(x :# xs) = x :@ sconcat⋅xs" lemma sconcat_strict[simp]: "sconcat⋅⊥ = ⊥" by fixrec_simp lemma sconcat_scons[simp]: shows "sconcat⋅(x :# xs) = x :@ sconcat⋅xs" by (cases "x = ⊥", force) (induct xs; fastforce) lemma sconcat_sfoldl_aux: "sfoldl⋅sappend⋅z⋅xs = z :@ sconcat⋅xs" by (induct xs arbitrary: z) simp_all lemma sconcat_sfoldl: "sconcat = sfoldl⋅sappend⋅[::]" by (clarsimp simp: cfun_eq_iff sconcat_sfoldl_aux) lemma sconcat_sappend[simp]: "sconcat⋅(xs :@ ys) = sconcat⋅xs :@ sconcat⋅ys" by (induct xs) simp_all fixrec slength :: "[:'a:] → Integer" where "slength⋅[::] = 0" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ slength⋅(x :# xs) = slength⋅xs + 1" lemma slength_strict[simp]: "slength⋅⊥ = ⊥" by fixrec_simp lemma slength_bottom_iff[simp]: "(slength⋅xs = ⊥) ⟷ (xs = ⊥)" by (induct xs) force+ lemma slength_ge_0: "slength⋅xs = MkI⋅n ⟹ n ≥ 0" by (induct xs arbitrary: n) (simp add: one_Integer_def plus_eq_MkI_conv; force)+ lemma slengthE: shows "⟦xs ≠ ⊥; ⋀n. ⟦slength⋅xs = MkI⋅n; 0 ≤ n⟧ ⟹ Q⟧ ⟹ Q" by (meson Integer.exhaust slength_bottom_iff slength_ge_0) lemma slength_0_conv[simp]: "(slength⋅xs = 0) ⟷ (xs = [::])" "(slength⋅xs = MkI⋅0) ⟷ (xs = [::])" "eq⋅0⋅(slength⋅xs) = snull⋅xs" "eq⋅(slength⋅xs)⋅0 = snull⋅xs" by (induct xs) (auto simp: one_Integer_def elim: slengthE) lemma le_slength_0[simp]: "(le⋅0⋅(slength⋅xs) = TT) ⟷ (xs ≠ ⊥)" by (cases "slength⋅xs") (auto simp: slength_ge_0 zero_Integer_def) lemma lt_slength_0[simp]: "xs ≠ ⊥ ⟹ lt⋅(slength⋅xs)⋅0 = FF" "xs ≠ ⊥ ⟹ lt⋅(slength⋅xs)⋅(slength⋅xs + 1) = TT" unfolding zero_Integer_def one_Integer_def by (auto elim: slengthE) lemma slength_smap[simp]: assumes "⋀x. x ≠ ⊥ ⟹ f⋅x ≠ ⊥" shows "slength⋅(smap⋅f⋅xs) = slength⋅xs" using assms by (induct xs) simp_all lemma slength_sappend[simp]: "slength⋅(xs :@ ys) = slength⋅xs + slength⋅ys" by (cases "ys = ⊥", force) (induct xs; force simp: ac_simps) lemma slength_sfoldl_aux: "sfoldl⋅(Λ i _. i + 1)⋅z⋅xs = z + slength⋅xs" by (induct xs arbitrary: z) (simp_all add: ac_simps) lemma slength_sfoldl: "slength = sfoldl⋅(Λ i _. i + 1)⋅0" by (clarsimp simp: cfun_eq_iff slength_sfoldl_aux) lemma le_slength_plus: assumes "xs ≠ ⊥" assumes "n ≠ ⊥" shows "le⋅n⋅(slength⋅xs + n) = TT" using assms by (cases n; force elim: slengthE) fixrec srev :: "[:'a:] → [:'a:]" where "srev⋅[::] = [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ srev⋅(x :# xs) = srev⋅xs :@ [:x:]" lemma srev_strict[simp]: "srev⋅⊥ = ⊥" by fixrec_simp lemma srev_bottom_iff[simp]: "(srev⋅xs = ⊥) ⟷ (xs = ⊥)" by (induct xs) simp_all lemma srev_scons[simp]: "srev⋅(x :# xs) = srev⋅xs :@ [:x:]" by (cases "x = ⊥", clarsimp) (induct xs; force) lemma srev_sappend[simp]: "srev⋅(xs :@ ys) = srev⋅ys :@ srev⋅xs" by (induct xs) simp_all lemma srev_srev_ident[simp]: "srev⋅(srev⋅xs) = xs" by (induct xs) auto lemma srev_cases[case_names bottom snil ssnoc]: assumes "xs = ⊥ ⟹ P" assumes "xs = [::] ⟹ P" assumes "⋀y ys. ⟦y ≠ ⊥; ys ≠ ⊥; xs = ys :@ [:y:]⟧ ⟹ P" shows "P" using assms by (metis slist.exhaust srev.simps(1) srev_scons srev_srev_ident srev_strict) lemma srev_induct[case_names bottom snil ssnoc]: assumes "P ⊥" assumes "P [::]" assumes "⋀x xs. ⟦x ≠ ⊥; xs ≠ ⊥; P xs⟧ ⟹ P (xs :@ [:x:])" shows "P xs" proof - have "P (srev⋅(srev⋅xs))" by (rule slist.induct[where x="srev⋅xs"]; simp add: assms) then show ?thesis by simp qed lemma sfoldr_conv_sfoldl: assumes "⋀x. f⋅x⋅⊥ = ⊥" ―‹‹f› must be strict in the accumulator.› shows "sfoldr⋅f⋅z⋅xs = sfoldl⋅(Λ acc x. f⋅x⋅acc)⋅z⋅(srev⋅xs)" using assms by (induct xs arbitrary: z) simp_all fixrec stake :: "Integer → [:'a:] → [:'a:]" where ―‹ Note: strict in both parameters. › "stake⋅⊥⋅⊥ = ⊥" | "i ≠ ⊥ ⟹ stake⋅i⋅[::] = [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ stake⋅i⋅(x :# xs) = If le⋅i⋅0 then [::] else x :# stake⋅(i - 1)⋅xs" lemma stake_strict[simp]: "stake⋅⊥ = ⊥" "stake⋅i⋅⊥ = ⊥" by fixrec_simp+ lemma stake_bottom_iff[simp]: "(stake⋅i⋅xs = ⊥) ⟷ (i = ⊥ ∨ xs = ⊥)" by (induct xs arbitrary: i; clarsimp; case_tac i; clarsimp) lemma stake_0[simp]: "xs ≠ ⊥ ⟹ stake⋅0⋅xs = [::]" "xs ≠ ⊥ ⟹ stake⋅(MkI⋅0)⋅xs = [::]" "stake⋅0⋅xs ⊑ [::]" by (cases xs; simp add: zero_Integer_def)+ lemma stake_scons[simp]: "le⋅1⋅i = TT ⟹ stake⋅i⋅(x :# xs) = x :# stake⋅(i - 1)⋅xs" by (cases i; cases "x = ⊥"; cases "xs = ⊥"; simp add: zero_Integer_def one_Integer_def split: if_splits) lemma take_MkI_scons[simp]: "0 < n ⟹ stake⋅(MkI⋅n)⋅(x :# xs) = x :# stake⋅(MkI⋅(n - 1))⋅xs" by (cases "x = ⊥"; cases "xs = ⊥"; simp add: zero_Integer_def one_Integer_def) lemma stake_numeral_scons[simp]: "xs ≠ ⊥ ⟹ stake⋅1⋅(x :# xs) = [:x:]" "stake⋅(numeral (Num.Bit0 k))⋅(x :# xs) = x :# stake⋅(numeral (Num.BitM k))⋅xs" "stake⋅(numeral (Num.Bit1 k))⋅(x :# xs) = x :# stake⋅(numeral (Num.Bit0 k))⋅xs" by (cases "x = ⊥"; cases xs; simp add: zero_Integer_def one_Integer_def numeral_Integer_eq)+ lemma stake_all: assumes "le⋅(slength⋅xs)⋅i = TT" shows "stake⋅i⋅xs = xs" using assms proof(induct xs arbitrary: i) case (scons x xs i) then show ?case by (cases i; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits if_splits elim!: slengthE) qed (simp_all add: le_defined) lemma stake_all_triv[simp]: "stake⋅(slength⋅xs)⋅xs = xs" by (cases "xs = ⊥") (auto simp: stake_all) lemma stake_append[simp]: "stake⋅i⋅(xs :@ ys) = stake⋅i⋅xs :@ stake⋅(i - slength⋅xs)⋅ys" proof(induct xs arbitrary: i) case (snil i) then show ?case by (cases i; simp add: zero_Integer_def) next case (scons x xs i) then show ?case by (cases i; cases ys; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits elim!: slengthE) qed simp_all fixrec sdrop :: "Integer → [:'a:] → [:'a:]" where ―‹ Note: strict in both parameters. › [simp del]: "sdrop⋅i⋅xs = If le⋅i⋅0 then xs else (case xs of [::] ⇒ [::] | y :# ys ⇒ sdrop⋅(i - 1)⋅ys)" lemma sdrop_strict[simp]: "sdrop⋅⊥ = ⊥" "sdrop⋅i⋅⊥ = ⊥" by fixrec_simp+ lemma sdrop_bottom_iff[simp]: "(sdrop⋅i⋅xs = ⊥) ⟷ (i = ⊥ ∨ xs = ⊥)" proof(induct xs arbitrary: i) case (snil i) then show ?case by (subst sdrop.unfold) (cases i; simp) next case (scons x xs i) then show ?case by (subst sdrop.unfold) fastforce qed simp lemma sdrop_snil[simp]: assumes "i ≠ ⊥" shows "sdrop⋅i⋅[::] = [::]" using assms by (subst sdrop.unfold; fastforce) lemma sdrop_snil_conv[simp]: "(sdrop⋅i⋅[::] = [::]) ⟷ (i ≠ ⊥)" by (subst sdrop.unfold; fastforce) lemma sdrop_0[simp]: "sdrop⋅0⋅xs = xs" "sdrop⋅(MkI⋅0)⋅xs = xs" by (subst sdrop.simps, simp add: zero_Integer_def)+ lemma sdrop_pos: "le⋅i⋅0 = FF ⟹ sdrop⋅i⋅xs = (case xs of [::] ⇒ [::] | y :# ys ⇒ sdrop⋅(i - 1)⋅ys)" by (subst sdrop.simps, simp) lemma sdrop_neg: "le⋅i⋅0 = TT ⟹ sdrop⋅i⋅xs = xs" by (subst sdrop.simps, simp) lemma sdrop_numeral_scons[simp]: "x ≠ ⊥ ⟹ sdrop⋅1⋅(x :# xs) = xs" "x ≠ ⊥ ⟹ sdrop⋅(numeral (Num.Bit0 k))⋅(x :# xs) = sdrop⋅(numeral (Num.BitM k))⋅xs" "x ≠ ⊥ ⟹ sdrop⋅(numeral (Num.Bit1 k))⋅(x :# xs) = sdrop⋅(numeral (Num.Bit0 k))⋅xs" by (subst sdrop.simps, simp add: zero_Integer_def one_Integer_def numeral_Integer_eq; cases xs; simp)+ lemma sdrop_sappend[simp]: "sdrop⋅i⋅(xs :@ ys) = sdrop⋅i⋅xs :@ sdrop⋅(i - slength⋅xs)⋅ys" proof(induct xs arbitrary: i) case (snil i) then show ?case by (cases i; simp add: zero_Integer_def) next case (scons x xs i) then show ?case by (cases "ys = ⊥"; cases "le⋅i⋅0"; cases i; clarsimp simp: zero_Integer_def one_Integer_def sdrop_neg sdrop_pos add.commute diff_diff_add split: if_splits elim!: slengthE) qed simp lemma sdrop_all: assumes "le⋅(slength⋅xs)⋅i = TT" shows "sdrop⋅i⋅xs = [::]" using assms proof(induct xs arbitrary: i) case (scons x xs i) then show ?case by (subst sdrop.unfold; cases i; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits if_splits elim!: slengthE) qed (simp_all add: le_defined) lemma slength_sdrop[simp]: "slength⋅(sdrop⋅i⋅xs) = If le⋅i⋅0 then slength⋅xs else If le⋅(slength⋅xs)⋅i then 0 else slength⋅xs - i" proof(induct xs arbitrary: i) case (snil i) then show ?case by (cases i; simp add: zero_Integer_def) next case (scons x xs i) then show ?case by (subst sdrop.unfold; cases i; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE) qed simp lemma sdrop_not_snilD: assumes "sdrop⋅(MkI⋅i)⋅xs ≠ [::]" assumes "xs ≠ ⊥" shows "lt⋅(MkI⋅i)⋅(slength⋅xs) = TT ∧ xs ≠ [::]" using assms proof(induct xs arbitrary: i) case (scons x xs i) then show ?case by (subst (asm) (2) sdrop.unfold, clarsimp simp: zero_Integer_def one_Integer_def not_le sdrop_all elim!: slengthE) qed simp_all lemma sdrop_sappend_same: assumes "xs ≠ ⊥" shows "sdrop⋅(slength⋅xs)⋅(xs :@ ys) = ys" using assms proof(induct xs arbitrary: ys) case (scons x xs ys) then show ?case by (cases "ys = ⊥"; subst sdrop.unfold; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE) qed simp_all fixrec sscanl :: "('a → 'b → 'a) → 'a → [:'b:] → [:'a:]" where "sscanl⋅f⋅z⋅[::] = z :# [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sscanl⋅f⋅z⋅(x :# xs) = z :# sscanl⋅f⋅(f⋅z⋅x)⋅xs" lemma sscanl_strict[simp]: "sscanl⋅f⋅⊥⋅xs = ⊥" "sscanl⋅f⋅z⋅⊥ = ⊥" by (cases xs) fixrec_simp+ lemma sscanl_cong: assumes "xs = xs'" assumes "z = z'" assumes "⋀x z. x ∈ sset xs ⟹ f⋅z⋅x = f'⋅z⋅x" shows "sscanl⋅f⋅z⋅xs = sscanl⋅f'⋅z'⋅xs'" using assms by (induct xs arbitrary: xs' z z') auto lemma sscanl_lfp_fusion': assumes "g⋅⊥ = ⊥" assumes *: "⋀acc x. x ≠ ⊥ ⟹ g⋅(f⋅acc⋅x) = f'⋅(g⋅acc)⋅x" shows "smap⋅g⋅(sscanl⋅f⋅z⋅xs) = sscanl⋅f'⋅(g⋅z)⋅xs" using assms by (induct xs arbitrary: z) simp_all lemma sscanl_lfp_fusion: assumes "g⋅⊥ = ⊥" assumes *: "⋀acc x. x ≠ ⊥ ⟹ g⋅(f⋅acc⋅x) = f'⋅(g⋅acc)⋅x" shows "smap⋅g oo sscanl⋅f⋅z = sscanl⋅f'⋅(g⋅z)" using assms by (clarsimp simp: cfun_eq_iff sscanl_lfp_fusion') lemma sscanl_ww_fusion': ―‹ Worker/wrapper \<^citep>‹"GillHutton:2009" and "Gammie:2011"› specialised to @{const ‹sscanl›} › fixes wrap :: "'b → 'a" fixes unwrap :: "'a → 'b" fixes z :: "'a" fixes f :: "'a → 'c → 'a" fixes f' :: "'b → 'c → 'b" assumes ww: "wrap oo unwrap = ID" assumes wb: "⋀z x. x ≠ ⊥ ⟹ unwrap⋅(f⋅(wrap⋅z)⋅x) = f'⋅(unwrap⋅(wrap⋅z))⋅x" shows "sscanl⋅f⋅z⋅xs = smap⋅wrap⋅(sscanl⋅f'⋅(unwrap⋅z)⋅xs)" using assms by (induct xs arbitrary: z) (simp add: cfun_eq_iff retraction_cfcomp_strict | metis)+ lemma sscanl_ww_fusion: ―‹ Worker/wrapper \<^citep>‹"GillHutton:2009" and "Gammie:2011"› specialised to @{const ‹sscanl›} › fixes wrap :: "'b → 'a" fixes unwrap :: "'a → 'b" fixes z :: "'a" fixes f :: "'a → 'c → 'a" fixes f' :: "'b → 'c → 'b" assumes ww: "wrap oo unwrap = ID" assumes wb: "⋀z x. x ≠ ⊥ ⟹ unwrap⋅(f⋅(wrap⋅z)⋅x) = f'⋅(unwrap⋅(wrap⋅z))⋅x" shows "sscanl⋅f⋅z = smap⋅wrap oo sscanl⋅f'⋅(unwrap⋅z)" using assms by (clarsimp simp: cfun_eq_iff sscanl_ww_fusion') fixrec sinits :: "[:'a:] → [:[:'a:]:]" where "sinits⋅[::] = [::] :# [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sinits⋅(x :# xs) = [::] :# smap⋅(scons⋅x)⋅(sinits⋅xs)" lemma sinits_strict[simp]: "sinits⋅⊥ = ⊥" by fixrec_simp lemma sinits_bottom_iff[simp]: "(sinits⋅xs = ⊥) ⟷ (xs = ⊥)" by (induct xs) simp_all lemma sinits_not_snil[iff]: "sinits⋅xs ≠ [::]" by (cases xs) simp_all lemma sinits_empty_bottom[simp]: "(sset (sinits⋅xs) = {}) ⟷ (xs = ⊥)" by (cases xs) simp_all lemma sinits_scons[simp]: "sinits⋅(x :# xs) = [::] :# smap⋅(x :#)⋅(sinits⋅xs)" by (cases "x = ⊥", force) (induct xs; force) lemma sinits_length[simp]: "slength⋅(sinits⋅xs) = slength⋅xs + 1" by (induct xs) simp_all lemma sinits_snoc[simp]: "sinits⋅(xs :@ [:x:]) = sinits⋅xs :@ [:xs :@ [:x:]:]" by (induct xs) simp_all lemma sinits_foldr': ―‹ \<^citet>‹‹p30› in "Bird:1987"› › shows "sinits⋅xs = sfoldr⋅(Λ x xs. [:[::]:] :@ smap⋅(x :#)⋅xs)⋅[:[::]:]⋅xs" by (induct xs) simp_all lemma sinits_sscanl': shows "smap⋅(sfoldl⋅f⋅z)⋅(sinits⋅xs) = sscanl⋅f⋅z⋅xs" by (induct xs arbitrary: z) (simp_all cong: smap_cong add: oo_def eta_cfun) lemma sinits_sscanl: ―‹ \<^citet>‹‹Lemma~5› in "Bird:1987"›, \<^citet>‹‹p118 ``the scan lemma''› in "Bird:PearlsofFAD:2010"› › shows "smap⋅(sfoldl⋅f⋅z) oo sinits = sscanl⋅f⋅z" by (simp add: sinits_sscanl' cfun_eq_iff) lemma sinits_all[simp]: "(xs ∈ sset (sinits⋅xs)) ⟷ (xs ≠ ⊥)" by (induct xs) simp_all fixrec stails :: "[:'a:] → [:[:'a:]:]" where "stails⋅[::] = [::] :# [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ stails⋅(x :# xs) = (x :# xs) :# stails⋅xs" lemma stails_strict[simp]: "stails⋅⊥ = ⊥" by fixrec_simp lemma stails_bottom_iff[simp]: "(stails⋅xs = ⊥) ⟷ (xs = ⊥)" by (induct xs) simp_all lemma stails_not_snil[iff]: "stails⋅xs ≠ [::]" by (cases xs) simp_all lemma stails_scons[simp]: "stails⋅(x :# xs) = (x :# xs) :# stails⋅xs" by (induct xs) (cases "x = ⊥"; simp)+ lemma stails_slength[simp]: "slength⋅(stails⋅xs) = slength⋅xs + 1" by (induct xs) simp_all lemma stails_snoc[simp]: shows "stails⋅(xs :@ [:x:]) = smap⋅(Λ ys. ys :@ [:x:])⋅(stails⋅xs) :@ [:[::]:]" by (induct xs) simp_all lemma stails_sfoldl': shows "stails⋅xs = sfoldl⋅(Λ xs x. smap⋅(Λ ys. ys :@ [:x:])⋅xs :@ [:[::]:])⋅[:[::]:]⋅xs" by (induct xs rule: srev_induct) simp_all lemma stails_sfoldl: shows "stails = sfoldl⋅(Λ xs x. smap⋅(Λ ys. ys :@ [:x:])⋅xs :@ [:[::]:])⋅[:[::]:]" by (clarsimp simp: cfun_eq_iff stails_sfoldl') lemma stails_all[simp]: "(xs ∈ sset (stails⋅xs)) ⟷ (xs ≠ ⊥)" by (cases xs) simp_all fixrec selem :: "'a::Eq_def → [:'a:] → tr" where "selem⋅x⋅[::] = FF" | "⟦y ≠ ⊥; ys ≠ ⊥⟧ ⟹ selem⋅x⋅(y :# ys) = (eq⋅x⋅y orelse selem⋅x⋅ys)" lemma selem_strict[simp]: "selem⋅x⋅⊥ = ⊥" by fixrec_simp lemma selem_bottom_iff[simp]: "(selem⋅x⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (xs ≠ [::] ∧ x = ⊥))" by (induct xs) auto lemma selem_sappend[simp]: assumes "ys ≠ ⊥" shows "selem⋅x⋅(xs :@ ys) = (selem⋅x⋅xs orelse selem⋅x⋅ys)" using assms by (induct xs) simp_all lemma elem_TT[simp]: "(selem⋅x⋅xs = TT) ⟷ (x ∈ sset xs)" by (induct xs; auto) (metis sset_defined)+ lemma elem_FF[simp]: "(selem⋅x⋅xs = FF) ⟷ (xs = [::] ∨ (x ≠ ⊥ ∧ xs ≠ ⊥ ∧ x ∉ sset xs))" by (induct xs) auto lemma selem_snil_stails[iff]: assumes "xs ≠ ⊥" shows "selem⋅[::]⋅(stails⋅xs) = TT" using assms by (induct xs) simp_all fixrec sconcatMap :: "('a → [:'b:]) → [:'a:] → [:'b:]" where [simp del]: "sconcatMap⋅f = sconcat oo smap⋅f" lemma sconcatMap_strict[simp]: "sconcatMap⋅f⋅⊥ = ⊥" by fixrec_simp lemma sconcatMap_snil[simp]: "sconcatMap⋅f⋅[::] = [::]" by fixrec_simp lemma sconcatMap_scons[simp]: "x ≠ ⊥ ⟹ sconcatMap⋅f⋅(x :# xs) = f⋅x :@ sconcatMap⋅f⋅xs" by (cases "xs = ⊥"; simp add: sconcatMap.unfold) lemma sconcatMap_bottom_iff[simp]: "(sconcatMap⋅f⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (∃x∈sset xs. f⋅x = ⊥))" by (induct xs) simp_all lemma sconcatMap_sappend[simp]: "sconcatMap⋅f⋅(xs :@ ys) = sconcatMap⋅f⋅xs :@ sconcatMap⋅f⋅ys" by (induct xs) simp_all lemma sconcatMap_monad_laws: "sconcatMap⋅(Λ x. [:x:])⋅xs = xs" "sconcatMap⋅g⋅(sconcatMap⋅f⋅xs) = sconcatMap⋅(Λ x. sconcatMap⋅g⋅(f⋅x))⋅xs" by (induct xs) simp_all fixrec supto :: "Integer → Integer → [:Integer:]" where [simp del]: "supto⋅i⋅j = If le⋅i⋅j then i :# supto⋅(i+1)⋅j else [::]" lemma upto_strict[simp]: "supto⋅⊥ = ⊥" "supto⋅m⋅⊥ = ⊥" by fixrec_simp+ lemma supto_is_snil_conv[simp]: "(supto⋅(MkI⋅i)⋅(MkI⋅j) = [::]) ⟷ (j < i)" "([::] = supto⋅(MkI⋅i)⋅(MkI⋅j)) ⟷ (j < i)" by (subst supto.unfold; simp)+ lemma supto_simp[simp]: "j < i ⟹ supto⋅(MkI⋅i)⋅(MkI⋅j) = [::]" "i ≤ j ⟹ supto⋅(MkI⋅i)⋅(MkI⋅j) = MkI⋅i :# supto⋅(MkI⋅i+1)⋅(MkI⋅j)" "supto⋅0⋅0 = [:0:]" by (subst supto.simps, simp)+ lemma supto_defined[simp]: "supto⋅(MkI⋅i)⋅(MkI⋅j) ≠ ⊥" (is "?P i j") proof (cases "j - i") fix d assume "j - i = int d" then show "?P i j" proof (induct d arbitrary: i j) case (Suc d i j) then have "j - (i + 1) = int d" and le: "i ≤ j" by simp_all from Suc(1)[OF this(1)] have IH: "?P (i+1) j" . then show ?case using le by (simp add: one_Integer_def) qed (simp add: one_Integer_def) next fix d assume "j - i = - int d" then have "j ≤ i" by auto moreover { assume "j = i" then have "?P i j" by (simp add: one_Integer_def) } moreover { assume "j < i" then have "?P i j" by (simp add: one_Integer_def) } ultimately show ?thesis by arith qed lemma supto_bottom_iff[simp]: "(supto⋅i⋅j = ⊥) ⟷ (i = ⊥ ∨ j = ⊥)" by (cases i; simp; cases j; simp) lemma supto_snoc[simp]: "i ≤ j ⟹ supto⋅(MkI⋅i)⋅(MkI⋅j) = supto⋅(MkI⋅i)⋅(MkI⋅j-1) :@ [:MkI⋅j:]" proof(induct "nat(j - i)" arbitrary: i j) case 0 then show ?case by (simp add: one_Integer_def) next case (Suc k i j) then have "k = nat (j - (i + 1))" "i < j" by linarith+ from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) show ?case by (simp add: one_Integer_def) qed lemma slength_supto[simp]: "slength⋅(supto⋅(MkI⋅i)⋅(MkI⋅j)) = MkI⋅(if j < i then 0 else j - i + 1)" (is "?P i j") proof (cases "j - i") fix d assume "j - i = int d" then show "?P i j" proof (induct d arbitrary: i j) case (Suc d i j) then have "j - (i + 1) = int d" and le: "i ≤ j" by simp_all from Suc(1)[OF this(1)] have IH: "?P (i+1) j" . then show ?case using le by (simp add: one_Integer_def) qed (simp add: one_Integer_def) next fix d assume "j - i = - int d" then have "j ≤ i" by auto moreover { assume "j = i" then have "?P i j" by (simp add: one_Integer_def) } moreover { assume "j < i" then have "?P i j" by (simp add: one_Integer_def) } ultimately show ?thesis by arith qed lemma sset_supto[simp]: "sset (supto⋅(MkI⋅i)⋅(MkI⋅j)) = {MkI⋅k |k. i ≤ k ∧ k ≤ j}" (is "sset (?u i j) = ?R i j") proof (cases "j - i") case (nonneg k) then show ?thesis proof (induct k arbitrary: i j) case (Suc k) then have *: "j - (i + 1) = int k" by simp from Suc(1)[OF *] have IH: "sset (?u (i+1) j) = ?R (i+1) j" . from * have "i ≤ j" by simp then have "sset (?u i j) = sset (MkI⋅i :# ?u (i+1) j)" by (simp add: one_Integer_def) also have "… = insert (MkI⋅i) (?R (i+1) j)" by (simp add: IH) also have "… = ?R i j" using ‹i ≤ j› by auto finally show ?case . qed (force simp: one_Integer_def) qed simp lemma supto_split1: ―‹From ‹HOL.List›› assumes "i ≤ j" assumes "j ≤ k" shows "supto⋅(MkI⋅i)⋅(MkI⋅k) = supto⋅(MkI⋅i)⋅(MkI⋅(j - 1)) :@ supto⋅(MkI⋅j)⋅(MkI⋅k)" using assms proof (induct j rule: int_ge_induct) case (step l) with supto_simp(2) supto_snoc show ?case by (clarsimp simp: one_Integer_def) qed simp lemma supto_split2: ―‹From ‹HOL.List›› assumes "i ≤ j" assumes "j ≤ k" shows "supto⋅(MkI⋅i)⋅(MkI⋅k) = supto⋅(MkI⋅i)⋅(MkI⋅j) :@ supto⋅(MkI⋅(j + 1))⋅(MkI⋅k)" proof(cases "j + 1 ≤ k") case True with assms show ?thesis by (subst supto_split1[where j="j + 1" and k=k]; clarsimp simp: one_Integer_def) next case False with assms show ?thesis by (clarsimp simp: one_Integer_def not_le) qed lemma supto_split3: ―‹From ‹HOL.List›› assumes "i ≤ j" assumes "j ≤ k" shows "supto⋅(MkI⋅i)⋅(MkI⋅k) = supto⋅(MkI⋅i)⋅(MkI⋅(j - 1)) :@ MkI⋅j :# supto⋅(MkI⋅(j + 1))⋅(MkI⋅k)" using assms supto_simp(2) supto_split1 by (metis one_Integer_def plus_MkI_MkI) lemma sinits_stake': shows "sinits⋅xs = smap⋅(Λ i. stake⋅i⋅xs)⋅(supto⋅0⋅(slength⋅xs))" proof(induct xs rule: srev_induct) case (ssnoc x xs) then show ?case apply (clarsimp simp: zero_Integer_def one_Integer_def stake_all simp del: supto_simp elim!: slengthE) apply (rule arg_cong, rule smap_cong[OF refl]) apply clarsimp done qed simp_all lemma stails_sdrop': shows "stails⋅xs = smap⋅(Λ i. sdrop⋅i⋅xs)⋅(supto⋅0⋅(slength⋅xs))" proof(induct xs rule: srev_induct) case (ssnoc x xs) then show ?case apply (clarsimp simp: zero_Integer_def one_Integer_def sdrop_all simp del: supto_simp elim!: slengthE) apply (rule arg_cong, rule smap_cong[OF refl]) apply clarsimp apply (subst (3) sdrop_neg; fastforce simp: zero_Integer_def) done qed simp_all lemma sdrop_elem_stails[iff]: assumes "xs ≠ ⊥" shows "sdrop⋅(MkI⋅i)⋅xs ∈ sset (stails⋅xs)" using assms by (clarsimp simp: stails_sdrop' zero_Integer_def one_Integer_def elim!: slengthE) (metis add.left_neutral le_MkI_MkI le_cases not_less sdrop_all sdrop_neg zero_Integer_def zless_imp_add1_zle) fixrec slast :: "[:'a:] → 'a" where "slast⋅[::] = ⊥" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ slast⋅(x :# xs) = (case xs of [::] ⇒ x | y :# ys ⇒ slast⋅xs)" lemma slast_strict[simp]: "slast⋅⊥ = ⊥" by fixrec_simp lemma slast_singleton[simp]: "slast⋅[:x:] = x" by (cases "x = ⊥"; simp) lemma slast_sappend_ssnoc[simp]: assumes "xs ≠ ⊥" shows "slast⋅(xs :@ [:x:]) = x" using assms proof(induct xs) case (scons y ys) then show ?case by (cases "x = ⊥"; simp; cases ys; simp) qed simp_all fixrec sbutlast :: "[:'a:] → [:'a:]" where "sbutlast⋅[::] = [::]" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sbutlast⋅(x :# xs) = (case xs of [::] ⇒ [::] | y :# ys ⇒ x :# sbutlast⋅xs)" lemma sbutlast_strict[simp]: "sbutlast⋅⊥ = ⊥" by fixrec_simp lemma sbutlast_sappend_ssnoc[simp]: assumes "x ≠ ⊥" shows "sbutlast⋅(xs :@ [:x:]) = xs" using assms proof(induct xs) case (scons y ys) then show ?case by (cases ys; simp) qed simp_all fixrec prefix :: "[:'a::Eq_def:] → [:'a:] → tr" where "prefix⋅xs⋅⊥ = ⊥" | "ys ≠ ⊥ ⟹ prefix⋅[::]⋅ys = TT" | "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ prefix⋅(x :# xs)⋅[::] = FF" | "⟦x ≠ ⊥; xs ≠ ⊥; y ≠ ⊥; ys ≠ ⊥⟧ ⟹ prefix⋅(x :# xs)⋅(y :# ys) = (eq⋅x⋅y andalso prefix⋅xs⋅ys)" lemma prefix_strict[simp]: "prefix⋅⊥ = ⊥" by (clarsimp simp: cfun_eq_iff) fixrec_simp lemma prefix_bottom_iff[simp]: "(prefix⋅xs⋅ys = ⊥) ⟷ (xs = ⊥ ∨ ys = ⊥)" proof(induct xs arbitrary: ys) case (snil ys) then show ?case by (cases ys) simp_all next case (scons a xs) then show ?case by (cases ys) simp_all qed simp lemma prefix_definedD: assumes "prefix⋅xs⋅ys = TT" shows "xs ≠ ⊥ ∧ ys ≠ ⊥" using assms by (induct xs arbitrary: ys) auto lemma prefix_refl[simp]: assumes "xs ≠ ⊥" shows "prefix⋅xs⋅xs = TT" using assms by (induct xs) simp_all lemma prefix_refl_conv[simp]: "(prefix⋅xs⋅xs = TT) ⟷ (xs ≠ ⊥)" by auto lemma prefix_of_snil[simp]: "prefix⋅xs⋅[::] = (case xs of [::] ⇒ TT | x :# xs ⇒ FF)" by (cases xs) simp_all lemma prefix_singleton_TT: shows "prefix⋅[:x:]⋅ys = TT ⟷ (x ≠ ⊥ ∧ (∃zs. zs ≠ ⊥ ∧ ys = x :# zs))" by (cases "x = ⊥"; clarsimp; cases ys; fastforce) lemma prefix_singleton_FF: shows "prefix⋅[:x:]⋅ys = FF ⟷ (x ≠ ⊥ ∧ (ys = [::] ∨ (∃z zs. z ≠ ⊥ ∧ zs ≠ ⊥ ∧ ys = z :# zs ∧ x ≠ z)))" by (cases "x = ⊥"; clarsimp; cases ys; fastforce) lemma prefix_FF_not_snilD: assumes "prefix⋅xs⋅ys = FF" shows "xs ≠ [::]" using assms by (cases xs; cases ys; simp) lemma prefix_slength: assumes "prefix⋅xs⋅ys = TT" shows "le⋅(slength⋅xs)⋅(slength⋅ys) = TT" using assms proof(induct ys arbitrary: xs) case (snil xs) then show ?case by (cases xs) simp_all next case (scons a ys) then show ?case by (cases xs) (simp_all add: le_plus_1) qed simp lemma prefix_slength_strengthen: "prefix⋅xs⋅ys = (le⋅(slength⋅xs)⋅(slength⋅ys) andalso prefix⋅xs⋅ys)" by (rule andalso_weaken_left) (auto dest: prefix_slength) lemma prefix_scons_snil[simp]: "prefix⋅(x :# xs)⋅[::] ≠ TT" by (cases "x :# xs ≠ ⊥") auto lemma scons_prefix_scons[simp]: "(prefix⋅(x :# xs)⋅(y :# ys) = TT) ⟷ (eq⋅x⋅y = TT ∧ prefix⋅xs⋅ys = TT)" by (cases "x :# xs ≠ ⊥ ∧ y :# ys ≠ ⊥") auto lemma append_prefixD: assumes "prefix⋅(xs :@ ys)⋅zs = TT" shows "prefix⋅xs⋅zs = TT" using assms proof(induct xs arbitrary: zs) case (snil zs) then show ?case using prefix.simps(2) by force next case (scons x xs zs) then show ?case by (metis prefix.simps(1) prefix_scons_snil sappend_scons scons_prefix_scons slist.exhaust) qed simp lemma same_prefix_prefix[simp]: assumes "xs ≠ ⊥" shows "prefix⋅(xs :@ ys)⋅(xs :@ zs) = prefix⋅ys⋅zs" using assms proof(cases "ys = ⊥" "zs = ⊥" rule: bool.exhaust[case_product bool.exhaust]) case False_False with assms show ?thesis by (induct xs) simp_all qed simp_all lemma eq_prefix_TT: assumes "eq⋅xs⋅ys = TT" shows "prefix⋅xs⋅ys = TT" using assms by (induct xs arbitrary: ys) (case_tac ys; simp)+ lemma prefix_eq_FF: assumes "prefix⋅xs⋅ys = FF" shows "eq⋅xs⋅ys = FF" using assms by (induct xs arbitrary: ys) (case_tac ys; auto)+ lemma prefix_slength_eq: shows "eq⋅xs⋅ys = (eq⋅(slength⋅xs)⋅(slength⋅ys) andalso prefix⋅xs⋅ys)" proof(induct xs arbitrary: ys) case (snil ys) then show ?case by (cases ys; clarsimp simp: one_Integer_def elim!: slengthE) next case (scons x xs ys) then show ?case by (cases ys; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE) qed simp lemma stake_slength_plus_1: shows "stake⋅(slength⋅xs + 1)⋅(y :# ys) = y :# stake⋅(slength⋅xs)⋅ys" by (cases "xs = ⊥" "y = ⊥" "ys = ⊥" rule: bool.exhaust[case_product bool.exhaust bool.exhaust]; clarsimp) (auto simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits elim!: slengthE) lemma sdrop_slength_plus_1: assumes "y ≠ ⊥" shows "sdrop⋅(slength⋅xs + 1)⋅(y :# ys) = sdrop⋅(slength⋅xs)⋅ys" using assms by (subst sdrop.simps; cases "xs = ⊥"; clarsimp; cases "ys = ⊥"; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits elim!: slengthE) lemma eq_take_length_prefix: "prefix⋅xs⋅ys = eq⋅xs⋅(stake⋅(slength⋅xs)⋅ys)" proof (induct xs arbitrary: ys) case (snil ys) show ?case by (cases ys; clarsimp) next case (scons x xs ys) note IH = this show ?case proof (cases "slength⋅xs = ⊥") case True then show ?thesis by simp next case False show ?thesis proof (cases ys) case bottom then show ?thesis using False using le_slength_plus[of xs 1] by simp next case snil then show ?thesis using False and IH(1,2) by simp next case (scons z zs) then show ?thesis using False and IH(1,2) IH(3)[of zs] by (simp add: stake_slength_plus_1 monofun_cfun_arg) qed qed qed simp lemma prefix_sdrop_slength: assumes