[STATEMENT]
lemma reachable_trace:
      assumes "q \<in> reachable p" "run r q"
      shows "sset (trace r q) \<subseteq> reachable p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (trace r q) \<subseteq> reachable p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> reachable p
run r q

goal (1 subgoal):
 1. sset (trace r q) \<subseteq> reachable p
[PROOF STEP]
unfolding sset_subset_stream_pred
[PROOF STATE]
proof (prove)
using this:
q \<in> reachable p
run r q

goal (1 subgoal):
 1. pred_stream (\<lambda>a. a \<in> reachable p) (trace r q)
[PROOF STEP]
by (coinduction arbitrary: r q) (force elim: run.cases)


[STATEMENT]
lemma valid_empty:
  "valid_mask empty_mask"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask empty_mask
[PROOF STEP]
by (metis empty_mask.simps le_add_same_cancel1 p_greater_exists padd.rep_eq pgte.rep_eq pnone.rep_eq valid_mask.simps)


[STATEMENT]
lemma chainPar:
  fixes P  :: pi
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "Q \<Longrightarrow>\<^sub>\<tau> Q'"

  shows "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
from \<open>P \<Longrightarrow>\<^sub>\<tau> P'\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
have "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
by(rule Par1Chain)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
from \<open>Q \<Longrightarrow>\<^sub>\<tau> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
Q \<Longrightarrow>\<^sub>\<tau> Q'
[PROOF STEP]
have "P' \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'"
[PROOF STATE]
proof (prove)
using this:
Q \<Longrightarrow>\<^sub>\<tau> Q'

goal (1 subgoal):
 1. P' \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
by(rule Par2Chain)
[PROOF STATE]
proof (state)
this:
P' \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
P' \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
P' \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_msb_alt: "msb w \<longleftrightarrow> hd (to_bl w)"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msb w = hd (to_bl w)
[PROOF STEP]
apply (simp add: msb_word_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w (LENGTH('a) - Suc 0) = hd (to_bl w)
[PROOF STEP]
apply (subst hd_conv_nth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. to_bl w \<noteq> []
 2. bit w (LENGTH('a) - Suc 0) = to_bl w ! 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w (LENGTH('a) - Suc 0) = to_bl w ! 0
[PROOF STEP]
apply (subst nth_to_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < LENGTH('a)
 2. bit w (LENGTH('a) - Suc 0) = bit w (LENGTH('a) - Suc 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w (LENGTH('a) - Suc 0) = bit w (LENGTH('a) - Suc 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Abs_viewres_inverse_None[simp]:
  "Rep_viewres (Abs_viewres None) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_viewres (Abs_viewres None) = None
[PROOF STEP]
by (simp add: Abs_viewres_inverse)


[STATEMENT]
lemma i_Exec_Stream_expand_aggregate_map_nth: "
  0 < k \<Longrightarrow>
  i_aggregate (f \<circ> (i_Exec_Comp_Stream trans_fun (input \<odot>\<^sub>i k) c)) k ag n =
  ag (map f (f_Exec_Comp_Stream trans_fun (input n # \<NoMsg>\<^bsup>k - Suc 0\<^esup>)
    (f_Exec_Comp trans_fun ((input \<Down> n) \<odot>\<^sub>f k) c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_aggregate (f \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) c) k ag n = ag (map f (f_Exec_Comp_Stream trans_fun (input n # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (input \<Down> n \<odot> k) c)))
[PROOF STEP]
by (simp add: i_aggregate_nth i_Exec_Stream_drop i_Exec_Stream_take i_expand_i_take_mod i_expand_i_drop_mod i_drop_i_take_1)


[STATEMENT]
lemma cl_eq_cl_in:
  assumes "X \<subseteq> carrier"
  shows "cl X = cl_in carrier X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
interpret \<E>: matroid carrier "indep_in carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matroid carrier (indep_in carrier)
[PROOF STEP]
by (intro matroid_subset) auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
have "cl X = {x \<in> carrier. rank_of (insert x X) = rank_of X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X = {x \<in> carrier. rank_of (insert x X) = rank_of X}
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier. rank_of (insert x X) = rank_of X} = {x \<in> carrier. rank_of (insert x X) = rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl X = {x \<in> carrier. rank_of (insert x X) = rank_of X}

goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cl X = {x \<in> carrier. rank_of (insert x X) = rank_of X}

goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
have "\<dots> = {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier. rank_of (insert x X) = rank_of X} = {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X}
[PROOF STEP]
using rank_of_sub_cong[of carrier] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>carrier \<subseteq> carrier; ?\<E>' \<subseteq> carrier\<rbrakk> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'
X \<subseteq> carrier

goal (1 subgoal):
 1. {x \<in> carrier. rank_of (insert x X) = rank_of X} = {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> carrier. rank_of (insert x X) = rank_of X} = {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X}

goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x \<in> carrier. rank_of (insert x X) = rank_of X} = {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X}

goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
have "\<dots> = cl_in carrier X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X} = cl_in carrier X
[PROOF STEP]
unfolding cl_in_def \<E>.cl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X} = {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X} = cl_in carrier X

goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cl X = cl_in carrier X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cl X = cl_in carrier X

goal (1 subgoal):
 1. cl X = cl_in carrier X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cl X = cl_in carrier X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ir_runs2sigs_upd_resp [simp]:
  "\<lbrakk> runz Rb = Some (Resp, [A, B], []) \<rbrakk>
  \<Longrightarrow> ir_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey Kab]))) =
     (ir_runs2sigs runz)(Running [A, B] (Kab, Rb$nb) := 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz Rb = Some (Resp, [A, B], []) \<Longrightarrow> ir_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey Kab]))) = (ir_runs2sigs runz)(Running [A, B] (Kab, Rb $ nb) := 1)
[PROOF STEP]
apply (rule ext, erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. runz Rb = Some (Resp, [A, B], []) \<longrightarrow> ir_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey Kab]))) x = ((ir_runs2sigs runz)(Running [A, B] (Kab, Rb $ nb) := 1)) x
[PROOF STEP]
apply (rule ir_runs2sigs.induct, fastforce+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma numeral_power_int_eq_of_complex_cancel_iff [simp]:
  "power_int (numeral x) n = (of_complex y :: 'a :: {complex_div_algebra, division_ring}) \<longleftrightarrow>
     power_int (numeral x) n = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (numeral x powi n = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (numeral x powi n = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
have "power_int (numeral x) n = (of_complex (power_int (numeral x) n) :: 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. numeral x powi n = of_complex (numeral x powi n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
numeral x powi n = of_complex (numeral x powi n)

goal (1 subgoal):
 1. (numeral x powi n = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
numeral x powi n = of_complex (numeral x powi n)

goal (1 subgoal):
 1. (numeral x powi n = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
have "\<dots> = of_complex y \<longleftrightarrow> power_int (numeral x) n = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex (numeral x powi n) = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
by (subst of_complex_eq_iff) auto
[PROOF STATE]
proof (state)
this:
(of_complex (numeral x powi n) = of_complex y) = (numeral x powi n = y)

goal (1 subgoal):
 1. (numeral x powi n = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(numeral x powi n = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(numeral x powi n = of_complex y) = (numeral x powi n = y)

goal (1 subgoal):
 1. (numeral x powi n = of_complex y) = (numeral x powi n = y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(numeral x powi n = of_complex y) = (numeral x powi n = y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pos_less_divideC_eq [field_simps]:
  "a < b /\<^sub>C c \<longleftrightarrow> c *\<^sub>C a < b" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < b /\<^sub>C c) = (c *\<^sub>C a < b)
[PROOF STEP]
using that pos_le_divideC_eq [of c a b]
[PROOF STATE]
proof (prove)
using this:
0 < c
0 < c \<Longrightarrow> (a \<le> b /\<^sub>C c) = (c *\<^sub>C a \<le> b)

goal (1 subgoal):
 1. (a < b /\<^sub>C c) = (c *\<^sub>C a < b)
[PROOF STEP]
by (auto simp add: le_less)


[STATEMENT]
lemma remaining_steps_step_sub [simp]: "\<lbrakk>invar (common :: 'a state)\<rbrakk>
 \<Longrightarrow> remaining_steps (step common) = remaining_steps common - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> remaining_steps (step common) = remaining_steps common - 1
[PROOF STEP]
by(induction common)(auto split: current.splits)


[STATEMENT]
lemma transitive_inf_closed:
  "transitive x \<Longrightarrow> transitive y \<Longrightarrow> transitive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transitive x; transitive y\<rbrakk> \<Longrightarrow> transitive (x \<sqinter> y)
[PROOF STEP]
by (meson comp_left_subdist_inf inf.cobounded1 inf.sup_mono inf_le2 mult_right_isotone order.trans)


[STATEMENT]
lemma cor_cmod_power_4 [simp]:
  shows "cor (cmod z) ^ 4 = (z * cnj z)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (cmod z) ^ 4 = (z * cnj z)\<^sup>2
[PROOF STEP]
by (simp add: complex_mult_cnj_cmod)


[STATEMENT]
lemma hconf_new: "\<lbrakk> P \<turnstile> h \<surd>; h a = None; P,h \<turnstile> obj \<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h(a\<mapsto>obj) \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> h \<surd>; h a = None; P,h \<turnstile> obj \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h(a \<mapsto> obj) \<surd>
[PROOF STEP]
by (unfold hconf_def) (auto intro: oconf_new preallocated_new)


[STATEMENT]
lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n
[PROOF STEP]
proof (induction N)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n \<le> 0; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ 0 \<le> a ^ n
 2. \<And>N. \<lbrakk>\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n; n \<le> Suc N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ Suc N \<le> a ^ n
[PROOF STEP]
case (Suc N)
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n
n \<le> Suc N
(0::'a) \<le> a
a \<le> (1::'a)

goal (2 subgoals):
 1. \<lbrakk>n \<le> 0; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ 0 \<le> a ^ n
 2. \<And>N. \<lbrakk>\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n; n \<le> Suc N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ Suc N \<le> a ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n
n \<le> Suc N
(0::'a) \<le> a
a \<le> (1::'a)
[PROOF STEP]
have "a * a^N \<le> 1 * a^n" if "n \<le> N"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n
n \<le> Suc N
(0::'a) \<le> a
a \<le> (1::'a)

goal (1 subgoal):
 1. a * a ^ N \<le> (1::'a) * a ^ n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n
n \<le> Suc N
(0::'a) \<le> a
a \<le> (1::'a)
n \<le> N

goal (1 subgoal):
 1. a * a ^ N \<le> (1::'a) * a ^ n
[PROOF STEP]
by (intro mult_mono) auto
[PROOF STATE]
proof (state)
this:
n \<le> N \<Longrightarrow> a * a ^ N \<le> (1::'a) * a ^ n

goal (2 subgoals):
 1. \<lbrakk>n \<le> 0; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ 0 \<le> a ^ n
 2. \<And>N. \<lbrakk>\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n; n \<le> Suc N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ Suc N \<le> a ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> N \<Longrightarrow> a * a ^ N \<le> (1::'a) * a ^ n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> N \<Longrightarrow> a * a ^ N \<le> (1::'a) * a ^ n

goal (1 subgoal):
 1. a ^ Suc N \<le> a ^ n
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
n \<le> N \<Longrightarrow> a * a ^ N \<le> (1::'a) * a ^ n
\<lbrakk>n \<le> N; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ N \<le> a ^ n
n \<le> Suc N
(0::'a) \<le> a
a \<le> (1::'a)

goal (1 subgoal):
 1. a ^ Suc N \<le> a ^ n
[PROOF STEP]
by (auto simp add: le_Suc_eq)
[PROOF STATE]
proof (state)
this:
a ^ Suc N \<le> a ^ n

goal (1 subgoal):
 1. \<lbrakk>n \<le> 0; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ 0 \<le> a ^ n
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma seq_mult_simp:
  assumes "s \<in> closed_seqs R"
  assumes "t \<in> closed_seqs R"
  shows "(s \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> t) k = s k \<otimes> t k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> t) k = s k \<otimes> t k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier R\<^bsup>\<omega>\<^esup>
t \<in> carrier R\<^bsup>\<omega>\<^esup>

goal (1 subgoal):
 1. (s \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> t) k = s k \<otimes> t k
[PROOF STEP]
unfolding nat_seqs_def
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier (function_ring UNIV R)
t \<in> carrier (function_ring UNIV R)

goal (1 subgoal):
 1. (s \<otimes>\<^bsub>function_ring UNIV R\<^esub> t) k = s k \<otimes> t k
[PROOF STEP]
by (simp add: ring_functions.function_mult_eval_car ring_functions_axioms)


[STATEMENT]
lemma extf_ext_irrefl: "ext_irrefl (extf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ext_irrefl (extf f)
[PROOF STEP]
by (rule ext_irrefl_before_trans.axioms(1)[OF extf_ext_irrefl_before_trans])


[STATEMENT]
lemma (in group) pow_eq_int_mod:
  fixes n m::int
  assumes "a \<in> carrier G" "a [^] n = a [^] m"
  shows "n mod (ord a) = m mod (ord a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n mod int (ord a) = m mod int (ord a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n mod int (ord a) = m mod int (ord a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in> carrier G
a [^] n = a [^] m
[PROOF STEP]
have "a [^] (n - m) = \<one>"
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier G
a [^] n = a [^] m

goal (1 subgoal):
 1. a [^] (n - m) = \<one>
[PROOF STEP]
using int_pow_closed int_pow_diff r_inv
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier G
a [^] n = a [^] m
?x \<in> carrier G \<Longrightarrow> ?x [^] ?i \<in> carrier G
?x \<in> carrier G \<Longrightarrow> ?x [^] (?n - ?m) = ?x [^] ?n \<otimes> inv (?x [^] ?m)
?x \<in> carrier G \<Longrightarrow> ?x \<otimes> inv ?x = \<one>

goal (1 subgoal):
 1. a [^] (n - m) = \<one>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
a [^] (n - m) = \<one>

goal (1 subgoal):
 1. n mod int (ord a) = m mod int (ord a)
[PROOF STEP]
hence "ord a dvd n - m"
[PROOF STATE]
proof (prove)
using this:
a [^] (n - m) = \<one>

goal (1 subgoal):
 1. int (ord a) dvd n - m
[PROOF STEP]
using assms(1) int_pow_eq_id
[PROOF STATE]
proof (prove)
using this:
a [^] (n - m) = \<one>
a \<in> carrier G
?x \<in> carrier G \<Longrightarrow> (?x [^] ?i = \<one>) = (int (ord ?x) dvd ?i)

goal (1 subgoal):
 1. int (ord a) dvd n - m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
int (ord a) dvd n - m

goal (1 subgoal):
 1. n mod int (ord a) = m mod int (ord a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int (ord a) dvd n - m

goal (1 subgoal):
 1. n mod int (ord a) = m mod int (ord a)
[PROOF STEP]
by (meson mod_eq_dvd_iff)
[PROOF STATE]
proof (state)
this:
n mod int (ord a) = m mod int (ord a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<tau>Exec_methr_converse_cases [consumes 1, case_names refl step]:
  assumes "\<tau>Exec_methr ci P ins xt t h s s'"
  obtains "s = s'"
  | stk loc pc xcp s''
    where "s = (stk, loc, pc, xcp)"
       "exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<epsilon> h s''"
       "xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc)"
       "\<tau>Exec_methr ci P ins xt t h s'' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = s' \<Longrightarrow> thesis; \<And>stk loc pc xcp s''. \<lbrakk>s = (stk, loc, pc, xcp); exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s''; xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc); \<tau>Exec_methr ci P ins xt t h s'' s'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_methr ci P ins xt t h s s'

goal (1 subgoal):
 1. \<lbrakk>s = s' \<Longrightarrow> thesis; \<And>stk loc pc xcp s''. \<lbrakk>s = (stk, loc, pc, xcp); exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s''; xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc); \<tau>Exec_methr ci P ins xt t h s'' s'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(erule converse_rtranclpE)(blast elim: \<tau>exec_methE)


[STATEMENT]
lemma While_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_WhileI2)


[STATEMENT]
lemma \<tau>Exec_1r_rtranclpD:
  "\<tau>Exec_1r P t (xcp, h, frs) (xcp', h', frs')
  \<Longrightarrow> (\<lambda>((xcp, frs), h) ((xcp', frs'), h'). exec_1 P t (xcp, h, frs) \<epsilon> (xcp', h', frs') \<and> \<tau>Move2 P (xcp, h, frs))^** ((xcp, frs), h) ((xcp', frs'), h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1r P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> (\<lambda>((xcp, frs), h) ((xcp', frs'), h'). P,t \<turnstile> (xcp, h, frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h', frs') \<and> \<tau>Move2 P (xcp, h, frs))\<^sup>*\<^sup>* ((xcp, frs), h) ((xcp', frs'), h')
[PROOF STEP]
by(induct rule: rtranclp_induct3)(fastforce intro: rtranclp.rtrancl_into_rtrancl)+


[STATEMENT]
lemma ghole_num_bef_at_pos_num_gholes_less_eq:
  assumes "p \<in> poss_gmctxt C"
  shows "ghole_num_bef_pos p C + ghole_num_at_pos p C \<le> num_gholes C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_num_bef_pos p C + ghole_num_at_pos p C \<le> num_gholes C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> poss_gmctxt C

goal (1 subgoal):
 1. ghole_num_bef_pos p C + ghole_num_at_pos p C \<le> num_gholes C
[PROOF STEP]
proof (induct C arbitrary: p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. p \<in> poss_gmctxt GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole + ghole_num_at_pos p GMHole \<le> num_gholes GMHole
 2. \<And>x1 x2 p. \<lbrakk>\<And>x2a p. \<lbrakk>x2a \<in> set x2; p \<in> poss_gmctxt x2a\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p x2a + ghole_num_at_pos p x2a \<le> num_gholes x2a; p \<in> poss_gmctxt (GMFun x1 x2)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun x1 x2) + ghole_num_at_pos p (GMFun x1 x2) \<le> num_gholes (GMFun x1 x2)
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; ?p \<in> poss_gmctxt ?x2a\<rbrakk> \<Longrightarrow> ghole_num_bef_pos ?p ?x2a + ghole_num_at_pos ?p ?x2a \<le> num_gholes ?x2a
p \<in> poss_gmctxt (GMFun f Cs)

goal (2 subgoals):
 1. \<And>p. p \<in> poss_gmctxt GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole + ghole_num_at_pos p GMHole \<le> num_gholes GMHole
 2. \<And>x1 x2 p. \<lbrakk>\<And>x2a p. \<lbrakk>x2a \<in> set x2; p \<in> poss_gmctxt x2a\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p x2a + ghole_num_at_pos p x2a \<le> num_gholes x2a; p \<in> poss_gmctxt (GMFun x1 x2)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun x1 x2) + ghole_num_at_pos p (GMFun x1 x2) \<le> num_gholes (GMFun x1 x2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
 2. \<And>a list. p = a # list \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
case (Cons i ps)
[PROOF STATE]
proof (state)
this:
p = i # ps

goal (2 subgoals):
 1. p = [] \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
 2. \<And>a list. p = a # list \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
have *: "num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))
[PROOF STEP]
using GMFun(2)
[PROOF STATE]
proof (prove)
using this:
p \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
using this:
i # ps \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))
[PROOF STEP]
by (auto simp flip: take_map take_drop)
         (metis Cons_nth_drop_Suc add.assoc append_take_drop_id drop_map length_map nth_map sum_list.Cons sum_list.append)
[PROOF STATE]
proof (state)
this:
num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))

goal (2 subgoals):
 1. p = [] \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
 2. \<And>a list. p = a # list \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
p = i # ps
[PROOF STEP]
have
      "(sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)))
       + sum_list (map num_gholes (drop (Suc i) Cs)) \<le>
       (sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i)) + sum_list (map num_gholes (drop (Suc i) Cs))"
[PROOF STATE]
proof (prove)
using this:
p = i # ps

goal (1 subgoal):
 1. sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)) + sum_list (map num_gholes (drop (Suc i) Cs)) \<le> sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))
[PROOF STEP]
using GMFun(1)[OF nth_mem, of i ps] GMFun(2)
[PROOF STATE]
proof (prove)
using this:
p = i # ps
\<lbrakk>i < length Cs; ps \<in> poss_gmctxt (Cs ! i)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i) \<le> num_gholes (Cs ! i)
p \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)) + sum_list (map num_gholes (drop (Suc i) Cs)) \<le> sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)) + sum_list (map num_gholes (drop (Suc i) Cs)) \<le> sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))

goal (2 subgoals):
 1. p = [] \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
 2. \<And>a list. p = a # list \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
from add_le_imp_le_right[OF this]
[PROOF STATE]
proof (chain)
picking this:
sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)) \<le> sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)) \<le> sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i)

goal (1 subgoal):
 1. ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
using GMFun(2) *
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)) \<le> sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i)
p \<in> poss_gmctxt (GMFun f Cs)
num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))

goal (1 subgoal):
 1. ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)) \<le> sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i)
i # ps \<in> poss_gmctxt (GMFun f Cs)
num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))

goal (1 subgoal):
 1. ghole_num_bef_pos (i # ps) (GMFun f Cs) + ghole_num_at_pos (i # ps) (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)

goal (1 subgoal):
 1. p = [] \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
ghole_num_bef_pos p (GMFun f Cs) + ghole_num_at_pos p (GMFun f Cs) \<le> num_gholes (GMFun f Cs)

goal (1 subgoal):
 1. \<And>p. p \<in> poss_gmctxt GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole + ghole_num_at_pos p GMHole \<le> num_gholes GMHole
[PROOF STEP]
qed auto


[STATEMENT]
lemma funas_gterm_gterm_of_gmctxt [simp]:
  "num_gholes C = 0 \<Longrightarrow> funas_gterm (gterm_of_gmctxt C) = funas_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = 0 \<Longrightarrow> funas_gterm (gterm_of_gmctxt C) = funas_gmctxt C
[PROOF STEP]
by (metis funas_gmctxt_gmctxt_of_gterm no_gholes_gmctxt_of_gterm_gterm_of_gmctxt_id)


[STATEMENT]
lemma refresh_1_dom[simp]: "dom (refresh_1 f) = dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (refresh_1 f) = dom f
[PROOF STEP]
unfolding refresh_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (if True \<in> snd ` ran f then f else map_option (apsnd \<top>) \<circ> f) = dom f
[PROOF STEP]
by simp


[STATEMENT]
lemma distinct_pair_filter': "distinct (map fst xs) \<Longrightarrow> (a,b)\<in> set xs \<Longrightarrow> (map snd (filter (\<lambda>(x,y). x = a) xs)) = [b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst xs); (a, b) \<in> set xs\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = a) xs) = [b]
[PROOF STEP]
using distinct_pair_filter
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (map fst ?xs); (?a, ?b) \<in> set ?xs\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>x. fst x = ?a) ?xs) = [?b]

goal (1 subgoal):
 1. \<lbrakk>distinct (map fst xs); (a, b) \<in> set xs\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = a) xs) = [b]
[PROOF STEP]
by (simp only: split_comp_eq_pair)


[STATEMENT]
lemma termination_lemma:
shows "\<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; sorted w; w \<noteq> [] \<rbrakk> \<Longrightarrow>
        ss [\<sqsubset>\<^sub>r] merges f qs ss \<or>
        merges f qs ss = ss \<and>
       (sorted_list_of_set ({q. \<exists>t. (q,t)\<in>set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss!q \<noteq> ss!q} \<union> set (tl w)),w) \<in>
       (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> ss [\<sqsubset>\<^bsub>r\<^esub>] merges f qs ss \<or> merges f qs ss = ss \<and> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply(insert is_semi)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f)\<rbrakk> \<Longrightarrow> ss [\<sqsubset>\<^bsub>r\<^esub>] merges f qs ss \<or> merges f qs ss = ss \<and> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply (unfold lesssub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f)\<rbrakk> \<Longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] merges f qs ss \<and> ss \<noteq> merges f qs ss \<or> merges f qs ss = ss \<and> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply (simp (no_asm_simp) add: merges_incr_dom)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f)\<rbrakk> \<Longrightarrow> ss = merges f qs ss \<longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply (rule merges_same_conv_dom [THEN iffD1, elim_format])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss\<rbrakk> \<Longrightarrow> ?xs13 \<in> nlists n A
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss\<rbrakk> \<Longrightarrow> distinct (map fst ?ps13)
 3. \<And>x. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; x \<in> set ?ps13\<rbrakk> \<Longrightarrow> case x of (p, x) \<Rightarrow> p < length ?xs13 \<and> x \<in> A
 4. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss\<rbrakk> \<Longrightarrow> merges f ?ps13 ?xs13 = ?xs13
 5. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set ?ps13. x \<sqsubseteq>\<^bsub>r\<^esub> ?xs13 ! p\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; x \<in> set qs\<rbrakk> \<Longrightarrow> case x of (p, x) \<Rightarrow> p < length ss \<and> x \<in> A
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss\<rbrakk> \<Longrightarrow> merges f qs ss = ss
 3. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss\<rbrakk> \<Longrightarrow> merges f qs ss = ss
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
 3. \<And>x. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; x \<in> set qs\<rbrakk> \<Longrightarrow> case x of (p, x) \<Rightarrow> p < length ss \<and> x \<in> A
[PROOF STEP]
apply (rule sym, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
 2. \<And>x. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; x \<in> set qs\<rbrakk> \<Longrightarrow> case x of (p, x) \<Rightarrow> p < length ss \<and> x \<in> A
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; x \<in> set qs\<rbrakk> \<Longrightarrow> case x of (p, x) \<Rightarrow> p < length ss \<and> x \<in> A
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q t. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>x\<in>set qs. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; (q, t) \<in> set qs\<rbrakk> \<Longrightarrow> t \<squnion>\<^bsub>f\<^esub> ss ! q = ss ! q
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply (drule bspec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q t. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>x\<in>set qs. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; (q, t) \<in> set qs; case (q, t) of (q, t) \<Rightarrow> q < n \<and> t \<in> A\<rbrakk> \<Longrightarrow> t \<squnion>\<^bsub>f\<^esub> ss ! q = ss ! q
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply (drule bspec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q t. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; (q, t) \<in> set qs; case (q, t) of (q, t) \<Rightarrow> q < n \<and> t \<in> A; case (q, t) of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p\<rbrakk> \<Longrightarrow> t \<squnion>\<^bsub>f\<^esub> ss ! q = ss ! q
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
apply(subgoal_tac "{q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q); {q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)\<rbrakk> \<Longrightarrow> (sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
 2. \<lbrakk>ss \<in> nlists n A; distinct (map fst qs); \<forall>(q, t)\<in>set qs. q < n \<and> t \<in> A; Sorted_Less.sorted w; w \<noteq> []; semilat (A, r, f); ss = merges f qs ss; \<forall>(p, x)\<in>set qs. x \<sqsubseteq>\<^bsub>r\<^esub> ss ! p; \<forall>q t. \<not> ((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)\<rbrakk> \<Longrightarrow> {q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)
[PROOF STEP]
apply (auto simp add: sorted_list_psub)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) KbaseTr1:"distinct_pds K n P \<Longrightarrow>  KbaseP K P n (Kb\<^bsub>K n P \<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> KbaseP K P n (Kb\<^bsub>K n P\<^esub>)
[PROOF STEP]
apply (subst Kbase_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> KbaseP K P n (Eps (KbaseP K P n))
[PROOF STEP]
apply (frule KbaseTr[of n P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; \<exists>f. KbaseP K P n f\<rbrakk> \<Longrightarrow> KbaseP K P n (Eps (KbaseP K P n))
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>distinct_pds K n P; KbaseP K P n f\<rbrakk> \<Longrightarrow> KbaseP K P n (Eps (KbaseP K P n))
[PROOF STEP]
apply (simp add:someI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subset_bound_invariant:
  "invariant step (r_ok r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant (\<Rightarrow>) (r_ok r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; r_ok r x\<rbrakk> \<Longrightarrow> r_ok r y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; r_ok r x\<rbrakk> \<Longrightarrow> r_ok r y
[PROOF STEP]
assume "x \<Rightarrow> y" and "r_ok r x"
[PROOF STATE]
proof (state)
this:
x \<Rightarrow> y
r_ok r x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; r_ok r x\<rbrakk> \<Longrightarrow> r_ok r y
[PROOF STEP]
thus "r_ok r y"
[PROOF STATE]
proof (prove)
using this:
x \<Rightarrow> y
r_ok r x

goal (1 subgoal):
 1. r_ok r y
[PROOF STEP]
by (induction) auto
[PROOF STATE]
proof (state)
this:
r_ok r y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_stores_points_to[rule_format, simplified conj_explode]:
  "heap (fold_stores ws (s sys)) r = Some obj \<and> obj_fields obj f = Some r'
     \<longrightarrow> (r points_to r') s \<or> (\<exists>w \<in> set ws. r' \<in> store_refs w)" (is "?P (fold_stores ws) obj")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap (fold_stores ws (s sys)) r = Some obj \<and> obj_fields obj f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)
[PROOF STEP]
unfolding fold_stores_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) ws id (s sys)) r = Some obj \<and> obj_fields obj f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)
[PROOF STEP]
apply (rule spec[OF fold_invariant[where P="\<lambda>fr. \<forall>obj. ?P fr obj" and Q="\<lambda>w. w \<in> set ws"]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set ws \<Longrightarrow> x \<in> set ws
 2. \<forall>x. heap (id (s sys)) r = Some x \<and> obj_fields x f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)
 3. \<And>x sa. \<lbrakk>x \<in> set ws; \<forall>x. heap (sa (s sys)) r = Some x \<and> obj_fields x f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)\<rbrakk> \<Longrightarrow> \<forall>xa. heap ((do_store_action x \<circ> sa) (s sys)) r = Some xa \<and> obj_fields xa f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x. heap (id (s sys)) r = Some x \<and> obj_fields x f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)
 2. \<And>x sa. \<lbrakk>x \<in> set ws; \<forall>x. heap (sa (s sys)) r = Some x \<and> obj_fields x f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)\<rbrakk> \<Longrightarrow> \<forall>xa. heap ((do_store_action x \<circ> sa) (s sys)) r = Some xa \<and> obj_fields xa f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)
[PROOF STEP]
apply (fastforce simp: ran_def split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x sa. \<lbrakk>x \<in> set ws; \<forall>x. heap (sa (s sys)) r = Some x \<and> obj_fields x f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)\<rbrakk> \<Longrightarrow> \<forall>xa. heap ((do_store_action x \<circ> sa) (s sys)) r = Some xa \<and> obj_fields xa f = Some r' \<longrightarrow> (r points_to r') s \<or> (\<exists>w\<in>set ws. r' \<in> store_refs w)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x sa xa. \<lbrakk>x \<in> set ws; heap (do_store_action x (sa (s sys))) r = Some xa; obj_fields xa f = Some r'; \<forall>w\<in>set ws. r' \<notin> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); \<forall>x. heap (sa (s sys)) r = Some x \<longrightarrow> obj_fields x f \<noteq> Some r'\<rbrakk> \<Longrightarrow> (r points_to r') s
[PROOF STEP]
apply (drule (1) bspec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x sa xa. \<lbrakk>x \<in> set ws; heap (do_store_action x (sa (s sys))) r = Some xa; obj_fields xa f = Some r'; \<forall>x. heap (sa (s sys)) r = Some x \<longrightarrow> obj_fields x f \<noteq> Some r'; r' \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> (r points_to r') s
[PROOF STEP]
apply (clarsimp simp: fun_upd_apply split: mem_store_action.split_asm if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clinear_eq_butterfly_ketI:
  fixes F G :: \<open>('a::finite ell2 \<Rightarrow>\<^sub>C\<^sub>L 'b::finite ell2) \<Rightarrow> 'c::complex_vector\<close>
  assumes "clinear F" and "clinear G"
  assumes "\<And>i j. F (butterfly (ket i) (ket j)) = G (butterfly (ket i) (ket j))"
  shows "F = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = G
[PROOF STEP]
apply (rule complex_vector.linear_eq_on_span[where f=F, THEN ext, rotated 3])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> cspan (?B1 x)
 2. \<And>x. clinear F
 3. \<And>x. clinear G
 4. \<And>x xa. xa \<in> ?B1 x \<Longrightarrow> F xa = G xa
[PROOF STEP]
apply (subst cspan_butterfly_ket)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> UNIV
 2. \<And>x. clinear F
 3. \<And>x. clinear G
 4. \<And>x xa. xa \<in> {butterfly (ket i) (ket j) |i j. True} \<Longrightarrow> F xa = G xa
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
clinear F
clinear G
F (butterfly (ket ?i) (ket ?j)) = G (butterfly (ket ?i) (ket ?j))

goal (4 subgoals):
 1. \<And>x. x \<in> UNIV
 2. \<And>x. clinear F
 3. \<And>x. clinear G
 4. \<And>x xa. xa \<in> {butterfly (ket i) (ket j) |i j. True} \<Longrightarrow> F xa = G xa
[PROOF STEP]
by auto


[STATEMENT]
lemma cltn2_left_inverse: "cltn2_compose (cltn2_inverse A) A = cltn2_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
let ?M = "cltn2_rep A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
let ?M' = "matrix_inv ?M"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
from cltn2_rep_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep ?A)
[PROOF STEP]
have "invertible ?M"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep ?A)

goal (1 subgoal):
 1. invertible (cltn2_rep A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invertible (cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
with matrix_inv_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible ?M \<Longrightarrow> invertible (matrix_inv ?M)
invertible (cltn2_rep A)
[PROOF STEP]
have "invertible ?M'"
[PROOF STATE]
proof (prove)
using this:
invertible ?M \<Longrightarrow> invertible (matrix_inv ?M)
invertible (cltn2_rep A)

goal (1 subgoal):
 1. invertible (matrix_inv (cltn2_rep A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible (matrix_inv (cltn2_rep A))

goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
with \<open>invertible ?M\<close> and cltn2_abs_rep_abs_mult
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep A)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs ?M) ** ?N) = cltn2_abs (?M ** ?N)
invertible (matrix_inv (cltn2_rep A))
[PROOF STEP]
have "cltn2_compose (cltn2_inverse A) A = cltn2_abs (?M' ** ?M)"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs ?M) ** ?N) = cltn2_abs (?M ** ?N)
invertible (matrix_inv (cltn2_rep A))

goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_abs (matrix_inv (cltn2_rep A) ** cltn2_rep A)
[PROOF STEP]
unfolding cltn2_compose_def and cltn2_inverse_def
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs ?M) ** ?N) = cltn2_abs (?M ** ?N)
invertible (matrix_inv (cltn2_rep A))

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs (matrix_inv (cltn2_rep A))) ** cltn2_rep A) = cltn2_abs (matrix_inv (cltn2_rep A) ** cltn2_rep A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_inverse A) A = cltn2_abs (matrix_inv (cltn2_rep A) ** cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
with \<open>invertible ?M\<close>
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep A)
cltn2_compose (cltn2_inverse A) A = cltn2_abs (matrix_inv (cltn2_rep A) ** cltn2_rep A)
[PROOF STEP]
show "cltn2_compose (cltn2_inverse A) A = cltn2_id"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A)
cltn2_compose (cltn2_inverse A) A = cltn2_abs (matrix_inv (cltn2_rep A) ** cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_id
[PROOF STEP]
unfolding cltn2_id_def
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A)
cltn2_compose (cltn2_inverse A) A = cltn2_abs (matrix_inv (cltn2_rep A) ** cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose (cltn2_inverse A) A = cltn2_abs (mat 1)
[PROOF STEP]
by (simp add: matrix_inv)
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_inverse A) A = cltn2_id

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma surj_on_empty_right: "surj_on f A {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f A {}
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>{}. \<exists>a\<in>A. b = f a
[PROOF STEP]
by blast


[STATEMENT]
lemma infinite_image_imp_infinite: "infinite (f ` A) \<Longrightarrow> infinite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (f ` A) \<Longrightarrow> infinite A
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Resolution_complete_standalone_finite:
  assumes ns: "\<forall>\<A>. \<not>cnf_semantics \<A> S"
  assumes fin: "finite (atoms_of_cnf S)"
  shows "S \<turnstile> \<box>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<turnstile> \<box>
[PROOF STEP]
using fin ns
[PROOF STATE]
proof (prove)
using this:
finite (atoms_of_cnf S)
\<forall>\<A>. \<not> cnf_semantics \<A> S

goal (1 subgoal):
 1. S \<turnstile> \<box>
[PROOF STEP]
proof(induction "atoms_of_cnf S" arbitrary: S rule: finite_psubset_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>finite (atoms_of_cnf S); \<And>Sa. \<lbrakk>atoms_of_cnf Sa \<subset> atoms_of_cnf S; \<forall>\<A>. \<not> cnf_semantics \<A> Sa\<rbrakk> \<Longrightarrow> Sa \<turnstile> \<box>; \<forall>\<A>. \<not> cnf_semantics \<A> S\<rbrakk> \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
case psubset
[PROOF STATE]
proof (state)
this:
finite (atoms_of_cnf S)
\<lbrakk>atoms_of_cnf ?S \<subset> atoms_of_cnf S; \<forall>\<A>. \<not> cnf_semantics \<A> ?S\<rbrakk> \<Longrightarrow> ?S \<turnstile> \<box>
\<forall>\<A>. \<not> cnf_semantics \<A> S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>finite (atoms_of_cnf S); \<And>Sa. \<lbrakk>atoms_of_cnf Sa \<subset> atoms_of_cnf S; \<forall>\<A>. \<not> cnf_semantics \<A> Sa\<rbrakk> \<Longrightarrow> Sa \<turnstile> \<box>; \<forall>\<A>. \<not> cnf_semantics \<A> S\<rbrakk> \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<turnstile> \<box>
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> S \<turnstile> \<box>
 2. \<not> ?P \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
assume e: "atoms_of_cnf S = {}"
[PROOF STATE]
proof (state)
this:
atoms_of_cnf S = {}

goal (2 subgoals):
 1. ?P \<Longrightarrow> S \<turnstile> \<box>
 2. \<not> ?P \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
from \<open>\<forall>\<A>. \<not> cnf_semantics \<A> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<A>. \<not> cnf_semantics \<A> S
[PROOF STEP]
have "S \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<A>. \<not> cnf_semantics \<A> S

goal (1 subgoal):
 1. S \<noteq> {}
[PROOF STEP]
unfolding cnf_semantics_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<A>. \<not> (\<forall>C\<in>S. clause_semantics \<A> C)

goal (1 subgoal):
 1. S \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (2 subgoals):
 1. ?P \<Longrightarrow> S \<turnstile> \<box>
 2. \<not> ?P \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
with e
[PROOF STATE]
proof (chain)
picking this:
atoms_of_cnf S = {}
S \<noteq> {}
[PROOF STEP]
have "S = {\<box>}"
[PROOF STATE]
proof (prove)
using this:
atoms_of_cnf S = {}
S \<noteq> {}

goal (1 subgoal):
 1. S = {\<box>}
[PROOF STEP]
unfolding atoms_of_cnf_def
[PROOF STATE]
proof (prove)
using this:
atoms_of_lit ` \<Union> S = {}
S \<noteq> {}

goal (1 subgoal):
 1. S = {\<box>}
[PROOF STEP]
by simp fast
[PROOF STATE]
proof (state)
this:
S = {\<box>}

goal (2 subgoals):
 1. ?P \<Longrightarrow> S \<turnstile> \<box>
 2. \<not> ?P \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
S = {\<box>}

goal (1 subgoal):
 1. S \<turnstile> \<box>
[PROOF STEP]
using Resolution.Ass
[PROOF STATE]
proof (prove)
using this:
S = {\<box>}
?C \<in> ?S \<Longrightarrow> ?S \<turnstile> ?C

goal (1 subgoal):
 1. S \<turnstile> \<box>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<turnstile> \<box>

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
have unsat_restrict: "\<forall>\<A>. \<not> cnf_semantics \<A> (restrict_cnf_atom a v S)" for a v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<A>. \<not> cnf_semantics \<A> (restrict_cnf_atom a v S)
[PROOF STEP]
using \<open>\<forall>\<A>. \<not> cnf_semantics \<A> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<A>. \<not> cnf_semantics \<A> S

goal (1 subgoal):
 1. \<forall>\<A>. \<not> cnf_semantics \<A> (restrict_cnf_atom a v S)
[PROOF STEP]
by(simp add: cnf_substitution_lemma)
[PROOF STATE]
proof (state)
this:
\<forall>\<A>. \<not> cnf_semantics \<A> (restrict_cnf_atom ?a ?v S)

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
assume ne: "atoms_of_cnf S \<noteq> {}"
[PROOF STATE]
proof (state)
this:
atoms_of_cnf S \<noteq> {}

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atoms_of_cnf S \<noteq> {}
[PROOF STEP]
obtain a where "a \<in> atoms_of_cnf S"
[PROOF STATE]
proof (prove)
using this:
atoms_of_cnf S \<noteq> {}

goal (1 subgoal):
 1. (\<And>a. a \<in> atoms_of_cnf S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> atoms_of_cnf S

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
hence "atoms_of_cnf (restrict_cnf_atom a v S) \<subset> atoms_of_cnf S" for v
[PROOF STATE]
proof (prove)
using this:
a \<in> atoms_of_cnf S

goal (1 subgoal):
 1. atoms_of_cnf (restrict_cnf_atom a v S) \<subset> atoms_of_cnf S
[PROOF STEP]
using restrict_cnf_remove[where 'a='a]
[PROOF STATE]
proof (prove)
using this:
a \<in> atoms_of_cnf S
atoms_of_cnf (restrict_cnf_atom ?a ?v ?c) \<subseteq> atoms_of_cnf ?c - {?a}

goal (1 subgoal):
 1. atoms_of_cnf (restrict_cnf_atom a v S) \<subset> atoms_of_cnf S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
atoms_of_cnf (restrict_cnf_atom a ?v S) \<subset> atoms_of_cnf S

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
from psubset(2)[OF this unsat_restrict]
[PROOF STATE]
proof (chain)
picking this:
restrict_cnf_atom a ?v3 S \<turnstile> \<box>
[PROOF STEP]
have IH: "restrict_cnf_atom a v S \<turnstile> \<box>" for v
[PROOF STATE]
proof (prove)
using this:
restrict_cnf_atom a ?v3 S \<turnstile> \<box>

goal (1 subgoal):
 1. restrict_cnf_atom a v S \<turnstile> \<box>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
restrict_cnf_atom a ?v S \<turnstile> \<box>

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
from unrestrict'[OF IH, of "\<not> _"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>R\<subseteq>{make_lit (\<not> \<not> ?uu3) a}. S \<turnstile> R
[PROOF STEP]
have unr_IH: "\<exists>R\<subseteq>{make_lit v a}. S \<turnstile> R"
        for v
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<subseteq>{make_lit (\<not> \<not> ?uu3) a}. S \<turnstile> R

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. S \<turnstile> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>{make_lit ?v a}. S \<turnstile> R

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
(* unbelievable, how much worry finding that "\<not> _" cost\<dots> otherwise, you get weird sledgehammer results. *)
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>{make_lit ?v a}. S \<turnstile> R

goal (1 subgoal):
 1. atoms_of_cnf S \<noteq> {} \<Longrightarrow> S \<turnstile> \<box>
[PROOF STEP]
from this[of False] this[of True]
[PROOF STATE]
proof (chain)
picking this:
\<exists>R\<subseteq>{make_lit False a}. S \<turnstile> R
\<exists>R\<subseteq>{make_lit True a}. S \<turnstile> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<subseteq>{make_lit False a}. S \<turnstile> R
\<exists>R\<subseteq>{make_lit True a}. S \<turnstile> R

goal (1 subgoal):
 1. S \<turnstile> \<box>
[PROOF STEP]
using Resolution.R[OF _ _ singletonI singletonI]
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<subseteq>{make_lit False a}. S \<turnstile> R
\<exists>R\<subseteq>{make_lit True a}. S \<turnstile> R
\<lbrakk>?S \<turnstile> {?k\<^sup>+}; ?S \<turnstile> {?k\<inverse>}\<rbrakk> \<Longrightarrow> ?S \<turnstile> {?k\<^sup>+} - {?k\<^sup>+} \<union> ({?k\<inverse>} - {?k\<inverse>})

goal (1 subgoal):
 1. S \<turnstile> \<box>
[PROOF STEP]
by (simp add: make_lit_def) (fast dest: subset_singletonD)
[PROOF STATE]
proof (state)
this:
S \<turnstile> \<box>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<turnstile> \<box>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_cnj_dsj_distrib:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>1[simp]: "\<chi>1 \<in> fmla" and \<chi>2[simp]: "\<chi>2 \<in> fmla"
 shows "prv (eqv (cnj \<phi> (dsj \<chi>1 \<chi>2)) (dsj (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (cnj \<phi> (dsj \<chi>1 \<chi>2)) (dsj (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)))
[PROOF STEP]
by (simp add: prv_cnj_dsj_distrib1 prv_cnj_dsj_distrib2 prv_eqvI)


[STATEMENT]
lemma set_less_aux_trans:
  assumes AB: "A \<sqsubset>' B" and BC: "B \<sqsubset>' C"
  shows "A \<sqsubset>' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
from AB BC
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' B
B \<sqsubset>' C
[PROOF STEP]
have A: "finite A" and B: "finite B" and C: "finite C"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' B
B \<sqsubset>' C

goal (1 subgoal):
 1. finite A &&& finite B &&& finite C
[PROOF STEP]
by(auto simp add: set_less_aux_def)
[PROOF STATE]
proof (state)
this:
finite A
finite B
finite C

goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
from AB A B
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' B
finite A
finite B
[PROOF STEP]
obtain ab where ab: "ab \<in> B - A"
    and minAB: "\<And>x. \<lbrakk> x \<in> A; x \<notin> B \<rbrakk> \<Longrightarrow> ab \<le> x \<and> (x \<le> ab \<longrightarrow> ab = x)"
    and minBA: "\<And>x. \<lbrakk> x \<in> B; x \<notin> A \<rbrakk> \<Longrightarrow> ab \<le> x \<and> (x \<le> ab \<longrightarrow> ab = x)"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' B
finite A
finite B

goal (1 subgoal):
 1. (\<And>ab. \<lbrakk>ab \<in> B - A; \<And>x. \<lbrakk>x \<in> A; x \<notin> B\<rbrakk> \<Longrightarrow> ab \<le> x \<and> (x \<le> ab \<longrightarrow> ab = x); \<And>x. \<lbrakk>x \<in> B; x \<notin> A\<rbrakk> \<Longrightarrow> ab \<le> x \<and> (x \<le> ab \<longrightarrow> ab = x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_less_aux_def
[PROOF STATE]
proof (prove)
using this:
finite A \<and> finite B \<and> (\<exists>y\<in>B - A. \<forall>z\<in>A - B \<union> (B - A). y \<le> z \<and> (z \<le> y \<longrightarrow> y = z))
finite A
finite B

goal (1 subgoal):
 1. (\<And>ab. \<lbrakk>ab \<in> B - A; \<And>x. \<lbrakk>x \<in> A; x \<notin> B\<rbrakk> \<Longrightarrow> ab \<le> x \<and> (x \<le> ab \<longrightarrow> ab = x); \<And>x. \<lbrakk>x \<in> B; x \<notin> A\<rbrakk> \<Longrightarrow> ab \<le> x \<and> (x \<le> ab \<longrightarrow> ab = x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ab \<in> B - A
\<lbrakk>?x \<in> A; ?x \<notin> B\<rbrakk> \<Longrightarrow> ab \<le> ?x \<and> (?x \<le> ab \<longrightarrow> ab = ?x)
\<lbrakk>?x \<in> B; ?x \<notin> A\<rbrakk> \<Longrightarrow> ab \<le> ?x \<and> (?x \<le> ab \<longrightarrow> ab = ?x)

goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
from BC B C
[PROOF STATE]
proof (chain)
picking this:
B \<sqsubset>' C
finite B
finite C
[PROOF STEP]
obtain bc where bc: "bc \<in> C - B"
    and minBC: "\<And>x. \<lbrakk> x \<in> B; x \<notin> C \<rbrakk> \<Longrightarrow> bc \<le> x \<and> (x \<le> bc \<longrightarrow> bc = x)"
    and minCB: "\<And>x. \<lbrakk> x \<in> C; x \<notin> B \<rbrakk> \<Longrightarrow> bc \<le> x \<and> (x \<le> bc \<longrightarrow> bc = x)"
[PROOF STATE]
proof (prove)
using this:
B \<sqsubset>' C
finite B
finite C

goal (1 subgoal):
 1. (\<And>bc. \<lbrakk>bc \<in> C - B; \<And>x. \<lbrakk>x \<in> B; x \<notin> C\<rbrakk> \<Longrightarrow> bc \<le> x \<and> (x \<le> bc \<longrightarrow> bc = x); \<And>x. \<lbrakk>x \<in> C; x \<notin> B\<rbrakk> \<Longrightarrow> bc \<le> x \<and> (x \<le> bc \<longrightarrow> bc = x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_less_aux_def
[PROOF STATE]
proof (prove)
using this:
finite B \<and> finite C \<and> (\<exists>y\<in>C - B. \<forall>z\<in>B - C \<union> (C - B). y \<le> z \<and> (z \<le> y \<longrightarrow> y = z))
finite B
finite C

goal (1 subgoal):
 1. (\<And>bc. \<lbrakk>bc \<in> C - B; \<And>x. \<lbrakk>x \<in> B; x \<notin> C\<rbrakk> \<Longrightarrow> bc \<le> x \<and> (x \<le> bc \<longrightarrow> bc = x); \<And>x. \<lbrakk>x \<in> C; x \<notin> B\<rbrakk> \<Longrightarrow> bc \<le> x \<and> (x \<le> bc \<longrightarrow> bc = x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bc \<in> C - B
\<lbrakk>?x \<in> B; ?x \<notin> C\<rbrakk> \<Longrightarrow> bc \<le> ?x \<and> (?x \<le> bc \<longrightarrow> bc = ?x)
\<lbrakk>?x \<in> C; ?x \<notin> B\<rbrakk> \<Longrightarrow> bc \<le> ?x \<and> (?x \<le> bc \<longrightarrow> bc = ?x)

goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
proof(cases "ab \<le> bc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ab \<le> bc

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
hence "ab \<in> C - A" "ab \<notin> A - C"
[PROOF STATE]
proof (prove)
using this:
ab \<le> bc

goal (1 subgoal):
 1. ab \<in> C - A &&& ab \<notin> A - C
[PROOF STEP]
using ab bc
[PROOF STATE]
proof (prove)
using this:
ab \<le> bc
ab \<in> B - A
bc \<in> C - B

goal (1 subgoal):
 1. ab \<in> C - A &&& ab \<notin> A - C
[PROOF STEP]
by(auto dest: minBC antisym)
[PROOF STATE]
proof (state)
this:
ab \<in> C - A
ab \<notin> A - C

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab \<in> C - A
ab \<notin> A - C

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ab \<in> C - A
ab \<notin> A - C

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
assume x: "x \<in> (C - A) \<union> (A - C)"
[PROOF STATE]
proof (state)
this:
x \<in> C - A \<union> (A - C)

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
hence "ab \<le> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> C - A \<union> (A - C)

goal (1 subgoal):
 1. ab \<le> x
[PROOF STEP]
by(cases "x \<in> B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF True])
[PROOF STATE]
proof (state)
this:
ab \<le> x

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab \<le> x

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
hence "ab \<noteq> x \<longrightarrow> \<not> x \<le> ab"
[PROOF STATE]
proof (prove)
using this:
ab \<le> x

goal (1 subgoal):
 1. ab \<noteq> x \<longrightarrow> \<not> x \<le> ab
[PROOF STEP]
using ab bc x
[PROOF STATE]
proof (prove)
using this:
ab \<le> x
ab \<in> B - A
bc \<in> C - B
x \<in> C - A \<union> (A - C)

goal (1 subgoal):
 1. ab \<noteq> x \<longrightarrow> \<not> x \<le> ab
[PROOF STEP]
by(cases "x \<in> B")(auto dest: antisym)
[PROOF STATE]
proof (state)
this:
ab \<noteq> x \<longrightarrow> \<not> x \<le> ab

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab \<noteq> x \<longrightarrow> \<not> x \<le> ab

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
ab \<le> x
ab \<noteq> x \<longrightarrow> \<not> x \<le> ab

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> ab

goal (2 subgoals):
 1. ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
 2. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ab \<in> C - A
ab \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> ab
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ab \<in> C - A
ab \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> ab

goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
using A C
[PROOF STATE]
proof (prove)
using this:
ab \<in> C - A
ab \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> ab
finite A
finite C

goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
unfolding set_less_aux_def
[PROOF STATE]
proof (prove)
using this:
ab \<in> C - A
ab \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> ab \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> ab
finite A
finite C

goal (1 subgoal):
 1. finite A \<and> finite C \<and> (\<exists>y\<in>C - A. \<forall>z\<in>A - C \<union> (C - A). y \<le> z \<and> (z \<le> y \<longrightarrow> y = z))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' C

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ab \<le> bc

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
with linear[of ab bc]
[PROOF STATE]
proof (chain)
picking this:
ab \<le> bc \<or> bc \<le> ab
\<not> ab \<le> bc
[PROOF STEP]
have "bc \<le> ab"
[PROOF STATE]
proof (prove)
using this:
ab \<le> bc \<or> bc \<le> ab
\<not> ab \<le> bc

goal (1 subgoal):
 1. bc \<le> ab
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bc \<le> ab

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
with ab bc
[PROOF STATE]
proof (chain)
picking this:
ab \<in> B - A
bc \<in> C - B
bc \<le> ab
[PROOF STEP]
have "bc \<in> C - A" "bc \<notin> A - C"
[PROOF STATE]
proof (prove)
using this:
ab \<in> B - A
bc \<in> C - B
bc \<le> ab

goal (1 subgoal):
 1. bc \<in> C - A &&& bc \<notin> A - C
[PROOF STEP]
by(auto dest: minAB antisym)
[PROOF STATE]
proof (state)
this:
bc \<in> C - A
bc \<notin> A - C

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc \<in> C - A
bc \<notin> A - C

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
bc \<in> C - A
bc \<notin> A - C

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
assume x: "x \<in> (C - A) \<union> (A - C)"
[PROOF STATE]
proof (state)
this:
x \<in> C - A \<union> (A - C)

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
hence "bc \<le> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> C - A \<union> (A - C)

goal (1 subgoal):
 1. bc \<le> x
[PROOF STEP]
by(cases "x \<in> B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF \<open>bc \<le> ab\<close>])
[PROOF STATE]
proof (state)
this:
bc \<le> x

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc \<le> x

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
hence "bc \<noteq> x \<longrightarrow> \<not> x \<le> bc"
[PROOF STATE]
proof (prove)
using this:
bc \<le> x

goal (1 subgoal):
 1. bc \<noteq> x \<longrightarrow> \<not> x \<le> bc
[PROOF STEP]
using ab bc x
[PROOF STATE]
proof (prove)
using this:
bc \<le> x
ab \<in> B - A
bc \<in> C - B
x \<in> C - A \<union> (A - C)

goal (1 subgoal):
 1. bc \<noteq> x \<longrightarrow> \<not> x \<le> bc
[PROOF STEP]
by(cases "x \<in> B")(auto dest: antisym)
[PROOF STATE]
proof (state)
this:
bc \<noteq> x \<longrightarrow> \<not> x \<le> bc

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc \<noteq> x \<longrightarrow> \<not> x \<le> bc

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
bc \<le> x
bc \<noteq> x \<longrightarrow> \<not> x \<le> bc

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> bc

goal (1 subgoal):
 1. \<not> ab \<le> bc \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bc \<in> C - A
bc \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> bc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bc \<in> C - A
bc \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> bc

goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
using A C
[PROOF STATE]
proof (prove)
using this:
bc \<in> C - A
bc \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> bc
finite A
finite C

goal (1 subgoal):
 1. A \<sqsubset>' C
[PROOF STEP]
unfolding set_less_aux_def
[PROOF STATE]
proof (prove)
using this:
bc \<in> C - A
bc \<notin> A - C
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<le> ?x2
?x2 \<in> C - A \<union> (A - C) \<Longrightarrow> bc \<noteq> ?x2 \<longrightarrow> \<not> ?x2 \<le> bc
finite A
finite C

goal (1 subgoal):
 1. finite A \<and> finite C \<and> (\<exists>y\<in>C - A. \<forall>z\<in>A - C \<union> (C - A). y \<le> z \<and> (z \<le> y \<longrightarrow> y = z))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma left_total_rel_pred: "left_unique A \<Longrightarrow> left_total (rel_pred A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_unique A \<Longrightarrow> left_total (rel_pred A)
[PROOF STEP]
unfolding rel_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_unique A \<Longrightarrow> left_total (A ===> (=))
[PROOF STEP]
by (erule left_total_fun) (rule left_total_eq)


[STATEMENT]
lemma augment_edge_cf[simp]: "(u,v)\<in>E\<union>E\<inverse> \<Longrightarrow>
    cf_of (augment_edge f (u,v) \<Delta>)
  = (cf_of f)( (u,v) := cf_of f (u,v) - \<Delta>, (v,u) := cf_of f (v,u) + \<Delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> E \<union> E\<inverse> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) = (cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)
[PROOF STEP]
apply (intro ext; cases "(u,v)\<in>E")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) x = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) x
 2. \<And>x. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) x = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) x
[PROOF STEP]
subgoal for e'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
apply (cases "e'=(u,v)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' = (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
 2. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' \<noteq> (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' = (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
by (simp split!: if_splits add: no_self_loop residualGraph_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' \<noteq> (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
apply (cases "e'=(v,u)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' \<noteq> (u, v); e' = (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
 2. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' \<noteq> (u, v); e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' \<noteq> (u, v); e' = (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
by (simp split!: if_splits add: no_parallel_edge residualGraph_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' \<noteq> (u, v); e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<in> E; e' \<noteq> (u, v); e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
by (simp
                  split!: if_splits prod.splits
                  add: residualGraph_def augment_edge_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) x = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) x
[PROOF STEP]
subgoal for e'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
apply (cases "e'=(u,v)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' = (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
 2. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' \<noteq> (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' = (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
by (simp split!: if_splits add: no_self_loop residualGraph_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' \<noteq> (u, v)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
apply (cases "e'=(v,u)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' \<noteq> (u, v); e' = (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
 2. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' \<noteq> (u, v); e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' \<noteq> (u, v); e' = (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
by (simp split!: if_splits add: no_self_loop residualGraph_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' \<noteq> (u, v); e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> E \<union> E\<inverse>; (u, v) \<notin> E; e' \<noteq> (u, v); e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) e' = ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) e'
[PROOF STEP]
by (simp
                  split!: if_splits prod.splits
                  add: residualGraph_def augment_edge_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fac_acc_work_final_fac_work: "fac_acc_work_final = fac_work_final" (is "?lhs=?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
have "?rhs = wrapA\<cdot>(fix\<cdot>fac_acc_body3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_work_final = wrapA\<cdot>(fix\<cdot>fac_acc_body3)
[PROOF STEP]
by (rule fac_work_final_body3_eq)
[PROOF STATE]
proof (state)
this:
fac_work_final = wrapA\<cdot>(fix\<cdot>fac_acc_body3)

goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fac_work_final = wrapA\<cdot>(fix\<cdot>fac_acc_body3)

goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
have "\<dots> = wrapA\<cdot>(fix\<cdot>fac_acc_body_final)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapA\<cdot>(fix\<cdot>fac_acc_body3) = wrapA\<cdot>(fix\<cdot>fac_acc_body_final)
[PROOF STEP]
using fac_acc_work_final_fac_acc_work3_eq
[PROOF STATE]
proof (prove)
using this:
fac_acc_body_final = fac_acc_body3

goal (1 subgoal):
 1. wrapA\<cdot>(fix\<cdot>fac_acc_body3) = wrapA\<cdot>(fix\<cdot>fac_acc_body_final)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wrapA\<cdot>(fix\<cdot>fac_acc_body3) = wrapA\<cdot>(fix\<cdot>fac_acc_body_final)

goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wrapA\<cdot>(fix\<cdot>fac_acc_body3) = wrapA\<cdot>(fix\<cdot>fac_acc_body_final)

goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
have "\<dots> = ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapA\<cdot>(fix\<cdot>fac_acc_body_final) = fac_acc_work_final
[PROOF STEP]
unfolding fac_acc_work_final_def wrapA_def a2n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_cfun ((oo) (\<Lambda> a. a\<cdot>1))\<cdot>(fix\<cdot>fac_acc_body_final) = (\<Lambda> x. fix\<cdot>fac_acc_body_final\<cdot>x\<cdot>1)
[PROOF STEP]
by (simp add: cfcomp1)
[PROOF STATE]
proof (state)
this:
wrapA\<cdot>(fix\<cdot>fac_acc_body_final) = fac_acc_work_final

goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fac_work_final = fac_acc_work_final
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fac_work_final = fac_acc_work_final

goal (1 subgoal):
 1. fac_acc_work_final = fac_work_final
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fac_acc_work_final = fac_work_final

goal:
No subgoals!
[PROOF STEP]
qed