[STATEMENT]
lemma Max_less_iMin_conv_less: "
  \<lbrakk> finite A; A \<noteq> {}; B \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A < iMin B) = (\<forall>a\<in>A. \<forall>b\<in>B. a < b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> (Max A < iMin B) = (\<forall>a\<in>A. \<forall>b\<in>B. a < b)
[PROOF STEP]
by (blast intro: Max_less_iMin_imp_less less_imp_Max_less_iMin)


[STATEMENT]
lemma Max_less_iMin_imp_disjoint: "
  \<lbrakk> finite A; Max A < iMin B \<rbrakk> \<Longrightarrow> A \<inter> B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < iMin B\<rbrakk> \<Longrightarrow> A \<inter> B = {}
[PROOF STEP]
apply (case_tac "A = {}", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < iMin B; A \<noteq> {}\<rbrakk> \<Longrightarrow> A \<inter> B = {}
[PROOF STEP]
apply (case_tac "B = {}", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < iMin B; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> A \<inter> B = {}
[PROOF STEP]
apply (rule disjoint_iff_not_equal[THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < iMin B; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y
[PROOF STEP]
apply (intro ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>finite A; Max A < iMin B; A \<noteq> {}; B \<noteq> {}; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<noteq> y
[PROOF STEP]
apply (rule less_imp_neq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>finite A; Max A < iMin B; A \<noteq> {}; B \<noteq> {}; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
by (rule Max_less_iMin_imp_less)


[STATEMENT]
lemma iMin_in_idem: "n \<in> I \<Longrightarrow> min n (iMin I) = iMin I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> I \<Longrightarrow> min n (iMin I) = iMin I
[PROOF STEP]
by (simp add: iMin_le min_eqR)


[STATEMENT]
lemma iMin_insert: "I \<noteq> {} \<Longrightarrow> iMin (insert n I) = min n (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> iMin (insert n I) = min n (iMin I)
[PROOF STEP]
apply (subst insert_is_Un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> iMin ({n} \<union> I) = min n (iMin I)
[PROOF STEP]
apply (subst iMin_Un)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. I \<noteq> {} \<Longrightarrow> {n} \<noteq> {}
 2. I \<noteq> {} \<Longrightarrow> I \<noteq> {}
 3. I \<noteq> {} \<Longrightarrow> min (iMin {n}) (iMin I) = min n (iMin I)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMin_insert_remove: "
  iMin (insert n I) =
  (if I - {n} = {} then n else min n (iMin (I - {n})))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMin (insert n I) = (if I - {n} = {} then n else min n (iMin (I - {n})))
[PROOF STEP]
by (metis iMin_insert iMin_singleton insert_Diff_single)


[STATEMENT]
lemma iMin_remove: "n \<in> I \<Longrightarrow> iMin I = (if I - {n} = {} then n else min n (iMin (I - {n})))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> I \<Longrightarrow> iMin I = (if I - {n} = {} then n else min n (iMin (I - {n})))
[PROOF STEP]
by (metis iMin_insert_remove insert_absorb)


[STATEMENT]
lemma iMin_subset_idem: "\<lbrakk> B \<noteq> {}; B \<subseteq> A \<rbrakk> \<Longrightarrow> min (iMin B) (iMin A) = iMin A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B \<noteq> {}; B \<subseteq> A\<rbrakk> \<Longrightarrow> min (iMin B) (iMin A) = iMin A
[PROOF STEP]
by (metis iMin_subset min.absorb2)


[STATEMENT]
lemma iMin_union_inter: "A \<inter> B \<noteq> {} \<Longrightarrow> min (iMin (A \<union> B)) (iMin (A \<inter> B)) = min (iMin A) (iMin B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> min (iMin (A \<union> B)) (iMin (A \<inter> B)) = min (iMin A) (iMin B)
[PROOF STEP]
by (metis Int_empty_left Int_lower2 Un_absorb2 Un_assoc Un_empty iMin_Un)


[STATEMENT]
lemma iMin_ge_iff: "I \<noteq> {} \<Longrightarrow> (n \<le> iMin I) = (\<forall>a\<in>I. n \<le> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> (n \<le> iMin I) = (\<forall>a\<in>I. n \<le> a)
[PROOF STEP]
by (metis Collect_iMin_le Collect_mem_eq iMinI_ex2 order_trans)


[STATEMENT]
lemma iMin_gr_iff: "I \<noteq> {} \<Longrightarrow> (n < iMin I) = (\<forall>a\<in>I. n < a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> (n < iMin I) = (\<forall>a\<in>I. n < a)
[PROOF STEP]
by (metis iMinI_ex2 iMin_neq_imp_greater order_less_trans)


[STATEMENT]
lemma iMin_le_iff: "I \<noteq> {} \<Longrightarrow> (iMin I \<le> n) = (\<exists>a\<in>I. a \<le> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> (iMin I \<le> n) = (\<exists>a\<in>I. a \<le> n)
[PROOF STEP]
by (metis Collect_iMin_le Collect_mem_eq iMinI_ex2 order_trans)


[STATEMENT]
lemma iMin_less_iff: "I \<noteq> {} \<Longrightarrow> (iMin I < n) = (\<exists>a\<in>I. a < n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> (iMin I < n) = (\<exists>a\<in>I. a < n)
[PROOF STEP]
by (metis iMinI_ex2 iMin_neq_imp_greater order_less_trans)


[STATEMENT]
lemma hom_iMin_commute: "\<lbrakk> \<And>x y. h (min x y) = min (h x) (h y); I \<noteq> {} \<rbrakk> \<Longrightarrow> iMin (h ` I) = h (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. h (min x y) = min (h x) (h y); I \<noteq> {}\<rbrakk> \<Longrightarrow> iMin (h ` I) = h (iMin I)
[PROOF STEP]
apply (rule iMin_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. h (min x y) = min (h x) (h y); I \<noteq> {}\<rbrakk> \<Longrightarrow> h (iMin I) \<in> h ` I
 2. \<And>x. \<lbrakk>\<And>x y. h (min x y) = min (h x) (h y); I \<noteq> {}; x \<in> h ` I\<rbrakk> \<Longrightarrow> h (iMin I) \<le> x
[PROOF STEP]
apply (blast intro: iMinI_ex2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x y. h (min x y) = min (h x) (h y); I \<noteq> {}; x \<in> h ` I\<rbrakk> \<Longrightarrow> h (iMin I) \<le> x
[PROOF STEP]
apply (rename_tac y)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<And>x y. h (min x y) = min (h x) (h y); I \<noteq> {}; y \<in> h ` I\<rbrakk> \<Longrightarrow> h (iMin I) \<le> y
[PROOF STEP]
apply (drule_tac x="iMin I" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>I \<noteq> {}; y \<in> h ` I; \<And>y. h (min (iMin I) y) = min (h (iMin I)) (h y)\<rbrakk> \<Longrightarrow> h (iMin I) \<le> y
[PROOF STEP]
apply (clarsimp simp: image_iff, rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>I \<noteq> {}; \<And>y. h (min (iMin I) y) = min (h (iMin I)) (h y); x \<in> I\<rbrakk> \<Longrightarrow> h (iMin I) \<le> h x
[PROOF STEP]
apply (drule_tac x=x in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>I \<noteq> {}; x \<in> I; h (min (iMin I) x) = min (h (iMin I)) (h x)\<rbrakk> \<Longrightarrow> h (iMin I) \<le> h x
[PROOF STEP]
apply (rule_tac t="h (iMin I)" and s="min (h (iMin I)) (h x)" in subst)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>I \<noteq> {}; x \<in> I; h (min (iMin I) x) = min (h (iMin I)) (h x)\<rbrakk> \<Longrightarrow> min (h (iMin I)) (h x) = h (iMin I)
 2. \<And>x. \<lbrakk>I \<noteq> {}; x \<in> I; h (min (iMin I) x) = min (h (iMin I)) (h x)\<rbrakk> \<Longrightarrow> min (h (iMin I)) (h x) \<le> h x
[PROOF STEP]
apply (simp add: min_eqL[OF iMin_le])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>I \<noteq> {}; x \<in> I; h (min (iMin I) x) = min (h (iMin I)) (h x)\<rbrakk> \<Longrightarrow> min (h (iMin I)) (h x) \<le> h x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "reflP ((\<le>)::('a::preorder \<Rightarrow> 'a \<Rightarrow> bool))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl {(x, y). x \<le> y}
[PROOF STEP]
by (simp add: refl_on_def)


[STATEMENT]
lemma "symP (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym {(x, y). x = y}
[PROOF STEP]
by (simp add: sym_def)


[STATEMENT]
lemma "equivP (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl {(x, y). x = y} \<and> sym {(x, y). x = y} \<and> transp (=)
[PROOF STEP]
by (simp add: trans_def refl_on_def sym_def)


[STATEMENT]
lemma "irreflP ((<)::('a::preorder \<Rightarrow> 'a \<Rightarrow> bool))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irrefl {(x, y). x < y}
[PROOF STEP]
by (simp add: irrefl_def)


[STATEMENT]
lemma singleton_not_empty: "{a} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a} \<noteq> {}
[PROOF STEP]
by blast


[STATEMENT]
lemma singleton_finite: "finite {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a}
[PROOF STEP]
by blast


[STATEMENT]
lemma singleton_ball: "(\<forall>x\<in>{a}. P x) = P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{a}. P x) = P a
[PROOF STEP]
by blast


[STATEMENT]
lemma singleton_bex: "(\<exists>x\<in>{a}. P x) = P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>{a}. P x) = P a
[PROOF STEP]
by blast


[STATEMENT]
lemma subset_singleton_conv: "(A \<subseteq> {a}) = (A = {} \<or> A = {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<subseteq> {a}) = (A = {} \<or> A = {a})
[PROOF STEP]
by blast


[STATEMENT]
lemma singleton_subset_conv: "({a} \<subseteq> A) = (a \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a} \<subseteq> A) = (a \<in> A)
[PROOF STEP]
by blast


[STATEMENT]
lemma singleton_eq_conv: "({a} = {b}) = (a = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a} = {b}) = (a = b)
[PROOF STEP]
by blast


[STATEMENT]
lemma singleton_subset_singleton_conv: "({a} \<subseteq> {b}) = (a = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a} \<subseteq> {b}) = (a = b)
[PROOF STEP]
by blast


[STATEMENT]
lemma singleton_Int1_if: "{a} \<inter> A = (if a \<in> A then {a} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a} \<inter> A = (if a \<in> A then {a} else {})
[PROOF STEP]
by (split if_split, blast)


[STATEMENT]
lemma singleton_Int2_if: "A \<inter> {a} = (if a \<in> A then {a} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> {a} = (if a \<in> A then {a} else {})
[PROOF STEP]
by (split if_split, blast)


[STATEMENT]
lemma singleton_image: "f ` {a} = {f a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {a} = {f a}
[PROOF STEP]
by blast


[STATEMENT]
lemma inj_on_singleton: "inj_on f {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f {a}
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_mono_on_singleton: "strict_mono_on f {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetInterval2.strict_mono_on f {a}
[PROOF STEP]
unfolding strict_mono_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>aa\<in>{a}. \<forall>b\<in>{a}. aa < b \<longrightarrow> f aa < f b
[PROOF STEP]
by blast


[STATEMENT]
lemma infinite_imp_not_singleton: "infinite A \<Longrightarrow> \<not> (\<exists>a. A = {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite A \<Longrightarrow> \<nexists>a. A = {a}
[PROOF STEP]
by blast


[STATEMENT]
lemma infinite_insert: "infinite (insert a A) = infinite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (insert a A) = infinite A
[PROOF STEP]
by simp


[STATEMENT]
lemma infinite_Diff_insert: "infinite (A - insert a B) = infinite (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (A - insert a B) = infinite (A - B)
[PROOF STEP]
by simp


[STATEMENT]
lemma subset_finite_imp_finite: "\<lbrakk> finite A; B \<subseteq> A \<rbrakk> \<Longrightarrow> finite B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; B \<subseteq> A\<rbrakk> \<Longrightarrow> finite B
[PROOF STEP]
by (rule finite_subset)


[STATEMENT]
lemma infinite_not_subset_finite: "\<lbrakk> infinite A; finite B \<rbrakk> \<Longrightarrow> \<not> A \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>infinite A; finite B\<rbrakk> \<Longrightarrow> \<not> A \<subseteq> B
[PROOF STEP]
by (blast intro: subset_finite_imp_finite)


[STATEMENT]
lemma Un_infinite_right: "infinite T \<Longrightarrow> infinite (S \<union> T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite T \<Longrightarrow> infinite (S \<union> T)
[PROOF STEP]
by blast


[STATEMENT]
lemma Un_infinite_iff: "infinite (S \<union> T) = (infinite S \<or> infinite T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (S \<union> T) = (infinite S \<or> infinite T)
[PROOF STEP]
by blast


[STATEMENT]
lemma cartesian_product_infiniteL_imp_infinite: "\<lbrakk> infinite A; B \<noteq> {} \<rbrakk> \<Longrightarrow> infinite (A \<times> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>infinite A; B \<noteq> {}\<rbrakk> \<Longrightarrow> infinite (A \<times> B)
[PROOF STEP]
by (blast dest: finite_cartesian_productD1)


[STATEMENT]
lemma cartesian_product_infiniteR_imp_infinite: "\<lbrakk> infinite B; A \<noteq> {} \<rbrakk> \<Longrightarrow> infinite (A \<times> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>infinite B; A \<noteq> {}\<rbrakk> \<Longrightarrow> infinite (A \<times> B)
[PROOF STEP]
by (blast dest: finite_cartesian_productD2)


[STATEMENT]
lemma finite_nat_iff_bounded2: "
  finite S = (\<exists>(k::nat).\<forall>n\<in>S. n < k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S = (\<exists>k. \<forall>n\<in>S. n < k)
[PROOF STEP]
by (simp only: finite_nat_iff_bounded, blast)


[STATEMENT]
lemma finite_nat_iff_bounded_le2: "
  finite S = (\<exists>(k::nat).\<forall>n\<in>S. n \<le> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S = (\<exists>k. \<forall>n\<in>S. n \<le> k)
[PROOF STEP]
by (simp only: finite_nat_iff_bounded_le, blast)


[STATEMENT]
lemma nat_asc_chain_imp_unbounded: "
  \<lbrakk> S \<noteq> {}; (\<forall>m\<in>S. \<exists>n\<in>S. m < (n::nat)) \<rbrakk> \<Longrightarrow> \<forall>m. \<exists>n\<in>S. m \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<noteq> {}; \<forall>m\<in>S. \<exists>n\<in>S. m < n\<rbrakk> \<Longrightarrow> \<forall>m. \<exists>n\<in>S. m \<le> n
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>S \<noteq> {}; \<forall>m\<in>S. \<exists>n\<in>S. m < n\<rbrakk> \<Longrightarrow> \<exists>n\<in>S. m \<le> n
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>S \<noteq> {}; \<forall>m\<in>S. \<exists>n\<in>S. m < n\<rbrakk> \<Longrightarrow> \<exists>n\<in>S. 0 \<le> n
 2. \<And>m n. \<lbrakk>S \<noteq> {}; \<forall>m\<in>S. \<exists>n\<in>S. m < n; \<exists>na\<in>S. n \<le> na\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n. \<lbrakk>S \<noteq> {}; \<forall>m\<in>S. \<exists>n\<in>S. m < n; \<exists>na\<in>S. n \<le> na\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n na. \<lbrakk>S \<noteq> {}; \<forall>m\<in>S. \<exists>n\<in>S. m < n; na \<in> S; n \<le> na\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
[PROOF STEP]
apply (rename_tac n1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n n1. \<lbrakk>S \<noteq> {}; \<forall>m\<in>S. \<exists>n\<in>S. m < n; n1 \<in> S; n \<le> n1\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
[PROOF STEP]
apply (erule_tac x=n1 in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n n1. \<lbrakk>S \<noteq> {}; n1 \<in> S; n \<le> n1; \<exists>n\<in>S. n1 < n\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
 2. \<And>m n n1. \<lbrakk>S \<noteq> {}; n1 \<in> S; n \<le> n1; n1 \<notin> S\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n n1. \<lbrakk>S \<noteq> {}; n1 \<in> S; n \<le> n1; n1 \<notin> S\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
 2. \<And>m n n1. \<lbrakk>S \<noteq> {}; n1 \<in> S; n \<le> n1; \<exists>n\<in>S. n1 < n\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n n1. \<lbrakk>S \<noteq> {}; n1 \<in> S; n \<le> n1; \<exists>n\<in>S. n1 < n\<rbrakk> \<Longrightarrow> \<exists>na\<in>S. Suc n \<le> na
[PROOF STEP]
apply (clarify, rename_tac x, rule_tac x=x in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n n1 x. \<lbrakk>S \<noteq> {}; n1 \<in> S; n \<le> n1; x \<in> S; n1 < x\<rbrakk> \<Longrightarrow> Suc n \<le> x
 2. \<And>m n n1 x. \<lbrakk>S \<noteq> {}; n1 \<in> S; n \<le> n1; x \<in> S; n1 < x\<rbrakk> \<Longrightarrow> x \<in> S
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma infinite_nat_iff_asc_chain: "
  S \<noteq> {} \<Longrightarrow> infinite S = (\<forall>m\<in>S. \<exists>n\<in>S. m < (n::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infinite S = (\<forall>m\<in>S. \<exists>n\<in>S. m < n)
[PROOF STEP]
by (metis Max_in infinite_nat_iff_unbounded not_greater_Max)


[STATEMENT]
lemma infinite_imp_asc_chain: "infinite S \<Longrightarrow> \<forall>m\<in>S. \<exists>n\<in>S. m < (n::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite S \<Longrightarrow> \<forall>m\<in>S. \<exists>n\<in>S. m < n
[PROOF STEP]
by (rule infinite_nat_iff_asc_chain[THEN iffD1, OF infinite_imp_nonempty])


[STATEMENT]
lemma inj_on_imp_infinite_image: "\<lbrakk> infinite A; inj_on f A \<rbrakk> \<Longrightarrow> infinite (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>infinite A; inj_on f A\<rbrakk> \<Longrightarrow> infinite (f ` A)
[PROOF STEP]
apply (frule card_image)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>infinite A; inj_on f A; card (f ` A) = card A\<rbrakk> \<Longrightarrow> infinite (f ` A)
[PROOF STEP]
apply (fastforce simp: card_eq_0_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inj_on_infinite_image_iff: "inj_on f A \<Longrightarrow> infinite (f ` A) = infinite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A \<Longrightarrow> infinite (f ` A) = infinite A
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj_on f A; infinite (f ` A)\<rbrakk> \<Longrightarrow> infinite A
 2. \<lbrakk>inj_on f A; infinite A\<rbrakk> \<Longrightarrow> infinite (f ` A)
[PROOF STEP]
apply (rule ccontr, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; infinite A\<rbrakk> \<Longrightarrow> infinite (f ` A)
[PROOF STEP]
apply (rule inj_on_imp_infinite_image, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inj_on_finite_image_iff: "inj_on f A \<Longrightarrow> finite (f ` A) = finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A \<Longrightarrow> finite (f ` A) = finite A
[PROOF STEP]
by (drule inj_on_infinite_image_iff, simp)


[STATEMENT]
lemma nat_ex_greater_finite_Max_conv: "
  A \<noteq> {} \<Longrightarrow> (\<exists>x\<in>A. (n::nat) < x) = (finite A \<longrightarrow> n < Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> (\<exists>x\<in>A. n < x) = (finite A \<longrightarrow> n < Max A)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; \<exists>x\<in>A. n < x\<rbrakk> \<Longrightarrow> finite A \<longrightarrow> n < Max A
 2. \<lbrakk>A \<noteq> {}; finite A \<longrightarrow> n < Max A\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. n < x
[PROOF STEP]
apply (blast intro: order_less_le_trans Max_ge)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A \<longrightarrow> n < Max A\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. n < x
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; finite A \<longrightarrow> n < Max A; finite A\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. n < x
 2. \<lbrakk>A \<noteq> {}; finite A \<longrightarrow> n < Max A; infinite A\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. n < x
[PROOF STEP]
apply (blast intro: Max_in)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A \<longrightarrow> n < Max A; infinite A\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. n < x
[PROOF STEP]
apply (drule infinite_nat_iff_unbounded[THEN iffD1, rule_format, of _ n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A \<longrightarrow> n < Max A; \<exists>na>n. na \<in> A\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. n < x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma disjoint_iff_in_not_in1: "(A \<inter> B = {}) = (\<forall>x\<in>A. x \<notin> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<inter> B = {}) = (\<forall>x\<in>A. x \<notin> B)
[PROOF STEP]
by blast


[STATEMENT]
lemma disjoint_iff_in_not_in2: "(A \<inter> B = {}) = (\<forall>x\<in>B. x \<notin> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<inter> B = {}) = (\<forall>x\<in>B. x \<notin> A)
[PROOF STEP]
by blast


[STATEMENT]
lemma disjoint_in_Un: "
  \<lbrakk> A \<inter> B = {}; x \<in> A \<union> B \<rbrakk> \<Longrightarrow> x \<notin> A \<or> x \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B = {}; x \<in> A \<union> B\<rbrakk> \<Longrightarrow> x \<notin> A \<or> x \<notin> B
[PROOF STEP]
by (blast intro: disjoint_iff_in_not_in1[THEN iffD1])+


[STATEMENT]
lemma partition_Union: "A \<subseteq> \<Union>C \<Longrightarrow> (\<Union>c\<in>C. A \<inter> c) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> \<Union> C \<Longrightarrow> \<Union> ((\<inter>) A ` C) = A
[PROOF STEP]
by blast


[STATEMENT]
lemma disjoint_partition_Int: "
  \<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<Longrightarrow>
  \<forall>a1\<in>{A \<inter> c| c. c \<in> C}. \<forall>a2\<in>{A \<inter> c| c. c \<in> C}.
    a1 \<noteq> a2 \<longrightarrow> a1 \<inter> a2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<Longrightarrow> \<forall>a1\<in>{A \<inter> c |c. c \<in> C}. \<forall>a2\<in>{A \<inter> c |c. c \<in> C}. a1 \<noteq> a2 \<longrightarrow> a1 \<inter> a2 = {}
[PROOF STEP]
by blast


[STATEMENT]
lemma "{f x |x. x \<in> A} = (\<Union>x\<in>A. {f x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f x |x. x \<in> A} = (\<Union>x\<in>A. {f x})
[PROOF STEP]
by fastforce


[STATEMENT]
lemma card_partition: "
  \<lbrakk> finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {} \<rbrakk> \<Longrightarrow>
  card (\<Union>C) = k * card C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}\<rbrakk> \<Longrightarrow> card (\<Union> C) = k * card C
[PROOF STEP]
by (metis card.infinite card_partition finite_Union mult_eq_if)


[STATEMENT]
lemma subset_image_Int: "A \<subseteq> B \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B
[PROOF STEP]
by (simp only: Int_absorb2 image_mono)


[STATEMENT]
lemma image_diff_disjoint_image_Int: "
  \<lbrakk> f ` (A - B) \<inter> f ` B = {} \<rbrakk> \<Longrightarrow>
  f ` (A \<inter> B) = f ` A \<inter> f ` B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (A - B) \<inter> f ` B = {} \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f ` (A - B) \<inter> f ` B = {} \<Longrightarrow> (x \<in> f ` (A \<inter> B)) = (x \<in> f ` A \<inter> f ` B)
[PROOF STEP]
apply (simp add: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f ` (A - B) \<inter> f ` B = {} \<Longrightarrow> (\<exists>xa\<in>A \<inter> B. x = f xa) = ((\<exists>xa\<in>A. x = f xa) \<and> (\<exists>xa\<in>B. x = f xa))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subset_imp_Int_subset1: "A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C
[PROOF STEP]
by (rule subset_trans[of _ "C \<inter> B", OF Int_mono, OF _ subset_refl Int_lower1])


[STATEMENT]
lemma subset_imp_Int_subset2: "B \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C
[PROOF STEP]
by (simp only: Int_commute[of A], rule subset_imp_Int_subset1)


[STATEMENT]
lemma image_add_atLeast:
  "(\<lambda>n::nat. n+k) ` {i..} = {i+k..}" (is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. n + k) ` {i..} = {i + k..}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>n. n + k) ` {i..} \<subseteq> {i + k..}
 2. {i + k..} \<subseteq> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
show "?A \<subseteq> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. n + k) ` {i..} \<subseteq> {i + k..}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<lambda>n. n + k) ` {i..} \<subseteq> {i + k..}

goal (1 subgoal):
 1. {i + k..} \<subseteq> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i + k..} \<subseteq> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
show "?B \<subseteq> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i + k..} \<subseteq> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {i + k..} \<Longrightarrow> x \<in> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {i + k..} \<Longrightarrow> x \<in> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
assume a: "n : ?B"
[PROOF STATE]
proof (state)
this:
n \<in> {i + k..}

goal (1 subgoal):
 1. \<And>x. x \<in> {i + k..} \<Longrightarrow> x \<in> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
hence "n - k \<in> {i..}"
[PROOF STATE]
proof (prove)
using this:
n \<in> {i + k..}

goal (1 subgoal):
 1. n - k \<in> {i..}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n - k \<in> {i..}

goal (1 subgoal):
 1. \<And>x. x \<in> {i + k..} \<Longrightarrow> x \<in> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n - k \<in> {i..}

goal (1 subgoal):
 1. \<And>x. x \<in> {i + k..} \<Longrightarrow> x \<in> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
have "n = (n - k) + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = n - k + k
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
n \<in> {i + k..}

goal (1 subgoal):
 1. n = n - k + k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = n - k + k

goal (1 subgoal):
 1. \<And>x. x \<in> {i + k..} \<Longrightarrow> x \<in> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n - k \<in> {i..}
n = n - k + k
[PROOF STEP]
show "n \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
n - k \<in> {i..}
n = n - k + k

goal (1 subgoal):
 1. n \<in> (\<lambda>n. n + k) ` {i..}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<in> (\<lambda>n. n + k) ` {i..}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{i + k..} \<subseteq> (\<lambda>n. n + k) ` {i..}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma image_add_atMost:
  "(\<lambda>n::nat. n+k) ` {..i} = {k..i+k}" (is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. n + k) ` {..i} = {k..i + k}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. n + k) ` {..i} = {k..i + k}
[PROOF STEP]
have s1: "{..i} = {0..i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..i} = {0..i}
[PROOF STEP]
by (simp add: set_interval_defs)
[PROOF STATE]
proof (state)
this:
{..i} = {0..i}

goal (1 subgoal):
 1. (\<lambda>n. n + k) ` {..i} = {k..i + k}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{..i} = {0..i}
[PROOF STEP]
show "?A = ?B"
[PROOF STATE]
proof (prove)
using this:
{..i} = {0..i}

goal (1 subgoal):
 1. (\<lambda>n. n + k) ` {..i} = {k..i + k}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. n + k) ` {..i} = {k..i + k}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atMost_atLeastAtMost_0_conv: "{..i::nat} = {0..i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..i} = {0..i}
[PROOF STEP]
by (simp add: set_interval_defs)


[STATEMENT]
lemma atLeastAtMost_subset_atMost: "(k::'a::order) \<le> k' \<Longrightarrow> {l..k} \<subseteq> {..k'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> k' \<Longrightarrow> {l..k} \<subseteq> {..k'}
[PROOF STEP]
by (simp)


[STATEMENT]
lemma lessThan_insert: "insert (n::'a::order) {..<n} = {..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert n {..<n} = {..n}
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> insert n {..<n}) = (x \<in> {..n})
[PROOF STEP]
apply (clarsimp simp add: order_le_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (x = n \<or> x < n) = (x < n \<or> x = n)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma atMost_remove: "{..n} - {(n::'a::order)} = {..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..n} - {n} = {..<n}
[PROOF STEP]
apply (simp only: lessThan_insert[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert n {..<n} - {n} = {..<n}
[PROOF STEP]
apply (rule Diff_insert_absorb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<notin> {..<n}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma atMost_lessThan_conv: "{..n} = {..<Suc n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..n} = {..<Suc n}
[PROOF STEP]
by (simp only: atMost_def lessThan_def less_Suc_eq_le)


[STATEMENT]
lemma atLeastAtMost_atLeastLessThan_conv: "{l..u} = {l..<Suc u}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {l..u} = {l..<Suc u}
[PROOF STEP]
by (simp only: atLeastAtMost_def atLeastLessThan_def atMost_lessThan_conv)


[STATEMENT]
lemma atLeast_greaterThan_conv: "{Suc n..} = {n<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Suc n..} = {n<..}
[PROOF STEP]
by (simp only: atLeast_def greaterThan_def Suc_le_eq)


[STATEMENT]
lemma atLeastAtMost_greaterThanAtMost_conv: "{Suc l..u} = {l<..u}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Suc l..u} = {l<..u}
[PROOF STEP]
by (simp only: greaterThanAtMost_def atLeastAtMost_def atLeast_greaterThan_conv)


[STATEMENT]
lemma finite_subset_atLeastAtMost: "finite A \<Longrightarrow> A \<subseteq> {Min A..Max A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> A \<subseteq> {Min A..Max A}
[PROOF STEP]
by (simp add: subset_eq)


[STATEMENT]
lemma Max_le_imp_subset_atMost: "
  \<lbrakk> finite A;  Max A \<le> n \<rbrakk> \<Longrightarrow> A \<subseteq> {..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A \<le> n\<rbrakk> \<Longrightarrow> A \<subseteq> {..n}
[PROOF STEP]
by (rule subset_trans[OF finite_subset_atLeastAtMost atLeastAtMost_subset_atMost])


[STATEMENT]
lemma subset_atMost_imp_Max_le:"
  \<lbrakk> finite A; A \<noteq> {}; A \<subseteq> {..n} \<rbrakk> \<Longrightarrow> Max A \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; A \<subseteq> {..n}\<rbrakk> \<Longrightarrow> Max A \<le> n
[PROOF STEP]
by (simp add: subset_iff)


[STATEMENT]
lemma subset_atMost_Max_le_conv: "
  \<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (A \<subseteq> {..n}) = (Max A \<le> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> (A \<subseteq> {..n}) = (Max A \<le> n)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite A; A \<noteq> {}; A \<subseteq> {..n}\<rbrakk> \<Longrightarrow> Max A \<le> n
 2. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> n\<rbrakk> \<Longrightarrow> A \<subseteq> {..n}
[PROOF STEP]
apply (blast intro: subset_atMost_imp_Max_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> n\<rbrakk> \<Longrightarrow> A \<subseteq> {..n}
[PROOF STEP]
apply (rule Max_le_imp_subset_atMost, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMin_greaterThan: "iMin {n<..} = Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMin {n<..} = Suc n
[PROOF STEP]
by (simp only: atLeast_Suc_greaterThan[symmetric] iMin_atLeast)


[STATEMENT]
lemma iMin_atMost: "iMin {..(n::nat)} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMin {..n} = 0
[PROOF STEP]
by (rule iMin_equality, simp_all)


[STATEMENT]
lemma iMin_lessThan: "0 < n \<Longrightarrow> iMin {..<(n::nat)} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> iMin {..<n} = 0
[PROOF STEP]
by (rule iMin_equality, simp_all)


[STATEMENT]
lemma Max_atMost: "Max {..(n::nat)} = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max {..n} = n
[PROOF STEP]
by (rule Max_equality[OF _ finite_atMost], simp_all)


[STATEMENT]
lemma Max_lessThan: "0 < n \<Longrightarrow> Max {..<n} = n - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> Max {..<n} = n - Suc 0
[PROOF STEP]
by (rule Max_equality[OF _ finite_lessThan], simp_all)


[STATEMENT]
lemma iMin_atLeastLessThan: "m < n \<Longrightarrow> iMin {m..<n} = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> iMin {m..<n} = m
[PROOF STEP]
by (rule iMin_equality, simp_all)


[STATEMENT]
lemma Max_atLeastLessThan: "m < n \<Longrightarrow> Max {m..<n} = n - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> Max {m..<n} = n - Suc 0
[PROOF STEP]
by (rule Max_equality[OF _ finite_atLeastLessThan], simp_all add: less_imp_le_pred)


[STATEMENT]
lemma iMin_greaterThanLessThan: "Suc m < n \<Longrightarrow> iMin {m<..<n} = Suc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc m < n \<Longrightarrow> iMin {m<..<n} = Suc m
[PROOF STEP]
by (simp only: atLeastSucLessThan_greaterThanLessThan[symmetric] iMin_atLeastLessThan)


[STATEMENT]
lemma Max_greaterThanLessThan: "Suc m < n \<Longrightarrow> Max {m<..<n} = n - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc m < n \<Longrightarrow> Max {m<..<n} = n - Suc 0
[PROOF STEP]
by (simp only: atLeastSucLessThan_greaterThanLessThan[symmetric] Max_atLeastLessThan)


[STATEMENT]
lemma iMin_greaterThanAtMost: "m < n \<Longrightarrow> iMin {m<..n} = Suc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> iMin {m<..n} = Suc m
[PROOF STEP]
by (simp only: atLeastSucAtMost_greaterThanAtMost[symmetric] atLeastLessThanSuc_atLeastAtMost[symmetric] iMin_atLeastLessThan)


[STATEMENT]
lemma Max_greaterThanAtMost: "m < n \<Longrightarrow> Max {m<..(n::nat)} = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> Max {m<..n} = n
[PROOF STEP]
by (simp add: atLeastSucAtMost_greaterThanAtMost[symmetric] atLeastLessThanSuc_atLeastAtMost[symmetric] Max_atLeastLessThan)


[STATEMENT]
lemma iMin_atLeastAtMost: "m \<le> n \<Longrightarrow> iMin {m..n} = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> iMin {m..n} = m
[PROOF STEP]
by (rule iMin_equality, simp_all)


[STATEMENT]
lemma Max_atLeastAtMost: "m \<le> n \<Longrightarrow> Max {m..(n::nat)} = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> Max {m..n} = n
[PROOF STEP]
by (rule Max_equality[OF _ finite_atLeastAtMost], simp_all)


[STATEMENT]
lemma infinite_atLeast: "infinite {(n::nat)..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {n..}
[PROOF STEP]
by (rule unbounded_k_infinite[of n], fastforce)


[STATEMENT]
lemma infinite_greaterThan: "infinite {(n::nat)<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {n<..}
[PROOF STEP]
by (simp add: atLeast_Suc_greaterThan[symmetric] infinite_atLeast)


[STATEMENT]
lemma infinite_atLeast_int: "infinite {(n::int)..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {n..}
[PROOF STEP]
apply (rule_tac f="\<lambda>x. nat (x - n)" in inj_on_infinite_image_iff[THEN iffD1, rule_format])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inj_on (\<lambda>x. nat (x - n)) {n..}
 2. infinite ((\<lambda>x. nat (x - n)) ` {n..})
[PROOF STEP]
apply (fastforce simp: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite ((\<lambda>x. nat (x - n)) ` {n..})
[PROOF STEP]
apply (rule_tac t="((\<lambda>x. nat (x - n)) ` {n..})" and s="{0..}" in subst)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {0..} = (\<lambda>x. nat (x - n)) ` {n..}
 2. infinite {0..}
[PROOF STEP]
apply (simp add: set_eq_iff image_iff Bex_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x. \<exists>xa\<ge>n. x = nat (xa - n)
 2. infinite {0..}
[PROOF STEP]
apply (clarify, rename_tac n1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n1. \<exists>x\<ge>n. n1 = nat (x - n)
 2. infinite {0..}
[PROOF STEP]
apply (rule_tac x="n + int n1" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n1. n \<le> n + int n1 \<and> n1 = nat (n + int n1 - n)
 2. infinite {0..}
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma infinite_greaterThan_int: "infinite {(n::int)<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {n<..}
[PROOF STEP]
apply (simp only: atLeast_remove[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite ({n..} - {n})
[PROOF STEP]
apply (rule Diff_infinite_finite[OF singleton_finite])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {n..}
[PROOF STEP]
apply (rule infinite_atLeast_int)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma infinite_atMost_int: "infinite {..(n::int)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {..n}
[PROOF STEP]
apply (rule_tac f="\<lambda>x. n - x" in inj_on_infinite_image_iff[THEN iffD1, rule_format])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inj_on ((-) n) {..n}
 2. infinite ((-) n ` {..n})
[PROOF STEP]
apply (simp add: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite ((-) n ` {..n})
[PROOF STEP]
apply (rule_tac t="((-) n ` {..n})" and s="{0..}" in subst)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {0..} = (-) n ` {..n}
 2. infinite {0..}
[PROOF STEP]
apply (simp add: set_eq_iff image_iff Bex_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {0..}
[PROOF STEP]
apply (rule infinite_atLeast_int)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma infinite_lessThan_int: "infinite {..<(n::int)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {..<n}
[PROOF STEP]
apply (simp only: atMost_remove[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite ({..n} - {n})
[PROOF STEP]
apply (rule Diff_infinite_finite[OF singleton_finite])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {..n}
[PROOF STEP]
apply (rule infinite_atMost_int)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_singleton: "(\<Sum>x\<in>{a}. f x) = f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {a} = f a
[PROOF STEP]
by simp


[STATEMENT]
lemma card_singleton: "card {a} = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {a} = Suc 0
[PROOF STEP]
by simp


[STATEMENT]
lemma card_cartesian_product_singleton_right: "card (A \<times> {x}) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (A \<times> {x}) = card A
[PROOF STEP]
by (simp add: card_cartesian_product)


[STATEMENT]
lemma card_1_imp_singleton: "card A = Suc 0 \<Longrightarrow> (\<exists>a. A = {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A = Suc 0 \<Longrightarrow> \<exists>a. A = {a}
[PROOF STEP]
by (metis card_eq_SucD)


[STATEMENT]
lemma card_1_singleton_conv: "(card A = Suc 0) = (\<exists>a. A = {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (card A = Suc 0) = (\<exists>a. A = {a})
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card A = Suc 0 \<Longrightarrow> \<exists>a. A = {a}
 2. \<exists>a. A = {a} \<Longrightarrow> card A = Suc 0
[PROOF STEP]
apply (simp add: card_1_imp_singleton)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. A = {a} \<Longrightarrow> card A = Suc 0
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma card_gr0_imp_finite: "0 < card A \<Longrightarrow> finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < card A \<Longrightarrow> finite A
[PROOF STEP]
by (rule ccontr, simp)


[STATEMENT]
lemma card_gr0_imp_not_empty: "(0 < card A) \<Longrightarrow> A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < card A \<Longrightarrow> A \<noteq> {}
[PROOF STEP]
by (rule ccontr, simp)


[STATEMENT]
lemma not_empty_card_gr0_conv: "finite A \<Longrightarrow> (A \<noteq> {}) = (0 < card A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> (A \<noteq> {}) = (0 < card A)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma nat_card_le_Max: "card (A::nat set) \<le> Suc (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A \<le> Suc (Max A)
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite A \<Longrightarrow> card A \<le> Suc (Max A)
 2. infinite A \<Longrightarrow> card A \<le> Suc (Max A)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. infinite A \<Longrightarrow> card A \<le> Suc (Max A)
 2. finite A \<Longrightarrow> card A \<le> Suc (Max A)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> card A \<le> Suc (Max A)
[PROOF STEP]
apply (cut_tac card_mono[OF finite_atMost, of A "Max A"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite A; card A \<le> card {..Max A}\<rbrakk> \<Longrightarrow> card A \<le> Suc (Max A)
 2. finite A \<Longrightarrow> A \<subseteq> {..Max A}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> A \<subseteq> {..Max A}
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Int_card1: "finite A \<Longrightarrow> card (A \<inter> B) \<le> card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> card (A \<inter> B) \<le> card A
[PROOF STEP]
by (rule card_mono, simp_all)


[STATEMENT]
lemma Int_card2: "finite B \<Longrightarrow> card (A \<inter> B) \<le> card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite B \<Longrightarrow> card (A \<inter> B) \<le> card B
[PROOF STEP]
by (simp only: Int_commute[of A], rule Int_card1)


[STATEMENT]
lemma Un_card1: "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> card A \<le> card (A \<union> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> card A \<le> card (A \<union> B)
[PROOF STEP]
by (rule card_mono, simp_all)


[STATEMENT]
lemma Un_card2: "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> card B \<le> card (A \<union> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> card B \<le> card (A \<union> B)
[PROOF STEP]
by (simp only: Un_commute[of A], rule Un_card1)


[STATEMENT]
lemma card_Un_conv: "
  \<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow>
  card (A \<union> B) = card A + card B - card (A \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> card (A \<union> B) = card A + card B - card (A \<inter> B)
[PROOF STEP]
by (simp only: card_Un_Int diff_add_inverse2)


[STATEMENT]
lemma card_Int_conv: "
  \<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow>
  card (A \<inter> B) = card A + card B - card (A \<union> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> card (A \<inter> B) = card A + card B - card (A \<union> B)
[PROOF STEP]
by (simp only: card_Un_Int diff_add_inverse)


[STATEMENT]
lemma pigeonhole_principle[rule_format]: "
  card (f ` A) < card A \<longrightarrow> (\<exists>x\<in>A. \<exists>y\<in>A. x \<noteq> y \<and> f x = f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (f ` A) < card A \<longrightarrow> (\<exists>x\<in>A. \<exists>y\<in>A. x \<noteq> y \<and> f x = f y)
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite A \<Longrightarrow> card (f ` A) < card A \<longrightarrow> (\<exists>x\<in>A. \<exists>y\<in>A. x \<noteq> y \<and> f x = f y)
 2. infinite A \<Longrightarrow> card (f ` A) < card A \<longrightarrow> (\<exists>x\<in>A. \<exists>y\<in>A. x \<noteq> y \<and> f x = f y)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. infinite A \<Longrightarrow> card (f ` A) < card A \<longrightarrow> (\<exists>x\<in>A. \<exists>y\<in>A. x \<noteq> y \<and> f x = f y)
 2. finite A \<Longrightarrow> card (f ` A) < card A \<longrightarrow> (\<exists>x\<in>A. \<exists>y\<in>A. x \<noteq> y \<and> f x = f y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> card (f ` A) < card A \<longrightarrow> (\<exists>x\<in>A. \<exists>y\<in>A. x \<noteq> y \<and> f x = f y)
[PROOF STEP]
apply (rule finite.induct[of A])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite A \<Longrightarrow> finite A
 2. finite A \<Longrightarrow> card (f ` {}) < card {} \<longrightarrow> (\<exists>x\<in>{}. \<exists>y\<in>{}. x \<noteq> y \<and> f x = f y)
 3. \<And>Aa a. \<lbrakk>finite A; finite Aa; card (f ` Aa) < card Aa \<longrightarrow> (\<exists>x\<in>Aa. \<exists>y\<in>Aa. x \<noteq> y \<and> f x = f y)\<rbrakk> \<Longrightarrow> card (f ` insert a Aa) < card (insert a Aa) \<longrightarrow> (\<exists>x\<in>insert a Aa. \<exists>y\<in>insert a Aa. x \<noteq> y \<and> f x = f y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Aa a. \<lbrakk>finite A; finite Aa; card (f ` Aa) < card Aa \<longrightarrow> (\<exists>x\<in>Aa. \<exists>y\<in>Aa. x \<noteq> y \<and> f x = f y)\<rbrakk> \<Longrightarrow> card (insert (f a) (f ` Aa)) < card (insert a Aa) \<longrightarrow> (\<exists>y\<in>Aa. a \<noteq> y \<and> f a = f y) \<or> (\<exists>x\<in>Aa. x \<noteq> a \<and> f x = f a \<or> (\<exists>y\<in>Aa. x \<noteq> y \<and> f x = f y))
[PROOF STEP]
apply (clarsimp, rename_tac A1 a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; card (f ` A1) < card A1 \<longrightarrow> (\<exists>x\<in>A1. \<exists>y\<in>A1. x \<noteq> y \<and> f x = f y); card (insert (f a) (f ` A1)) < card (insert a A1); \<forall>x\<in>A1. (x = a \<or> f x \<noteq> f a) \<and> (\<forall>y\<in>A1. x = y \<or> f x \<noteq> f y)\<rbrakk> \<Longrightarrow> \<exists>y\<in>A1. a \<noteq> y \<and> f a = f y
[PROOF STEP]
apply (case_tac "a \<in> A1", force simp: insert_absorb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; card (f ` A1) < card A1 \<longrightarrow> (\<exists>x\<in>A1. \<exists>y\<in>A1. x \<noteq> y \<and> f x = f y); card (insert (f a) (f ` A1)) < card (insert a A1); \<forall>x\<in>A1. (x = a \<or> f x \<noteq> f a) \<and> (\<forall>y\<in>A1. x = y \<or> f x \<noteq> f y); a \<notin> A1\<rbrakk> \<Longrightarrow> \<exists>y\<in>A1. a \<noteq> y \<and> f a = f y
[PROOF STEP]
apply (case_tac "f a \<in> f ` A1", fastforce+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_cnf_remove: "atoms_of_cnf (restrict_cnf_atom a v c) \<subseteq>
  atoms_of_cnf c - {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_of_cnf (restrict_cnf_atom a v c) \<subseteq> atoms_of_cnf c - {a}
[PROOF STEP]
unfolding  restrict_cnf_atom_def atoms_of_cnf_alt lit_atoms_cases make_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> ((`) (\<lambda>xa. case xa of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` {ca - {case \<not> v of True \<Rightarrow> a\<^sup>+ | False \<Rightarrow> a\<inverse>} |ca. ca \<in> c \<and> (case v of True \<Rightarrow> a\<^sup>+ | False \<Rightarrow> a\<inverse>) \<notin> ca}) \<subseteq> \<Union> ((`) (\<lambda>xa. case xa of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` c) - {a}
[PROOF STEP]
by (force split: literal.splits bool.splits)


[STATEMENT]
lemma cnf_substitution_lemma:
  "cnf_semantics A (restrict_cnf_atom a v S) = cnf_semantics (A(a := v)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf_semantics A (restrict_cnf_atom a v S) = cnf_semantics (A(a := v)) S
[PROOF STEP]
unfolding restrict_cnf_atom_def cnf_semantics_def clause_semantics_def lit_semantics_cases make_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>C\<in>{c - {case \<not> v of True \<Rightarrow> a\<^sup>+ | False \<Rightarrow> a\<inverse>} |c. c \<in> S \<and> (case v of True \<Rightarrow> a\<^sup>+ | False \<Rightarrow> a\<inverse>) \<notin> c}. \<exists>L\<in>C. case L of x\<^sup>+ \<Rightarrow> A x | x2ca\<inverse> \<Rightarrow> \<not> A x2ca) = (\<forall>C\<in>S. \<exists>L\<in>C. case L of x\<^sup>+ \<Rightarrow> (A(a := v)) x | x2ca\<inverse> \<Rightarrow> \<not> (A(a := v)) x2ca)
[PROOF STEP]
apply (clarsimp split: bool.splits literal.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<longrightarrow> (\<forall>C. (\<exists>c. C = c - {a\<inverse>} \<and> c \<in> S \<and> a\<^sup>+ \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2))) = (\<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. (x2 = a \<longrightarrow> L \<noteq> a\<inverse>) \<and> (x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)))) \<and> (\<not> v \<longrightarrow> (\<forall>C. (\<exists>c. C = c - {a\<^sup>+} \<and> c \<in> S \<and> a\<inverse> \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2))) = (\<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>C. \<lbrakk>v; \<forall>C. (\<exists>c. C = c - {a\<inverse>} \<and> c \<in> S \<and> a\<^sup>+ \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)); C \<in> S\<rbrakk> \<Longrightarrow> \<exists>L\<in>C. (\<forall>x1. x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. (x2 = a \<longrightarrow> L \<noteq> a\<inverse>) \<and> (x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2))
 2. \<And>C c. \<lbrakk>v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. (x2 = a \<longrightarrow> L \<noteq> a\<inverse>) \<and> (x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)); c \<in> S; a\<^sup>+ \<notin> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c - {a\<inverse>}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
 3. \<And>C. \<lbrakk>\<not> v; \<forall>C. (\<exists>c. C = c - {a\<^sup>+} \<and> c \<in> S \<and> a\<inverse> \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)); C \<in> S\<rbrakk> \<Longrightarrow> \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)
 4. \<And>C c. \<lbrakk>\<not> v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2); c \<in> S; a\<inverse> \<notin> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c - {a\<^sup>+}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v; \<forall>C. (\<exists>c. C = c - {a\<inverse>} \<and> c \<in> S \<and> a\<^sup>+ \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)); s \<in> S\<rbrakk> \<Longrightarrow> \<exists>L\<in>s. (\<forall>x1. x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. (x2 = a \<longrightarrow> L \<noteq> a\<inverse>) \<and> (x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2))
[PROOF STEP]
by(fastforce elim!: allE[of _ "s - {Neg a}"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C c. \<lbrakk>v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. (x2 = a \<longrightarrow> L \<noteq> a\<inverse>) \<and> (x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)); c \<in> S; a\<^sup>+ \<notin> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c - {a\<inverse>}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
 2. \<And>C. \<lbrakk>\<not> v; \<forall>C. (\<exists>c. C = c - {a\<^sup>+} \<and> c \<in> S \<and> a\<inverse> \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)); C \<in> S\<rbrakk> \<Longrightarrow> \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)
 3. \<And>C c. \<lbrakk>\<not> v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2); c \<in> S; a\<inverse> \<notin> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c - {a\<^sup>+}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. (x2 = a \<longrightarrow> L \<noteq> a\<inverse>) \<and> (x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)); c_ \<in> S; a\<^sup>+ \<notin> c_\<rbrakk> \<Longrightarrow> \<exists>x\<in>c_ - {a\<inverse>}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
[PROOF STEP]
by (metis DiffI singletonD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> v; \<forall>C. (\<exists>c. C = c - {a\<^sup>+} \<and> c \<in> S \<and> a\<inverse> \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)); C \<in> S\<rbrakk> \<Longrightarrow> \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)
 2. \<And>C c. \<lbrakk>\<not> v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2); c \<in> S; a\<inverse> \<notin> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c - {a\<^sup>+}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> v; \<forall>C. (\<exists>c. C = c - {a\<^sup>+} \<and> c \<in> S \<and> a\<inverse> \<notin> c) \<longrightarrow> (\<exists>x\<in>C. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)); s \<in> S\<rbrakk> \<Longrightarrow> \<exists>L\<in>s. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2)
[PROOF STEP]
by(fastforce elim!: allE[of _ "s - {Pos a}"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C c. \<lbrakk>\<not> v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2); c \<in> S; a\<inverse> \<notin> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c - {a\<^sup>+}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> v; \<forall>C\<in>S. \<exists>L\<in>C. (\<forall>x1. (x1 = a \<longrightarrow> L \<noteq> a\<^sup>+) \<and> (x1 \<noteq> a \<longrightarrow> L = x1\<^sup>+ \<longrightarrow> A x1)) \<and> (\<forall>x2. x2 \<noteq> a \<longrightarrow> L = x2\<inverse> \<longrightarrow> \<not> A x2); c_ \<in> S; a\<inverse> \<notin> c_\<rbrakk> \<Longrightarrow> \<exists>x\<in>c_ - {a\<^sup>+}. (\<forall>x1. x = x1\<^sup>+ \<longrightarrow> A x1) \<and> (\<forall>x2. x = x2\<inverse> \<longrightarrow> \<not> A x2)
[PROOF STEP]
by (metis DiffI singletonD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_restrict: "finite S \<Longrightarrow> finite (restrict_cnf_atom a v S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> finite (restrict_cnf_atom a v S)
[PROOF STEP]
unfolding restrict_cnf_atom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> finite {c - {make_lit (\<not> v) a} |c. c \<in> S \<and> make_lit v a \<notin> c}
[PROOF STEP]
by(simp add: image_iff)


[STATEMENT]
lemma unrestrict_effects:
  "(\<lambda>c. if {make_lit (\<not>v) a} \<union> c \<in> S then {make_lit (\<not>v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
[PROOF STEP]
have "\<lbrakk>xa \<in> restrict_cnf_atom a v S; {make_lit (\<not> v) a} \<union> xa \<notin> S; x = xa\<rbrakk> \<Longrightarrow> xa \<in> S" for x xa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa \<in> restrict_cnf_atom a v S; {make_lit (\<not> v) a} \<union> xa \<notin> S; x = xa\<rbrakk> \<Longrightarrow> xa \<in> S
[PROOF STEP]
unfolding restrict_cnf_atom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa \<in> {c - {make_lit (\<not> v) a} |c. c \<in> S \<and> make_lit v a \<notin> c}; {make_lit (\<not> v) a} \<union> xa \<notin> S; x = xa\<rbrakk> \<Longrightarrow> xa \<in> S
[PROOF STEP]
using insert_Diff
[PROOF STATE]
proof (prove)
using this:
?a \<in> ?A \<Longrightarrow> insert ?a (?A - {?a}) = ?A

goal (1 subgoal):
 1. \<lbrakk>xa \<in> {c - {make_lit (\<not> v) a} |c. c \<in> S \<and> make_lit v a \<notin> c}; {make_lit (\<not> v) a} \<union> xa \<notin> S; x = xa\<rbrakk> \<Longrightarrow> xa \<in> S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?xa \<in> restrict_cnf_atom a v S; {make_lit (\<not> v) a} \<union> ?xa \<notin> S; ?x = ?xa\<rbrakk> \<Longrightarrow> ?xa \<in> S

goal (1 subgoal):
 1. (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
[PROOF STEP]
hence "x \<in> (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<Longrightarrow> x \<in> S" for x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xa \<in> restrict_cnf_atom a v S; {make_lit (\<not> v) a} \<union> ?xa \<notin> S; ?x = ?xa\<rbrakk> \<Longrightarrow> ?xa \<in> S

goal (1 subgoal):
 1. x \<in> (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<Longrightarrow> x \<in> S
[PROOF STEP]
unfolding image_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xa \<in> restrict_cnf_atom a v S; {make_lit (\<not> v) a} \<union> ?xa \<notin> S; ?x = ?xa\<rbrakk> \<Longrightarrow> ?xa \<in> S

goal (1 subgoal):
 1. \<exists>xa\<in>restrict_cnf_atom a v S. x = (if {make_lit (\<not> v) a} \<union> xa \<in> S then {make_lit (\<not> v) a} \<union> xa else xa) \<Longrightarrow> x \<in> S
[PROOF STEP]
by(elim bexE) simp
[PROOF STATE]
proof (state)
this:
?x \<in> (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<Longrightarrow> ?x \<in> S

goal (1 subgoal):
 1. (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<Longrightarrow> ?x \<in> S

goal (1 subgoal):
 1. (\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma can_cope_with_unrestrict_effects:
  assumes pr: "S \<turnstile> \<box>"
  assumes su: "S \<subseteq> T"
  shows "\<exists>R \<subseteq> {make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
from Resolution_taint_assumptions[where D="{make_lit v a}"]
[PROOF STATE]
proof (chain)
picking this:
?S \<union> ?T \<turnstile> ?C \<Longrightarrow> \<exists>R\<subseteq>{make_lit v a}. (\<union>) {make_lit v a} ` ?S \<union> ?T \<turnstile> R \<union> ?C
[PROOF STEP]
have taint: "\<Gamma> \<union> \<Lambda> \<turnstile> \<box> \<Longrightarrow> \<exists>R\<subseteq>{make_lit v a}. insert (make_lit v a) ` \<Gamma> \<union> \<Lambda> \<turnstile> R"
    for \<Gamma> \<Lambda>
[PROOF STATE]
proof (prove)
using this:
?S \<union> ?T \<turnstile> ?C \<Longrightarrow> \<exists>R\<subseteq>{make_lit v a}. (\<union>) {make_lit v a} ` ?S \<union> ?T \<turnstile> R \<union> ?C

goal (1 subgoal):
 1. \<Gamma> \<union> \<Lambda> \<turnstile> \<box> \<Longrightarrow> \<exists>R\<subseteq>{make_lit v a}. insert (make_lit v a) ` \<Gamma> \<union> \<Lambda> \<turnstile> R
[PROOF STEP]
by (metis image_cong insert_def sup_bot.right_neutral)
[PROOF STATE]
proof (state)
this:
?\<Gamma> \<union> ?\<Lambda> \<turnstile> \<box> \<Longrightarrow> \<exists>R\<subseteq>{make_lit v a}. insert (make_lit v a) ` ?\<Gamma> \<union> ?\<Lambda> \<turnstile> R

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
have S: "S = {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S = {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n}

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
hence SI: "(\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S =
    (insert (make_lit v a) ` {c \<in> S. c \<in> n}) \<union> {c \<in> S. c \<notin> n}
  "
[PROOF STATE]
proof (prove)
using this:
S = {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n}

goal (1 subgoal):
 1. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S = insert (make_lit v a) ` {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S = insert (make_lit v a) ` {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n}

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
from pr
[PROOF STATE]
proof (chain)
picking this:
S \<turnstile> \<box>
[PROOF STEP]
have "\<exists>R \<subseteq> {make_lit v a}.
  (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S \<turnstile> R"
[PROOF STATE]
proof (prove)
using this:
S \<turnstile> \<box>

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S \<turnstile> R
[PROOF STEP]
apply(subst SI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<turnstile> \<box> \<Longrightarrow> \<exists>R\<subseteq>{make_lit v a}. insert (make_lit v a) ` {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n} \<turnstile> R
[PROOF STEP]
apply(subst(asm) S)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n} \<turnstile> \<box> \<Longrightarrow> \<exists>R\<subseteq>{make_lit v a}. insert (make_lit v a) ` {c \<in> S. c \<in> n} \<union> {c \<in> S. c \<notin> n} \<turnstile> R
[PROOF STEP]
apply(elim taint)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S \<turnstile> R

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S \<turnstile> R

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
using Resolution_weaken su
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` S \<turnstile> R
?S \<turnstile> ?D \<Longrightarrow> ?T \<union> ?S \<turnstile> ?D
S \<subseteq> T

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R
[PROOF STEP]
by (metis (no_types, lifting) image_Un sup.order_iff)
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>{make_lit v a}. (\<lambda>c. if c \<in> n then {make_lit v a} \<union> c else c) ` T \<turnstile> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unrestrict':
  fixes R :: "'a clause"
  assumes rp: "restrict_cnf_atom a v S \<turnstile> \<box>"
  shows "\<exists>R \<subseteq> {make_lit (\<not>v) a}. S \<turnstile> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
fix C :: "'a clause"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
fix k :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
from unrestrict_effects[of v a S]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
[PROOF STEP]
text\<open>The idea is that the restricted set lost some clauses, and that some others were crippled.
    So, there must be a set of clauses to heal and a set of clauses to reinsert to get the original.
    (Mind you, this is not exactly what is happening, because e.g. both
   @{term C} and @{term "{k\<inverse>} \<union> C"} might be in there and get reduced to one @{term C}.
    You then heal that @{term C} to @{term "{k\<inverse>} \<union> C"} and insert the shadowed @{term C}\<open>\<dots>\<close> Details.)
 \<close>
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
[PROOF STEP]
obtain n where S:
    "(\<lambda>c. if c \<in> n then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S

goal (1 subgoal):
 1. (\<And>n. (\<lambda>c. if c \<in> n then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using exI[where x="{c. {make_lit (\<not>v) a} \<union> c \<in> S}"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>c. if {make_lit (\<not> v) a} \<union> c \<in> S then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S
?P {c. {make_lit (\<not> v) a} \<union> c \<in> S} \<Longrightarrow> \<exists>x. ?P x

goal (1 subgoal):
 1. (\<And>n. (\<lambda>c. if c \<in> n then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>c. if c \<in> n then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
note  finite_restrict S
[PROOF STATE]
proof (state)
this:
finite ?S \<Longrightarrow> finite (restrict_cnf_atom ?a ?v ?S)
(\<lambda>c. if c \<in> n then {make_lit (\<not> v) a} \<union> c else c) ` restrict_cnf_atom a v S \<subseteq> S

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
using can_cope_with_unrestrict_effects[OF rp]
[PROOF STATE]
proof (prove)
using this:
restrict_cnf_atom a v S \<subseteq> ?T \<Longrightarrow> \<exists>R\<subseteq>{make_lit ?v ?a}. (\<lambda>c. if c \<in> ?n then {make_lit ?v ?a} \<union> c else c) ` ?T \<turnstile> R

goal (1 subgoal):
 1. \<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R
[PROOF STEP]
by (metis (no_types) S Resolution_weaken subset_refl sup.order_iff)
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>{make_lit (\<not> v) a}. S \<turnstile> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contr_sel_gt0: "sel_reasonable sf \<Longrightarrow> contr_sel sf x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sel_reasonable sf \<Longrightarrow> 0 < contr_sel sf x
[PROOF STEP]
unfolding contr_sel_def sel_reasonable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. sf x y \<le> 1 \<and> 0 < sf x y \<Longrightarrow> 0 < (if \<exists>xa. xa \<rightarrow>\<^bsub>T\<^esub> x then sf (THE xa. xa \<rightarrow>\<^bsub>T\<^esub> x) x else 1)
[PROOF STEP]
by simp


[STATEMENT]
lemma contr_sel_le1: "sel_reasonable sf \<Longrightarrow> contr_sel sf x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sel_reasonable sf \<Longrightarrow> contr_sel sf x \<le> 1
[PROOF STEP]
unfolding contr_sel_def sel_reasonable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. sf x y \<le> 1 \<and> 0 < sf x y \<Longrightarrow> (if \<exists>xa. xa \<rightarrow>\<^bsub>T\<^esub> x then sf (THE xa. xa \<rightarrow>\<^bsub>T\<^esub> x) x else 1) \<le> 1
[PROOF STEP]
by simp


[STATEMENT]
lemma nempty_if_not_fwd_conc: "\<not>forward_arcs (y#xs) \<Longrightarrow> xs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward_arcs (y # xs) \<Longrightarrow> xs \<noteq> []
[PROOF STEP]
by auto


[STATEMENT]
lemma len_gt1_if_not_fwd_conc: "\<not>forward_arcs (y#xs) \<Longrightarrow> length (y#xs) > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward_arcs (y # xs) \<Longrightarrow> 1 < length (y # xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma two_elems_if_not_fwd_conc: "\<not>forward_arcs (y#xs) \<Longrightarrow> \<exists>a b cs. a # b # cs = y#xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward_arcs (y # xs) \<Longrightarrow> \<exists>a b cs. a # b # cs = y # xs
[PROOF STEP]
by (metis forward_arcs.cases forward_arcs.simps(2))


[STATEMENT]
lemma hd_reach_all_if_nfwd_app_fwd:
  "\<lbrakk>\<not>forward_arcs (y#xs); forward_arcs (y#ys@xs); x \<in> set (y#ys@xs)\<rbrakk>
    \<Longrightarrow> hd (rev (y#ys@xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs); x \<in> set (y # ys @ xs)\<rbrakk> \<Longrightarrow> hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> x
[PROOF STEP]
using hd_reach_all_forward'[of "rev (y#ys@xs)"] len_gt1_if_not_fwd_conc forward_arcs_alt
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < length (rev (y # ys @ xs)); forward (rev (y # ys @ xs)); ?x \<in> set (rev (y # ys @ xs))\<rbrakk> \<Longrightarrow> hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> ?x
\<not> forward_arcs (?y # ?xs) \<Longrightarrow> 1 < length (?y # ?xs)
forward ?xs = forward_arcs (rev ?xs)

goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs); x \<in> set (y # ys @ xs)\<rbrakk> \<Longrightarrow> hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> x
[PROOF STEP]
by auto


[STATEMENT]
lemma hd_not_y_if_if_nfwd_app_fwd:
  assumes "\<not>forward_arcs (y#xs)" and "forward_arcs (y#ys@xs)"
  shows "hd (rev (y#ys@xs)) \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<noteq> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<noteq> y
[PROOF STEP]
obtain a where a_def: "a \<in> set (ys@xs)" "a \<rightarrow>\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> set (ys @ xs); a \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms Nil_is_append_conv forward_arcs.simps(3) neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
a \<in> set (ys @ xs)
a \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<noteq> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set (ys @ xs)
a \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
have "hd (rev (y#ys@xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> a"
[PROOF STATE]
proof (prove)
using this:
a \<in> set (ys @ xs)
a \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> a
[PROOF STEP]
using hd_reach_all_if_nfwd_app_fwd[OF assms]
[PROOF STATE]
proof (prove)
using this:
a \<in> set (ys @ xs)
a \<rightarrow>\<^bsub>T\<^esub> y
?x \<in> set (y # ys @ xs) \<Longrightarrow> hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> ?x

goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> a

goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<noteq> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> a

goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<noteq> y
[PROOF STEP]
using a_def(2) reachable1_not_reverse
[PROOF STATE]
proof (prove)
using this:
hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> a
a \<rightarrow>\<^bsub>T\<^esub> y
?x \<rightarrow>\<^sup>+\<^bsub>T\<^esub> ?y \<Longrightarrow> (?y, ?x) \<notin> (arcs_ends T)\<^sup>+

goal (1 subgoal):
 1. hd (rev (y # ys @ xs)) \<noteq> y
[PROOF STEP]
by (metis loopfree.adj_not_same reachable_adjI reachable_neq_reachable1)
[PROOF STATE]
proof (state)
this:
hd (rev (y # ys @ xs)) \<noteq> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hd_reach1_y_if_nfwd_app_fwd:
  "\<lbrakk>\<not>forward_arcs (y#xs); forward_arcs (y#ys@xs)\<rbrakk> \<Longrightarrow> hd (rev (y#ys@xs)) \<rightarrow>\<^sup>+\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs)\<rbrakk> \<Longrightarrow> hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>+\<^bsub>T\<^esub> y
[PROOF STEP]
using hd_not_y_if_if_nfwd_app_fwd hd_reach_all_if_nfwd_app_fwd
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> forward_arcs (?y # ?xs); forward_arcs (?y # ?ys @ ?xs)\<rbrakk> \<Longrightarrow> hd (rev (?y # ?ys @ ?xs)) \<noteq> ?y
\<lbrakk>\<not> forward_arcs (?y # ?xs); forward_arcs (?y # ?ys @ ?xs); ?x \<in> set (?y # ?ys @ ?xs)\<rbrakk> \<Longrightarrow> hd (rev (?y # ?ys @ ?xs)) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> ?x

goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs)\<rbrakk> \<Longrightarrow> hd (rev (y # ys @ xs)) \<rightarrow>\<^sup>+\<^bsub>T\<^esub> y
[PROOF STEP]
by auto


[STATEMENT]
lemma not_fwd_if_skip1:
  "\<lbrakk>\<not> forward_arcs (y#x#x'#xs); forward_arcs (x#x'#xs)\<rbrakk> \<Longrightarrow> \<not> forward_arcs (y#x'#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # x # x' # xs); forward_arcs (x # x' # xs)\<rbrakk> \<Longrightarrow> \<not> forward_arcs (y # x' # xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma fwd_arcs_conc_nlast_elem:
  assumes "forward_arcs xs" and "y \<in> set xs" and "y \<noteq> last xs"
  shows "forward_arcs (y#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
obtain as bs where as_def: "as @ y # bs = xs" "bs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as bs. \<lbrakk>as @ y # bs = xs; bs \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using split_list_not_last[OF assms(2,3)]
[PROOF STATE]
proof (prove)
using this:
\<exists>as bs. as @ y # bs = xs \<and> bs \<noteq> []

goal (1 subgoal):
 1. (\<And>as bs. \<lbrakk>as @ y # bs = xs; bs \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
as @ y # bs = xs
bs \<noteq> []

goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as @ y # bs = xs
bs \<noteq> []
[PROOF STEP]
have "forward_arcs (y#bs)"
[PROOF STATE]
proof (prove)
using this:
as @ y # bs = xs
bs \<noteq> []

goal (1 subgoal):
 1. forward_arcs (y # bs)
[PROOF STEP]
using assms(1) forward_arcs_split
[PROOF STATE]
proof (prove)
using this:
as @ y # bs = xs
bs \<noteq> []
forward_arcs xs
forward_arcs (?ys @ ?xs) \<Longrightarrow> forward_arcs ?xs

goal (1 subgoal):
 1. forward_arcs (y # bs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
forward_arcs (y # bs)

goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
forward_arcs (y # bs)
[PROOF STEP]
obtain x where x_def: "x \<in> set bs" "x \<rightarrow>\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
using this:
forward_arcs (y # bs)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> set bs; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using as_def(2)
[PROOF STATE]
proof (prove)
using this:
forward_arcs (y # bs)
bs \<noteq> []

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> set bs; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force intro: list.exhaust)
[PROOF STATE]
proof (state)
this:
x \<in> set bs
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set bs
x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
have "x \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
x \<in> set bs
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. x \<in> set xs
[PROOF STEP]
using as_def(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> set bs
x \<rightarrow>\<^bsub>T\<^esub> y
as @ y # bs = xs

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

goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs

goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
using assms(1) x_def(2) forward_arcs.elims(3)
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
forward_arcs xs
x \<rightarrow>\<^bsub>T\<^esub> y
\<lbrakk>\<not> forward_arcs ?x; \<And>x v va. \<lbrakk>?x = x # v # va; \<not> ((\<exists>y\<in>set (v # va). y \<rightarrow>\<^bsub>T\<^esub> x) \<and> forward_arcs (v # va))\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. forward_arcs (y # xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
forward_arcs (y # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fwd_app_nhead_elem: "\<lbrakk>forward xs; y \<in> set xs; y \<noteq> hd xs\<rbrakk> \<Longrightarrow> forward (xs@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>forward xs; y \<in> set xs; y \<noteq> hd xs\<rbrakk> \<Longrightarrow> forward (xs @ [y])
[PROOF STEP]
using fwd_arcs_conc_nlast_elem forward_arcs_alt
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>forward_arcs ?xs; ?y \<in> set ?xs; ?y \<noteq> last ?xs\<rbrakk> \<Longrightarrow> forward_arcs (?y # ?xs)
forward ?xs = forward_arcs (rev ?xs)

goal (1 subgoal):
 1. \<lbrakk>forward xs; y \<in> set xs; y \<noteq> hd xs\<rbrakk> \<Longrightarrow> forward (xs @ [y])
[PROOF STEP]
by (simp add: last_rev)


[STATEMENT]
lemma hd_last_not_fwd_arcs: "\<not>forward_arcs (x#xs@[x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward_arcs (x # xs @ [x])
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. forward_arcs (x # xs @ [x]) \<Longrightarrow> False
[PROOF STEP]
assume asm: "forward_arcs (x#xs@[x])"
[PROOF STATE]
proof (state)
this:
forward_arcs (x # xs @ [x])

goal (1 subgoal):
 1. forward_arcs (x # xs @ [x]) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
forward_arcs (x # xs @ [x])
[PROOF STEP]
obtain y where y_def: "y \<in> set (xs@[x])" "y \<rightarrow>\<^bsub>T\<^esub> x"
[PROOF STATE]
proof (prove)
using this:
forward_arcs (x # xs @ [x])

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> set (xs @ [x]); y \<rightarrow>\<^bsub>T\<^esub> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_is_Nil_conv forward_arcs.simps(3) no_back_arcs.cases)
[PROOF STATE]
proof (state)
this:
y \<in> set (xs @ [x])
y \<rightarrow>\<^bsub>T\<^esub> x

goal (1 subgoal):
 1. forward_arcs (x # xs @ [x]) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set (xs @ [x])
y \<rightarrow>\<^bsub>T\<^esub> x
[PROOF STEP]
have hd_in_verts: "hd (rev (xs @ [x])) \<in> verts T"
[PROOF STATE]
proof (prove)
using this:
y \<in> set (xs @ [x])
y \<rightarrow>\<^bsub>T\<^esub> x

goal (1 subgoal):
 1. hd (rev (xs @ [x])) \<in> verts T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd (rev (xs @ [x])) \<in> verts T

goal (1 subgoal):
 1. forward_arcs (x # xs @ [x]) \<Longrightarrow> False
[PROOF STEP]
have "forward_arcs (xs@[x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. forward_arcs (xs @ [x])
[PROOF STEP]
using asm forward_arcs_split[of "[x]" "xs@[x]"]
[PROOF STATE]
proof (prove)
using this:
forward_arcs (x # xs @ [x])
forward_arcs ([x] @ xs @ [x]) \<Longrightarrow> forward_arcs (xs @ [x])

goal (1 subgoal):
 1. forward_arcs (xs @ [x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
forward_arcs (xs @ [x])

goal (1 subgoal):
 1. forward_arcs (x # xs @ [x]) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
forward_arcs (xs @ [x])
[PROOF STEP]
have "x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
using this:
forward_arcs (xs @ [x])

goal (1 subgoal):
 1. x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> y
[PROOF STEP]
using hd_reach_all_forward[OF hd_in_verts] y_def forward_arcs_alt
[PROOF STATE]
proof (prove)
using this:
forward_arcs (xs @ [x])
\<lbrakk>forward (rev (xs @ [x])); ?x \<in> set (rev (xs @ [x]))\<rbrakk> \<Longrightarrow> hd (rev (xs @ [x])) \<rightarrow>\<^sup>*\<^bsub>T\<^esub> ?x
y \<in> set (xs @ [x])
y \<rightarrow>\<^bsub>T\<^esub> x
forward ?xs = forward_arcs (rev ?xs)

goal (1 subgoal):
 1. x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. forward_arcs (x # xs @ [x]) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. False
[PROOF STEP]
using y_def(2) reachable1_not_reverse
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> y
y \<rightarrow>\<^bsub>T\<^esub> x
?x \<rightarrow>\<^sup>+\<^bsub>T\<^esub> ?y \<Longrightarrow> (?y, ?x) \<notin> (arcs_ends T)\<^sup>+

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hd_not_fwd_arcs: "\<not>forward_arcs (ys@x#xs@[x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward_arcs (ys @ x # xs @ [x])
[PROOF STEP]
using hd_last_not_fwd_arcs forward_arcs_split
[PROOF STATE]
proof (prove)
using this:
\<not> forward_arcs (?x # ?xs @ [?x])
forward_arcs (?ys @ ?xs) \<Longrightarrow> forward_arcs ?xs

goal (1 subgoal):
 1. \<not> forward_arcs (ys @ x # xs @ [x])
[PROOF STEP]
by blast


[STATEMENT]
lemma hd_last_not_fwd: "\<not>forward (x#xs@[x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward (x # xs @ [x])
[PROOF STEP]
using hd_last_not_fwd_arcs forward_arcs_alt
[PROOF STATE]
proof (prove)
using this:
\<not> forward_arcs (?x # ?xs @ [?x])
forward ?xs = forward_arcs (rev ?xs)

goal (1 subgoal):
 1. \<not> forward (x # xs @ [x])
[PROOF STEP]
by simp


[STATEMENT]
lemma hd_not_fwd: "\<not>forward (x#xs@[x]@ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward (x # xs @ [x] @ ys)
[PROOF STEP]
using hd_not_fwd_arcs forward_arcs_alt
[PROOF STATE]
proof (prove)
using this:
\<not> forward_arcs (?ys @ ?x # ?xs @ [?x])
forward ?xs = forward_arcs (rev ?xs)

goal (1 subgoal):
 1. \<not> forward (x # xs @ [x] @ ys)
[PROOF STEP]
by simp


[STATEMENT]
lemma y_not_dom_if_nfwd_app_fwd:
  "\<lbrakk>\<not>forward_arcs (y#xs); forward_arcs (y#ys@xs); x \<in> set xs\<rbrakk> \<Longrightarrow> \<not> x \<rightarrow>\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs); x \<in> set xs\<rbrakk> \<Longrightarrow> (x, y) \<notin> arcs_ends T
[PROOF STEP]
using forward_arcs_split[of "y#ys" xs] two_elems_if_not_fwd_conc
[PROOF STATE]
proof (prove)
using this:
forward_arcs ((y # ys) @ xs) \<Longrightarrow> forward_arcs xs
\<not> forward_arcs (?y # ?xs) \<Longrightarrow> \<exists>a b cs. a # b # cs = ?y # ?xs

goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs); x \<in> set xs\<rbrakk> \<Longrightarrow> (x, y) \<notin> arcs_ends T
[PROOF STEP]
by force


[STATEMENT]
lemma not_y_dom_if_nfwd_app_fwd:
  "\<lbrakk>\<not>forward_arcs (y#xs); forward_arcs (y#ys@xs); x \<in> set xs\<rbrakk> \<Longrightarrow> \<not> y \<rightarrow>\<^bsub>T\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs); x \<in> set xs\<rbrakk> \<Longrightarrow> (y, x) \<notin> arcs_ends T
[PROOF STEP]
by (smt (verit, ccfv_threshold) append_is_Nil_conv forward_arcs_alt' forward_arcs_split
      forward_cons fwd_app_nhead_elem hd_append hd_reach1_y_if_nfwd_app_fwd
      hd_reachable1_from_outside' list.distinct(1) reachable1_not_reverse reachable_adjI
      reachable_neq_reachable1 rev.simps(2) rev_append set_rev split_list)