Stream7.thy

theory Stream7 imports Main begin

codatatype (sset:'a) stream = SCons (shd:'a) (stl:"'a stream")

coinductive_set
  cle :: "(('a::order) stream * 'a stream) set"
where
  cle: "shd s <= shd t & (shd s = shd t --> (stl s, stl t) : cle) ==> (s, t) : cle"

inductive_set
  nle :: "(('a::order) stream * 'a stream) set"
where
  nle1: "~(shd s <= shd t) ==> (s, t) : nle" |
  nle2: "(s, t) : nle ==> (SCons x s, SCons x t) : nle"

lemma nle_cle: "UNIV - nle <= cle"
apply(clarsimp)
apply(rule_tac X="%s t. (s, t) ~: nle" in cle.coinduct)
apply(simp)
apply(clarsimp)
apply(rotate_tac -1)
apply(erule contrapos_np)
apply(auto)
apply (metis nle.nle1)
by (metis nle.nle2 stream.collapse)

lemma cle_nle0: "(a, b) : nle ==> (a, b) ~: cle"
apply(erule nle.induct)
apply(clarsimp)
apply (metis cle.cases)
by (metis cle.simps stream.sel(1) stream.sel(2))

lemma cle_nle: "cle <= UNIV - nle"
apply(clarsimp)
by (metis cle_nle0)

lemma "cle = UNIV - nle"
by (metis cle_nle nle_cle subset_antisym)

end