1(* Title: HOL/HOLCF/IOA/Seq.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close> 6 7theory Seq 8imports HOLCF 9begin 10 11default_sort pcpo 12 13domain (unsafe) 'a seq = nil ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65) 14 15inductive Finite :: "'a seq \<Rightarrow> bool" 16where 17 sfinite_0: "Finite nil" 18| sfinite_n: "Finite tr \<Longrightarrow> a \<noteq> UU \<Longrightarrow> Finite (a ## tr)" 19 20declare Finite.intros [simp] 21 22definition Partial :: "'a seq \<Rightarrow> bool" 23 where "Partial x \<longleftrightarrow> seq_finite x \<and> \<not> Finite x" 24 25definition Infinite :: "'a seq \<Rightarrow> bool" 26 where "Infinite x \<longleftrightarrow> \<not> seq_finite x" 27 28 29subsection \<open>Recursive equations of operators\<close> 30 31subsubsection \<open>\<open>smap\<close>\<close> 32 33fixrec smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a seq \<rightarrow> 'b seq" 34where 35 smap_nil: "smap \<cdot> f \<cdot> nil = nil" 36| smap_cons: "x \<noteq> UU \<Longrightarrow> smap \<cdot> f \<cdot> (x ## xs) = (f \<cdot> x) ## smap \<cdot> f \<cdot> xs" 37 38lemma smap_UU [simp]: "smap \<cdot> f \<cdot> UU = UU" 39 by fixrec_simp 40 41 42subsubsection \<open>\<open>sfilter\<close>\<close> 43 44fixrec sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq" 45where 46 sfilter_nil: "sfilter \<cdot> P \<cdot> nil = nil" 47| sfilter_cons: 48 "x \<noteq> UU \<Longrightarrow> 49 sfilter \<cdot> P \<cdot> (x ## xs) = 50 (If P \<cdot> x then x ## (sfilter \<cdot> P \<cdot> xs) else sfilter \<cdot> P \<cdot> xs)" 51 52lemma sfilter_UU [simp]: "sfilter \<cdot> P \<cdot> UU = UU" 53 by fixrec_simp 54 55 56subsubsection \<open>\<open>sforall2\<close>\<close> 57 58fixrec sforall2 :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> tr" 59where 60 sforall2_nil: "sforall2 \<cdot> P \<cdot> nil = TT" 61| sforall2_cons: "x \<noteq> UU \<Longrightarrow> sforall2 \<cdot> P \<cdot> (x ## xs) = ((P \<cdot> x) andalso sforall2 \<cdot> P \<cdot> xs)" 62 63lemma sforall2_UU [simp]: "sforall2 \<cdot> P \<cdot> UU = UU" 64 by fixrec_simp 65 66definition "sforall P t \<longleftrightarrow> sforall2 \<cdot> P \<cdot> t \<noteq> FF" 67 68 69subsubsection \<open>\<open>stakewhile\<close>\<close> 70 71fixrec stakewhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq" 72where 73 stakewhile_nil: "stakewhile \<cdot> P \<cdot> nil = nil" 74| stakewhile_cons: 75 "x \<noteq> UU \<Longrightarrow> stakewhile \<cdot> P \<cdot> (x ## xs) = (If P \<cdot> x then x ## (stakewhile \<cdot> P \<cdot> xs) else nil)" 76 77lemma stakewhile_UU [simp]: "stakewhile \<cdot> P \<cdot> UU = UU" 78 by fixrec_simp 79 80 81subsubsection \<open>\<open>sdropwhile\<close>\<close> 82 83fixrec sdropwhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq" 84where 85 sdropwhile_nil: "sdropwhile \<cdot> P \<cdot> nil = nil" 86| sdropwhile_cons: 87 "x \<noteq> UU \<Longrightarrow> sdropwhile \<cdot> P \<cdot> (x ## xs) = (If P \<cdot> x then sdropwhile \<cdot> P \<cdot> xs else x ## xs)" 88 89lemma sdropwhile_UU [simp]: "sdropwhile \<cdot> P \<cdot> UU = UU" 90 by fixrec_simp 91 92 93subsubsection \<open>\<open>slast\<close>\<close> 94 95fixrec slast :: "'a seq \<rightarrow> 'a" 96where 97 slast_nil: "slast \<cdot> nil = UU" 98| slast_cons: "x \<noteq> UU \<Longrightarrow> slast \<cdot> (x ## xs) = (If is_nil \<cdot> xs then x else slast \<cdot> xs)" 99 100lemma slast_UU [simp]: "slast \<cdot> UU = UU" 101 by fixrec_simp 102 103 104subsubsection \<open>\<open>sconc\<close>\<close> 105 106fixrec sconc :: "'a seq \<rightarrow> 'a seq \<rightarrow> 'a seq" 107where 108 sconc_nil: "sconc \<cdot> nil \<cdot> y = y" 109| sconc_cons': "x \<noteq> UU \<Longrightarrow> sconc \<cdot> (x ## xs) \<cdot> y = x ## (sconc \<cdot> xs \<cdot> y)" 110 111abbreviation sconc_syn :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq" (infixr "@@" 65) 112 where "xs @@ ys \<equiv> sconc \<cdot> xs \<cdot> ys" 113 114lemma sconc_UU [simp]: "UU @@ y = UU" 115 by fixrec_simp 116 117lemma sconc_cons [simp]: "(x ## xs) @@ y = x ## (xs @@ y)" 118 by (cases "x = UU") simp_all 119 120declare sconc_cons' [simp del] 121 122 123subsubsection \<open>\<open>sflat\<close>\<close> 124 125fixrec sflat :: "'a seq seq \<rightarrow> 'a seq" 126where 127 sflat_nil: "sflat \<cdot> nil = nil" 128| sflat_cons': "x \<noteq> UU \<Longrightarrow> sflat \<cdot> (x ## xs) = x @@ (sflat \<cdot> xs)" 129 130lemma sflat_UU [simp]: "sflat \<cdot> UU = UU" 131 by fixrec_simp 132 133lemma sflat_cons [simp]: "sflat \<cdot> (x ## xs) = x @@ (sflat \<cdot> xs)" 134 by (cases "x = UU") simp_all 135 136declare sflat_cons' [simp del] 137 138 139subsubsection \<open>\<open>szip\<close>\<close> 140 141fixrec szip :: "'a seq \<rightarrow> 'b seq \<rightarrow> ('a \<times> 'b) seq" 142where 143 szip_nil: "szip \<cdot> nil \<cdot> y = nil" 144| szip_cons_nil: "x \<noteq> UU \<Longrightarrow> szip \<cdot> (x ## xs) \<cdot> nil = UU" 145| szip_cons: "x \<noteq> UU \<Longrightarrow> y \<noteq> UU \<Longrightarrow> szip \<cdot> (x ## xs) \<cdot> (y ## ys) = (x, y) ## szip \<cdot> xs \<cdot> ys" 146 147lemma szip_UU1 [simp]: "szip \<cdot> UU \<cdot> y = UU" 148 by fixrec_simp 149 150lemma szip_UU2 [simp]: "x \<noteq> nil \<Longrightarrow> szip \<cdot> x \<cdot> UU = UU" 151 by (cases x) (simp_all, fixrec_simp) 152 153 154subsection \<open>\<open>scons\<close>, \<open>nil\<close>\<close> 155 156lemma scons_inject_eq: "x \<noteq> UU \<Longrightarrow> y \<noteq> UU \<Longrightarrow> x ## xs = y ## ys \<longleftrightarrow> x = y \<and> xs = ys" 157 by simp 158 159lemma nil_less_is_nil: "nil \<sqsubseteq> x \<Longrightarrow> nil = x" 160 by (cases x) simp_all 161 162 163subsection \<open>\<open>sfilter\<close>, \<open>sforall\<close>, \<open>sconc\<close>\<close> 164 165lemma if_and_sconc [simp]: 166 "(if b then tr1 else tr2) @@ tr = (if b then tr1 @@ tr else tr2 @@ tr)" 167 by simp 168 169lemma sfiltersconc: "sfilter \<cdot> P \<cdot> (x @@ y) = (sfilter \<cdot> P \<cdot> x @@ sfilter \<cdot> P \<cdot> y)" 170 apply (induct x) 171 text \<open>adm\<close> 172 apply simp 173 text \<open>base cases\<close> 174 apply simp 175 apply simp 176 text \<open>main case\<close> 177 apply (rule_tac p = "P\<cdot>a" in trE) 178 apply simp 179 apply simp 180 apply simp 181 done 182 183lemma sforallPstakewhileP: "sforall P (stakewhile \<cdot> P \<cdot> x)" 184 apply (simp add: sforall_def) 185 apply (induct x) 186 text \<open>adm\<close> 187 apply simp 188 text \<open>base cases\<close> 189 apply simp 190 apply simp 191 text \<open>main case\<close> 192 apply (rule_tac p = "P\<cdot>a" in trE) 193 apply simp 194 apply simp 195 apply simp 196 done 197 198lemma forallPsfilterP: "sforall P (sfilter \<cdot> P \<cdot> x)" 199 apply (simp add: sforall_def) 200 apply (induct x) 201 text \<open>adm\<close> 202 apply simp 203 text \<open>base cases\<close> 204 apply simp 205 apply simp 206 text \<open>main case\<close> 207 apply (rule_tac p="P\<cdot>a" in trE) 208 apply simp 209 apply simp 210 apply simp 211 done 212 213 214subsection \<open>Finite\<close> 215 216(* 217 Proofs of rewrite rules for Finite: 218 1. Finite nil (by definition) 219 2. \<not> Finite UU 220 3. a \<noteq> UU \<Longrightarrow> Finite (a ## x) = Finite x 221*) 222 223lemma Finite_UU_a: "Finite x \<longrightarrow> x \<noteq> UU" 224 apply (rule impI) 225 apply (erule Finite.induct) 226 apply simp 227 apply simp 228 done 229 230lemma Finite_UU [simp]: "\<not> Finite UU" 231 using Finite_UU_a [where x = UU] by fast 232 233lemma Finite_cons_a: "Finite x \<longrightarrow> a \<noteq> UU \<longrightarrow> x = a ## xs \<longrightarrow> Finite xs" 234 apply (intro strip) 235 apply (erule Finite.cases) 236 apply fastforce 237 apply simp 238 done 239 240lemma Finite_cons: "a \<noteq> UU \<Longrightarrow> Finite (a##x) \<longleftrightarrow> Finite x" 241 apply (rule iffI) 242 apply (erule (1) Finite_cons_a [rule_format]) 243 apply fast 244 apply simp 245 done 246 247lemma Finite_upward: "Finite x \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> Finite y" 248 apply (induct arbitrary: y set: Finite) 249 apply (case_tac y, simp, simp, simp) 250 apply (case_tac y, simp, simp) 251 apply simp 252 done 253 254lemma adm_Finite [simp]: "adm Finite" 255 by (rule adm_upward) (rule Finite_upward) 256 257 258subsection \<open>Induction\<close> 259 260text \<open>Extensions to Induction Theorems.\<close> 261 262lemma seq_finite_ind_lemma: 263 assumes "\<And>n. P (seq_take n \<cdot> s)" 264 shows "seq_finite s \<longrightarrow> P s" 265 apply (unfold seq.finite_def) 266 apply (intro strip) 267 apply (erule exE) 268 apply (erule subst) 269 apply (rule assms) 270 done 271 272lemma seq_finite_ind: 273 assumes "P UU" 274 and "P nil" 275 and "\<And>x s1. x \<noteq> UU \<Longrightarrow> P s1 \<Longrightarrow> P (x ## s1)" 276 shows "seq_finite s \<longrightarrow> P s" 277 apply (insert assms) 278 apply (rule seq_finite_ind_lemma) 279 apply (erule seq.finite_induct) 280 apply assumption 281 apply simp 282 done 283 284end 285