equal
deleted
inserted
replaced
359 by (cases x) (auto simp add: enat_0 eSuc_enat[THEN sym]) |
359 by (cases x) (auto simp add: enat_0 eSuc_enat[THEN sym]) |
360 |
360 |
361 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)" |
361 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)" |
362 by (cases x) auto |
362 by (cases x) auto |
363 |
363 |
364 lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y \<and> a \<noteq> \<bottom> \<and> enat n < #y)" |
364 lemma slen_scons_eq: "(enat (Suc n) < #x) = (\<exists>a y. x = a && y \<and> a \<noteq> \<bottom> \<and> enat n < #y)" |
365 apply (auto, case_tac "x=UU",auto) |
365 apply (auto, case_tac "x=UU",auto) |
366 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
366 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
367 apply (case_tac "#y") apply simp_all |
367 apply (case_tac "#y") apply simp_all |
368 apply (case_tac "#y") apply simp_all |
368 apply (case_tac "#y") apply simp_all |
369 done |
369 done |