[STATEMENT]
lemma evalS_models:
  assumes tC: "t \<in> Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and subj_phi: "subjective a \<phi>"
      and s: "s \<in> ODList.toSet aec"
  shows "evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<phi>
     \<longleftrightarrow> clock_repMC (ODList.toSet cec), s \<Turnstile> \<phi>" (is "?lhs \<phi> = ?rhs \<phi>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<phi> = clock_repMC (toSet cec), s \<Turnstile> \<phi>
[PROOF STEP]
using subj_phi s aec cec
[PROOF STATE]
proof (prove)
using this:
subjective a \<phi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (1 subgoal):
 1. evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<phi> = clock_repMC (toSet cec), s \<Turnstile> \<phi>
[PROOF STEP]
proof(induct \<phi> rule: subjective.induct[case_names Kprop Knot Kand Kknows Kcknows])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a a' f. \<lbrakk>subjective a \<^bold>K\<^sub>a' f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>K\<^sub>a' f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a' f
 5. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
case (Kknows a a' \<psi>)
[PROOF STATE]
proof (state)
this:
subjective a \<^bold>K\<^sub>a' \<psi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (5 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a a' f. \<lbrakk>subjective a \<^bold>K\<^sub>a' f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>K\<^sub>a' f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a' f
 5. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>K\<^sub>a' \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a' \<psi>
[PROOF STEP]
apply (clarsimp simp: toSet_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)) = (\<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi>)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>) \<Longrightarrow> \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi>
 2. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), w' \<Turnstile> \<psi>
 2. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply (subgoal_tac "w' \<in> ODList.toSet aec")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec; w' \<in> toSet aec\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), w' \<Turnstile> \<psi>
 2. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> w' \<in> toSet aec
 3. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply (drule_tac c="w'" in subsetD)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>w'. \<lbrakk>(s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec; w' \<in> toSet aec\<rbrakk> \<Longrightarrow> w' \<in> toSet aec
 2. \<And>w'. \<lbrakk>(s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec; w' \<in> toSet aec; w' \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), w' \<Turnstile> \<psi>
 3. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> w' \<in> toSet aec
 4. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>w'. \<lbrakk>(s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec; w' \<in> toSet aec; w' \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), w' \<Turnstile> \<psi>
 2. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> w' \<in> toSet aec
 3. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply (simp add: eval_rec_models[OF subsetI[OF aec_cec_subset[OF tC aec cec]]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> w' \<in> toSet aec
 2. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply (rule clock_repMC_aec[OF tC Kknows(3) Kknows(4), rotated, where x=s])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> (s, w') \<in> relations (clock_repMC (toSet cec)) a
 2. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> s \<in> toSet aec
 3. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
using Kknows
[PROOF STATE]
proof (prove)
using this:
subjective a \<^bold>K\<^sub>a' \<psi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (3 subgoals):
 1. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> (s, w') \<in> relations (clock_repMC (toSet cec)) a
 2. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> s \<in> toSet aec
 3. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> s \<in> toSet aec
 2. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
using Kknows
[PROOF STATE]
proof (prove)
using this:
subjective a \<^bold>K\<^sub>a' \<psi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (2 subgoals):
 1. \<And>w'. \<lbrakk>toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>); (s, w') \<in> clock_repRels a'; s \<in> toSet cec; w' \<in> toSet cec\<rbrakk> \<Longrightarrow> s \<in> toSet aec
 2. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi> \<Longrightarrow> toSet aec \<subseteq> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi>; x \<in> toSet aec\<rbrakk> \<Longrightarrow> x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<psi>)
[PROOF STEP]
apply (simp add: eval_rec_models[OF subsetI[OF aec_cec_subset[OF tC aec cec]]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi>; x \<in> toSet aec\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), x \<Turnstile> \<psi>
[PROOF STEP]
using tC Kknows
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
subjective a \<^bold>K\<^sub>a' \<psi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>w'\<in>Restr (clock_repRels a') (toSet cec) `` {s}. clock_repMC (toSet cec), w' \<Turnstile> \<psi>; x \<in> toSet aec\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), x \<Turnstile> \<psi>
[PROOF STEP]
apply (clarsimp simp: agent_abs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t' t'a. \<lbrakk>\<forall>w'\<in>Restr (clock_repRels a') (common_abs t) `` {tLast t'a}. clock_repMC (common_abs t), w' \<Turnstile> \<psi>; t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t)\<rbrakk> \<Longrightarrow> clock_repMC (common_abs t), tLast t' \<Turnstile> \<psi>
[PROOF STEP]
apply (erule (1) ballE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (clock_repRels a') (common_abs t) `` {tLast t'a}\<rbrakk> \<Longrightarrow> clock_repMC (common_abs t), tLast t' \<Turnstile> \<psi>
[PROOF STEP]
using Kknows
[PROOF STATE]
proof (prove)
using this:
subjective a \<^bold>K\<^sub>a' \<psi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (1 subgoal):
 1. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (clock_repRels a') (common_abs t) `` {tLast t'a}\<rbrakk> \<Longrightarrow> clock_repMC (common_abs t), tLast t' \<Turnstile> \<psi>
[PROOF STEP]
apply (cut_tac x="tLast t'" and y="tLast t'a" in clock_repMC_cec[OF tC Kknows(3) Kknows(4)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (clock_repRels a') (common_abs t) `` {tLast t'a}; subjective a \<^bold>K\<^sub>a' \<psi>; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> tLast t' \<in> toSet aec
 2. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (clock_repRels a') (common_abs t) `` {tLast t'a}; subjective a \<^bold>K\<^sub>a' \<psi>; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> tLast t'a \<in> toSet aec
 3. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (clock_repRels a') (common_abs t) `` {tLast t'a}; subjective a \<^bold>K\<^sub>a' \<psi>; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t; (tLast t', tLast t'a) \<in> relations (clock_repMC (toSet cec)) a\<rbrakk> \<Longrightarrow> clock_repMC (common_abs t), tLast t' \<Turnstile> \<psi>
[PROOF STEP]
unfolding clock_repRels_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (rel_ext (\<lambda>(s, s'). envObs a' s = envObs a' s')) (common_abs t) `` {tLast t'a}; subjective a \<^bold>K\<^sub>a' \<psi>; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> tLast t' \<in> toSet aec
 2. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (rel_ext (\<lambda>(s, s'). envObs a' s = envObs a' s')) (common_abs t) `` {tLast t'a}; subjective a \<^bold>K\<^sub>a' \<psi>; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> tLast t'a \<in> toSet aec
 3. \<And>t' t'a. \<lbrakk>t \<in> Clock.jkbpC; a = a'; toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a' (tLast t') = envObs a' (tLast t)); toSet cec = common_abs t; s = tLast t'a; t' \<in> Clock.jkbpC; t'a \<in> Clock.jkbpC; tLength t' = tLength t; envObs a' (tLast t') = envObs a' (tLast t); tLength t'a = tLength t; envObs a' (tLast t'a) = envObs a' (tLast t); tLast t' \<notin> Restr (rel_ext (\<lambda>(s, s'). envObs a' s = envObs a' s')) (common_abs t) `` {tLast t'a}; subjective a \<^bold>K\<^sub>a' \<psi>; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t; (tLast t', tLast t'a) \<in> relations (mkKripke (toSet cec) (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal) a\<rbrakk> \<Longrightarrow> mkKripke (common_abs t) (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal, tLast t' \<Turnstile> \<psi>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>K\<^sub>a' \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a' \<psi>

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
case (Kcknows a as \<psi>)
[PROOF STATE]
proof (state)
this:
subjective a \<^bold>C\<^bsub>as\<^esub> \<psi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
have "?lhs (Kcknows as \<psi>)
      = (\<forall>y\<in>ODList.toSet aec.
           \<forall>x\<in>(\<Union>a\<in>set as. relations (clock_repMC (ODList.toSet cec)) a)\<^sup>+ `` {y}.
              x \<in> ODList.toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec)
                       (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = (\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
(* FIXME dreaming of a cong rule here. *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = (\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
using toSet_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
set (toList ?X) = toSet ?X

goal (1 subgoal):
 1. evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = (\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply (clarsimp simp: toSet_eq_iff toSet_def[symmetric] subset_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y\<in>toSet aec. \<forall>x\<in>toSet (clock_commonKnowledge envObs cec as y). x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (\<forall>y\<in>toSet aec. \<forall>x\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply (rule ball_cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> toSet aec \<Longrightarrow> (\<forall>x\<in>toSet (clock_commonKnowledge envObs cec as y). x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (\<forall>x\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply (rule ball_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. y \<in> toSet aec \<Longrightarrow> toSet (clock_commonKnowledge envObs cec as y) = (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}
 2. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply (subst clock_commonKnowledge_relation_image[OF aec_cec_subset[OF tC Kcknows(3) Kcknows(4)]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y. y \<in> toSet aec \<Longrightarrow> y \<in> toSet aec
 2. \<And>y. y \<in> toSet aec \<Longrightarrow> (\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y} = (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}
 3. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = (\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = (\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
have "... = (\<forall>s\<in>ODList.toSet aec. clock_repMC (ODList.toSet cec), s \<Turnstile> Kcknows as \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (\<forall>s\<in>toSet aec. clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>)
[PROOF STEP]
apply (rule ball_cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> toSet aec \<Longrightarrow> (\<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = clock_repMC (toSet cec), y \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> toSet aec \<Longrightarrow> (\<forall>x\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (\<forall>w'\<in>(Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}. clock_repMC (toSet cec), w' \<Turnstile> \<psi>)
[PROOF STEP]
apply (rule ball_cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = clock_repMC (toSet cec), x \<Turnstile> \<psi>
[PROOF STEP]
apply (subst eval_rec_models[OF trc_aux[OF tC Kcknows(3) Kcknows(4), where as=as], symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> x \<in> toSet (big_union (clock_commonKnowledge envObs cec as) (toList aec))
 2. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply (simp add: toSet_def[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y x. \<lbrakk>y \<in> toSet aec; (y, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>xa\<in>toSet aec. x \<in> toSet (clock_commonKnowledge envObs cec as xa)
 2. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply (rule_tac x=y in bexI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y x. \<lbrakk>y \<in> toSet aec; (y, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> toSet (clock_commonKnowledge envObs cec as y)
 2. \<And>y x. \<lbrakk>y \<in> toSet aec; (y, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> toSet aec
 3. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply (subst clock_commonKnowledge_relation_image[OF aec_cec_subset[OF tC Kcknows(3) Kcknows(4)]])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>y x. \<lbrakk>y \<in> toSet aec; (y, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> toSet aec
 2. \<And>y x. \<lbrakk>y \<in> toSet aec; (y, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> (\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}
 3. \<And>y x. \<lbrakk>y \<in> toSet aec; (y, x) \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> toSet aec
 4. \<And>y x. \<lbrakk>y \<in> toSet aec; x \<in> (Restr (\<Union> (clock_repRels ` set as)) (toSet cec))\<^sup>+ `` {y}\<rbrakk> \<Longrightarrow> (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (\<forall>s\<in>toSet aec. clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>)

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y\<in>toSet aec. \<forall>x\<in>(\<Union> (relations (clock_repMC (toSet cec)) ` set as))\<^sup>+ `` {y}. x \<in> toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) (big_union (clock_commonKnowledge envObs cec as) (toList aec)) \<psi>)) = (\<forall>s\<in>toSet aec. clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>)

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
have "... = clock_repMC (ODList.toSet cec), s \<Turnstile> Kknows a (Kcknows as \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s\<in>toSet aec. clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>) = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a \<^bold>C\<^bsub>as\<^esub> \<psi>
[PROOF STEP]
using clock_repMC_aec[OF tC Kcknows(3) Kcknows(4) Kcknows(2)]
          clock_repMC_cec[OF tC Kcknows(3) Kcknows(4) Kcknows(2)]
[PROOF STATE]
proof (prove)
using this:
(s, ?y) \<in> relations (clock_repMC (toSet cec)) a \<Longrightarrow> ?y \<in> toSet aec
?y \<in> toSet aec \<Longrightarrow> (s, ?y) \<in> relations (clock_repMC (toSet cec)) a

goal (1 subgoal):
 1. (\<forall>s\<in>toSet aec. clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>) = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a \<^bold>C\<^bsub>as\<^esub> \<psi>
[PROOF STEP]
by (auto cong: ball_cong)
[PROOF STATE]
proof (state)
this:
(\<forall>s\<in>toSet aec. clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>) = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a \<^bold>C\<^bsub>as\<^esub> \<psi>

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>s\<in>toSet aec. clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>) = clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a \<^bold>C\<^bsub>as\<^esub> \<psi>

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
have "... = clock_repMC (ODList.toSet cec), s \<Turnstile> Kcknows as \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a \<^bold>C\<^bsub>as\<^esub> \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>
[PROOF STEP]
apply (rule S5n_common_knowledge_fixed_point_simpler[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. S5n (clock_repMC (toSet cec))
 2. s \<in> worlds (clock_repMC (toSet cec))
 3. a \<in> set as
[PROOF STEP]
using Kcknows
[PROOF STATE]
proof (prove)
using this:
subjective a \<^bold>C\<^bsub>as\<^esub> \<psi>
s \<in> toSet aec
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (3 subgoals):
 1. S5n (clock_repMC (toSet cec))
 2. s \<in> worlds (clock_repMC (toSet cec))
 3. a \<in> set as
[PROOF STEP]
apply (auto intro: aec_cec_subset[OF tC Kcknows(3) Kcknows(4) Kcknows(2)])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
clock_repMC (toSet cec), s \<Turnstile> \<^bold>K\<^sub>a \<^bold>C\<^bsub>as\<^esub> \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>

goal (4 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
 4. \<And>a as f. \<lbrakk>subjective a \<^bold>C\<^bsub>as\<^esub> f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> f = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>

goal (1 subgoal):
 1. evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<^bold>C\<^bsub>as\<^esub> \<psi> = clock_repMC (toSet cec), s \<Turnstile> \<^bold>C\<^bsub>as\<^esub> \<psi>

goal (3 subgoals):
 1. \<And>a p. \<lbrakk>subjective a (Kprop p); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kprop p) = clock_repMC (toSet cec), s \<Turnstile> Kprop p
 2. \<And>a f. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; subjective a (Knot f); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Knot f) = clock_repMC (toSet cec), s \<Turnstile> Knot f
 3. \<And>a f g. \<lbrakk>\<lbrakk>subjective a f; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec f = clock_repMC (toSet cec), s \<Turnstile> f; \<lbrakk>subjective a g; s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec g = clock_repMC (toSet cec), s \<Turnstile> g; subjective a (Kand f g); s \<in> toSet aec; toSet aec = agent_abs a t; toSet cec = common_abs t\<rbrakk> \<Longrightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec (Kand f g) = clock_repMC (toSet cec), s \<Turnstile> Kand f g
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma eval_models:
  assumes tC: "t \<in> Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and subj_phi: "subjective a \<phi>"
      and s: "s \<in> ODList.toSet aec"
  shows "eval envVal envObs (cec, aec) \<phi>
     \<longleftrightarrow> clock_repMC (ODList.toSet cec), s \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval envVal envObs (cec, aec) \<phi> = clock_repMC (toSet cec), s \<Turnstile> \<phi>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval envVal envObs (cec, aec) \<phi> = clock_repMC (toSet cec), s \<Turnstile> \<phi>
[PROOF STEP]
unfolding eval_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (cec, aec) of (cec, aec) \<Rightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec) \<phi> = clock_repMC (toSet cec), s \<Turnstile> \<phi>
[PROOF STEP]
using evalS_models[OF tC aec cec subj_phi s]
[PROOF STATE]
proof (prove)
using this:
evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec \<phi> = clock_repMC (toSet cec), s \<Turnstile> \<phi>

goal (1 subgoal):
 1. (case (cec, aec) of (cec, aec) \<Rightarrow> evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec) \<phi> = clock_repMC (toSet cec), s \<Turnstile> \<phi>
[PROOF STEP]
apply (simp add: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_simAction_jAction:
  assumes tC: "t \<in> Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
  shows "set (clock_simAction a (cec, aec))
       = set (jAction (clock_repMC (ODList.toSet cec)) (tLast t) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction (clock_repMC (toSet cec)) (tLast t) a)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction (clock_repMC (toSet cec)) (tLast t) a)
[PROOF STEP]
unfolding clock_simAction_def jAction_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (case (cec, aec) of (Y, X) \<Rightarrow> concat (map (\<lambda>gc. if eval envVal envObs (Y, X) (guard gc) then [action gc] else []) (jkbp a))) = set (concat (map (\<lambda>gc. if clock_repMC (toSet cec), tLast t \<Turnstile> guard gc then [action gc] else []) (jkbp a)))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x}) = (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x})
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x})
 2. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). action xa = action x
 2. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
apply (rule_tac x=xa in bexI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> action xa = action xa
 2. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> xa \<in> set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc)
 3. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> xa \<in> set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc)
 2. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), tLast t \<Turnstile> guard xa
 2. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
apply (subst eval_models[OF tC aec cec, symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> subjective a (guard xa)
 2. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> tLast t \<in> toSet aec
 3. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> eval envVal envObs (cec, aec) (guard xa)
 4. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
using tC aec cec subj
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t
\<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc)

goal (4 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> subjective a (guard xa)
 2. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> tLast t \<in> toSet aec
 3. \<And>xa. \<lbrakk>xa \<in> set (jkbp a); eval envVal envObs (cec, aec) (guard xa)\<rbrakk> \<Longrightarrow> eval envVal envObs (cec, aec) (guard xa)
 4. (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (toSet cec), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. clock_repMC (common_abs t), tLast t \<Turnstile> guard gc). {action x}) \<subseteq> (\<Union>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). {action x})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc)). action xa = action x
[PROOF STEP]
apply (rule_tac x=xa in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> action xa = action xa
 2. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> xa \<in> set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc))
[PROOF STEP]
apply (rule refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> xa \<in> set (jkbp a) \<inter> rel_ext (\<lambda>gc. eval envVal envObs (cec, aec) (guard gc))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> eval envVal envObs (cec, aec) (guard xa)
[PROOF STEP]
apply (subst eval_models[OF tC aec cec])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> subjective a (guard xa)
 2. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> ?s58 xa \<in> toSet aec
 3. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), ?s58 xa \<Turnstile> guard xa
[PROOF STEP]
using tC aec cec subj
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t
\<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc)

goal (3 subgoals):
 1. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> subjective a (guard xa)
 2. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> ?s58 xa \<in> toSet aec
 3. \<And>xa. \<lbrakk>t \<in> Clock.jkbpC; toSet aec = agent_abs a t; toSet cec = common_abs t; \<forall>a gc. gc \<in> set (jkbp a) \<longrightarrow> subjective a (guard gc); xa \<in> set (jkbp a); clock_repMC (common_abs t), tLast t \<Turnstile> guard xa\<rbrakk> \<Longrightarrow> clock_repMC (toSet cec), ?s58 xa \<Turnstile> guard xa
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_submodel_aux:
  assumes tC: "t \<in> Clock.jkbpC"
      and s: "s \<in> worlds (clock_simMCt t)"
  shows "gen_model Clock.MCS s = gen_model (clock_simMCt t) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_model clock_simMC s = gen_model (clock_simMCt t) s
[PROOF STEP]
proof(rule gen_model_subset[where T="clock_jkbpCSt t"])
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. \<And>a. Restr (relations clock_simMC a) (clock_jkbpCSt t) = Restr (relations (clock_simMCt t) a) (clock_jkbpCSt t)
 4. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 5. (\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 6. s \<in> worlds clock_simMC
 7. s \<in> worlds (clock_simMCt t)
 8. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. \<And>a. Restr (relations clock_simMC a) (clock_jkbpCSt t) = Restr (relations (clock_simMCt t) a) (clock_jkbpCSt t)
 4. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 5. (\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 6. s \<in> worlds clock_simMC
 7. s \<in> worlds (clock_simMCt t)
 8. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
let ?X = "clock_sim ` Clock.jkbpCn (tLength t)"
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. \<And>a. Restr (relations clock_simMC a) (clock_jkbpCSt t) = Restr (relations (clock_simMCt t) a) (clock_jkbpCSt t)
 4. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 5. (\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 6. s \<in> worlds clock_simMC
 7. s \<in> worlds (clock_simMCt t)
 8. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
show "relations Clock.MCS a \<inter> ?X \<times> ?X
      = relations (clock_simMCt t) a \<inter> ?X \<times> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Restr (relations clock_simMC a) (clock_jkbpCSt t) = Restr (relations (clock_simMCt t) a) (clock_jkbpCSt t)
[PROOF STEP]
by (simp add: Int_ac Int_absorb1
                  relation_mono[OF jkbpCSt_jkbpCS_subset jkbpCSt_jkbpCS_subset])
[PROOF STATE]
proof (state)
this:
Restr (relations clock_simMC a) (clock_jkbpCSt t) = Restr (relations (clock_simMCt t) a) (clock_jkbpCSt t)

goal (7 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. (\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 5. s \<in> worlds clock_simMC
 6. s \<in> worlds (clock_simMCt t)
 7. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. (\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 5. s \<in> worlds clock_simMC
 6. s \<in> worlds (clock_simMCt t)
 7. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
let ?X = "clock_sim ` Clock.jkbpCn (tLength t)"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. (\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 5. s \<in> worlds clock_simMC
 6. s \<in> worlds (clock_simMCt t)
 7. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> worlds (clock_simMCt t)
[PROOF STEP]
show "(\<Union>a. relations (clock_simMCt t) a)\<^sup>* `` {s} \<subseteq> ?X"
[PROOF STATE]
proof (prove)
using this:
s \<in> worlds (clock_simMCt t)

goal (1 subgoal):
 1. (\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
[PROOF STEP]
apply (clarsimp simp del: mkKripke_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(aa, ba) \<in> worlds (clock_simMCt t); ((aa, ba), a, b) \<in> (\<Union> (range (relations (clock_simMCt t))))\<^sup>*; s = (aa, ba)\<rbrakk> \<Longrightarrow> (a, b) \<in> clock_jkbpCSt t
[PROOF STEP]
apply (erule kripke_rels_trc_worlds)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(aa, ba) \<in> worlds (clock_simMCt t); s = (aa, ba)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> worlds (clock_simMCt t)
 2. \<And>a b aa ba. \<lbrakk>(aa, ba) \<in> worlds (clock_simMCt t); s = (aa, ba)\<rbrakk> \<Longrightarrow> kripke (clock_simMCt t)
 3. \<And>a b aa ba. \<lbrakk>(aa, ba) \<in> worlds (clock_simMCt t); s = (aa, ba)\<rbrakk> \<Longrightarrow> clock_jkbpCSt t = worlds (clock_simMCt t)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<Union> (range (relations (clock_simMCt t))))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
let ?Y = "Clock.jkbpCn (tLength t)"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
let ?X = "clock_sim ` ?Y"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> worlds (clock_simMCt t)
[PROOF STEP]
obtain t'
    where st': "s = clock_sim t'"
      and t'C: "t' \<in> Clock.jkbpC"
      and t'O: "tLength t = tLength t'"
[PROOF STATE]
proof (prove)
using this:
s \<in> worlds (clock_simMCt t)

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>s = clock_sim t'; t' \<in> Clock.jkbpC; tLength t = tLength t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
s = clock_sim t'
t' \<in> Clock.jkbpC
tLength t = tLength t'

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
s = clock_sim t'
t' \<in> Clock.jkbpC
tLength t = tLength t'

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
fix t''
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
assume tt': "(t', t'') \<in> (\<Union>a. relations Clock.MC a)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(t', t'') \<in> (\<Union> (range (relations Clock.MC)))\<^sup>*

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
from t'C tt'
[PROOF STATE]
proof (chain)
picking this:
t' \<in> Clock.jkbpC
(t', t'') \<in> (\<Union> (range (relations Clock.MC)))\<^sup>*
[PROOF STEP]
have t''C: "t'' \<in> Clock.jkbpC"
[PROOF STATE]
proof (prove)
using this:
t' \<in> Clock.jkbpC
(t', t'') \<in> (\<Union> (range (relations Clock.MC)))\<^sup>*

goal (1 subgoal):
 1. t'' \<in> Clock.jkbpC
[PROOF STEP]
by - (erule kripke_rels_trc_worlds, simp_all)
[PROOF STATE]
proof (state)
this:
t'' \<in> Clock.jkbpC

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
from t'O tt'
[PROOF STATE]
proof (chain)
picking this:
tLength t = tLength t'
(t', t'') \<in> (\<Union> (range (relations Clock.MC)))\<^sup>*
[PROOF STEP]
have t''O: "tLength t = tLength t''"
[PROOF STATE]
proof (prove)
using this:
tLength t = tLength t'
(t', t'') \<in> (\<Union> (range (relations Clock.MC)))\<^sup>*

goal (1 subgoal):
 1. tLength t = tLength t''
[PROOF STEP]
by (simp add: Clock.sync_tLength_eq_trc)
[PROOF STATE]
proof (state)
this:
tLength t = tLength t''

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
from t''C t''O
[PROOF STATE]
proof (chain)
picking this:
t'' \<in> Clock.jkbpC
tLength t = tLength t''
[PROOF STEP]
have "t'' \<in> ?Y"
[PROOF STATE]
proof (prove)
using this:
t'' \<in> Clock.jkbpC
tLength t = tLength t''

goal (1 subgoal):
 1. t'' \<in> Clock.jkbpCn (tLength t)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
t'' \<in> Clock.jkbpCn (tLength t)

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(t', ?t''5) \<in> (\<Union> (range (relations Clock.MC)))\<^sup>* \<Longrightarrow> ?t''5 \<in> Clock.jkbpCn (tLength t)

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
hence "(\<Union>a. relations Clock.MC a)\<^sup>* `` {t'} \<subseteq> ?Y"
[PROOF STATE]
proof (prove)
using this:
(t', ?t''5) \<in> (\<Union> (range (relations Clock.MC)))\<^sup>* \<Longrightarrow> ?t''5 \<in> Clock.jkbpCn (tLength t)

goal (1 subgoal):
 1. (\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> Clock.jkbpCn (tLength t)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
(\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> Clock.jkbpCn (tLength t)

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
hence "clock_sim ` ((\<Union>a. relations Clock.MC a)\<^sup>* `` {t'}) \<subseteq> ?X"
[PROOF STATE]
proof (prove)
using this:
(\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> Clock.jkbpCn (tLength t)

goal (1 subgoal):
 1. clock_sim ` (\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> clock_jkbpCSt t
[PROOF STEP]
by (rule image_mono)
[PROOF STATE]
proof (state)
this:
clock_sim ` (\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> clock_jkbpCSt t

goal (6 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
 4. s \<in> worlds clock_simMC
 5. s \<in> worlds (clock_simMCt t)
 6. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
with st' t'C
[PROOF STATE]
proof (chain)
picking this:
s = clock_sim t'
t' \<in> Clock.jkbpC
clock_sim ` (\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> clock_jkbpCSt t
[PROOF STEP]
show "(\<Union>a. relations Clock.MCS a)\<^sup>* `` {s} \<subseteq> ?X"
[PROOF STATE]
proof (prove)
using this:
s = clock_sim t'
t' \<in> Clock.jkbpC
clock_sim ` (\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> clock_jkbpCSt t

goal (1 subgoal):
 1. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
[PROOF STEP]
using sim_trc_commute[OF Clock.mkM_kripke clock_sim, where t=t']
[PROOF STATE]
proof (prove)
using this:
s = clock_sim t'
t' \<in> Clock.jkbpC
clock_sim ` (\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} \<subseteq> clock_jkbpCSt t
t' \<in> worlds Clock.MC \<Longrightarrow> clock_sim ` (\<Union> (range (relations Clock.MC)))\<^sup>* `` {t'} = (\<Union> (range (relations clock_simMC)))\<^sup>* `` {clock_sim t'}

goal (1 subgoal):
 1. (\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Union> (range (relations clock_simMC)))\<^sup>* `` {s} \<subseteq> clock_jkbpCSt t

goal (5 subgoals):
 1. kripke clock_simMC
 2. kripke (clock_simMCt t)
 3. s \<in> worlds clock_simMC
 4. s \<in> worlds (clock_simMCt t)
 5. valuation clock_simMC = valuation (clock_simMCt t)
[PROOF STEP]
qed (insert s, auto)


[STATEMENT]
lemma clock_simAction':
  assumes tC: "t \<in> Clock.jkbpC"
  assumes aec: "ODList.toSet aec = agent_abs a t"
  assumes cec: "ODList.toSet cec = common_abs t"
  shows "set (clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)"
(*<*) (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
from tC aec cec
[PROOF STATE]
proof (chain)
picking this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t
[PROOF STEP]
have "?lhs = set (jAction (clock_repMC (ODList.toSet cec)) (tLast t) a)"
[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. set (local.clock_simAction a (cec, aec)) = set (jAction (clock_repMC (toSet cec)) (tLast t) a)
[PROOF STEP]
by (rule clock_simAction_jAction)
[PROOF STATE]
proof (state)
this:
set (local.clock_simAction a (cec, aec)) = set (jAction (clock_repMC (toSet cec)) (tLast t) a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (local.clock_simAction a (cec, aec)) = set (jAction (clock_repMC (toSet cec)) (tLast t) a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
from tC aec cec
[PROOF STATE]
proof (chain)
picking this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t
[PROOF STEP]
have "... = set (jAction (clock_simMCt t) (clock_sim t) a)"
[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. set (jAction (clock_repMC (toSet cec)) (tLast t) a) = set (jAction (clock_simMCt t) (clock_sim t) a)
[PROOF STEP]
by (simp add: simulation_jAction_eq[OF _ clock_repSim] common_abs_def)
[PROOF STATE]
proof (state)
this:
set (jAction (clock_repMC (toSet cec)) (tLast t) a) = set (jAction (clock_simMCt t) (clock_sim t) a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (jAction (clock_repMC (toSet cec)) (tLast t) a) = set (jAction (clock_simMCt t) (clock_sim t) a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
from tC
[PROOF STATE]
proof (chain)
picking this:
t \<in> Clock.jkbpC
[PROOF STEP]
have "... = set (jAction Clock.MCS (clock_sim t) a)"
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC

goal (1 subgoal):
 1. set (jAction (clock_simMCt t) (clock_sim t) a) = set (jAction clock_simMC (clock_sim t) a)
[PROOF STEP]
using gen_model_jAction_eq[OF clock_submodel_aux[OF tC, where s="clock_sim t"], where w'="clock_sim t"]
          gen_model_world_refl[where w="clock_sim t" and M="clock_simMCt t"]
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
\<lbrakk>clock_sim t \<in> worlds (clock_simMCt t); clock_sim t \<in> worlds (gen_model (clock_simMCt t) (clock_sim t)); kripke clock_simMC; kripke (clock_simMCt t)\<rbrakk> \<Longrightarrow> jAction clock_simMC (clock_sim t) = jAction (clock_simMCt t) (clock_sim t)
clock_sim t \<in> worlds (clock_simMCt t) \<Longrightarrow> clock_sim t \<in> worlds (gen_model (clock_simMCt t) (clock_sim t))

goal (1 subgoal):
 1. set (jAction (clock_simMCt t) (clock_sim t) a) = set (jAction clock_simMC (clock_sim t) a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (jAction (clock_simMCt t) (clock_sim t) a) = set (jAction clock_simMC (clock_sim t) a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (jAction (clock_simMCt t) (clock_sim t) a) = set (jAction clock_simMC (clock_sim t) a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
from tC
[PROOF STATE]
proof (chain)
picking this:
t \<in> Clock.jkbpC
[PROOF STEP]
have "... = set (jAction Clock.MC t a)"
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC

goal (1 subgoal):
 1. set (jAction clock_simMC (clock_sim t) a) = set (jAction Clock.MC t a)
[PROOF STEP]
by (simp add: simulation_jAction_eq[OF _ clock_sim])
[PROOF STATE]
proof (state)
this:
set (jAction clock_simMC (clock_sim t) a) = set (jAction Clock.MC t a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)

goal (1 subgoal):
 1. set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (local.clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clock_simAction:
  assumes tC: "t \<in> Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "set (clock_simAction a ec) = set (jAction Clock.MC t a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.clock_simAction a ec) = set (jAction Clock.MC t a)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.clock_simAction a ec) = set (jAction Clock.MC t a)
[PROOF STEP]
using assms clock_simAction'[OF tC, where cec="fst ec" and aec="snd ec"]
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
clock_simAbs ec = Clock.sim_equiv_class a t
\<lbrakk>toSet (snd ec) = agent_abs ?a t; toSet (fst ec) = common_abs t\<rbrakk> \<Longrightarrow> set (local.clock_simAction ?a (fst ec, snd ec)) = set (jAction Clock.MC t ?a)

goal (1 subgoal):
 1. set (local.clock_simAction a ec) = set (jAction Clock.MC t a)
[PROOF STEP]
apply (simp add: common_abs agent_abs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done