equal
deleted
inserted
replaced
66 apply (cut_tac fstream_exhaust) |
66 apply (cut_tac fstream_exhaust) |
67 apply (erule disjE) |
67 apply (erule disjE) |
68 apply fast |
68 apply fast |
69 apply fast |
69 apply fast |
70 done |
70 done |
71 (* |
71 |
72 fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i |
|
73 THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
|
74 *) |
|
75 lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)" |
72 lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)" |
76 apply (simp add: fscons_def2 stream_exhaust_eq) |
73 apply (simp add: fscons_def2 stream_exhaust_eq) |
77 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
74 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
78 done |
75 done |
79 |
76 |