[STATEMENT]
lemma get_distinguishing_sequence_from_ofsm_tables_is_minimally_distinguishing :
  fixes M :: "('a,'b::linorder,'c::linorder) fsm"
  assumes "observable M"
  and     "minimal M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "q1 \<noteq> q2"
shows "minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
have *:"ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
using \<open>minimal M\<close>
[PROOF STATE]
proof (prove)
using this:
minimal M

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
unfolding minimal_observable_code[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>FSM.states M. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = {q}

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
using assms(3,4,5)
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>FSM.states M. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = {q}
q1 \<in> FSM.states M
q2 \<in> FSM.states M
q1 \<noteq> q2

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
obtain k where "k = find_first_distinct_ofsm_table M q1 q2"
             and "get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k = find_first_distinct_ofsm_table_gt M q1 q2 0; get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = find_first_distinct_ofsm_table_gt M q1 q2 0
get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k

goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = find_first_distinct_ofsm_table_gt M q1 q2 0
get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k
[PROOF STEP]
have "length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k"
[PROOF STATE]
proof (prove)
using this:
k = find_first_distinct_ofsm_table_gt M q1 q2 0
get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k

goal (1 subgoal):
 1. length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k
[PROOF STEP]
using assemble_distinguishing_sequence_from_ofsm_table_length
[PROOF STATE]
proof (prove)
using this:
k = find_first_distinct_ofsm_table_gt M q1 q2 0
get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k
length (assemble_distinguishing_sequence_from_ofsm_table ?M ?q1.0 ?q2.0 ?k) \<le> ?k

goal (1 subgoal):
 1. length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k

goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k

goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
have "\<And> io . length io < k \<Longrightarrow> \<not>distinguishes M q1 q2 io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>io. length io < k \<Longrightarrow> \<not> distinguishes M q1 q2 io
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io. length io < k \<Longrightarrow> \<not> distinguishes M q1 q2 io
[PROOF STEP]
fix io :: "('b \<times> 'c) list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io. length io < k \<Longrightarrow> \<not> distinguishes M q1 q2 io
[PROOF STEP]
assume "length io < k"
[PROOF STATE]
proof (state)
this:
length io < k

goal (1 subgoal):
 1. \<And>io. length io < k \<Longrightarrow> \<not> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length io < k
[PROOF STEP]
have "ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2"
[PROOF STATE]
proof (prove)
using this:
length io < k

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2
[PROOF STEP]
using find_first_distinct_ofsm_table_is_first[OF assms(3,4) *]
[PROOF STATE]
proof (prove)
using this:
length io < k
ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2
?k' < find_first_distinct_ofsm_table_gt M q1 q2 0 \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?k' q1 = ofsm_table M (\<lambda>q. FSM.states M) ?k' q2

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2
[PROOF STEP]
unfolding \<open>k = find_first_distinct_ofsm_table M q1 q2\<close>
[PROOF STATE]
proof (prove)
using this:
length io < find_first_distinct_ofsm_table_gt M q1 q2 0
ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2
?k' < find_first_distinct_ofsm_table_gt M q1 q2 0 \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) ?k' q1 = ofsm_table M (\<lambda>q. FSM.states M) ?k' q2

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2

goal (1 subgoal):
 1. \<And>io. length io < k \<Longrightarrow> \<not> distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2
[PROOF STEP]
show "\<not>distinguishes M q1 q2 io"
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2

goal (1 subgoal):
 1. \<not> distinguishes M q1 q2 io
[PROOF STEP]
using ofsm_table_set_observable[OF assms(1,3) minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2
ofsm_table M (\<lambda>q. FSM.states M) ?k q1 = {q' \<in> FSM.states M. \<forall>io. length io \<le> ?k \<longrightarrow> (io \<in> LS M q1) = (io \<in> LS M q') \<and> (io \<in> LS M q1 \<longrightarrow> after M q' io \<in> FSM.states M)}

goal (1 subgoal):
 1. \<not> distinguishes M q1 q2 io
[PROOF STEP]
using ofsm_table_set_observable[OF assms(1,4) minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2
ofsm_table M (\<lambda>q. FSM.states M) ?k q1 = {q' \<in> FSM.states M. \<forall>io. length io \<le> ?k \<longrightarrow> (io \<in> LS M q1) = (io \<in> LS M q') \<and> (io \<in> LS M q1 \<longrightarrow> after M q' io \<in> FSM.states M)}
ofsm_table M (\<lambda>q. FSM.states M) ?k q2 = {q' \<in> FSM.states M. \<forall>io. length io \<le> ?k \<longrightarrow> (io \<in> LS M q2) = (io \<in> LS M q') \<and> (io \<in> LS M q2 \<longrightarrow> after M q' io \<in> FSM.states M)}

goal (1 subgoal):
 1. \<not> distinguishes M q1 q2 io
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (length io) q1 = ofsm_table M (\<lambda>q. FSM.states M) (length io) q2
ofsm_table M (\<lambda>q. FSM.states M) ?k q1 = {q' \<in> FSM.states M. \<forall>io. length io \<le> ?k \<longrightarrow> (io \<in> LS M q1) = (io \<in> LS M q') \<and> (io \<in> LS M q1 \<longrightarrow> after M q' io \<in> FSM.states M)}
ofsm_table M (\<lambda>q. FSM.states M) ?k q2 = {q' \<in> FSM.states M. \<forall>io. length io \<le> ?k \<longrightarrow> (io \<in> LS M q2) = (io \<in> LS M q') \<and> (io \<in> LS M q2 \<longrightarrow> after M q' io \<in> FSM.states M)}

goal (1 subgoal):
 1. \<not> (io \<in> LS M q1 \<union> LS M q2 \<and> io \<notin> LS M q1 \<inter> LS M q2)
[PROOF STEP]
by (metis (mono_tags, lifting) Int_iff Un_iff assms(3) le_refl mem_Collect_eq ofsm_table_containment)
[PROOF STATE]
proof (state)
this:
\<not> distinguishes M q1 q2 io

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length ?io < k \<Longrightarrow> \<not> distinguishes M q1 q2 ?io

goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k
length ?io < k \<Longrightarrow> \<not> distinguishes M q1 q2 ?io
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k
length ?io < k \<Longrightarrow> \<not> distinguishes M q1 q2 ?io

goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
using get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace(1,2)[OF assms]
[PROOF STATE]
proof (prove)
using this:
length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k
length ?io < k \<Longrightarrow> \<not> distinguishes M q1 q2 ?io
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
unfolding minimally_distinguishes_def distinguishes_def
[PROOF STATE]
proof (prove)
using this:
length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k
length ?io < k \<Longrightarrow> \<not> (?io \<in> LS M q1 \<union> LS M q2 \<and> ?io \<notin> LS M q1 \<inter> LS M q2)
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. (get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2 \<and> get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2) \<and> (\<forall>io'. io' \<in> LS M q1 \<union> LS M q2 \<and> io' \<notin> LS M q1 \<inter> LS M q2 \<longrightarrow> length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> length io')
[PROOF STEP]
using le_neq_implies_less not_le_imp_less
[PROOF STATE]
proof (prove)
using this:
length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> k
length ?io < k \<Longrightarrow> \<not> (?io \<in> LS M q1 \<union> LS M q2 \<and> ?io \<notin> LS M q1 \<inter> LS M q2)
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
\<lbrakk>?m \<le> ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> ?m < ?n
\<not> ?y \<le> ?x \<Longrightarrow> ?x < ?y

goal (1 subgoal):
 1. (get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2 \<and> get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2) \<and> (\<forall>io'. io' \<in> LS M q1 \<union> LS M q2 \<and> io' \<notin> LS M q1 \<inter> LS M q2 \<longrightarrow> length (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<le> length io')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
minimally_distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minimally_distinguishes_length :
  assumes "observable M"
  and     "minimal M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "q1 \<noteq> q2"
  and     "minimally_distinguishes M q1 q2 io"
shows "length io \<le> size M - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
have "ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
using \<open>minimal M\<close>
[PROOF STATE]
proof (prove)
using this:
minimal M

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
unfolding minimal_observable_code[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>FSM.states M. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = {q}

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
using assms(3,4,5)
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>FSM.states M. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = {q}
q1 \<in> FSM.states M
q2 \<in> FSM.states M
q1 \<noteq> q2

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
have "ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q2"
[PROOF STATE]
proof (prove)
using this:
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q2
[PROOF STEP]
using ofsm_table_fix_partition_fixpoint_trivial_partition assms(3,4)
[PROOF STATE]
proof (prove)
using this:
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
?q \<in> FSM.states ?M \<Longrightarrow> ofsm_table_fix ?M (\<lambda>q. FSM.states ?M) 0 ?q = ofsm_table ?M (\<lambda>q. FSM.states ?M) (FSM.size ?M - 1) ?q
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q2

goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q2
[PROOF STEP]
obtain io' where "distinguishes M q1 q2 io'" and "length io' \<le> size M - 1"
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q2

goal (1 subgoal):
 1. (\<And>io'. \<lbrakk>distinguishes M q1 q2 io'; length io' \<le> FSM.size M - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ofsm_table_set_observable[OF assms(1,3) minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
{q' \<in> FSM.states M. \<forall>io. length io \<le> FSM.size M - 1 \<longrightarrow> (io \<in> LS M q1) = (io \<in> LS M q') \<and> (io \<in> LS M q1 \<longrightarrow> after M q' io \<in> FSM.states M)} \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q2

goal (1 subgoal):
 1. (\<And>io'. \<lbrakk>distinguishes M q1 q2 io'; length io' \<le> FSM.size M - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ofsm_table_set_observable[OF assms(1,4) minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
{q' \<in> FSM.states M. \<forall>io. length io \<le> FSM.size M - 1 \<longrightarrow> (io \<in> LS M q1) = (io \<in> LS M q') \<and> (io \<in> LS M q1 \<longrightarrow> after M q' io \<in> FSM.states M)} \<noteq> {q' \<in> FSM.states M. \<forall>io. length io \<le> FSM.size M - 1 \<longrightarrow> (io \<in> LS M q2) = (io \<in> LS M q') \<and> (io \<in> LS M q2 \<longrightarrow> after M q' io \<in> FSM.states M)}

goal (1 subgoal):
 1. (\<And>io'. \<lbrakk>distinguishes M q1 q2 io'; length io' \<le> FSM.size M - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
{q' \<in> FSM.states M. \<forall>io. length io \<le> FSM.size M - 1 \<longrightarrow> (io \<in> LS M q1) = (io \<in> LS M q') \<and> (io \<in> LS M q1 \<longrightarrow> after M q' io \<in> FSM.states M)} \<noteq> {q' \<in> FSM.states M. \<forall>io. length io \<le> FSM.size M - 1 \<longrightarrow> (io \<in> LS M q2) = (io \<in> LS M q') \<and> (io \<in> LS M q2 \<longrightarrow> after M q' io \<in> FSM.states M)}

goal (1 subgoal):
 1. (\<And>io'. \<lbrakk>io' \<in> LS M q1 \<union> LS M q2 \<and> io' \<notin> LS M q1 \<inter> LS M q2; length io' \<le> FSM.size M - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinguishes M q1 q2 io'
length io' \<le> FSM.size M - 1

goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1 q2 io'
length io' \<le> FSM.size M - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 io'
length io' \<le> FSM.size M - 1

goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
using assms(6)
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 io'
length io' \<le> FSM.size M - 1
minimally_distinguishes M q1 q2 io

goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
unfolding minimally_distinguishes_def
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 io'
length io' \<le> FSM.size M - 1
distinguishes M q1 q2 io \<and> (\<forall>io'. distinguishes M q1 q2 io' \<longrightarrow> length io \<le> length io')

goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
using dual_order.trans
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 io'
length io' \<le> FSM.size M - 1
distinguishes M q1 q2 io \<and> (\<forall>io'. distinguishes M q1 q2 io' \<longrightarrow> length io \<le> length io')
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. length io \<le> FSM.size M - 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length io \<le> FSM.size M - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cong_add_poly:
  "[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[a = b] (mod m); [c = d] (mod m)\<rbrakk> \<Longrightarrow> [a + c = b + d] (mod m)
[PROOF STEP]
by (fact cong_add)


[STATEMENT]
lemma cong_mult_poly:
  "[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[a = b] (mod m); [c = d] (mod m)\<rbrakk> \<Longrightarrow> [a * c = b * d] (mod m)
[PROOF STEP]
by (fact cong_mult)


[STATEMENT]
lemma cong_mult_self_poly: "[(a::'b::{field_gcd} poly) * m = 0] (mod m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a * m = 0] (mod m)
[PROOF STEP]
by (fact cong_mult_self_right)


[STATEMENT]
lemma cong_scalar2_poly: "[(a::'b::{field_gcd} poly)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)
[PROOF STEP]
by (fact cong_scalar_left)


[STATEMENT]
lemma cong_sum_poly:
    "(\<And>x. x \<in> A \<Longrightarrow> [((f x)::'b::{field_gcd} poly) = g x] (mod m)) \<Longrightarrow>
      [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [sum f A = sum g A] (mod m)
[PROOF STEP]
by (rule cong_sum)


[STATEMENT]
lemma cong_iff_lin_poly: "([(a::'b::{field_gcd} poly) = b] (mod m)) = (\<exists>k. b = a + m * k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = b] (mod m) = (\<exists>k. b = a + m * k)
[PROOF STEP]
using cong_diff_iff_cong_0 [of b a m]
[PROOF STATE]
proof (prove)
using this:
[b - a = 0] (mod m) = [b = a] (mod m)

goal (1 subgoal):
 1. [a = b] (mod m) = (\<exists>k. b = a + m * k)
[PROOF STEP]
by (auto simp add: cong_0_iff dvd_def algebra_simps dest: cong_sym)


[STATEMENT]
lemma cong_solve_poly: "(a::'b::{field_gcd} poly) \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> 0; n = 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
 2. \<lbrakk>a \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. \<lbrakk>a \<noteq> 0; n = 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
 2. \<lbrakk>a \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
note n0=True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. \<lbrakk>a \<noteq> 0; n = 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
 2. \<lbrakk>a \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
proof (cases "monic a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. monic a \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
 2. lead_coeff a \<noteq> (1::'b) \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
monic a

goal (2 subgoals):
 1. monic a \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
 2. lead_coeff a \<noteq> (1::'b) \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
have n: "normalize a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize a = a
[PROOF STEP]
by (rule normalize_monic[OF True])
[PROOF STATE]
proof (state)
this:
normalize a = a

goal (2 subgoals):
 1. monic a \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
 2. lead_coeff a \<noteq> (1::'b) \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
by (rule exI[of _ 1], auto simp add: n0 n cong_def)
[PROOF STATE]
proof (state)
this:
\<exists>x. [a * x = gcd a n] (mod n)

goal (1 subgoal):
 1. lead_coeff a \<noteq> (1::'b) \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lead_coeff a \<noteq> (1::'b) \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
lead_coeff a \<noteq> (1::'b)

goal (1 subgoal):
 1. lead_coeff a \<noteq> (1::'b) \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
by (auto simp add: True cong_def normalize_poly_old_def map_div_is_smult_inverse)
         (metis mult.right_neutral mult_smult_right)
[PROOF STATE]
proof (state)
this:
\<exists>x. [a * x = gcd a n] (mod n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. [a * x = gcd a n] (mod n)

goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
note n_not_0 = False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
using bezout_coefficients_fst_snd [of a n, symmetric]
[PROOF STATE]
proof (prove)
using this:
gcd a n = fst (bezout_coefficients a n) * a + snd (bezout_coefficients a n) * n

goal (1 subgoal):
 1. \<exists>x. [a * x = gcd a n] (mod n)
[PROOF STEP]
by (auto simp add: cong_iff_lin_poly mult.commute [of a] mult.commute [of n])
[PROOF STATE]
proof (state)
this:
\<exists>x. [a * x = gcd a n] (mod n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cong_solve_coprime_poly:
assumes coprime_an:"coprime (a::'b::{field_gcd} poly) n"
shows "\<exists>x. [a * x = 1] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
proof (cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)
 2. a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = 0

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)
 2. a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
unfolding cong_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. a * x mod n = 1 mod n
[PROOF STEP]
using True coprime_an
[PROOF STATE]
proof (prove)
using this:
a = 0
coprime a n

goal (1 subgoal):
 1. \<exists>x. a * x mod n = 1 mod n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. [a * x = 1] (mod n)

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> 0

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
using coprime_an cong_solve_poly[OF False, of n]
[PROOF STATE]
proof (prove)
using this:
coprime a n
\<exists>x. [a * x = gcd a n] (mod n)

goal (1 subgoal):
 1. \<exists>x. [a * x = 1] (mod n)
[PROOF STEP]
unfolding cong_def
[PROOF STATE]
proof (prove)
using this:
coprime a n
\<exists>x. a * x mod n = gcd a n mod n

goal (1 subgoal):
 1. \<exists>x. a * x mod n = 1 mod n
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<exists>x. [a * x = 1] (mod n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cong_dvd_modulus_poly:
  "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" for x y :: "'b::{field_gcd} poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[x = y] (mod m); n dvd m\<rbrakk> \<Longrightarrow> [x = y] (mod n)
[PROOF STEP]
by (auto simp add: cong_iff_lin_poly elim!: dvdE)


[STATEMENT]
lemma chinese_remainder_aux_poly:
  fixes A :: "'a set"
    and m :: "'a \<Rightarrow> 'b::{field_gcd} poly"
  assumes fin: "finite A"
    and cop: "\<forall>i \<in> A. (\<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
  shows "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. \<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i}))
[PROOF STEP]
proof (rule finite_set_choice, rule fin, rule ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
assume "i : A"
[PROOF STATE]
proof (state)
this:
i \<in> A

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
with cop
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)
i \<in> A
[PROOF STEP]
have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)
i \<in> A

goal (1 subgoal):
 1. coprime (prod m (A - {i})) (m i)
[PROOF STEP]
by (auto intro: prod_coprime_left)
[PROOF STATE]
proof (state)
this:
coprime (prod m (A - {i})) (m i)

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
coprime (prod m (A - {i})) (m i)
[PROOF STEP]
have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
[PROOF STATE]
proof (prove)
using this:
coprime (prod m (A - {i})) (m i)

goal (1 subgoal):
 1. \<exists>x. [prod m (A - {i}) * x = 1] (mod m i)
[PROOF STEP]
by (elim cong_solve_coprime_poly)
[PROOF STATE]
proof (state)
this:
\<exists>x. [prod m (A - {i}) * x = 1] (mod m i)

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. [prod m (A - {i}) * x = 1] (mod m i)
[PROOF STEP]
obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. [prod m (A - {i}) * x = 1] (mod m i)

goal (1 subgoal):
 1. (\<And>x. [prod m (A - {i}) * x = 1] (mod m i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[prod m (A - {i}) * x = 1] (mod m i)

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[prod m (A - {i}) * x = 1] (mod m i)

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
have "[(\<Prod>j \<in> A - {i}. m j) * x = 0]
    (mod (\<Prod>j \<in> A - {i}. m j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [prod m (A - {i}) * x = 0] (mod prod m (A - {i}))
[PROOF STEP]
by (subst mult.commute, rule cong_mult_self_poly)
[PROOF STATE]
proof (state)
this:
[prod m (A - {i}) * x = 0] (mod prod m (A - {i}))

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> \<exists>y. [y = 1] (mod m i) \<and> [y = 0] (mod prod m (A - {i}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[prod m (A - {i}) * x = 1] (mod m i)
[prod m (A - {i}) * x = 0] (mod prod m (A - {i}))
[PROOF STEP]
show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
      (mod prod m (A - {i}))"
[PROOF STATE]
proof (prove)
using this:
[prod m (A - {i}) * x = 1] (mod m i)
[prod m (A - {i}) * x = 0] (mod prod m (A - {i}))

goal (1 subgoal):
 1. \<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chinese_remainder_poly:
  fixes A :: "'a set"
    and m :: "'a \<Rightarrow> 'b::{field_gcd} poly"
    and u :: "'a \<Rightarrow> 'b poly"
  assumes fin: "finite A"
    and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
  shows "\<exists>x. (\<forall>i\<in>A. [x = u i] (mod m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>i\<in>A. [x = u i] (mod m i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. \<forall>i\<in>A. [x = u i] (mod m i)
[PROOF STEP]
from chinese_remainder_aux_poly [OF fin cop]
[PROOF STATE]
proof (chain)
picking this:
\<exists>b. \<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i}))
[PROOF STEP]
obtain b where
    bprop: "\<forall>i\<in>A. [b i = 1] (mod m i) \<and>
      [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
[PROOF STATE]
proof (prove)
using this:
\<exists>b. \<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i}))

goal (1 subgoal):
 1. (\<And>b. \<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i}))

goal (1 subgoal):
 1. \<exists>x. \<forall>i\<in>A. [x = u i] (mod m i)
[PROOF STEP]
let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. \<forall>i\<in>A. [x = u i] (mod m i)
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>i\<in>A. [x = u i] (mod m i)
[PROOF STEP]
proof (rule exI, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [?x = u i] (mod m i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [?x = u i] (mod m i)
[PROOF STEP]
assume a: "i : A"
[PROOF STATE]
proof (state)
this:
i \<in> A

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [?x = u i] (mod m i)
[PROOF STEP]
show "[?x = u i] (mod m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i] (mod m i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i] (mod m i)
[PROOF STEP]
from fin a
[PROOF STATE]
proof (chain)
picking this:
finite A
i \<in> A
[PROOF STEP]
have "?x = (\<Sum>j \<in> {i}. u j * b j) +
          (\<Sum>j \<in> A - {i}. u j * b j)"
[PROOF STATE]
proof (prove)
using this:
finite A
i \<in> A

goal (1 subgoal):
 1. (\<Sum>i\<in>A. u i * b i) = (\<Sum>j\<in>{i}. u j * b j) + (\<Sum>j\<in>A - {i}. u j * b j)
[PROOF STEP]
by (subst sum.union_disjoint [symmetric], auto intro: sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. u i * b i) = (\<Sum>j\<in>{i}. u j * b j) + (\<Sum>j\<in>A - {i}. u j * b j)

goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i] (mod m i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>A. u i * b i) = (\<Sum>j\<in>{i}. u j * b j) + (\<Sum>j\<in>A - {i}. u j * b j)
[PROOF STEP]
have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. u i * b i) = (\<Sum>j\<in>{i}. u j * b j) + (\<Sum>j\<in>A - {i}. u j * b j)

goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i * b i + (\<Sum>j\<in>A - {i}. u j * b j)] (mod m i)
[PROOF STEP]
unfolding cong_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. u i * b i) = (\<Sum>j\<in>{i}. u j * b j) + (\<Sum>j\<in>A - {i}. u j * b j)

goal (1 subgoal):
 1. (\<Sum>i\<in>A. u i * b i) mod m i = (u i * b i + (\<Sum>j\<in>A - {i}. u j * b j)) mod m i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[\<Sum>i\<in>A. u i * b i = u i * b i + (\<Sum>j\<in>A - {i}. u j * b j)] (mod m i)

goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i] (mod m i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[\<Sum>i\<in>A. u i * b i = u i * b i + (\<Sum>j\<in>A - {i}. u j * b j)] (mod m i)

goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i] (mod m i)
[PROOF STEP]
have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
                  u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [u i * b i + (\<Sum>j\<in>A - {i}. u j * b j) = u i * 1 + (\<Sum>j\<in>A - {i}. u j * 0)] (mod m i)
[PROOF STEP]
apply (rule cong_add_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [u i * b i = u i * 1] (mod m i)
 2. [\<Sum>j\<in>A - {i}. u j * b j = \<Sum>j\<in>A - {i}. u j * 0] (mod m i)
[PROOF STEP]
apply (rule cong_scalar2_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [b i = 1] (mod m i)
 2. [\<Sum>j\<in>A - {i}. u j * b j = \<Sum>j\<in>A - {i}. u j * 0] (mod m i)
[PROOF STEP]
using bprop a
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i}))
i \<in> A

goal (2 subgoals):
 1. [b i = 1] (mod m i)
 2. [\<Sum>j\<in>A - {i}. u j * b j = \<Sum>j\<in>A - {i}. u j * 0] (mod m i)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<Sum>j\<in>A - {i}. u j * b j = \<Sum>j\<in>A - {i}. u j * 0] (mod m i)
[PROOF STEP]
apply (rule cong_sum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A - {i} \<Longrightarrow> [u x * b x = u x * 0] (mod m i)
[PROOF STEP]
apply (rule cong_scalar2_poly)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A - {i} \<Longrightarrow> [b x = 0] (mod m i)
[PROOF STEP]
using bprop
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i}))

goal (1 subgoal):
 1. \<And>x. x \<in> A - {i} \<Longrightarrow> [b x = 0] (mod m i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> [b x = 0] (mod m i)
[PROOF STEP]
apply (rule cong_dvd_modulus_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> [b x = 0] (mod ?m19 x)
 2. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> m i dvd ?m19 x
[PROOF STEP]
apply (drule (1) bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> A; x \<noteq> i; [b x = 1] (mod m x) \<and> [b x = 0] (mod prod m (A - {x}))\<rbrakk> \<Longrightarrow> [b x = 0] (mod ?m19 x)
 2. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> m i dvd ?m19 x
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> A; x \<noteq> i; [b x = 1] (mod m x); [b x = 0] (mod prod m (A - {x}))\<rbrakk> \<Longrightarrow> [b x = 0] (mod ?m19 x)
 2. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> m i dvd ?m19 x
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> m i dvd prod m (A - {x})
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> finite (A - {x})
 2. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> i \<in> A - {x}
[PROOF STEP]
using fin a
[PROOF STATE]
proof (prove)
using this:
finite A
i \<in> A

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> finite (A - {x})
 2. \<And>x. \<lbrakk>\<forall>i\<in>A. [b i = 1] (mod m i) \<and> [b i = 0] (mod prod m (A - {i})); x \<in> A; x \<noteq> i\<rbrakk> \<Longrightarrow> i \<in> A - {x}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
[u i * b i + (\<Sum>j\<in>A - {i}. u j * b j) = u i * 1 + (\<Sum>j\<in>A - {i}. u j * 0)] (mod m i)

goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i] (mod m i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[u i * b i + (\<Sum>j\<in>A - {i}. u j * b j) = u i * 1 + (\<Sum>j\<in>A - {i}. u j * 0)] (mod m i)

goal (1 subgoal):
 1. [\<Sum>i\<in>A. u i * b i = u i] (mod m i)
[PROOF STEP]
by (metis (no_types, lifting) a add.right_neutral fin mult_cancel_left1 mult_cancel_right1
         sum.not_neutral_contains_not_neutral sum.remove)
[PROOF STATE]
proof (state)
this:
[\<Sum>i\<in>A. u i * b i = u i] (mod m i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[\<Sum>i\<in>A. u i * b i = u i] (mod m i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>i\<in>A. [x = u i] (mod m i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cong_trans_poly:
    "[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[a = b] (mod m); [b = c] (mod m)\<rbrakk> \<Longrightarrow> [a = c] (mod m)
[PROOF STEP]
by (fact cong_trans)


[STATEMENT]
lemma cong_mod_poly: "(n::'b::{field_gcd} poly) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)
[PROOF STEP]
by auto


[STATEMENT]
lemma cong_sym_poly: "[(a::'b::{field_gcd} poly) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = b] (mod m) \<Longrightarrow> [b = a] (mod m)
[PROOF STEP]
by (fact cong_sym)


[STATEMENT]
lemma cong_1_poly: "[(a::'b::{field_gcd} poly) = b] (mod 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = b] (mod 1)
[PROOF STEP]
by (fact cong_1)


[STATEMENT]
lemma coprime_cong_mult_poly:
  assumes "[(a::'b::{field_gcd} poly) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
  shows "[a = b] (mod m * n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = b] (mod m * n)
[PROOF STEP]
using divides_mult assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a dvd ?c; ?b dvd ?c; coprime ?a ?b\<rbrakk> \<Longrightarrow> ?a * ?b dvd ?c
[a = b] (mod m)
[a = b] (mod n)
coprime m n

goal (1 subgoal):
 1. [a = b] (mod m * n)
[PROOF STEP]
by (metis (no_types, opaque_lifting) cong_dvd_modulus_poly cong_iff_lin_poly dvd_mult2 dvd_refl minus_add_cancel mult.right_neutral)


[STATEMENT]
lemma coprime_cong_prod_poly:
    "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<Longrightarrow>
      (\<forall>i\<in>A. [(x::'b::{field_gcd} poly) = y] (mod m i)) \<Longrightarrow>
         [x = y] (mod (\<Prod>i\<in>A. m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j); \<forall>i\<in>A. [x = y] (mod m i)\<rbrakk> \<Longrightarrow> [x = y] (mod prod m A)
[PROOF STEP]
apply (induct A rule: infinite_finite_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j); \<forall>i\<in>A. [x = y] (mod m i)\<rbrakk> \<Longrightarrow> [x = y] (mod prod m A)
 2. \<lbrakk>\<forall>i\<in>{}. \<forall>j\<in>{}. i \<noteq> j \<longrightarrow> coprime (m i) (m j); \<forall>i\<in>{}. [x = y] (mod m i)\<rbrakk> \<Longrightarrow> [x = y] (mod prod m {})
 3. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; \<lbrakk>\<forall>i\<in>F. \<forall>j\<in>F. i \<noteq> j \<longrightarrow> coprime (m i) (m j); \<forall>i\<in>F. [x = y] (mod m i)\<rbrakk> \<Longrightarrow> [x = y] (mod prod m F); \<forall>i\<in>insert xa F. \<forall>j\<in>insert xa F. i \<noteq> j \<longrightarrow> coprime (m i) (m j); \<forall>i\<in>insert xa F. [x = y] (mod m i)\<rbrakk> \<Longrightarrow> [x = y] (mod prod m (insert xa F))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; [x = y] (mod prod m F); \<forall>j\<in>F. xa \<noteq> j \<longrightarrow> coprime (m xa) (m j); \<forall>i\<in>F. (i \<noteq> xa \<longrightarrow> coprime (m i) (m xa)) \<and> (\<forall>j\<in>F. i \<noteq> j \<longrightarrow> coprime (m i) (m j)); [x = y] (mod m xa); \<forall>i\<in>F. [x = y] (mod m i)\<rbrakk> \<Longrightarrow> [x = y] (mod m xa * prod m F)
[PROOF STEP]
apply (metis coprime_cong_mult_poly prod_coprime_right)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cong_less_modulus_unique_poly:
    "[(x::'b::{field_gcd} poly) = y] (mod m) \<Longrightarrow> degree x < degree m \<Longrightarrow> degree y < degree m \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[x = y] (mod m); degree x < degree m; degree y < degree m\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (simp add: cong_def mod_poly_less)


[STATEMENT]
lemma chinese_remainder_unique_poly:
  fixes A :: "'a set"
    and m :: "'a \<Rightarrow> 'b::{field_gcd} poly"
    and u :: "'a \<Rightarrow> 'b poly"
  assumes nz: "\<forall>i\<in>A. (m i) \<noteq> 0"
    and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
    (*The following assumption should not be necessary, but I need it since in Isabelle
      degree 0 is 0 instead of -\<infinity>*)
    and not_constant: "0 < degree (prod m A)"
  shows "\<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
from not_constant
[PROOF STATE]
proof (chain)
picking this:
0 < degree (prod m A)
[PROOF STEP]
have fin: "finite A"
[PROOF STATE]
proof (prove)
using this:
0 < degree (prod m A)

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by (metis degree_1 gr_implies_not0 prod.infinite)
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
from chinese_remainder_poly [OF fin cop]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. \<forall>i\<in>A. [x = ?u i] (mod m i)
[PROOF STEP]
obtain y where one: "(\<forall>i\<in>A. [y = u i] (mod m i))"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>i\<in>A. [x = ?u i] (mod m i)

goal (1 subgoal):
 1. (\<And>y. \<forall>i\<in>A. [y = u i] (mod m i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>A. [y = u i] (mod m i)

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
let ?x = "y mod (\<Prod>i\<in>A. m i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
have degree_prod_sum: "degree (prod m A) = (\<Sum>i\<in>A. degree (m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (prod m A) = (\<Sum>i\<in>A. degree (m i))
[PROOF STEP]
by (rule degree_prod_eq_sum_degree[OF nz])
[PROOF STATE]
proof (state)
this:
degree (prod m A) = (\<Sum>i\<in>A. degree (m i))

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
from fin nz
[PROOF STATE]
proof (chain)
picking this:
finite A
\<forall>i\<in>A. m i \<noteq> 0
[PROOF STEP]
have prodnz: "(\<Prod>i\<in>A. (m i)) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
finite A
\<forall>i\<in>A. m i \<noteq> 0

goal (1 subgoal):
 1. prod m A \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod m A \<noteq> 0

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
(*This would hold without the premise not_constant if degree 0 = -\<infinity>*)
[PROOF STATE]
proof (state)
this:
prod m A \<noteq> 0

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
have less: "degree ?x < (\<Sum>i\<in>A. degree (m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (y mod prod m A) < (\<Sum>i\<in>A. degree (m i))
[PROOF STEP]
unfolding degree_prod_sum[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (y mod prod m A) < degree (prod m A)
[PROOF STEP]
using degree_mod_less[OF prodnz, of y]
[PROOF STATE]
proof (prove)
using this:
y mod prod m A = 0 \<or> degree (y mod prod m A) < degree (prod m A)

goal (1 subgoal):
 1. degree (y mod prod m A) < degree (prod m A)
[PROOF STEP]
using not_constant
[PROOF STATE]
proof (prove)
using this:
y mod prod m A = 0 \<or> degree (y mod prod m A) < degree (prod m A)
0 < degree (prod m A)

goal (1 subgoal):
 1. degree (y mod prod m A) < degree (prod m A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (y mod prod m A) < (\<Sum>i\<in>A. degree (m i))

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>A. [y mod prod m A = u i] (mod m i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [y mod prod m A = u i] (mod m i)
[PROOF STEP]
apply (rule cong_trans_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> A \<Longrightarrow> [y mod prod m A = ?b1 i] (mod m i)
 2. \<And>i. i \<in> A \<Longrightarrow> [?b1 i = u i] (mod m i)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> A \<Longrightarrow> [?b1 i = u i] (mod m i)
 2. \<And>i. i \<in> A \<Longrightarrow> [y mod prod m A = ?b1 i] (mod m i)
[PROOF STEP]
using one
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>A. [y = u i] (mod m i)

goal (2 subgoals):
 1. \<And>i. i \<in> A \<Longrightarrow> [?b1 i = u i] (mod m i)
 2. \<And>i. i \<in> A \<Longrightarrow> [y mod prod m A = ?b1 i] (mod m i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i)\<rbrakk> \<Longrightarrow> [y mod prod m A = y] (mod m i)
[PROOF STEP]
apply (rule cong_dvd_modulus_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i)\<rbrakk> \<Longrightarrow> [y mod prod m A = y] (mod ?m11 i)
 2. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i)\<rbrakk> \<Longrightarrow> m i dvd ?m11 i
[PROOF STEP]
apply (rule cong_mod_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i)\<rbrakk> \<Longrightarrow> prod m A \<noteq> 0
 2. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i)\<rbrakk> \<Longrightarrow> m i dvd prod m A
[PROOF STEP]
using prodnz
[PROOF STATE]
proof (prove)
using this:
prod m A \<noteq> 0

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i)\<rbrakk> \<Longrightarrow> prod m A \<noteq> 0
 2. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i)\<rbrakk> \<Longrightarrow> m i dvd prod m A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i); prod m A \<noteq> 0\<rbrakk> \<Longrightarrow> m i dvd prod m A
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i); prod m A \<noteq> 0\<rbrakk> \<Longrightarrow> finite A
 2. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i); prod m A \<noteq> 0\<rbrakk> \<Longrightarrow> i \<in> A
[PROOF STEP]
apply (rule fin)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> A; \<forall>i\<in>A. [y = u i] (mod m i); prod m A \<noteq> 0\<rbrakk> \<Longrightarrow> i \<in> A
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>A. [y mod prod m A = u i] (mod m i)

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
have unique: "\<forall>z. degree z < (\<Sum>i\<in>A. degree (m i)) \<and>
      (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. degree z < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = y mod prod m A
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
fix z::"'b poly"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
assume zless: "degree z < (\<Sum>i\<in>A. degree (m i))"
[PROOF STATE]
proof (state)
this:
degree z < (\<Sum>i\<in>A. degree (m i))

goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))"
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>A. [z = u i] (mod m i)

goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
have deg1: "degree z < degree (prod m A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree z < degree (prod m A)
[PROOF STEP]
using degree_prod_sum zless
[PROOF STATE]
proof (prove)
using this:
degree (prod m A) = (\<Sum>i\<in>A. degree (m i))
degree z < (\<Sum>i\<in>A. degree (m i))

goal (1 subgoal):
 1. degree z < degree (prod m A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree z < degree (prod m A)

goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
have deg2: "degree ?x < degree (prod m A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (y mod prod m A) < degree (prod m A)
[PROOF STEP]
by (metis deg1 degree_0 degree_mod_less gr0I gr_implies_not0)
[PROOF STATE]
proof (state)
this:
degree (y mod prod m A) < degree (prod m A)

goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
have "\<forall>i\<in>A. [?x = z] (mod m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>A. [y mod prod m A = z] (mod m i)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [y mod prod m A = z] (mod m i)
[PROOF STEP]
apply (rule cong_trans_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> A \<Longrightarrow> [y mod prod m A = ?b1 i] (mod m i)
 2. \<And>i. i \<in> A \<Longrightarrow> [?b1 i = z] (mod m i)
[PROOF STEP]
using cong
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>A. [y mod prod m A = u i] (mod m i)

goal (2 subgoals):
 1. \<And>i. i \<in> A \<Longrightarrow> [y mod prod m A = ?b1 i] (mod m i)
 2. \<And>i. i \<in> A \<Longrightarrow> [?b1 i = z] (mod m i)
[PROOF STEP]
apply (erule bspec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [u i = z] (mod m i)
[PROOF STEP]
apply (rule cong_sym_poly)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [z = u i] (mod m i)
[PROOF STEP]
using zcong
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>A. [z = u i] (mod m i)

goal (1 subgoal):
 1. \<And>i. i \<in> A \<Longrightarrow> [z = u i] (mod m i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>A. [y mod prod m A = z] (mod m i)

goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
with fin cop
[PROOF STATE]
proof (chain)
picking this:
finite A
\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)
\<forall>i\<in>A. [y mod prod m A = z] (mod m i)
[PROOF STEP]
have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
[PROOF STATE]
proof (prove)
using this:
finite A
\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)
\<forall>i\<in>A. [y mod prod m A = z] (mod m i)

goal (1 subgoal):
 1. [y mod prod m A = z] (mod prod m A)
[PROOF STEP]
by (intro coprime_cong_prod_poly) auto
[PROOF STATE]
proof (state)
this:
[y mod prod m A = z] (mod prod m A)

goal (1 subgoal):
 1. \<And>z. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); \<forall>i\<in>A. [z = u i] (mod m i)\<rbrakk> \<Longrightarrow> z = y mod prod m A
[PROOF STEP]
with zless
[PROOF STATE]
proof (chain)
picking this:
degree z < (\<Sum>i\<in>A. degree (m i))
[y mod prod m A = z] (mod prod m A)
[PROOF STEP]
show "z = ?x"
[PROOF STATE]
proof (prove)
using this:
degree z < (\<Sum>i\<in>A. degree (m i))
[y mod prod m A = z] (mod prod m A)

goal (1 subgoal):
 1. z = y mod prod m A
[PROOF STEP]
apply (intro cong_less_modulus_unique_poly)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); [y mod prod m A = z] (mod prod m A)\<rbrakk> \<Longrightarrow> [z = y mod prod m A] (mod ?m2)
 2. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); [y mod prod m A = z] (mod prod m A)\<rbrakk> \<Longrightarrow> degree z < degree ?m2
 3. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); [y mod prod m A = z] (mod prod m A)\<rbrakk> \<Longrightarrow> degree (y mod prod m A) < degree ?m2
[PROOF STEP]
apply (erule cong_sym_poly)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); [y mod prod m A = z] (mod prod m A)\<rbrakk> \<Longrightarrow> degree z < degree (prod m A)
 2. \<lbrakk>degree z < (\<Sum>i\<in>A. degree (m i)); [y mod prod m A = z] (mod prod m A)\<rbrakk> \<Longrightarrow> degree (y mod prod m A) < degree (prod m A)
[PROOF STEP]
apply (auto simp add:  deg1 deg2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
z = y mod prod m A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. degree z < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = y mod prod m A

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
from less cong unique
[PROOF STATE]
proof (chain)
picking this:
degree (y mod prod m A) < (\<Sum>i\<in>A. degree (m i))
\<forall>i\<in>A. [y mod prod m A = u i] (mod m i)
\<forall>z. degree z < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = y mod prod m A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree (y mod prod m A) < (\<Sum>i\<in>A. degree (m i))
\<forall>i\<in>A. [y mod prod m A = u i] (mod m i)
\<forall>z. degree z < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = y mod prod m A

goal (1 subgoal):
 1. \<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>!x. degree x < (\<Sum>i\<in>A. degree (m i)) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addBalance_val:
  assumes "addBalance ad val acc = Some acc'"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) + ReadL\<^sub>i\<^sub>n\<^sub>t val < 2^256"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
addBalance ad val acc = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
by (simp add:Let_def split:if_split_asm)


[STATEMENT]
lemma addBalance_limit:
  assumes "addBalance ad val acc = Some acc'"
     and "\<forall>ad. ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) < 2 ^ 256"
   shows "\<forall>ad. ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) < 2 ^ 256"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
fix ad'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
show "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad') \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad') < 2 ^ 256"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
proof (cases "ReadL\<^sub>i\<^sub>n\<^sub>t val \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case t1: True
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>val\<rceil>

goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
define v where v_def: "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) + ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>ad. 0 \<le> \<lceil>accessBalance acc ad\<rceil> \<and> \<lceil>accessBalance acc ad\<rceil> < 2 ^ 256
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
have "v \<ge>0"
[PROOF STATE]
proof (prove)
using this:
\<forall>ad. 0 \<le> \<lceil>accessBalance acc ad\<rceil> \<and> \<lceil>accessBalance acc ad\<rceil> < 2 ^ 256
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. 0 \<le> v
[PROOF STEP]
by (simp add: t1)
[PROOF STATE]
proof (state)
this:
0 \<le> v

goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> v

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
proof (cases "v < 2^256")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> v; v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<lbrakk>0 \<le> v; \<not> v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case t2: True
[PROOF STATE]
proof (state)
this:
v < 2 ^ 256

goal (2 subgoals):
 1. \<lbrakk>0 \<le> v; v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<lbrakk>0 \<le> v; \<not> v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with t1 v_def
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
v < 2 ^ 256
[PROOF STEP]
have "addBalance ad val acc = Some (updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
v < 2 ^ 256

goal (1 subgoal):
 1. addBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
addBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)

goal (2 subgoals):
 1. \<lbrakk>0 \<le> v; v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<lbrakk>0 \<le> v; \<not> v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with t2 `v \<ge>0`
[PROOF STATE]
proof (chain)
picking this:
v < 2 ^ 256
0 \<le> v
addBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v < 2 ^ 256
0 \<le> v
addBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
using assms Read_ShowL_id
[PROOF STATE]
proof (prove)
using this:
v < 2 ^ 256
0 \<le> v
addBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)
addBalance ad val acc = Some acc'
\<forall>ad. 0 \<le> \<lceil>accessBalance acc ad\<rceil> \<and> \<lceil>accessBalance acc ad\<rceil> < 2 ^ 256
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. \<lbrakk>0 \<le> v; \<not> v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> v; \<not> v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> v < 2 ^ 256

goal (1 subgoal):
 1. \<lbrakk>0 \<le> v; \<not> v < 2 ^ 256\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with t1 v_def
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
\<not> v < 2 ^ 256
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
\<not> v < 2 ^ 256

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
\<not> v < 2 ^ 256
addBalance ad val acc = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> \<lceil>val\<rceil>

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> \<lceil>val\<rceil>
addBalance ad val acc = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addBalance_add:
  assumes "addBalance ad val acc = Some acc'"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) + ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
define v where "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) + ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
addBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
have "acc' = updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc"
[PROOF STATE]
proof (prove)
using this:
addBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. acc' = updateBalance ad \<lfloor>v\<rfloor> acc
[PROOF STEP]
by (simp add:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
using v_def Read_ShowL_id assms
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x
addBalance ad val acc = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addBalance_mono:
  assumes "addBalance ad val acc = Some acc'"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) \<ge> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> \<le> \<lceil>accessBalance acc' ad\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> \<le> \<lceil>accessBalance acc' ad\<rceil>
[PROOF STEP]
define v where "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) + ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> \<le> \<lceil>accessBalance acc' ad\<rceil>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
addBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
have "acc' = updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc"
[PROOF STATE]
proof (prove)
using this:
addBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. acc' = updateBalance ad \<lfloor>v\<rfloor> acc
[PROOF STEP]
by (simp add:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> \<le> \<lceil>accessBalance acc' ad\<rceil>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> \<le> \<lceil>accessBalance acc' ad\<rceil>
[PROOF STEP]
using v_def Read_ShowL_id assms
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x
addBalance ad val acc = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc ad\<rceil> \<le> \<lceil>accessBalance acc' ad\<rceil>
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc ad\<rceil> \<le> \<lceil>accessBalance acc' ad\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addBalance_eq:
  assumes "addBalance ad val acc = Some acc'"
      and "ad \<noteq> ad'"
    shows "(accessBalance acc ad') = (accessBalance acc' ad')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
define v where "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) + ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
addBalance ad val acc = Some acc'
ad \<noteq> ad'
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
have "acc' = updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc"
[PROOF STATE]
proof (prove)
using this:
addBalance ad val acc = Some acc'
ad \<noteq> ad'
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. acc' = updateBalance ad \<lfloor>v\<rfloor> acc
[PROOF STEP]
by (simp add:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
using v_def Read_ShowL_id assms
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc
v = \<lceil>accessBalance acc ad\<rceil> + \<lceil>val\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x
addBalance ad val acc = Some acc'
ad \<noteq> ad'

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
accessBalance acc ad' = accessBalance acc' ad'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subBalance_val:
  assumes "subBalance ad val acc = Some acc'"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t val \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subBalance ad val acc = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
by (simp split:if_split_asm)


[STATEMENT]
lemma subBalance_sub:
  assumes "subBalance ad val acc = Some acc'"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) - ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
define v where "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) - ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
subBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
have "acc' = updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc"
[PROOF STATE]
proof (prove)
using this:
subBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. acc' = updateBalance ad \<lfloor>v\<rfloor> acc
[PROOF STEP]
by (simp add:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
using v_def Read_ShowL_id assms
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x
subBalance ad val acc = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subBalance_limit:
  assumes "subBalance ad val acc = Some acc'"
     and "\<forall>ad. ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) < 2 ^ 256"
   shows "\<forall>ad. ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) < 2 ^ 256"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
fix ad'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
show "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad') \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad') < 2 ^ 256"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
proof (cases "ReadL\<^sub>i\<^sub>n\<^sub>t val \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case t1: True
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>val\<rceil>

goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
define v where v_def: "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) - ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with assms(2) t1
[PROOF STATE]
proof (chain)
picking this:
\<forall>ad. 0 \<le> \<lceil>accessBalance acc ad\<rceil> \<and> \<lceil>accessBalance acc ad\<rceil> < 2 ^ 256
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
have "v < 2 ^ 256"
[PROOF STATE]
proof (prove)
using this:
\<forall>ad. 0 \<le> \<lceil>accessBalance acc ad\<rceil> \<and> \<lceil>accessBalance acc ad\<rceil> < 2 ^ 256
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. v < 2 ^ 256
[PROOF STEP]
by (smt (verit))
[PROOF STATE]
proof (state)
this:
v < 2 ^ 256

goal (2 subgoals):
 1. 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v < 2 ^ 256
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v < 2 ^ 256

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
proof (cases "v \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>v < 2 ^ 256; 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<lbrakk>v < 2 ^ 256; \<not> 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case t2: True
[PROOF STATE]
proof (state)
this:
0 \<le> v

goal (2 subgoals):
 1. \<lbrakk>v < 2 ^ 256; 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<lbrakk>v < 2 ^ 256; \<not> 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with t1 v_def
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
0 \<le> v
[PROOF STEP]
have "subBalance ad val acc = Some (updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
0 \<le> v

goal (1 subgoal):
 1. subBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)

goal (2 subgoals):
 1. \<lbrakk>v < 2 ^ 256; 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
 2. \<lbrakk>v < 2 ^ 256; \<not> 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with t2 `v < 2 ^ 256`
[PROOF STATE]
proof (chain)
picking this:
0 \<le> v
v < 2 ^ 256
subBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> v
v < 2 ^ 256
subBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
using assms Read_ShowL_id
[PROOF STATE]
proof (prove)
using this:
0 \<le> v
v < 2 ^ 256
subBalance ad val acc = Some (updateBalance ad \<lfloor>v\<rfloor> acc)
subBalance ad val acc = Some acc'
\<forall>ad. 0 \<le> \<lceil>accessBalance acc ad\<rceil> \<and> \<lceil>accessBalance acc ad\<rceil> < 2 ^ 256
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. \<lbrakk>v < 2 ^ 256; \<not> 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>v < 2 ^ 256; \<not> 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> v

goal (1 subgoal):
 1. \<lbrakk>v < 2 ^ 256; \<not> 0 \<le> v\<rbrakk> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
with t1 v_def
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
\<not> 0 \<le> v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
\<not> 0 \<le> v

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<lceil>val\<rceil>
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
\<not> 0 \<le> v
subBalance ad val acc = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<not> 0 \<le> \<lceil>val\<rceil> \<Longrightarrow> 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> \<lceil>val\<rceil>

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> \<lceil>val\<rceil>
subBalance ad val acc = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subBalance_mono:
  assumes "subBalance ad val acc = Some acc'"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) \<ge> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> \<le> \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> \<le> \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
define v where "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) - ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> \<le> \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
subBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
have "acc' = updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc"
[PROOF STATE]
proof (prove)
using this:
subBalance ad val acc = Some acc'
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. acc' = updateBalance ad \<lfloor>v\<rfloor> acc
[PROOF STEP]
by (simp add:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> \<le> \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> \<le> \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
using v_def Read_ShowL_id assms
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x
subBalance ad val acc = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> \<le> \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ad\<rceil> \<le> \<lceil>accessBalance acc ad\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subBalance_eq:
  assumes "subBalance ad val acc = Some acc'"
      and "ad \<noteq> ad'"
    shows "(accessBalance acc ad') = (accessBalance acc' ad')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
define v where "v = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) - ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (state)
this:
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
subBalance ad val acc = Some acc'
ad \<noteq> ad'
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
have "acc' = updateBalance ad (ShowL\<^sub>i\<^sub>n\<^sub>t v) acc"
[PROOF STATE]
proof (prove)
using this:
subBalance ad val acc = Some acc'
ad \<noteq> ad'
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. acc' = updateBalance ad \<lfloor>v\<rfloor> acc
[PROOF STEP]
by (simp add:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
using v_def Read_ShowL_id assms
[PROOF STATE]
proof (prove)
using this:
acc' = updateBalance ad \<lfloor>v\<rfloor> acc
v = \<lceil>accessBalance acc ad\<rceil> - \<lceil>val\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x
subBalance ad val acc = Some acc'
ad \<noteq> ad'

goal (1 subgoal):
 1. accessBalance acc ad' = accessBalance acc' ad'
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
accessBalance acc ad' = accessBalance acc' ad'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_val1:
  assumes "transfer ads addr val acc = Some acc'"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t val \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
transfer ads addr val acc = Some acc'
[PROOF STEP]
obtain acc''
    where *: "subBalance ads val acc = Some acc''"
      and **: "addBalance addr val acc'' = Some acc'"
[PROOF STATE]
proof (prove)
using this:
transfer ads addr val acc = Some acc'

goal (1 subgoal):
 1. (\<And>acc''. \<lbrakk>subBalance ads val acc = Some acc''; addBalance addr val acc'' = Some acc'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
[PROOF STEP]
show "ReadL\<^sub>i\<^sub>n\<^sub>t val \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
using subBalance_val[OF *]
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
0 \<le> \<lceil>val\<rceil>

goal (1 subgoal):
 1. 0 \<le> \<lceil>val\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>val\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed