[STATEMENT]
lemma mset_un_single_un_cases [consumes 1, case_names left right]:
    assumes A: "add_mset a A = B + C"
      and CASES: "a \<in># B \<Longrightarrow> A = (B - {#a#}) + C \<Longrightarrow> P"
        "a \<in># C \<Longrightarrow> A = B + (C - {#a#}) \<Longrightarrow> P"
    shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
have "a \<in># A+{#a#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in># A + {#a#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<in># A + {#a#}

goal (1 subgoal):
 1. P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset a A = B + C
a \<in># A + {#a#}
[PROOF STEP]
have "a \<in># B+C"
[PROOF STATE]
proof (prove)
using this:
add_mset a A = B + C
a \<in># A + {#a#}

goal (1 subgoal):
 1. a \<in># B + C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in># B + C

goal (1 subgoal):
 1. P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in># B + C

goal (1 subgoal):
 1. P
[PROOF STEP]
proof (cases rule: mset_un_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in># B \<Longrightarrow> P
 2. a \<in># C \<Longrightarrow> P
[PROOF STEP]
case left
[PROOF STATE]
proof (state)
this:
a \<in># B

goal (2 subgoals):
 1. a \<in># B \<Longrightarrow> P
 2. a \<in># C \<Longrightarrow> P
[PROOF STEP]
hence "B=B-{#a#}+{#a#}"
[PROOF STATE]
proof (prove)
using this:
a \<in># B

goal (1 subgoal):
 1. B = B - {#a#} + {#a#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = B - {#a#} + {#a#}

goal (2 subgoals):
 1. a \<in># B \<Longrightarrow> P
 2. a \<in># C \<Longrightarrow> P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset a A = B + C
B = B - {#a#} + {#a#}
[PROOF STEP]
have "A+{#a#} = (B-{#a#})+C+{#a#}"
[PROOF STATE]
proof (prove)
using this:
add_mset a A = B + C
B = B - {#a#} + {#a#}

goal (1 subgoal):
 1. A + {#a#} = B - {#a#} + C + {#a#}
[PROOF STEP]
by (auto simp add: union_ac)
[PROOF STATE]
proof (state)
this:
A + {#a#} = B - {#a#} + C + {#a#}

goal (2 subgoals):
 1. a \<in># B \<Longrightarrow> P
 2. a \<in># C \<Longrightarrow> P
[PROOF STEP]
hence "A=(B-{#a#})+C"
[PROOF STATE]
proof (prove)
using this:
A + {#a#} = B - {#a#} + C + {#a#}

goal (1 subgoal):
 1. A = B - {#a#} + C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A = B - {#a#} + C

goal (2 subgoals):
 1. a \<in># B \<Longrightarrow> P
 2. a \<in># C \<Longrightarrow> P
[PROOF STEP]
with CASES(1)[OF left]
[PROOF STATE]
proof (chain)
picking this:
A = B - {#a#} + C \<Longrightarrow> P
A = B - {#a#} + C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = B - {#a#} + C \<Longrightarrow> P
A = B - {#a#} + C

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P

goal (1 subgoal):
 1. a \<in># C \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in># C \<Longrightarrow> P
[PROOF STEP]
case right
[PROOF STATE]
proof (state)
this:
a \<in># C

goal (1 subgoal):
 1. a \<in># C \<Longrightarrow> P
[PROOF STEP]
hence "C=C-{#a#}+{#a#}"
[PROOF STATE]
proof (prove)
using this:
a \<in># C

goal (1 subgoal):
 1. C = C - {#a#} + {#a#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = C - {#a#} + {#a#}

goal (1 subgoal):
 1. a \<in># C \<Longrightarrow> P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset a A = B + C
C = C - {#a#} + {#a#}
[PROOF STEP]
have "A+{#a#} = B+(C-{#a#})+{#a#}"
[PROOF STATE]
proof (prove)
using this:
add_mset a A = B + C
C = C - {#a#} + {#a#}

goal (1 subgoal):
 1. A + {#a#} = B + (C - {#a#}) + {#a#}
[PROOF STEP]
by (auto simp add: union_ac)
[PROOF STATE]
proof (state)
this:
A + {#a#} = B + (C - {#a#}) + {#a#}

goal (1 subgoal):
 1. a \<in># C \<Longrightarrow> P
[PROOF STEP]
hence "A=B+(C-{#a#})"
[PROOF STATE]
proof (prove)
using this:
A + {#a#} = B + (C - {#a#}) + {#a#}

goal (1 subgoal):
 1. A = B + (C - {#a#})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A = B + (C - {#a#})

goal (1 subgoal):
 1. a \<in># C \<Longrightarrow> P
[PROOF STEP]
with CASES(2)[OF right]
[PROOF STATE]
proof (chain)
picking this:
A = B + (C - {#a#}) \<Longrightarrow> P
A = B + (C - {#a#})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = B + (C - {#a#}) \<Longrightarrow> P
A = B + (C - {#a#})

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_distrib[consumes 1, case_names dist]: assumes A: "(A::'a multiset)+B = M+N" "!!Am An Bm Bn. \<lbrakk>A=Am+An; B=Bm+Bn; M=Am+Bm; N=An+Bn\<rbrakk> \<Longrightarrow> P" shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
have BN_MA: "B - N = M - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B - N = M - A
[PROOF STEP]
by (metis (no_types) add_diff_cancel_right assms(1) union_commute)
[PROOF STATE]
proof (state)
this:
B - N = M - A

goal (1 subgoal):
 1. P
[PROOF STEP]
have H: "A = A\<inter># C + (A - C) \<inter># D" if "A + B = C + D" for A B C D :: "'a multiset"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = A \<inter># C + (A - C) \<inter># D
[PROOF STEP]
by (metis add.commute diff_intersect_left_idem mset_subset_eq_add_left subset_eq_diff_conv
          subset_mset.add_diff_inverse subset_mset.inf_absorb1 subset_mset.inf_le1 that)
[PROOF STATE]
proof (state)
this:
?A + ?B = ?C + ?D \<Longrightarrow> ?A = ?A \<inter># ?C + (?A - ?C) \<inter># ?D

goal (1 subgoal):
 1. P
[PROOF STEP]
have A': "A = A\<inter># M + (A - M) \<inter># N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = A \<inter># M + (A - M) \<inter># N
[PROOF STEP]
using A(1) H
[PROOF STATE]
proof (prove)
using this:
A + B = M + N
?A + ?B = ?C + ?D \<Longrightarrow> ?A = ?A \<inter># ?C + (?A - ?C) \<inter># ?D

goal (1 subgoal):
 1. A = A \<inter># M + (A - M) \<inter># N
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A = A \<inter># M + (A - M) \<inter># N

goal (1 subgoal):
 1. P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A = A \<inter># M + (A - M) \<inter># N

goal (1 subgoal):
 1. P
[PROOF STEP]
have B': "B = (B - N) \<inter># M + B\<inter># N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = (B - N) \<inter># M + B \<inter># N
[PROOF STEP]
using A(1) H[of B A N M]
[PROOF STATE]
proof (prove)
using this:
A + B = M + N
B + A = N + M \<Longrightarrow> B = B \<inter># N + (B - N) \<inter># M

goal (1 subgoal):
 1. B = (B - N) \<inter># M + B \<inter># N
[PROOF STEP]
by (auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
B = (B - N) \<inter># M + B \<inter># N

goal (1 subgoal):
 1. P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B = (B - N) \<inter># M + B \<inter># N

goal (1 subgoal):
 1. P
[PROOF STEP]
have "M = A \<inter># M + (B - N) \<inter># M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M = A \<inter># M + (B - N) \<inter># M
[PROOF STEP]
using H[of M N A B] BN_MA[symmetric] A(1)
[PROOF STATE]
proof (prove)
using this:
M + N = A + B \<Longrightarrow> M = M \<inter># A + (M - A) \<inter># B
M - A = B - N
A + B = M + N

goal (1 subgoal):
 1. M = A \<inter># M + (B - N) \<inter># M
[PROOF STEP]
by (metis (no_types) diff_intersect_left_idem
          diff_union_cancelR multiset_inter_commute subset_mset.diff_add subset_mset.inf.cobounded1
          union_commute)
[PROOF STATE]
proof (state)
this:
M = A \<inter># M + (B - N) \<inter># M

goal (1 subgoal):
 1. P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
M = A \<inter># M + (B - N) \<inter># M

goal (1 subgoal):
 1. P
[PROOF STEP]
have "N = (A - M) \<inter># N + B \<inter># N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N = (A - M) \<inter># N + B \<inter># N
[PROOF STEP]
by (metis A' assms(1) diff_union_cancelL inter_union_distrib_left inter_union_distrib_right
          mset_subset_eq_multiset_union_diff_commute subset_mset.inf.cobounded1 subset_mset.inf.commute)
[PROOF STATE]
proof (state)
this:
N = (A - M) \<inter># N + B \<inter># N

goal (1 subgoal):
 1. P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A = A \<inter># M + (A - M) \<inter># N
B = (B - N) \<inter># M + B \<inter># N
M = A \<inter># M + (B - N) \<inter># M
N = (A - M) \<inter># N + B \<inter># N
[PROOF STEP]
show P
[PROOF STATE]
proof (prove)
using this:
A = A \<inter># M + (A - M) \<inter># N
B = (B - N) \<inter># M + B \<inter># N
M = A \<inter># M + (B - N) \<inter># M
N = (A - M) \<inter># N + B \<inter># N

goal (1 subgoal):
 1. P
[PROOF STEP]
using A(2)
[PROOF STATE]
proof (prove)
using this:
A = A \<inter># M + (A - M) \<inter># N
B = (B - N) \<inter># M + B \<inter># N
M = A \<inter># M + (B - N) \<inter># M
N = (A - M) \<inter># N + B \<inter># N
\<lbrakk>A = ?Am + ?An; B = ?Bm + ?Bn; M = ?Am + ?Bm; N = ?An + ?Bn\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_size_le1_cases[case_names empty singleton,consumes 1]: "\<lbrakk> size M \<le> Suc 0; M={#} \<Longrightarrow> P; !!m. M={#m#} \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size M \<le> Suc 0; M = {#} \<Longrightarrow> P; \<And>m. M = {#m#} \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (cases M) auto


[STATEMENT]
lemma diff_union_single_conv2:
  "a \<in># J \<Longrightarrow> J + I - {#a#} = (J - {#a#}) + I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in># J \<Longrightarrow> J + I - {#a#} = J - {#a#} + I
[PROOF STEP]
using diff_union_single_conv [of a J I]
[PROOF STATE]
proof (prove)
using this:
a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})

goal (1 subgoal):
 1. a \<in># J \<Longrightarrow> J + I - {#a#} = J - {#a#} + I
[PROOF STEP]
by (simp add: union_ac)


[STATEMENT]
lemma mset_contains_eq: "(m \<in># M) = ({#m#}+(M-{#m#})=M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m \<in># M) = ({#m#} + (M - {#m#}) = M)
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_mset m (M - {#m#}) = M \<Longrightarrow> m \<in># M
[PROOF STEP]
assume "add_mset m (M - {#m#}) = M"
[PROOF STATE]
proof (state)
this:
add_mset m (M - {#m#}) = M

goal (1 subgoal):
 1. add_mset m (M - {#m#}) = M \<Longrightarrow> m \<in># M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
add_mset m (M - {#m#}) = M

goal (1 subgoal):
 1. add_mset m (M - {#m#}) = M \<Longrightarrow> m \<in># M
[PROOF STEP]
have "m \<in># {#m#} + (M - {#m#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in># {#m#} + (M - {#m#})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m \<in># {#m#} + (M - {#m#})

goal (1 subgoal):
 1. add_mset m (M - {#m#}) = M \<Longrightarrow> m \<in># M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
add_mset m (M - {#m#}) = M
m \<in># {#m#} + (M - {#m#})
[PROOF STEP]
show "m \<in># M"
[PROOF STATE]
proof (prove)
using this:
add_mset m (M - {#m#}) = M
m \<in># {#m#} + (M - {#m#})

goal (1 subgoal):
 1. m \<in># M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m \<in># M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_le_incr_right1: "(a::'a multiset)\<subseteq>#b \<Longrightarrow> a\<subseteq>#b+c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<subseteq># b \<Longrightarrow> a \<subseteq># b + c
[PROOF STEP]
using mset_subset_eq_mono_add[of a b "{#}" c, simplified]
[PROOF STATE]
proof (prove)
using this:
a \<subseteq># b \<Longrightarrow> a \<subseteq># b + c

goal (1 subgoal):
 1. a \<subseteq># b \<Longrightarrow> a \<subseteq># b + c
[PROOF STEP]
.


[STATEMENT]
lemma mset_le_incr_right2: "(a::'a multiset)\<subseteq>#b \<Longrightarrow> a\<subseteq>#c+b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<subseteq># b \<Longrightarrow> a \<subseteq># c + b
[PROOF STEP]
using mset_le_incr_right1
[PROOF STATE]
proof (prove)
using this:
?a \<subseteq># ?b \<Longrightarrow> ?a \<subseteq># ?b + ?c

goal (1 subgoal):
 1. a \<subseteq># b \<Longrightarrow> a \<subseteq># c + b
[PROOF STEP]
by (auto simp add: union_commute)


[STATEMENT]
lemma mset_le_decr_left1: "(a::'a multiset)+c\<subseteq>#b \<Longrightarrow> a\<subseteq>#b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + c \<subseteq># b \<Longrightarrow> a \<subseteq># b
[PROOF STEP]
using mset_le_incr_right1 mset_subset_eq_mono_add_right_cancel
[PROOF STATE]
proof (prove)
using this:
?a \<subseteq># ?b \<Longrightarrow> ?a \<subseteq># ?b + ?c
(?A + ?C \<subseteq># ?B + ?C) = (?A \<subseteq># ?B)

goal (1 subgoal):
 1. a + c \<subseteq># b \<Longrightarrow> a \<subseteq># b
[PROOF STEP]
by blast


[STATEMENT]
lemma mset_le_decr_left2: "c+(a::'a multiset)\<subseteq>#b \<Longrightarrow> a\<subseteq>#b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c + a \<subseteq># b \<Longrightarrow> a \<subseteq># b
[PROOF STEP]
using mset_le_decr_left1
[PROOF STATE]
proof (prove)
using this:
?a + ?c \<subseteq># ?b \<Longrightarrow> ?a \<subseteq># ?b

goal (1 subgoal):
 1. c + a \<subseteq># b \<Longrightarrow> a \<subseteq># b
[PROOF STEP]
by (auto simp add: union_ac)


[STATEMENT]
lemma mset_le_add_mset_decr_left1: "add_mset c a\<subseteq>#(b::'a multiset) \<Longrightarrow> a\<subseteq>#b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset c a \<subseteq># b \<Longrightarrow> a \<subseteq># b
[PROOF STEP]
by (simp add: mset_subset_eq_insertD subset_mset.dual_order.strict_implies_order)


[STATEMENT]
lemma mset_le_add_mset_decr_left2: "add_mset c a\<subseteq>#(b::'a multiset) \<Longrightarrow> {#c#}\<subseteq>#b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset c a \<subseteq># b \<Longrightarrow> {#c#} \<subseteq># b
[PROOF STEP]
by (simp add: mset_subset_eq_insertD subset_mset.dual_order.strict_implies_order)


[STATEMENT]
lemma mset_union_subset: "(A::'a multiset)+B \<subseteq># C \<Longrightarrow> A\<subseteq>#C \<and> B\<subseteq>#C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A + B \<subseteq># C \<Longrightarrow> A \<subseteq># C \<and> B \<subseteq># C
[PROOF STEP]
by (auto dest: mset_le_decr_left)


[STATEMENT]
lemma mset_le_add_mset: "add_mset x B \<subseteq># C \<Longrightarrow> {#x#}\<subseteq>#C \<and> B\<subseteq>#(C::'a multiset)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset x B \<subseteq># C \<Longrightarrow> {#x#} \<subseteq># C \<and> B \<subseteq># C
[PROOF STEP]
by (auto dest: mset_le_decr_left)


[STATEMENT]
lemma mset_le_subtract_left: "(A::'a multiset)+B \<subseteq># X \<Longrightarrow> B \<subseteq># X-A \<and> A\<subseteq>#X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A + B \<subseteq># X \<Longrightarrow> B \<subseteq># X - A \<and> A \<subseteq># X
[PROOF STEP]
by (auto dest: mset_le_subtract[of "A+B" "X" "A"] mset_union_subset)


[STATEMENT]
lemma mset_le_subtract_right: "(A::'a multiset)+B \<subseteq># X \<Longrightarrow> A \<subseteq># X-B \<and> B\<subseteq>#X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A + B \<subseteq># X \<Longrightarrow> A \<subseteq># X - B \<and> B \<subseteq># X
[PROOF STEP]
by (auto dest: mset_le_subtract[of "A+B" "X" "B"] mset_union_subset)


[STATEMENT]
lemma mset_le_subtract_add_mset_left: "add_mset x B \<subseteq># (X::'a multiset) \<Longrightarrow> B \<subseteq># X-{#x#} \<and> {#x#}\<subseteq>#X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset x B \<subseteq># X \<Longrightarrow> B \<subseteq># X - {#x#} \<and> {#x#} \<subseteq># X
[PROOF STEP]
by (auto dest: mset_le_subtract[of "add_mset x B" "X" "{#x#}"] mset_le_add_mset)


[STATEMENT]
lemma mset_le_subtract_add_mset_right: "add_mset x B \<subseteq># (X::'a multiset) \<Longrightarrow> {#x#} \<subseteq># X-B \<and> B\<subseteq>#X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset x B \<subseteq># X \<Longrightarrow> {#x#} \<subseteq># X - B \<and> B \<subseteq># X
[PROOF STEP]
by (auto dest: mset_le_subtract[of "add_mset x B" "X" "B"] mset_le_add_mset)


[STATEMENT]
lemma mset_le_addE: "\<lbrakk> (xs::'a multiset) \<subseteq># ys; !!zs. ys=xs+zs \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<subseteq># ys; \<And>zs. ys = xs + zs \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
using mset_subset_eq_exists_conv
[PROOF STATE]
proof (prove)
using this:
(?A \<subseteq># ?B) = (\<exists>C. ?B = ?A + C)

goal (1 subgoal):
 1. \<lbrakk>xs \<subseteq># ys; \<And>zs. ys = xs + zs \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by blast


[STATEMENT]
lemma mset_2dist2_cases:
    assumes A: "{#a, b#} \<subseteq># A + B"
    assumes CASES: "{#a, b#} \<subseteq># A \<Longrightarrow> P" "{#a, b#} \<subseteq># B \<Longrightarrow> P"
      "a \<in># A \<Longrightarrow> b \<in># B \<Longrightarrow> P" "a \<in># B \<Longrightarrow> b \<in># A \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
{#a, b#} \<subseteq># A + B
[PROOF STEP]
have "count A a + count B a \<ge> 1"
      "count A b + count B b \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
{#a, b#} \<subseteq># A + B

goal (1 subgoal):
 1. 1 \<le> count A a + count B a &&& 1 \<le> count A b + count B b
[PROOF STEP]
using mset_subset_eq_count [of "{#a, b#}" "A + B" a] mset_subset_eq_count [of "{#a, b#}" "A + B" b]
[PROOF STATE]
proof (prove)
using this:
{#a, b#} \<subseteq># A + B
{#a, b#} \<subseteq># A + B \<Longrightarrow> count {#a, b#} a \<le> count (A + B) a
{#a, b#} \<subseteq># A + B \<Longrightarrow> count {#a, b#} b \<le> count (A + B) b

goal (1 subgoal):
 1. 1 \<le> count A a + count B a &&& 1 \<le> count A b + count B b
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
1 \<le> count A a + count B a
1 \<le> count A b + count B b

goal (1 subgoal):
 1. P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> count A a + count B a
1 \<le> count A b + count B b
[PROOF STEP]
have B: "a \<in># A \<or> a \<in># B"
      "b \<in># A \<or> b \<in># B"
[PROOF STATE]
proof (prove)
using this:
1 \<le> count A a + count B a
1 \<le> count A b + count B b

goal (1 subgoal):
 1. a \<in># A \<or> a \<in># B &&& b \<in># A \<or> b \<in># B
[PROOF STEP]
by (auto simp add: not_in_iff Suc_le_eq)
[PROOF STATE]
proof (state)
this:
a \<in># A \<or> a \<in># B
b \<in># A \<or> b \<in># B

goal (1 subgoal):
 1. P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a \<in># A \<or> a \<in># B
b \<in># A \<or> b \<in># B

goal (1 subgoal):
 1. P
[PROOF STEP]
assume C: "a \<in># A" "b \<in># A - {#a#}"
[PROOF STATE]
proof (state)
this:
a \<in># A
b \<in># A - {#a#}

goal (1 subgoal):
 1. P
[PROOF STEP]
with mset_subset_eq_mono_add [of "{#a#}" "{#a#}" "{#b#}" "A-{#a#}"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>{#a#} \<subseteq># {#a#}; {#b#} \<subseteq># A - {#a#}\<rbrakk> \<Longrightarrow> {#a#} + {#b#} \<subseteq># {#a#} + (A - {#a#})
a \<in># A
b \<in># A - {#a#}
[PROOF STEP]
have "{#a, b#} \<subseteq># A"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{#a#} \<subseteq># {#a#}; {#b#} \<subseteq># A - {#a#}\<rbrakk> \<Longrightarrow> {#a#} + {#b#} \<subseteq># {#a#} + (A - {#a#})
a \<in># A
b \<in># A - {#a#}

goal (1 subgoal):
 1. {#a, b#} \<subseteq># A
[PROOF STEP]
by (auto simp: add_mset_commute)
[PROOF STATE]
proof (state)
this:
{#a, b#} \<subseteq># A

goal (1 subgoal):
 1. P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in># A; b \<in># A - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># A

goal (1 subgoal):
 1. P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in># A; b \<in># A - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># A

goal (1 subgoal):
 1. P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in># A; b \<in># A - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># A

goal (1 subgoal):
 1. P
[PROOF STEP]
assume C: "a \<in># A" "b \<notin># A - {#a#}"
[PROOF STATE]
proof (state)
this:
a \<in># A
b \<notin># A - {#a#}

goal (1 subgoal):
 1. P
[PROOF STEP]
with B A
[PROOF STATE]
proof (chain)
picking this:
a \<in># A \<or> a \<in># B
b \<in># A \<or> b \<in># B
{#a, b#} \<subseteq># A + B
a \<in># A
b \<notin># A - {#a#}
[PROOF STEP]
have "b \<in># B"
[PROOF STATE]
proof (prove)
using this:
a \<in># A \<or> a \<in># B
b \<in># A \<or> b \<in># B
{#a, b#} \<subseteq># A + B
a \<in># A
b \<notin># A - {#a#}

goal (1 subgoal):
 1. b \<in># B
[PROOF STEP]
by (auto simp: insert_subset_eq_iff diff_union_single_convs
            simp del: subset_mset.add_diff_assoc2)
[PROOF STATE]
proof (state)
this:
b \<in># B

goal (1 subgoal):
 1. P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in># A; b \<notin># A - {#a#}\<rbrakk> \<Longrightarrow> b \<in># B

goal (1 subgoal):
 1. P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in># A; b \<notin># A - {#a#}\<rbrakk> \<Longrightarrow> b \<in># B

goal (1 subgoal):
 1. P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in># A; b \<notin># A - {#a#}\<rbrakk> \<Longrightarrow> b \<in># B

goal (1 subgoal):
 1. P
[PROOF STEP]
assume C: "a \<notin># A" "b \<in># B - {#a#}"
[PROOF STATE]
proof (state)
this:
a \<notin># A
b \<in># B - {#a#}

goal (1 subgoal):
 1. P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
{#a, b#} \<subseteq># A + B
a \<notin># A
b \<in># B - {#a#}
[PROOF STEP]
have "a \<in># B"
[PROOF STATE]
proof (prove)
using this:
{#a, b#} \<subseteq># A + B
a \<notin># A
b \<in># B - {#a#}

goal (1 subgoal):
 1. a \<in># B
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
{#a, b#} \<subseteq># A + B
a \<notin># A
b \<in># B - {#a#}
a \<in># A \<or> a \<in># B
b \<in># A \<or> b \<in># B

goal (1 subgoal):
 1. a \<in># B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in># B

goal (1 subgoal):
 1. P
[PROOF STEP]
with C mset_subset_eq_mono_add [of "{#a#}" "{#a#}" "{#b#}" "B-{#a#}"]
[PROOF STATE]
proof (chain)
picking this:
a \<notin># A
b \<in># B - {#a#}
\<lbrakk>{#a#} \<subseteq># {#a#}; {#b#} \<subseteq># B - {#a#}\<rbrakk> \<Longrightarrow> {#a#} + {#b#} \<subseteq># {#a#} + (B - {#a#})
a \<in># B
[PROOF STEP]
have "{#a, b#} \<subseteq># B"
[PROOF STATE]
proof (prove)
using this:
a \<notin># A
b \<in># B - {#a#}
\<lbrakk>{#a#} \<subseteq># {#a#}; {#b#} \<subseteq># B - {#a#}\<rbrakk> \<Longrightarrow> {#a#} + {#b#} \<subseteq># {#a#} + (B - {#a#})
a \<in># B

goal (1 subgoal):
 1. {#a, b#} \<subseteq># B
[PROOF STEP]
by (auto simp: add_mset_commute)
[PROOF STATE]
proof (state)
this:
{#a, b#} \<subseteq># B

goal (1 subgoal):
 1. P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<notin># A; b \<in># B - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># B

goal (1 subgoal):
 1. P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<notin># A; b \<in># B - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># B

goal (1 subgoal):
 1. P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<notin># A; b \<in># B - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># B

goal (1 subgoal):
 1. P
[PROOF STEP]
assume C: "a \<notin># A" "b \<notin># B - {#a#}"
[PROOF STATE]
proof (state)
this:
a \<notin># A
b \<notin># B - {#a#}

goal (1 subgoal):
 1. P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
{#a, b#} \<subseteq># A + B
a \<notin># A
b \<notin># B - {#a#}
[PROOF STEP]
have "a \<in># B \<and> b \<in># A"
[PROOF STATE]
proof (prove)
using this:
{#a, b#} \<subseteq># A + B
a \<notin># A
b \<notin># B - {#a#}

goal (1 subgoal):
 1. a \<in># B \<and> b \<in># A
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{#a, b#} \<subseteq># A + B; a \<notin># A; b \<notin># B - {#a#}\<rbrakk> \<Longrightarrow> a \<in># B
 2. \<lbrakk>{#a, b#} \<subseteq># A + B; a \<notin># A; b \<notin># B - {#a#}\<rbrakk> \<Longrightarrow> b \<in># A
[PROOF STEP]
apply (auto dest!: mset_subset_eq_insertD simp: insert_union_subset_iff; fail)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{#a, b#} \<subseteq># A + B; a \<notin># A; b \<notin># B - {#a#}\<rbrakk> \<Longrightarrow> b \<in># A
[PROOF STEP]
by (metis (no_types, lifting) B(1) add_mset_remove_trivial insert_DiffM2
            mset_diff_cancel1elem single_subset_iff subset_eq_diff_conv subset_mset.diff_diff_right
            union_single_eq_member)
[PROOF STATE]
proof (state)
this:
a \<in># B \<and> b \<in># A

goal (1 subgoal):
 1. P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<notin># A; b \<notin># B - {#a#}\<rbrakk> \<Longrightarrow> a \<in># B \<and> b \<in># A

goal (1 subgoal):
 1. P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<in># A; b \<in># A - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># A
\<lbrakk>a \<in># A; b \<notin># A - {#a#}\<rbrakk> \<Longrightarrow> b \<in># B
\<lbrakk>a \<notin># A; b \<in># B - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># B
\<lbrakk>a \<notin># A; b \<notin># B - {#a#}\<rbrakk> \<Longrightarrow> a \<in># B \<and> b \<in># A
[PROOF STEP]
show P
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<in># A; b \<in># A - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># A
\<lbrakk>a \<in># A; b \<notin># A - {#a#}\<rbrakk> \<Longrightarrow> b \<in># B
\<lbrakk>a \<notin># A; b \<in># B - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># B
\<lbrakk>a \<notin># A; b \<notin># B - {#a#}\<rbrakk> \<Longrightarrow> a \<in># B \<and> b \<in># A

goal (1 subgoal):
 1. P
[PROOF STEP]
using CASES
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<in># A; b \<in># A - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># A
\<lbrakk>a \<in># A; b \<notin># A - {#a#}\<rbrakk> \<Longrightarrow> b \<in># B
\<lbrakk>a \<notin># A; b \<in># B - {#a#}\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># B
\<lbrakk>a \<notin># A; b \<notin># B - {#a#}\<rbrakk> \<Longrightarrow> a \<in># B \<and> b \<in># A
{#a, b#} \<subseteq># A \<Longrightarrow> P
{#a, b#} \<subseteq># B \<Longrightarrow> P
\<lbrakk>a \<in># A; b \<in># B\<rbrakk> \<Longrightarrow> P
\<lbrakk>a \<in># B; b \<in># A\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_union_subset_s: "{#a#}+B \<subseteq># C \<Longrightarrow> a \<in># C \<and> B \<subseteq># C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#a#} + B \<subseteq># C \<Longrightarrow> a \<in># C \<and> B \<subseteq># C
[PROOF STEP]
by (drule mset_union_subset) simp


[STATEMENT]
lemma mset_le_single_cases[consumes 1, case_names empty singleton]: "\<lbrakk>M\<subseteq>#{#a#}; M={#} \<Longrightarrow> P; M={#a#} \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M \<subseteq># {#a#}; M = {#} \<Longrightarrow> P; M = {#a#} \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (induct M) auto


[STATEMENT]
lemma mset_le_mono_add_single: "\<lbrakk>a \<in># ys; b \<in># ws\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># ys + ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in># ys; b \<in># ws\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># ys + ws
[PROOF STEP]
using mset_subset_eq_mono_add[of "{#a#}" _ "{#b#}", simplified]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<in># ?B; b \<in># ?D\<rbrakk> \<Longrightarrow> {#b, a#} \<subseteq># ?B + ?D

goal (1 subgoal):
 1. \<lbrakk>a \<in># ys; b \<in># ws\<rbrakk> \<Longrightarrow> {#a, b#} \<subseteq># ys + ws
[PROOF STEP]
by (simp add: add_mset_commute)


[STATEMENT]
lemma mset_size1elem: "\<lbrakk>size P \<le> 1; q \<in># P\<rbrakk> \<Longrightarrow> P={#q#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size P \<le> 1; q \<in># P\<rbrakk> \<Longrightarrow> P = {#q#}
[PROOF STEP]
by (auto elim: mset_size_le1_cases)


[STATEMENT]
lemma mset_size2elem: "\<lbrakk>size P \<le> 2; {#q#}+{#q'#} \<subseteq># P\<rbrakk> \<Longrightarrow> P={#q#}+{#q'#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size P \<le> 2; {#q#} + {#q'#} \<subseteq># P\<rbrakk> \<Longrightarrow> P = {#q#} + {#q'#}
[PROOF STEP]
by (auto elim: mset_le_addE)


[STATEMENT]
lemma mset_map_single_rightE[consumes 1, case_names orig]: "\<lbrakk>f `# P = {#y#}; !!x. \<lbrakk> P={#x#}; f x = y \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f `# P = {#y#}; \<And>x. \<lbrakk>P = {#x#}; f x = y\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
by (cases P) auto


[STATEMENT]
lemma mset_map_split_orig: "!!M1 M2. \<lbrakk>f `# P = M1+M2; !!P1 P2. \<lbrakk>P=P1+P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M1 M2. \<lbrakk>f `# P = M1 + M2; \<And>P1 P2. \<lbrakk>P = P1 + P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
apply (induct P)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M1 M2. \<lbrakk>f `# {#} = M1 + M2; \<And>P1 P2. \<lbrakk>{#} = P1 + P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
 2. \<And>x P M1 M2. \<lbrakk>\<And>M1 M2. \<lbrakk>f `# P = M1 + M2; \<And>P1 P2. \<lbrakk>P = P1 + P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q; f `# add_mset x P = M1 + M2; \<And>P1 P2. \<lbrakk>add_mset x P = P1 + P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x P M1 M2. \<lbrakk>\<And>M1 M2. \<lbrakk>f `# P = M1 + M2; \<And>P1 P2. \<lbrakk>P = P1 + P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q; f `# add_mset x P = M1 + M2; \<And>P1 P2. \<lbrakk>add_mset x P = P1 + P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
apply (force elim!: mset_un_single_un_cases simp add: union_ac)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
(* TODO: This proof need's quite long. Try to write a faster one. *)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mset_map_id: "\<lbrakk>!!x. f (g x) = x\<rbrakk> \<Longrightarrow> f `# g `# X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f (g x) = x) \<Longrightarrow> f `# g `# X = X
[PROOF STEP]
by (induct X) auto


[STATEMENT]
lemma mset_map_split_orig_le: assumes A: "f `# P \<subseteq># M1+M2" and EX: "!!P1 P2. \<lbrakk>P=P1+P2; f `# P1 \<subseteq># M1; f `# P2 \<subseteq># M2\<rbrakk> \<Longrightarrow> Q" shows "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
using A EX
[PROOF STATE]
proof (prove)
using this:
f `# P \<subseteq># M1 + M2
\<lbrakk>P = ?P1.0 + ?P2.0; f `# ?P1.0 \<subseteq># M1; f `# ?P2.0 \<subseteq># M2\<rbrakk> \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by (auto elim: mset_le_distrib mset_map_split_orig)


[STATEMENT]
lemma list_rev_decomp[rule_format]: "l~=[] \<longrightarrow> (EX ll e . l = ll@[e])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> [] \<longrightarrow> (\<exists>ll e. l = ll @ [e])
[PROOF STEP]
apply(induct_tac l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [] \<noteq> [] \<longrightarrow> (\<exists>ll e. [] = ll @ [e])
 2. \<And>a list. list \<noteq> [] \<longrightarrow> (\<exists>ll e. list = ll @ [e]) \<Longrightarrow> a # list \<noteq> [] \<longrightarrow> (\<exists>ll e. a # list = ll @ [e])
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_compl_rev_induct[case_names Nil snoc]: "\<lbrakk>P []; !! l e . \<lbrakk>!! ll . length ll <= length l \<Longrightarrow> P ll\<rbrakk> \<Longrightarrow> P (l@[e])\<rbrakk> \<Longrightarrow> P l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P []; \<And>l e. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (l @ [e])\<rbrakk> \<Longrightarrow> P l
[PROOF STEP]
apply(induct_tac l rule: length_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>P []; \<And>l e. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (l @ [e]); \<forall>ys. length ys < length xs \<longrightarrow> P ys\<rbrakk> \<Longrightarrow> P xs
[PROOF STEP]
apply(case_tac "xs" rule: rev_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>P []; \<And>l e. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (l @ [e]); \<forall>ys. length ys < length xs \<longrightarrow> P ys; xs = []\<rbrakk> \<Longrightarrow> P xs
 2. \<And>xs ys y. \<lbrakk>P []; \<And>l e. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (l @ [e]); \<forall>ys. length ys < length xs \<longrightarrow> P ys; xs = ys @ [y]\<rbrakk> \<Longrightarrow> P xs
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_append_eq_Cons_cases: "\<lbrakk>ys@zs = x#xs; \<lbrakk>ys=[]; zs=x#xs\<rbrakk> \<Longrightarrow> P; !!ys'. \<lbrakk> ys=x#ys'; ys'@zs=xs \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys @ zs = x # xs; \<lbrakk>ys = []; zs = x # xs\<rbrakk> \<Longrightarrow> P; \<And>ys'. \<lbrakk>ys = x # ys'; ys' @ zs = xs\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto iff add: append_eq_Cons_conv)


[STATEMENT]
lemma list_Cons_eq_append_cases: "\<lbrakk>x#xs = ys@zs; \<lbrakk>ys=[]; zs=x#xs\<rbrakk> \<Longrightarrow> P; !!ys'. \<lbrakk> ys=x#ys'; ys'@zs=xs \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x # xs = ys @ zs; \<lbrakk>ys = []; zs = x # xs\<rbrakk> \<Longrightarrow> P; \<And>ys'. \<lbrakk>ys = x # ys'; ys' @ zs = xs\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto iff add: Cons_eq_append_conv)


[STATEMENT]
lemma foldl_A1_eq: "!!i. \<lbrakk> !! e. f n e = e; !! e. f e n = e; !!a b c. f a (f b c) = f (f a b) c \<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww)
[PROOF STEP]
proof (induct ww)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i [] = f i (foldl f n [])
 2. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f n ?e = ?e
f ?e n = ?e
f ?a (f ?b ?c) = f (f ?a ?b) ?c

goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i [] = f i (foldl f n [])
 2. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f n ?e = ?e
f ?e n = ?e
f ?a (f ?b ?c) = f (f ?a ?b) ?c

goal (1 subgoal):
 1. foldl f i [] = f i (foldl f n [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldl f i [] = f i (foldl f n [])

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
case (Cons a ww i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f ?i ww = f ?i (foldl f n ww)
f n ?e = ?e
f ?e n = ?e
f ?a (f ?b ?c) = f (f ?a ?b) ?c

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
note IHP[simplified]=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f ?i ww = f ?i (foldl f n ww)
f n ?e = ?e
f ?e n = ?e
f ?a (f ?b ?c) = f (f ?a ?b) ?c

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
have "foldl f i (a # ww) = foldl f (f i a) ww"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl f i (a # ww) = foldl f (f i a) ww
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldl f i (a # ww) = foldl f (f i a) ww

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldl f i (a # ww) = foldl f (f i a) ww

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
from IHP
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f ?i ww = f ?i (foldl f n ww)
f n ?e = ?e
f ?e n = ?e
f ?a (f ?b ?c) = f (f ?a ?b) ?c
[PROOF STEP]
have "\<dots> = f (f i a) (foldl f n ww)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f ?i ww = f ?i (foldl f n ww)
f n ?e = ?e
f ?e n = ?e
f ?a (f ?b ?c) = f (f ?a ?b) ?c

goal (1 subgoal):
 1. foldl f (f i a) ww = f (f i a) (foldl f n ww)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
foldl f (f i a) ww = f (f i a) (foldl f n ww)

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldl f (f i a) ww = f (f i a) (foldl f n ww)

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
from IHP(4)
[PROOF STATE]
proof (chain)
picking this:
f ?a (f ?b ?c) = f (f ?a ?b) ?c
[PROOF STEP]
have "\<dots> = f i (f a (foldl f n ww))"
[PROOF STATE]
proof (prove)
using this:
f ?a (f ?b ?c) = f (f ?a ?b) ?c

goal (1 subgoal):
 1. f (f i a) (foldl f n ww) = f i (f a (foldl f n ww))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (f i a) (foldl f n ww) = f i (f a (foldl f n ww))

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (f i a) (foldl f n ww) = f i (f a (foldl f n ww))

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
from IHP(1)[OF IHP(2,3,4), where i=a]
[PROOF STATE]
proof (chain)
picking this:
foldl f a ww = f a (foldl f n ww)
[PROOF STEP]
have "\<dots> = f i (foldl f a ww)"
[PROOF STATE]
proof (prove)
using this:
foldl f a ww = f a (foldl f n ww)

goal (1 subgoal):
 1. f i (f a (foldl f n ww)) = f i (foldl f a ww)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f i (f a (foldl f n ww)) = f i (foldl f a ww)

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f i (f a (foldl f n ww)) = f i (foldl f a ww)

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
from IHP(2)[of a]
[PROOF STATE]
proof (chain)
picking this:
f n a = a
[PROOF STEP]
have "\<dots> = f i (foldl f (f n a) ww)"
[PROOF STATE]
proof (prove)
using this:
f n a = a

goal (1 subgoal):
 1. f i (foldl f a ww) = f i (foldl f (f n a) ww)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f i (foldl f a ww) = f i (foldl f (f n a) ww)

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f i (foldl f a ww) = f i (foldl f (f n a) ww)

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
have "\<dots> = f i (foldl f n (a#ww))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i (foldl f (f n a) ww) = f i (foldl f n (a # ww))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f i (foldl f (f n a) ww) = f i (foldl f n (a # ww))

goal (1 subgoal):
 1. \<And>a ww i. \<lbrakk>\<And>i. \<lbrakk>\<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i ww = f i (foldl f n ww); \<And>e. f n e = e; \<And>e. f e n = e; \<And>a b c. f a (f b c) = f (f a b) c\<rbrakk> \<Longrightarrow> foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
foldl f i (a # ww) = f i (foldl f n (a # ww))

goal (1 subgoal):
 1. foldl f i (a # ww) = f i (foldl f n (a # ww))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
foldl f i (a # ww) = f i (foldl f n (a # ww))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_set: "foldl (\<union>) {} l = \<Union>{x. x\<in>set l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<union>) {} l = \<Union> {x. x \<in> set l}
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. foldl (\<union>) {} [] = \<Union> {x. x \<in> set []}
 2. \<And>a l. foldl (\<union>) {} l = \<Union> {x. x \<in> set l} \<Longrightarrow> foldl (\<union>) {} (a # l) = \<Union> {x. x \<in> set (a # l)}
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. foldl (\<union>) {} l = \<Union> (set l) \<Longrightarrow> foldl (\<union>) a l = \<Union> {x. x = a \<or> x \<in> set l}
[PROOF STEP]
apply (subst foldl_un_empty_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. foldl (\<union>) {} l = \<Union> (set l) \<Longrightarrow> a \<union> foldl (\<union>) {} l = \<Union> {x. x = a \<or> x \<in> set l}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_compl_induct[case_names Nil Cons]: "\<lbrakk>P []; !! e l . \<lbrakk>!! ll . length ll <= length l \<Longrightarrow> P ll\<rbrakk> \<Longrightarrow> P (e#l)\<rbrakk> \<Longrightarrow> P l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P []; \<And>e l. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (e # l)\<rbrakk> \<Longrightarrow> P l
[PROOF STEP]
apply(induct_tac l rule: length_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>P []; \<And>e l. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (e # l); \<forall>ys. length ys < length xs \<longrightarrow> P ys\<rbrakk> \<Longrightarrow> P xs
[PROOF STEP]
apply(case_tac "xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>P []; \<And>e l. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (e # l); \<forall>ys. length ys < length xs \<longrightarrow> P ys; xs = []\<rbrakk> \<Longrightarrow> P xs
 2. \<And>xs a list. \<lbrakk>P []; \<And>e l. (\<And>ll. length ll \<le> length l \<Longrightarrow> P ll) \<Longrightarrow> P (e # l); \<forall>ys. length ys < length xs \<longrightarrow> P ys; xs = a # list\<rbrakk> \<Longrightarrow> P xs
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_2pre_induct[case_names base left right]: assumes BASE: "P [] []" and LEFT: "!!e w1' w2. P w1' w2 \<Longrightarrow> P (e#w1') w2" and RIGHT: "!!e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e#w2')" shows "P w1 w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P w1 w2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P w1 w2
[PROOF STEP]
{ \<comment> \<open>The proof is done by induction over the sum of the lengths of the lists\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P w1 w2
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P w1 w2
[PROOF STEP]
have "!!w1 w2. \<lbrakk>length w1 + length w2 = n; P [] []; !!e w1' w2. P w1' w2 \<Longrightarrow> P (e#w1') w2; !!e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e#w2') \<rbrakk> \<Longrightarrow> P w1 w2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2. \<lbrakk>length w1 + length w2 = n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2. \<lbrakk>length w1 + length w2 = 0; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2
 2. \<And>n w1 w2. \<lbrakk>\<And>w1 w2. \<lbrakk>length w1 + length w2 = n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2; length w1 + length w2 = Suc n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n w1 w2. \<lbrakk>\<And>w1 w2. \<lbrakk>length w1 + length w2 = n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2; length w1 + length w2 = Suc n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2
[PROOF STEP]
apply (case_tac w1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n w1 w2. \<lbrakk>\<And>w1 w2. \<lbrakk>length w1 + length w2 = n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2; length w1 + length w2 = Suc n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2'); w1 = []\<rbrakk> \<Longrightarrow> P w1 w2
 2. \<And>n w1 w2 a list. \<lbrakk>\<And>w1 w2. \<lbrakk>length w1 + length w2 = n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P w1 w2; length w1 + length w2 = Suc n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2'); w1 = a # list\<rbrakk> \<Longrightarrow> P w1 w2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n w2. \<lbrakk>\<And>w1 w2. length w1 + length w2 = n \<Longrightarrow> P w1 w2; length w2 = Suc n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P [] w2
[PROOF STEP]
apply (case_tac w2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n w2. \<lbrakk>\<And>w1 w2. length w1 + length w2 = n \<Longrightarrow> P w1 w2; length w2 = Suc n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2'); w2 = []\<rbrakk> \<Longrightarrow> P [] w2
 2. \<And>n w2 a list. \<lbrakk>\<And>w1 w2. length w1 + length w2 = n \<Longrightarrow> P w1 w2; length w2 = Suc n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2'); w2 = a # list\<rbrakk> \<Longrightarrow> P [] w2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?w1.0 + length ?w2.0 = n; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P ?w1.0 ?w2.0

goal (1 subgoal):
 1. P w1 w2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?w1.0 + length ?w2.0 = ?n3; P [] []; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P (e # w1') w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 (e # w2')\<rbrakk> \<Longrightarrow> P ?w1.0 ?w2.0

goal (1 subgoal):
 1. P w1 w2
[PROOF STEP]
from this[OF _ BASE LEFT RIGHT]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length ?w1.0 + length ?w2.0 = ?n3; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P w1' w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 w2'\<rbrakk> \<Longrightarrow> P ?w1.0 ?w2.0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?w1.0 + length ?w2.0 = ?n3; \<And>e w1' w2. P w1' w2 \<Longrightarrow> P w1' w2; \<And>e w1 w2'. P w1 w2' \<Longrightarrow> P w1 w2'\<rbrakk> \<Longrightarrow> P ?w1.0 ?w2.0

goal (1 subgoal):
 1. P w1 w2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P w1 w2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_decomp_1: "length l=1 \<Longrightarrow> EX a . l=[a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l = 1 \<Longrightarrow> \<exists>a. l = [a]
[PROOF STEP]
by (case_tac l, auto)


[STATEMENT]
lemma list_decomp_2: "length l=2 \<Longrightarrow> EX a b . l=[a,b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l = 2 \<Longrightarrow> \<exists>a b. l = [a, b]
[PROOF STEP]
by (case_tac l, auto simp add: list_decomp_1)


[STATEMENT]
lemma drop_all_conc: "drop (length a) (a@b) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length a) (a @ b) = b
[PROOF STEP]
by (simp)


[STATEMENT]
lemma list_rest_coinc: "\<lbrakk>length s2 <= length s1; s1@r1 = s2@r2\<rbrakk> \<Longrightarrow> EX r1p . r2=r1p@r1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
assume A: "length s2 <= length s1" "s1@r1 = s2@r2"
[PROOF STATE]
proof (state)
this:
length s2 \<le> length s1
s1 @ r1 = s2 @ r2

goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
hence "r1 = drop (length s1) (s2@r2)"
[PROOF STATE]
proof (prove)
using this:
length s2 \<le> length s1
s1 @ r1 = s2 @ r2

goal (1 subgoal):
 1. r1 = drop (length s1) (s2 @ r2)
[PROOF STEP]
by (auto simp only:drop_all_conc dest: sym)
[PROOF STATE]
proof (state)
this:
r1 = drop (length s1) (s2 @ r2)

goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r1 = drop (length s1) (s2 @ r2)

goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
length s2 \<le> length s1
s1 @ r1 = s2 @ r2
[PROOF STEP]
have "length s1 = length s1 - length s2 + length s2"
[PROOF STATE]
proof (prove)
using this:
length s2 \<le> length s1
s1 @ r1 = s2 @ r2

goal (1 subgoal):
 1. length s1 = length s1 - length s2 + length s2
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
length s1 = length s1 - length s2 + length s2

goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r1 = drop (length s1) (s2 @ r2)
length s1 = length s1 - length s2 + length s2
[PROOF STEP]
have "r1 = drop ((length s1 - length s2)) r2"
[PROOF STATE]
proof (prove)
using this:
r1 = drop (length s1) (s2 @ r2)
length s1 = length s1 - length s2 + length s2

goal (1 subgoal):
 1. r1 = drop (length s1 - length s2) r2
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
r1 = drop (length s1 - length s2) r2

goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
hence "r2 = take ((length s1 - length s2)) r2 @ r1"
[PROOF STATE]
proof (prove)
using this:
r1 = drop (length s1 - length s2) r2

goal (1 subgoal):
 1. r2 = take (length s1 - length s2) r2 @ r1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r2 = take (length s1 - length s2) r2 @ r1

goal (1 subgoal):
 1. \<lbrakk>length s2 \<le> length s1; s1 @ r1 = s2 @ r2\<rbrakk> \<Longrightarrow> \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r2 = take (length s1 - length s2) r2 @ r1

goal (1 subgoal):
 1. \<exists>r1p. r2 = r1p @ r1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r1p. r2 = r1p @ r1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_tail_coinc: "n1#r1 = n2#r2 \<Longrightarrow> n1=n2 & r1=r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n1 # r1 = n2 # r2 \<Longrightarrow> n1 = n2 \<and> r1 = r2
[PROOF STEP]
by (auto)


[STATEMENT]
lemma last_in_set[intro]: "\<lbrakk>l\<noteq>[]\<rbrakk> \<Longrightarrow> last l \<in> set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> last l \<in> set l
[PROOF STEP]
by (induct l) auto


[STATEMENT]
lemma nat_compl_induct[case_names 0 Suc]: "\<lbrakk>P 0; !! n . ALL nn . nn <= n \<longrightarrow> P nn \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P 0; \<And>n. \<forall>nn\<le>n. P nn \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply(induct_tac n rule: nat_less_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>P 0; \<And>n. \<forall>nn\<le>n. P nn \<Longrightarrow> P (Suc n); \<forall>m<n. P m\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply(case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>P 0; \<And>n. \<forall>nn\<le>n. P nn \<Longrightarrow> P (Suc n); \<forall>m<n. P m; n = 0\<rbrakk> \<Longrightarrow> P n
 2. \<And>n nat. \<lbrakk>P 0; \<And>n. \<forall>nn\<le>n. P nn \<Longrightarrow> P (Suc n); \<forall>m<n. P m; n = Suc nat\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma boolfun_cases_helper: "g=(\<lambda>x. False) | g=(\<lambda>x. x) | g=(\<lambda>x. True) | g= (\<lambda>x. \<not>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
assume "g False" "g True"
[PROOF STATE]
proof (state)
this:
g False
g True

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
hence "g = (\<lambda>x. True)"
[PROOF STATE]
proof (prove)
using this:
g False
g True

goal (1 subgoal):
 1. g = (\<lambda>x. True)
[PROOF STEP]
by (rule_tac ext, case_tac x, auto)
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. True)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. True)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. True)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. True)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
assume "g False" "\<not>g True"
[PROOF STATE]
proof (state)
this:
g False
\<not> g True

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
hence "g = (\<lambda>x. \<not>x)"
[PROOF STATE]
proof (prove)
using this:
g False
\<not> g True

goal (1 subgoal):
 1. g = Not
[PROOF STEP]
by (rule_tac ext, case_tac x, auto)
[PROOF STATE]
proof (state)
this:
g = Not

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>g False; \<not> g True\<rbrakk> \<Longrightarrow> g = Not

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>g False; \<not> g True\<rbrakk> \<Longrightarrow> g = Not

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>g False; \<not> g True\<rbrakk> \<Longrightarrow> g = Not

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
assume "\<not>g False" "g True"
[PROOF STATE]
proof (state)
this:
\<not> g False
g True

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
hence "g = (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
using this:
\<not> g False
g True

goal (1 subgoal):
 1. g = (\<lambda>x. x)
[PROOF STEP]
by (rule_tac ext, case_tac x, auto)
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. x)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. x)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. x)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. x)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
assume "\<not>g False" "\<not>g True"
[PROOF STATE]
proof (state)
this:
\<not> g False
\<not> g True

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
hence "g = (\<lambda>x. False)"
[PROOF STATE]
proof (prove)
using this:
\<not> g False
\<not> g True

goal (1 subgoal):
 1. g = (\<lambda>x. False)
[PROOF STEP]
by (rule_tac ext, case_tac x, auto)
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. False)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> g False; \<not> g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. False)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. True)
\<lbrakk>g False; \<not> g True\<rbrakk> \<Longrightarrow> g = Not
\<lbrakk>\<not> g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. x)
\<lbrakk>\<not> g False; \<not> g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. False)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. True)
\<lbrakk>g False; \<not> g True\<rbrakk> \<Longrightarrow> g = Not
\<lbrakk>\<not> g False; g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. x)
\<lbrakk>\<not> g False; \<not> g True\<rbrakk> \<Longrightarrow> g = (\<lambda>x. False)

goal (1 subgoal):
 1. g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma boolfun_cases[case_names False Id True Neg]: "\<lbrakk>g=(\<lambda>x. False) \<Longrightarrow> P g; g=(\<lambda>x. x) \<Longrightarrow> P g; g=(\<lambda>x. True) \<Longrightarrow> P g; g=(\<lambda>x. \<not>x) \<Longrightarrow> P g\<rbrakk> \<Longrightarrow> P g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g = (\<lambda>x. False) \<Longrightarrow> P g; g = (\<lambda>x. x) \<Longrightarrow> P g; g = (\<lambda>x. True) \<Longrightarrow> P g; g = Not \<Longrightarrow> P g\<rbrakk> \<Longrightarrow> P g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>g = (\<lambda>x. False) \<Longrightarrow> P g; g = (\<lambda>x. x) \<Longrightarrow> P g; g = (\<lambda>x. True) \<Longrightarrow> P g; g = Not \<Longrightarrow> P g\<rbrakk> \<Longrightarrow> P g
[PROOF STEP]
note boolfun_cases_helper[of g]
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not

goal (1 subgoal):
 1. \<lbrakk>g = (\<lambda>x. False) \<Longrightarrow> P g; g = (\<lambda>x. x) \<Longrightarrow> P g; g = (\<lambda>x. True) \<Longrightarrow> P g; g = Not \<Longrightarrow> P g\<rbrakk> \<Longrightarrow> P g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not

goal (1 subgoal):
 1. \<lbrakk>g = (\<lambda>x. False) \<Longrightarrow> P g; g = (\<lambda>x. x) \<Longrightarrow> P g; g = (\<lambda>x. True) \<Longrightarrow> P g; g = Not \<Longrightarrow> P g\<rbrakk> \<Longrightarrow> P g
[PROOF STEP]
assume "g=(\<lambda>x. False) \<Longrightarrow> P g" "g=(\<lambda>x. x) \<Longrightarrow> P g" "g=(\<lambda>x. True) \<Longrightarrow> P g" "g=(\<lambda>x. \<not>x) \<Longrightarrow> P g"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. False) \<Longrightarrow> P g
g = (\<lambda>x. x) \<Longrightarrow> P g
g = (\<lambda>x. True) \<Longrightarrow> P g
g = Not \<Longrightarrow> P g

goal (1 subgoal):
 1. \<lbrakk>g = (\<lambda>x. False) \<Longrightarrow> P g; g = (\<lambda>x. x) \<Longrightarrow> P g; g = (\<lambda>x. True) \<Longrightarrow> P g; g = Not \<Longrightarrow> P g\<rbrakk> \<Longrightarrow> P g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
g = (\<lambda>x. False) \<Longrightarrow> P g
g = (\<lambda>x. x) \<Longrightarrow> P g
g = (\<lambda>x. True) \<Longrightarrow> P g
g = Not \<Longrightarrow> P g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g = (\<lambda>x. False) \<or> g = (\<lambda>x. x) \<or> g = (\<lambda>x. True) \<or> g = Not
g = (\<lambda>x. False) \<Longrightarrow> P g
g = (\<lambda>x. x) \<Longrightarrow> P g
g = (\<lambda>x. True) \<Longrightarrow> P g
g = Not \<Longrightarrow> P g

goal (1 subgoal):
 1. P g
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
P g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma some_theI: assumes EX: "\<exists>a b . P a b" and BUN: "!! b1 b2 . \<lbrakk>\<exists>a . P a b1; \<exists>a . P a b2\<rbrakk> \<Longrightarrow> b1=b2"
    shows "P (SOME a . \<exists>b . P a b) (THE b . \<exists>a . P a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
from EX
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. P a b
[PROOF STEP]
have "EX b . P (SOME a . EX b . P a b) b"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. P a b

goal (1 subgoal):
 1. \<exists>b. P (SOME a. \<exists>b. P a b) b
[PROOF STEP]
by (rule someI_ex)
[PROOF STATE]
proof (state)
this:
\<exists>b. P (SOME a. \<exists>b. P a b) b

goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>b. P (SOME a. \<exists>b. P a b) b

goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
from EX
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. P a b
[PROOF STEP]
have "EX b . EX a . P a b"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. P a b

goal (1 subgoal):
 1. \<exists>b a. P a b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b a. P a b

goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
with BUN theI'[of "\<lambda>b . EX a . P a b"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>a. P a ?b1.0; \<exists>a. P a ?b2.0\<rbrakk> \<Longrightarrow> ?b1.0 = ?b2.0
\<exists>!x. \<exists>a. P a x \<Longrightarrow> \<exists>a. P a (THE x. \<exists>a. P a x)
\<exists>b a. P a b
[PROOF STEP]
have "EX a . P a (THE b . EX a . P a b)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>a. P a ?b1.0; \<exists>a. P a ?b2.0\<rbrakk> \<Longrightarrow> ?b1.0 = ?b2.0
\<exists>!x. \<exists>a. P a x \<Longrightarrow> \<exists>a. P a (THE x. \<exists>a. P a x)
\<exists>b a. P a b

goal (1 subgoal):
 1. \<exists>a. P a (THE b. \<exists>a. P a b)
[PROOF STEP]
by (unfold Ex1_def, blast)
[PROOF STATE]
proof (state)
this:
\<exists>a. P a (THE b. \<exists>a. P a b)

goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>a. P a (THE b. \<exists>a. P a b)

goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
note BUN
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>a. P a ?b1.0; \<exists>a. P a ?b2.0\<rbrakk> \<Longrightarrow> ?b1.0 = ?b2.0

goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>b. P (SOME a. \<exists>b. P a b) b
\<exists>a. P a (THE b. \<exists>a. P a b)
\<lbrakk>\<exists>a. P a ?b1.0; \<exists>a. P a ?b2.0\<rbrakk> \<Longrightarrow> ?b1.0 = ?b2.0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>b. P (SOME a. \<exists>b. P a b) b
\<exists>a. P a (THE b. \<exists>a. P a b)
\<lbrakk>\<exists>a. P a ?b1.0; \<exists>a. P a ?b2.0\<rbrakk> \<Longrightarrow> ?b1.0 = ?b2.0

goal (1 subgoal):
 1. P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)
[PROOF STEP]
by (fast)
[PROOF STATE]
proof (state)
this:
P (SOME a. \<exists>b. P a b) (THE b. \<exists>a. P a b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_M_is_l_get_M: "l_get_M get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t type_wf object_ptr_kinds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_get_M get type_wf object_ptr_kinds
[PROOF STEP]
by (simp add: a_type_wf_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf l_get_M_def)


[STATEMENT]
lemma object_ptr_kinds_M_reads:
  "reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) object_ptr_kinds_M h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reads (\<Union>object_ptr. {preserved (get_M object_ptr nothing)}) object_ptr_kinds_M h h'
[PROOF STEP]
apply(auto simp add: object_ptr_kinds_M_defs get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf type_wf_defs reads_def
      preserved_def get_M_defs
      split: option.splits)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>y. (get y h = None \<longrightarrow> get y h' = None) \<and> ((\<exists>x2. get y h = Some x2) \<longrightarrow> (\<exists>ya. get y h' = Some ya)); get x h' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. get x h = Some y
 2. \<And>x y. \<lbrakk>\<forall>y. (get y h = None \<longrightarrow> get y h' = None) \<and> ((\<exists>x2. get y h = Some x2) \<longrightarrow> (\<exists>ya. get y h' = Some ya)); get x h' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. get x h = Some y
[PROOF STEP]
using a_type_wf_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf
[PROOF STATE]
proof (prove)
using this:
type_wf ?h = True
type_wf ?h \<Longrightarrow> (?object_ptr |\<in>| object_ptr_kinds ?h) = (get ?object_ptr ?h \<noteq> None)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>y. (get y h = None \<longrightarrow> get y h' = None) \<and> ((\<exists>x2. get y h = Some x2) \<longrightarrow> (\<exists>ya. get y h' = Some ya)); get x h' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. get x h = Some y
 2. \<And>x y. \<lbrakk>\<forall>y. (get y h = None \<longrightarrow> get y h' = None) \<and> ((\<exists>x2. get y h = Some x2) \<longrightarrow> (\<exists>ya. get y h' = Some ya)); get x h' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. get x h = Some y
[PROOF STEP]
by blast+


[STATEMENT]
lemma check_in_heap_ptr_in_heap: "ptr |\<in>| object_ptr_kinds h \<longleftrightarrow> h \<turnstile> ok (check_in_heap ptr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ptr |\<in>| object_ptr_kinds h) = h \<turnstile> ok check_in_heap ptr
[PROOF STEP]
by(auto simp add: check_in_heap_def)


[STATEMENT]
lemma check_in_heap_pure [simp]: "pure (check_in_heap ptr) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure (check_in_heap ptr) h
[PROOF STEP]
by(auto simp add: check_in_heap_def intro!: bind_pure_I)


[STATEMENT]
lemma check_in_heap_is_OK [simp]:
  "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (check_in_heap ptr \<bind> f) = h \<turnstile> ok (f ())"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (check_in_heap ptr \<bind> f) = h \<turnstile> ok f ()
[PROOF STEP]
by(simp add: check_in_heap_def)


[STATEMENT]
lemma check_in_heap_returns_result [simp]:
  "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> (check_in_heap ptr \<bind> f) \<rightarrow>\<^sub>r x = h \<turnstile> f () \<rightarrow>\<^sub>r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> check_in_heap ptr \<bind> f \<rightarrow>\<^sub>r x = h \<turnstile> f () \<rightarrow>\<^sub>r x
[PROOF STEP]
by(simp add: check_in_heap_def)


[STATEMENT]
lemma check_in_heap_returns_heap [simp]:
  "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> (check_in_heap ptr \<bind> f) \<rightarrow>\<^sub>h h' = h \<turnstile> f () \<rightarrow>\<^sub>h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptr |\<in>| object_ptr_kinds h \<Longrightarrow> h \<turnstile> check_in_heap ptr \<bind> f \<rightarrow>\<^sub>h h' = h \<turnstile> f () \<rightarrow>\<^sub>h h'
[PROOF STEP]
by(simp add: check_in_heap_def)


[STATEMENT]
lemma check_in_heap_reads:
  "reads {preserved (get_M object_ptr nothing)} (check_in_heap object_ptr) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reads {preserved (get_M object_ptr nothing)} (check_in_heap object_ptr) h h'
[PROOF STEP]
apply(simp add: check_in_heap_def reads_def preserved_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (object_ptr |\<in>| object_ptr_kinds h \<longrightarrow> object_ptr |\<notin>| object_ptr_kinds h' \<longrightarrow> h \<turnstile> get_M object_ptr nothing \<rightarrow>\<^sub>r () = (\<not> h' \<turnstile> get_M object_ptr nothing \<rightarrow>\<^sub>r ())) \<and> (object_ptr |\<notin>| object_ptr_kinds h \<longrightarrow> object_ptr |\<in>| object_ptr_kinds h' \<longrightarrow> h \<turnstile> get_M object_ptr nothing \<rightarrow>\<^sub>r () = (\<not> h' \<turnstile> get_M object_ptr nothing \<rightarrow>\<^sub>r ()))
[PROOF STEP]
by (metis a_type_wf_def get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ok get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ptr_in_heap is_OK_returns_result_E
      is_OK_returns_result_I unit_all_impI)


[STATEMENT]
lemma invoke_split: "P (invoke ((Pred, f) # xs) ptr args) =
    ((\<not>(Pred ptr) \<longrightarrow> P (invoke xs ptr args))
  \<and> (Pred ptr \<longrightarrow> P (do {check_in_heap ptr; f ptr args})))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (invoke ((Pred, f) # xs) ptr args) = ((\<not> Pred ptr \<longrightarrow> P (invoke xs ptr args)) \<and> (Pred ptr \<longrightarrow> P (check_in_heap ptr \<bind> (\<lambda>_. f ptr args))))
[PROOF STEP]
by(simp add: invoke_def)


[STATEMENT]
lemma invoke_split_asm: "P (invoke ((Pred, f) # xs) ptr args) =
    (\<not>((\<not>(Pred ptr) \<and> (\<not> P (invoke xs ptr args)))
    \<or> (Pred ptr \<and> (\<not> P (do {check_in_heap ptr; f ptr args})))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (invoke ((Pred, f) # xs) ptr args) = (\<not> (\<not> Pred ptr \<and> \<not> P (invoke xs ptr args) \<or> Pred ptr \<and> \<not> P (check_in_heap ptr \<bind> (\<lambda>_. f ptr args))))
[PROOF STEP]
by(simp add: invoke_def)


[STATEMENT]
lemma invoke_ptr_in_heap: "h \<turnstile> ok (invoke xs ptr args) \<Longrightarrow> ptr |\<in>| object_ptr_kinds h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> ok invoke xs ptr args \<Longrightarrow> ptr |\<in>| object_ptr_kinds h
[PROOF STEP]
by (metis bind_is_OK_E check_in_heap_ptr_in_heap invoke_def is_OK_returns_heap_I)


[STATEMENT]
lemma invoke_pure [simp]: "pure (invoke [] ptr args) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure (invoke [] ptr args) h
[PROOF STEP]
by(auto simp add: invoke_def intro!: bind_pure_I)


[STATEMENT]
lemma invoke_is_OK [simp]:
  "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> Pred ptr
    \<Longrightarrow> h \<turnstile> ok (invoke ((Pred, f) # xs) ptr args) = h \<turnstile> ok (f ptr args)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr |\<in>| object_ptr_kinds h; Pred ptr\<rbrakk> \<Longrightarrow> h \<turnstile> ok invoke ((Pred, f) # xs) ptr args = h \<turnstile> ok f ptr args
[PROOF STEP]
by(simp add: invoke_def)


[STATEMENT]
lemma invoke_returns_result [simp]:
  "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> Pred ptr
   \<Longrightarrow> h \<turnstile> (invoke ((Pred, f) # xs) ptr args) \<rightarrow>\<^sub>r x = h \<turnstile> f ptr args \<rightarrow>\<^sub>r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr |\<in>| object_ptr_kinds h; Pred ptr\<rbrakk> \<Longrightarrow> h \<turnstile> invoke ((Pred, f) # xs) ptr args \<rightarrow>\<^sub>r x = h \<turnstile> f ptr args \<rightarrow>\<^sub>r x
[PROOF STEP]
by(simp add: invoke_def)


[STATEMENT]
lemma invoke_returns_heap [simp]:
  "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> Pred ptr
   \<Longrightarrow> h \<turnstile> (invoke ((Pred, f) # xs) ptr args) \<rightarrow>\<^sub>h h' = h \<turnstile> f ptr args \<rightarrow>\<^sub>h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr |\<in>| object_ptr_kinds h; Pred ptr\<rbrakk> \<Longrightarrow> h \<turnstile> invoke ((Pred, f) # xs) ptr args \<rightarrow>\<^sub>h h' = h \<turnstile> f ptr args \<rightarrow>\<^sub>h h'
[PROOF STEP]
by(simp add: invoke_def)


[STATEMENT]
lemma invoke_not [simp]: "\<not>Pred ptr \<Longrightarrow> invoke ((Pred, f) # xs) ptr args = invoke xs ptr args"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Pred ptr \<Longrightarrow> invoke ((Pred, f) # xs) ptr args = invoke xs ptr args
[PROOF STEP]
by(auto simp add: invoke_def)


[STATEMENT]
lemma invoke_empty [simp]: "\<not>h \<turnstile> ok (invoke [] ptr args)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> h \<turnstile> ok invoke [] ptr args
[PROOF STEP]
by(auto simp add: invoke_def check_in_heap_def)


[STATEMENT]
lemma invoke_empty_reads [simp]: "\<forall>P \<in> S. reflp P \<and> transp P \<Longrightarrow> reads S (invoke [] ptr args) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>S. reflp P \<and> transp P \<Longrightarrow> reads S (invoke [] ptr args) h h'
[PROOF STEP]
apply(simp add: invoke_def reads_def preserved_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>S. reflp P \<and> transp P \<Longrightarrow> (\<forall>P\<in>S. P h h') \<longrightarrow> (\<forall>x. h \<turnstile> check_in_heap ptr \<bind> (\<lambda>_. error InvokeError) \<rightarrow>\<^sub>r x = h' \<turnstile> check_in_heap ptr \<bind> (\<lambda>_. error InvokeError) \<rightarrow>\<^sub>r x)
[PROOF STEP]
by (meson bind_returns_result_E error_returns_result)


[STATEMENT]
lemma get_object_ptr_simp [simp]:
  "get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = (if ptr = object_ptr then Some obj else get object_ptr h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get object_ptr (put ptr obj h) = (if ptr = object_ptr then Some obj else get object_ptr h)
[PROOF STEP]
by(auto simp add: get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: option.splits Option.bind_splits)


[STATEMENT]
lemma object_ptr_kinds_simp [simp]: "object_ptr_kinds (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = object_ptr_kinds h |\<union>| {|ptr|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr_kinds (put ptr obj h) = object_ptr_kinds h |\<union>| {|ptr|}
[PROOF STEP]
by(auto simp add: object_ptr_kinds_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: option.splits)


[STATEMENT]
lemma type_wf_put_I:
  assumes "type_wf h"
  shows "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf (put ptr obj h)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
type_wf h

goal (1 subgoal):
 1. type_wf (put ptr obj h)
[PROOF STEP]
by(auto simp add: type_wf_defs split: option.splits)


[STATEMENT]
lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "ptr |\<notin>| object_ptr_kinds h"
  shows "type_wf h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
type_wf (put ptr obj h)
ptr |\<notin>| object_ptr_kinds h

goal (1 subgoal):
 1. type_wf h
[PROOF STEP]
by(auto simp add: type_wf_defs split: option.splits if_splits)


[STATEMENT]
lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "ptr |\<in>| object_ptr_kinds h"
  shows "type_wf h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
type_wf (put ptr obj h)
ptr |\<in>| object_ptr_kinds h

goal (1 subgoal):
 1. type_wf h
[PROOF STEP]
by(auto simp add: type_wf_defs split: option.splits if_splits)


[STATEMENT]
lemma type_wf_preserved: "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
by(auto simp add: type_wf_defs)


[STATEMENT]
lemma object_ptr_kinds_preserved_small:
  assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
preserved (get_M ?object_ptr nothing) h h'

goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
apply(auto simp add: object_ptr_kinds_def preserved_def get_M_defs get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
      split: option.splits)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>object_ptr. h \<turnstile> (case fmlookup (the_heap h) object_ptr of None \<Rightarrow> error SegmentationFault | Some res \<Rightarrow> return (nothing res)) \<rightarrow>\<^sub>r () = h' \<turnstile> (case fmlookup (the_heap h') object_ptr of None \<Rightarrow> error SegmentationFault | Some res \<Rightarrow> return (nothing res)) \<rightarrow>\<^sub>r (); x |\<in>| fmdom (the_heap h)\<rbrakk> \<Longrightarrow> x |\<in>| fmdom (the_heap h')
 2. \<And>x. \<lbrakk>\<And>object_ptr. h \<turnstile> (case fmlookup (the_heap h) object_ptr of None \<Rightarrow> error SegmentationFault | Some res \<Rightarrow> return (nothing res)) \<rightarrow>\<^sub>r () = h' \<turnstile> (case fmlookup (the_heap h') object_ptr of None \<Rightarrow> error SegmentationFault | Some res \<Rightarrow> return (nothing res)) \<rightarrow>\<^sub>r (); x |\<in>| fmdom (the_heap h')\<rbrakk> \<Longrightarrow> x |\<in>| fmdom (the_heap h)
[PROOF STEP]
apply (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq fmember.rep_eq
      old.unit.exhaust option.case_eq_if return_returns_result)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>object_ptr. h \<turnstile> (case fmlookup (the_heap h) object_ptr of None \<Rightarrow> error SegmentationFault | Some res \<Rightarrow> return (nothing res)) \<rightarrow>\<^sub>r () = h' \<turnstile> (case fmlookup (the_heap h') object_ptr of None \<Rightarrow> error SegmentationFault | Some res \<Rightarrow> return (nothing res)) \<rightarrow>\<^sub>r (); x |\<in>| fmdom (the_heap h')\<rbrakk> \<Longrightarrow> x |\<in>| fmdom (the_heap h)
[PROOF STEP]
by (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq fmember.rep_eq
      old.unit.exhaust option.case_eq_if return_returns_result)


[STATEMENT]
lemma object_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
  assumes "\<And>h h' w object_ptr. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h'
          \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
fix object_ptr w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
have "preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preserved (get_M object_ptr nothing) h h'
[PROOF STEP]
apply(rule writes_small_big[OF assms])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> ?w1 h h' w \<in> SW
 2. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h \<turnstile> ?w1 h h' w \<rightarrow>\<^sub>h h'
 3. reflp (preserved (get_M object_ptr nothing))
 4. transp (preserved (get_M object_ptr nothing))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
preserved (get_M object_ptr nothing) h h'

goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
preserved (get_M ?object_ptr2 nothing) h h'

goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
preserved (get_M ?object_ptr2 nothing) h h'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
preserved (get_M ?object_ptr2 nothing) h h'

goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
using object_ptr_kinds_preserved_small
[PROOF STATE]
proof (prove)
using this:
preserved (get_M ?object_ptr2 nothing) h h'
(\<And>object_ptr. preserved (get_M object_ptr nothing) ?h ?h') \<Longrightarrow> object_ptr_kinds ?h = object_ptr_kinds ?h'

goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
object_ptr_kinds h = object_ptr_kinds h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reads_writes_preserved2:
  assumes "writes SW setter h h'"
  assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
  assumes "\<And>h h' x. \<forall>w \<in> SW. h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h'"
  shows "preserved (get_M ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preserved (get_M ptr getter) h h'
[PROOF STEP]
apply(clarsimp simp add: preserved_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. h \<turnstile> get_M ptr getter \<rightarrow>\<^sub>r x = h' \<turnstile> get_M ptr getter \<rightarrow>\<^sub>r x
[PROOF STEP]
using reads_singleton assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
reads {preserved ?f} ?f ?h ?h'
writes SW setter h h'
h \<turnstile> setter \<rightarrow>\<^sub>h h'

goal (1 subgoal):
 1. \<And>x. h \<turnstile> get_M ptr getter \<rightarrow>\<^sub>r x = h' \<turnstile> get_M ptr getter \<rightarrow>\<^sub>r x
[PROOF STEP]
apply(rule reads_writes_preserved)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h h'. \<forall>w\<in>SW. h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r\<in>{preserved (get_M ptr getter)}. r h h')
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>SW. ?h \<turnstile> w \<rightarrow>\<^sub>h ?h' \<longrightarrow> preserved (get_M ptr getter) ?h ?h'

goal (1 subgoal):
 1. \<And>x h h'. \<forall>w\<in>SW. h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r\<in>{preserved (get_M ptr getter)}. r h h')
[PROOF STEP]
by(auto simp add: preserved_def)


[STATEMENT]
lemma viette2_monic:
  fixes b c \<xi>1 \<xi>2 :: real
  assumes "b\<^sup>2 - 4*c \<ge> 0" and "\<xi>1\<^sup>2 + b*\<xi>1 + c = 0" and "\<xi>2\<^sup>2 + b*\<xi>2 + c = 0" and "\<xi>1 \<noteq> \<xi>2"
  shows "\<xi>1*\<xi>2 = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>1 * \<xi>2 = c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> b\<^sup>2 - 4 * c
\<xi>1\<^sup>2 + b * \<xi>1 + c = 0
\<xi>2\<^sup>2 + b * \<xi>2 + c = 0
\<xi>1 \<noteq> \<xi>2

goal (1 subgoal):
 1. \<xi>1 * \<xi>2 = c
[PROOF STEP]
by algebra


[STATEMENT]
lemma viette2:
  fixes a b c \<xi>1 \<xi>2 :: real
  assumes "a \<noteq> 0" and "b\<^sup>2 - 4*a*c \<ge> 0" and "a*\<xi>1\<^sup>2 + b*\<xi>1 + c = 0" and "a*\<xi>2\<^sup>2 + b*\<xi>2 + c = 0" and "\<xi>1 \<noteq> \<xi>2"
  shows "\<xi>1*\<xi>2 = c/a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>1 * \<xi>2 = c / a
[PROOF STEP]
proof (rule viette2_monic[of "b/a" "c/a" \<xi>1 \<xi>2])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. 0 \<le> (b / a)\<^sup>2 - 4 * (c / a)
 2. \<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0
 3. \<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0
 4. \<xi>1 \<noteq> \<xi>2
[PROOF STEP]
have "(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4*a*c) / a\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2
[PROOF STEP]
using \<open>a \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2
[PROOF STEP]
by (auto simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2

goal (4 subgoals):
 1. 0 \<le> (b / a)\<^sup>2 - 4 * (c / a)
 2. \<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0
 3. \<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0
 4. \<xi>1 \<noteq> \<xi>2
[PROOF STEP]
thus "0 \<le> (b / a)\<^sup>2 - 4 * (c / a)"
[PROOF STATE]
proof (prove)
using this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2

goal (1 subgoal):
 1. 0 \<le> (b / a)\<^sup>2 - 4 * (c / a)
[PROOF STEP]
using \<open>b\<^sup>2 - 4*a*c \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2
0 \<le> b\<^sup>2 - 4 * a * c

goal (1 subgoal):
 1. 0 \<le> (b / a)\<^sup>2 - 4 * (c / a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> (b / a)\<^sup>2 - 4 * (c / a)

goal (3 subgoals):
 1. \<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0
 2. \<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0
 3. \<xi>1 \<noteq> \<xi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0
 2. \<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0
 3. \<xi>1 \<noteq> \<xi>2
[PROOF STEP]
show "\<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0" "\<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0 &&& \<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
0 \<le> b\<^sup>2 - 4 * a * c
a * \<xi>1\<^sup>2 + b * \<xi>1 + c = 0
a * \<xi>2\<^sup>2 + b * \<xi>2 + c = 0
\<xi>1 \<noteq> \<xi>2

goal (1 subgoal):
 1. \<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0 &&& \<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0
[PROOF STEP]
by (auto simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
\<xi>1\<^sup>2 + b / a * \<xi>1 + c / a = 0
\<xi>2\<^sup>2 + b / a * \<xi>2 + c / a = 0

goal (1 subgoal):
 1. \<xi>1 \<noteq> \<xi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<xi>1 \<noteq> \<xi>2
[PROOF STEP]
show "\<xi>1 \<noteq> \<xi>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>1 \<noteq> \<xi>2
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<xi>1 \<noteq> \<xi>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma viette2'_monic:
  fixes b c \<xi> :: real
  assumes "b\<^sup>2 - 4*c = 0" and "\<xi>\<^sup>2 + b*\<xi> + c = 0"
  shows "\<xi>*\<xi> = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi> * \<xi> = c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b\<^sup>2 - 4 * c = 0
\<xi>\<^sup>2 + b * \<xi> + c = 0

goal (1 subgoal):
 1. \<xi> * \<xi> = c
[PROOF STEP]
by algebra


[STATEMENT]
lemma viette2':
  fixes a b c \<xi> :: real
  assumes "a \<noteq> 0" and "b\<^sup>2 - 4*a*c = 0" and "a*\<xi>\<^sup>2 + b*\<xi> + c = 0"
  shows "\<xi>*\<xi> = c/a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi> * \<xi> = c / a
[PROOF STEP]
proof (rule viette2'_monic)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?b\<^sup>2 - 4 * (c / a) = 0
 2. \<xi>\<^sup>2 + ?b * \<xi> + c / a = 0
[PROOF STEP]
have "(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4*a*c) / a\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2
[PROOF STEP]
using \<open>a \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2
[PROOF STEP]
by (auto simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2

goal (2 subgoals):
 1. ?b\<^sup>2 - 4 * (c / a) = 0
 2. \<xi>\<^sup>2 + ?b * \<xi> + c / a = 0
[PROOF STEP]
thus "(b / a)\<^sup>2 - 4 * (c / a) = 0"
[PROOF STATE]
proof (prove)
using this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2

goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = 0
[PROOF STEP]
using \<open>b\<^sup>2 - 4*a*c = 0\<close>
[PROOF STATE]
proof (prove)
using this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) / a\<^sup>2
b\<^sup>2 - 4 * a * c = 0

goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(b / a)\<^sup>2 - 4 * (c / a) = 0

goal (1 subgoal):
 1. \<xi>\<^sup>2 + b / a * \<xi> + c / a = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<xi>\<^sup>2 + b / a * \<xi> + c / a = 0
[PROOF STEP]
show "\<xi>\<^sup>2 + b / a * \<xi> + c / a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>\<^sup>2 + b / a * \<xi> + c / a = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
b\<^sup>2 - 4 * a * c = 0
a * \<xi>\<^sup>2 + b * \<xi> + c = 0

goal (1 subgoal):
 1. \<xi>\<^sup>2 + b / a * \<xi> + c / a = 0
[PROOF STEP]
by (auto simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
\<xi>\<^sup>2 + b / a * \<xi> + c / a = 0

goal:
No subgoals!
[PROOF STEP]
qed