IndStudy.thy

theory IndStudy imports Main begin

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

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"

definition
  F :: "(('a::order) stream * 'a stream) set => ('a stream * 'a stream) set"
where
  "F X = ({(s, t). ~ shd s <= shd t} Un
       {(s, t). EX x s2 t2. s = SCons x s2 & t = SCons x t2 & (s2, t2) : X})"

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

(* The induction rule indicates F X <= X => nle <= X *)
lemma nle_1_0: "(s, t) : nle ==> F X <= X --> (s, t) : X"
apply(erule nle.induct)
apply(unfold F_def)
apply(auto)
done

lemma nle_1: "F X <= X ==> nle <= X"
apply(rule subsetI)
apply(clarsimp)
apply(erule nle_1_0[rule_format])
apply(simp)
done

(* The set of induction rules indicates F nle <= nle *)
lemma nle_2: "F nle <= nle"
apply(rule subsetI)
apply(unfold F_def)
apply(auto)
apply (metis nle.nle1)
by (metis nle.nle2)

(* inductive set is the least fixed point *)
lemma nle_lfp: "nle = lfp F"
apply(unfold lfp_def)
apply(rule antisym)
apply(rule subsetI)
apply(clarsimp)
apply (metis contra_subsetD nle_1)
apply(rule subsetI)
apply(clarsimp)
apply(drule_tac x="nle" in spec)
apply(drule mp)
apply(clarsimp)
apply (metis contra_subsetD nle_2)
apply(simp)
done

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

end