[STATEMENT]
theorem fundamental_property_of_path_slicing:
  assumes "n -as\<rightarrow>* n'" and "preds (kinds as) s"
  shows "(\<forall>V \<in> Use n'. state_val (transfers (slice_kinds as) s) V =
                         state_val (transfers (kinds as) s) V)"
  and "preds (slice_kinds as) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V &&& preds (slice_kinds as) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
 2. preds (slice_kinds as) s
[PROOF STEP]
have "length as = length (slice_path as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length as = length (slice_path as)
[PROOF STEP]
by(simp add:slice_path_length)
[PROOF STATE]
proof (state)
this:
length as = length (slice_path as)

goal (2 subgoals):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
 2. preds (slice_kinds as) s
[PROOF STEP]
hence "slice_path as \<preceq>\<^sub>b replicate (length as) True"
[PROOF STATE]
proof (prove)
using this:
length as = length (slice_path as)

goal (1 subgoal):
 1. slice_path as \<preceq>\<^sub>b replicate (length as) True
[PROOF STEP]
by(simp add:maximal_element)
[PROOF STATE]
proof (state)
this:
slice_path as \<preceq>\<^sub>b replicate (length as) True

goal (2 subgoals):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
 2. preds (slice_kinds as) s
[PROOF STEP]
have "select_edge_kinds as (replicate (length as) True) = kinds as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_edge_kinds as (replicate (length as) True) = kinds as
[PROOF STEP]
by(rule select_edge_kinds_max_bv)
[PROOF STATE]
proof (state)
this:
select_edge_kinds as (replicate (length as) True) = kinds as

goal (2 subgoals):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
 2. preds (slice_kinds as) s
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close> \<open>slice_path as \<preceq>\<^sub>b replicate (length as) True\<close>
    \<open>preds (kinds as) s\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
slice_path as \<preceq>\<^sub>b replicate (length as) True
preds (kinds as) s
select_edge_kinds as (replicate (length as) True) = kinds as
[PROOF STEP]
have "(\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V =
       state_val (transfers (kinds as) s) V) \<and> preds (slice_kinds as) s"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
slice_path as \<preceq>\<^sub>b replicate (length as) True
preds (kinds as) s
select_edge_kinds as (replicate (length as) True) = kinds as

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V) \<and> preds (slice_kinds as) s
[PROOF STEP]
by -(rule slice_path_leqs_information_same_Uses,simp_all add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V) \<and> preds (slice_kinds as) s

goal (2 subgoals):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
 2. preds (slice_kinds as) s
[PROOF STEP]
thus "\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V =
    state_val (transfers (kinds as) s) V" and "preds (slice_kinds as) s"
[PROOF STATE]
proof (prove)
using this:
(\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V) \<and> preds (slice_kinds as) s

goal (1 subgoal):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V &&& preds (slice_kinds as) s
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
preds (slice_kinds as) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem fundamental_property_of_path_slicing_semantically:
  assumes "n \<triangleq> c" and "\<langle>c,s\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>"
  obtains n' as where "n -as\<rightarrow>* n'" and "preds (slice_kinds as) s"
  and "n' \<triangleq> c'"
  and "\<forall>V \<in> Use n'. state_val (transfers (slice_kinds as) s) V =
                     state_val s' V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as n'. \<lbrakk>n -as\<rightarrow>* n'; preds (slice_kinds as) s; n' \<triangleq> c'; \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as n'. n -as\<rightarrow>* n' \<and> preds (slice_kinds as) s \<and> n' \<triangleq> c' \<and> (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)
[PROOF STEP]
from \<open>n \<triangleq> c\<close> \<open>\<langle>c,s\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<triangleq> c
\<langle>c,s\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>
[PROOF STEP]
obtain n' as where "n -as\<rightarrow>* n'"
    and "transfers (kinds as) s = s'"
    and "preds (kinds as) s"
    and "n' \<triangleq> c'"
[PROOF STATE]
proof (prove)
using this:
n \<triangleq> c
\<langle>c,s\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>

goal (1 subgoal):
 1. (\<And>as n'. \<lbrakk>n -as\<rightarrow>* n'; transfers (kinds as) s = s'; preds (kinds as) s; n' \<triangleq> c'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:fundamental_property)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n'
transfers (kinds as) s = s'
preds (kinds as) s
n' \<triangleq> c'

goal (1 subgoal):
 1. \<exists>as n'. n -as\<rightarrow>* n' \<and> preds (slice_kinds as) s \<and> n' \<triangleq> c' \<and> (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close> \<open>preds (kinds as) s\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
preds (kinds as) s
n -as\<rightarrow>* n'
transfers (kinds as) s = s'
preds (kinds as) s
n' \<triangleq> c'
[PROOF STEP]
have "\<forall>V \<in> Use n'. state_val (transfers (slice_kinds as) s) V =
    state_val (transfers (kinds as) s) V" and "preds (slice_kinds as) s"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
preds (kinds as) s
n -as\<rightarrow>* n'
transfers (kinds as) s = s'
preds (kinds as) s
n' \<triangleq> c'

goal (1 subgoal):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V &&& preds (slice_kinds as) s
[PROOF STEP]
by -(rule fundamental_property_of_path_slicing,simp_all)+
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
preds (slice_kinds as) s

goal (1 subgoal):
 1. \<exists>as n'. n -as\<rightarrow>* n' \<and> preds (slice_kinds as) s \<and> n' \<triangleq> c' \<and> (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)
[PROOF STEP]
with \<open>transfers (kinds as) s = s'\<close>
[PROOF STATE]
proof (chain)
picking this:
transfers (kinds as) s = s'
\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
preds (slice_kinds as) s
[PROOF STEP]
have "\<forall>V \<in> Use n'.
    state_val (transfers (slice_kinds as) s) V =
    state_val s' V"
[PROOF STATE]
proof (prove)
using this:
transfers (kinds as) s = s'
\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val (transfers (kinds as) s) V
preds (slice_kinds as) s

goal (1 subgoal):
 1. \<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V

goal (1 subgoal):
 1. \<exists>as n'. n -as\<rightarrow>* n' \<and> preds (slice_kinds as) s \<and> n' \<triangleq> c' \<and> (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close> \<open>preds (slice_kinds as) s\<close> \<open>n' \<triangleq> c'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
preds (slice_kinds as) s
n' \<triangleq> c'
\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V
[PROOF STEP]
show "\<exists>as n'. n -as\<rightarrow>* n' \<and> preds (slice_kinds as) s \<and> n' \<triangleq> c' \<and>
       (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
preds (slice_kinds as) s
n' \<triangleq> c'
\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V

goal (1 subgoal):
 1. \<exists>as n'. n -as\<rightarrow>* n' \<and> preds (slice_kinds as) s \<and> n' \<triangleq> c' \<and> (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>as n'. n -as\<rightarrow>* n' \<and> preds (slice_kinds as) s \<and> n' \<triangleq> c' \<and> (\<forall>V\<in>Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma corrKey_shrK_bad [simp]: "corrKey = shrK`bad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. corrKey = shrK ` bad
[PROOF STEP]
by (auto simp add: keySetup_def ltkeySetup_def corrKey_def)


[STATEMENT]
lemma PO_m3_inv1_lkeysec_init [iff]:
  "init m3 \<subseteq> m3_inv1_lkeysec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m3 \<subseteq> m3_inv1_lkeysec
[PROOF STEP]
by (auto simp add: m3_defs intro!: m3_inv1_lkeysecI)


[STATEMENT]
lemma PO_m3_inv1_lkeysec_trans [iff]:
  "{m3_inv1_lkeysec} trans m3 {> m3_inv1_lkeysec}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m3_inv1_lkeysec} TS.trans m3 {> m3_inv1_lkeysec}
[PROOF STEP]
by (fastforce simp add: PO_hoare_defs m3_defs intro!: m3_inv1_lkeysecI)


[STATEMENT]
lemma PO_m3_inv1_lkeysec [iff]: "reach m3 \<subseteq> m3_inv1_lkeysec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m3 \<subseteq> m3_inv1_lkeysec
[PROOF STEP]
by (rule inv_rule_incr) (fast+)


[STATEMENT]
lemma m3_inv1_lkeysec_for_parts [simp]:
  "\<lbrakk> s \<in> m3_inv1_lkeysec \<rbrakk> \<Longrightarrow> Key (shrK C) \<in> parts (IK s) \<longleftrightarrow> C \<in> bad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> m3_inv1_lkeysec \<Longrightarrow> (Key (shrK C) \<in> parts (IK s)) = (C \<in> bad)
[PROOF STEP]
by auto


[STATEMENT]
lemma m3_inv1_lkeysec_for_analz [simp]:
  "\<lbrakk> s \<in> m3_inv1_lkeysec \<rbrakk> \<Longrightarrow> Key (shrK C) \<in> analz (IK s) \<longleftrightarrow> C \<in> bad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> m3_inv1_lkeysec \<Longrightarrow> (Key (shrK C) \<in> analz (IK s)) = (C \<in> bad)
[PROOF STEP]
by auto


[STATEMENT]
lemma abs_msg_empty: "abs_msg {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_msg {} = {}
[PROOF STEP]
by (auto)


[STATEMENT]
lemma abs_msg_Un [simp]:
  "abs_msg (G \<union> H) = abs_msg G \<union> abs_msg H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_msg (G \<union> H) = abs_msg G \<union> abs_msg H
[PROOF STEP]
by (auto)


[STATEMENT]
lemma abs_msg_mono [elim]:
  "\<lbrakk> m \<in> abs_msg G; G \<subseteq> H \<rbrakk> \<Longrightarrow> m \<in> abs_msg H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<in> abs_msg G; G \<subseteq> H\<rbrakk> \<Longrightarrow> m \<in> abs_msg H
[PROOF STEP]
by (auto)


[STATEMENT]
lemma abs_msg_insert_mono [intro]:
  "\<lbrakk> m \<in> abs_msg H \<rbrakk> \<Longrightarrow> m \<in> abs_msg (insert m' H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> abs_msg H \<Longrightarrow> m \<in> abs_msg (insert m' H)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma abs_msg_DY_subset_fakeable:
  "\<lbrakk> (s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec \<rbrakk>
  \<Longrightarrow> abs_msg (synth (analz (IK t))) \<subseteq> fake ik0 (dom (runs s)) (chan s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec\<rbrakk> \<Longrightarrow> abs_msg (synth (analz (IK t))) \<subseteq> fake ik0 (dom (runs s)) (chan s)
[PROOF STEP]
apply (auto)
\<comment> \<open>4 subgoals, deal with replays first\<close>
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>C B K T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; Crypt (shrK C) \<lbrace>msg.Agent B, Key K, Number T\<rbrace> \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aAgt B, aKey K, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 2. \<And>C B K T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aAgt B, aKey K, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 3. \<And>C K A T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; Crypt (shrK C) \<lbrace>Key K, msg.Agent A, Number T\<rbrace> \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aKey K, aAgt A, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 4. \<And>C K A T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aKey K, aAgt A, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
[PROOF STEP]
apply (blast)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C B K T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aAgt B, aKey K, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 2. \<And>C K A T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; Crypt (shrK C) \<lbrace>Key K, msg.Agent A, Number T\<rbrace> \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aKey K, aAgt A, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 3. \<And>C K A T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aKey K, aAgt A, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
[PROOF STEP]
defer 1
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C K A T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; Crypt (shrK C) \<lbrace>Key K, msg.Agent A, Number T\<rbrace> \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aKey K, aAgt A, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 2. \<And>C K A T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aKey K, aAgt A, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 3. \<And>C B K T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aAgt B, aKey K, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
[PROOF STEP]
apply (blast)
\<comment> \<open>remaining 2 subgoals are real fakes\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C K A T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aKey K, aAgt A, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
 2. \<And>C B K T. \<lbrakk>(s, t) \<in> R23_msgs; (s, t) \<in> R23_keys; t \<in> m3_inv1_lkeysec; C \<in> bad; Key K \<in> analz (IK t)\<rbrakk> \<Longrightarrow> StatCh secure Sv C (Msg [aAgt B, aKey K, aNum T]) \<in> fake ik0 (dom (runs s)) (chan s)
[PROOF STEP]
apply (rule fake_StatCh, auto simp add: R23_keys_simps)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m3_step1_refines_m2_step1:
  "{R23}
     (m2_step1 Ra A B), (m3_step1 Ra A B)
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23} m2_step1 Ra A B, m3_step1 Ra A B {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
   (auto)


[STATEMENT]
lemma PO_m3_step2_refines_m2_step2:
  "{R23}
     (m2_step2 Rb A B), (m3_step2 Rb A B)
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23} m2_step2 Rb A B, m3_step2 Rb A B {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
   (auto)


[STATEMENT]
lemma PO_m3_step3_refines_m2_step3:
  "{R23 \<inter> (m2_inv3a_sesK_compr) \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)}
     (m2_step3 Rs A B Kab Ts), (m3_step3 Rs A B Kab Ts)
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
fix s t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
assume H:
      "(s, t) \<in> R23_msgs" "(s, t) \<in> R23_keys" "(s, t) \<in> R23_pres"
      "s \<in> m2_inv3a_sesK_compr" "t \<in> m3_inv3_sesK_compr" "t \<in> m3_inv1_lkeysec"
      "Kab = sesK (Rs$sk)" "Rs \<notin> dom (runs t)"
      "\<lbrace> Agent A, Agent B \<rbrace> \<in> parts (IK t)"
[PROOF STATE]
proof (state)
this:
(s, t) \<in> R23_msgs
(s, t) \<in> R23_keys
(s, t) \<in> R23_pres
s \<in> m2_inv3a_sesK_compr
t \<in> m3_inv3_sesK_compr
t \<in> m3_inv1_lkeysec
Kab = sesK (Rs $ sk)
Rs \<notin> dom (runs t)
\<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK t)

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
let ?s'=
      "s\<lparr> runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])),
          chan := insert (Secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)]))
                 (insert (Secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s)) \<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
let ?t'=
      "t\<lparr> runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])),
          IK := insert
                  (Crypt (shrK A) \<lbrace> Agent B, Key Kab, Number (clk t) \<rbrace>)
                (insert
                  (Crypt (shrK B) \<lbrace> Key Kab, Agent A, Number (clk t) \<rbrace>)
                (IK t)) \<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
have "(?s', ?t') \<in> R23_msgs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_msgs
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> R23_msgs
(s, t) \<in> R23_keys
(s, t) \<in> R23_pres
s \<in> m2_inv3a_sesK_compr
t \<in> m3_inv3_sesK_compr
t \<in> m3_inv1_lkeysec
Kab = sesK (Rs $ sk)
Rs \<notin> dom (runs t)
\<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK t)

goal (1 subgoal):
 1. (s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_msgs
[PROOF STEP]
by (-) (rule R23_intros, auto)
[PROOF STATE]
proof (state)
this:
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_msgs

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_msgs

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
have "(?s', ?t') \<in> R23_keys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_keys
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> R23_msgs
(s, t) \<in> R23_keys
(s, t) \<in> R23_pres
s \<in> m2_inv3a_sesK_compr
t \<in> m3_inv3_sesK_compr
t \<in> m3_inv1_lkeysec
Kab = sesK (Rs $ sk)
Rs \<notin> dom (runs t)
\<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK t)

goal (1 subgoal):
 1. (s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_keys
[PROOF STEP]
by (-) (rule R23_intros,
            auto simp add: m2_inv3a_sesK_compr_simps m3_inv3_sesK_compr_simps,
            auto simp add: R23_keys_simps)
[PROOF STATE]
proof (state)
this:
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_keys

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_keys

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
have "(?s', ?t') \<in> R23_pres"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_pres
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> R23_msgs
(s, t) \<in> R23_keys
(s, t) \<in> R23_pres
s \<in> m2_inv3a_sesK_compr
t \<in> m3_inv3_sesK_compr
t \<in> m3_inv1_lkeysec
Kab = sesK (Rs $ sk)
Rs \<notin> dom (runs t)
\<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK t)

goal (1 subgoal):
 1. (s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_pres
[PROOF STEP]
by (-) (rule R23_intros, auto)
[PROOF STATE]
proof (state)
this:
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_pres

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_pres

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_msgs
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_keys
(s\<lparr>runs := runs s(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk t)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s))\<rparr>, t\<lparr>runs := runs t(Rs \<mapsto> (Serv, [A, B], [aNum (clk t)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk t)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk t)\<rbrace>) (IK t))\<rparr>) \<in> R23_pres

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?s2, ?t2) \<in> R23_msgs; (?s2, ?t2) \<in> R23_keys; (?s2, ?t2) \<in> R23_pres; ?s2 \<in> m2_inv3a_sesK_compr; ?t2 \<in> m3_inv3_sesK_compr; ?t2 \<in> m3_inv1_lkeysec; Kab = sesK (Rs $ sk); Rs \<notin> dom (runs ?t2); \<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK ?t2)\<rbrakk> \<Longrightarrow> (?s2\<lparr>runs := runs ?s2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk ?t2)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk ?t2)])) (chan ?s2))\<rparr>, ?t2\<lparr>runs := runs ?t2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk ?t2)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk ?t2)\<rbrace>) (IK ?t2))\<rparr>) \<in> R23_msgs
\<lbrakk>(?s2, ?t2) \<in> R23_msgs; (?s2, ?t2) \<in> R23_keys; (?s2, ?t2) \<in> R23_pres; ?s2 \<in> m2_inv3a_sesK_compr; ?t2 \<in> m3_inv3_sesK_compr; ?t2 \<in> m3_inv1_lkeysec; Kab = sesK (Rs $ sk); Rs \<notin> dom (runs ?t2); \<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK ?t2)\<rbrakk> \<Longrightarrow> (?s2\<lparr>runs := runs ?s2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk ?t2)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk ?t2)])) (chan ?s2))\<rparr>, ?t2\<lparr>runs := runs ?t2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk ?t2)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk ?t2)\<rbrace>) (IK ?t2))\<rparr>) \<in> R23_keys
\<lbrakk>(?s2, ?t2) \<in> R23_msgs; (?s2, ?t2) \<in> R23_keys; (?s2, ?t2) \<in> R23_pres; ?s2 \<in> m2_inv3a_sesK_compr; ?t2 \<in> m3_inv3_sesK_compr; ?t2 \<in> m3_inv1_lkeysec; Kab = sesK (Rs $ sk); Rs \<notin> dom (runs ?t2); \<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK ?t2)\<rbrakk> \<Longrightarrow> (?s2\<lparr>runs := runs ?s2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk ?t2)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk ?t2)])) (chan ?s2))\<rparr>, ?t2\<lparr>runs := runs ?t2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk ?t2)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk ?t2)\<rbrace>) (IK ?t2))\<rparr>) \<in> R23_pres

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?s2, ?t2) \<in> R23_msgs; (?s2, ?t2) \<in> R23_keys; (?s2, ?t2) \<in> R23_pres; ?s2 \<in> m2_inv3a_sesK_compr; ?t2 \<in> m3_inv3_sesK_compr; ?t2 \<in> m3_inv1_lkeysec; Kab = sesK (Rs $ sk); Rs \<notin> dom (runs ?t2); \<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK ?t2)\<rbrakk> \<Longrightarrow> (?s2\<lparr>runs := runs ?s2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk ?t2)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk ?t2)])) (chan ?s2))\<rparr>, ?t2\<lparr>runs := runs ?t2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk ?t2)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk ?t2)\<rbrace>) (IK ?t2))\<rparr>) \<in> R23_msgs
\<lbrakk>(?s2, ?t2) \<in> R23_msgs; (?s2, ?t2) \<in> R23_keys; (?s2, ?t2) \<in> R23_pres; ?s2 \<in> m2_inv3a_sesK_compr; ?t2 \<in> m3_inv3_sesK_compr; ?t2 \<in> m3_inv1_lkeysec; Kab = sesK (Rs $ sk); Rs \<notin> dom (runs ?t2); \<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK ?t2)\<rbrakk> \<Longrightarrow> (?s2\<lparr>runs := runs ?s2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk ?t2)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk ?t2)])) (chan ?s2))\<rparr>, ?t2\<lparr>runs := runs ?t2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk ?t2)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk ?t2)\<rbrace>) (IK ?t2))\<rparr>) \<in> R23_keys
\<lbrakk>(?s2, ?t2) \<in> R23_msgs; (?s2, ?t2) \<in> R23_keys; (?s2, ?t2) \<in> R23_pres; ?s2 \<in> m2_inv3a_sesK_compr; ?t2 \<in> m3_inv3_sesK_compr; ?t2 \<in> m3_inv1_lkeysec; Kab = sesK (Rs $ sk); Rs \<notin> dom (runs ?t2); \<lbrace>msg.Agent A, msg.Agent B\<rbrace> \<in> parts (IK ?t2)\<rbrakk> \<Longrightarrow> (?s2\<lparr>runs := runs ?s2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), chan := insert (StatCh secure Sv A (Msg [aAgt B, aKey Kab, aNum (clk ?t2)])) (insert (StatCh secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk ?t2)])) (chan ?s2))\<rparr>, ?t2\<lparr>runs := runs ?t2(Rs \<mapsto> (Serv, [A, B], [aNum (clk ?t2)])), IK := insert (Crypt (shrK A) \<lbrace>msg.Agent B, Key Kab, Number (clk ?t2)\<rbrace>) (insert (Crypt (shrK B) \<lbrace>Key Kab, msg.Agent A, Number (clk ?t2)\<rbrace>) (IK ?t2))\<rparr>) \<in> R23_pres

goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}
[PROOF STEP]
by  (auto simp add: PO_rhoare_defs R23_def m3_defs)
[PROOF STATE]
proof (state)
this:
{R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} m2_step3 Rs A B Kab Ts, m3_step3 Rs A B Kab Ts {> R23}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PO_m3_step4_refines_m2_step4:
  "{R23 \<inter> UNIV \<times> (m3_inv1_lkeysec)}
     (m2_step4 Ra A B Kab Ts), (m3_step4 Ra A B Kab Ts)
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23 \<inter> UNIV \<times> m3_inv1_lkeysec} m2_step4 Ra A B Kab Ts, m3_step4 Ra A B Kab Ts {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
   (auto)


[STATEMENT]
lemma PO_m3_step5_refines_m2_step5:
  "{R23}
     (m2_step5 Rb A B Kab Ts), (m3_step5 Rb A B Kab Ts)
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23} m2_step5 Rb A B Kab Ts, m3_step5 Rb A B Kab Ts {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
   (auto)


[STATEMENT]
lemma PO_m3_tick_refines_m2_tick:
  "{R23}
     (m2_tick T), (m3_tick T)
   {>R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23} m2_tick T, m3_tick T {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
   (auto)


[STATEMENT]
lemma PO_m3_leak_refines_m2_leak:
  "{R23}
     (m2_leak Rs), (m3_leak Rs)
   {>R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23} m2_leak Rs, m3_leak Rs {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m3_defs  intro!: R23_intros)
   (auto simp add: R23_keys_simps)


[STATEMENT]
lemma PO_m3_refines_init_m2 [iff]:
  "init m3 \<subseteq> R23``(init m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m3 \<subseteq> R23 `` init m2
[PROOF STEP]
by (auto simp add: R23_def m3_defs intro!: R23_intros)


[STATEMENT]
lemma PO_m3_refines_trans_m2 [iff]:
  "{R23 \<inter> (m2_inv3a_sesK_compr) \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)}
     (trans m2), (trans m3)
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23 \<inter> m2_inv3a_sesK_compr \<times> (m3_inv3_sesK_compr \<inter> m3_inv1_lkeysec)} TS.trans m2, TS.trans m3 {> R23}
[PROOF STEP]
by (auto simp add: m3_def m3_trans_def m2_def m2_trans_def)
   (blast intro!: PO_m3_trans_refines_m2_trans)+


[STATEMENT]
lemma PO_m3_observation_consistent [iff]:
  "obs_consistent R23 med32 m2 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_consistent R23 med32 m2 m3
[PROOF STEP]
by (auto simp add: obs_consistent_def R23_def med32_def m3_defs)


[STATEMENT]
lemma m3_refines_m2 [iff]:
  "refines
     (R23 \<inter> (m2_inv3a_sesK_compr) \<times> (m3_inv1_lkeysec))
     med32 m2 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refines (R23 \<inter> m2_inv3a_sesK_compr \<times> m3_inv1_lkeysec) med32 m2 m3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. refines (R23 \<inter> m2_inv3a_sesK_compr \<times> m3_inv1_lkeysec) med32 m2 m3
[PROOF STEP]
have "R23 \<inter> m2_inv3a_sesK_compr \<times> UNIV \<subseteq> UNIV \<times> m3_inv3_sesK_compr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R23 \<inter> m2_inv3a_sesK_compr \<times> UNIV \<subseteq> UNIV \<times> m3_inv3_sesK_compr
[PROOF STEP]
by (auto simp add: R23_def R23_keys_simps intro!: m3_inv3_sesK_comprI)
[PROOF STATE]
proof (state)
this:
R23 \<inter> m2_inv3a_sesK_compr \<times> UNIV \<subseteq> UNIV \<times> m3_inv3_sesK_compr

goal (1 subgoal):
 1. refines (R23 \<inter> m2_inv3a_sesK_compr \<times> m3_inv1_lkeysec) med32 m2 m3
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
R23 \<inter> m2_inv3a_sesK_compr \<times> UNIV \<subseteq> UNIV \<times> m3_inv3_sesK_compr

goal (1 subgoal):
 1. refines (R23 \<inter> m2_inv3a_sesK_compr \<times> m3_inv1_lkeysec) med32 m2 m3
[PROOF STEP]
by (-) (rule Refinement_using_invariants, auto)
[PROOF STATE]
proof (state)
this:
refines (R23 \<inter> m2_inv3a_sesK_compr \<times> m3_inv1_lkeysec) med32 m2 m3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma m3_implements_m2 [iff]:
  "implements med32 m2 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. implements med32 m2 m3
[PROOF STEP]
by (rule refinement_soundness) (auto)


[STATEMENT]
lemma ideal_generated_subset2:
  assumes  "\<forall>b\<in>B. b \<in> ideal_generated A"
  shows "ideal_generated B \<subseteq> ideal_generated A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated B \<subseteq> ideal_generated A
[PROOF STEP]
by (metis (mono_tags, lifting) InterE assms ideal_generated_def
ideal_ideal_generated mem_Collect_eq subsetI)


[STATEMENT]
lemma ideal_explicit: "ideal_generated S
      = {y. \<exists>f U. finite U \<and> U \<subseteq> S \<and> (\<Sum>i\<in>U. f i * i) = y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S = {y. \<exists>f U. finite U \<and> U \<subseteq> S \<and> (\<Sum>i\<in>U. f i * i) = y}
[PROOF STEP]
by (simp add: ideal_generated_eq_left_ideal left_ideal_explicit)


[STATEMENT]
lemma ideal_generated_minus:
  assumes a: "a \<in> ideal_generated (S-{a})"
  shows "ideal_generated S = ideal_generated (S-{a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
proof (cases "a \<in> S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
 2. a \<notin> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> S

goal (2 subgoals):
 1. a \<in> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
 2. a \<notin> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
note a_in_S = True
[PROOF STATE]
proof (state)
this:
a \<in> S

goal (2 subgoals):
 1. a \<in> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
 2. a \<notin> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal_generated S \<subseteq> ideal_generated (S - {a})
 2. ideal_generated (S - {a}) \<subseteq> ideal_generated S
[PROOF STEP]
show "ideal_generated S \<subseteq> ideal_generated (S - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S \<subseteq> ideal_generated (S - {a})
[PROOF STEP]
proof (rule ideal_generated_subset2, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> S \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> S \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
assume b: "b \<in> S"
[PROOF STATE]
proof (state)
this:
b \<in> S

goal (1 subgoal):
 1. \<And>b. b \<in> S \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
show "b \<in> ideal_generated (S - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> ideal_generated (S - {a})
[PROOF STEP]
proof (cases "b = a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = a \<Longrightarrow> b \<in> ideal_generated (S - {a})
 2. b \<noteq> a \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = a

goal (2 subgoals):
 1. b = a \<Longrightarrow> b \<in> ideal_generated (S - {a})
 2. b \<noteq> a \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = a

goal (1 subgoal):
 1. b \<in> ideal_generated (S - {a})
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
b = a
a \<in> ideal_generated (S - {a})

goal (1 subgoal):
 1. b \<in> ideal_generated (S - {a})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> ideal_generated (S - {a})

goal (1 subgoal):
 1. b \<noteq> a \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> a \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> a

goal (1 subgoal):
 1. b \<noteq> a \<Longrightarrow> b \<in> ideal_generated (S - {a})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<noteq> a

goal (1 subgoal):
 1. b \<in> ideal_generated (S - {a})
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
b \<noteq> a
b \<in> S

goal (1 subgoal):
 1. b \<in> ideal_generated (S - {a})
[PROOF STEP]
by (simp add: ideal_generated_in)
[PROOF STATE]
proof (state)
this:
b \<in> ideal_generated (S - {a})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b \<in> ideal_generated (S - {a})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_generated S \<subseteq> ideal_generated (S - {a})

goal (1 subgoal):
 1. ideal_generated (S - {a}) \<subseteq> ideal_generated S
[PROOF STEP]
show "ideal_generated (S - {a}) \<subseteq> ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated (S - {a}) \<subseteq> ideal_generated S
[PROOF STEP]
by (rule ideal_generated_subset, auto)
[PROOF STATE]
proof (state)
this:
ideal_generated (S - {a}) \<subseteq> ideal_generated S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_generated S = ideal_generated (S - {a})

goal (1 subgoal):
 1. a \<notin> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> S

goal (1 subgoal):
 1. a \<notin> S \<Longrightarrow> ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<notin> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<notin> S

goal (1 subgoal):
 1. ideal_generated S = ideal_generated (S - {a})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ideal_generated S = ideal_generated (S - {a})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_dvd_eq:
  assumes a_dvd_b: "a dvd b"
  and a: "a \<in> S"
  and a_not_b: "a \<noteq> b"
  shows "ideal_generated S = ideal_generated (S - {b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S = ideal_generated (S - {b})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal_generated S \<subseteq> ideal_generated (S - {b})
 2. ideal_generated (S - {b}) \<subseteq> ideal_generated S
[PROOF STEP]
show "ideal_generated S \<subseteq> ideal_generated (S - {b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S \<subseteq> ideal_generated (S - {b})
[PROOF STEP]
proof (rule ideal_generated_subset2, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ba. ba \<in> S \<Longrightarrow> ba \<in> ideal_generated (S - {b})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ba. ba \<in> S \<Longrightarrow> ba \<in> ideal_generated (S - {b})
[PROOF STEP]
assume x: "x \<in> S"
[PROOF STATE]
proof (state)
this:
x \<in> S

goal (1 subgoal):
 1. \<And>ba. ba \<in> S \<Longrightarrow> ba \<in> ideal_generated (S - {b})
[PROOF STEP]
show "x \<in> ideal_generated (S - {b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ideal_generated (S - {b})
[PROOF STEP]
proof (cases "x = b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = b

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
obtain k where b_ak: "b = a * k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. b = a * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a_dvd_b
[PROOF STATE]
proof (prove)
using this:
a dvd b

goal (1 subgoal):
 1. (\<And>k. b = a * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. b = a * k

goal (1 subgoal):
 1. (\<And>k. b = a * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = a * k

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
let ?f = "\<lambda>c. k"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
have "(\<Sum>i\<in>{a}. i * ?f i) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{a}. i * k) = x
[PROOF STEP]
using True b_ak
[PROOF STATE]
proof (prove)
using this:
x = b
b = a * k

goal (1 subgoal):
 1. (\<Sum>i\<in>{a}. i * k) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a}. i * k) = x

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{a}. i * k) = x

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
have "{a} \<subseteq> S - {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a} \<subseteq> S - {b}
[PROOF STEP]
using a_not_b a
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b
a \<in> S

goal (1 subgoal):
 1. {a} \<subseteq> S - {b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a} \<subseteq> S - {b}

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{a} \<subseteq> S - {b}

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
have "finite {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {a}

goal (2 subgoals):
 1. x = b \<Longrightarrow> x \<in> ideal_generated (S - {b})
 2. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>{a}. i * k) = x
{a} \<subseteq> S - {b}
finite {a}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a}. i * k) = x
{a} \<subseteq> S - {b}
finite {a}

goal (1 subgoal):
 1. x \<in> ideal_generated (S - {b})
[PROOF STEP]
unfolding ideal_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{a}. i * k) = x
{a} \<subseteq> S - {b}
finite {a}

goal (1 subgoal):
 1. x \<in> ideal_generated (S - {b})
[PROOF STEP]
by (metis True b_ak ideal_def ideal_generated_in ideal_ideal_generated insert_subset right_ideal_def)
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated (S - {b})

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> b

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> x \<in> ideal_generated (S - {b})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> b

goal (1 subgoal):
 1. x \<in> ideal_generated (S - {b})
[PROOF STEP]
by (simp add: ideal_generated_in x)
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated (S - {b})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated (S - {b})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_generated S \<subseteq> ideal_generated (S - {b})

goal (1 subgoal):
 1. ideal_generated (S - {b}) \<subseteq> ideal_generated S
[PROOF STEP]
show "ideal_generated (S - {b}) \<subseteq> ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated (S - {b}) \<subseteq> ideal_generated S
[PROOF STEP]
by (rule ideal_generated_subset, auto)
[PROOF STATE]
proof (state)
this:
ideal_generated (S - {b}) \<subseteq> ideal_generated S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_dvd_eq_diff_set:
  assumes i_in_I: "i\<in>I" and i_in_J: "i \<notin> J" and i_dvd_j: "\<forall>j\<in>J. i dvd j"
  and f: "finite J"
  shows "ideal_generated I = ideal_generated (I - J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated I = ideal_generated (I - J)
[PROOF STEP]
using f i_in_J i_dvd_j i_in_I
[PROOF STATE]
proof (prove)
using this:
finite J
i \<notin> J
\<forall>j\<in>J. i dvd j
i \<in> I

goal (1 subgoal):
 1. ideal_generated I = ideal_generated (I - J)
[PROOF STEP]
proof (induct J arbitrary: I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I. \<lbrakk>i \<notin> {}; Ball {} ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - {})
 2. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
i \<notin> {}
\<forall>a\<in>{}. i dvd a
i \<in> I

goal (2 subgoals):
 1. \<And>I. \<lbrakk>i \<notin> {}; Ball {} ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - {})
 2. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<notin> {}
\<forall>a\<in>{}. i dvd a
i \<in> I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<notin> {}
\<forall>a\<in>{}. i dvd a
i \<in> I

goal (1 subgoal):
 1. ideal_generated I = ideal_generated (I - {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated I = ideal_generated (I - {})

goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
case (insert x J)
[PROOF STATE]
proof (state)
this:
finite J
x \<notin> J
\<lbrakk>i \<notin> J; \<forall>a\<in>J. i dvd a; i \<in> ?I\<rbrakk> \<Longrightarrow> ideal_generated ?I = ideal_generated (?I - J)
i \<notin> insert x J
\<forall>a\<in>insert x J. i dvd a
i \<in> I

goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
have "ideal_generated I = ideal_generated (I-{x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated I = ideal_generated (I - {x})
[PROOF STEP]
by (rule ideal_generated_dvd_eq[of i], insert insert.prems , auto)
[PROOF STATE]
proof (state)
this:
ideal_generated I = ideal_generated (I - {x})

goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ideal_generated I = ideal_generated (I - {x})

goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
have "... = ideal_generated ((I-{x}) - J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated (I - {x}) = ideal_generated (I - {x} - J)
[PROOF STEP]
by (rule insert.hyps, insert insert.prems insert.hyps, auto)
[PROOF STATE]
proof (state)
this:
ideal_generated (I - {x}) = ideal_generated (I - {x} - J)

goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ideal_generated (I - {x}) = ideal_generated (I - {x} - J)

goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
have "... = ideal_generated (I - insert x J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated (I - {x} - J) = ideal_generated (I - insert x J)
[PROOF STEP]
using Diff_insert2[of I x J]
[PROOF STATE]
proof (prove)
using this:
I - insert x J = I - {x} - J

goal (1 subgoal):
 1. ideal_generated (I - {x} - J) = ideal_generated (I - insert x J)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated (I - {x} - J) = ideal_generated (I - insert x J)

goal (1 subgoal):
 1. \<And>x F I. \<lbrakk>finite F; x \<notin> F; \<And>I. \<lbrakk>i \<notin> F; Ball F ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - F); i \<notin> insert x F; Ball (insert x F) ((dvd) i); i \<in> I\<rbrakk> \<Longrightarrow> ideal_generated I = ideal_generated (I - insert x F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ideal_generated I = ideal_generated (I - insert x J)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ideal_generated I = ideal_generated (I - insert x J)

goal (1 subgoal):
 1. ideal_generated I = ideal_generated (I - insert x J)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ideal_generated I = ideal_generated (I - insert x J)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_singleton_subset:
  assumes d: "d \<in> ideal_generated S" and fin_S: "finite S"
  shows "ideal_generated {d} \<subseteq> ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {d} \<subseteq> ideal_generated S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d} \<Longrightarrow> x \<in> ideal_generated S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d} \<Longrightarrow> x \<in> ideal_generated S
[PROOF STEP]
assume x: "x \<in> ideal_generated {d}"
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {d}

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d} \<Longrightarrow> x \<in> ideal_generated S
[PROOF STEP]
obtain k where x_kd: "x = k*d "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. x = k * d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_generated {d}

goal (1 subgoal):
 1. (\<And>k. x = k * d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_sum_ideal_generated[OF x]
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_generated {d}
\<lbrakk>finite {d}; \<And>f. (\<Sum>i\<in>{d}. f i * i) = x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>k. x = k * d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite.emptyI finite.insertI sum_singleton)
[PROOF STATE]
proof (state)
this:
x = k * d

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated {d} \<Longrightarrow> x \<in> ideal_generated S
[PROOF STEP]
show "x \<in> ideal_generated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ideal_generated S
[PROOF STEP]
using d ideal_eq_right_ideal ideal_ideal_generated right_ideal_def mult_commute x_kd
[PROOF STATE]
proof (prove)
using this:
d \<in> ideal_generated S
ideal ?I = right_ideal ?I
ideal (ideal_generated ?S)
right_ideal ?I = (subgroup ?I \<and> (\<forall>x\<in>?I. \<forall>r. x * r \<in> ?I))
?a * ?b = ?b * ?a
x = k * d

goal (1 subgoal):
 1. x \<in> ideal_generated S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_singleton_dvd:
  assumes i: "ideal_generated S = ideal_generated {d}" and x: "x \<in> S"
  shows "d dvd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d dvd x
[PROOF STEP]
by (metis i x finite.intros dvd_ideal_generated_singleton
      ideal_generated_in ideal_generated_singleton_subset)


[STATEMENT]
lemma ideal_generated_UNIV_insert:
  assumes "ideal_generated S = UNIV"
  shows "ideal_generated (insert a S) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated (insert a S) = UNIV
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ideal_generated S = UNIV

goal (1 subgoal):
 1. ideal_generated (insert a S) = UNIV
[PROOF STEP]
using local.ideal_generated_subset
[PROOF STATE]
proof (prove)
using this:
ideal_generated S = UNIV
?S \<subseteq> ?T \<Longrightarrow> ideal_generated ?S \<subseteq> ideal_generated ?T

goal (1 subgoal):
 1. ideal_generated (insert a S) = UNIV
[PROOF STEP]
by blast


[STATEMENT]
lemma ideal_generated_UNIV_union:
  assumes "ideal_generated S = UNIV"
  shows "ideal_generated (A \<union> S) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated (A \<union> S) = UNIV
[PROOF STEP]
using assms local.ideal_generated_subset
[PROOF STATE]
proof (prove)
using this:
ideal_generated S = UNIV
?S \<subseteq> ?T \<Longrightarrow> ideal_generated ?S \<subseteq> ideal_generated ?T

goal (1 subgoal):
 1. ideal_generated (A \<union> S) = UNIV
[PROOF STEP]
by (metis UNIV_I Un_subset_iff equalityI subsetI)


[STATEMENT]
lemma ideal_explicit2:
  assumes "finite S"
  shows "ideal_generated S = {y. \<exists>f. (\<Sum>i\<in>S. f i * i) = y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S = {y. \<exists>f. (\<Sum>i\<in>S. f i * i) = y}
[PROOF STEP]
by (smt Collect_cong assms ideal_explicit obtain_sum_ideal_generated mem_Collect_eq subsetI)


[STATEMENT]
lemma ideal_generated_unit:
  assumes u: "u dvd 1"
  shows "ideal_generated {u} = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated {u} = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal_generated {u} = UNIV
[PROOF STEP]
have "x \<in> ideal_generated {u}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
obtain inv_u where inv_u: "inv_u * u = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
u dvd (1::'a)

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. (1::'a) = u * k

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using local.mult_ac(2)
[PROOF STATE]
proof (prove)
using this:
\<exists>k. (1::'a) = u * k
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. (\<And>inv_u. inv_u * u = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv_u * u = (1::'a)

goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
have "x = x * inv_u * u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x * inv_u * u
[PROOF STEP]
using inv_u
[PROOF STATE]
proof (prove)
using this:
inv_u * u = (1::'a)

goal (1 subgoal):
 1. x = x * inv_u * u
[PROOF STEP]
by (simp add: local.mult_ac(1))
[PROOF STATE]
proof (state)
this:
x = x * inv_u * u

goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = x * inv_u * u

goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
have "... \<in> {k * u |k. k \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * inv_u * u \<in> {k * u |k. k \<in> UNIV}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * inv_u * u \<in> {k * u |k. k \<in> UNIV}

goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * inv_u * u \<in> {k * u |k. k \<in> UNIV}

goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
have "... = ideal_generated {u}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {k * u |k. k \<in> UNIV} = ideal_generated {u}
[PROOF STEP]
unfolding ideal_generated_singleton
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {k * u |k. k \<in> UNIV} = {k * u |k. k \<in> UNIV}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{k * u |k. k \<in> UNIV} = ideal_generated {u}

goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> ideal_generated {u}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_generated {u}

goal (1 subgoal):
 1. x \<in> ideal_generated {u}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {u}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x1 \<in> ideal_generated {u}

goal (1 subgoal):
 1. ideal_generated {u} = UNIV
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> ideal_generated {u}

goal (1 subgoal):
 1. ideal_generated {u} = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ideal_generated {u} = UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_generated_dvd_subset:
  assumes x: "\<forall>x \<in> S. d dvd x" and S: "finite S"
  shows "ideal_generated S \<subseteq> ideal_generated {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_generated S \<subseteq> ideal_generated {d}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
assume "x\<in> ideal_generated S"
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated S

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> ideal_generated S
[PROOF STEP]
obtain f where f: "(\<Sum>i\<in>S. f i * i) = x"
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_generated S

goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>S. f i * i) = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ideal_explicit2[OF S]
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_generated S
ideal_generated S = {y. \<exists>f. (\<Sum>i\<in>S. f i * i) = y}

goal (1 subgoal):
 1. (\<And>f. (\<Sum>i\<in>S. f i * i) = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>S. f i * i) = x

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
have "d dvd (\<Sum>i\<in>S. f i * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d dvd (\<Sum>i\<in>S. f i * i)
[PROOF STEP]
by (rule dvd_sum, insert x, auto)
[PROOF STATE]
proof (state)
this:
d dvd (\<Sum>i\<in>S. f i * i)

goal (1 subgoal):
 1. \<And>x. x \<in> ideal_generated S \<Longrightarrow> x \<in> ideal_generated {d}
[PROOF STEP]
thus "x \<in> ideal_generated {d}"
[PROOF STATE]
proof (prove)
using this:
d dvd (\<Sum>i\<in>S. f i * i)

goal (1 subgoal):
 1. x \<in> ideal_generated {d}
[PROOF STEP]
using f dvd_ideal_generated_singleton' ideal_generated_in singletonI
[PROOF STATE]
proof (prove)
using this:
d dvd (\<Sum>i\<in>S. f i * i)
(\<Sum>i\<in>S. f i * i) = x
?b dvd ?a \<Longrightarrow> ideal_generated {?a} \<subseteq> ideal_generated {?b}
?a \<in> ?A \<Longrightarrow> ?a \<in> ideal_generated ?A
?a \<in> {?a}

goal (1 subgoal):
 1. x \<in> ideal_generated {d}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> ideal_generated {d}

goal:
No subgoals!
[PROOF STEP]
qed