[STATEMENT]
lemma persistent_clauses_subsume_redundant_clauses:
  assumes "redundant C (inferred_clause_sets R S N)"
  assumes "all_fulfill finite S"
  assumes "derived_clauses_are_finite R"
  assumes "finite C"
  shows "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
let ?nat_order = "{ (x::nat,y::nat). x < y}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
fix I
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
have "\<forall>C N. finite C \<longrightarrow> card C = I
         \<longrightarrow> (redundant C (inferred_clause_sets R S N)) \<longrightarrow> redundant C (saturation R S)" (is "?P I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C N. finite C \<longrightarrow> card C = I \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
[PROOF STEP]
proof ((rule wf_induct [of ?nat_order ?P I]),(simp add:wf))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C N. finite C \<longrightarrow> card C = y \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)) \<Longrightarrow> \<forall>C N. finite C \<longrightarrow> card C = x \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
[PROOF STEP]
fix I
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C N. finite C \<longrightarrow> card C = y \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)) \<Longrightarrow> \<forall>C N. finite C \<longrightarrow> card C = x \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
[PROOF STEP]
assume hyp_induct: "\<forall>J. (J,I) \<in> ?nat_order \<longrightarrow> (?P J)"
[PROOF STATE]
proof (state)
this:
\<forall>J. (J, I) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C N. finite C \<longrightarrow> card C = J \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S))

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C N. finite C \<longrightarrow> card C = y \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)) \<Longrightarrow> \<forall>C N. finite C \<longrightarrow> card C = x \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
[PROOF STEP]
show "?P I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C N. finite C \<longrightarrow> card C = I \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
[PROOF STEP]
proof ((rule allI)+,(rule impI)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C N. \<lbrakk>finite C; card C = I; redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
fix C N
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C N. \<lbrakk>finite C; card C = I; redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
assume "finite C" "card C = I" "redundant C (inferred_clause_sets R S N)"
[PROOF STATE]
proof (state)
this:
finite C
card C = I
redundant C (inferred_clause_sets R S N)

goal (1 subgoal):
 1. \<And>C N. \<lbrakk>finite C; card C = I; redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
show "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> redundant C (saturation R S)
 2. \<not> ?P \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
assume "tautology C"
[PROOF STATE]
proof (state)
this:
tautology C

goal (2 subgoals):
 1. ?P \<Longrightarrow> redundant C (saturation R S)
 2. \<not> ?P \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tautology C
[PROOF STEP]
show "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
using this:
tautology C

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology C

goal (1 subgoal):
 1. tautology C \<or> (\<exists>D. D \<in> saturation R S \<and> subsumes D C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
assume "\<not>tautology C"
[PROOF STATE]
proof (state)
this:
\<not> tautology C

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from this and \<open>redundant C (inferred_clause_sets R S N)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology C
redundant C (inferred_clause_sets R S N)
[PROOF STEP]
obtain D
          where "subsumes D C" and "D \<in> inferred_clause_sets R S N"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C
redundant C (inferred_clause_sets R S N)

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>subsumes D C; D \<in> inferred_clause_sets R S N\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C
tautology C \<or> (\<exists>D. D \<in> inferred_clause_sets R S N \<and> subsumes D C)

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>subsumes D C; D \<in> inferred_clause_sets R S N\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subsumes D C
D \<in> inferred_clause_sets R S N

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
show "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> redundant C (saturation R S)
 2. \<not> ?P \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
assume "D \<in> saturation R S"
[PROOF STATE]
proof (state)
this:
D \<in> saturation R S

goal (2 subgoals):
 1. ?P \<Longrightarrow> redundant C (saturation R S)
 2. \<not> ?P \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from this and \<open>subsumes D C\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<in> saturation R S
subsumes D C
[PROOF STEP]
show "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
using this:
D \<in> saturation R S
subsumes D C

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
D \<in> saturation R S
subsumes D C

goal (1 subgoal):
 1. tautology C \<or> (\<exists>D. D \<in> saturation R S \<and> subsumes D C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
assume "D \<notin> saturation R S"
[PROOF STATE]
proof (state)
this:
D \<notin> saturation R S

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from assms(2) assms(3) and \<open>D \<in> inferred_clause_sets R S N\<close> and \<open>D \<notin> saturation R S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
derived_clauses_are_finite R
D \<in> inferred_clause_sets R S N
D \<notin> saturation R S
[PROOF STEP]
obtain M where "strictly_redundant D (inferred_clause_sets R S M)"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
derived_clauses_are_finite R
D \<in> inferred_clause_sets R S N
D \<notin> saturation R S

goal (1 subgoal):
 1. (\<And>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
            non_persistent_clauses_are_redundant [of D R S]
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
derived_clauses_are_finite R
D \<in> inferred_clause_sets R S N
D \<notin> saturation R S
\<lbrakk>D \<in> inferred_clause_sets R S ?N; D \<notin> saturation R S; all_fulfill finite S; derived_clauses_are_finite R\<rbrakk> \<Longrightarrow> \<exists>M. strictly_redundant D (inferred_clause_sets R S M)

goal (1 subgoal):
 1. (\<And>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_redundant D (inferred_clause_sets R S M)

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from \<open>subsumes D C\<close> and \<open>\<not>tautology C\<close>
[PROOF STATE]
proof (chain)
picking this:
subsumes D C
\<not> tautology C
[PROOF STEP]
have "\<not>tautology D"
[PROOF STATE]
proof (prove)
using this:
subsumes D C
\<not> tautology C

goal (1 subgoal):
 1. \<not> tautology D
[PROOF STEP]
unfolding subsumes_def tautology_def
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> C
\<nexists>A. Pos A \<in> C \<and> Neg A \<in> C

goal (1 subgoal):
 1. \<nexists>A. Pos A \<in> D \<and> Neg A \<in> D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> tautology D

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from \<open>strictly_redundant D (inferred_clause_sets R S M)\<close> and \<open>\<not>tautology D\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_redundant D (inferred_clause_sets R S M)
\<not> tautology D
[PROOF STEP]
obtain D' where "D' \<subset> D" and "D' \<in> inferred_clause_sets R S M"
[PROOF STATE]
proof (prove)
using this:
strictly_redundant D (inferred_clause_sets R S M)
\<not> tautology D

goal (1 subgoal):
 1. (\<And>D'. \<lbrakk>D' \<subset> D; D' \<in> inferred_clause_sets R S M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding strictly_redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology D \<or> (\<exists>Da. Da \<in> inferred_clause_sets R S M \<and> Da \<subset> D)
\<not> tautology D

goal (1 subgoal):
 1. (\<And>D'. \<lbrakk>D' \<subset> D; D' \<in> inferred_clause_sets R S M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D' \<subset> D
D' \<in> inferred_clause_sets R S M

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from \<open>D' \<subset> D\<close> and \<open>subsumes D C\<close>
[PROOF STATE]
proof (chain)
picking this:
D' \<subset> D
subsumes D C
[PROOF STEP]
have "D' \<subset> C"
[PROOF STATE]
proof (prove)
using this:
D' \<subset> D
subsumes D C

goal (1 subgoal):
 1. D' \<subset> C
[PROOF STEP]
unfolding subsumes_def
[PROOF STATE]
proof (prove)
using this:
D' \<subset> D
D \<subseteq> C

goal (1 subgoal):
 1. D' \<subset> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D' \<subset> C

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from \<open>D' \<subset> C\<close> and \<open>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
D' \<subset> C
finite C
[PROOF STEP]
have "finite D'"
[PROOF STATE]
proof (prove)
using this:
D' \<subset> C
finite C

goal (1 subgoal):
 1. finite D'
[PROOF STEP]
by (meson psubset_imp_subset rev_finite_subset)
[PROOF STATE]
proof (state)
this:
finite D'

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from \<open>D' \<subset> C\<close> and \<open>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
D' \<subset> C
finite C
[PROOF STEP]
have "card D' < card C"
[PROOF STATE]
proof (prove)
using this:
D' \<subset> C
finite C

goal (1 subgoal):
 1. card D' < card C
[PROOF STEP]
unfolding all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
D' \<subset> C
finite C

goal (1 subgoal):
 1. card D' < card C
[PROOF STEP]
using psubset_card_mono
[PROOF STATE]
proof (prove)
using this:
D' \<subset> C
finite C
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B

goal (1 subgoal):
 1. card D' < card C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card D' < card C

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from this and \<open>card C = I\<close>
[PROOF STATE]
proof (chain)
picking this:
card D' < card C
card C = I
[PROOF STEP]
have "(card D',I) \<in> ?nat_order"
[PROOF STATE]
proof (prove)
using this:
card D' < card C
card C = I

goal (1 subgoal):
 1. (card D', I) \<in> {(x, y). x < y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(card D', I) \<in> {(x, y). x < y}

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from \<open>D' \<in> inferred_clause_sets R S M\<close>
[PROOF STATE]
proof (chain)
picking this:
D' \<in> inferred_clause_sets R S M
[PROOF STEP]
have "redundant D' (inferred_clause_sets R S M)"
[PROOF STATE]
proof (prove)
using this:
D' \<in> inferred_clause_sets R S M

goal (1 subgoal):
 1. redundant D' (inferred_clause_sets R S M)
[PROOF STEP]
unfolding redundant_def subsumes_def
[PROOF STATE]
proof (prove)
using this:
D' \<in> inferred_clause_sets R S M

goal (1 subgoal):
 1. tautology D' \<or> (\<exists>D. D \<in> inferred_clause_sets R S M \<and> D \<subseteq> D')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant D' (inferred_clause_sets R S M)

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from  hyp_induct and \<open>(card D',I) \<in> ?nat_order\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>J. (J, I) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C N. finite C \<longrightarrow> card C = J \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S))
(card D', I) \<in> {(x, y). x < y}
[PROOF STEP]
have "?P (card D')"
[PROOF STATE]
proof (prove)
using this:
\<forall>J. (J, I) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C N. finite C \<longrightarrow> card C = J \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S))
(card D', I) \<in> {(x, y). x < y}

goal (1 subgoal):
 1. \<forall>C N. finite C \<longrightarrow> card C = card D' \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>C N. finite C \<longrightarrow> card C = card D' \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
from this and \<open>finite D'\<close> and \<open>redundant D' (inferred_clause_sets R S M)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>C N. finite C \<longrightarrow> card C = card D' \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
finite D'
redundant D' (inferred_clause_sets R S M)
[PROOF STEP]
have
            "redundant D' (saturation R S)"
[PROOF STATE]
proof (prove)
using this:
\<forall>C N. finite C \<longrightarrow> card C = card D' \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
finite D'
redundant D' (inferred_clause_sets R S M)

goal (1 subgoal):
 1. redundant D' (saturation R S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant D' (saturation R S)

goal (1 subgoal):
 1. D \<notin> saturation R S \<Longrightarrow> redundant C (saturation R S)
[PROOF STEP]
show "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
by (meson \<open>D' \<subset> C\<close> \<open>redundant D' (saturation R S)\<close>
              psubset_imp_subset subsumes_def subsumption_preserves_redundancy)
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C N. finite C \<longrightarrow> card C = I \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C N. finite C \<longrightarrow> card C = I \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>C N. finite C \<longrightarrow> card C = ?I2 \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>C N. finite C \<longrightarrow> card C = ?I2 \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
[PROOF STEP]
show "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
using this:
\<forall>C N. finite C \<longrightarrow> card C = ?I2 \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
using assms(1) assms(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>C N. finite C \<longrightarrow> card C = ?I2 \<longrightarrow> redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (saturation R S)
redundant C (inferred_clause_sets R S N)
finite C

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem persistent_clauses_are_saturated:
 assumes "derived_clauses_are_finite R"
 assumes "all_fulfill finite S"
  shows "saturated_binary_rule R (saturation R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated_binary_rule R (saturation R S)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
let ?S = "saturation R S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>saturated_binary_rule R ?S"
[PROOF STATE]
proof (state)
this:
\<not> saturated_binary_rule R (saturation R S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> saturated_binary_rule R (saturation R S)
[PROOF STEP]
obtain P1 P2 C where "R P1 P2 C" and "P1 \<in> ?S" and "P2 \<in> ?S" and "\<not>redundant C ?S"
[PROOF STATE]
proof (prove)
using this:
\<not> saturated_binary_rule R (saturation R S)

goal (1 subgoal):
 1. (\<And>P1 P2 C. \<lbrakk>R P1 P2 C; P1 \<in> saturation R S; P2 \<in> saturation R S; \<not> redundant C (saturation R S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding saturated_binary_rule_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>P1 P2 C. P1 \<in> saturation R S \<and> P2 \<in> saturation R S \<and> R P1 P2 C \<longrightarrow> redundant C (saturation R S))

goal (1 subgoal):
 1. (\<And>P1 P2 C. \<lbrakk>R P1 P2 C; P1 \<in> saturation R S; P2 \<in> saturation R S; \<not> redundant C (saturation R S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R P1 P2 C
P1 \<in> saturation R S
P2 \<in> saturation R S
\<not> redundant C (saturation R S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>P1 \<in> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
P1 \<in> saturation R S
[PROOF STEP]
obtain N1 where i: "\<forall>M. (M \<ge> N1 \<longrightarrow> P1 \<in> (inferred_clause_sets R S M))"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> saturation R S

goal (1 subgoal):
 1. (\<And>N1. \<forall>M\<ge>N1. P1 \<in> inferred_clause_sets R S M \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>M\<ge>N1. P1 \<in> inferred_clause_sets R S M

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>P2 \<in> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
P2 \<in> saturation R S
[PROOF STEP]
obtain N2 where ii: "\<forall>M. (M \<ge> N2 \<longrightarrow> P2 \<in> (inferred_clause_sets R S M))"
[PROOF STATE]
proof (prove)
using this:
P2 \<in> saturation R S

goal (1 subgoal):
 1. (\<And>N2. \<forall>M\<ge>N2. P2 \<in> inferred_clause_sets R S M \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>M\<ge>N2. P2 \<in> inferred_clause_sets R S M

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
let ?N = "max N1 N2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
have "?N \<ge> N1" and "?N \<ge> N2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N1 \<le> max N1 N2 &&& N2 \<le> max N1 N2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N1 \<le> max N1 N2
N2 \<le> max N1 N2

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from this and i
[PROOF STATE]
proof (chain)
picking this:
N1 \<le> max N1 N2
N2 \<le> max N1 N2
\<forall>M\<ge>N1. P1 \<in> inferred_clause_sets R S M
[PROOF STEP]
have "P1 \<in> inferred_clause_sets R S ?N"
[PROOF STATE]
proof (prove)
using this:
N1 \<le> max N1 N2
N2 \<le> max N1 N2
\<forall>M\<ge>N1. P1 \<in> inferred_clause_sets R S M

goal (1 subgoal):
 1. P1 \<in> inferred_clause_sets R S (max N1 N2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P1 \<in> inferred_clause_sets R S (max N1 N2)

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>?N \<ge> N2\<close> and ii
[PROOF STATE]
proof (chain)
picking this:
N2 \<le> max N1 N2
\<forall>M\<ge>N2. P2 \<in> inferred_clause_sets R S M
[PROOF STEP]
have "P2 \<in> inferred_clause_sets R S ?N"
[PROOF STATE]
proof (prove)
using this:
N2 \<le> max N1 N2
\<forall>M\<ge>N2. P2 \<in> inferred_clause_sets R S M

goal (1 subgoal):
 1. P2 \<in> inferred_clause_sets R S (max N1 N2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P2 \<in> inferred_clause_sets R S (max N1 N2)

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>R P1 P2 C\<close> and \<open>P1 \<in> inferred_clause_sets R S ?N\<close> and \<open>P2 \<in> inferred_clause_sets R S ?N\<close>
[PROOF STATE]
proof (chain)
picking this:
R P1 P2 C
P1 \<in> inferred_clause_sets R S (max N1 N2)
P2 \<in> inferred_clause_sets R S (max N1 N2)
[PROOF STEP]
have "C \<in> all_deducible_clauses R ( inferred_clause_sets R S ?N)"
[PROOF STATE]
proof (prove)
using this:
R P1 P2 C
P1 \<in> inferred_clause_sets R S (max N1 N2)
P2 \<in> inferred_clause_sets R S (max N1 N2)

goal (1 subgoal):
 1. C \<in> all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
C \<in> all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))
[PROOF STEP]
have "C \<in> add_all_deducible_clauses R (inferred_clause_sets R S ?N)"
[PROOF STATE]
proof (prove)
using this:
C \<in> all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))

goal (1 subgoal):
 1. C \<in> add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
derived_clauses_are_finite R
all_fulfill finite S
[PROOF STEP]
have "all_fulfill finite (inferred_clause_sets R S ?N)"
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S

goal (1 subgoal):
 1. all_fulfill finite (inferred_clause_sets R S (max N1 N2))
[PROOF STEP]
using all_inferred_clause_sets_are_finite [of R S ?N]
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S
\<lbrakk>derived_clauses_are_finite R; all_fulfill finite S\<rbrakk> \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (max N1 N2))

goal (1 subgoal):
 1. all_fulfill finite (inferred_clause_sets R S (max N1 N2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (inferred_clause_sets R S (max N1 N2))

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
derived_clauses_are_finite R
all_fulfill finite S
[PROOF STEP]
have "all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S ?N))"
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2)))
[PROOF STEP]
using add_all_deducible_clauses_finite
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S
\<lbrakk>derived_clauses_are_finite ?R; all_fulfill finite ?S\<rbrakk> \<Longrightarrow> all_fulfill finite (add_all_deducible_clauses ?R (inferred_clause_sets ?R ?S ?N))

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2)))

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>C \<in> add_all_deducible_clauses R (inferred_clause_sets R S ?N)\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2)))
C \<in> add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))
[PROOF STEP]
have "redundant C (inferred_clause_sets R S (Suc ?N))"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2)))
C \<in> add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))

goal (1 subgoal):
 1. redundant C (inferred_clause_sets R S (Suc (max N1 N2)))
[PROOF STEP]
using simplify_and_membership
    [of "add_all_deducible_clauses R (inferred_clause_sets R S ?N)"
      "inferred_clause_sets R S (Suc ?N)" C]
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2)))
C \<in> add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))
\<lbrakk>all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))); inferred_clause_sets R S (Suc (max N1 N2)) = simplify (add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))); C \<in> add_all_deducible_clauses R (inferred_clause_sets R S (max N1 N2))\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (max N1 N2)))

goal (1 subgoal):
 1. redundant C (inferred_clause_sets R S (Suc (max N1 N2)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (inferred_clause_sets R S (Suc (max N1 N2)))

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
have "finite P1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite P1
[PROOF STEP]
using \<open>P1 \<in> inferred_clause_sets R S (max N1 N2)\<close>
      \<open>all_fulfill finite (inferred_clause_sets R S (max N1 N2))\<close> all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
P1 \<in> inferred_clause_sets R S (max N1 N2)
all_fulfill finite (inferred_clause_sets R S (max N1 N2))
all_fulfill ?P ?S = (\<forall>C. C \<in> ?S \<longrightarrow> ?P C)

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
have "finite P2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite P2
[PROOF STEP]
using \<open>P2 \<in> inferred_clause_sets R S (max N1 N2)\<close>
      \<open>all_fulfill finite (inferred_clause_sets R S (max N1 N2))\<close> all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
P2 \<in> inferred_clause_sets R S (max N1 N2)
all_fulfill finite (inferred_clause_sets R S (max N1 N2))
all_fulfill ?P ?S = (\<forall>C. C \<in> ?S \<longrightarrow> ?P C)

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>R P1 P2 C\<close> and \<open>finite P1\<close> and \<open>finite P2\<close> and \<open>derived_clauses_are_finite R\<close>
[PROOF STATE]
proof (chain)
picking this:
R P1 P2 C
finite P1
finite P2
derived_clauses_are_finite R
[PROOF STEP]
have "finite C"
[PROOF STATE]
proof (prove)
using this:
R P1 P2 C
finite P1
finite P2
derived_clauses_are_finite R

goal (1 subgoal):
 1. finite C
[PROOF STEP]
unfolding derived_clauses_are_finite_def
[PROOF STATE]
proof (prove)
using this:
R P1 P2 C
finite P1
finite P2
\<forall>P1 P2 C. finite P1 \<longrightarrow> finite P2 \<longrightarrow> R P1 P2 C \<longrightarrow> finite C

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from assms this and \<open>redundant C (inferred_clause_sets R S (Suc ?N))\<close>
[PROOF STATE]
proof (chain)
picking this:
derived_clauses_are_finite R
all_fulfill finite S
finite C
redundant C (inferred_clause_sets R S (Suc (max N1 N2)))
[PROOF STEP]
have "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S
finite C
redundant C (inferred_clause_sets R S (Suc (max N1 N2)))

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
using  persistent_clauses_subsume_redundant_clauses [of C R S "Suc ?N"]
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S
finite C
redundant C (inferred_clause_sets R S (Suc (max N1 N2)))
\<lbrakk>redundant C (inferred_clause_sets R S (Suc (max N1 N2))); all_fulfill finite S; derived_clauses_are_finite R; finite C\<rbrakk> \<Longrightarrow> redundant C (saturation R S)

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule R (saturation R S) \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
redundant C (saturation R S)

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>\<not>redundant C ?S\<close>
[PROOF STATE]
proof (prove)
using this:
redundant C (saturation R S)
\<not> redundant C (saturation R S)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem saturation_is_correct:
  assumes "Sound R"
  assumes "derived_clauses_are_finite R"
  assumes "all_fulfill finite S"
  shows "equivalent S (saturation R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalent S (saturation R S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. equivalent S (saturation R S)
[PROOF STEP]
have "entails_formula S (saturation R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula S (saturation R S)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> entails_formula S (saturation R S)"
[PROOF STATE]
proof (state)
this:
\<not> entails_formula S (saturation R S)

goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> entails_formula S (saturation R S)
[PROOF STEP]
obtain C where "C \<in> saturation R S" and "\<not> entails S C"
[PROOF STATE]
proof (prove)
using this:
\<not> entails_formula S (saturation R S)

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> saturation R S; \<not> entails S C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding entails_formula_def
[PROOF STATE]
proof (prove)
using this:
\<not> Ball (saturation R S) (entails S)

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> saturation R S; \<not> entails S C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> saturation R S
\<not> entails S C

goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>C \<in> saturation R S\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<in> saturation R S
[PROOF STEP]
obtain N where "C \<in> inferred_clause_sets R S N"
[PROOF STATE]
proof (prove)
using this:
C \<in> saturation R S

goal (1 subgoal):
 1. (\<And>N. C \<in> inferred_clause_sets R S N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> inferred_clause_sets R S N

goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
C \<in> inferred_clause_sets R S N

goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
fix N
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
have "entails_formula S (inferred_clause_sets R S N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula S (inferred_clause_sets R S N)
[PROOF STEP]
proof (induction N)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. entails_formula S (inferred_clause_sets R S 0)
 2. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
show "entails_formula S (inferred_clause_sets R S 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula S (inferred_clause_sets R S 0)
[PROOF STEP]
using assms(3) simplify_preserves_semantic validity_implies_entailment
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
\<lbrakk>?T = simplify ?S; all_fulfill finite ?S\<rbrakk> \<Longrightarrow> ?I \<Turnstile> ?S = ?I \<Turnstile> ?T
\<forall>I. I \<Turnstile> ?S1.0 \<longrightarrow> I \<Turnstile> ?S2.0 \<Longrightarrow> entails_formula ?S1.0 ?S2.0

goal (1 subgoal):
 1. entails_formula S (inferred_clause_sets R S 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
entails_formula S (inferred_clause_sets R S 0)

goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
fix N
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
assume "entails_formula S (inferred_clause_sets R S N)"
[PROOF STATE]
proof (state)
this:
entails_formula S (inferred_clause_sets R S N)

goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
Sound R
[PROOF STEP]
have "entails_formula (inferred_clause_sets R S N)
          (add_all_deducible_clauses R (inferred_clause_sets R S N))"
[PROOF STATE]
proof (prove)
using this:
Sound R

goal (1 subgoal):
 1. entails_formula (inferred_clause_sets R S N) (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
using add_all_deducible_sound
[PROOF STATE]
proof (prove)
using this:
Sound R
Sound ?R \<Longrightarrow> entails_formula ?S (add_all_deducible_clauses ?R ?S)

goal (1 subgoal):
 1. entails_formula (inferred_clause_sets R S N) (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
entails_formula (inferred_clause_sets R S N) (add_all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
from this and \<open>entails_formula S (inferred_clause_sets R S N)\<close>
[PROOF STATE]
proof (chain)
picking this:
entails_formula (inferred_clause_sets R S N) (add_all_deducible_clauses R (inferred_clause_sets R S N))
entails_formula S (inferred_clause_sets R S N)
[PROOF STEP]
have "entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))"
[PROOF STATE]
proof (prove)
using this:
entails_formula (inferred_clause_sets R S N) (add_all_deducible_clauses R (inferred_clause_sets R S N))
entails_formula S (inferred_clause_sets R S N)

goal (1 subgoal):
 1. entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
using entails_transitive
        [of S "inferred_clause_sets R S N" "add_all_deducible_clauses R (inferred_clause_sets R S N)"]
[PROOF STATE]
proof (prove)
using this:
entails_formula (inferred_clause_sets R S N) (add_all_deducible_clauses R (inferred_clause_sets R S N))
entails_formula S (inferred_clause_sets R S N)
\<lbrakk>entails_formula S (inferred_clause_sets R S N); entails_formula (inferred_clause_sets R S N) (add_all_deducible_clauses R (inferred_clause_sets R S N))\<rbrakk> \<Longrightarrow> entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
have "inferred_clause_sets R S (Suc N) \<subseteq> add_all_deducible_clauses R
                (inferred_clause_sets R S N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inferred_clause_sets R S (Suc N) \<subseteq> add_all_deducible_clauses R (inferred_clause_sets R S N)
[PROOF STEP]
using simplify_def
[PROOF STATE]
proof (prove)
using this:
simplify ?S = {C \<in> ?S. \<not> strictly_redundant C ?S}

goal (1 subgoal):
 1. inferred_clause_sets R S (Suc N) \<subseteq> add_all_deducible_clauses R (inferred_clause_sets R S N)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inferred_clause_sets R S (Suc N) \<subseteq> add_all_deducible_clauses R (inferred_clause_sets R S N)

goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inferred_clause_sets R S (Suc N) \<subseteq> add_all_deducible_clauses R (inferred_clause_sets R S N)
[PROOF STEP]
have "entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N))
              (inferred_clause_sets R S (Suc N))"
[PROOF STATE]
proof (prove)
using this:
inferred_clause_sets R S (Suc N) \<subseteq> add_all_deducible_clauses R (inferred_clause_sets R S N)

goal (1 subgoal):
 1. entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N)) (inferred_clause_sets R S (Suc N))
[PROOF STEP]
using entailment_subset
[PROOF STATE]
proof (prove)
using this:
inferred_clause_sets R S (Suc N) \<subseteq> add_all_deducible_clauses R (inferred_clause_sets R S N)
?S2.0 \<subseteq> ?S1.0 \<Longrightarrow> entails_formula ?S1.0 ?S2.0

goal (1 subgoal):
 1. entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N)) (inferred_clause_sets R S (Suc N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N)) (inferred_clause_sets R S (Suc N))

goal (1 subgoal):
 1. \<And>N. entails_formula S (inferred_clause_sets R S N) \<Longrightarrow> entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
from this and \<open>entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))\<close>
[PROOF STATE]
proof (chain)
picking this:
entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N)) (inferred_clause_sets R S (Suc N))
entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
show "entails_formula S (inferred_clause_sets R S (Suc N))"
[PROOF STATE]
proof (prove)
using this:
entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N)) (inferred_clause_sets R S (Suc N))
entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
using entails_transitive [of S "add_all_deducible_clauses R (inferred_clause_sets R S N)"]
[PROOF STATE]
proof (prove)
using this:
entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N)) (inferred_clause_sets R S (Suc N))
entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N))
\<lbrakk>entails_formula S (add_all_deducible_clauses R (inferred_clause_sets R S N)); entails_formula (add_all_deducible_clauses R (inferred_clause_sets R S N)) ?S3.0\<rbrakk> \<Longrightarrow> entails_formula S ?S3.0

goal (1 subgoal):
 1. entails_formula S (inferred_clause_sets R S (Suc N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
entails_formula S (inferred_clause_sets R S (Suc N))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
entails_formula S (inferred_clause_sets R S N)

goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
entails_formula S (inferred_clause_sets R S ?Na2)

goal (1 subgoal):
 1. \<not> entails_formula S (saturation R S) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>C \<in> inferred_clause_sets R S N\<close> and \<open>\<not> entails S C\<close>
[PROOF STATE]
proof (chain)
picking this:
entails_formula S (inferred_clause_sets R S ?Na2)
C \<in> inferred_clause_sets R S N
\<not> entails S C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
entails_formula S (inferred_clause_sets R S ?Na2)
C \<in> inferred_clause_sets R S N
\<not> entails S C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding entails_formula_def
[PROOF STATE]
proof (prove)
using this:
Ball (inferred_clause_sets R S ?Na2) (entails S)
C \<in> inferred_clause_sets R S N
\<not> entails S C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
entails_formula S (saturation R S)

goal (1 subgoal):
 1. equivalent S (saturation R S)
[PROOF STEP]
have "entails_formula (saturation R S) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula (saturation R S) S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> entails_formula (saturation R S) S \<Longrightarrow> False
[PROOF STEP]
assume "\<not> entails_formula (saturation R S) S"
[PROOF STATE]
proof (state)
this:
\<not> entails_formula (saturation R S) S

goal (1 subgoal):
 1. \<not> entails_formula (saturation R S) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> entails_formula (saturation R S) S
[PROOF STEP]
obtain C where "C \<in> S" and "\<not> entails (saturation R S) C"
[PROOF STATE]
proof (prove)
using this:
\<not> entails_formula (saturation R S) S

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> S; \<not> entails (saturation R S) C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding entails_formula_def
[PROOF STATE]
proof (prove)
using this:
\<not> Ball S (entails (saturation R S))

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> S; \<not> entails (saturation R S) C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> S
\<not> entails (saturation R S) C

goal (1 subgoal):
 1. \<not> entails_formula (saturation R S) S \<Longrightarrow> False
[PROOF STEP]
from \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<in> S
[PROOF STEP]
have "redundant C S"
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. redundant C S
[PROOF STEP]
unfolding redundant_def subsumes_def
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. tautology C \<or> (\<exists>D. D \<in> S \<and> D \<subseteq> C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C S

goal (1 subgoal):
 1. \<not> entails_formula (saturation R S) S \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<open>redundant C S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
redundant C S
[PROOF STEP]
have "redundant C (inferred_clause_sets R S 0)"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
redundant C S

goal (1 subgoal):
 1. redundant C (inferred_clause_sets R S 0)
[PROOF STEP]
using simplify_preserves_redundancy
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
redundant C S
\<lbrakk>all_fulfill finite ?S; redundant ?C ?S\<rbrakk> \<Longrightarrow> redundant ?C (simplify ?S)

goal (1 subgoal):
 1. redundant C (inferred_clause_sets R S 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (inferred_clause_sets R S 0)

goal (1 subgoal):
 1. \<not> entails_formula (saturation R S) S \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
C \<in> S
[PROOF STEP]
have "finite C"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
C \<in> S

goal (1 subgoal):
 1. finite C
[PROOF STEP]
unfolding all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
\<forall>C. C \<in> S \<longrightarrow> finite C
C \<in> S

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

goal (1 subgoal):
 1. \<not> entails_formula (saturation R S) S \<Longrightarrow> False
[PROOF STEP]
from \<open>redundant C (inferred_clause_sets R S 0)\<close> assms(2) assms(3) \<open>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
redundant C (inferred_clause_sets R S 0)
derived_clauses_are_finite R
all_fulfill finite S
finite C
[PROOF STEP]
have "redundant C (saturation R S)"
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S 0)
derived_clauses_are_finite R
all_fulfill finite S
finite C

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
using persistent_clauses_subsume_redundant_clauses [of C R S 0]
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S 0)
derived_clauses_are_finite R
all_fulfill finite S
finite C
\<lbrakk>redundant C (inferred_clause_sets R S 0); all_fulfill finite S; derived_clauses_are_finite R; finite C\<rbrakk> \<Longrightarrow> redundant C (saturation R S)

goal (1 subgoal):
 1. redundant C (saturation R S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (saturation R S)

goal (1 subgoal):
 1. \<not> entails_formula (saturation R S) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> entails (saturation R S) C\<close>
[PROOF STATE]
proof (chain)
picking this:
redundant C (saturation R S)
\<not> entails (saturation R S) C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
redundant C (saturation R S)
\<not> entails (saturation R S) C

goal (1 subgoal):
 1. False
[PROOF STEP]
using entails_formula_def redundancy_implies_entailment
[PROOF STATE]
proof (prove)
using this:
redundant C (saturation R S)
\<not> entails (saturation R S) C
entails_formula ?S1.0 ?S2.0 = (\<forall>C\<in>?S2.0. entails ?S1.0 C)
redundant ?C ?S \<Longrightarrow> entails ?S ?C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
entails_formula (saturation R S) S

goal (1 subgoal):
 1. equivalent S (saturation R S)
[PROOF STEP]
from \<open>entails_formula S (saturation R S)\<close> and \<open>entails_formula (saturation R S) S\<close>
[PROOF STATE]
proof (chain)
picking this:
entails_formula S (saturation R S)
entails_formula (saturation R S) S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
entails_formula S (saturation R S)
entails_formula (saturation R S) S

goal (1 subgoal):
 1. equivalent S (saturation R S)
[PROOF STEP]
unfolding equivalent_def
[PROOF STATE]
proof (prove)
using this:
entails_formula S (saturation R S)
entails_formula (saturation R S) S

goal (1 subgoal):
 1. entails_formula S (saturation R S) \<and> entails_formula (saturation R S) S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
equivalent S (saturation R S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma FOREACH_oci_to_monadic:
  "FOREACHoci R \<Phi> S c f \<sigma>0 = monadic_FOREACH R \<Phi> S (\<lambda>\<sigma>. RETURN (c \<sigma>)) f \<sigma>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FOREACH\<^sub>O\<^sub>C\<^bsup>R,\<Phi>\<^esup> S c f \<sigma>0 = monadic_FOREACH R \<Phi> S (\<lambda>\<sigma>. RETURN (c \<sigma>)) f \<sigma>0
[PROOF STEP]
unfolding FOREACHoci_def monadic_FOREACH_def WHILEIT_def WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>xs. distinct xs \<and> S = set xs \<and> sorted_wrt R xs) \<bind> (\<lambda>xs. REC\<^sub>T (\<lambda>W s. if case s of (it, \<sigma>) \<Rightarrow> \<exists>xs'. xs = xs' @ it \<and> \<Phi> (set it) \<sigma> then if FOREACH_cond c s then FOREACH_body f s \<bind> W else RETURN s else FAIL) (xs, \<sigma>0) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>))) = ASSERT (finite S) \<bind> (\<lambda>_. it_to_sorted_list R S \<bind> (\<lambda>xs0. REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 \<Phi> (xs, \<sigma>)) \<bind> (\<lambda>_. if xs \<noteq> [] then RETURN (c \<sigma>) \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)) else RETURN (xs, \<sigma>))) (xs0, \<sigma>0) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>)))
[PROOF STEP]
unfolding it_to_sorted_list_def FOREACH_cond_def FOREACH_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>xs. distinct xs \<and> S = set xs \<and> sorted_wrt R xs) \<bind> (\<lambda>xs. REC\<^sub>T (\<lambda>W s. if case s of (it, \<sigma>) \<Rightarrow> \<exists>xs'. xs = xs' @ it \<and> \<Phi> (set it) \<sigma> then if case s of (xs, \<sigma>) \<Rightarrow> xs \<noteq> [] \<and> c \<sigma> then FOREACH_body f s \<bind> W else RETURN s else FAIL) (xs, \<sigma>0) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>))) = ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt R l) \<bind> (\<lambda>xs0. REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (case (xs, \<sigma>) of (it, \<sigma>) \<Rightarrow> \<exists>xs'. xs0 = xs' @ it \<and> \<Phi> (set it) \<sigma>) \<bind> (\<lambda>_. if xs \<noteq> [] then RETURN (c \<sigma>) \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)) else RETURN (xs, \<sigma>))) (xs0, \<sigma>0) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>xs. distinct xs \<and> S = set xs \<and> sorted_wrt R xs) \<bind> (\<lambda>xs. REC\<^sub>T (\<lambda>W s. if case s of (it, \<sigma>) \<Rightarrow> (\<exists>xs'. xs = xs' @ it) \<and> \<Phi> (set it) \<sigma> then if case s of (xs, \<sigma>) \<Rightarrow> xs \<noteq> [] \<and> c \<sigma> then FOREACH_body f s \<bind> W else RETURN s else FAIL) (xs, \<sigma>0) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>))) = ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt R l) \<bind> (\<lambda>xs0. REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT ((\<exists>xs'. xs0 = xs' @ xs) \<and> \<Phi> (set xs) \<sigma>) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else RETURN (c \<sigma>) \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (xs0, \<sigma>0) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>)))
[PROOF STEP]
apply (fo_rule arg_cong[THEN cong] | rule refl ext)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>_ xs W s. (if case s of (it, \<sigma>) \<Rightarrow> (\<exists>xs'. xs = xs' @ it) \<and> \<Phi> (set it) \<sigma> then if case s of (xs, \<sigma>) \<Rightarrow> xs \<noteq> [] \<and> c \<sigma> then FOREACH_body f s \<bind> W else RETURN s else FAIL) = (case s of (xsa, \<sigma>) \<Rightarrow> ASSERT ((\<exists>xs'. xs = xs' @ xsa) \<and> \<Phi> (set xsa) \<sigma>) \<bind> (\<lambda>_. if xsa = [] then RETURN (xsa, \<sigma>) else RETURN (c \<sigma>) \<bind> (\<lambda>b. if b then FOREACH_body f (xsa, \<sigma>) \<bind> W else RETURN (xsa, \<sigma>))))
 2. \<And>_ xs. (xs, \<sigma>0) = (xs, \<sigma>0)
 3. \<And>_ xs. (\<lambda>(uu_, \<sigma>). RETURN \<sigma>) = (\<lambda>(uu_, \<sigma>). RETURN \<sigma>)
[PROOF STEP]
apply (simp split: prod.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>_ xs. (xs, \<sigma>0) = (xs, \<sigma>0)
 2. \<And>_ xs. (\<lambda>(uu_, \<sigma>). RETURN \<sigma>) = (\<lambda>(uu_, \<sigma>). RETURN \<sigma>)
[PROOF STEP]
apply (rule refl)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma monadic_nfoldli_eq:
  "monadic_nfoldli l c f s = (
    case l of
      [] \<Rightarrow> RETURN s
    | x#ls \<Rightarrow> do {
        b\<leftarrow>c s;
        if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s
      }
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli l c f s = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s))
[PROOF STEP]
apply (subst monadic_nfoldli_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC\<^sub>T (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s)) (l, s) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s))
[PROOF STEP]
apply (subst RECT_unfold)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. trimono (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s))
 2. (case (l, s) of ([], s) \<Rightarrow> RETURN s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. REC\<^sub>T (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s)) (ls, s')) else RETURN s)) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s))
[PROOF STEP]
apply (tagged_solver)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (l, s) of ([], s) \<Rightarrow> RETURN s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. REC\<^sub>T (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s)) (ls, s')) else RETURN s)) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s))
[PROOF STEP]
apply (subst monadic_nfoldli_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (l, s) of ([], s) \<Rightarrow> RETURN s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s)) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma monadic_nfoldli_simp[simp]:
  "monadic_nfoldli [] c f s = RETURN s"
  "monadic_nfoldli (x#ls) c f s = do {
    b\<leftarrow>c s;
    if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s
  }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli [] c f s = RETURN s &&& monadic_nfoldli (x # ls) c f s = c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s)
[PROOF STEP]
apply (subst monadic_nfoldli_eq, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli (x # ls) c f s = c s \<bind> (\<lambda>b. if b then f x s \<bind> monadic_nfoldli ls c f else RETURN s)
[PROOF STEP]
apply (subst monadic_nfoldli_eq, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nfoldli_to_monadic:
  "nfoldli l c f = monadic_nfoldli l (\<lambda>x. RETURN (c x)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli l c f = monadic_nfoldli l (\<lambda>x. RETURN (c x)) f
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nfoldli [] c f = monadic_nfoldli [] (\<lambda>x. RETURN (c x)) f
 2. \<And>a l. nfoldli l c f = monadic_nfoldli l (\<lambda>x. RETURN (c x)) f \<Longrightarrow> nfoldli (a # l) c f = monadic_nfoldli (a # l) (\<lambda>x. RETURN (c x)) f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nfoldli_alt_eq:
  "nfoldli_alt l c f s = (
    case l of
      [] \<Rightarrow> RETURN s
    | x#ls \<Rightarrow> do {let b=c s; if b then f x s \<bind> nfoldli_alt ls c f else RETURN s}
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli_alt l c f s = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s)
[PROOF STEP]
apply (subst nfoldli_alt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC\<^sub>T (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s) (l, s) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s)
[PROOF STEP]
apply (subst RECT_unfold)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. trimono (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s)
 2. (case (l, s) of ([], s) \<Rightarrow> RETURN s | (x # ls, s) \<Rightarrow> let b = c s in if b then f x s \<bind> (\<lambda>s'. REC\<^sub>T (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s) (ls, s')) else RETURN s) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s)
[PROOF STEP]
apply (tagged_solver)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (l, s) of ([], s) \<Rightarrow> RETURN s | (x # ls, s) \<Rightarrow> let b = c s in if b then f x s \<bind> (\<lambda>s'. REC\<^sub>T (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s) (ls, s')) else RETURN s) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s)
[PROOF STEP]
apply (subst nfoldli_alt_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (l, s) of ([], s) \<Rightarrow> RETURN s | (x # ls, s) \<Rightarrow> let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s) = (case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nfoldli_alt_simp[simp]:
  "nfoldli_alt [] c f s = RETURN s"
  "nfoldli_alt (x#ls) c f s = do {
    let b = c s;
    if b then f x s \<bind> nfoldli_alt ls c f else RETURN s
  }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli_alt [] c f s = RETURN s &&& nfoldli_alt (x # ls) c f s = (let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s)
[PROOF STEP]
apply (subst nfoldli_alt_eq, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli_alt (x # ls) c f s = (let b = c s in if b then f x s \<bind> nfoldli_alt ls c f else RETURN s)
[PROOF STEP]
apply (subst nfoldli_alt_eq, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nfoldli_alt:
  "(nfoldli::'a list \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b nres) \<Rightarrow> 'b \<Rightarrow> 'b nres)
  = nfoldli_alt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli = nfoldli_alt
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb xc. nfoldli x xa xb xc = nfoldli_alt x xa xb xc
[PROOF STEP]
fix l::"'a list" and c::"'b \<Rightarrow> bool" and f::"'a \<Rightarrow> 'b \<Rightarrow> 'b nres" and s :: 'b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb xc. nfoldli x xa xb xc = nfoldli_alt x xa xb xc
[PROOF STEP]
have "nfoldli l c f = nfoldli_alt l c f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli l c f = nfoldli_alt l c f
[PROOF STEP]
by (induct l) auto
[PROOF STATE]
proof (state)
this:
nfoldli l c f = nfoldli_alt l c f

goal (1 subgoal):
 1. \<And>x xa xb xc. nfoldli x xa xb xc = nfoldli_alt x xa xb xc
[PROOF STEP]
thus "nfoldli l c f s = nfoldli_alt l c f s"
[PROOF STATE]
proof (prove)
using this:
nfoldli l c f = nfoldli_alt l c f

goal (1 subgoal):
 1. nfoldli l c f s = nfoldli_alt l c f s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nfoldli l c f s = nfoldli_alt l c f s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma monadic_nfoldli_rec:
  "monadic_nfoldli x' c f \<sigma>
          \<le>\<Down>Id (REC\<^sub>T
             (\<lambda>W (xs, \<sigma>).
                 ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind>
                 (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>)
                      else c \<sigma> \<bind>
                           (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W
                                else RETURN (xs, \<sigma>))))
             (x', \<sigma>) \<bind>
            (\<lambda>(_, y). RETURN y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (induct x' arbitrary: \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. monadic_nfoldli [] c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) ([], \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))
 2. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> monadic_nfoldli (a # x') c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (a # x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (subst RECT_unfold, refine_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. monadic_nfoldli [] c f \<sigma> \<le> \<Down> Id ((case ([], \<sigma>) of (xs, \<sigma>) \<Rightarrow> ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) else RETURN (xs, \<sigma>)))) \<bind> (\<lambda>(uu_, y). RETURN y))
 2. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> monadic_nfoldli (a # x') c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (a # x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. RETURN \<sigma> \<le> ASSERT (FOREACH_inv xs0 I ([], \<sigma>)) \<bind> (\<lambda>x. RETURN \<sigma>)
 2. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> monadic_nfoldli (a # x') c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (a # x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (rule le_ASSERTI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. FOREACH_inv xs0 I ([], \<sigma>) \<Longrightarrow> RETURN \<sigma> \<le> RETURN \<sigma>
 2. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> monadic_nfoldli (a # x') c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (a # x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> monadic_nfoldli (a # x') c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (a # x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (subst RECT_unfold, refine_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> monadic_nfoldli (a # x') c f \<sigma> \<le> \<Down> Id ((case (a # x', \<sigma>) of (xs, \<sigma>) \<Rightarrow> ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) else RETURN (xs, \<sigma>)))) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (subst monadic_nfoldli_simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> c \<sigma> \<bind> (\<lambda>b. if b then f a \<sigma> \<bind> monadic_nfoldli x' c f else RETURN \<sigma>) \<le> \<Down> Id ((case (a # x', \<sigma>) of (xs, \<sigma>) \<Rightarrow> ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) else RETURN (xs, \<sigma>)))) \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (simp del: conc_Id cong: if_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x' \<sigma>. (\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y))) \<Longrightarrow> c \<sigma> \<bind> (\<lambda>b. if b then f a \<sigma> \<bind> monadic_nfoldli x' c f else RETURN \<sigma>) \<le> \<Down> Id (ASSERT (FOREACH_inv xs0 I (a # x', \<sigma>)) \<bind> (\<lambda>x. c \<sigma> \<bind> (\<lambda>x. if x then FOREACH_body f (a # x', \<sigma>) \<bind> (\<lambda>x. REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) x \<bind> (\<lambda>(uu_, y). RETURN y)) else RETURN \<sigma>)))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a x' \<sigma> b x. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel\<rbrakk> \<Longrightarrow> b = x
 2. \<And>a x' \<sigma> b x. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x\<rbrakk> \<Longrightarrow> f a \<sigma> \<le> \<Down> (?R'517 a x' \<sigma> b x) (FOREACH_body f (a # x', \<sigma>))
 3. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> ?R'517 a x' \<sigma> b x\<rbrakk> \<Longrightarrow> monadic_nfoldli x' c f xa \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) xb \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x' \<sigma> b x. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x\<rbrakk> \<Longrightarrow> f a \<sigma> \<le> \<Down> (?R'517 a x' \<sigma> b x) (FOREACH_body f (a # x', \<sigma>))
 2. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> ?R'517 a x' \<sigma> b x\<rbrakk> \<Longrightarrow> monadic_nfoldli x' c f xa \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) xb \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (clarsimp simp add: FOREACH_body_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x' \<sigma> b x. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y); FOREACH_inv xs0 I (a # x', \<sigma>); b; x\<rbrakk> \<Longrightarrow> f a \<sigma> \<le> \<Down> (?R'517 a x' \<sigma> True True) (f a \<sigma> \<bind> (\<lambda>\<sigma>'. RETURN (x', \<sigma>')))
 2. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> ?R'517 a x' \<sigma> b x\<rbrakk> \<Longrightarrow> monadic_nfoldli x' c f xa \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) xb \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (rule_tac R="br (Pair x') (\<lambda>_. True)" in intro_prgR)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x' \<sigma> b x. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y); FOREACH_inv xs0 I (a # x', \<sigma>); b; x\<rbrakk> \<Longrightarrow> f a \<sigma> \<le> \<Down> (br (Pair x') (\<lambda>_. True)) (f a \<sigma> \<bind> (\<lambda>\<sigma>'. RETURN (x', \<sigma>')))
 2. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> br (Pair x') (\<lambda>_. x)\<rbrakk> \<Longrightarrow> monadic_nfoldli x' c f xa \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) xb \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (simp add: pw_le_iff refine_pw_simps br_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> br (Pair x') (\<lambda>_. x)\<rbrakk> \<Longrightarrow> monadic_nfoldli x' c f xa \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) xb \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> br (Pair x') (\<lambda>_. x)\<rbrakk> \<Longrightarrow> monadic_nfoldli x' c f xa \<le> ?y523 a x' \<sigma> b x xa xb
 2. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> br (Pair x') (\<lambda>_. x)\<rbrakk> \<Longrightarrow> ?y523 a x' \<sigma> b x xa xb \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) xb \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply rprems
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x' \<sigma> b x xa xb. \<lbrakk>\<And>\<sigma>. monadic_nfoldli x' c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)); FOREACH_inv xs0 I (a # x', \<sigma>); (b, x) \<in> bool_rel; b; x; (xa, xb) \<in> br (Pair x') (\<lambda>_. x)\<rbrakk> \<Longrightarrow> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (x', xa) \<bind> (\<lambda>(uu_, y). RETURN y)) \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN ([], \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) xb \<bind> (\<lambda>(uu_, y). RETURN y))
[PROOF STEP]
apply (simp add: br_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma monadic_nfoldli_arities[sepref_monadify_arity]:
  "monadic_nfoldli \<equiv> \<lambda>\<^sub>2s c f \<sigma>. SP (monadic_nfoldli)$s$(\<lambda>\<^sub>2x. c$x)$(\<lambda>\<^sub>2x \<sigma>. f$x$\<sigma>)$\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli \<equiv> \<lambda>x. (#\<lambda>xa. (#\<lambda>xb. (#\<lambda>xc. (#SP monadic_nfoldli $ x $ (\<lambda>x. (#xa $ x#)) $ (\<lambda>x. (#\<lambda>xa. (#xb $ x $ xa#)#)) $ xc#)#)#)#)
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma monadic_nfoldli_comb[sepref_monadify_comb]:
  "\<And>s c f \<sigma>. (monadic_nfoldli)$s$c$f$\<sigma> \<equiv>
    Refine_Basic.bind$(EVAL$s)$(\<lambda>\<^sub>2s. Refine_Basic.bind$(EVAL$\<sigma>)$(\<lambda>\<^sub>2\<sigma>.
      SP (monadic_nfoldli)$s$c$f$\<sigma>
    ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s c f \<sigma>. monadic_nfoldli $ s $ c $ f $ \<sigma> \<equiv> (\<bind>) $ (EVAL $ s) $ (\<lambda>x. (#(\<bind>) $ (EVAL $ \<sigma>) $ (\<lambda>xa. (#SP monadic_nfoldli $ x $ c $ f $ xa#))#))
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma list_rel_congD:
  assumes A: "(li,l)\<in>\<langle>S\<rangle>list_rel"
  shows "(li,l)\<in>\<langle>S\<inter>(set li\<times>set l)\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
fix Si0 S0
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
assume "set li \<subseteq> Si0" "set l \<subseteq> S0"
[PROOF STATE]
proof (state)
this:
set li \<subseteq> Si0
set l \<subseteq> S0

goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
(li, l) \<in> \<langle>S\<rangle>list_rel
set li \<subseteq> Si0
set l \<subseteq> S0
[PROOF STEP]
have "(li,l)\<in>\<langle>S\<inter>(Si0\<times>S0)\<rangle>list_rel"
[PROOF STATE]
proof (prove)
using this:
(li, l) \<in> \<langle>S\<rangle>list_rel
set li \<subseteq> Si0
set l \<subseteq> S0

goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> Si0 \<times> S0\<rangle>list_rel
[PROOF STEP]
by (induction rule: list_rel_induct) auto
[PROOF STATE]
proof (state)
this:
(li, l) \<in> \<langle>S \<inter> Si0 \<times> S0\<rangle>list_rel

goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>set li \<subseteq> ?Si0.2; set l \<subseteq> ?S0.2\<rbrakk> \<Longrightarrow> (li, l) \<in> \<langle>S \<inter> ?Si0.2 \<times> ?S0.2\<rangle>list_rel

goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
from this[OF order_refl order_refl]
[PROOF STATE]
proof (chain)
picking this:
(li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel

goal (1 subgoal):
 1. (li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(li, l) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel

goal:
No subgoals!
[PROOF STEP]
qed