[STATEMENT]
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>A = 0\<rbrace>
      \<lbrace>\<acute>A < 0\<rbrace> \<longmapsto> BASIC
       LET (a,b,c) = foo \<acute>A
       IN
            \<acute>A :== a,
            \<acute>G :== b + \<acute>B,
            \<acute>H :== c
      END
      \<lbrace>\<acute>A = x \<and> \<acute>G = y \<and> \<acute>H = c\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>A = 0\<rbrace> (False, \<lbrace>\<acute>A < 0\<rbrace>)\<longmapsto> BASIC LET (a, b, c) = foo \<acute>A IN \<acute>H :== c END \<lbrace>\<acute>A = x \<and> \<acute>G = y \<and> \<acute>H = c\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. A = 0 \<Longrightarrow> A < 0 \<and> fst (foo A) = x \<and> fst (snd (foo A)) + B = y \<and> snd (snd (foo A)) = c
[PROOF STEP]
oops


[STATEMENT]
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>A = 0\<rbrace>
      \<lbrace>\<acute>A < 0\<rbrace> \<longmapsto> BASIC
       LET (a,b,c) = foo \<acute>A
       IN
            \<acute>A :== a,
            \<acute>G :== b + \<acute>B,
            \<acute>H :== c
      END
      \<lbrace>\<acute>A = x \<and> \<acute>G = y \<and> \<acute>H = c\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>A = 0\<rbrace> (False, \<lbrace>\<acute>A < 0\<rbrace>)\<longmapsto> BASIC LET (a, b, c) = foo \<acute>A IN \<acute>H :== c END \<lbrace>\<acute>A = x \<and> \<acute>G = y \<and> \<acute>H = c\<rbrace>
[PROOF STEP]
apply (vcg add: foo_def snd_conv fst_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. A = 0 \<Longrightarrow> A < 0 \<and> A = x \<and> A + 1 + B = y \<and> A + 2 = c
[PROOF STEP]
oops


[STATEMENT]
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<union> (B \<union> A) = B \<union> A
[PROOF STEP]
by blast


[STATEMENT]
lemma parts_mono: "G \<subseteq> H \<Longrightarrow> parts(G) \<subseteq> parts(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<subseteq> H \<Longrightarrow> parts G \<subseteq> parts H
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>G \<subseteq> H; x \<in> parts G\<rbrakk> \<Longrightarrow> x \<in> parts H
[PROOF STEP]
apply (erule parts.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x X. \<lbrakk>G \<subseteq> H; X \<in> G\<rbrakk> \<Longrightarrow> X \<in> parts H
 2. \<And>x X Y. \<lbrakk>G \<subseteq> H; \<lbrace>X, Y\<rbrace> \<in> parts G; \<lbrace>X, Y\<rbrace> \<in> parts H\<rbrakk> \<Longrightarrow> X \<in> parts H
 3. \<And>x X Y. \<lbrakk>G \<subseteq> H; \<lbrace>X, Y\<rbrace> \<in> parts G; \<lbrace>X, Y\<rbrace> \<in> parts H\<rbrakk> \<Longrightarrow> Y \<in> parts H
 4. \<And>x K X. \<lbrakk>G \<subseteq> H; Crypt K X \<in> parts G; Crypt K X \<in> parts H\<rbrakk> \<Longrightarrow> X \<in> parts H
[PROOF STEP]
apply (blast dest: parts.Fst parts.Snd parts.Body)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Friend x \<in> Friend ` A) = (x \<in> A)
[PROOF STEP]
by auto


[STATEMENT]
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Key x \<in> Key ` A) = (x \<in> A)
[PROOF STEP]
by auto


[STATEMENT]
lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nonce x \<notin> Key ` A
[PROOF STEP]
by auto


[STATEMENT]
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invKey K = invKey K') = (K = K')
[PROOF STEP]
by (metis invKey)


[STATEMENT]
lemma keysFor_empty [simp]: "keysFor {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor {} = {}
[PROOF STEP]
by (unfold keysFor_def, blast)


[STATEMENT]
lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (H \<union> H') = keysFor H \<union> keysFor H'
[PROOF STEP]
by (unfold keysFor_def, blast)


[STATEMENT]
lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (\<Union> (H ` A)) = (\<Union>i\<in>A. keysFor (H i))
[PROOF STEP]
by (unfold keysFor_def, blast)


[STATEMENT]
lemma keysFor_mono: "G \<subseteq> H \<Longrightarrow> keysFor(G) \<subseteq> keysFor(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<subseteq> H \<Longrightarrow> keysFor G \<subseteq> keysFor H
[PROOF STEP]
by (unfold keysFor_def, blast)


[STATEMENT]
lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Agent A) H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Nonce N) H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Number N) H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Key K) H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Hash X) H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert \<lbrace>X, Y\<rbrace> H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma keysFor_insert_Crypt [simp]:
    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (Key ` E) = {}
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H
[PROOF STEP]
by (unfold keysFor_def, blast)


[STATEMENT]
lemma MPair_parts:
     "[| \<lbrace>X,Y\<rbrace> \<in> parts H;
         [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> parts H; \<lbrakk>X \<in> parts H; Y \<in> parts H\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (blast dest: parts.Fst parts.Snd)


[STATEMENT]
lemma parts_increasing: "H \<subseteq> parts(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<subseteq> parts H
[PROOF STEP]
by blast


[STATEMENT]
lemma parts_empty [simp]: "parts{} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts {} = {}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts {} \<Longrightarrow> x \<in> {}
[PROOF STEP]
apply (erule parts.induct, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_emptyE [elim!]: "X\<in> parts{} \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> parts {} \<Longrightarrow> P
[PROOF STEP]
by simp


[STATEMENT]
lemma parts_singleton: "X\<in> parts H \<Longrightarrow> \<exists>Y\<in>H. X\<in> parts {Y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> parts H \<Longrightarrow> \<exists>Y\<in>H. X \<in> parts {Y}
[PROOF STEP]
by (erule parts.induct, fast+)


[STATEMENT]
lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts G \<union> parts H \<subseteq> parts (G \<union> H)
[PROOF STEP]
by (intro Un_least parts_mono Un_upper1 Un_upper2)


[STATEMENT]
lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (G \<union> H) \<subseteq> parts G \<union> parts H
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (G \<union> H) \<Longrightarrow> x \<in> parts G \<union> parts H
[PROOF STEP]
apply (erule parts.induct, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (G \<union> H) = parts G \<union> parts H
[PROOF STEP]
by (intro equalityI parts_Un_subset1 parts_Un_subset2)


[STATEMENT]
lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert X H) = parts {X} \<union> parts H
[PROOF STEP]
by (metis insert_is_Un parts_Un)


[STATEMENT]
lemma parts_insert2:
     "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H
[PROOF STEP]
by (metis Un_commute Un_empty_right Un_insert_right insert_is_Un parts_Un)


[STATEMENT]
lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>A. parts (H x)) \<subseteq> parts (\<Union> (H ` A))
[PROOF STEP]
by (intro UN_least parts_mono UN_upper)


[STATEMENT]
lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (\<Union> (H ` A)) \<subseteq> (\<Union>x\<in>A. parts (H x))
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (\<Union> (H ` A)) \<Longrightarrow> x \<in> (\<Union>x\<in>A. parts (H x))
[PROOF STEP]
apply (erule parts.induct, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (\<Union> (H ` A)) = (\<Union>x\<in>A. parts (H x))
[PROOF STEP]
by (intro equalityI parts_UN_subset1 parts_UN_subset2)


[STATEMENT]
lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert X (parts H) \<subseteq> parts (insert X H)
[PROOF STEP]
by (blast intro: parts_mono [THEN [2] rev_subsetD])


[STATEMENT]
lemma parts_partsD [dest!]: "X \<in> parts (parts H) \<Longrightarrow> X\<in> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> parts (parts H) \<Longrightarrow> X \<in> parts H
[PROOF STEP]
by (erule parts.induct, blast+)


[STATEMENT]
lemma parts_idem [simp]: "parts (parts H) = parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (parts H) = parts H
[PROOF STEP]
by blast


[STATEMENT]
lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (parts G \<subseteq> parts H) = (G \<subseteq> parts H)
[PROOF STEP]
by (metis parts_idem parts_increasing parts_mono subset_trans)


[STATEMENT]
lemma parts_trans: "[| X \<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> parts G; G \<subseteq> parts H\<rbrakk> \<Longrightarrow> X \<in> parts H
[PROOF STEP]
by (drule parts_mono, blast)


[STATEMENT]
lemma parts_cut:
     "[| Y\<in> parts (insert X G);  X \<in> parts H |] ==> Y\<in> parts (G \<union> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Y \<in> parts (insert X G); X \<in> parts H\<rbrakk> \<Longrightarrow> Y \<in> parts (G \<union> H)
[PROOF STEP]
by (blast intro: parts_trans)


[STATEMENT]
lemma parts_cut_eq [simp]: "X \<in> parts H \<Longrightarrow> parts (insert X H) = parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> parts H \<Longrightarrow> parts (insert X H) = parts H
[PROOF STEP]
by (force dest!: parts_cut intro: parts_insertI)


[STATEMENT]
lemma parts_insert_Agent [simp]:
     "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert (Agent agt) H) = insert (Agent agt) (parts H)
[PROOF STEP]
apply (rule parts_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (insert (Agent agt) H) \<Longrightarrow> x \<in> insert (Agent agt) (parts H)
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_insert_Nonce [simp]:
     "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert (Nonce N) H) = insert (Nonce N) (parts H)
[PROOF STEP]
apply (rule parts_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (insert (Nonce N) H) \<Longrightarrow> x \<in> insert (Nonce N) (parts H)
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_insert_Number [simp]:
     "parts (insert (Number N) H) = insert (Number N) (parts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert (Number N) H) = insert (Number N) (parts H)
[PROOF STEP]
apply (rule parts_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (insert (Number N) H) \<Longrightarrow> x \<in> insert (Number N) (parts H)
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_insert_Key [simp]:
     "parts (insert (Key K) H) = insert (Key K) (parts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert (Key K) H) = insert (Key K) (parts H)
[PROOF STEP]
apply (rule parts_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (insert (Key K) H) \<Longrightarrow> x \<in> insert (Key K) (parts H)
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_insert_Hash [simp]:
     "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert (Hash X) H) = insert (Hash X) (parts H)
[PROOF STEP]
apply (rule parts_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (insert (Hash X) H) \<Longrightarrow> x \<in> insert (Hash X) (parts H)
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_insert_Crypt [simp]:
     "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. parts (insert (Crypt K X) H) \<subseteq> insert (Crypt K X) (parts (insert X H))
 2. insert (Crypt K X) (parts (insert X H)) \<subseteq> parts (insert (Crypt K X) H)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> parts (insert (Crypt K X) H) \<Longrightarrow> x \<in> insert (Crypt K X) (parts (insert X H))
 2. insert (Crypt K X) (parts (insert X H)) \<subseteq> parts (insert (Crypt K X) H)
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> parts (insert (Crypt K X) H)
[PROOF STEP]
apply (blast intro: parts.Body)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_insert_MPair [simp]:
     "parts (insert \<lbrace>X,Y\<rbrace> H) =
          insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert \<lbrace>X, Y\<rbrace> H) = insert \<lbrace>X, Y\<rbrace> (parts (insert X (insert Y H)))
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. parts (insert \<lbrace>X, Y\<rbrace> H) \<subseteq> insert \<lbrace>X, Y\<rbrace> (parts (insert X (insert Y H)))
 2. insert \<lbrace>X, Y\<rbrace> (parts (insert X (insert Y H))) \<subseteq> parts (insert \<lbrace>X, Y\<rbrace> H)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> parts (insert \<lbrace>X, Y\<rbrace> H) \<Longrightarrow> x \<in> insert \<lbrace>X, Y\<rbrace> (parts (insert X (insert Y H)))
 2. insert \<lbrace>X, Y\<rbrace> (parts (insert X (insert Y H))) \<subseteq> parts (insert \<lbrace>X, Y\<rbrace> H)
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. X \<in> parts (insert \<lbrace>X, Y\<rbrace> H)
 2. Y \<in> parts (insert \<lbrace>X, Y\<rbrace> H)
[PROOF STEP]
apply (blast intro: parts.Fst parts.Snd)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (Key ` N) = Key ` N
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> parts (Key ` N) \<Longrightarrow> x \<in> Key ` N
[PROOF STEP]
apply (erule parts.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> parts {msg}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg}
[PROOF STEP]
apply (induct msg)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {Agent x}
 2. \<And>x. \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {Number x}
 3. \<And>x. \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {Nonce x}
 4. \<And>x. \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {Key x}
 5. \<And>msg. \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg} \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {Hash msg}
 6. \<And>msg1 msg2. \<lbrakk>\<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1}; \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg2}\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {\<lbrace>msg1, msg2\<rbrace>}
 7. \<And>x1a msg. \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg} \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {Crypt x1a msg}
[PROOF STEP]
apply (simp_all (no_asm_simp) add: exI parts_insert2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>N. \<forall>n\<ge>N. n \<noteq> x
 2. \<And>msg1 msg2. \<lbrakk>\<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1}; \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg2}\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1} \<and> Nonce n \<notin> parts {msg2}
[PROOF STEP]
txt\<open>Nonce case\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>N. \<forall>n\<ge>N. n \<noteq> x
 2. \<And>msg1 msg2. \<lbrakk>\<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1}; \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg2}\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1} \<and> Nonce n \<notin> parts {msg2}
[PROOF STEP]
apply (metis Suc_n_not_le_n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>msg1 msg2. \<lbrakk>\<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1}; \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg2}\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1} \<and> Nonce n \<notin> parts {msg2}
[PROOF STEP]
txt\<open>MPair case: metis works out the necessary sum itself!\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>msg1 msg2. \<lbrakk>\<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1}; \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg2}\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. Nonce n \<notin> parts {msg1} \<and> Nonce n \<notin> parts {msg2}
[PROOF STEP]
apply (metis le_trans nat_le_linear)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_mono: "G\<subseteq>H \<Longrightarrow> analz(G) \<subseteq> analz(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<subseteq> H \<Longrightarrow> analz G \<subseteq> analz H
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>G \<subseteq> H; x \<in> analz G\<rbrakk> \<Longrightarrow> x \<in> analz H
[PROOF STEP]
apply (erule analz.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x X. \<lbrakk>G \<subseteq> H; X \<in> G\<rbrakk> \<Longrightarrow> X \<in> analz H
 2. \<And>x X Y. \<lbrakk>G \<subseteq> H; \<lbrace>X, Y\<rbrace> \<in> analz G; \<lbrace>X, Y\<rbrace> \<in> analz H\<rbrakk> \<Longrightarrow> X \<in> analz H
 3. \<And>x X Y. \<lbrakk>G \<subseteq> H; \<lbrace>X, Y\<rbrace> \<in> analz G; \<lbrace>X, Y\<rbrace> \<in> analz H\<rbrakk> \<Longrightarrow> Y \<in> analz H
 4. \<And>x K X. \<lbrakk>G \<subseteq> H; Crypt K X \<in> analz G; Crypt K X \<in> analz H; Key (invKey K) \<in> analz G; Key (invKey K) \<in> analz H\<rbrakk> \<Longrightarrow> X \<in> analz H
[PROOF STEP]
apply (auto dest: analz.Fst analz.Snd)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MPair_analz [elim!]:
     "[| \<lbrace>X,Y\<rbrace> \<in> analz H;
             [| X \<in> analz H; Y \<in> analz H |] ==> P
          |] ==> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz H; \<lbrakk>X \<in> analz H; Y \<in> analz H\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (blast dest: analz.Fst analz.Snd)


[STATEMENT]
lemma analz_increasing: "H \<subseteq> analz(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<subseteq> analz H
[PROOF STEP]
by blast


[STATEMENT]
lemma analz_subset_parts: "analz H \<subseteq> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz H \<subseteq> parts H
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz H \<Longrightarrow> x \<in> parts H
[PROOF STEP]
apply (erule analz.induct, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_analz [simp]: "parts (analz H) = parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (analz H) = parts H
[PROOF STEP]
by (metis analz_increasing analz_subset_parts equalityI parts_mono parts_subset_iff)


[STATEMENT]
lemma analz_parts [simp]: "analz (parts H) = parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (parts H) = parts H
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (parts H) \<Longrightarrow> x \<in> parts H
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_empty [simp]: "analz{} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz {} = {}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz {} \<Longrightarrow> x \<in> {}
[PROOF STEP]
apply (erule analz.induct, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz G \<union> analz H \<subseteq> analz (G \<union> H)
[PROOF STEP]
by (intro Un_least analz_mono Un_upper1 Un_upper2)


[STATEMENT]
lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert X (analz H) \<subseteq> analz (insert X H)
[PROOF STEP]
by (blast intro: analz_mono [THEN [2] rev_subsetD])


[STATEMENT]
lemma analz_insert_Agent [simp]:
     "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Agent agt) H) = insert (Agent agt) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert (Agent agt) H) \<Longrightarrow> x \<in> insert (Agent agt) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_Nonce [simp]:
     "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Nonce N) H) = insert (Nonce N) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert (Nonce N) H) \<Longrightarrow> x \<in> insert (Nonce N) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_Number [simp]:
     "analz (insert (Number N) H) = insert (Number N) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Number N) H) = insert (Number N) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert (Number N) H) \<Longrightarrow> x \<in> insert (Number N) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_Hash [simp]:
     "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Hash X) H) = insert (Hash X) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert (Hash X) H) \<Longrightarrow> x \<in> insert (Hash X) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_Key [simp]:
    "K \<notin> keysFor (analz H) \<Longrightarrow>
          analz (insert (Key K) H) = insert (Key K) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K \<notin> keysFor (analz H) \<Longrightarrow> analz (insert (Key K) H) = insert (Key K) (analz H)
[PROOF STEP]
apply (unfold keysFor_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K \<notin> invKey ` {K. \<exists>X. Crypt K X \<in> analz H} \<Longrightarrow> analz (insert (Key K) H) = insert (Key K) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>K \<notin> invKey ` {K. \<exists>X. Crypt K X \<in> analz H}; x \<in> analz (insert (Key K) H)\<rbrakk> \<Longrightarrow> x \<in> insert (Key K) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_MPair [simp]:
     "analz (insert \<lbrace>X,Y\<rbrace> H) =
          insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert \<lbrace>X, Y\<rbrace> H) = insert \<lbrace>X, Y\<rbrace> (analz (insert X (insert Y H)))
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. analz (insert \<lbrace>X, Y\<rbrace> H) \<subseteq> insert \<lbrace>X, Y\<rbrace> (analz (insert X (insert Y H)))
 2. insert \<lbrace>X, Y\<rbrace> (analz (insert X (insert Y H))) \<subseteq> analz (insert \<lbrace>X, Y\<rbrace> H)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> analz (insert \<lbrace>X, Y\<rbrace> H) \<Longrightarrow> x \<in> insert \<lbrace>X, Y\<rbrace> (analz (insert X (insert Y H)))
 2. insert \<lbrace>X, Y\<rbrace> (analz (insert X (insert Y H))) \<subseteq> analz (insert \<lbrace>X, Y\<rbrace> H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert X (insert Y H)) \<Longrightarrow> x \<in> analz (insert \<lbrace>X, Y\<rbrace> H)
[PROOF STEP]
apply (erule analz.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x Xa. Xa \<in> insert X (insert Y H) \<Longrightarrow> Xa \<in> analz (insert \<lbrace>X, Y\<rbrace> H)
 2. \<And>x Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> analz (insert X (insert Y H)); \<lbrace>Xa, Ya\<rbrace> \<in> analz (insert \<lbrace>X, Y\<rbrace> H)\<rbrakk> \<Longrightarrow> Xa \<in> analz (insert \<lbrace>X, Y\<rbrace> H)
 3. \<And>x Xa Ya. \<lbrakk>\<lbrace>Xa, Ya\<rbrace> \<in> analz (insert X (insert Y H)); \<lbrace>Xa, Ya\<rbrace> \<in> analz (insert \<lbrace>X, Y\<rbrace> H)\<rbrakk> \<Longrightarrow> Ya \<in> analz (insert \<lbrace>X, Y\<rbrace> H)
 4. \<And>x K Xa. \<lbrakk>Crypt K Xa \<in> analz (insert X (insert Y H)); Crypt K Xa \<in> analz (insert \<lbrace>X, Y\<rbrace> H); Key (invKey K) \<in> analz (insert X (insert Y H)); Key (invKey K) \<in> analz (insert \<lbrace>X, Y\<rbrace> H)\<rbrakk> \<Longrightarrow> Xa \<in> analz (insert \<lbrace>X, Y\<rbrace> H)
[PROOF STEP]
apply (blast intro: analz.Fst analz.Snd)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_Crypt:
     "Key (invKey K) \<notin> analz H
      \<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key (invKey K) \<notin> analz H \<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Key (invKey K) \<notin> analz H; x \<in> analz (insert (Crypt K X) H)\<rbrakk> \<Longrightarrow> x \<in> insert (Crypt K X) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lemma1: "Key (invKey K) \<in> analz H \<Longrightarrow>
               analz (insert (Crypt K X) H) \<subseteq>
               insert (Crypt K X) (analz (insert X H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key (invKey K) \<in> analz H \<Longrightarrow> analz (insert (Crypt K X) H) \<subseteq> insert (Crypt K X) (analz (insert X H))
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Key (invKey K) \<in> analz H; x \<in> analz (insert (Crypt K X) H)\<rbrakk> \<Longrightarrow> x \<in> insert (Crypt K X) (analz (insert X H))
[PROOF STEP]
apply (erule_tac x = x in analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lemma2: "Key (invKey K) \<in> analz H \<Longrightarrow>
               insert (Crypt K X) (analz (insert X H)) \<subseteq>
               analz (insert (Crypt K X) H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key (invKey K) \<in> analz H \<Longrightarrow> insert (Crypt K X) (analz (insert X H)) \<subseteq> analz (insert (Crypt K X) H)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Key (invKey K) \<in> analz H; x \<in> analz (insert X H)\<rbrakk> \<Longrightarrow> x \<in> analz (insert (Crypt K X) H)
[PROOF STEP]
apply (erule_tac x = x in analz.induct, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key (invKey K) \<in> analz H \<Longrightarrow> X \<in> analz (insert (Crypt K X) H)
[PROOF STEP]
apply (blast intro: analz_insertI analz.Decrypt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_Decrypt:
     "Key (invKey K) \<in> analz H \<Longrightarrow>
               analz (insert (Crypt K X) H) =
               insert (Crypt K X) (analz (insert X H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key (invKey K) \<in> analz H \<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H))
[PROOF STEP]
by (intro equalityI lemma1 lemma2)


[STATEMENT]
lemma analz_Crypt_if [simp]:
     "analz (insert (Crypt K X) H) =
          (if (Key (invKey K) \<in> analz H)
           then insert (Crypt K X) (analz (insert X H))
           else insert (Crypt K X) (analz H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Crypt K X) H) = (if Key (invKey K) \<in> analz H then insert (Crypt K X) (analz (insert X H)) else insert (Crypt K X) (analz H))
[PROOF STEP]
by (simp add: analz_insert_Crypt analz_insert_Decrypt)


[STATEMENT]
lemma analz_insert_Crypt_subset:
     "analz (insert (Crypt K X) H) \<subseteq>
           insert (Crypt K X) (analz (insert X H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Crypt K X) H) \<subseteq> insert (Crypt K X) (analz (insert X H))
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert (Crypt K X) H) \<Longrightarrow> x \<in> insert (Crypt K X) (analz (insert X H))
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (Key ` N) = Key ` N
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (Key ` N) \<Longrightarrow> x \<in> Key ` N
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_analzD [dest!]: "X\<in> analz (analz H) \<Longrightarrow> X \<in> analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> analz (analz H) \<Longrightarrow> X \<in> analz H
[PROOF STEP]
by (erule analz.induct, blast+)


[STATEMENT]
lemma analz_idem [simp]: "analz (analz H) = analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (analz H) = analz H
[PROOF STEP]
by blast


[STATEMENT]
lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (analz G \<subseteq> analz H) = (G \<subseteq> analz H)
[PROOF STEP]
by (metis analz_idem analz_increasing analz_mono subset_trans)


[STATEMENT]
lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> analz G; G \<subseteq> analz H\<rbrakk> \<Longrightarrow> X \<in> analz H
[PROOF STEP]
by (drule analz_mono, blast)


[STATEMENT]
lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Y \<in> analz (insert X H); X \<in> analz H\<rbrakk> \<Longrightarrow> Y \<in> analz H
[PROOF STEP]
by (erule analz_trans, blast)


[STATEMENT]
lemma analz_insert_eq: "X \<in> analz H \<Longrightarrow> analz (insert X H) = analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> analz H \<Longrightarrow> analz (insert X H) = analz H
[PROOF STEP]
by (blast intro: analz_cut analz_insertI)


[STATEMENT]
lemma analz_subset_cong:
     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
      ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>analz G \<subseteq> analz G'; analz H \<subseteq> analz H'\<rbrakk> \<Longrightarrow> analz (G \<union> H) \<subseteq> analz (G' \<union> H')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<subseteq> analz G'; H \<subseteq> analz H'\<rbrakk> \<Longrightarrow> G \<subseteq> analz (G' \<union> H') \<and> H \<subseteq> analz (G' \<union> H')
[PROOF STEP]
apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_cong:
     "[| analz G = analz G'; analz H = analz H' |]
      ==> analz (G \<union> H) = analz (G' \<union> H')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>analz G = analz G'; analz H = analz H'\<rbrakk> \<Longrightarrow> analz (G \<union> H) = analz (G' \<union> H')
[PROOF STEP]
by (intro equalityI analz_subset_cong, simp_all)


[STATEMENT]
lemma analz_insert_cong:
     "analz H = analz H' \<Longrightarrow> analz(insert X H) = analz(insert X H')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz H = analz H' \<Longrightarrow> analz (insert X H) = analz (insert X H')
[PROOF STEP]
by (force simp only: insert_def intro!: analz_cong)


[STATEMENT]
lemma analz_trivial:
     "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>X Y. \<lbrace>X, Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H\<rbrakk> \<Longrightarrow> analz H = H
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>X Y. \<lbrace>X, Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H; x \<in> analz H\<rbrakk> \<Longrightarrow> x \<in> H
 2. \<And>x. \<lbrakk>\<forall>X Y. \<lbrace>X, Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H; x \<in> H\<rbrakk> \<Longrightarrow> x \<in> analz H
[PROOF STEP]
apply (erule analz.induct, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_UN_analz_lemma:
     "X\<in> analz (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X\<in> analz (\<Union>i\<in>A. H i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> analz (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X \<in> analz (\<Union> (H ` A))
[PROOF STEP]
apply (erule analz.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>X. X \<in> (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X \<in> analz (\<Union> (H ` A))
 2. \<And>X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (\<Union>i\<in>A. analz (H i)); \<lbrace>X, Y\<rbrace> \<in> analz (\<Union> (H ` A))\<rbrakk> \<Longrightarrow> X \<in> analz (\<Union> (H ` A))
 3. \<And>X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (\<Union>i\<in>A. analz (H i)); \<lbrace>X, Y\<rbrace> \<in> analz (\<Union> (H ` A))\<rbrakk> \<Longrightarrow> Y \<in> analz (\<Union> (H ` A))
 4. \<And>K X. \<lbrakk>Crypt K X \<in> analz (\<Union>i\<in>A. analz (H i)); Crypt K X \<in> analz (\<Union> (H ` A)); Key (invKey K) \<in> analz (\<Union>i\<in>A. analz (H i)); Key (invKey K) \<in> analz (\<Union> (H ` A))\<rbrakk> \<Longrightarrow> X \<in> analz (\<Union> (H ` A))
[PROOF STEP]
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union> (H ` A))
[PROOF STEP]
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])


[STATEMENT]
lemma synth_mono: "G\<subseteq>H \<Longrightarrow> synth(G) \<subseteq> synth(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<subseteq> H \<Longrightarrow> synth G \<subseteq> synth H
[PROOF STEP]
by (auto, erule synth.induct, auto)


[STATEMENT]
lemma synth_increasing: "H \<subseteq> synth(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<subseteq> synth H
[PROOF STEP]
by blast


[STATEMENT]
lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. synth G \<union> synth H \<subseteq> synth (G \<union> H)
[PROOF STEP]
by (intro Un_least synth_mono Un_upper1 Un_upper2)


[STATEMENT]
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert X (synth H) \<subseteq> synth (insert X H)
[PROOF STEP]
by (blast intro: synth_mono [THEN [2] rev_subsetD])


[STATEMENT]
lemma synth_synthD [dest!]: "X \<in> synth (synth H) \<Longrightarrow> X\<in> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> synth (synth H) \<Longrightarrow> X \<in> synth H
[PROOF STEP]
by (erule synth.induct, auto)


[STATEMENT]
lemma synth_idem: "synth (synth H) = synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. synth (synth H) = synth H
[PROOF STEP]
by blast


[STATEMENT]
lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (synth G \<subseteq> synth H) = (G \<subseteq> synth H)
[PROOF STEP]
by (metis subset_trans synth_idem synth_increasing synth_mono)


[STATEMENT]
lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> synth G; G \<subseteq> synth H\<rbrakk> \<Longrightarrow> X \<in> synth H
[PROOF STEP]
by (drule synth_mono, blast)


[STATEMENT]
lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Y \<in> synth (insert X H); X \<in> synth H\<rbrakk> \<Longrightarrow> Y \<in> synth H
[PROOF STEP]
by (erule synth_trans, blast)


[STATEMENT]
lemma Agent_synth [simp]: "Agent A \<in> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Agent A \<in> synth H
[PROOF STEP]
by blast


[STATEMENT]
lemma Number_synth [simp]: "Number n \<in> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Number n \<in> synth H
[PROOF STEP]
by blast


[STATEMENT]
lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Nonce N \<in> synth H) = (Nonce N \<in> H)
[PROOF STEP]
by blast


[STATEMENT]
lemma Crypt_synth_eq [simp]:
     "Key K \<notin> H \<Longrightarrow> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key K \<notin> H \<Longrightarrow> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)
[PROOF STEP]
by blast


[STATEMENT]
lemma keysFor_synth [simp]:
    "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (synth H) = keysFor H \<union> invKey ` {K. Key K \<in> H}
[PROOF STEP]
by (unfold keysFor_def, blast)


[STATEMENT]
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (synth H) = parts H \<union> synth H
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. parts (synth H) \<subseteq> parts H \<union> synth H
 2. parts H \<union> synth H \<subseteq> parts (synth H)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> parts (synth H) \<Longrightarrow> x \<in> parts H \<union> synth H
 2. parts H \<union> synth H \<subseteq> parts (synth H)
[PROOF STEP]
apply (erule parts.induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x X. X \<in> synth H \<Longrightarrow> X \<in> parts H \<union> synth H
 2. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> parts (synth H); \<lbrace>X, Y\<rbrace> \<in> parts H \<union> synth H\<rbrakk> \<Longrightarrow> X \<in> parts H \<union> synth H
 3. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> parts (synth H); \<lbrace>X, Y\<rbrace> \<in> parts H \<union> synth H\<rbrakk> \<Longrightarrow> Y \<in> parts H \<union> synth H
 4. \<And>x K X. \<lbrakk>Crypt K X \<in> parts (synth H); Crypt K X \<in> parts H \<union> synth H\<rbrakk> \<Longrightarrow> X \<in> parts H \<union> synth H
 5. parts H \<union> synth H \<subseteq> parts (synth H)
[PROOF STEP]
apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
                    parts.Fst parts.Snd parts.Body)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (analz G \<union> H) = analz (G \<union> H)
[PROOF STEP]
apply (intro equalityI analz_subset_cong)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. analz (analz G) \<subseteq> analz G
 2. analz H \<subseteq> analz H
 3. analz G \<subseteq> analz (analz G)
 4. analz H \<subseteq> analz H
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. analz (synth G \<union> H) \<subseteq> analz (G \<union> H) \<union> synth G
 2. analz (G \<union> H) \<union> synth G \<subseteq> analz (synth G \<union> H)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> analz (synth G \<union> H) \<Longrightarrow> x \<in> analz (G \<union> H) \<union> synth G
 2. analz (G \<union> H) \<union> synth G \<subseteq> analz (synth G \<union> H)
[PROOF STEP]
apply (erule analz.induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x X. X \<in> synth G \<union> H \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
 2. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (synth G \<union> H); \<lbrace>X, Y\<rbrace> \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
 3. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (synth G \<union> H); \<lbrace>X, Y\<rbrace> \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> Y \<in> analz (G \<union> H) \<union> synth G
 4. \<And>x K X. \<lbrakk>Crypt K X \<in> analz (synth G \<union> H); Crypt K X \<in> analz (G \<union> H) \<union> synth G; Key (invKey K) \<in> analz (synth G \<union> H); Key (invKey K) \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
 5. analz (G \<union> H) \<union> synth G \<subseteq> analz (synth G \<union> H)
[PROOF STEP]
prefer 5
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. analz (G \<union> H) \<union> synth G \<subseteq> analz (synth G \<union> H)
 2. \<And>x X. X \<in> synth G \<union> H \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
 3. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (synth G \<union> H); \<lbrace>X, Y\<rbrace> \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
 4. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (synth G \<union> H); \<lbrace>X, Y\<rbrace> \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> Y \<in> analz (G \<union> H) \<union> synth G
 5. \<And>x K X. \<lbrakk>Crypt K X \<in> analz (synth G \<union> H); Crypt K X \<in> analz (G \<union> H) \<union> synth G; Key (invKey K) \<in> analz (synth G \<union> H); Key (invKey K) \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
[PROOF STEP]
apply (blast intro: analz_mono [THEN [2] rev_subsetD])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x X. X \<in> synth G \<union> H \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
 2. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (synth G \<union> H); \<lbrace>X, Y\<rbrace> \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
 3. \<And>x X Y. \<lbrakk>\<lbrace>X, Y\<rbrace> \<in> analz (synth G \<union> H); \<lbrace>X, Y\<rbrace> \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> Y \<in> analz (G \<union> H) \<union> synth G
 4. \<And>x K X. \<lbrakk>Crypt K X \<in> analz (synth G \<union> H); Crypt K X \<in> analz (G \<union> H) \<union> synth G; Key (invKey K) \<in> analz (synth G \<union> H); Key (invKey K) \<in> analz (G \<union> H) \<union> synth G\<rbrakk> \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G
[PROOF STEP]
apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (synth H) = analz H \<union> synth H
[PROOF STEP]
by (metis Un_empty_right analz_synth_Un)


[STATEMENT]
lemma parts_insert_subset_Un: "X \<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> G \<Longrightarrow> parts (insert X H) \<subseteq> parts G \<union> parts H
[PROOF STEP]
by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono)


[STATEMENT]
lemma Fake_parts_insert:
     "X \<in> synth (analz H) \<Longrightarrow>
      parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
by (metis Un_commute analz_increasing insert_subset parts_analz parts_mono
          parts_synth synth_mono synth_subset_iff)


[STATEMENT]
lemma Fake_parts_insert_in_Un:
     "[|Z \<in> parts (insert X H);  X: synth (analz H)|]
      ==> Z \<in>  synth (analz H) \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Z \<in> parts (insert X H); X \<in> synth (analz H)\<rbrakk> \<Longrightarrow> Z \<in> synth (analz H) \<union> parts H
[PROOF STEP]
by (metis Fake_parts_insert subsetD)


[STATEMENT]
lemma Fake_analz_insert:
     "X\<in> synth (analz G) \<Longrightarrow>
      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> synth (analz G) \<Longrightarrow> analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>X \<in> synth (analz G); x \<in> analz (insert X H)\<rbrakk> \<Longrightarrow> x \<in> synth (analz G) \<union> analz (G \<union> H)
[PROOF STEP]
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H)", force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>X \<in> synth (analz G); x \<in> analz (insert X H)\<rbrakk> \<Longrightarrow> x \<in> analz (synth (analz G) \<union> H)
[PROOF STEP]
apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_conj_parts [simp]:
     "(X \<in> analz H \<and> X \<in> parts H) = (X \<in> analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<in> analz H \<and> X \<in> parts H) = (X \<in> analz H)
[PROOF STEP]
by (blast intro: analz_subset_parts [THEN subsetD])


[STATEMENT]
lemma analz_disj_parts [simp]:
     "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<in> analz H \<or> X \<in> parts H) = (X \<in> parts H)
[PROOF STEP]
by (blast intro: analz_subset_parts [THEN subsetD])


[STATEMENT]
lemma MPair_synth_analz [iff]:
     "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =
      (X \<in> synth (analz H) \<and> Y \<in> synth (analz H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>X, Y\<rbrace> \<in> synth (analz H)) = (X \<in> synth (analz H) \<and> Y \<in> synth (analz H))
[PROOF STEP]
by blast


[STATEMENT]
lemma Crypt_synth_analz:
     "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]
       ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Key K \<in> analz H; Key (invKey K) \<in> analz H\<rbrakk> \<Longrightarrow> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))
[PROOF STEP]
by blast


[STATEMENT]
lemma Hash_synth_analz [simp]:
     "X \<notin> synth (analz H)
      \<Longrightarrow> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<notin> synth (analz H) \<Longrightarrow> (Hash \<lbrace>X, Y\<rbrace> \<in> synth (analz H)) = (Hash \<lbrace>X, Y\<rbrace> \<in> analz H)
[PROOF STEP]
by blast


[STATEMENT]
lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Agent A \<noteq> Hash[X] Y
[PROOF STEP]
by (unfold HPair_def, simp)


[STATEMENT]
lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nonce N \<noteq> Hash[X] Y
[PROOF STEP]
by (unfold HPair_def, simp)


[STATEMENT]
lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Number N \<noteq> Hash[X] Y
[PROOF STEP]
by (unfold HPair_def, simp)


[STATEMENT]
lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key K \<noteq> Hash[X] Y
[PROOF STEP]
by (unfold HPair_def, simp)


[STATEMENT]
lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hash Z \<noteq> Hash[X] Y
[PROOF STEP]
by (unfold HPair_def, simp)


[STATEMENT]
lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Crypt K X' \<noteq> Hash[X] Y
[PROOF STEP]
by (unfold HPair_def, simp)


[STATEMENT]
lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X \<and> Y'=Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Hash[X'] Y' = Hash[X] Y) = (X' = X \<and> Y' = Y)
[PROOF STEP]
by (simp add: HPair_def)


[STATEMENT]
lemma MPair_eq_HPair [iff]:
     "(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>X', Y'\<rbrace> = Hash[X] Y) = (X' = Hash \<lbrace>X, Y\<rbrace> \<and> Y' = Y)
[PROOF STEP]
by (simp add: HPair_def)


[STATEMENT]
lemma HPair_eq_MPair [iff]:
     "(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Hash[X] Y = \<lbrace>X', Y'\<rbrace>) = (X' = Hash \<lbrace>X, Y\<rbrace> \<and> Y' = Y)
[PROOF STEP]
by (auto simp add: HPair_def)


[STATEMENT]
lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert Hash[X] Y H) = keysFor H
[PROOF STEP]
by (simp add: HPair_def)


[STATEMENT]
lemma parts_insert_HPair [simp]:
    "parts (insert (Hash[X] Y) H) =
     insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (insert Hash[X] Y H) = insert Hash[X] Y (insert (Hash \<lbrace>X, Y\<rbrace>) (parts (insert Y H)))
[PROOF STEP]
by (simp add: HPair_def)


[STATEMENT]
lemma analz_insert_HPair [simp]:
    "analz (insert (Hash[X] Y) H) =
     insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert Hash[X] Y H) = insert Hash[X] Y (insert (Hash \<lbrace>X, Y\<rbrace>) (analz (insert Y H)))
[PROOF STEP]
by (simp add: HPair_def)


[STATEMENT]
lemma HPair_synth_analz [simp]:
     "X \<notin> synth (analz H)
    \<Longrightarrow> (Hash[X] Y \<in> synth (analz H)) =
        (Hash \<lbrace>X, Y\<rbrace> \<in> analz H \<and> Y \<in> synth (analz H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<notin> synth (analz H) \<Longrightarrow> (Hash[X] Y \<in> synth (analz H)) = (Hash \<lbrace>X, Y\<rbrace> \<in> analz H \<and> Y \<in> synth (analz H))
[PROOF STEP]
by (auto simp add: HPair_def)


[STATEMENT]
lemma parts_keyfree: "parts (keyfree) \<subseteq> keyfree"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts keyfree \<subseteq> keyfree
[PROOF STEP]
by (clarify, erule parts.induct, auto elim!: keyfree_KeyE keyfree_MPairE keyfree_CryptE)


[STATEMENT]
lemma analz_keyfree_into_Un: "\<lbrakk>X \<in> analz (G \<union> H); G \<subseteq> keyfree\<rbrakk> \<Longrightarrow> X \<in> parts G \<union> analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> analz (G \<union> H); G \<subseteq> keyfree\<rbrakk> \<Longrightarrow> X \<in> parts G \<union> analz H
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>K X. \<lbrakk>G \<subseteq> keyfree; Crypt K X \<in> analz (G \<union> H); Key (invKey K) \<in> analz (G \<union> H); X \<notin> analz H; Crypt K X \<in> parts G; Key (invKey K) \<in> parts G\<rbrakk> \<Longrightarrow> X \<in> parts G
 2. \<And>K X. \<lbrakk>G \<subseteq> keyfree; Crypt K X \<in> analz (G \<union> H); Key (invKey K) \<in> analz (G \<union> H); X \<notin> analz H; Crypt K X \<in> parts G; Key (invKey K) \<in> analz H\<rbrakk> \<Longrightarrow> X \<in> parts G
 3. \<And>K X. \<lbrakk>G \<subseteq> keyfree; Crypt K X \<in> analz (G \<union> H); Key (invKey K) \<in> analz (G \<union> H); X \<notin> analz H; Crypt K X \<in> analz H; Key (invKey K) \<in> parts G\<rbrakk> \<Longrightarrow> X \<in> parts G
[PROOF STEP]
apply (blast dest:parts.Body)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>K X. \<lbrakk>G \<subseteq> keyfree; Crypt K X \<in> analz (G \<union> H); Key (invKey K) \<in> analz (G \<union> H); X \<notin> analz H; Crypt K X \<in> parts G; Key (invKey K) \<in> analz H\<rbrakk> \<Longrightarrow> X \<in> parts G
 2. \<And>K X. \<lbrakk>G \<subseteq> keyfree; Crypt K X \<in> analz (G \<union> H); Key (invKey K) \<in> analz (G \<union> H); X \<notin> analz H; Crypt K X \<in> analz H; Key (invKey K) \<in> parts G\<rbrakk> \<Longrightarrow> X \<in> parts G
[PROOF STEP]
apply (blast dest: parts.Body)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>K X. \<lbrakk>G \<subseteq> keyfree; Crypt K X \<in> analz (G \<union> H); Key (invKey K) \<in> analz (G \<union> H); X \<notin> analz H; Crypt K X \<in> analz H; Key (invKey K) \<in> parts G\<rbrakk> \<Longrightarrow> X \<in> parts G
[PROOF STEP]
apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Crypt K X \<notin> Key ` A
[PROOF STEP]
by auto


[STATEMENT]
lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hash X \<notin> Key ` A
[PROOF STEP]
by auto


[STATEMENT]
lemma synth_analz_mono: "G\<subseteq>H \<Longrightarrow> synth (analz(G)) \<subseteq> synth (analz(H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<subseteq> H \<Longrightarrow> synth (analz G) \<subseteq> synth (analz H)
[PROOF STEP]
by (iprover intro: synth_mono analz_mono)


[STATEMENT]
lemma Fake_analz_eq [simp]:
     "X \<in> synth(analz H) \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)
[PROOF STEP]
by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute
          subset_insertI synth_analz_mono synth_increasing synth_subset_iff)


[STATEMENT]
lemma gen_analz_insert_eq [rule_format]:
     "X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> analz (insert X G) = analz G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> analz (insert X G) = analz G
[PROOF STEP]
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])


[STATEMENT]
lemma Fake_parts_sing:
     "X \<in> synth (analz H) \<Longrightarrow> parts{X} \<subseteq> synth (analz H) \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts {X} \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
by (metis Fake_parts_insert empty_subsetI insert_mono parts_mono subset_trans)


[STATEMENT]
lemma le_enn2realI: "\<lbrakk> ennreal x \<le> y; y = \<top> \<Longrightarrow> x \<le> 0 \<rbrakk> \<Longrightarrow> x \<le> enn2real y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ennreal x \<le> y; y = \<top> \<Longrightarrow> x \<le> 0\<rbrakk> \<Longrightarrow> x \<le> enn2real y
[PROOF STEP]
by(cases y) simp_all


[STATEMENT]
lemma enn2real_leD: "\<lbrakk> enn2real x < y; x \<noteq> \<top> \<rbrakk> \<Longrightarrow> x < ennreal y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enn2real x < y; x \<noteq> \<top>\<rbrakk> \<Longrightarrow> x < ennreal y
[PROOF STEP]
by(cases x)(simp_all add: ennreal_lessI)


[STATEMENT]
lemma ennreal_mult_le_self2I: "\<lbrakk> y > 0 \<Longrightarrow> x \<le> 1 \<rbrakk> \<Longrightarrow> x * y \<le> y" for x y :: ennreal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < y \<Longrightarrow> x \<le> 1) \<Longrightarrow> x * y \<le> y
[PROOF STEP]
apply(cases x; cases y)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>r ra. \<lbrakk>0 < y \<Longrightarrow> x \<le> 1; 0 \<le> r; x = ennreal r; 0 \<le> ra; y = ennreal ra\<rbrakk> \<Longrightarrow> x * y \<le> y
 2. \<And>r. \<lbrakk>0 < y \<Longrightarrow> x \<le> 1; 0 \<le> r; x = ennreal r; y = \<top>\<rbrakk> \<Longrightarrow> x * y \<le> y
 3. \<And>r. \<lbrakk>0 < y \<Longrightarrow> x \<le> 1; x = \<top>; 0 \<le> r; y = ennreal r\<rbrakk> \<Longrightarrow> x * y \<le> y
 4. \<lbrakk>0 < y \<Longrightarrow> x \<le> 1; x = \<top>; y = \<top>\<rbrakk> \<Longrightarrow> x * y \<le> y
[PROOF STEP]
apply(auto simp add: top_unique ennreal_top_mult ennreal_mult[symmetric] intro: ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>0 < ra \<Longrightarrow> r \<le> 1; 0 \<le> r; x = ennreal r; 0 \<le> ra; y = ennreal ra\<rbrakk> \<Longrightarrow> r * ra \<le> ra
[PROOF STEP]
using mult_left_le_one_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::?'a) \<le> ?x; (0::?'a) \<le> ?y; ?y \<le> (1::?'a)\<rbrakk> \<Longrightarrow> ?y * ?x \<le> ?x

goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>0 < ra \<Longrightarrow> r \<le> 1; 0 \<le> r; x = ennreal r; 0 \<le> ra; y = ennreal ra\<rbrakk> \<Longrightarrow> r * ra \<le> ra
[PROOF STEP]
by force


[STATEMENT]
lemma ennreal_leI: "x \<le> enn2real y \<Longrightarrow> ennreal x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> enn2real y \<Longrightarrow> ennreal x \<le> y
[PROOF STEP]
by(cases y) simp_all


[STATEMENT]
lemma enn2real_INF: "\<lbrakk> A \<noteq> {}; \<forall>x\<in>A. f x < \<top> \<rbrakk> \<Longrightarrow> enn2real (INF x\<in>A. f x) = (INF x\<in>A. enn2real (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> enn2real (\<Sqinter> (f ` A)) = (\<Sqinter>x\<in>A. enn2real (f x))
[PROOF STEP]
apply(rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> enn2real (\<Sqinter> (f ` A)) \<le> (\<Sqinter>x\<in>A. enn2real (f x))
 2. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> enn2real (\<Sqinter> (f ` A))
[PROOF STEP]
apply(rule cINF_greatest)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> A \<noteq> {}
 2. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> enn2real (\<Sqinter> (f ` A)) \<le> enn2real (f x)
 3. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> enn2real (\<Sqinter> (f ` A))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> enn2real (\<Sqinter> (f ` A)) \<le> enn2real (f x)
 2. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> enn2real (\<Sqinter> (f ` A))
[PROOF STEP]
apply(rule enn2real_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> \<Sqinter> (f ` A) \<le> f x
 2. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> f x < \<top>
 3. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> enn2real (\<Sqinter> (f ` A))
[PROOF STEP]
apply(erule INF_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> f x < \<top>
 2. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> enn2real (\<Sqinter> (f ` A))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> enn2real (\<Sqinter> (f ` A))
[PROOF STEP]
apply(rule le_enn2realI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> ennreal (\<Sqinter>x\<in>A. enn2real (f x)) \<le> \<Sqinter> (f ` A)
 2. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; \<Sqinter> (f ` A) = \<top>\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> 0
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>\<rbrakk> \<Longrightarrow> ennreal (\<Sqinter>x\<in>A. enn2real (f x)) \<le> \<Sqinter> (f ` A)
[PROOF STEP]
apply(rule INF_greatest)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> ennreal (\<Sqinter>x\<in>A. enn2real (f x)) \<le> f x
[PROOF STEP]
apply(rule ennreal_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> (\<Sqinter>x\<in>A. enn2real (f x)) \<le> enn2real (f x)
[PROOF STEP]
apply(rule cINF_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> bdd_below ((\<lambda>x. enn2real (f x)) ` A)
 2. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
apply(rule bdd_belowI[where m=0])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A; xa \<in> (\<lambda>x. enn2real (f x)) ` A\<rbrakk> \<Longrightarrow> 0 \<le> xa
 2. \<And>x. \<lbrakk>A \<noteq> {}; \<forall>x\<in>A. f x < \<top>; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma monotone_times_ennreal1: "monotone (\<le>) (\<le>) (\<lambda>x. x * y :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>x. x * y)
[PROOF STEP]
by(auto intro!: monotoneI mult_right_mono)


[STATEMENT]
lemma monotone_times_ennreal2: "monotone (\<le>) (\<le>) (\<lambda>x. y * x :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono ((*) y)
[PROOF STEP]
by(auto intro!: monotoneI mult_left_mono)


[STATEMENT]
lemma mono2mono_times_ennreal[THEN lfp.mono2mono2, cont_intro, simp]:
  shows monotone_times_ennreal: "monotone (rel_prod (\<le>) (\<le>)) (\<le>) (\<lambda>(x, y). x * y :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (rel_prod (\<le>) (\<le>)) (\<le>) (\<lambda>(x, y). x * y)
[PROOF STEP]
by(simp add: monotone_times_ennreal1 monotone_times_ennreal2)


[STATEMENT]
lemma mcont_times_ennreal1: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. x * y :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcont Sup (\<le>) Sup (\<le>) ((*) x)
[PROOF STEP]
by(auto intro!: mcontI contI simp add: SUP_mult_left_ennreal[symmetric])


[STATEMENT]
lemma mcont_times_ennreal2: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. y * x :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. y * x)
[PROOF STEP]
by(subst mult.commute)(rule mcont_times_ennreal1)


[STATEMENT]
lemma mcont2mcont_times_ennreal [cont_intro, simp]:
  "\<lbrakk> mcont lub ord Sup (\<le>) (\<lambda>x. f x);
    mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
  \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x * g x :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mcont lub ord Sup (\<le>) f; mcont lub ord Sup (\<le>) g\<rbrakk> \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x * g x)
[PROOF STEP]
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_times_ennreal1 mcont_times_ennreal2 ccpo.mcont_const[OF complete_lattice_ccpo])


[STATEMENT]
lemma ereal_INF_cmult: "0 < c \<Longrightarrow> (INF i\<in>I. c * f i) = ereal c * (INF i\<in>I. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (\<Sqinter>i\<in>I. ereal c * f i) = ereal c * \<Sqinter> (f ` I)
[PROOF STEP]
using ereal_Inf_cmult[where P="\<lambda>x. \<exists>i\<in>I. x = f i", of c]
[PROOF STATE]
proof (prove)
using this:
0 < c \<Longrightarrow> \<Sqinter> {ereal c * x |x. \<exists>i\<in>I. x = f i} = ereal c * \<Sqinter> {x. \<exists>i\<in>I. x = f i}

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (\<Sqinter>i\<in>I. ereal c * f i) = ereal c * \<Sqinter> (f ` I)
[PROOF STEP]
by(rule box_equals)(auto intro!: arg_cong[where f="Inf"] arg_cong2[where f="(*)"])


[STATEMENT]
lemma ereal_INF_multc: "0 < c \<Longrightarrow> (INF i\<in>I. f i * c) = (INF i\<in>I. f i) * ereal c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (\<Sqinter>i\<in>I. f i * ereal c) = \<Sqinter> (f ` I) * ereal c
[PROOF STEP]
using ereal_INF_cmult[of c f I]
[PROOF STATE]
proof (prove)
using this:
0 < c \<Longrightarrow> (\<Sqinter>i\<in>I. ereal c * f i) = ereal c * \<Sqinter> (f ` I)

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (\<Sqinter>i\<in>I. f i * ereal c) = \<Sqinter> (f ` I) * ereal c
[PROOF STEP]
by(simp add: mult.commute)


[STATEMENT]
lemma INF_mult_left_ennreal:
  assumes "I = {} \<Longrightarrow> c \<noteq> 0"
  and "\<lbrakk> c = \<top>; \<exists>i\<in>I. f i > 0 \<rbrakk> \<Longrightarrow> \<exists>p>0. \<forall>i\<in>I. f i \<ge> p"
  shows "c * (INF i\<in>I. f i) = (INF i\<in>I. c * f i ::ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
consider (empty) "I = {}" | (top) "c = \<top>" | (zero) "c = 0" | (normal) "I \<noteq> {}" "c \<noteq> \<top>" "c \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I = {} \<Longrightarrow> thesis; c = \<top> \<Longrightarrow> thesis; c = 0 \<Longrightarrow> thesis; \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>I = {} \<Longrightarrow> ?thesis; c = \<top> \<Longrightarrow> ?thesis; c = 0 \<Longrightarrow> ?thesis; \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>I = {} \<Longrightarrow> ?thesis; c = \<top> \<Longrightarrow> ?thesis; c = 0 \<Longrightarrow> ?thesis; \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>I = {} \<Longrightarrow> ?thesis; c = \<top> \<Longrightarrow> ?thesis; c = 0 \<Longrightarrow> ?thesis; \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. I = {} \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. c = \<top> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 3. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 4. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
I = {}

goal (4 subgoals):
 1. I = {} \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. c = \<top> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 3. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 4. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I = {}

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
by(simp add: ennreal_mult_top assms(1))
[PROOF STATE]
proof (state)
this:
c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)

goal (3 subgoals):
 1. c = \<top> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 3. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. c = \<top> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 3. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
case top
[PROOF STATE]
proof (state)
this:
c = \<top>

goal (3 subgoals):
 1. c = \<top> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 3. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
proof(cases "\<exists>i\<in>I. f i > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>i\<in>I. 0 < f i \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>I. 0 < f i

goal (2 subgoals):
 1. \<exists>i\<in>I. 0 < f i \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
with assms(2) top
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>c = \<top>; \<exists>i\<in>I. 0 < f i\<rbrakk> \<Longrightarrow> \<exists>p>0. \<forall>i\<in>I. p \<le> f i
c = \<top>
\<exists>i\<in>I. 0 < f i
[PROOF STEP]
obtain p where "p > 0" and p: "\<And>i. i \<in> I \<Longrightarrow> f i \<ge> p"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c = \<top>; \<exists>i\<in>I. 0 < f i\<rbrakk> \<Longrightarrow> \<exists>p>0. \<forall>i\<in>I. p \<le> f i
c = \<top>
\<exists>i\<in>I. 0 < f i

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>0 < p; \<And>i. i \<in> I \<Longrightarrow> p \<le> f i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < p
?i \<in> I \<Longrightarrow> p \<le> f ?i

goal (2 subgoals):
 1. \<exists>i\<in>I. 0 < f i \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < p
?i \<in> I \<Longrightarrow> p \<le> f ?i
[PROOF STEP]
have *: "\<And>i. i \<in> I \<Longrightarrow> f i > 0"
[PROOF STATE]
proof (prove)
using this:
0 < p
?i \<in> I \<Longrightarrow> p \<le> f ?i

goal (1 subgoal):
 1. \<And>i. i \<in> I \<Longrightarrow> 0 < f i
[PROOF STEP]
by(auto intro: less_le_trans)
[PROOF STATE]
proof (state)
this:
?i \<in> I \<Longrightarrow> 0 < f ?i

goal (2 subgoals):
 1. \<exists>i\<in>I. 0 < f i \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
note \<open>0 < p\<close>
[PROOF STATE]
proof (state)
this:
0 < p

goal (2 subgoals):
 1. \<exists>i\<in>I. 0 < f i \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 < p

goal (2 subgoals):
 1. \<exists>i\<in>I. 0 < f i \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
?i \<in> I \<Longrightarrow> p \<le> f ?i
[PROOF STEP]
have "p \<le> (INF i\<in>I. f i)"
[PROOF STATE]
proof (prove)
using this:
?i \<in> I \<Longrightarrow> p \<le> f ?i

goal (1 subgoal):
 1. p \<le> \<Sqinter> (f ` I)
[PROOF STEP]
by(rule INF_greatest)
[PROOF STATE]
proof (state)
this:
p \<le> \<Sqinter> (f ` I)

goal (2 subgoals):
 1. \<exists>i\<in>I. 0 < f i \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < \<Sqinter> (f ` I)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < \<Sqinter> (f ` I)

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
using top
[PROOF STATE]
proof (prove)
using this:
0 < \<Sqinter> (f ` I)
c = \<top>

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
by(auto simp add: ennreal_top_mult dest: *)
[PROOF STATE]
proof (state)
this:
c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<in>I. 0 < f i)

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
hence "f i = 0" if "i \<in> I" for i
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<in>I. 0 < f i)

goal (1 subgoal):
 1. f i = 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<in>I. 0 < f i)
i \<in> I

goal (1 subgoal):
 1. f i = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in> I \<Longrightarrow> f ?i = 0

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>I. 0 < f i) \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?i \<in> I \<Longrightarrow> f ?i = 0

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
using top
[PROOF STATE]
proof (prove)
using this:
?i \<in> I \<Longrightarrow> f ?i = 0
c = \<top>

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
by(simp add: INF_constant ennreal_mult_top)
[PROOF STATE]
proof (state)
this:
c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
 2. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
c = 0
I = {} \<Longrightarrow> c \<noteq> 0

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
by(auto simp add: INF_constant)
[PROOF STATE]
proof (state)
this:
c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
case normal
[PROOF STATE]
proof (state)
this:
I \<noteq> {}
c \<noteq> \<top>
c \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; c \<noteq> \<top>; c \<noteq> 0\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I \<noteq> {}
c \<noteq> \<top>
c \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I \<noteq> {}
c \<noteq> \<top>
c \<noteq> 0

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
including ennreal.lifting
[PROOF STATE]
proof (prove)
using this:
I \<noteq> {}
c \<noteq> \<top>
c \<noteq> 0

goal (1 subgoal):
 1. c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I c f. \<lbrakk>I \<noteq> {}; 0 \<le> c; c \<noteq> \<top>; c \<noteq> 0; pred_fun \<top> ((\<le>) 0) f\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
subgoal for I c f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; 0 \<le> c; c \<noteq> \<top>; c \<noteq> 0; pred_fun \<top> ((\<le>) 0) f\<rbrakk> \<Longrightarrow> c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)
[PROOF STEP]
by(cases c)(simp_all add: top_ereal_def ereal_INF_cmult)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c * \<Sqinter> (f ` I) = (\<Sqinter>i\<in>I. c * f i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_map_spmf_None: "pmf (map_spmf f p) None = pmf p None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (map_spmf f p) None = pmf p None
[PROOF STEP]
by(simp add: pmf_None_eq_weight_spmf)


[STATEMENT]
lemma nn_integral_try_spmf:
  "nn_integral (measure_spmf (try_spmf p q)) f = nn_integral (measure_spmf p) f + nn_integral (measure_spmf q) f * pmf p None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf (TRY p ELSE q)) f = integral\<^sup>N (measure_spmf p) f + integral\<^sup>N (measure_spmf q) f * ennreal (pmf p None)
[PROOF STEP]
by(simp add: nn_integral_measure_spmf spmf_try_spmf distrib_right nn_integral_add ennreal_mult mult.assoc nn_integral_cmult)
  (simp add: mult.commute)


[STATEMENT]
lemma INF_UNION: "(INF z \<in> \<Union>x\<in>A. B x. f z) = (INF x\<in>A. INF z\<in>B x. f z)" for f :: "_ \<Rightarrow> 'b::complete_lattice"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (f ` \<Union> (B ` A)) = (\<Sqinter>x\<in>A. \<Sqinter> (f ` B x))
[PROOF STEP]
by(auto intro!: antisym INF_greatest intro: INF_lower2)


[STATEMENT]
lemma nn_integral_spmf_parametric [transfer_rule]:
  includes lifting_syntax
  shows "(rel_spmf A ===> (A ===> (=)) ===> (=)) nn_integral_spmf nn_integral_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_spmf A ===> (A ===> (=)) ===> (=)) nn_integral_spmf nn_integral_spmf
[PROOF STEP]
unfolding nn_integral_spmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_spmf A ===> (A ===> (=)) ===> (=)) (\<lambda>p. integral\<^sup>N (measure_spmf p)) (\<lambda>p. integral\<^sup>N (measure_spmf p))
[PROOF STEP]
proof(rule rel_funI)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>rel_spmf A x y; (A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf x) xa = integral\<^sup>N (measure_spmf y) ya
[PROOF STEP]
fix p q and f g :: "_ \<Rightarrow> ennreal"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>rel_spmf A x y; (A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf x) xa = integral\<^sup>N (measure_spmf y) ya
[PROOF STEP]
assume pq: "rel_spmf A p q" and fg: "(A ===> (=)) f g"
[PROOF STATE]
proof (state)
this:
rel_spmf A p q
(A ===> (=)) f g

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>rel_spmf A x y; (A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf x) xa = integral\<^sup>N (measure_spmf y) ya
[PROOF STEP]
from pq
[PROOF STATE]
proof (chain)
picking this:
rel_spmf A p q
[PROOF STEP]
obtain pq where pq [rule_format]: "\<forall>(x, y)\<in>set_spmf pq. A x y"
    and p: "p = map_spmf fst pq" and q: "q = map_spmf snd pq"
[PROOF STATE]
proof (prove)
using this:
rel_spmf A p q

goal (1 subgoal):
 1. (\<And>pq. \<lbrakk>\<forall>(x, y)\<in>set_spmf pq. A x y; p = map_spmf fst pq; q = map_spmf snd pq\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases rule: rel_spmfE) auto
[PROOF STATE]
proof (state)
this:
?x \<in> set_spmf pq \<Longrightarrow> case ?x of (x, xa) \<Rightarrow> A x xa
p = map_spmf fst pq
q = map_spmf snd pq

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>rel_spmf A x y; (A ===> (=)) xa ya\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf x) xa = integral\<^sup>N (measure_spmf y) ya
[PROOF STEP]
show "nn_integral (measure_spmf p) f = nn_integral (measure_spmf q) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf p) f = integral\<^sup>N (measure_spmf q) g
[PROOF STEP]
by(simp add: p q)(auto simp add: nn_integral_measure_spmf spmf_eq_0_set_spmf dest!: pq rel_funD[OF fg] intro: ennreal_mult_left_cong intro!: nn_integral_cong)
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf p) f = integral\<^sup>N (measure_spmf q) g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weight_spmf_mcont2mcont [THEN lfp.mcont2mcont, cont_intro]:
  shows weight_spmf_mcont: "mcont (lub_spmf) (ord_spmf (=)) Sup (\<le>) (\<lambda>p. ennreal (weight_spmf p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p. ennreal (weight_spmf p))
[PROOF STEP]
apply(simp add: mcont_def cont_def weight_spmf_def measure_spmf.emeasure_eq_measure[symmetric] emeasure_lub_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (ord_spmf (=)) (\<le>) (\<lambda>p. emeasure (measure_spmf p) UNIV)
[PROOF STEP]
apply(rule call_mono[THEN lfp.mono2mono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (ord_spmf (=)) lfp.le_fun (\<lambda>p. emeasure (measure_spmf p))
[PROOF STEP]
apply(unfold fun_ord_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (ord_spmf (=)) (\<lambda>f g. \<forall>x. f x \<le> g x) (\<lambda>p. emeasure (measure_spmf p))
[PROOF STEP]
apply(rule monotone_emeasure_spmf[unfolded le_fun_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mono2mono_nn_integral_spmf [THEN lfp.mono2mono, cont_intro]:
  shows monotone_nn_integral_spmf: "monotone (ord_spmf (=)) (\<le>) (\<lambda>p. integral\<^sup>N (measure_spmf p) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (ord_spmf (=)) (\<le>) (\<lambda>p. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
by(rule monotoneI)(auto simp add: nn_integral_measure_spmf intro!: nn_integral_mono mult_right_mono dest: monotone_spmf[THEN monotoneD])


[STATEMENT]
lemma cont_nn_integral_spmf:
  "cont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p :: 'a spmf. nn_integral (measure_spmf p) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
fix Y :: "'a spmf set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
assume Y: "Complete_Partial_Order.chain (ord_spmf (=)) Y" "Y \<noteq> {}"
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (ord_spmf (=)) Y
Y \<noteq> {}

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
let ?M = "count_space (set_spmf (lub_spmf Y))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
have "nn_integral (measure_spmf (lub_spmf Y)) f = \<integral>\<^sup>+ x. ennreal (spmf (lub_spmf Y) x) * f x \<partial>?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf (lub_spmf Y) x) * f x)
[PROOF STEP]
by(simp add: nn_integral_measure_spmf')
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf (lub_spmf Y) x) * f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf (lub_spmf Y) x) * f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
have "\<dots> = \<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x) * f x) \<partial>?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf (lub_spmf Y) x) * f x) = (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). \<Squnion>p\<in>Y. ennreal (spmf p x) * f x)
[PROOF STEP]
by(simp add: spmf_lub_spmf Y ennreal_SUP[OF SUP_spmf_neq_top'] SUP_mult_right_ennreal)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf (lub_spmf Y) x) * f x) = (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). \<Squnion>p\<in>Y. ennreal (spmf p x) * f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf (lub_spmf Y) x) * f x) = (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). \<Squnion>p\<in>Y. ennreal (spmf p x) * f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf p x) * f x \<partial>?M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). \<Squnion>p\<in>Y. ennreal (spmf p x) * f x) = (\<Squnion>p\<in>Y. \<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf p x) * f x)
[PROOF STEP]
proof(rule nn_integral_monotone_convergence_SUP_countable)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Y \<noteq> {}
 2. Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * f x) ` Y)
 3. countable (set_spmf (lub_spmf Y))
[PROOF STEP]
show "Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * f x) ` Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * f x) ` Y)
[PROOF STEP]
using Y(1)
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (ord_spmf (=)) Y

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * f x) ` Y)
[PROOF STEP]
by(rule chain_imageI)(auto simp add: le_fun_def intro!: mult_right_mono dest: monotone_spmf[THEN monotoneD])
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * f x) ` Y)

goal (2 subgoals):
 1. Y \<noteq> {}
 2. countable (set_spmf (lub_spmf Y))
[PROOF STEP]
qed(simp_all add: Y(2))
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). \<Squnion>p\<in>Y. ennreal (spmf p x) * f x) = (\<Squnion>p\<in>Y. \<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf p x) * f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). \<Squnion>p\<in>Y. ennreal (spmf p x) * f x) = (\<Squnion>p\<in>Y. \<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf p x) * f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
have "\<dots> = (SUP p\<in>Y. nn_integral (measure_spmf p) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>p\<in>Y. \<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf p x) * f x) = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
by(auto simp add: nn_integral_measure_spmf Y nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: SUP_cong nn_integral_cong)
[PROOF STATE]
proof (state)
this:
(\<Squnion>p\<in>Y. \<Sum>\<^sup>+ x\<in>set_spmf (lub_spmf Y). ennreal (spmf p x) * f x) = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (ord_spmf (=)) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
show "nn_integral (measure_spmf (lub_spmf Y)) f = (SUP p\<in>Y. nn_integral (measure_spmf p) f)"
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)

goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf (lub_spmf Y)) f = (\<Squnion>p\<in>Y. integral\<^sup>N (measure_spmf p) f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mcont2mcont_nn_integral_spmf [THEN lfp.mcont2mcont, cont_intro]:
  shows mcont_nn_integral_spmf:
  "mcont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p :: 'a spmf. nn_integral (measure_spmf p) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p. integral\<^sup>N (measure_spmf p) f)
[PROOF STEP]
by(rule mcontI)(simp_all add: cont_nn_integral_spmf)


[STATEMENT]
lemma nn_integral_mono2mono:
  assumes "\<And>x. x \<in> space M \<Longrightarrow> monotone ord (\<le>) (\<lambda>f. F f x)"
  shows "monotone ord (\<le>) (\<lambda>f. nn_integral M (F f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone ord (\<le>) (\<lambda>f. integral\<^sup>N M (F f))
[PROOF STEP]
by(rule monotoneI nn_integral_mono monotoneD[OF assms])+


[STATEMENT]
lemma nn_integral_mono_lfp [partial_function_mono]:
  \<comment> \<open>@{ML Partial_Function.mono_tac} does not like conditional assumptions (more precisely the case splitter)\<close>
  "(\<And>x. lfp.mono_body (\<lambda>f. F f x)) \<Longrightarrow> lfp.mono_body (\<lambda>f. nn_integral M (F f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. monotone lfp.le_fun (\<le>) (\<lambda>f. F f x)) \<Longrightarrow> monotone lfp.le_fun (\<le>) (\<lambda>f. integral\<^sup>N M (F f))
[PROOF STEP]
by(rule nn_integral_mono2mono)