equal
deleted
inserted
replaced
69 by auto |
69 by auto |
70 |
70 |
71 lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)" |
71 lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)" |
72 by (auto,insert stream.exhaust [of x],auto) |
72 by (auto,insert stream.exhaust [of x],auto) |
73 |
73 |
74 lemma stream_neq_UU: "x~=UU ==> EX a as. x=a&&as & a~=UU" |
74 lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU" |
75 by (simp add: stream_exhaust_eq,auto) |
75 by (simp add: stream_exhaust_eq,auto) |
76 |
76 |
77 lemma stream_inject_eq [simp]: |
77 lemma stream_inject_eq [simp]: |
78 "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)" |
78 "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)" |
79 by (insert stream.injects [of a s b t], auto) |
79 by (insert stream.injects [of a s b t], auto) |