equal
deleted
inserted
replaced
79 by (simp add: fscons_def2) |
79 by (simp add: fscons_def2) |
80 |
80 |
81 lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt & s << tt" |
81 lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt & s << tt" |
82 apply (cases t) |
82 apply (cases t) |
83 apply (cut_tac fscons_not_empty) |
83 apply (cut_tac fscons_not_empty) |
84 apply (fast dest: eq_UU_iff [THEN iffD2]) |
84 apply (fast dest: bottomI) |
85 apply (simp add: fscons_def2) |
85 apply (simp add: fscons_def2) |
86 done |
86 done |
87 |
87 |
88 lemma fstream_prefix' [simp]: |
88 lemma fstream_prefix' [simp]: |
89 "x << a~> z = (x = <> | (? y. x = a~> y & y << z))" |
89 "x << a~> z = (x = <> | (? y. x = a~> y & y << z))" |
90 apply (simp add: fscons_def2 Def_not_UU [THEN stream_prefix']) |
90 apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix']) |
91 apply (safe) |
91 apply (safe) |
92 apply (erule_tac [!] contrapos_np) |
92 apply (erule_tac [!] contrapos_np) |
93 prefer 2 apply (fast elim: DefE) |
93 prefer 2 apply (fast elim: DefE) |
94 apply (rule lift.exhaust) |
94 apply (rule lift.exhaust) |
95 apply (erule (1) notE) |
95 apply (erule (1) notE) |