[STATEMENT]
lemma clock_simInit:
  assumes "iobs \<in> envObs a ` set envInit"
  shows "clock_simAbs (clock_simInit a iobs)
       = clock_sim ` { t' \<in> Clock.jkbpC.
                       clock_jview a t' = clock_jviewInit a iobs }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_simAbs (local.clock_simInit a iobs) = clock_sim ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a iobs)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_simAbs (local.clock_simInit a iobs) = clock_sim ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a iobs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
iobs \<in> envObs a ` set envInit

goal (1 subgoal):
 1. clock_simAbs (local.clock_simInit a iobs) = clock_sim ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a iobs)
[PROOF STEP]
unfolding clock_simInit_def clock_simAbs_def clock_sim_def [abs_def] Let_def
[PROOF STATE]
proof (prove)
using this:
iobs \<in> envObs a ` set envInit

goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst (fromList envInit, ODList.filter (\<lambda>s. envObs a s = iobs) (fromList envInit))), s) \<and> s \<in> toSet (snd (fromList envInit, ODList.filter (\<lambda>s. envObs a s = iobs) (fromList envInit)))) = (\<lambda>t. (clock_commonAbs t, tLast t)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a iobs)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> set envInit; iobs = envObs a x\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (set envInit, s) \<and> s \<in> set envInit \<and> envObs a s = envObs a x) = (\<lambda>x. (clock_commonAbs x, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set envInit; iobs = envObs a x\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (set envInit, s) \<and> s \<in> set envInit \<and> envObs a s = envObs a x) \<subseteq> (\<lambda>x. (clock_commonAbs x, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x))
 2. \<And>x. \<lbrakk>x \<in> set envInit; iobs = envObs a x\<rbrakk> \<Longrightarrow> (\<lambda>x. (clock_commonAbs x, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (set envInit, s) \<and> s \<in> set envInit \<and> envObs a s = envObs a x)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set envInit; iobs = envObs a x; s \<in> set envInit; envObs a s = envObs a x\<rbrakk> \<Longrightarrow> (set envInit, s) \<in> (\<lambda>x. (clock_commonAbs x, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x))
 2. \<And>x. \<lbrakk>x \<in> set envInit; iobs = envObs a x\<rbrakk> \<Longrightarrow> (\<lambda>x. (clock_commonAbs x, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (set envInit, s) \<and> s \<in> set envInit \<and> envObs a s = envObs a x)
[PROOF STEP]
apply (rule_tac x="tInit s" in image_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set envInit; iobs = envObs a x; s \<in> set envInit; envObs a s = envObs a x\<rbrakk> \<Longrightarrow> (set envInit, s) = (clock_commonAbs (tInit s), tLast (tInit s))
 2. \<And>x s. \<lbrakk>x \<in> set envInit; iobs = envObs a x; s \<in> set envInit; envObs a s = envObs a x\<rbrakk> \<Longrightarrow> tInit s \<in> rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x))
 3. \<And>x. \<lbrakk>x \<in> set envInit; iobs = envObs a x\<rbrakk> \<Longrightarrow> (\<lambda>x. (clock_commonAbs x, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (set envInit, s) \<and> s \<in> set envInit \<and> envObs a s = envObs a x)
[PROOF STEP]
apply (auto simp: Set.image_def Clock.jviewInit)[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> set envInit; iobs = envObs a x\<rbrakk> \<Longrightarrow> (\<lambda>x. (clock_commonAbs x, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jviewInit a (envObs a x)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (set envInit, s) \<and> s \<in> set envInit \<and> envObs a s = envObs a x)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply (case_tac xa)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = tInit x1\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
 2. \<And>x xa x21 x22. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = x21 \<leadsto> x22\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>s. uu_ = tInit s \<and> s \<in> set envInit) = set envInit \<and> envObs a x1 = envObs a x
 2. \<And>x xa x21 x22. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = x21 \<leadsto> x22\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>s. uu_ = tInit s \<and> s \<in> set envInit) = set envInit
 2. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> envObs a x1 = envObs a x
 3. \<And>x xa x21 x22. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = x21 \<leadsto> x22\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>s. uu_ = tInit s \<and> s \<in> set envInit) \<subseteq> set envInit
 2. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> set envInit \<subseteq> tLast ` rel_ext (\<lambda>uu_. \<exists>s. uu_ = tInit s \<and> s \<in> set envInit)
 3. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> envObs a x1 = envObs a x
 4. \<And>x xa x21 x22. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = x21 \<leadsto> x22\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> set envInit \<subseteq> tLast ` rel_ext (\<lambda>uu_. \<exists>s. uu_ = tInit s \<and> s \<in> set envInit)
 2. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> envObs a x1 = envObs a x
 3. \<And>x xa x21 x22. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = x21 \<leadsto> x22\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x1 xa. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x); xa \<in> set envInit\<rbrakk> \<Longrightarrow> xa \<in> tLast ` rel_ext (\<lambda>uu_. \<exists>s. uu_ = tInit s \<and> s \<in> set envInit)
 2. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> envObs a x1 = envObs a x
 3. \<And>x xa x21 x22. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = x21 \<leadsto> x22\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply (rule_tac x="tInit xa" in image_eqI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x1 xa. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x); xa \<in> set envInit\<rbrakk> \<Longrightarrow> xa = tLast (tInit xa)
 2. \<And>x x1 xa. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x); xa \<in> set envInit\<rbrakk> \<Longrightarrow> tInit xa \<in> rel_ext (\<lambda>uu_. \<exists>s. uu_ = tInit s \<and> s \<in> set envInit)
 3. \<And>x x1. \<lbrakk>x \<in> set envInit; iobs = envObs a x; x1 \<in> set envInit; clock_jview a (tInit x1) = clock_jviewInit a (envObs a x)\<rbrakk> \<Longrightarrow> envObs a x1 = envObs a x
 4. \<And>x xa x21 x22. \<lbrakk>x \<in> set envInit; iobs = envObs a x; xa \<in> Clock.jkbpC; clock_jview a xa = clock_jviewInit a (envObs a x); xa = x21 \<leadsto> x22\<rbrakk> \<Longrightarrow> clock_commonAbs xa = set envInit \<and> tLast xa \<in> set envInit \<and> envObs a (tLast xa) = envObs a x
[PROOF STEP]
apply (auto intro!: image_eqI simp: Clock.jviewInit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_simObs:
  assumes tC: "t \<in> Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "clock_simObs a ec = envObs a (tLast t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.clock_simObs a ec = envObs a (tLast t)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.clock_simObs a ec = envObs a (tLast t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.clock_simObs a ec = envObs a (tLast t)
[PROOF STEP]
have A: "\<forall>s \<in> set (toList (snd ec)). envObs a s = envObs a (tLast t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>set (toList (snd ec)). envObs a s = envObs a (tLast t)
[PROOF STEP]
using agent_abs[OF tC ec]
[PROOF STATE]
proof (prove)
using this:
toSet (snd ec) = agent_abs a t

goal (1 subgoal):
 1. \<forall>s\<in>set (toList (snd ec)). envObs a s = envObs a (tLast t)
[PROOF STEP]
by (clarsimp simp: agent_abs_def toSet_def)
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>set (toList (snd ec)). envObs a s = envObs a (tLast t)

goal (1 subgoal):
 1. local.clock_simObs a ec = envObs a (tLast t)
[PROOF STEP]
have B: "tLast t \<in> set (toList (snd ec))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tLast t \<in> set (toList (snd ec))
[PROOF STEP]
using clock_simAbs_refl[OF assms]
[PROOF STATE]
proof (prove)
using this:
clock_sim t \<in> clock_simAbs ec

goal (1 subgoal):
 1. tLast t \<in> set (toList (snd ec))
[PROOF STEP]
unfolding clock_simAbs_def clock_sim_def
[PROOF STATE]
proof (prove)
using this:
(clock_commonAbs t, tLast t) \<in> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec))

goal (1 subgoal):
 1. tLast t \<in> set (toList (snd ec))
[PROOF STEP]
by (simp add: toSet_def snd_def)
[PROOF STATE]
proof (state)
this:
tLast t \<in> set (toList (snd ec))

goal (1 subgoal):
 1. local.clock_simObs a ec = envObs a (tLast t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.clock_simObs a ec = envObs a (tLast t)
[PROOF STEP]
unfolding clock_simObs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (envObs a \<circ> ODList.hd \<circ> snd) ec = envObs a (tLast t)
[PROOF STEP]
by (simp add: list_choose_hd[OF A B] ODList.hd_def)
[PROOF STATE]
proof (state)
this:
local.clock_simObs a ec = envObs a (tLast t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clock_coEC_relation_image:
  "s \<in> ODList.toSet Y
    \<Longrightarrow> ODList.toSet (clock_knowledge envObs Y a s) = relations (clock_repMC (ODList.toSet Y)) a `` {s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> toSet Y \<Longrightarrow> toSet (clock_knowledge envObs Y a s) = relations (clock_repMC (toSet Y)) a `` {s}
[PROOF STEP]
unfolding clock_knowledge_def clock_repRels_def Image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> toSet Y \<Longrightarrow> toSet (ODList.filter (\<lambda>s'. envObs a s = envObs a s') Y) = rel_ext (\<lambda>y. \<exists>x\<in>{s}. (x, y) \<in> relations (mkKripke (toSet Y) (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal) a)
[PROOF STEP]
by auto


[STATEMENT]
lemma clock_commonKnowledge_relation_image_aux:
  "(\<Union>x\<in>set as. \<Union>a\<in>ODList.toSet Y. \<Union>aa\<in>ODList.toSet Y \<inter> {s''. envObs x a = envObs x s''}. {(a, aa)})
 = ((\<Union>a\<in>set as. {(s, s'). envObs a s = envObs a s'}) \<inter> ODList.toSet Y \<times> ODList.toSet Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>set as. \<Union>a\<in>toSet Y. \<Union>aa\<in>toSet Y \<inter> rel_ext (\<lambda>s''. envObs x a = envObs x s''). {(a, aa)}) = Restr (\<Union>a\<in>set as. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) (toSet Y)
[PROOF STEP]
by auto


[STATEMENT]
lemma clock_commonKnowledge_relation_image:
  "s \<in> ODList.toSet Y
    \<Longrightarrow> ODList.toSet (clock_commonKnowledge envObs Y as s) = (\<Union>a \<in> set as. relations (clock_repMC (ODList.toSet Y)) a)\<^sup>+ `` {s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> toSet Y \<Longrightarrow> toSet (clock_commonKnowledge envObs Y as s) = (\<Union> (relations (clock_repMC (toSet Y)) ` set as))\<^sup>+ `` {s}
[PROOF STEP]
unfolding clock_commonKnowledge_def clock_repRels_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> toSet Y \<Longrightarrow> toSet (fromList (memo_list_trancl (toList (big_union (\<lambda>a. fromList (concat (map (\<lambda>s'. concat (map (\<lambda>s''. if envObs a s' = envObs a s'' then [(s', s'')] else []) (toList Y))) (toList Y)))) as)) s)) = (\<Union> (relations (mkKripke (toSet Y) (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal) ` set as))\<^sup>+ `` {s}
[PROOF STEP]
apply (simp add: memo_list_trancl toSet_def[symmetric] Image_def clock_commonKnowledge_relation_image_aux)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eval_rec_models:
  assumes XY: "ODList.toSet X \<subseteq> ODList.toSet Y"
      and s: "s \<in> ODList.toSet X"
  shows "s \<in> ODList.toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)
     \<longleftrightarrow> clock_repMC (ODList.toSet Y), s \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>
[PROOF STEP]
using XY s
[PROOF STATE]
proof (prove)
using this:
toSet X \<subseteq> toSet Y
s \<in> toSet X

goal (1 subgoal):
 1. (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>
[PROOF STEP]
proof(induct \<phi> arbitrary: X s)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kprop x))) = clock_repMC (toSet Y), s \<Turnstile> Kprop x
 2. \<And>\<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Knot \<phi>))) = clock_repMC (toSet Y), s \<Turnstile> Knot \<phi>
 3. \<And>\<phi>1 \<phi>2 X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>1)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>1; \<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>2)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>2; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kand \<phi>1 \<phi>2))) = clock_repMC (toSet Y), s \<Turnstile> Kand \<phi>1 \<phi>2
 4. \<And>x1a \<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>K\<^sub>x1a \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>K\<^sub>x1a \<phi>
 5. \<And>x1a \<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>x1a\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>x1a\<^esub> \<phi>
[PROOF STEP]
case (Kknows a' \<phi> X s)
[PROOF STATE]
proof (state)
this:
\<lbrakk>toSet ?X3 \<subseteq> toSet Y; ?s3 \<in> toSet ?X3\<rbrakk> \<Longrightarrow> (?s3 \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) ?X3 \<phi>)) = clock_repMC (toSet Y), ?s3 \<Turnstile> \<phi>
toSet X \<subseteq> toSet Y
s \<in> toSet X

goal (5 subgoals):
 1. \<And>x X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kprop x))) = clock_repMC (toSet Y), s \<Turnstile> Kprop x
 2. \<And>\<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Knot \<phi>))) = clock_repMC (toSet Y), s \<Turnstile> Knot \<phi>
 3. \<And>\<phi>1 \<phi>2 X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>1)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>1; \<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>2)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>2; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kand \<phi>1 \<phi>2))) = clock_repMC (toSet Y), s \<Turnstile> Kand \<phi>1 \<phi>2
 4. \<And>x1a \<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>K\<^sub>x1a \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>K\<^sub>x1a \<phi>
 5. \<And>x1a \<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>x1a\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>x1a\<^esub> \<phi>
[PROOF STEP]
from \<open>s \<in> ODList.toSet X\<close> clock_coEC_relation_image[OF subsetD[OF Kknows(2) Kknows(3)], where a=a']
[PROOF STATE]
proof (chain)
picking this:
s \<in> toSet X
toSet (clock_knowledge envObs Y a' s) = relations (clock_repMC (toSet Y)) a' `` {s}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s \<in> toSet X
toSet (clock_knowledge envObs Y a' s) = relations (clock_repMC (toSet Y)) a' `` {s}

goal (1 subgoal):
 1. (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>K\<^sub>a' \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>K\<^sub>a' \<phi>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}\<rbrakk> \<Longrightarrow> (ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty) = (\<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty\<rbrakk> \<Longrightarrow> \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 2. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty
[PROOF STEP]
apply (drule arg_cong[where f="ODList.toSet"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; toSet (ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>)) = toSet ODList.empty\<rbrakk> \<Longrightarrow> \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 2. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty
[PROOF STEP]
apply (clarsimp simp: odlist_all_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; Restr (clock_repRels a') (toSet Y) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>); (s, w') \<in> clock_repRels a'; s \<in> toSet Y; w' \<in> toSet Y\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 2. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty
[PROOF STEP]
apply (cut_tac s3="w'" and X3="clock_knowledge envObs Y a' s" in Kknows.hyps)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; Restr (clock_repRels a') (toSet Y) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>); (s, w') \<in> clock_repRels a'; s \<in> toSet Y; w' \<in> toSet Y\<rbrakk> \<Longrightarrow> toSet (clock_knowledge envObs Y a' s) \<subseteq> toSet Y
 2. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; Restr (clock_repRels a') (toSet Y) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>); (s, w') \<in> clock_repRels a'; s \<in> toSet Y; w' \<in> toSet Y\<rbrakk> \<Longrightarrow> w' \<in> toSet (clock_knowledge envObs Y a' s)
 3. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; Restr (clock_repRels a') (toSet Y) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>); (s, w') \<in> clock_repRels a'; s \<in> toSet Y; w' \<in> toSet Y; (w' \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>)) = clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 4. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty
[PROOF STEP]
using Kknows(2) Kknows(3)
[PROOF STATE]
proof (prove)
using this:
toSet X \<subseteq> toSet Y
s \<in> toSet X

goal (4 subgoals):
 1. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; Restr (clock_repRels a') (toSet Y) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>); (s, w') \<in> clock_repRels a'; s \<in> toSet Y; w' \<in> toSet Y\<rbrakk> \<Longrightarrow> toSet (clock_knowledge envObs Y a' s) \<subseteq> toSet Y
 2. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; Restr (clock_repRels a') (toSet Y) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>); (s, w') \<in> clock_repRels a'; s \<in> toSet Y; w' \<in> toSet Y\<rbrakk> \<Longrightarrow> w' \<in> toSet (clock_knowledge envObs Y a' s)
 3. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; Restr (clock_repRels a') (toSet Y) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>); (s, w') \<in> clock_repRels a'; s \<in> toSet Y; w' \<in> toSet Y; (w' \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>)) = clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 4. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty
[PROOF STEP]
apply (auto simp add: S5n_rels_closed[OF clock_repMC_S5n])[3]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_knowledge envObs Y a' s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>) = ODList.empty
[PROOF STEP]
apply (clarsimp simp: toSet_eq_iff odlist_all_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> clock_repRels a'; s \<in> toSet Y; x \<in> toSet Y\<rbrakk> \<Longrightarrow> x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_knowledge envObs Y a' s) \<phi>)
[PROOF STEP]
apply (subst Kknows.hyps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> clock_repRels a'; s \<in> toSet Y; x \<in> toSet Y\<rbrakk> \<Longrightarrow> toSet (clock_knowledge envObs Y a' s) \<subseteq> toSet Y
 2. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> clock_repRels a'; s \<in> toSet Y; x \<in> toSet Y\<rbrakk> \<Longrightarrow> x \<in> toSet (clock_knowledge envObs Y a' s)
 3. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> clock_repRels a'; s \<in> toSet Y; x \<in> toSet Y\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), x \<Turnstile> \<phi>
[PROOF STEP]
using Kknows(2) Kknows(3)
[PROOF STATE]
proof (prove)
using this:
toSet X \<subseteq> toSet Y
s \<in> toSet X

goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> clock_repRels a'; s \<in> toSet Y; x \<in> toSet Y\<rbrakk> \<Longrightarrow> toSet (clock_knowledge envObs Y a' s) \<subseteq> toSet Y
 2. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> clock_repRels a'; s \<in> toSet Y; x \<in> toSet Y\<rbrakk> \<Longrightarrow> x \<in> toSet (clock_knowledge envObs Y a' s)
 3. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_knowledge envObs Y a' s) = Restr (clock_repRels a') (toSet Y) `` {s}; \<forall>w'\<in>Restr (clock_repRels a') (toSet Y) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> clock_repRels a'; s \<in> toSet Y; x \<in> toSet Y\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), x \<Turnstile> \<phi>
[PROOF STEP]
apply (auto simp add: S5n_rels_closed[OF clock_repMC_S5n])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>K\<^sub>a' \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>K\<^sub>a' \<phi>

goal (4 subgoals):
 1. \<And>x X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kprop x))) = clock_repMC (toSet Y), s \<Turnstile> Kprop x
 2. \<And>\<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Knot \<phi>))) = clock_repMC (toSet Y), s \<Turnstile> Knot \<phi>
 3. \<And>\<phi>1 \<phi>2 X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>1)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>1; \<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>2)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>2; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kand \<phi>1 \<phi>2))) = clock_repMC (toSet Y), s \<Turnstile> Kand \<phi>1 \<phi>2
 4. \<And>x1a \<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>x1a\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>x1a\<^esub> \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kprop x))) = clock_repMC (toSet Y), s \<Turnstile> Kprop x
 2. \<And>\<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Knot \<phi>))) = clock_repMC (toSet Y), s \<Turnstile> Knot \<phi>
 3. \<And>\<phi>1 \<phi>2 X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>1)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>1; \<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>2)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>2; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kand \<phi>1 \<phi>2))) = clock_repMC (toSet Y), s \<Turnstile> Kand \<phi>1 \<phi>2
 4. \<And>x1a \<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>x1a\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>x1a\<^esub> \<phi>
[PROOF STEP]
case (Kcknows as \<phi> X s)
[PROOF STATE]
proof (state)
this:
\<lbrakk>toSet ?X3 \<subseteq> toSet Y; ?s3 \<in> toSet ?X3\<rbrakk> \<Longrightarrow> (?s3 \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) ?X3 \<phi>)) = clock_repMC (toSet Y), ?s3 \<Turnstile> \<phi>
toSet X \<subseteq> toSet Y
s \<in> toSet X

goal (4 subgoals):
 1. \<And>x X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kprop x))) = clock_repMC (toSet Y), s \<Turnstile> Kprop x
 2. \<And>\<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Knot \<phi>))) = clock_repMC (toSet Y), s \<Turnstile> Knot \<phi>
 3. \<And>\<phi>1 \<phi>2 X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>1)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>1; \<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>2)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>2; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kand \<phi>1 \<phi>2))) = clock_repMC (toSet Y), s \<Turnstile> Kand \<phi>1 \<phi>2
 4. \<And>x1a \<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>x1a\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>x1a\<^esub> \<phi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
proof(cases "as = Nil")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as = [] \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
 2. as \<noteq> [] \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as = []

goal (2 subgoals):
 1. as = [] \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
 2. as \<noteq> [] \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
with \<open>s \<in> ODList.toSet X\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> toSet X
as = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> toSet X
as = []

goal (1 subgoal):
 1. (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
(s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>

goal (1 subgoal):
 1. as \<noteq> [] \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as \<noteq> [] \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as \<noteq> []

goal (1 subgoal):
 1. as \<noteq> [] \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
with \<open>s \<in> ODList.toSet X\<close> clock_commonKnowledge_relation_image[OF subsetD[OF Kcknows(2) Kcknows(3)], where as=as]
[PROOF STATE]
proof (chain)
picking this:
s \<in> toSet X
toSet (clock_commonKnowledge envObs Y as s) = (\<Union> (relations (clock_repMC (toSet Y)) ` set as))\<^sup>+ `` {s}
as \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> toSet X
toSet (clock_commonKnowledge envObs Y as s) = (\<Union> (relations (clock_repMC (toSet Y)) ` set as))\<^sup>+ `` {s}
as \<noteq> []

goal (1 subgoal):
 1. (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []\<rbrakk> \<Longrightarrow> (ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty) = (\<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty\<rbrakk> \<Longrightarrow> \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
apply (drule arg_cong[where f="ODList.toSet"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; toSet (ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>)) = toSet ODList.empty\<rbrakk> \<Longrightarrow> \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
apply (clarsimp simp: odlist_all_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
apply (cut_tac s3="w'" and X3="clock_commonKnowledge envObs Y as s" in Kcknows.hyps)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> toSet (clock_commonKnowledge envObs Y as s) \<subseteq> toSet Y
 2. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> w' \<in> toSet (clock_commonKnowledge envObs Y as s)
 3. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; (w' \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>)) = clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 4. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
using Kcknows(2) Kcknows(3)
[PROOF STATE]
proof (prove)
using this:
toSet X \<subseteq> toSet Y
s \<in> toSet X

goal (4 subgoals):
 1. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> toSet (clock_commonKnowledge envObs Y as s) \<subseteq> toSet Y
 2. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> w' \<in> toSet (clock_commonKnowledge envObs Y as s)
 3. \<And>w'. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; (w' \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>)) = clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), w' \<Turnstile> \<phi>
 4. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
apply (auto simp add: S5n_rels_closed[OF clock_repMC_S5n])[3]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w' x. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet Y
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
apply (subst (asm) trancl_unfold)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w' x. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y)) `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet Y
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w' x. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y)) `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet Y
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w' x. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, w') \<in> Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y); toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet Y
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w' x. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s} \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>); (s, x) \<in> Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y); (s, w') \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> x \<in> toSet Y
 2. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
(* FIXME disgusting *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> ODList.difference (clock_commonKnowledge envObs Y as s) (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>) = ODList.empty
[PROOF STEP]
apply (clarsimp simp: toSet_eq_iff odlist_all_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) (clock_commonKnowledge envObs Y as s) \<phi>)
[PROOF STEP]
apply (subst Kcknows.hyps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> toSet (clock_commonKnowledge envObs Y as s) \<subseteq> toSet Y
 2. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet (clock_commonKnowledge envObs Y as s)
 3. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), x \<Turnstile> \<phi>
[PROOF STEP]
using Kcknows(2) Kcknows(3)
[PROOF STATE]
proof (prove)
using this:
toSet X \<subseteq> toSet Y
s \<in> toSet X

goal (3 subgoals):
 1. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> toSet (clock_commonKnowledge envObs Y as s) \<subseteq> toSet Y
 2. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet (clock_commonKnowledge envObs Y as s)
 3. \<And>x. \<lbrakk>s \<in> toSet X; toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> clock_repMC (toSet Y), x \<Turnstile> \<phi>
[PROOF STEP]
apply (auto simp add: S5n_rels_closed[OF clock_repMC_S5n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, xa) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> toSet Y
[PROOF STEP]
apply (subst (asm) trancl_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y)) `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, xa) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> toSet Y
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y)) `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, xa) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> toSet Y
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, x) \<in> Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y); toSet X \<subseteq> toSet Y; s \<in> toSet X; (s, xa) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> toSet Y
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>toSet (clock_commonKnowledge envObs Y as s) = (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}; as \<noteq> []; \<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ `` {s}. clock_repMC (toSet Y), w' \<Turnstile> \<phi>; (s, xa) \<in> Restr (\<Union> (clock_repRels ` set as)) (toSet Y) \<union> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+ O Restr (\<Union> (clock_repRels ` set as)) (toSet Y); (s, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet Y))\<^sup>+; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> xa \<in> toSet Y
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
(* FIXME disgusting *)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<^bold>C\<^bsub>as\<^esub> \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<phi>

goal (3 subgoals):
 1. \<And>x X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kprop x))) = clock_repMC (toSet Y), s \<Turnstile> Kprop x
 2. \<And>\<phi> X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Knot \<phi>))) = clock_repMC (toSet Y), s \<Turnstile> Knot \<phi>
 3. \<And>\<phi>1 \<phi>2 X s. \<lbrakk>\<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>1)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>1; \<And>X s. \<lbrakk>toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X \<phi>2)) = clock_repMC (toSet Y), s \<Turnstile> \<phi>2; toSet X \<subseteq> toSet Y; s \<in> toSet X\<rbrakk> \<Longrightarrow> (s \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X (Kand \<phi>1 \<phi>2))) = clock_repMC (toSet Y), s \<Turnstile> Kand \<phi>1 \<phi>2
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma trc_aux:
  assumes tC: "t \<in> Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
  shows "ODList.toSet (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<subseteq> ODList.toSet cec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<subseteq> toSet cec
[PROOF STEP]
apply (clarsimp simp: toSet_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> toSet aec; x \<in> toSet (clock_commonKnowledge envObs cec as xa)\<rbrakk> \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
apply (subst (asm) clock_commonKnowledge_relation_image)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> toSet aec \<Longrightarrow> xa \<in> toSet cec
 2. \<And>x xa. \<lbrakk>xa \<in> toSet aec; x \<in> (\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {xa}\<rbrakk> \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
apply (erule aec_cec_subset[OF tC aec cec])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> toSet aec; x \<in> (\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {xa}\<rbrakk> \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
apply (subst (asm) trancl_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> toSet aec; x \<in> (\<Union> (relations (clock_repMC (toSet cec)) ` set as) \<union> (\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ O \<Union> (relations (clock_repMC (toSet cec)) ` set as)) `` {xa}\<rbrakk> \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> toSet aec; x \<in> (\<Union> (relations (clock_repMC (toSet cec)) ` set as) \<union> (\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ O \<Union> (relations (clock_repMC (toSet cec)) ` set as)) `` {xa}\<rbrakk> \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
apply (auto simp: agent_abs_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_repMC_aec:
  assumes tC: "t \<in> Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and x: "x \<in> ODList.toSet aec"
      and xy: "(x, y) \<in> relations (clock_repMC (ODList.toSet cec)) a"
  shows "y \<in> ODList.toSet aec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> toSet aec
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t
x \<in> toSet aec
(x, y) \<in> relations (clock_repMC (toSet cec)) a

goal (1 subgoal):
 1. y \<in> toSet aec
[PROOF STEP]
unfolding clock_repRels_def agent_abs_def common_abs_def
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
toSet cec = clock_commonAbs t
x \<in> toSet aec
(x, y) \<in> relations (mkKripke (toSet cec) (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal) a

goal (1 subgoal):
 1. y \<in> toSet aec
[PROOF STEP]
by auto


[STATEMENT]
lemma clock_repMC_cec:
  assumes tC: "t \<in> Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and x: "x \<in> ODList.toSet aec"
      and y: "y \<in> ODList.toSet aec"
  shows "(x, y) \<in> relations (clock_repMC (ODList.toSet cec)) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> relations (clock_repMC (toSet cec)) a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t
x \<in> toSet aec
y \<in> toSet aec

goal (1 subgoal):
 1. (x, y) \<in> relations (clock_repMC (toSet cec)) a
[PROOF STEP]
unfolding clock_repRels_def agent_abs_def common_abs_def
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
toSet cec = clock_commonAbs t
x \<in> toSet aec
y \<in> toSet aec

goal (1 subgoal):
 1. (x, y) \<in> relations (mkKripke (toSet cec) (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal) a
[PROOF STEP]
by auto