[STATEMENT]
lemma parts_mpair_1:
 "parts (insert \<lbrace>X, Y\<rbrace> H) \<subseteq> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert \<lbrace>X, Y\<rbrace> H) \<subseteq> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (insert \<lbrace>X, Y\<rbrace> H) \<Longrightarrow> x \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
[PROOF STEP]
apply (erule parts.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x Xa. Xa \<in> insert \<lbrace>X, Y\<rbrace> H \<Longrightarrow> Xa \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
 2. \<And>x Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))\<rbrakk> \<Longrightarrow> Xa \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
 3. \<And>x Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))\<rbrakk> \<Longrightarrow> Ya \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
 4. \<And>x K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))\<rbrakk> \<Longrightarrow> Xa \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
 5. \<And>x xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
 6. \<And>x xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> insert \<lbrace>X, Y\<rbrace> (parts ({X, Y} \<union> H))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Xa. Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> H \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya = \<lbrace>X, Y\<rbrace> \<or> Ya \<in> parts (insert X (insert Y H))
 4. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>Xa. Xa = \<lbrace>X, Y\<rbrace> \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 2. \<And>Xa. Xa \<in> H \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 4. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya = \<lbrace>X, Y\<rbrace> \<or> Ya \<in> parts (insert X (insert Y H))
 5. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 7. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Xa. Xa \<in> H \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya = \<lbrace>X, Y\<rbrace> \<or> Ya \<in> parts (insert X (insert Y H))
 4. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa = \<lbrace>X, Y\<rbrace> \<or> Xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (rule_tac [1-4] disjI2)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Xa. Xa \<in> H \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 4. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (rule parts.Inj)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Xa. Xa \<in> H \<Longrightarrow> Xa \<in> insert X (insert Y H)
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 4. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 3. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 4. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 4. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Xa. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X\<rbrakk> \<Longrightarrow> X \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 4. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (rule parts.Inj)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Xa. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X\<rbrakk> \<Longrightarrow> X \<in> insert X (insert Y H)
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 3. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 4. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 6. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 3. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 4. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule parts.Fst)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y \<or> \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 2. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 3. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 4. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X \<and> Ya = Y\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 3. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 4. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Xa. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X\<rbrakk> \<Longrightarrow> Y \<in> parts (insert X (insert Y H))
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 3. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 4. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (rule parts.Inj)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Xa. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Xa = X\<rbrakk> \<Longrightarrow> Y \<in> insert X (insert Y H)
 2. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 3. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 4. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 5. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> parts (insert \<lbrace>X, Y\<rbrace> H); \<lbrace>Xa, Ya\<rbrace> \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Ya \<in> parts (insert X (insert Y H))
 2. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 3. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 4. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule parts.Snd)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>K Xa. \<lbrakk>Crypt K Xa \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Crypt K Xa \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Xa \<in> parts (insert X (insert Y H))
 2. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 3. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule parts.Body)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK xa \<in> parts (insert X (insert Y H))
 2. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule parts.Auth_Fst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>Auth_Data xa y \<in> parts (insert \<lbrace>X, Y\<rbrace> H); Auth_Data xa y \<in> parts (insert X (insert Y H))\<rbrakk> \<Longrightarrow> Pri_AgrK y \<in> parts (insert X (insert Y H))
[PROOF STEP]
apply (erule parts.Auth_Snd)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bisimSubstResNil:
  fixes \<Psi> :: 'b
  and   x :: name

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero> \<sim>\<^sub>s \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero> \<sim>\<^sub>s \<zero>
[PROOF STEP]
proof(rule closeSubstI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero>[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]
[PROOF STEP]
fix \<sigma>:: "(name list \<times> 'a list) list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero>[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]
[PROOF STEP]
assume "wellFormedSubst \<sigma>"
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero>[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]
[PROOF STEP]
obtain y::name where "y \<sharp> \<Psi>" and "y \<sharp> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<sharp> \<Psi>; y \<sharp> \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(generate_fresh "name") (auto simp add: fresh_prod)
[PROOF STATE]
proof (state)
this:
y \<sharp> \<Psi>
y \<sharp> \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero>[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]
[PROOF STEP]
have "\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>\<zero> \<sim> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>y\<rparr>\<zero> \<sim> \<zero>
[PROOF STEP]
by(rule bisimResNil)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>\<zero> \<sim> \<zero>

goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero>[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]
[PROOF STEP]
with \<open>y \<sharp> \<sigma>\<close> \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> \<sigma>
wellFormedSubst \<sigma>
\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>\<zero> \<sim> \<zero>
[PROOF STEP]
show "\<Psi> \<rhd> (\<lparr>\<nu>x\<rparr>\<zero>)[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> \<sigma>
wellFormedSubst \<sigma>
\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>\<zero> \<sim> \<zero>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero>[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]
[PROOF STEP]
by(subst alphaRes[of y]) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero>[<\<sigma>>] \<sim> \<zero>[<\<sigma>>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem secure: "secure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
proof (intro preserve_source_secure ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
fix aid
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
interpret Receiver: OuterFriendReceiver UIDs AID UID aid
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OuterFriendReceiver UIDs AID UID
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
assume "aid \<in> AIDs - {AID}"
[PROOF STATE]
proof (state)
this:
aid \<in> nodes'

goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
aid \<in> nodes'
[PROOF STEP]
show "Net.lsecure aid"
[PROOF STATE]
proof (prove)
using this:
aid \<in> nodes'

goal (1 subgoal):
 1. Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
using Receiver.secure
[PROOF STATE]
proof (prove)
using this:
aid \<in> nodes'
Receiver.secure

goal (1 subgoal):
 1. Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (\<lambda>a. False))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reductio_aa_4[PLM]:
    "\<lbrakk>[\<phi> \<^bold>\<rightarrow> \<^bold>\<not>\<psi> in v]; [\<phi> \<^bold>\<rightarrow> \<psi> in v]\<rbrakk> \<Longrightarrow> [\<^bold>\<not>\<phi> in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[\<phi> \<^bold>\<rightarrow> \<^bold>\<not>\<psi> in v]; [\<phi> \<^bold>\<rightarrow> \<psi> in v]\<rbrakk> \<Longrightarrow> [\<^bold>\<not>\<phi> in v]
[PROOF STEP]
using reductio_aa_2 vdash_properties_10
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>[?\<phi> in ?v] \<Longrightarrow> [\<^bold>\<not>?\<psi> in ?v]; [?\<phi> in ?v] \<Longrightarrow> [?\<psi> in ?v]\<rbrakk> \<Longrightarrow> [\<^bold>\<not>?\<phi> in ?v]
\<lbrakk>[?\<phi> \<^bold>\<rightarrow> ?\<psi> in ?v]; [?\<phi> in ?v]\<rbrakk> \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. \<lbrakk>[\<phi> \<^bold>\<rightarrow> \<^bold>\<not>\<psi> in v]; [\<phi> \<^bold>\<rightarrow> \<psi> in v]\<rbrakk> \<Longrightarrow> [\<^bold>\<not>\<phi> in v]
[PROOF STEP]
by blast


[STATEMENT]
lemma oth_class_taut_3_d[PLM]:
    "[(\<phi> \<^bold>\<or> \<phi>) \<^bold>\<equiv> \<phi> in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<phi> \<^bold>\<or> \<phi> \<^bold>\<equiv> \<phi> in v]
[PROOF STEP]
by PLM_solver


[STATEMENT]
lemma lambda_p_q_p_eq_q[PLM]:
    "[((\<^bold>\<lambda>\<^sup>0 p) \<^bold>= (\<^bold>\<lambda>\<^sup>0 q)) \<^bold>\<equiv> (p \<^bold>= q) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<lambda>\<^sup>0 p \<^bold>= \<^bold>\<lambda>\<^sup>0 q \<^bold>\<equiv> p \<^bold>= q in v]
[PROOF STEP]
using eta_conversion_lemma_0
          l_identity[axiom_instance, deduction, deduction]
          eta_conversion_lemma_0[eq_sym] "\<^bold>\<equiv>I" CP
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<lambda>\<^sup>0 ?p \<^bold>= ?p in ?v]
\<lbrakk>[?\<alpha>3 \<^bold>= ?\<beta>3 in ?v]; [?\<phi>3 ?\<alpha>3 in ?v]\<rbrakk> \<Longrightarrow> [?\<phi>3 ?\<beta>3 in ?v]
[?y1 \<^bold>= \<^bold>\<lambda>\<^sup>0 ?y1 in ?v]
\<lbrakk>[?\<phi> \<^bold>\<rightarrow> ?\<psi> in ?v]; [?\<psi> \<^bold>\<rightarrow> ?\<phi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> \<^bold>\<equiv> ?\<psi> in ?v]
([?\<phi> in ?v] \<Longrightarrow> [?\<psi> in ?v]) \<Longrightarrow> [?\<phi> \<^bold>\<rightarrow> ?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<lambda>\<^sup>0 p \<^bold>= \<^bold>\<lambda>\<^sup>0 q \<^bold>\<equiv> p \<^bold>= q in v]
[PROOF STEP]
by metis


[STATEMENT]
lemma set_val_pointers_preserved:
  assumes "w \<in> set_val_locs character_data_ptr"
  assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
using assms CD.set_val_pointers_preserved
[PROOF STATE]
proof (prove)
using this:
w \<in> set_val_locs character_data_ptr
h \<turnstile> w \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> set_val_locs ?character_data_ptr; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> object_ptr_kinds ?h = object_ptr_kinds ?h'

goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
by simp


[STATEMENT]
lemma mat_inter_num_MM_Rel:
  assumes "MM_Rel A B"
  assumes "j1 < dim_col A" "j2 < dim_col B"
  shows "mat_inter_num (mat_mod A) j1 j2 = mat_inter_num B j1 j2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_inter_num (local.mat_mod A) j1 j2 = mat_inter_num B j1 j2
[PROOF STEP]
unfolding mat_inter_num_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i < dim_row (local.mat_mod A) \<and> local.mat_mod A $$ (i, j1) = 1 \<and> local.mat_mod A $$ (i, j2) = 1} = card {i. i < dim_row B \<and> B $$ (i, j1) = 1 \<and> B $$ (i, j2) = 1}
[PROOF STEP]
using assms index_map_mat mat_mod_dim(2)
[PROOF STATE]
proof (prove)
using this:
MM_Rel A B
j1 < dim_col A
j2 < dim_col B
\<lbrakk>?i < dim_row ?A; ?j < dim_col ?A\<rbrakk> \<Longrightarrow> map_mat ?f ?A $$ (?i, ?j) = ?f (?A $$ (?i, ?j))
dim_row (map_mat ?f ?A) = dim_row ?A
dim_col (map_mat ?f ?A) = dim_col ?A
dim_col (local.mat_mod ?M) = dim_col ?M

goal (1 subgoal):
 1. card {i. i < dim_row (local.mat_mod A) \<and> local.mat_mod A $$ (i, j1) = 1 \<and> local.mat_mod A $$ (i, j2) = 1} = card {i. i < dim_row B \<and> B $$ (i, j1) = 1 \<and> B $$ (i, j2) = 1}
[PROOF STEP]
by (smt (z3) Collect_cong MM_Rel_def to_int_mod_ring_hom.hom_1 to_int_mod_ring_hom.hom_one)


[STATEMENT]
lemma type_less_eq_x_String [elim!]:
  "\<tau> \<le> String \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = String \<Longrightarrow> P) \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<le> String; \<tau> = OclVoid \<Longrightarrow> P; \<tau> = String \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (drule le_imp_less_or_eq; auto)


[STATEMENT]
lemma (in is_cat_equalizer) cat_eq_unique':
  assumes "\<epsilon>' : E' <\<^sub>C\<^sub>F\<^sub>.\<^sub>e\<^sub>q (\<aa>,\<bb>,F,F') : \<Up>\<^sub>C \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<exists>!f'. f' : E' \<mapsto>\<^bsub>\<CC>\<^esub> E \<and> \<epsilon>'\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> = \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f'. f' : E' \<mapsto>\<^bsub>\<CC>\<^esub> E \<and> \<epsilon>'\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> = \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!f'. f' : E' \<mapsto>\<^bsub>\<CC>\<^esub> E \<and> \<epsilon>'\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> = \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f'
[PROOF STEP]
interpret \<epsilon>': is_cat_equalizer \<alpha> \<aa> \<bb> F F' \<CC> E' \<epsilon>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon>' : E' <\<^sub>C\<^sub>F\<^sub>.\<^sub>e\<^sub>q (\<aa>,\<bb>,F,F') : \<Up>\<^sub>C \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!f'. f' : E' \<mapsto>\<^bsub>\<CC>\<^esub> E \<and> \<epsilon>'\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> = \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f'. f' : E' \<mapsto>\<^bsub>\<CC>\<^esub> E \<and> \<epsilon>'\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> = \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f'
[PROOF STEP]
by (rule cat_eq_unique_cone[OF \<epsilon>'.is_cat_cone_axioms])
[PROOF STATE]
proof (state)
this:
\<exists>!f'. f' : E' \<mapsto>\<^bsub>\<CC>\<^esub> E \<and> \<epsilon>'\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> = \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L F\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma conv_finite_path:
  "finite_path x \<longleftrightarrow> finite_path (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_path x = finite_path (x\<^sup>T)
[PROOF STEP]
using conv_finite conv_path
[PROOF STATE]
proof (prove)
using this:
relation_algebra_rtc_class.finite ?x = relation_algebra_rtc_class.finite (?x\<^sup>T)
path ?x = path (?x\<^sup>T)

goal (1 subgoal):
 1. finite_path x = finite_path (x\<^sup>T)
[PROOF STEP]
by blast


[STATEMENT]
lemma many_strongly_connected_iff_5:
  "many_strongly_connected x \<longleftrightarrow> x\<^sup>\<star>;x\<^sup>T \<le> x\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. many_strongly_connected x = (x\<^sup>\<star> ; x\<^sup>T \<le> x\<^sup>+)
[PROOF STEP]
by (metis comp_assoc conv_contrav conway.dagger_unfoldr_distr star_conv star_denest_var_2
          star_invol star_trans_eq star_unfoldl_eq sup.boundedE many_strongly_connected_iff_2)


[STATEMENT]
lemma If2_split_asm: "P (If2 Q x y) \<longleftrightarrow> \<not>(Q = \<bottom> \<and> \<not>P \<bottom> \<or> Q = TT \<and> \<not>P x \<or> Q = FF \<and> \<not>P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (If2 Q x y) = (\<not> (Q = \<bottom> \<and> \<not> P \<bottom> \<or> Q = TT \<and> \<not> P x \<or> Q = FF \<and> \<not> P y))
[PROOF STEP]
by (cases Q) (simp_all add: If2_def)


[STATEMENT]
lemma trim_code[code]:
  "trim = dropWhile (\<lambda> c. let ci = integer_of_char c
    in if ci \<ge> 34 then False else ci = 32 \<or> ci = 10 \<or> ci = 9 \<or> ci = 13)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trim = dropWhile (\<lambda>c. let ci = integer_of_char c in if 34 \<le> ci then False else ci = 32 \<or> ci = 10 \<or> ci = 9 \<or> ci = 13)
[PROOF STEP]
unfolding trim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dropWhile (\<lambda>c. c \<in> set [CHR '' '', CHR ''\<newline>'', CHR 0x09, CHR 0x0D]) = dropWhile (\<lambda>c. let ci = integer_of_char c in if 34 \<le> ci then False else ci = 32 \<or> ci = 10 \<or> ci = 9 \<or> ci = 13)
[PROOF STEP]
apply (rule arg_cong[of _ _ dropWhile], rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. (c \<in> set [CHR '' '', CHR ''\<newline>'', CHR 0x09, CHR 0x0D]) = (let ci = integer_of_char c in if 34 \<le> ci then False else ci = 32 \<or> ci = 10 \<or> ci = 9 \<or> ci = 13)
[PROOF STEP]
unfolding Let_def in_set_simps less_eq_char_code char_eq_via_integer_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. (integer_of_char c = integer_of_char CHR '' '' \<or> integer_of_char c = integer_of_char CHR ''\<newline>'' \<or> integer_of_char c = integer_of_char CHR 0x09 \<or> integer_of_char c = integer_of_char CHR 0x0D) = (if 34 \<le> integer_of_char c then False else integer_of_char c = 32 \<or> integer_of_char c = 10 \<or> integer_of_char c = 9 \<or> integer_of_char c = 13)
[PROOF STEP]
by (auto simp: integer_of_char_def Let_def)


[STATEMENT]
lemma (in Ring) Zm_to_M_0:"\<lbrakk>R module M; f \<in> mHom R (Zm R e) M\<rbrakk> \<Longrightarrow>
                     f e = \<zero>\<^bsub>M\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R module M; f \<in> mHom R (Zm R e) M\<rbrakk> \<Longrightarrow> f e = \<zero>\<^bsub>M\<^esub>
[PROOF STEP]
apply (cut_tac Zm_Module [of e])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R module M; f \<in> mHom R (Zm R e) M; R module Zm R e\<rbrakk> \<Longrightarrow> f e = \<zero>\<^bsub>M\<^esub>
[PROOF STEP]
apply (frule Module.mHom_add [of "Zm R e" R M f e e], assumption+,
        (simp add:Zm_carrier)+,
        frule_tac R = R and M = "Zm R e" in Module.module_is_ag,
        frule_tac x = e and y = e in aGroup.ag_pOp_closed[of "Zm R e"],
        (simp add:Zm_carrier)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R module M; f \<in> mHom R (Zm R e) M; R module Zm R e; f e = f e \<plusminus>\<^bsub>M\<^esub> f e; aGroup (Zm R e); e \<plusminus>\<^bsub>Zm R e\<^esub> e = e\<rbrakk> \<Longrightarrow> f e = \<zero>\<^bsub>M\<^esub>
[PROOF STEP]
apply (frule_tac R = R and M = "Zm R e" and N = M and f = f and m = e in
        Module.mHom_mem, assumption+, simp add:Zm_carrier,
        frule sym, thin_tac "f e =  f e  \<plusminus>\<^bsub>M\<^esub> (f e)",
        frule_tac R = R and M = M in Module.module_is_ag,
        frule aGroup.ag_eq_sol2 [of M "f e" "f e" "f e"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R module M; f \<in> mHom R (Zm R e) M; R module Zm R e; aGroup (Zm R e); e \<plusminus>\<^bsub>Zm R e\<^esub> e = e; f e \<in> carrier M; f e \<plusminus>\<^bsub>M\<^esub> f e = f e; aGroup M; f e = f e \<plusminus>\<^bsub>M\<^esub> -\<^sub>a\<^bsub>M\<^esub> f e\<rbrakk> \<Longrightarrow> f e = \<zero>\<^bsub>M\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]:
    "ppath (s\<lparr>state.more := state.more s'\<rparr>) = ppath s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ppath (s\<lparr>state.more := state.more s'\<rparr>) = ppath s'
[PROOF STEP]
by (cases s, cases s') auto


[STATEMENT]
lemma (in program) trace_to_steps:
assumes trace: "trace c 0 k"
shows steps: "c 0 \<Rightarrow>\<^sub>d\<^sup>* c k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c 0 \<Rightarrow>\<^sub>d\<^sup>* c k
[PROOF STEP]
using trace
[PROOF STATE]
proof (prove)
using this:
trace c 0 k

goal (1 subgoal):
 1. c 0 \<Rightarrow>\<^sub>d\<^sup>* c k
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trace c 0 0 \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c 0
 2. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
trace c 0 0

goal (2 subgoals):
 1. trace c 0 0 \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c 0
 2. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
show "c 0 \<Rightarrow>\<^sub>d\<^sup>* c 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c 0 \<Rightarrow>\<^sub>d\<^sup>* c 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c 0

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k
trace c 0 (Suc k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
have prem: "trace c 0 (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace c 0 (Suc k)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
trace c 0 (Suc k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
hence "trace c 0 k"
[PROOF STATE]
proof (prove)
using this:
trace c 0 (Suc k)

goal (1 subgoal):
 1. trace c 0 k
[PROOF STEP]
by (auto simp add: program_trace_def)
[PROOF STATE]
proof (state)
this:
trace c 0 k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
from Suc.hyps [OF this]
[PROOF STATE]
proof (chain)
picking this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c k
[PROOF STEP]
have "c 0 \<Rightarrow>\<^sub>d\<^sup>* c k"
[PROOF STATE]
proof (prove)
using this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c k

goal (1 subgoal):
 1. c 0 \<Rightarrow>\<^sub>d\<^sup>* c k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
term program_trace
[PROOF STATE]
proof (state)
this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
from prem
[PROOF STATE]
proof (chain)
picking this:
trace c 0 (Suc k)
[PROOF STEP]
interpret program_trace program_step  c 0 "Suc k"
[PROOF STATE]
proof (prove)
using this:
trace c 0 (Suc k)

goal (1 subgoal):
 1. trace c 0 (Suc k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
from step [of k]
[PROOF STATE]
proof (chain)
picking this:
k < Suc k \<Longrightarrow> c (0 + k) \<Rightarrow>\<^sub>d c (0 + Suc k)
[PROOF STEP]
have "c (k) \<Rightarrow>\<^sub>d c (Suc k)"
[PROOF STATE]
proof (prove)
using this:
k < Suc k \<Longrightarrow> c (0 + k) \<Rightarrow>\<^sub>d c (0 + Suc k)

goal (1 subgoal):
 1. c k \<Rightarrow>\<^sub>d c (Suc k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c k \<Rightarrow>\<^sub>d c (Suc k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>trace c 0 k \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c k; trace c 0 (Suc k)\<rbrakk> \<Longrightarrow> c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)

goal (1 subgoal):
 1. c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c 0 \<Rightarrow>\<^sub>d\<^sup>* c (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delete_first_eq_none [simp] :
  "delete_first P l = None \<longleftrightarrow> (\<forall>x \<in> set l. \<not> (P x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (delete_first P l = None) = (\<forall>x\<in>set l. \<not> P x)
[PROOF STEP]
by (induct l) (auto simp add: delete_first_unroll)


[STATEMENT]
lemma ts_process_futures:
 "trace_set T \<Longrightarrow>
  futures (ts_process T) xs =
  {(ys, Y). xs @ ys \<in> T \<and> (\<forall>y \<in> Y. xs @ ys @ [y] \<notin> T)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_set T \<Longrightarrow> futures (ts_process T) xs = {(ys, Y). xs @ ys \<in> T \<and> (\<forall>y\<in>Y. xs @ ys @ [y] \<notin> T)}
[PROOF STEP]
by (simp add: futures_def ts_process_failures)


[STATEMENT]
lemma succ_to_list_pat[autoref_op_pat]: "it_to_sorted_list (\<lambda>_ _. True) (Graph.succ g v) \<equiv> succ_to_list g v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list (\<lambda>_ _. True) (succ g v) \<equiv> succ_to_list g v
[PROOF STEP]
unfolding succ_to_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list (\<lambda>_ _. True) (succ g v) \<equiv> it_to_sorted_list (\<lambda>_ _. True) (succ g v)
[PROOF STEP]
by simp