[STATEMENT]
lemma surj_on_mult:
  assumes coprime: "coprime x (q::nat)"
    and inj: "inj_on (\<lambda> b. x*b mod q) {..<q}"
  shows "(\<lambda> b. x*b mod q) ` {..< q} = {..< q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` {..<q} = {..<q}
[PROOF STEP]
apply(rule endo_inj_surj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. x * b mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. x * b mod q) {..<q}
[PROOF STEP]
using coprime inj
[PROOF STATE]
proof (prove)
using this:
coprime x q
inj_on (\<lambda>b. x * b mod q) {..<q}

goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. x * b mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. x * b mod q) {..<q}
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_one_time_pad:
  assumes coprime: "coprime x q"
  shows "map_spmf (\<lambda> b. x*b mod q) (sample_uniform q) = (sample_uniform q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>b. x * b mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
using inj_on_mult surj_on_mult one_time_pad coprime
[PROOF STATE]
proof (prove)
using this:
coprime ?x ?q \<Longrightarrow> inj_on (\<lambda>b. ?x * b mod ?q) {..<?q}
\<lbrakk>coprime ?x ?q; inj_on (\<lambda>b. ?x * b mod ?q) {..<?q}\<rbrakk> \<Longrightarrow> (\<lambda>b. ?x * b mod ?q) ` {..<?q} = {..<?q}
\<lbrakk>inj_on ?f {..<?q}; ?f ` {..<?q} = {..<?q}\<rbrakk> \<Longrightarrow> map_spmf ?f (sample_uniform ?q) = sample_uniform ?q
coprime x q

goal (1 subgoal):
 1. map_spmf (\<lambda>b. x * b mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
by simp


[STATEMENT]
lemma inj_on_mult_units:
  assumes 1: "coprime x (q::nat)" shows "inj_on (\<lambda> b. x*b mod q) ({..<q} - {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})
[PROOF STEP]
apply(auto simp add: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa < q; 0 < xa; y < q; x * xa mod q = x * y mod q; 0 < y\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
coprime x q

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa < q; 0 < xa; y < q; x * xa mod q = x * y mod q; 0 < y\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
by(simp only: inj_mult)


[STATEMENT]
lemma surj_on_mult_units:
  assumes coprime: "coprime x (q::nat)"
    and inj: "inj_on (\<lambda> b. x*b mod q) ({..<q} - {0})"
  shows "(\<lambda> b. x*b mod q) ` ({..<q} - {0}) = ({..<q} - {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) = {..<q} - {0}
[PROOF STEP]
proof(rule endo_inj_surj)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite ({..<q} - {0})
 2. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
 3. inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})
[PROOF STEP]
show "finite ({..<q} - {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({..<q} - {0})
[PROOF STEP]
using coprime inj
[PROOF STATE]
proof (prove)
using this:
coprime x q
inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})

goal (1 subgoal):
 1. finite ({..<q} - {0})
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
finite ({..<q} - {0})

goal (2 subgoals):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
 2. inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})
[PROOF STEP]
show "(\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
obtain n :: "nat set \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat set \<Rightarrow> nat" where
      "\<forall>x0 x1 x2. (\<exists>v3. v3 \<in> x2 \<and> x1 v3 \<notin> x0) = (n x0 x1 x2 \<in> x2 \<and> x1 (n x0 x1 x2) \<notin> x0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<forall>x0 x1 x2. (\<exists>v3. v3 \<in> x2 \<and> x1 v3 \<notin> x0) = (n x0 x1 x2 \<in> x2 \<and> x1 (n x0 x1 x2) \<notin> x0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
\<forall>x0 x1 x2. (\<exists>v3. v3 \<in> x2 \<and> x1 v3 \<notin> x0) = (n x0 x1 x2 \<in> x2 \<and> x1 (n x0 x1 x2) \<notin> x0)

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x0 x1 x2. (\<exists>v3. v3 \<in> x2 \<and> x1 v3 \<notin> x0) = (n x0 x1 x2 \<in> x2 \<and> x1 (n x0 x1 x2) \<notin> x0)
[PROOF STEP]
have subset: "\<forall>N f Na. n Na f N \<in> N \<and> f (n Na f N) \<notin> Na \<or> f ` N \<subseteq> Na"
[PROOF STATE]
proof (prove)
using this:
\<forall>x0 x1 x2. (\<exists>v3. v3 \<in> x2 \<and> x1 v3 \<notin> x0) = (n x0 x1 x2 \<in> x2 \<and> x1 (n x0 x1 x2) \<notin> x0)

goal (1 subgoal):
 1. \<forall>N f Na. n Na f N \<in> N \<and> f (n Na f N) \<notin> Na \<or> f ` N \<subseteq> Na
[PROOF STEP]
by (meson image_subsetI)
[PROOF STATE]
proof (state)
this:
\<forall>N f Na. n Na f N \<in> N \<and> f (n Na f N) \<notin> Na \<or> f ` N \<subseteq> Na

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
have mem_insert: "x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {..<q} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {..<q} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {..<q} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
have map_eq: "(x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} - {0}) = (x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} - {0}) = (x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} - {0}) = (x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0})

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} - {0}) = (x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0})

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
assume "x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q"
[PROOF STATE]
proof (state)
this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q
[PROOF STEP]
have "(0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}"
[PROOF STATE]
proof (prove)
using this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q

goal (1 subgoal):
 1. (0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}
[PROOF STEP]
by (metis antisym_conv1 insertCI lessThan_iff local.coprime inj_mult)
[PROOF STATE]
proof (state)
this:
(0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q \<Longrightarrow> (0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q \<Longrightarrow> (0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q \<Longrightarrow> (0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
assume "0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q"
[PROOF STATE]
proof (state)
this:
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
assume "x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0}"
[PROOF STATE]
proof (state)
this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0}
[PROOF STEP]
have "(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}"
[PROOF STATE]
proof (prove)
using this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0}

goal (1 subgoal):
 1. (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
using map_eq subset
[PROOF STATE]
proof (prove)
using this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0}
(x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} - {0}) = (x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0})
\<forall>N f Na. n Na f N \<in> N \<and> f (n Na f N) \<notin> Na \<or> f ` N \<subseteq> Na

goal (1 subgoal):
 1. (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
by (meson Diff_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0} \<Longrightarrow> (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0} \<Longrightarrow> (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
have "(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> (0 \<le> q) = (0 = q)"
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0} \<Longrightarrow> (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> (0 \<le> q) = (0 = q)
[PROOF STEP]
using mem_insert
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q} \<and> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {0} \<Longrightarrow> (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<notin> {..<q} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> insert 0 {..<q}

goal (1 subgoal):
 1. (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> (0 \<le> q) = (0 = q)
[PROOF STEP]
by (metis antisym_conv1 lessThan_iff mod_less_divisor singletonD)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> (0 \<le> q) = (0 = q)

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<Longrightarrow> (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> (0 \<le> q) = (0 = q)

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q \<Longrightarrow> (0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<Longrightarrow> (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> (0 \<le> q) = (0 = q)
[PROOF STEP]
have "(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}"
[PROOF STATE]
proof (prove)
using this:
x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q \<Longrightarrow> (0 \<le> q) = (0 = q) \<or> (n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<in> {0}) \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}
0 \<noteq> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<Longrightarrow> (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> (0 \<le> q) = (0 = q)

goal (1 subgoal):
 1. (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}
[PROOF STEP]
show "(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}

goal (1 subgoal):
 1. (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
using subset
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0} \<or> n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) \<notin> {..<q} - {0} \<or> x * n ({..<q} - {0}) (\<lambda>n. x * n mod q) ({..<q} - {0}) mod q \<in> {..<q} - {0}
\<forall>N f Na. n Na f N \<in> N \<and> f (n Na f N) \<notin> Na \<or> f ` N \<subseteq> Na

goal (1 subgoal):
 1. (\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
(\<lambda>n. x * n mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>b. x * b mod q) ` ({..<q} - {0}) \<subseteq> {..<q} - {0}

goal (1 subgoal):
 1. inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})
[PROOF STEP]
show "inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
coprime x q
inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})

goal (1 subgoal):
 1. inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>b. x * b mod q) ({..<q} - {0})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_one_time_pad_units:
  assumes coprime: "coprime x q"
  shows "map_spmf (\<lambda> b. x*b mod q) (sample_uniform_units q) = sample_uniform_units q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>b. x * b mod q) (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
using inj_on_mult_units surj_on_mult_units one_time_pad_units coprime
[PROOF STATE]
proof (prove)
using this:
coprime ?x ?q \<Longrightarrow> inj_on (\<lambda>b. ?x * b mod ?q) ({..<?q} - {0})
\<lbrakk>coprime ?x ?q; inj_on (\<lambda>b. ?x * b mod ?q) ({..<?q} - {0})\<rbrakk> \<Longrightarrow> (\<lambda>b. ?x * b mod ?q) ` ({..<?q} - {0}) = {..<?q} - {0}
\<lbrakk>inj_on ?f ({..<?q} - {0}); ?f ` ({..<?q} - {0}) = {..<?q} - {0}\<rbrakk> \<Longrightarrow> map_spmf ?f (sample_uniform_units ?q) = sample_uniform_units ?q
coprime x q

goal (1 subgoal):
 1. map_spmf (\<lambda>b. x * b mod q) (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
by simp


[STATEMENT]
lemma samp_uni_add_mult:
  assumes coprime: "coprime x (q::nat)"
    and xa: "xa < q"
    and ya: "ya < q"
    and map: "(y + x * xa) mod q = (y + x * ya) mod q"
  shows "xa = ya"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa = ya
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xa = ya
[PROOF STEP]
have "(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q
[PROOF STEP]
have "(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> [y + x*xa = y + x *ya] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> [y + x * xa = y + x * ya] (mod q)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. (y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> [y + x * xa = y + x * ya] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> [y + x * xa = y + x * ya] (mod q)

goal (1 subgoal):
 1. (y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> [y + x * xa = y + x * ya] (mod q)

goal (1 subgoal):
 1. (y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q
[PROOF STEP]
have "[y + x*xa = y + x *ya] (mod q) \<Longrightarrow> [xa = ya] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y + x * xa = y + x * ya] (mod q) \<Longrightarrow> [xa = ya] (mod q)
[PROOF STEP]
by(simp add: cong_add_lcancel_nat)(simp add: coprime cong_mult_lcancel_nat)
[PROOF STATE]
proof (state)
this:
[y + x * xa = y + x * ya] (mod q) \<Longrightarrow> [xa = ya] (mod q)

goal (1 subgoal):
 1. (y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> [y + x * xa = y + x * ya] (mod q)
[y + x * xa = y + x * ya] (mod q) \<Longrightarrow> [xa = ya] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> [y + x * xa = y + x * ya] (mod q)
[y + x * xa = y + x * ya] (mod q) \<Longrightarrow> [xa = ya] (mod q)

goal (1 subgoal):
 1. xa mod q = ya mod q
[PROOF STEP]
by(simp add: cong_def map)
[PROOF STATE]
proof (state)
this:
xa mod q = ya mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q

goal (1 subgoal):
 1. xa = ya
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q

goal (1 subgoal):
 1. xa = ya
[PROOF STEP]
have "xa mod q = ya mod q \<Longrightarrow> xa = ya"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa mod q = ya mod q \<Longrightarrow> xa = ya
[PROOF STEP]
by(simp add: xa ya)
[PROOF STATE]
proof (state)
this:
xa mod q = ya mod q \<Longrightarrow> xa = ya

goal (1 subgoal):
 1. xa = ya
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q
xa mod q = ya mod q \<Longrightarrow> xa = ya
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(y + x * xa) mod q = (y + x * ya) mod q \<Longrightarrow> xa mod q = ya mod q
xa mod q = ya mod q \<Longrightarrow> xa = ya

goal (1 subgoal):
 1. xa = ya
[PROOF STEP]
by(simp add: map)
[PROOF STATE]
proof (state)
this:
xa = ya

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_add_mult:
  assumes coprime: "coprime x (q::nat)"
  shows "inj_on (\<lambda> b. (y + x*b) mod q) {..<q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>b. (y + x * b) mod q) {..<q}
[PROOF STEP]
apply(auto simp add: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>xa < q; ya < q; (y + x * xa) mod q = (y + x * ya) mod q\<rbrakk> \<Longrightarrow> xa = ya
[PROOF STEP]
using coprime
[PROOF STATE]
proof (prove)
using this:
coprime x q

goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>xa < q; ya < q; (y + x * xa) mod q = (y + x * ya) mod q\<rbrakk> \<Longrightarrow> xa = ya
[PROOF STEP]
by(simp only: samp_uni_add_mult)


[STATEMENT]
lemma surj_on_add_mult: assumes coprime: "coprime x (q::nat)" and inj: "inj_on (\<lambda> b. (y + x*b) mod q) {..<q}"
  shows "(\<lambda> b. (y + x*b) mod q) ` {..< q} = {..< q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. (y + x * b) mod q) ` {..<q} = {..<q}
[PROOF STEP]
apply(rule endo_inj_surj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. (y + x * b) mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. (y + x * b) mod q) {..<q}
[PROOF STEP]
using coprime inj
[PROOF STATE]
proof (prove)
using this:
coprime x q
inj_on (\<lambda>b. (y + x * b) mod q) {..<q}

goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. (y + x * b) mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. (y + x * b) mod q) {..<q}
[PROOF STEP]
by auto


[STATEMENT]
lemma add_mult_one_time_pad: assumes coprime: "coprime x q"
  shows "map_spmf (\<lambda> b. (y + x*b) mod q) (sample_uniform q) = (sample_uniform q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>b. (y + x * b) mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
using inj_on_add_mult surj_on_add_mult one_time_pad coprime
[PROOF STATE]
proof (prove)
using this:
coprime ?x ?q \<Longrightarrow> inj_on (\<lambda>b. (?y + ?x * b) mod ?q) {..<?q}
\<lbrakk>coprime ?x ?q; inj_on (\<lambda>b. (?y + ?x * b) mod ?q) {..<?q}\<rbrakk> \<Longrightarrow> (\<lambda>b. (?y + ?x * b) mod ?q) ` {..<?q} = {..<?q}
\<lbrakk>inj_on ?f {..<?q}; ?f ` {..<?q} = {..<?q}\<rbrakk> \<Longrightarrow> map_spmf ?f (sample_uniform ?q) = sample_uniform ?q
coprime x q

goal (1 subgoal):
 1. map_spmf (\<lambda>b. (y + x * b) mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
by simp


[STATEMENT]
lemma inj_minus:
  assumes x: "(x :: nat) < q"
    and ya: "ya < q"
    and map: "(y + q - x) mod q = (y + q - ya) mod q"
  shows  "x = ya"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = ya
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = ya
[PROOF STEP]
have "(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
[PROOF STEP]
have "(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> [y + q - x = y + q - ya] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> [y + q - x = y + q - ya] (mod q)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> [y + q - x = y + q - ya] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> [y + q - x = y + q - ya] (mod q)

goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> [y + q - x = y + q - ya] (mod q)

goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
[PROOF STEP]
have "[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q - x = q - ya] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q - x = q - ya] (mod q)
[PROOF STEP]
using x ya cong_add_lcancel_nat
[PROOF STATE]
proof (prove)
using this:
x < q
ya < q
[?a + ?x = ?a + ?y] (mod ?n) = [?x = ?y] (mod ?n)

goal (1 subgoal):
 1. [y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q - x = q - ya] (mod q)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q - x = q - ya] (mod q)

goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q - x = q - ya] (mod q)

goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
[PROOF STEP]
have "[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q + x = q + ya] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q + x = q + ya] (mod q)
[PROOF STEP]
by (metis add_diff_inverse_nat calculation(2) cong_add_lcancel_nat cong_add_rcancel_nat cong_sym less_imp_le_nat not_le x ya)
[PROOF STATE]
proof (state)
this:
[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q + x = q + ya] (mod q)

goal (1 subgoal):
 1. (y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> [y + q - x = y + q - ya] (mod q)
[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q - x = q - ya] (mod q)
[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q + x = q + ya] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> [y + q - x = y + q - ya] (mod q)
[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q - x = q - ya] (mod q)
[y + q - x = y + q - ya] (mod q) \<Longrightarrow> [q + x = q + ya] (mod q)

goal (1 subgoal):
 1. x mod q = ya mod q
[PROOF STEP]
by (simp add: cong_def map)
[PROOF STATE]
proof (state)
this:
x mod q = ya mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q

goal (1 subgoal):
 1. x = ya
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q

goal (1 subgoal):
 1. x = ya
[PROOF STEP]
have "x mod q = ya mod q \<Longrightarrow> x = ya"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mod q = ya mod q \<Longrightarrow> x = ya
[PROOF STEP]
by(simp add: x ya)
[PROOF STATE]
proof (state)
this:
x mod q = ya mod q \<Longrightarrow> x = ya

goal (1 subgoal):
 1. x = ya
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
x mod q = ya mod q \<Longrightarrow> x = ya
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(y + q - x) mod q = (y + q - ya) mod q \<Longrightarrow> x mod q = ya mod q
x mod q = ya mod q \<Longrightarrow> x = ya

goal (1 subgoal):
 1. x = ya
[PROOF STEP]
by(simp add: map)
[PROOF STATE]
proof (state)
this:
x = ya

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_minus: "inj_on  (\<lambda>(b :: nat). (y + (q - b)) mod q ) {..<q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>b. (y + (q - b)) mod q) {..<q}
[PROOF STEP]
by(auto simp add: inj_on_def inj_minus)


[STATEMENT]
lemma surj_on_minus:
  assumes inj: "inj_on  (\<lambda>(b :: nat). (y + (q - b)) mod q ) {..<q}"
  shows "(\<lambda>(b :: nat). (y + (q - b)) mod q) ` {..< q} = {..< q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. (y + (q - b)) mod q) ` {..<q} = {..<q}
[PROOF STEP]
apply(rule endo_inj_surj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. (y + (q - b)) mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. (y + (q - b)) mod q) {..<q}
[PROOF STEP]
using inj
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>b. (y + (q - b)) mod q) {..<q}

goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. (y + (q - b)) mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. (y + (q - b)) mod q) {..<q}
[PROOF STEP]
by auto


[STATEMENT]
lemma samp_uni_minus_one_time_pad:
  shows "map_spmf(\<lambda> b. (y + (q - b)) mod q) (sample_uniform q) = (sample_uniform q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
using inj_on_minus surj_on_minus one_time_pad
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>b. (?y + (?q - b)) mod ?q) {..<?q}
inj_on (\<lambda>b. (?y + (?q - b)) mod ?q) {..<?q} \<Longrightarrow> (\<lambda>b. (?y + (?q - b)) mod ?q) ` {..<?q} = {..<?q}
\<lbrakk>inj_on ?f {..<?q}; ?f ` {..<?q} = {..<?q}\<rbrakk> \<Longrightarrow> map_spmf ?f (sample_uniform ?q) = sample_uniform ?q

goal (1 subgoal):
 1. map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
by simp


[STATEMENT]
lemma not_coin_flip: "map_spmf (\<lambda> a. \<not> a) coin_spmf = coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf Not coin_spmf = coin_spmf
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_spmf Not coin_spmf = coin_spmf
[PROOF STEP]
have "inj_on Not {True, False}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Not {True, False}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inj_on Not {True, False}

goal (1 subgoal):
 1. map_spmf Not coin_spmf = coin_spmf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inj_on Not {True, False}

goal (1 subgoal):
 1. map_spmf Not coin_spmf = coin_spmf
[PROOF STEP]
have  "Not ` {True, False} = {True, False}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Not ` {True, False} = {True, False}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Not ` {True, False} = {True, False}

goal (1 subgoal):
 1. map_spmf Not coin_spmf = coin_spmf
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inj_on Not {True, False}
Not ` {True, False} = {True, False}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on Not {True, False}
Not ` {True, False} = {True, False}

goal (1 subgoal):
 1. map_spmf Not coin_spmf = coin_spmf
[PROOF STEP]
using one_time_pad
[PROOF STATE]
proof (prove)
using this:
inj_on Not {True, False}
Not ` {True, False} = {True, False}
\<lbrakk>inj_on ?f {..<?q}; ?f ` {..<?q} = {..<?q}\<rbrakk> \<Longrightarrow> map_spmf ?f (sample_uniform ?q) = sample_uniform ?q

goal (1 subgoal):
 1. map_spmf Not coin_spmf = coin_spmf
[PROOF STEP]
by (simp add: UNIV_bool)
[PROOF STATE]
proof (state)
this:
map_spmf Not coin_spmf = coin_spmf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma xor_uni_samp: "map_spmf(\<lambda> b. y \<oplus> b) (coin_spmf) = map_spmf(\<lambda> b. b) (coin_spmf)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
have rhs: "?rhs = spmf_of_set {True, False}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>b. b) coin_spmf = spmf_of_set {True, False}
[PROOF STEP]
by (simp add: UNIV_bool insert_commute)
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>b. b) coin_spmf = spmf_of_set {True, False}

goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>b. b) coin_spmf = spmf_of_set {True, False}

goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
have "map_spmf(\<lambda> b. y \<oplus> b) (spmf_of_set {True, False}) = spmf_of_set((\<lambda> b. y \<oplus> b) ` {True, False})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) (spmf_of_set {True, False}) = spmf_of_set ((\<oplus>) y ` {True, False})
[PROOF STEP]
by (simp add: xor_def)
[PROOF STATE]
proof (state)
this:
map_spmf ((\<oplus>) y) (spmf_of_set {True, False}) = spmf_of_set ((\<oplus>) y ` {True, False})

goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf ((\<oplus>) y) (spmf_of_set {True, False}) = spmf_of_set ((\<oplus>) y ` {True, False})

goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
have "(\<lambda> b. xor y b) ` {True, False} = {True, False}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<oplus>) y ` {True, False} = {True, False}
[PROOF STEP]
using xor_def
[PROOF STATE]
proof (prove)
using this:
?x \<oplus> ?y = (?x \<squnion> ?y) \<sqinter> - (?x \<sqinter> ?y)

goal (1 subgoal):
 1. (\<oplus>) y ` {True, False} = {True, False}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<oplus>) y ` {True, False} = {True, False}

goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map_spmf ((\<oplus>) y) (map_spmf (\<lambda>b. b) coin_spmf) = spmf_of_set {True, False}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_spmf ((\<oplus>) y) (map_spmf (\<lambda>b. b) coin_spmf) = spmf_of_set {True, False}

goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
using rhs
[PROOF STATE]
proof (prove)
using this:
map_spmf ((\<oplus>) y) (map_spmf (\<lambda>b. b) coin_spmf) = spmf_of_set {True, False}
map_spmf (\<lambda>b. b) coin_spmf = spmf_of_set {True, False}

goal (1 subgoal):
 1. map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
map_spmf ((\<oplus>) y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eff_NatRuleI:
  "nat_rule rule c ants
    \<Longrightarrow> entail = (\<Gamma> \<turnstile> subst s (freshen a c))
    \<Longrightarrow> hyps = ((\<lambda>ant. ((\<lambda>p. subst s (freshen a p)) |`| a_hyps ant |\<union>| \<Gamma> \<turnstile> subst s (freshen a (a_conc ant)))) |`| ants)
    \<Longrightarrow> (\<And> ant f. ant |\<in>| ants \<Longrightarrow> f |\<in>| \<Gamma> \<Longrightarrow> freshenLC a ` (a_fresh ant) \<inter> lconsts f = {})
    \<Longrightarrow> (\<And> ant. ant |\<in>| ants \<Longrightarrow> freshenLC a ` (a_fresh ant) \<inter> subst_lconsts s = {})
    \<Longrightarrow> eff (NatRule rule) entail hyps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nat_rule rule c ants; entail = (\<Gamma> \<turnstile> subst s (freshen a c)); hyps = (\<lambda>ant. (\<lambda>p. subst s (freshen a p)) |`| a_hyps ant |\<union>| \<Gamma> \<turnstile> subst s (freshen a (a_conc ant))) |`| ants; \<And>ant f. \<lbrakk>ant |\<in>| ants; f |\<in>| \<Gamma>\<rbrakk> \<Longrightarrow> freshenLC a ` a_fresh ant \<inter> lconsts f = {}; \<And>ant. ant |\<in>| ants \<Longrightarrow> freshenLC a ` a_fresh ant \<inter> subst_lconsts s = {}\<rbrakk> \<Longrightarrow> eff (NatRule rule) entail hyps
[PROOF STEP]
by (drule eff.intros(2)) simp_all


[STATEMENT]
lemma  natEff_InstI:
  "rule = (r,c)
  \<Longrightarrow> c \<in> set (consequent r)
  \<Longrightarrow> antec = f_antecedent r
  \<Longrightarrow> natEff_Inst rule c antec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rule = (r, c); c \<in> set (consequent r); antec = f_antecedent r\<rbrakk> \<Longrightarrow> natEff_Inst rule c antec
[PROOF STEP]
by (metis natEff_Inst.intros)


[STATEMENT]
lemma fv_subst_s1[simp]: "fv_subst s1 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv_subst s1 = {}
[PROOF STEP]
by (simp add: fv_subst_def)


[STATEMENT]
lemma subst1_simps[simp]:
  "subst s1 (P (LC n)) = imp (Q (LC n)) (Q (LC n))"
  "subst s1 (ForallX (P x)) = ForallX (imp (Q x) (Q x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst s1 (P (LC n)) = imp (Q (LC n)) (Q (LC n)) &&& subst s1 (ForallX (P x)) = ForallX (imp (Q x) (Q x))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma subst2_simps[simp]:
    "subst s2 X = Q (LC lx)"
    "subst s2 Y = Q (LC lx)"
    "subst s2 (imp X Y) = imp (subst s2 X) (subst s2 Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst s2 X = Q (LC lx) &&& subst s2 Y = Q (LC lx) &&& subst s2 (imp X Y) = imp (subst s2 X) (subst s2 Y)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma substI1: "ForallX (imp (Q x) (Q x)) = subst s1 (predicate.freshen 1 (ForallX (P x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ForallX (imp (Q x) (Q x)) = subst s1 (predicate.freshen 1 (ForallX (P x)))
[PROOF STEP]
by (auto simp add: predicate.freshen_def Let_def)


[STATEMENT]
lemma substI2: "imp (Q (LC lx)) (Q (LC lx)) = subst s2 (predicate.freshen 2 (imp X Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp (Q (LC lx)) (Q (LC lx)) = subst s2 (predicate.freshen 2 (imp X Y))
[PROOF STEP]
by (auto simp add: predicate.freshen_def Let_def)


[STATEMENT]
lemma "task.solved"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. task.solved
[PROOF STEP]
unfolding task.solved_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. c |\<in>| task.conc_forms \<longrightarrow> (\<exists>\<Gamma> t. fst (tree.root t) = (\<Gamma> \<turnstile> c) \<and> \<Gamma> |\<subseteq>| task.ass_forms \<and> task.wf t \<and> tfinite t)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<Gamma> t. fst (tree.root t) = (\<Gamma> \<turnstile> ForallX (imp (Q x) (Q x))) \<and> \<Gamma> |\<subseteq>| task.ass_forms \<and> task.wf t \<and> tfinite t
[PROOF STEP]
apply (rule_tac x="{||}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. fst (tree.root t) = ({||} \<turnstile> ForallX (imp (Q x) (Q x))) \<and> {||} |\<subseteq>| task.ass_forms \<and> task.wf t \<and> tfinite t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. fst (tree.root t) = ({||} \<turnstile> ForallX (imp (Q x) (Q x))) \<and> task.wf t \<and> tfinite t
[PROOF STEP]
apply (rule_tac x="solution_tree" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (tree.root solution_tree) = ({||} \<turnstile> ForallX (imp (Q x) (Q x))) \<and> task.wf solution_tree \<and> tfinite solution_tree
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. task.wf solution_tree \<and> tfinite solution_tree
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. task.wf solution_tree
 2. tfinite solution_tree
[PROOF STEP]
apply (rule task.wf)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. snd (tree.root solution_tree) \<in> task.R
 2. task.effStep (tree.root solution_tree) ((fst \<circ> tree.root) |`| cont solution_tree)
 3. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 4. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>(auto simp add: stream.set_map task.n_rules_def)[1]\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. task.effStep (tree.root solution_tree) ((fst \<circ> tree.root) |`| cont solution_tree)
 2. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 3. tfinite solution_tree
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. task.eff (NatRule (allI, ForallX (P x))) ({||} \<turnstile> ForallX (imp (Q x) (Q x))) {|{||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))|}
 2. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 3. tfinite solution_tree
[PROOF STEP]
apply (rule task.eff_NatRuleI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. task.natEff_Inst (allI, ForallX (P x)) ?c55 ?ants55
 2. ({||} \<turnstile> ForallX (imp (Q x) (Q x))) = (?\<Gamma>55 \<turnstile> subst ?s55 (predicate.freshen ?a55 ?c55))
 3. {|{||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))|} = (\<lambda>ant. (\<lambda>p. subst ?s55 (predicate.freshen ?a55 p)) |`| a_hyps ant |\<union>| ?\<Gamma>55 \<turnstile> subst ?s55 (predicate.freshen ?a55 (a_conc ant))) |`| ?ants55
 4. \<And>ant f. \<lbrakk>ant |\<in>| ?ants55; f |\<in>| ?\<Gamma>55\<rbrakk> \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc f = {}
 5. \<And>ant. ant |\<in>| ?ants55 \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc_subst ?s55 = {}
 6. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 7. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>rule task.natEff_Inst.intros;simp\<close>)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. ({||} \<turnstile> ForallX (imp (Q x) (Q x))) = (?\<Gamma>55 \<turnstile> subst ?s55 (predicate.freshen ?a55 (ForallX (P x))))
 2. {|{||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))|} = (\<lambda>ant. (\<lambda>p. subst ?s55 (predicate.freshen ?a55 p)) |`| a_hyps ant |\<union>| ?\<Gamma>55 \<turnstile> subst ?s55 (predicate.freshen ?a55 (a_conc ant))) |`| predicate.f_antecedent allI
 3. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| ?\<Gamma>55\<rbrakk> \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc f = {}
 4. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc_subst ?s55 = {}
 5. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 6. tfinite solution_tree
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. {||} = ?\<Gamma>55 \<and> ForallX (imp (Q x) (Q x)) = subst ?s55 (predicate.freshen ?a55 (ForallX (P x)))
 2. {|{||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))|} = (\<lambda>ant. (\<lambda>p. subst ?s55 (predicate.freshen ?a55 p)) |`| a_hyps ant |\<union>| ?\<Gamma>55 \<turnstile> subst ?s55 (predicate.freshen ?a55 (a_conc ant))) |`| predicate.f_antecedent allI
 3. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| ?\<Gamma>55\<rbrakk> \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc f = {}
 4. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc_subst ?s55 = {}
 5. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 6. tfinite solution_tree
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. {||} = ?\<Gamma>55
 2. ForallX (imp (Q x) (Q x)) = subst ?s55 (predicate.freshen ?a55 (ForallX (P x)))
 3. {|{||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))|} = (\<lambda>ant. (\<lambda>p. subst ?s55 (predicate.freshen ?a55 p)) |`| a_hyps ant |\<union>| ?\<Gamma>55 \<turnstile> subst ?s55 (predicate.freshen ?a55 (a_conc ant))) |`| predicate.f_antecedent allI
 4. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| ?\<Gamma>55\<rbrakk> \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc f = {}
 5. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc_subst ?s55 = {}
 6. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 7. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp\<close>)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. ForallX (imp (Q x) (Q x)) = subst ?s55 (predicate.freshen ?a55 (ForallX (P x)))
 2. {|{||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))|} = (\<lambda>ant. (\<lambda>p. subst ?s55 (predicate.freshen ?a55 p)) |`| a_hyps ant |\<union>| {||} \<turnstile> subst ?s55 (predicate.freshen ?a55 (a_conc ant))) |`| predicate.f_antecedent allI
 3. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc f = {}
 4. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat ?a55 ` a_fresh ant \<inter> lc_subst ?s55 = {}
 5. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 6. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>rule substI1\<close>)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. {|{||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))|} = (\<lambda>ant. (\<lambda>p. subst s1 (predicate.freshen 1 p)) |`| a_hyps ant |\<union>| {||} \<turnstile> subst s1 (predicate.freshen 1 (a_conc ant))) |`| predicate.f_antecedent allI
 2. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc f = {}
 3. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc_subst s1 = {}
 4. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 5. tfinite solution_tree
[PROOF STEP]
apply (simp add: predicate.f_antecedent_def predicate.freshen_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. imp (Q (LC lx)) (Q (LC lx)) = subst s1 (map_lc (\<lambda>x. to_nat (1, x)) (a_conc allI_input))
 2. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc f = {}
 3. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc_subst s1 = {}
 4. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 5. tfinite solution_tree
[PROOF STEP]
apply (subst antecedent.sel(2))
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. imp (Q (LC lx)) (Q (LC lx)) = subst s1 (map_lc (\<lambda>x. to_nat (1, x)) (P (LC 0)))
 2. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc f = {}
 3. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc_subst s1 = {}
 4. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 5. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent allI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc f = {}
 2. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc_subst s1 = {}
 3. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 4. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ant. ant |\<in>| predicate.f_antecedent allI \<Longrightarrow> curry to_nat 1 ` a_fresh ant \<inter> lc_subst s1 = {}
 2. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 3. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t'. t' |\<in>| cont solution_tree \<Longrightarrow> task.wf t'
 2. tfinite solution_tree
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. task.wf imp_tree
 2. tfinite solution_tree
[PROOF STEP]
apply (rule task.wf)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. snd (tree.root imp_tree) \<in> task.R
 2. task.effStep (tree.root imp_tree) ((fst \<circ> tree.root) |`| cont imp_tree)
 3. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 4. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>(auto simp add: stream.set_map task.n_rules_def)[1]\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. task.effStep (tree.root imp_tree) ((fst \<circ> tree.root) |`| cont imp_tree)
 2. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 3. tfinite solution_tree
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. task.eff (NatRule (impI, imp X Y)) ({||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))) {|{|Q (LC lx)|} \<turnstile> Q (LC lx)|}
 2. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 3. tfinite solution_tree
[PROOF STEP]
apply (rule task.eff_NatRuleI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. task.natEff_Inst (impI, imp X Y) ?c97 ?ants97
 2. ({||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))) = (?\<Gamma>97 \<turnstile> subst ?s97 (predicate.freshen ?a97 ?c97))
 3. {|{|Q (LC lx)|} \<turnstile> Q (LC lx)|} = (\<lambda>ant. (\<lambda>p. subst ?s97 (predicate.freshen ?a97 p)) |`| a_hyps ant |\<union>| ?\<Gamma>97 \<turnstile> subst ?s97 (predicate.freshen ?a97 (a_conc ant))) |`| ?ants97
 4. \<And>ant f. \<lbrakk>ant |\<in>| ?ants97; f |\<in>| ?\<Gamma>97\<rbrakk> \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc f = {}
 5. \<And>ant. ant |\<in>| ?ants97 \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc_subst ?s97 = {}
 6. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 7. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>rule task.natEff_Inst.intros; simp\<close>)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. ({||} \<turnstile> imp (Q (LC lx)) (Q (LC lx))) = (?\<Gamma>97 \<turnstile> subst ?s97 (predicate.freshen ?a97 (imp X Y)))
 2. {|{|Q (LC lx)|} \<turnstile> Q (LC lx)|} = (\<lambda>ant. (\<lambda>p. subst ?s97 (predicate.freshen ?a97 p)) |`| a_hyps ant |\<union>| ?\<Gamma>97 \<turnstile> subst ?s97 (predicate.freshen ?a97 (a_conc ant))) |`| predicate.f_antecedent impI
 3. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent impI; f |\<in>| ?\<Gamma>97\<rbrakk> \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc f = {}
 4. \<And>ant. ant |\<in>| predicate.f_antecedent impI \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc_subst ?s97 = {}
 5. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 6. tfinite solution_tree
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. {||} = ?\<Gamma>97 \<and> imp (Q (LC lx)) (Q (LC lx)) = subst ?s97 (predicate.freshen ?a97 (imp X Y))
 2. {|{|Q (LC lx)|} \<turnstile> Q (LC lx)|} = (\<lambda>ant. (\<lambda>p. subst ?s97 (predicate.freshen ?a97 p)) |`| a_hyps ant |\<union>| ?\<Gamma>97 \<turnstile> subst ?s97 (predicate.freshen ?a97 (a_conc ant))) |`| predicate.f_antecedent impI
 3. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent impI; f |\<in>| ?\<Gamma>97\<rbrakk> \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc f = {}
 4. \<And>ant. ant |\<in>| predicate.f_antecedent impI \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc_subst ?s97 = {}
 5. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 6. tfinite solution_tree
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. {||} = ?\<Gamma>97
 2. imp (Q (LC lx)) (Q (LC lx)) = subst ?s97 (predicate.freshen ?a97 (imp X Y))
 3. {|{|Q (LC lx)|} \<turnstile> Q (LC lx)|} = (\<lambda>ant. (\<lambda>p. subst ?s97 (predicate.freshen ?a97 p)) |`| a_hyps ant |\<union>| ?\<Gamma>97 \<turnstile> subst ?s97 (predicate.freshen ?a97 (a_conc ant))) |`| predicate.f_antecedent impI
 4. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent impI; f |\<in>| ?\<Gamma>97\<rbrakk> \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc f = {}
 5. \<And>ant. ant |\<in>| predicate.f_antecedent impI \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc_subst ?s97 = {}
 6. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 7. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp\<close>)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. imp (Q (LC lx)) (Q (LC lx)) = subst ?s97 (predicate.freshen ?a97 (imp X Y))
 2. {|{|Q (LC lx)|} \<turnstile> Q (LC lx)|} = (\<lambda>ant. (\<lambda>p. subst ?s97 (predicate.freshen ?a97 p)) |`| a_hyps ant |\<union>| {||} \<turnstile> subst ?s97 (predicate.freshen ?a97 (a_conc ant))) |`| predicate.f_antecedent impI
 3. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent impI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc f = {}
 4. \<And>ant. ant |\<in>| predicate.f_antecedent impI \<Longrightarrow> curry to_nat ?a97 ` a_fresh ant \<inter> lc_subst ?s97 = {}
 5. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 6. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>rule substI2\<close>)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. {|{|Q (LC lx)|} \<turnstile> Q (LC lx)|} = (\<lambda>ant. (\<lambda>p. subst s2 (predicate.freshen 2 p)) |`| a_hyps ant |\<union>| {||} \<turnstile> subst s2 (predicate.freshen 2 (a_conc ant))) |`| predicate.f_antecedent impI
 2. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent impI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat 2 ` a_fresh ant \<inter> lc f = {}
 3. \<And>ant. ant |\<in>| predicate.f_antecedent impI \<Longrightarrow> curry to_nat 2 ` a_fresh ant \<inter> lc_subst s2 = {}
 4. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 5. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp add: predicate.f_antecedent_def predicate.freshen_def\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ant f. \<lbrakk>ant |\<in>| predicate.f_antecedent impI; f |\<in>| {||}\<rbrakk> \<Longrightarrow> curry to_nat 2 ` a_fresh ant \<inter> lc f = {}
 2. \<And>ant. ant |\<in>| predicate.f_antecedent impI \<Longrightarrow> curry to_nat 2 ` a_fresh ant \<inter> lc_subst s2 = {}
 3. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 4. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ant. ant |\<in>| predicate.f_antecedent impI \<Longrightarrow> curry to_nat 2 ` a_fresh ant \<inter> lc_subst s2 = {}
 2. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 3. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>simp add: predicate.f_antecedent_def\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t'. t' |\<in>| cont imp_tree \<Longrightarrow> task.wf t'
 2. tfinite solution_tree
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. task.wf base_tree
 2. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>(auto intro: task.wf intro!: task.eff.intros(1))[1]\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tfinite solution_tree
[PROOF STEP]
apply (solves \<open>(rule tfinite.intros, simp)+\<close>)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma no_path_01[simp]: "task.path 0 v pth \<longleftrightarrow> (pth = [] \<and> v = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. task.path 0 v pth = (pth = [] \<and> v = 0)
[PROOF STEP]
by (cases pth) (auto simp add: task.path_cons_simp)


[STATEMENT]
lemma no_path_12[simp]: "\<not> task.path 1 2 pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> task.path 1 2 pth
[PROOF STEP]
by (cases pth) (auto simp add: task.path_cons_simp)


[STATEMENT]
lemma path_20:
  assumes "task.path 2 0 pth"
  shows "(1, allI_input) \<in> snd ` set pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
assume "task.path v 0 pth"
[PROOF STATE]
proof (state)
this:
task.path v 0 pth

goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
hence "v = 0 \<or> v = 1 \<or> (1, allI_input) \<in> snd ` set pth"
[PROOF STATE]
proof (prove)
using this:
task.path v 0 pth

goal (1 subgoal):
 1. v = 0 \<or> v = 1 \<or> (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
by (induction v "0::nat" pth rule: task.path.induct) auto
[PROOF STATE]
proof (state)
this:
v = 0 \<or> v = 1 \<or> (1, allI_input) \<in> snd ` set pth

goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
task.path ?v3 0 pth \<Longrightarrow> ?v3 = 0 \<or> ?v3 = 1 \<or> (1, allI_input) \<in> snd ` set pth

goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
from this[OF assms]
[PROOF STATE]
proof (chain)
picking this:
2 = 0 \<or> 2 = 1 \<or> (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 = 0 \<or> 2 = 1 \<or> (1, allI_input) \<in> snd ` set pth

goal (1 subgoal):
 1. (1, allI_input) \<in> snd ` set pth
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1, allI_input) \<in> snd ` set pth

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scope_21: "2 \<in> task.scope (1, allI_input)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<in> task.scope (1, allI_input)
[PROOF STEP]
by (auto intro!: task.scope.intros elim: path_20 simp add: task.outPortsRule_def predicate.f_antecedent_def predicate.f_consequent_def)


[STATEMENT]
lemma Resolution_weaken: "S \<turnstile> D \<Longrightarrow> T \<union> S \<turnstile> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<turnstile> D \<Longrightarrow> T \<union> S \<turnstile> D
[PROOF STEP]
by(induction rule: Resolution.induct; auto intro: Resolution.intros)


[STATEMENT]
lemma Resolution_unnecessary:
  assumes sd: "\<forall>C \<in> T. S \<turnstile> C"
  shows "T \<union> S \<turnstile> D \<longleftrightarrow> S \<turnstile> D" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (T \<union> S \<turnstile> D) = (S \<turnstile> D)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T \<union> S \<turnstile> D \<Longrightarrow> S \<turnstile> D
 2. S \<turnstile> D \<Longrightarrow> T \<union> S \<turnstile> D
[PROOF STEP]
assume ?l
[PROOF STATE]
proof (state)
this:
T \<union> S \<turnstile> D

goal (2 subgoals):
 1. T \<union> S \<turnstile> D \<Longrightarrow> S \<turnstile> D
 2. S \<turnstile> D \<Longrightarrow> T \<union> S \<turnstile> D
[PROOF STEP]
from \<open>?l\<close> sd
[PROOF STATE]
proof (chain)
picking this:
T \<union> S \<turnstile> D
\<forall>C\<in>T. S \<turnstile> C
[PROOF STEP]
show  ?r
[PROOF STATE]
proof (prove)
using this:
T \<union> S \<turnstile> D
\<forall>C\<in>T. S \<turnstile> C

goal (1 subgoal):
 1. S \<turnstile> D
[PROOF STEP]
proof(induction "T \<union> S" D rule: Resolution.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>C \<in> T \<union> S; Ball T (Resolution S)\<rbrakk> \<Longrightarrow> S \<turnstile> C
 2. \<And>C D k. \<lbrakk>T \<union> S \<turnstile> C; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> C; T \<union> S \<turnstile> D; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> D; k\<^sup>+ \<in> C; k\<inverse> \<in> D; Ball T (Resolution S)\<rbrakk> \<Longrightarrow> S \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>})
[PROOF STEP]
case (Ass D)
[PROOF STATE]
proof (state)
this:
D \<in> T \<union> S
Ball T (Resolution S)

goal (2 subgoals):
 1. \<And>C. \<lbrakk>C \<in> T \<union> S; Ball T (Resolution S)\<rbrakk> \<Longrightarrow> S \<turnstile> C
 2. \<And>C D k. \<lbrakk>T \<union> S \<turnstile> C; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> C; T \<union> S \<turnstile> D; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> D; k\<^sup>+ \<in> C; k\<inverse> \<in> D; Ball T (Resolution S)\<rbrakk> \<Longrightarrow> S \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<turnstile> D
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> S \<turnstile> D
 2. \<not> ?P \<Longrightarrow> S \<turnstile> D
[PROOF STEP]
assume "D \<in> S"
[PROOF STATE]
proof (state)
this:
D \<in> S

goal (2 subgoals):
 1. ?P \<Longrightarrow> S \<turnstile> D
 2. \<not> ?P \<Longrightarrow> S \<turnstile> D
[PROOF STEP]
with Resolution.Ass
[PROOF STATE]
proof (chain)
picking this:
?C \<in> ?S \<Longrightarrow> ?S \<turnstile> ?C
D \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?C \<in> ?S \<Longrightarrow> ?S \<turnstile> ?C
D \<in> S

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

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

goal (1 subgoal):
 1. D \<notin> S \<Longrightarrow> S \<turnstile> D
[PROOF STEP]
with Ass.hyps
[PROOF STATE]
proof (chain)
picking this:
D \<in> T \<union> S
D \<notin> S
[PROOF STEP]
have "D \<in> T"
[PROOF STATE]
proof (prove)
using this:
D \<in> T \<union> S
D \<notin> S

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

goal (1 subgoal):
 1. D \<notin> S \<Longrightarrow> S \<turnstile> D
[PROOF STEP]
with Ass.prems
[PROOF STATE]
proof (chain)
picking this:
Ball T (Resolution S)
D \<in> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Ball T (Resolution S)
D \<in> T

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

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

goal (1 subgoal):
 1. \<And>C D k. \<lbrakk>T \<union> S \<turnstile> C; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> C; T \<union> S \<turnstile> D; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> D; k\<^sup>+ \<in> C; k\<inverse> \<in> D; Ball T (Resolution S)\<rbrakk> \<Longrightarrow> S \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C D k. \<lbrakk>T \<union> S \<turnstile> C; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> C; T \<union> S \<turnstile> D; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> D; k\<^sup>+ \<in> C; k\<inverse> \<in> D; Ball T (Resolution S)\<rbrakk> \<Longrightarrow> S \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>})
[PROOF STEP]
case (R D H k)
[PROOF STATE]
proof (state)
this:
T \<union> S \<turnstile> D
Ball T (Resolution S) \<Longrightarrow> S \<turnstile> D
T \<union> S \<turnstile> H
Ball T (Resolution S) \<Longrightarrow> S \<turnstile> H
k\<^sup>+ \<in> D
k\<inverse> \<in> H
Ball T (Resolution S)

goal (1 subgoal):
 1. \<And>C D k. \<lbrakk>T \<union> S \<turnstile> C; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> C; T \<union> S \<turnstile> D; Ball T (Resolution S) \<Longrightarrow> S \<turnstile> D; k\<^sup>+ \<in> C; k\<inverse> \<in> D; Ball T (Resolution S)\<rbrakk> \<Longrightarrow> S \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>})
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
T \<union> S \<turnstile> D
Ball T (Resolution S) \<Longrightarrow> S \<turnstile> D
T \<union> S \<turnstile> H
Ball T (Resolution S) \<Longrightarrow> S \<turnstile> H
k\<^sup>+ \<in> D
k\<inverse> \<in> H
Ball T (Resolution S)

goal (1 subgoal):
 1. S \<turnstile> D - {k\<^sup>+} \<union> (H - {k\<inverse>})
[PROOF STEP]
by (simp add: Resolution.R)
[PROOF STATE]
proof (state)
this:
S \<turnstile> D - {k\<^sup>+} \<union> (H - {k\<inverse>})

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

goal (1 subgoal):
 1. S \<turnstile> D \<Longrightarrow> T \<union> S \<turnstile> D
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<turnstile> D \<Longrightarrow> T \<union> S \<turnstile> D
[PROOF STEP]
assume ?r
[PROOF STATE]
proof (state)
this:
S \<turnstile> D

goal (1 subgoal):
 1. S \<turnstile> D \<Longrightarrow> T \<union> S \<turnstile> D
[PROOF STEP]
with Resolution_weaken
[PROOF STATE]
proof (chain)
picking this:
?S \<turnstile> ?D \<Longrightarrow> ?T \<union> ?S \<turnstile> ?D
S \<turnstile> D
[PROOF STEP]
show ?l
[PROOF STATE]
proof (prove)
using this:
?S \<turnstile> ?D \<Longrightarrow> ?T \<union> ?S \<turnstile> ?D
S \<turnstile> D

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Resolution_taint_assumptions: "S \<union> T \<turnstile> C \<Longrightarrow> \<exists>R \<subseteq> D. ((\<union>) D ` S) \<union> T \<turnstile> R \<union> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> T \<turnstile> C \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
(* No, we don't need to show this for an arbitrary clause D, but the proof doesn't get any more readable if you only allow a single atom. *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> T \<turnstile> C \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
proof(induction "S \<union> T" "C" rule: Resolution.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C. C \<in> S \<union> T \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
 2. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
case (Ass C)
[PROOF STATE]
proof (state)
this:
C \<in> S \<union> T

goal (2 subgoals):
 1. \<And>C. C \<in> S \<union> T \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
 2. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
proof(cases "C \<in> S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C \<in> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
 2. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C \<in> S

goal (2 subgoals):
 1. C \<in> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
 2. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
hence "D \<union> C \<in> (\<union>) D ` S \<union> T"
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. D \<union> C \<in> (\<union>) D ` S \<union> T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D \<union> C \<in> (\<union>) D ` S \<union> T

goal (2 subgoals):
 1. C \<in> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
 2. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
with Resolution.Ass
[PROOF STATE]
proof (chain)
picking this:
?C \<in> ?S \<Longrightarrow> ?S \<turnstile> ?C
D \<union> C \<in> (\<union>) D ` S \<union> T
[PROOF STEP]
have "((\<union>) D ` S) \<union> T \<turnstile> D \<union> C"
[PROOF STATE]
proof (prove)
using this:
?C \<in> ?S \<Longrightarrow> ?S \<turnstile> ?C
D \<union> C \<in> (\<union>) D ` S \<union> T

goal (1 subgoal):
 1. (\<union>) D ` S \<union> T \<turnstile> D \<union> C
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<union>) D ` S \<union> T \<turnstile> D \<union> C

goal (2 subgoals):
 1. C \<in> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
 2. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<union>) D ` S \<union> T \<turnstile> D \<union> C

goal (1 subgoal):
 1. \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C

goal (1 subgoal):
 1. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<notin> S

goal (1 subgoal):
 1. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
with Ass
[PROOF STATE]
proof (chain)
picking this:
C \<in> S \<union> T
C \<notin> S
[PROOF STEP]
have "C \<in> T"
[PROOF STATE]
proof (prove)
using this:
C \<in> S \<union> T
C \<notin> S

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

goal (1 subgoal):
 1. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
hence "((\<union>) D ` S) \<union> T \<turnstile> C"
[PROOF STATE]
proof (prove)
using this:
C \<in> T

goal (1 subgoal):
 1. (\<union>) D ` S \<union> T \<turnstile> C
[PROOF STEP]
by(simp add: Resolution.Ass)
[PROOF STATE]
proof (state)
this:
(\<union>) D ` S \<union> T \<turnstile> C

goal (1 subgoal):
 1. C \<notin> S \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<union>) D ` S \<union> T \<turnstile> C

goal (1 subgoal):
 1. \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C
[PROOF STEP]
by(intro exI[where x="{}"]) simp
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
case (R C1 C2 k)
[PROOF STATE]
proof (state)
this:
S \<union> T \<turnstile> C1
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C1
S \<union> T \<turnstile> C2
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C2
k\<^sup>+ \<in> C1
k\<inverse> \<in> C2

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
let ?m = "((\<union>) D ` S) \<union> T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
S \<union> T \<turnstile> C1
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C1
S \<union> T \<turnstile> C2
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C2
k\<^sup>+ \<in> C1
k\<inverse> \<in> C2
[PROOF STEP]
obtain R1 where IH1: "R1 \<subseteq> D" "?m \<turnstile> R1 \<union> C1"
[PROOF STATE]
proof (prove)
using this:
S \<union> T \<turnstile> C1
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C1
S \<union> T \<turnstile> C2
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C2
k\<^sup>+ \<in> C1
k\<inverse> \<in> C2

goal (1 subgoal):
 1. (\<And>R1. \<lbrakk>R1 \<subseteq> D; (\<union>) D ` S \<union> T \<turnstile> R1 \<union> C1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R1 \<subseteq> D
(\<union>) D ` S \<union> T \<turnstile> R1 \<union> C1

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
S \<union> T \<turnstile> C1
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C1
S \<union> T \<turnstile> C2
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C2
k\<^sup>+ \<in> C1
k\<inverse> \<in> C2
[PROOF STEP]
obtain R2 where IH2: "R2 \<subseteq> D" "?m \<turnstile> R2 \<union> C2"
[PROOF STATE]
proof (prove)
using this:
S \<union> T \<turnstile> C1
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C1
S \<union> T \<turnstile> C2
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C2
k\<^sup>+ \<in> C1
k\<inverse> \<in> C2

goal (1 subgoal):
 1. (\<And>R2. \<lbrakk>R2 \<subseteq> D; (\<union>) D ` S \<union> T \<turnstile> R2 \<union> C2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R2 \<subseteq> D
(\<union>) D ` S \<union> T \<turnstile> R2 \<union> C2

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
S \<union> T \<turnstile> C1
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C1
S \<union> T \<turnstile> C2
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C2
k\<^sup>+ \<in> C1
k\<inverse> \<in> C2
[PROOF STEP]
have "k\<^sup>+ \<in> R1 \<union> C1" "k\<inverse> \<in> R2 \<union> C2"
[PROOF STATE]
proof (prove)
using this:
S \<union> T \<turnstile> C1
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C1
S \<union> T \<turnstile> C2
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C2
k\<^sup>+ \<in> C1
k\<inverse> \<in> C2

goal (1 subgoal):
 1. k\<^sup>+ \<in> R1 \<union> C1 &&& k\<inverse> \<in> R2 \<union> C2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
k\<^sup>+ \<in> R1 \<union> C1
k\<inverse> \<in> R2 \<union> C2

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
note Resolution.R[OF IH1(2) IH2(2) this]
[PROOF STATE]
proof (state)
this:
(\<union>) D ` S \<union> T \<turnstile> R1 \<union> C1 - {k\<^sup>+} \<union> (R2 \<union> C2 - {k\<inverse>})

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
hence "?m \<turnstile> (R1 - {k\<^sup>+}) \<union> (R2 - {k\<inverse>}) \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))"
[PROOF STATE]
proof (prove)
using this:
(\<union>) D ` S \<union> T \<turnstile> R1 \<union> C1 - {k\<^sup>+} \<union> (R2 \<union> C2 - {k\<inverse>})

goal (1 subgoal):
 1. (\<union>) D ` S \<union> T \<turnstile> R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))
[PROOF STEP]
by (simp add: Un_Diff Un_left_commute sup.assoc)
[PROOF STATE]
proof (state)
this:
(\<union>) D ` S \<union> T \<turnstile> R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<union>) D ` S \<union> T \<turnstile> R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
have "(R1 - {k\<^sup>+}) \<union> (R2 - {k\<inverse>}) \<subseteq> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<subseteq> D
[PROOF STEP]
(* hah\<triangleright> gotcha. This is the reason that I should be doing this on sets\<triangleright> not multisets. - neh, actually, there are others. how is the rule even supposed to look? *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<subseteq> D
[PROOF STEP]
using IH1(1) IH2(1)
[PROOF STATE]
proof (prove)
using this:
R1 \<subseteq> D
R2 \<subseteq> D

goal (1 subgoal):
 1. R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<subseteq> D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<subseteq> D

goal (1 subgoal):
 1. \<And>C Da k. \<lbrakk>S \<union> T \<turnstile> C; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> C; S \<union> T \<turnstile> Da; \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> Da; k\<^sup>+ \<in> C; k\<inverse> \<in> Da\<rbrakk> \<Longrightarrow> \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C - {k\<^sup>+} \<union> (Da - {k\<inverse>}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<union>) D ` S \<union> T \<turnstile> R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))
R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<subseteq> D
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<union>) D ` S \<union> T \<turnstile> R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))
R1 - {k\<^sup>+} \<union> (R2 - {k\<inverse>}) \<subseteq> D

goal (1 subgoal):
 1. \<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>R\<subseteq>D. (\<union>) D ` S \<union> T \<turnstile> R \<union> (C1 - {k\<^sup>+} \<union> (C2 - {k\<inverse>}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Resolution_useless_infinite:
assumes R: "S \<turnstile> R"
assumes "finite R"
shows "\<exists>S' \<subseteq> S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
S \<turnstile> R
finite R

goal (1 subgoal):
 1. \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> R)
[PROOF STEP]
proof(induction rule: Resolution.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; finite C\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C)
 2. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
case (Ass C S)
[PROOF STATE]
proof (state)
this:
C \<in> S
finite C

goal (2 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; finite C\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C)
 2. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
C \<in> S
finite C

goal (1 subgoal):
 1. \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C)
[PROOF STEP]
using Resolution.Ass
[PROOF STATE]
proof (prove)
using this:
C \<in> S
finite C
?C \<in> ?S \<Longrightarrow> ?S \<turnstile> ?C

goal (1 subgoal):
 1. \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C)
[PROOF STEP]
by(intro exI[where x="{C}"]) auto
[PROOF STATE]
proof (state)
this:
\<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C)

goal (1 subgoal):
 1. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
case (R S C D k)
[PROOF STATE]
proof (state)
this:
S \<turnstile> C
S \<turnstile> D
k\<^sup>+ \<in> C
k\<inverse> \<in> D
finite C \<Longrightarrow> \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C)
finite D \<Longrightarrow> \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> D)
finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))

goal (1 subgoal):
 1. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
from R.prems
[PROOF STATE]
proof (chain)
picking this:
finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
have "finite C" "finite D"
[PROOF STATE]
proof (prove)
using this:
finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))

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

goal (1 subgoal):
 1. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
with R.IH
[PROOF STATE]
proof (chain)
picking this:
finite C \<Longrightarrow> \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C)
finite D \<Longrightarrow> \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> D)
finite C
finite D
[PROOF STEP]
obtain SC SD where IH:
    "SC\<subseteq>S" "(\<forall>C\<in>SC. finite C)" "finite SC" "SC \<turnstile> C"
    "SD\<subseteq>S" "(\<forall>D\<in>SD. finite D)" "finite SD" "SD \<turnstile> D"
[PROOF STATE]
proof (prove)
using this:
finite C \<Longrightarrow> \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C)
finite D \<Longrightarrow> \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> D)
finite C
finite D

goal (1 subgoal):
 1. (\<And>SC SD. \<lbrakk>SC \<subseteq> S; \<forall>C\<in>SC. finite C; finite SC; SC \<turnstile> C; SD \<subseteq> S; \<forall>D\<in>SD. finite D; finite SD; SD \<turnstile> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SC \<subseteq> S
\<forall>C\<in>SC. finite C
finite SC
SC \<turnstile> C
SD \<subseteq> S
\<forall>D\<in>SD. finite D
finite SD
SD \<turnstile> D

goal (1 subgoal):
 1. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
hence IHw: "SC \<union> SD \<turnstile> C" "SC \<union> SD \<turnstile> D"
[PROOF STATE]
proof (prove)
using this:
SC \<subseteq> S
\<forall>C\<in>SC. finite C
finite SC
SC \<turnstile> C
SD \<subseteq> S
\<forall>D\<in>SD. finite D
finite SD
SD \<turnstile> D

goal (1 subgoal):
 1. SC \<union> SD \<turnstile> C &&& SC \<union> SD \<turnstile> D
[PROOF STEP]
using Resolution_weaken
[PROOF STATE]
proof (prove)
using this:
SC \<subseteq> S
\<forall>C\<in>SC. finite C
finite SC
SC \<turnstile> C
SD \<subseteq> S
\<forall>D\<in>SD. finite D
finite SD
SD \<turnstile> D
?S \<turnstile> ?D \<Longrightarrow> ?T \<union> ?S \<turnstile> ?D

goal (1 subgoal):
 1. SC \<union> SD \<turnstile> C &&& SC \<union> SD \<turnstile> D
[PROOF STEP]
by(simp_all add: sup_commute Resolution_weaken (* yes, using and simp set. whatever. *))
[PROOF STATE]
proof (state)
this:
SC \<union> SD \<turnstile> C
SC \<union> SD \<turnstile> D

goal (1 subgoal):
 1. \<And>S C D k. \<lbrakk>S \<turnstile> C; finite C \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C); S \<turnstile> D; finite D \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> D); k\<^sup>+ \<in> C; k\<inverse> \<in> D; finite (C - {k\<^sup>+} \<union> (D - {k\<inverse>}))\<rbrakk> \<Longrightarrow> \<exists>S'\<subseteq>S. Ball S' finite \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
with IH(1-3,5-7)
[PROOF STATE]
proof (chain)
picking this:
SC \<subseteq> S
\<forall>C\<in>SC. finite C
finite SC
SD \<subseteq> S
\<forall>D\<in>SD. finite D
finite SD
SC \<union> SD \<turnstile> C
SC \<union> SD \<turnstile> D
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
SC \<subseteq> S
\<forall>C\<in>SC. finite C
finite SC
SD \<subseteq> S
\<forall>D\<in>SD. finite D
finite SD
SC \<union> SD \<turnstile> C
SC \<union> SD \<turnstile> D

goal (1 subgoal):
 1. \<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))
[PROOF STEP]
by(blast intro!: exI[where x="SC \<union> SD"] Resolution.R[OF _ _ \<open>k\<^sup>+ \<in> C\<close> \<open>k\<inverse> \<in> D\<close>])
[PROOF STATE]
proof (state)
this:
\<exists>S'\<subseteq>S. (\<forall>a\<in>S'. finite a) \<and> finite S' \<and> (S' \<turnstile> C - {k\<^sup>+} \<union> (D - {k\<inverse>}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "\<box> \<in> the (Rwhile ex1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box> \<in> the (Rwhile ex1)
[PROOF STEP]
by eval


[STATEMENT]
lemma Rwhile_sound: assumes "Rwhile S = Some S'"
  shows "\<forall>C \<in> S'. Resolution S C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
apply(rule while_option_rule[OF _ assms[unfolded Rwhile_def]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>C\<in>s. S \<turnstile> C; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> \<forall>C\<in>res s \<union> s. S \<turnstile> C
 2. \<forall>C\<in>S. S \<turnstile> C
[PROOF STEP]
apply (auto simp: Ass R res_def split: if_splits literal.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done