CoindStudy.thy

theory CoindStudy 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"

definition
  F :: "(('a::order) stream * 'a stream) set => ('a stream * 'a stream) set"
where
  "F X =
      {(s, t). shd s <= shd t & (shd s = shd t --> (stl s, stl t) : X)}"

lemma mono_F: "mono F"
apply(unfold mono_def F_def)
apply(auto)
done

(* The *.cases rule indicates cle <= F cle *)
lemma cle_F_1: "cle <= F cle"
apply(rule subsetI)
apply(clarsimp)
apply(erule cle.cases)
apply(unfold F_def)
apply(auto)
done

(* The coinduction rule indicates X <= F X ==> X <= cle *)
lemma cle_F_2_0:
  "(a, b) : Union {X. X <= F X} ==> (a, b) : cle"
apply(erule cle.coinduct)
apply(clarsimp)
apply(unfold F_def)
apply(auto)
done

lemma cle_F_2: "X <= F X ==> X <= cle"
apply(rule subsetI)
apply(clarsimp)
apply(rule cle_F_2_0)
apply(clarsimp)
by metis

(* coinductive set is the greatest fixed point *)
lemma cle_gfp: "cle = gfp F"
apply(unfold gfp_def)
apply(rule antisym)
apply(rule subsetI)
apply(clarsimp)
apply(rule_tac x="cle" in exI)
apply (metis cle_F_1 contra_subsetD)
apply(rule subsetI)
apply(clarsimp)
by (metis cle_F_2 subsetCE)

(* The rules described in 'coinductive_set' indicates F cle <= cle *)
lemma "F cle <= cle"
apply(unfold F_def)
apply(clarsimp)
by (metis cle.intros)

end