1(* Title: HOL/HOLCF/IOA/Sequence.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Sequences over flat domains with lifted elements\<close> 6 7theory Sequence 8imports Seq 9begin 10 11default_sort type 12 13type_synonym 'a Seq = "'a lift seq" 14 15definition Consq :: "'a \<Rightarrow> 'a Seq \<rightarrow> 'a Seq" 16 where "Consq a = (LAM s. Def a ## s)" 17 18definition Filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq" 19 where "Filter P = sfilter \<cdot> (flift2 P)" 20 21definition Map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Seq \<rightarrow> 'b Seq" 22 where "Map f = smap \<cdot> (flift2 f)" 23 24definition Forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool" 25 where "Forall P = sforall (flift2 P)" 26 27definition Last :: "'a Seq \<rightarrow> 'a lift" 28 where "Last = slast" 29 30definition Dropwhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq" 31 where "Dropwhile P = sdropwhile \<cdot> (flift2 P)" 32 33definition Takewhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq" 34 where "Takewhile P = stakewhile \<cdot> (flift2 P)" 35 36definition Zip :: "'a Seq \<rightarrow> 'b Seq \<rightarrow> ('a * 'b) Seq" 37 where "Zip = 38 (fix \<cdot> (LAM h t1 t2. 39 case t1 of 40 nil \<Rightarrow> nil 41 | x ## xs \<Rightarrow> 42 (case t2 of 43 nil \<Rightarrow> UU 44 | y ## ys \<Rightarrow> 45 (case x of 46 UU \<Rightarrow> UU 47 | Def a \<Rightarrow> 48 (case y of 49 UU \<Rightarrow> UU 50 | Def b \<Rightarrow> Def (a, b) ## (h \<cdot> xs \<cdot> ys))))))" 51 52definition Flat :: "'a Seq seq \<rightarrow> 'a Seq" 53 where "Flat = sflat" 54 55definition Filter2 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq" 56 where "Filter2 P = 57 (fix \<cdot> 58 (LAM h t. 59 case t of 60 nil \<Rightarrow> nil 61 | x ## xs \<Rightarrow> 62 (case x of 63 UU \<Rightarrow> UU 64 | Def y \<Rightarrow> (if P y then x ## (h \<cdot> xs) else h \<cdot> xs))))" 65 66abbreviation Consq_syn ("(_/\<leadsto>_)" [66, 65] 65) 67 where "a \<leadsto> s \<equiv> Consq a \<cdot> s" 68 69 70subsection \<open>List enumeration\<close> 71 72syntax 73 "_totlist" :: "args \<Rightarrow> 'a Seq" ("[(_)!]") 74 "_partlist" :: "args \<Rightarrow> 'a Seq" ("[(_)?]") 75translations 76 "[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]" 77 "[x!]" \<rightleftharpoons> "x\<leadsto>nil" 78 "[x, xs?]" \<rightleftharpoons> "x \<leadsto> [xs?]" 79 "[x?]" \<rightleftharpoons> "x \<leadsto> CONST bottom" 80 81 82declare andalso_and [simp] 83declare andalso_or [simp] 84 85 86subsection \<open>Recursive equations of operators\<close> 87 88subsubsection \<open>Map\<close> 89 90lemma Map_UU: "Map f \<cdot> UU = UU" 91 by (simp add: Map_def) 92 93lemma Map_nil: "Map f \<cdot> nil = nil" 94 by (simp add: Map_def) 95 96lemma Map_cons: "Map f \<cdot> (x \<leadsto> xs) = (f x) \<leadsto> Map f \<cdot> xs" 97 by (simp add: Map_def Consq_def flift2_def) 98 99 100subsubsection \<open>Filter\<close> 101 102lemma Filter_UU: "Filter P \<cdot> UU = UU" 103 by (simp add: Filter_def) 104 105lemma Filter_nil: "Filter P \<cdot> nil = nil" 106 by (simp add: Filter_def) 107 108lemma Filter_cons: "Filter P \<cdot> (x \<leadsto> xs) = (if P x then x \<leadsto> (Filter P \<cdot> xs) else Filter P \<cdot> xs)" 109 by (simp add: Filter_def Consq_def flift2_def If_and_if) 110 111 112subsubsection \<open>Forall\<close> 113 114lemma Forall_UU: "Forall P UU" 115 by (simp add: Forall_def sforall_def) 116 117lemma Forall_nil: "Forall P nil" 118 by (simp add: Forall_def sforall_def) 119 120lemma Forall_cons: "Forall P (x \<leadsto> xs) = (P x \<and> Forall P xs)" 121 by (simp add: Forall_def sforall_def Consq_def flift2_def) 122 123 124subsubsection \<open>Conc\<close> 125 126lemma Conc_cons: "(x \<leadsto> xs) @@ y = x \<leadsto> (xs @@ y)" 127 by (simp add: Consq_def) 128 129 130subsubsection \<open>Takewhile\<close> 131 132lemma Takewhile_UU: "Takewhile P \<cdot> UU = UU" 133 by (simp add: Takewhile_def) 134 135lemma Takewhile_nil: "Takewhile P \<cdot> nil = nil" 136 by (simp add: Takewhile_def) 137 138lemma Takewhile_cons: 139 "Takewhile P \<cdot> (x \<leadsto> xs) = (if P x then x \<leadsto> (Takewhile P \<cdot> xs) else nil)" 140 by (simp add: Takewhile_def Consq_def flift2_def If_and_if) 141 142 143subsubsection \<open>DropWhile\<close> 144 145lemma Dropwhile_UU: "Dropwhile P \<cdot> UU = UU" 146 by (simp add: Dropwhile_def) 147 148lemma Dropwhile_nil: "Dropwhile P \<cdot> nil = nil" 149 by (simp add: Dropwhile_def) 150 151lemma Dropwhile_cons: "Dropwhile P \<cdot> (x \<leadsto> xs) = (if P x then Dropwhile P \<cdot> xs else x \<leadsto> xs)" 152 by (simp add: Dropwhile_def Consq_def flift2_def If_and_if) 153 154 155subsubsection \<open>Last\<close> 156 157lemma Last_UU: "Last \<cdot> UU = UU" 158 by (simp add: Last_def) 159 160lemma Last_nil: "Last \<cdot> nil = UU" 161 by (simp add: Last_def) 162 163lemma Last_cons: "Last \<cdot> (x \<leadsto> xs) = (if xs = nil then Def x else Last \<cdot> xs)" 164 by (cases xs) (simp_all add: Last_def Consq_def) 165 166 167subsubsection \<open>Flat\<close> 168 169lemma Flat_UU: "Flat \<cdot> UU = UU" 170 by (simp add: Flat_def) 171 172lemma Flat_nil: "Flat \<cdot> nil = nil" 173 by (simp add: Flat_def) 174 175lemma Flat_cons: "Flat \<cdot> (x ## xs) = x @@ (Flat \<cdot> xs)" 176 by (simp add: Flat_def Consq_def) 177 178 179subsubsection \<open>Zip\<close> 180 181lemma Zip_unfold: 182 "Zip = 183 (LAM t1 t2. 184 case t1 of 185 nil \<Rightarrow> nil 186 | x ## xs \<Rightarrow> 187 (case t2 of 188 nil \<Rightarrow> UU 189 | y ## ys \<Rightarrow> 190 (case x of 191 UU \<Rightarrow> UU 192 | Def a \<Rightarrow> 193 (case y of 194 UU \<Rightarrow> UU 195 | Def b \<Rightarrow> Def (a, b) ## (Zip \<cdot> xs \<cdot> ys)))))" 196 apply (rule trans) 197 apply (rule fix_eq4) 198 apply (rule Zip_def) 199 apply (rule beta_cfun) 200 apply simp 201 done 202 203lemma Zip_UU1: "Zip \<cdot> UU \<cdot> y = UU" 204 apply (subst Zip_unfold) 205 apply simp 206 done 207 208lemma Zip_UU2: "x \<noteq> nil \<Longrightarrow> Zip \<cdot> x \<cdot> UU = UU" 209 apply (subst Zip_unfold) 210 apply simp 211 apply (cases x) 212 apply simp_all 213 done 214 215lemma Zip_nil: "Zip \<cdot> nil \<cdot> y = nil" 216 apply (subst Zip_unfold) 217 apply simp 218 done 219 220lemma Zip_cons_nil: "Zip \<cdot> (x \<leadsto> xs) \<cdot> nil = UU" 221 apply (subst Zip_unfold) 222 apply (simp add: Consq_def) 223 done 224 225lemma Zip_cons: "Zip \<cdot> (x \<leadsto> xs) \<cdot> (y \<leadsto> ys) = (x, y) \<leadsto> Zip \<cdot> xs \<cdot> ys" 226 apply (rule trans) 227 apply (subst Zip_unfold) 228 apply simp 229 apply (simp add: Consq_def) 230 done 231 232lemmas [simp del] = 233 sfilter_UU sfilter_nil sfilter_cons 234 smap_UU smap_nil smap_cons 235 sforall2_UU sforall2_nil sforall2_cons 236 slast_UU slast_nil slast_cons 237 stakewhile_UU stakewhile_nil stakewhile_cons 238 sdropwhile_UU sdropwhile_nil sdropwhile_cons 239 sflat_UU sflat_nil sflat_cons 240 szip_UU1 szip_UU2 szip_nil szip_cons_nil szip_cons 241 242lemmas [simp] = 243 Filter_UU Filter_nil Filter_cons 244 Map_UU Map_nil Map_cons 245 Forall_UU Forall_nil Forall_cons 246 Last_UU Last_nil Last_cons 247 Conc_cons 248 Takewhile_UU Takewhile_nil Takewhile_cons 249 Dropwhile_UU Dropwhile_nil Dropwhile_cons 250 Zip_UU1 Zip_UU2 Zip_nil Zip_cons_nil Zip_cons 251 252 253subsection \<open>Cons\<close> 254 255lemma Consq_def2: "a \<leadsto> s = Def a ## s" 256 by (simp add: Consq_def) 257 258lemma Seq_exhaust: "x = UU \<or> x = nil \<or> (\<exists>a s. x = a \<leadsto> s)" 259 apply (simp add: Consq_def2) 260 apply (cut_tac seq.nchotomy) 261 apply (fast dest: not_Undef_is_Def [THEN iffD1]) 262 done 263 264lemma Seq_cases: obtains "x = UU" | "x = nil" | a s where "x = a \<leadsto> s" 265 apply (cut_tac x="x" in Seq_exhaust) 266 apply (erule disjE) 267 apply simp 268 apply (erule disjE) 269 apply simp 270 apply (erule exE)+ 271 apply simp 272 done 273 274lemma Cons_not_UU: "a \<leadsto> s \<noteq> UU" 275 apply (subst Consq_def2) 276 apply simp 277 done 278 279lemma Cons_not_less_UU: "\<not> (a \<leadsto> x) \<sqsubseteq> UU" 280 apply (rule notI) 281 apply (drule below_antisym) 282 apply simp 283 apply (simp add: Cons_not_UU) 284 done 285 286lemma Cons_not_less_nil: "\<not> a \<leadsto> s \<sqsubseteq> nil" 287 by (simp add: Consq_def2) 288 289lemma Cons_not_nil: "a \<leadsto> s \<noteq> nil" 290 by (simp add: Consq_def2) 291 292lemma Cons_not_nil2: "nil \<noteq> a \<leadsto> s" 293 by (simp add: Consq_def2) 294 295lemma Cons_inject_eq: "a \<leadsto> s = b \<leadsto> t \<longleftrightarrow> a = b \<and> s = t" 296 by (simp add: Consq_def2 scons_inject_eq) 297 298lemma Cons_inject_less_eq: "a \<leadsto> s \<sqsubseteq> b \<leadsto> t \<longleftrightarrow> a = b \<and> s \<sqsubseteq> t" 299 by (simp add: Consq_def2) 300 301lemma seq_take_Cons: "seq_take (Suc n) \<cdot> (a \<leadsto> x) = a \<leadsto> (seq_take n \<cdot> x)" 302 by (simp add: Consq_def) 303 304lemmas [simp] = 305 Cons_not_nil2 Cons_inject_eq Cons_inject_less_eq seq_take_Cons 306 Cons_not_UU Cons_not_less_UU Cons_not_less_nil Cons_not_nil 307 308 309subsection \<open>Induction\<close> 310 311lemma Seq_induct: 312 assumes "adm P" 313 and "P UU" 314 and "P nil" 315 and "\<And>a s. P s \<Longrightarrow> P (a \<leadsto> s)" 316 shows "P x" 317 apply (insert assms) 318 apply (erule (2) seq.induct) 319 apply defined 320 apply (simp add: Consq_def) 321 done 322 323lemma Seq_FinitePartial_ind: 324 assumes "P UU" 325 and "P nil" 326 and "\<And>a s. P s \<Longrightarrow> P (a \<leadsto> s)" 327 shows "seq_finite x \<longrightarrow> P x" 328 apply (insert assms) 329 apply (erule (1) seq_finite_ind) 330 apply defined 331 apply (simp add: Consq_def) 332 done 333 334lemma Seq_Finite_ind: 335 assumes "Finite x" 336 and "P nil" 337 and "\<And>a s. Finite s \<Longrightarrow> P s \<Longrightarrow> P (a \<leadsto> s)" 338 shows "P x" 339 apply (insert assms) 340 apply (erule (1) Finite.induct) 341 apply defined 342 apply (simp add: Consq_def) 343 done 344 345 346subsection \<open>\<open>HD\<close> and \<open>TL\<close>\<close> 347 348lemma HD_Cons [simp]: "HD \<cdot> (x \<leadsto> y) = Def x" 349 by (simp add: Consq_def) 350 351lemma TL_Cons [simp]: "TL \<cdot> (x \<leadsto> y) = y" 352 by (simp add: Consq_def) 353 354 355subsection \<open>\<open>Finite\<close>, \<open>Partial\<close>, \<open>Infinite\<close>\<close> 356 357lemma Finite_Cons [simp]: "Finite (a \<leadsto> xs) = Finite xs" 358 by (simp add: Consq_def2 Finite_cons) 359 360lemma FiniteConc_1: "Finite (x::'a Seq) \<Longrightarrow> Finite y \<longrightarrow> Finite (x @@ y)" 361 apply (erule Seq_Finite_ind) 362 apply simp_all 363 done 364 365lemma FiniteConc_2: "Finite (z::'a Seq) \<Longrightarrow> \<forall>x y. z = x @@ y \<longrightarrow> Finite x \<and> Finite y" 366 apply (erule Seq_Finite_ind) 367 text \<open>\<open>nil\<close>\<close> 368 apply (intro strip) 369 apply (rule_tac x="x" in Seq_cases, simp_all) 370 text \<open>\<open>cons\<close>\<close> 371 apply (intro strip) 372 apply (rule_tac x="x" in Seq_cases, simp_all) 373 apply (rule_tac x="y" in Seq_cases, simp_all) 374 done 375 376lemma FiniteConc [simp]: "Finite (x @@ y) \<longleftrightarrow> Finite (x::'a Seq) \<and> Finite y" 377 apply (rule iffI) 378 apply (erule FiniteConc_2 [rule_format]) 379 apply (rule refl) 380 apply (rule FiniteConc_1 [rule_format]) 381 apply auto 382 done 383 384 385lemma FiniteMap1: "Finite s \<Longrightarrow> Finite (Map f \<cdot> s)" 386 apply (erule Seq_Finite_ind) 387 apply simp_all 388 done 389 390lemma FiniteMap2: "Finite s \<Longrightarrow> \<forall>t. s = Map f \<cdot> t \<longrightarrow> Finite t" 391 apply (erule Seq_Finite_ind) 392 apply (intro strip) 393 apply (rule_tac x="t" in Seq_cases, simp_all) 394 text \<open>\<open>main case\<close>\<close> 395 apply auto 396 apply (rule_tac x="t" in Seq_cases, simp_all) 397 done 398 399lemma Map2Finite: "Finite (Map f \<cdot> s) = Finite s" 400 apply auto 401 apply (erule FiniteMap2 [rule_format]) 402 apply (rule refl) 403 apply (erule FiniteMap1) 404 done 405 406 407lemma FiniteFilter: "Finite s \<Longrightarrow> Finite (Filter P \<cdot> s)" 408 apply (erule Seq_Finite_ind) 409 apply simp_all 410 done 411 412 413subsection \<open>\<open>Conc\<close>\<close> 414 415lemma Conc_cong: "\<And>x::'a Seq. Finite x \<Longrightarrow> (x @@ y) = (x @@ z) \<longleftrightarrow> y = z" 416 apply (erule Seq_Finite_ind) 417 apply simp_all 418 done 419 420lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z" 421 apply (rule_tac x="x" in Seq_induct) 422 apply simp_all 423 done 424 425lemma nilConc [simp]: "s@@ nil = s" 426 apply (induct s) 427 apply simp 428 apply simp 429 apply simp 430 apply simp 431 done 432 433 434(*Should be same as nil_is_Conc2 when all nils are turned to right side!*) 435lemma nil_is_Conc: "nil = x @@ y \<longleftrightarrow> (x::'a Seq) = nil \<and> y = nil" 436 apply (rule_tac x="x" in Seq_cases) 437 apply auto 438 done 439 440lemma nil_is_Conc2: "x @@ y = nil \<longleftrightarrow> (x::'a Seq) = nil \<and> y = nil" 441 apply (rule_tac x="x" in Seq_cases) 442 apply auto 443 done 444 445 446subsection \<open>Last\<close> 447 448lemma Finite_Last1: "Finite s \<Longrightarrow> s \<noteq> nil \<longrightarrow> Last \<cdot> s \<noteq> UU" 449 by (erule Seq_Finite_ind) simp_all 450 451lemma Finite_Last2: "Finite s \<Longrightarrow> Last \<cdot> s = UU \<longrightarrow> s = nil" 452 by (erule Seq_Finite_ind) auto 453 454 455subsection \<open>Filter, Conc\<close> 456 457lemma FilterPQ: "Filter P \<cdot> (Filter Q \<cdot> s) = Filter (\<lambda>x. P x \<and> Q x) \<cdot> s" 458 by (rule_tac x="s" in Seq_induct) simp_all 459 460lemma FilterConc: "Filter P \<cdot> (x @@ y) = (Filter P \<cdot> x @@ Filter P \<cdot> y)" 461 by (simp add: Filter_def sfiltersconc) 462 463 464subsection \<open>Map\<close> 465 466lemma MapMap: "Map f \<cdot> (Map g \<cdot> s) = Map (f \<circ> g) \<cdot> s" 467 by (rule_tac x="s" in Seq_induct) simp_all 468 469lemma MapConc: "Map f \<cdot> (x @@ y) = (Map f \<cdot> x) @@ (Map f \<cdot> y)" 470 by (rule_tac x="x" in Seq_induct) simp_all 471 472lemma MapFilter: "Filter P \<cdot> (Map f \<cdot> x) = Map f \<cdot> (Filter (P \<circ> f) \<cdot> x)" 473 by (rule_tac x="x" in Seq_induct) simp_all 474 475lemma nilMap: "nil = (Map f \<cdot> s) \<longrightarrow> s = nil" 476 by (rule_tac x="s" in Seq_cases) simp_all 477 478lemma ForallMap: "Forall P (Map f \<cdot> s) = Forall (P \<circ> f) s" 479 apply (rule_tac x="s" in Seq_induct) 480 apply (simp add: Forall_def sforall_def) 481 apply simp_all 482 done 483 484 485subsection \<open>Forall\<close> 486 487lemma ForallPForallQ1: "Forall P ys \<and> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> Forall Q ys" 488 apply (rule_tac x="ys" in Seq_induct) 489 apply (simp add: Forall_def sforall_def) 490 apply simp_all 491 done 492 493lemmas ForallPForallQ = 494 ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI] 495 496lemma Forall_Conc_impl: "Forall P x \<and> Forall P y \<longrightarrow> Forall P (x @@ y)" 497 apply (rule_tac x="x" in Seq_induct) 498 apply (simp add: Forall_def sforall_def) 499 apply simp_all 500 done 501 502lemma Forall_Conc [simp]: "Finite x \<Longrightarrow> Forall P (x @@ y) \<longleftrightarrow> Forall P x \<and> Forall P y" 503 by (erule Seq_Finite_ind) simp_all 504 505lemma ForallTL1: "Forall P s \<longrightarrow> Forall P (TL \<cdot> s)" 506 apply (rule_tac x="s" in Seq_induct) 507 apply (simp add: Forall_def sforall_def) 508 apply simp_all 509 done 510 511lemmas ForallTL = ForallTL1 [THEN mp] 512 513lemma ForallDropwhile1: "Forall P s \<longrightarrow> Forall P (Dropwhile Q \<cdot> s)" 514 apply (rule_tac x="s" in Seq_induct) 515 apply (simp add: Forall_def sforall_def) 516 apply simp_all 517 done 518 519lemmas ForallDropwhile = ForallDropwhile1 [THEN mp] 520 521 522(*only admissible in t, not if done in s*) 523lemma Forall_prefix: "\<forall>s. Forall P s \<longrightarrow> t \<sqsubseteq> s \<longrightarrow> Forall P t" 524 apply (rule_tac x="t" in Seq_induct) 525 apply (simp add: Forall_def sforall_def) 526 apply simp_all 527 apply (intro strip) 528 apply (rule_tac x="sa" in Seq_cases) 529 apply simp 530 apply auto 531 done 532 533lemmas Forall_prefixclosed = Forall_prefix [rule_format] 534 535lemma Forall_postfixclosed: "Finite h \<Longrightarrow> Forall P s \<Longrightarrow> s= h @@ t \<Longrightarrow> Forall P t" 536 by auto 537 538 539lemma ForallPFilterQR1: 540 "(\<forall>x. P x \<longrightarrow> Q x = R x) \<and> Forall P tr \<longrightarrow> Filter Q \<cdot> tr = Filter R \<cdot> tr" 541 apply (rule_tac x="tr" in Seq_induct) 542 apply (simp add: Forall_def sforall_def) 543 apply simp_all 544 done 545 546lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI] 547 548 549subsection \<open>Forall, Filter\<close> 550 551lemma ForallPFilterP: "Forall P (Filter P \<cdot> x)" 552 by (simp add: Filter_def Forall_def forallPsfilterP) 553 554(*holds also in other direction, then equal to forallPfilterP*) 555lemma ForallPFilterPid1: "Forall P x \<longrightarrow> Filter P \<cdot> x = x" 556 apply (rule_tac x="x" in Seq_induct) 557 apply (simp add: Forall_def sforall_def Filter_def) 558 apply simp_all 559 done 560 561lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp] 562 563(*holds also in other direction*) 564lemma ForallnPFilterPnil1: "Finite ys \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P \<cdot> ys = nil" 565 by (erule Seq_Finite_ind) simp_all 566 567lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp] 568 569 570(*holds also in other direction*) 571lemma ForallnPFilterPUU1: "\<not> Finite ys \<and> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P \<cdot> ys = UU" 572 apply (rule_tac x="ys" in Seq_induct) 573 apply (simp add: Forall_def sforall_def) 574 apply simp_all 575 done 576 577lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI] 578 579 580(*inverse of ForallnPFilterPnil*) 581lemma FilternPnilForallP [rule_format]: "Filter P \<cdot> ys = nil \<longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<and> Finite ys" 582 apply (rule_tac x="ys" in Seq_induct) 583 text \<open>adm\<close> 584 apply (simp add: Forall_def sforall_def) 585 text \<open>base cases\<close> 586 apply simp 587 apply simp 588 text \<open>main case\<close> 589 apply simp 590 done 591 592(*inverse of ForallnPFilterPUU*) 593lemma FilternPUUForallP: 594 assumes "Filter P \<cdot> ys = UU" 595 shows "Forall (\<lambda>x. \<not> P x) ys \<and> \<not> Finite ys" 596proof 597 show "Forall (\<lambda>x. \<not> P x) ys" 598 proof (rule classical) 599 assume "\<not> ?thesis" 600 then have "Filter P \<cdot> ys \<noteq> UU" 601 apply (rule rev_mp) 602 apply (induct ys rule: Seq_induct) 603 apply (simp add: Forall_def sforall_def) 604 apply simp_all 605 done 606 with assms show ?thesis by contradiction 607 qed 608 show "\<not> Finite ys" 609 proof 610 assume "Finite ys" 611 then have "Filter P\<cdot>ys \<noteq> UU" 612 by (rule Seq_Finite_ind) simp_all 613 with assms show False by contradiction 614 qed 615qed 616 617 618lemma ForallQFilterPnil: 619 "Forall Q ys \<Longrightarrow> Finite ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P \<cdot> ys = nil" 620 apply (erule ForallnPFilterPnil) 621 apply (erule ForallPForallQ) 622 apply auto 623 done 624 625lemma ForallQFilterPUU: "\<not> Finite ys \<Longrightarrow> Forall Q ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P \<cdot> ys = UU" 626 apply (erule ForallnPFilterPUU) 627 apply (erule ForallPForallQ) 628 apply auto 629 done 630 631 632subsection \<open>Takewhile, Forall, Filter\<close> 633 634lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P \<cdot> x)" 635 by (simp add: Forall_def Takewhile_def sforallPstakewhileP) 636 637 638lemma ForallPTakewhileQ [simp]: "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Forall P (Takewhile Q \<cdot> x)" 639 apply (rule ForallPForallQ) 640 apply (rule ForallPTakewhileP) 641 apply auto 642 done 643 644 645lemma FilterPTakewhileQnil [simp]: 646 "Finite (Takewhile Q \<cdot> ys) \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P \<cdot> (Takewhile Q \<cdot> ys) = nil" 647 apply (erule ForallnPFilterPnil) 648 apply (rule ForallPForallQ) 649 apply (rule ForallPTakewhileP) 650 apply auto 651 done 652 653lemma FilterPTakewhileQid [simp]: 654 "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Filter P \<cdot> (Takewhile Q \<cdot> ys) = Takewhile Q \<cdot> ys" 655 apply (rule ForallPFilterPid) 656 apply (rule ForallPForallQ) 657 apply (rule ForallPTakewhileP) 658 apply auto 659 done 660 661 662lemma Takewhile_idempotent: "Takewhile P \<cdot> (Takewhile P \<cdot> s) = Takewhile P \<cdot> s" 663 apply (rule_tac x="s" in Seq_induct) 664 apply (simp add: Forall_def sforall_def) 665 apply simp_all 666 done 667 668lemma ForallPTakewhileQnP [simp]: 669 "Forall P s \<longrightarrow> Takewhile (\<lambda>x. Q x \<or> (\<not> P x)) \<cdot> s = Takewhile Q \<cdot> s" 670 apply (rule_tac x="s" in Seq_induct) 671 apply (simp add: Forall_def sforall_def) 672 apply simp_all 673 done 674 675lemma ForallPDropwhileQnP [simp]: 676 "Forall P s \<longrightarrow> Dropwhile (\<lambda>x. Q x \<or> (\<not> P x)) \<cdot> s = Dropwhile Q \<cdot> s" 677 apply (rule_tac x="s" in Seq_induct) 678 apply (simp add: Forall_def sforall_def) 679 apply simp_all 680 done 681 682 683lemma TakewhileConc1: "Forall P s \<longrightarrow> Takewhile P \<cdot> (s @@ t) = s @@ (Takewhile P \<cdot> t)" 684 apply (rule_tac x="s" in Seq_induct) 685 apply (simp add: Forall_def sforall_def) 686 apply simp_all 687 done 688 689lemmas TakewhileConc = TakewhileConc1 [THEN mp] 690 691lemma DropwhileConc1: "Finite s \<Longrightarrow> Forall P s \<longrightarrow> Dropwhile P \<cdot> (s @@ t) = Dropwhile P \<cdot> t" 692 by (erule Seq_Finite_ind) simp_all 693 694lemmas DropwhileConc = DropwhileConc1 [THEN mp] 695 696 697subsection \<open>Coinductive characterizations of Filter\<close> 698 699lemma divide_Seq_lemma: 700 "HD \<cdot> (Filter P \<cdot> y) = Def x \<longrightarrow> 701 y = (Takewhile (\<lambda>x. \<not> P x) \<cdot> y) @@ (x \<leadsto> TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> y)) \<and> 702 Finite (Takewhile (\<lambda>x. \<not> P x) \<cdot> y) \<and> P x" 703 (* FIX: pay attention: is only admissible with chain-finite package to be added to 704 adm test and Finite f x admissibility *) 705 apply (rule_tac x="y" in Seq_induct) 706 apply (simp add: adm_subst [OF _ adm_Finite]) 707 apply simp 708 apply simp 709 apply (case_tac "P a") 710 apply simp 711 apply blast 712 text \<open>\<open>\<not> P a\<close>\<close> 713 apply simp 714 done 715 716lemma divide_Seq: "(x \<leadsto> xs) \<sqsubseteq> Filter P \<cdot> y \<Longrightarrow> 717 y = ((Takewhile (\<lambda>a. \<not> P a) \<cdot> y) @@ (x \<leadsto> TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> y))) \<and> 718 Finite (Takewhile (\<lambda>a. \<not> P a) \<cdot> y) \<and> P x" 719 apply (rule divide_Seq_lemma [THEN mp]) 720 apply (drule_tac f="HD" and x="x \<leadsto> xs" in monofun_cfun_arg) 721 apply simp 722 done 723 724 725lemma nForall_HDFilter: "\<not> Forall P y \<longrightarrow> (\<exists>x. HD \<cdot> (Filter (\<lambda>a. \<not> P a) \<cdot> y) = Def x)" 726 unfolding not_Undef_is_Def [symmetric] 727 apply (induct y rule: Seq_induct) 728 apply (simp add: Forall_def sforall_def) 729 apply simp_all 730 done 731 732 733lemma divide_Seq2: 734 "\<not> Forall P y \<Longrightarrow> 735 \<exists>x. y = Takewhile P\<cdot>y @@ (x \<leadsto> TL \<cdot> (Dropwhile P \<cdot> y)) \<and> Finite (Takewhile P \<cdot> y) \<and> \<not> P x" 736 apply (drule nForall_HDFilter [THEN mp]) 737 apply safe 738 apply (rule_tac x="x" in exI) 739 apply (cut_tac P1="\<lambda>x. \<not> P x" in divide_Seq_lemma [THEN mp]) 740 apply auto 741 done 742 743 744lemma divide_Seq3: 745 "\<not> Forall P y \<Longrightarrow> \<exists>x bs rs. y = (bs @@ (x\<leadsto>rs)) \<and> Finite bs \<and> Forall P bs \<and> \<not> P x" 746 apply (drule divide_Seq2) 747 apply fastforce 748 done 749 750lemmas [simp] = FilterPQ FilterConc Conc_cong 751 752 753subsection \<open>Take-lemma\<close> 754 755lemma seq_take_lemma: "(\<forall>n. seq_take n \<cdot> x = seq_take n \<cdot> x') \<longleftrightarrow> x = x'" 756 apply (rule iffI) 757 apply (rule seq.take_lemma) 758 apply auto 759 done 760 761lemma take_reduction1: 762 "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k \<cdot> y1 = seq_take k \<cdot> y2) \<longrightarrow> 763 seq_take n \<cdot> (x @@ (t \<leadsto> y1)) = seq_take n \<cdot> (x @@ (t \<leadsto> y2)))" 764 apply (rule_tac x="x" in Seq_induct) 765 apply simp_all 766 apply (intro strip) 767 apply (case_tac "n") 768 apply auto 769 apply (case_tac "n") 770 apply auto 771 done 772 773lemma take_reduction: 774 "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k \<cdot> y1 = seq_take k \<cdot> y2) 775 \<Longrightarrow> seq_take n \<cdot> (x @@ (s \<leadsto> y1)) = seq_take n \<cdot> (y @@ (t \<leadsto> y2))" 776 by (auto intro!: take_reduction1 [rule_format]) 777 778 779text \<open> 780 Take-lemma and take-reduction for \<open>\<sqsubseteq>\<close> instead of \<open>=\<close>. 781\<close> 782 783lemma take_reduction_less1: 784 "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k \<cdot> y1 \<sqsubseteq> seq_take k\<cdot>y2) \<longrightarrow> 785 seq_take n \<cdot> (x @@ (t \<leadsto> y1)) \<sqsubseteq> seq_take n \<cdot> (x @@ (t \<leadsto> y2)))" 786 apply (rule_tac x="x" in Seq_induct) 787 apply simp_all 788 apply (intro strip) 789 apply (case_tac "n") 790 apply auto 791 apply (case_tac "n") 792 apply auto 793 done 794 795lemma take_reduction_less: 796 "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k \<cdot> y1 \<sqsubseteq> seq_take k \<cdot> y2) \<Longrightarrow> 797 seq_take n \<cdot> (x @@ (s \<leadsto> y1)) \<sqsubseteq> seq_take n \<cdot> (y @@ (t \<leadsto> y2))" 798 by (auto intro!: take_reduction_less1 [rule_format]) 799 800lemma take_lemma_less1: 801 assumes "\<And>n. seq_take n \<cdot> s1 \<sqsubseteq> seq_take n \<cdot> s2" 802 shows "s1 \<sqsubseteq> s2" 803 apply (rule_tac t="s1" in seq.reach [THEN subst]) 804 apply (rule_tac t="s2" in seq.reach [THEN subst]) 805 apply (rule lub_mono) 806 apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL]) 807 apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL]) 808 apply (rule assms) 809 done 810 811lemma take_lemma_less: "(\<forall>n. seq_take n \<cdot> x \<sqsubseteq> seq_take n \<cdot> x') \<longleftrightarrow> x \<sqsubseteq> x'" 812 apply (rule iffI) 813 apply (rule take_lemma_less1) 814 apply auto 815 apply (erule monofun_cfun_arg) 816 done 817 818 819text \<open>Take-lemma proof principles.\<close> 820 821lemma take_lemma_principle1: 822 assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s" 823 and "\<And>s1 s2 y. Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> 824 \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow> f (s1 @@ y \<leadsto> s2) = g (s1 @@ y \<leadsto> s2)" 825 shows "A x \<longrightarrow> f x = g x" 826 using assms by (cases "Forall Q x") (auto dest!: divide_Seq3) 827 828lemma take_lemma_principle2: 829 assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s" 830 and "\<And>s1 s2 y. Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow> 831 \<forall>n. seq_take n \<cdot> (f (s1 @@ y \<leadsto> s2)) = seq_take n \<cdot> (g (s1 @@ y \<leadsto> s2))" 832 shows "A x \<longrightarrow> f x = g x" 833 using assms 834 apply (cases "Forall Q x") 835 apply (auto dest!: divide_Seq3) 836 apply (rule seq.take_lemma) 837 apply auto 838 done 839 840 841text \<open> 842 Note: in the following proofs the ordering of proof steps is very important, 843 as otherwise either \<open>Forall Q s1\<close> would be in the IH as assumption (then 844 rule useless) or it is not possible to strengthen the IH apply doing a 845 forall closure of the sequence \<open>t\<close> (then rule also useless). This is also 846 the reason why the induction rule (\<open>nat_less_induct\<close> or \<open>nat_induct\<close>) has to 847 to be imbuilt into the rule, as induction has to be done early and the take 848 lemma has to be used in the trivial direction afterwards for the 849 \<open>Forall Q x\<close> case. 850\<close> 851 852lemma take_lemma_induct: 853 assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s" 854 and "\<And>s1 s2 y n. 855 \<forall>t. A t \<longrightarrow> seq_take n \<cdot> (f t) = seq_take n \<cdot> (g t) \<Longrightarrow> 856 Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow> 857 seq_take (Suc n) \<cdot> (f (s1 @@ y \<leadsto> s2)) = 858 seq_take (Suc n) \<cdot> (g (s1 @@ y \<leadsto> s2))" 859 shows "A x \<longrightarrow> f x = g x" 860 apply (insert assms) 861 apply (rule impI) 862 apply (rule seq.take_lemma) 863 apply (rule mp) 864 prefer 2 apply assumption 865 apply (rule_tac x="x" in spec) 866 apply (rule nat.induct) 867 apply simp 868 apply (rule allI) 869 apply (case_tac "Forall Q xa") 870 apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec]) 871 apply (auto dest!: divide_Seq3) 872 done 873 874 875lemma take_lemma_less_induct: 876 assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s" 877 and "\<And>s1 s2 y n. 878 \<forall>t m. m < n \<longrightarrow> A t \<longrightarrow> seq_take m \<cdot> (f t) = seq_take m \<cdot> (g t) \<Longrightarrow> 879 Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow> 880 seq_take n \<cdot> (f (s1 @@ y \<leadsto> s2)) = 881 seq_take n \<cdot> (g (s1 @@ y \<leadsto> s2))" 882 shows "A x \<longrightarrow> f x = g x" 883 apply (insert assms) 884 apply (rule impI) 885 apply (rule seq.take_lemma) 886 apply (rule mp) 887 prefer 2 apply assumption 888 apply (rule_tac x="x" in spec) 889 apply (rule nat_less_induct) 890 apply (rule allI) 891 apply (case_tac "Forall Q xa") 892 apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec]) 893 apply (auto dest!: divide_Seq3) 894 done 895 896 897 898lemma take_lemma_in_eq_out: 899 assumes "A UU \<Longrightarrow> f UU = g UU" 900 and "A nil \<Longrightarrow> f nil = g nil" 901 and "\<And>s y n. 902 \<forall>t. A t \<longrightarrow> seq_take n \<cdot> (f t) = seq_take n \<cdot> (g t) \<Longrightarrow> A (y \<leadsto> s) \<Longrightarrow> 903 seq_take (Suc n) \<cdot> (f (y \<leadsto> s)) = 904 seq_take (Suc n) \<cdot> (g (y \<leadsto> s))" 905 shows "A x \<longrightarrow> f x = g x" 906 apply (insert assms) 907 apply (rule impI) 908 apply (rule seq.take_lemma) 909 apply (rule mp) 910 prefer 2 apply assumption 911 apply (rule_tac x="x" in spec) 912 apply (rule nat.induct) 913 apply simp 914 apply (rule allI) 915 apply (rule_tac x="xa" in Seq_cases) 916 apply simp_all 917 done 918 919 920subsection \<open>Alternative take_lemma proofs\<close> 921 922subsubsection \<open>Alternative Proof of FilterPQ\<close> 923 924declare FilterPQ [simp del] 925 926 927(*In general: How to do this case without the same adm problems 928 as for the entire proof?*) 929lemma Filter_lemma1: 930 "Forall (\<lambda>x. \<not> (P x \<and> Q x)) s \<longrightarrow> 931 Filter P \<cdot> (Filter Q \<cdot> s) = Filter (\<lambda>x. P x \<and> Q x) \<cdot> s" 932 apply (rule_tac x="s" in Seq_induct) 933 apply (simp add: Forall_def sforall_def) 934 apply simp_all 935 done 936 937lemma Filter_lemma2: "Finite s \<Longrightarrow> 938 Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter P \<cdot> (Filter Q \<cdot> s) = nil" 939 by (erule Seq_Finite_ind) simp_all 940 941lemma Filter_lemma3: "Finite s \<Longrightarrow> 942 Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter (\<lambda>x. P x \<and> Q x) \<cdot> s = nil" 943 by (erule Seq_Finite_ind) simp_all 944 945lemma FilterPQ_takelemma: "Filter P \<cdot> (Filter Q \<cdot> s) = Filter (\<lambda>x. P x \<and> Q x) \<cdot> s" 946 apply (rule_tac A1="\<lambda>x. True" and Q1="\<lambda>x. \<not> (P x \<and> Q x)" and x1="s" in 947 take_lemma_induct [THEN mp]) 948 (*better support for A = \<lambda>x. True*) 949 apply (simp add: Filter_lemma1) 950 apply (simp add: Filter_lemma2 Filter_lemma3) 951 apply simp 952 done 953 954declare FilterPQ [simp] 955 956 957subsubsection \<open>Alternative Proof of \<open>MapConc\<close>\<close> 958 959lemma MapConc_takelemma: "Map f \<cdot> (x @@ y) = (Map f \<cdot> x) @@ (Map f \<cdot> y)" 960 apply (rule_tac A1="\<lambda>x. True" and x1="x" in take_lemma_in_eq_out [THEN mp]) 961 apply auto 962 done 963 964ML \<open> 965fun Seq_case_tac ctxt s i = 966 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i 967 THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i + 1) THEN hyp_subst_tac ctxt (i + 2); 968 969(* on a\<leadsto>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) 970fun Seq_case_simp_tac ctxt s i = 971 Seq_case_tac ctxt s i 972 THEN asm_simp_tac ctxt (i + 2) 973 THEN asm_full_simp_tac ctxt (i + 1) 974 THEN asm_full_simp_tac ctxt i; 975 976(* rws are definitions to be unfolded for admissibility check *) 977fun Seq_induct_tac ctxt s rws i = 978 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i 979 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i + 1)))) 980 THEN simp_tac (ctxt addsimps rws) i; 981 982fun Seq_Finite_induct_tac ctxt i = 983 eresolve_tac ctxt @{thms Seq_Finite_ind} i 984 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i))); 985 986fun pair_tac ctxt s = 987 Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm prod.exhaust} 988 THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt; 989 990(* induction on a sequence of pairs with pairsplitting and simplification *) 991fun pair_induct_tac ctxt s rws i = 992 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i 993 THEN pair_tac ctxt "a" (i + 3) 994 THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i + 1)))) 995 THEN simp_tac (ctxt addsimps rws) i; 996\<close> 997 998method_setup Seq_case = 999 \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close> 1000 1001method_setup Seq_case_simp = 1002 \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close> 1003 1004method_setup Seq_induct = 1005 \<open>Scan.lift Args.embedded -- 1006 Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) [] 1007 >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))\<close> 1008 1009method_setup Seq_Finite_induct = 1010 \<open>Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\<close> 1011 1012method_setup pair = 1013 \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close> 1014 1015method_setup pair_induct = 1016 \<open>Scan.lift Args.embedded -- 1017 Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) [] 1018 >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close> 1019 1020lemma Mapnil: "Map f \<cdot> s = nil \<longleftrightarrow> s = nil" 1021 by (Seq_case_simp s) 1022 1023lemma MapUU: "Map f \<cdot> s = UU \<longleftrightarrow> s = UU" 1024 by (Seq_case_simp s) 1025 1026lemma MapTL: "Map f \<cdot> (TL \<cdot> s) = TL \<cdot> (Map f \<cdot> s)" 1027 by (Seq_induct s) 1028 1029end 1030