79 by (insert stream.injects [of a s b t], auto) |
79 by (insert stream.injects [of a s b t], auto) |
80 |
80 |
81 lemma stream_prefix: |
81 lemma stream_prefix: |
82 "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt" |
82 "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt" |
83 apply (insert stream.exhaust [of t], auto) |
83 apply (insert stream.exhaust [of t], auto) |
84 apply (drule eq_UU_iff [THEN iffD2], simp) |
|
85 by (drule stream.inverts, auto) |
84 by (drule stream.inverts, auto) |
86 |
85 |
87 lemma stream_prefix': |
86 lemma stream_prefix': |
88 "b ~= UU ==> x << b && z = |
87 "b ~= UU ==> x << b && z = |
89 (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))" |
88 (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))" |
98 *) |
97 *) |
99 |
98 |
100 lemma stream_flat_prefix: |
99 lemma stream_flat_prefix: |
101 "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" |
100 "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" |
102 apply (case_tac "y=UU",auto) |
101 apply (case_tac "y=UU",auto) |
103 apply (drule eq_UU_iff [THEN iffD2],auto) |
|
104 apply (drule stream.inverts,auto) |
102 apply (drule stream.inverts,auto) |
105 apply (drule ax_flat [rule_format],simp) |
103 apply (drule ax_flat [rule_format],simp) |
106 by (drule stream.inverts,auto) |
104 by (drule stream.inverts,auto) |
107 |
105 |
108 |
106 |
321 apply (rule stream.casedist [of s], auto) |
319 apply (rule stream.casedist [of s], auto) |
322 apply (rule stream_finite_lemma1, simp) |
320 apply (rule stream_finite_lemma1, simp) |
323 by (rule stream_finite_lemma2,simp) |
321 by (rule stream_finite_lemma2,simp) |
324 |
322 |
325 lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t" |
323 lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t" |
326 apply (erule stream_finite_ind [of s]) |
324 apply (erule stream_finite_ind [of s], auto) |
327 apply (clarsimp, drule eq_UU_iff [THEN iffD2], auto) |
|
328 apply (case_tac "t=UU", auto) |
325 apply (case_tac "t=UU", auto) |
329 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
326 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
330 apply (drule stream.inverts, auto) |
327 apply (drule stream.inverts, auto) |
331 apply (erule_tac x="y" in allE, simp) |
328 apply (erule_tac x="y" in allE, simp) |
332 by (rule stream_finite_lemma1, simp) |
329 by (rule stream_finite_lemma1, simp) |
455 by (simp add: slen_def) |
452 by (simp add: slen_def) |
456 |
453 |
457 lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t" |
454 lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t" |
458 apply (erule stream_finite_ind [of s], auto) |
455 apply (erule stream_finite_ind [of s], auto) |
459 apply (case_tac "t=UU", auto) |
456 apply (case_tac "t=UU", auto) |
460 apply (drule eq_UU_iff [THEN iffD2]) |
|
461 apply (drule scons_eq_UU [THEN iffD2], simp) |
|
462 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
457 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
463 apply (erule_tac x="y" in allE, auto) |
458 apply (erule_tac x="y" in allE, auto) |
464 by (drule stream.inverts, auto) |
459 by (drule stream.inverts, auto) |
465 |
460 |
466 lemma slen_mono: "s << t ==> #s <= #t" |
461 lemma slen_mono: "s << t ==> #s <= #t" |
487 apply (induct_tac n, auto) |
482 apply (induct_tac n, auto) |
488 apply (case_tac "x=UU", auto) |
483 apply (case_tac "x=UU", auto) |
489 apply (simp add: inat_defs) |
484 apply (simp add: inat_defs) |
490 apply (simp add: Suc_ile_eq) |
485 apply (simp add: Suc_ile_eq) |
491 apply (case_tac "y=UU", clarsimp) |
486 apply (case_tac "y=UU", clarsimp) |
492 apply (drule eq_UU_iff [THEN iffD2],simp) |
|
493 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ |
487 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ |
494 apply (erule_tac x="ya" in allE, simp) |
488 apply (erule_tac x="ya" in allE, simp) |
495 apply (drule stream.inverts,auto) |
489 apply (drule stream.inverts,auto) |
496 by (drule ax_flat [rule_format], simp) |
490 by (drule ax_flat [rule_format], simp) |
497 |
491 |
498 lemma slen_strict_mono_lemma: |
492 lemma slen_strict_mono_lemma: |
499 "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t" |
493 "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t" |
500 apply (erule stream_finite_ind, auto) |
494 apply (erule stream_finite_ind, auto) |
501 apply (drule eq_UU_iff [THEN iffD2], simp) |
|
502 apply (case_tac "sa=UU", auto) |
495 apply (case_tac "sa=UU", auto) |
503 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
496 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
504 apply (drule stream.inverts, simp, simp, clarsimp) |
497 apply (drule stream.inverts, simp, simp, clarsimp) |
505 by (drule ax_flat [rule_format], simp) |
498 by (drule ax_flat [rule_format], simp) |
506 |
499 |
650 "[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==> |
643 "[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==> |
651 i_rt n s1 << i_rt n s2" |
644 i_rt n s1 << i_rt n s2" |
652 apply (simp add: i_th_def i_rt_Suc_back) |
645 apply (simp add: i_th_def i_rt_Suc_back) |
653 apply (rule stream.casedist [of "i_rt n s1"],simp) |
646 apply (rule stream.casedist [of "i_rt n s1"],simp) |
654 apply (rule stream.casedist [of "i_rt n s2"],auto) |
647 apply (rule stream.casedist [of "i_rt n s2"],auto) |
655 apply (drule eq_UU_iff [THEN iffD2], simp add: scons_eq_UU) |
|
656 by (intro monofun_cfun, auto) |
648 by (intro monofun_cfun, auto) |
657 |
649 |
658 lemma i_th_stream_take_Suc [rule_format]: |
650 lemma i_th_stream_take_Suc [rule_format]: |
659 "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s" |
651 "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s" |
660 apply (induct_tac n,auto) |
652 apply (induct_tac n,auto) |
819 (* ----------------------------------------------------------------------- *) |
811 (* ----------------------------------------------------------------------- *) |
820 |
812 |
821 lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)" |
813 lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)" |
822 apply (case_tac "#x",auto) |
814 apply (case_tac "#x",auto) |
823 apply (insert sconc_mono1 [of x y]) |
815 apply (insert sconc_mono1 [of x y]) |
824 by (insert eq_UU_iff [THEN iffD2, of x],auto) |
816 by auto |
825 |
817 |
826 (* ----------------------------------------------------------------------- *) |
818 (* ----------------------------------------------------------------------- *) |
827 |
819 |
828 lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x" |
820 lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x" |
829 by (rule stream.casedist,auto) |
821 by (rule stream.casedist,auto) |
1004 apply (simp add: sconc_def) |
996 apply (simp add: sconc_def) |
1005 apply (simp add: constr_sconc_def) |
997 apply (simp add: constr_sconc_def) |
1006 apply (simp add: stream.finite_def) |
998 apply (simp add: stream.finite_def) |
1007 by (drule slen_take_lemma1,auto) |
999 by (drule slen_take_lemma1,auto) |
1008 |
1000 |
1009 declare eq_UU_iff [THEN sym, simp add] |
|
1010 |
|
1011 end |
1001 end |