[STATEMENT]
lemma clock_trans_aux:
  assumes t'C: "t' \<in> Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a' t'"
      and tC: "t \<in> Clock.jkbpCn (tLength t')"
      and eact: "eact \<in> set (envAction (tLast t))"
  shows "(aact \<in> set (listToFuns (\<lambda>a. clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t)))
                            (toList agents)))
     \<longleftrightarrow> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t))) (toList agents))) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t' \<in> Clock.jkbpC
clock_simAbs ec = Clock.sim_equiv_class a' t'
t \<in> Clock.jkbpCn (tLength t')
eact \<in> set (envAction (tLast t))

goal (1 subgoal):
 1. (aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t))) (toList agents))) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = Clock.sim_equiv_class a' t'; t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t))\<rbrakk> \<Longrightarrow> (aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t))) (toList agents))) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (frule Clock.jkbpCn_jkbpC_inc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = Clock.sim_equiv_class a' t'; t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t))) (toList agents))) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (clarsimp simp: listToFuns_ext[OF agents[unfolded toSet_def]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (\<forall>x. aact x \<in> set (local.clock_simAction x (fst ec, clock_knowledge envObs (fst ec) x (tLast t)))) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (subst clock_simAction')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> ?t6 \<in> Clock.jkbpC
 2. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> toSet (clock_knowledge envObs (fst ec) x (tLast t)) = agent_abs x ?t6
 3. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> toSet (fst ec) = common_abs ?t6
 4. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (\<forall>x. aact x \<in> set (jAction Clock.MC ?t6 x)) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (erule Clock.jkbpCn_jkbpC_inc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> toSet (clock_knowledge envObs (fst ec) x (tLast t)) = agent_abs x t
 2. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> toSet (fst ec) = common_abs t
 3. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (\<forall>x. aact x \<in> set (jAction Clock.MC t x)) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (subst clock_coEC_relation_image)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> tLast t \<in> toSet (fst ec)
 2. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> relations (clock_repMC (toSet (fst ec))) x `` {tLast t} = agent_abs x t
 3. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> toSet (fst ec) = common_abs t
 4. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (\<forall>x. aact x \<in> set (jAction Clock.MC t x)) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (simp add: common_abs common_abs_def toSet_def[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> relations (clock_repMC (toSet (fst ec))) x `` {tLast t} = agent_abs x t
 2. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> toSet (fst ec) = common_abs t
 3. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (\<forall>x. aact x \<in> set (jAction Clock.MC t x)) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (fastforce simp: common_abs agent_abs_def common_abs_def clock_repRels_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> toSet (fst ec) = common_abs t
 2. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (\<forall>x. aact x \<in> set (jAction Clock.MC t x)) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (simp add: common_abs common_abs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<in> Clock.jkbpC; clock_simAbs ec = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = tLength t' \<and> envObs a' (tLast t'a) = envObs a' (tLast t')); t \<in> Clock.jkbpCn (tLength t'); eact \<in> set (envAction (tLast t)); t \<in> Clock.jkbpC\<rbrakk> \<Longrightarrow> (\<forall>x. aact x \<in> set (jAction Clock.MC t x)) = (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t')) t a))
[PROOF STEP]
apply (simp add: Clock.jkbpC_jkbpCn_jAction_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_trans_common:
  assumes tC: "t \<in> Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (clock_trans (fst ec) (fst ec))
       = { s |t' s. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t }"
(*<*) (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (local.clock_trans (fst ec) (fst ec)) = rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. toSet (local.clock_trans (fst ec) (fst ec)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t)
 2. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> toSet (local.clock_trans (fst ec) (fst ec))
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (local.clock_trans (fst ec) (fst ec)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
unfolding clock_trans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (fromList (concat (map (\<lambda>s. concat (map (\<lambda>eact. map (\<lambda>aact. envTrans eact aact s) (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a s)) (toList agents))) (envAction s))) (toList (fst ec))))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] common_abs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb aact. \<lbrakk>xa \<in> Clock.jkbpCn (tLength t); xb \<in> set (envAction (tLast xa)); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast xa))) (toList agents))\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> envTrans xb aact (tLast xa) \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (rule_tac x=xa in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb aact. \<lbrakk>xa \<in> Clock.jkbpCn (tLength t); xb \<in> set (envAction (tLast xa)); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast xa))) (toList agents))\<rbrakk> \<Longrightarrow> xa \<leadsto> envTrans xb aact (tLast xa) \<in> Clock.jkbpC \<and> tLength xa = tLength t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb aact. \<lbrakk>xa \<in> Clock.jkbpCn (tLength t); xb \<in> set (envAction (tLast xa)); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast xa))) (toList agents))\<rbrakk> \<Longrightarrow> xa \<leadsto> envTrans xb aact (tLast xa) \<in> Clock.jkbpC
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb aact. \<lbrakk>xa \<in> Clock.jkbpCn (tLength t); xb \<in> set (envAction (tLast xa)); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast xa))) (toList agents))\<rbrakk> \<Longrightarrow> xa \<leadsto> envTrans xb aact (tLast xa) \<in> Clock.jkbpCn (Suc (tLength t))
[PROOF STEP]
apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
toSet (local.clock_trans (fst ec) (fst ec)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t)

goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> toSet (local.clock_trans (fst ec) (fst ec))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> toSet (local.clock_trans (fst ec) (fst ec))
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> toSet (local.clock_trans (fst ec) (fst ec))
[PROOF STEP]
unfolding clock_trans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> toSet (fromList (concat (map (\<lambda>s. concat (map (\<lambda>eact. map (\<lambda>aact. envTrans eact aact s) (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a s)) (toList agents))) (envAction s))) (toList (fst ec)))))
[PROOF STEP]
apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] common_abs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x t'. \<lbrakk>t' \<leadsto> x \<in> Clock.jkbpC; tLength t' = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Clock.jkbpCn (tLength t). \<exists>xb\<in>set (envAction (tLast xa)). x \<in> (\<lambda>aact. envTrans xb aact (tLast xa)) ` set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast xa))) (toList agents))
[PROOF STEP]
apply (drule Clock.jkbpC_tLength_inv[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t'. tLength t' = tLength t \<Longrightarrow> tLength (t' \<leadsto> x) = Suc (tLength t)
 2. \<And>x t'. \<lbrakk>tLength t' = tLength t; t' \<leadsto> x \<in> Clock.jkbpCn (Suc (tLength t))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Clock.jkbpCn (tLength t). \<exists>xb\<in>set (envAction (tLast xa)). x \<in> (\<lambda>aact. envTrans xb aact (tLast xa)) ` set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast xa))) (toList agents))
[PROOF STEP]
apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> toSet (local.clock_trans (fst ec) (fst ec))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clock_trans_agent:
  assumes tC: "t \<in> Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (clock_trans (fst ec) (snd ec))
       = { s |t' s. t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t }"
(*<*) (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (local.clock_trans (fst ec) (snd ec)) = rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. toSet (local.clock_trans (fst ec) (snd ec)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
 2. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> toSet (local.clock_trans (fst ec) (snd ec))
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (local.clock_trans (fst ec) (snd ec)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
unfolding clock_trans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (fromList (concat (map (\<lambda>s. concat (map (\<lambda>eact. map (\<lambda>aact. envTrans eact aact s) (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a s)) (toList agents))) (envAction s))) (toList (snd ec))))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] agent_abs[OF assms] common_abs_def agent_abs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xb aact t'. \<lbrakk>xb \<in> set (envAction (tLast t')); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t'))) (toList agents)); t' \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> \<exists>t'a. t'a \<leadsto> envTrans xb aact (tLast t') \<in> Clock.jkbpC \<and> tLength t'a = tLength t \<and> envObs a (tLast t'a) = envObs a (tLast t)
[PROOF STEP]
apply (rule_tac x=t' in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xb aact t'. \<lbrakk>xb \<in> set (envAction (tLast t')); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t'))) (toList agents)); t' \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> t' \<leadsto> envTrans xb aact (tLast t') \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xb aact t'. \<lbrakk>xb \<in> set (envAction (tLast t')); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t'))) (toList agents)); t' \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> t' \<leadsto> envTrans xb aact (tLast t') \<in> Clock.jkbpC
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xb aact t'. \<lbrakk>xb \<in> set (envAction (tLast t')); aact \<in> set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t'))) (toList agents)); t' \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> t' \<leadsto> envTrans xb aact (tLast t') \<in> Clock.jkbpCn (Suc (tLength t))
[PROOF STEP]
apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
toSet (local.clock_trans (fst ec) (snd ec)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)

goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> toSet (local.clock_trans (fst ec) (snd ec))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> toSet (local.clock_trans (fst ec) (snd ec))
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> toSet (local.clock_trans (fst ec) (snd ec))
[PROOF STEP]
unfolding clock_trans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> toSet (fromList (concat (map (\<lambda>s. concat (map (\<lambda>eact. map (\<lambda>aact. envTrans eact aact s) (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a s)) (toList agents))) (envAction s))) (toList (snd ec)))))
[PROOF STEP]
apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] agent_abs[OF assms] common_abs_def agent_abs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x t'. \<lbrakk>t' \<leadsto> x \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>t'. xa = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)) \<and> (\<exists>xb\<in>set (envAction xa). x \<in> (\<lambda>aact. envTrans xb aact xa) ` set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a xa)) (toList agents)))
[PROOF STEP]
apply (drule Clock.jkbpC_tLength_inv[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t'. \<lbrakk>tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> tLength (t' \<leadsto> x) = Suc (tLength t)
 2. \<And>x t'. \<lbrakk>tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); t' \<leadsto> x \<in> Clock.jkbpCn (Suc (tLength t))\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>t'. xa = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)) \<and> (\<exists>xb\<in>set (envAction xa). x \<in> (\<lambda>aact. envTrans xb aact xa) ` set (listToFuns (\<lambda>a. local.clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a xa)) (toList agents)))
[PROOF STEP]
apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> toSet (local.clock_trans (fst ec) (snd ec))

goal:
No subgoals!
[PROOF STEP]
qed