[STATEMENT]
lemma tainting_iff_blp_extended:
  defines "extract \<equiv> \<lambda>A ts. card (A \<inter> ts)"
  assumes finite: "\<forall>ts v. nP v = ts \<longrightarrow> finite ts"
  shows "SINVAR_Tainting.sinvar G nP \<longleftrightarrow> (\<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP = (\<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)
 2. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
show "SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)
[PROOF STEP]
apply(simp add: extract_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>A. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> card (A \<inter> nP e1) \<le> card (A \<inter> nP e2)
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>SINVAR_Tainting.sinvar G nP; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> card (A \<inter> nP a) \<le> card (A \<inter> nP b)
[PROOF STEP]
apply(simp add: SINVAR_Tainting.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> card (A \<inter> nP a) \<le> card (A \<inter> nP b)
[PROOF STEP]
apply(rename_tac A a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> card (A \<inter> nP a) \<le> card (A \<inter> nP b)
[PROOF STEP]
apply(subgoal_tac "finite (A \<inter> nP a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (A \<inter> nP a)\<rbrakk> \<Longrightarrow> card (A \<inter> nP a) \<le> card (A \<inter> nP b)
 2. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> finite (A \<inter> nP a)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> finite (A \<inter> nP a)
 2. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (A \<inter> nP a)\<rbrakk> \<Longrightarrow> card (A \<inter> nP a) \<le> card (A \<inter> nP b)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a_, b_) \<in> edges G\<rbrakk> \<Longrightarrow> finite (A_ \<inter> nP a_)
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
\<forall>ts v. nP v = ts \<longrightarrow> finite ts

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a_, b_) \<in> edges G\<rbrakk> \<Longrightarrow> finite (A_ \<inter> nP a_)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (A \<inter> nP a)\<rbrakk> \<Longrightarrow> card (A \<inter> nP a) \<le> card (A \<inter> nP b)
[PROOF STEP]
apply(rule card_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (A \<inter> nP a)\<rbrakk> \<Longrightarrow> finite (A \<inter> nP b)
 2. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (A \<inter> nP a)\<rbrakk> \<Longrightarrow> A \<inter> nP a \<subseteq> A \<inter> nP b
[PROOF STEP]
apply(simp add: finite; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (A \<inter> nP a)\<rbrakk> \<Longrightarrow> A \<inter> nP a \<subseteq> A \<inter> nP b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
assume blp: "\<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)"
[PROOF STATE]
proof (state)
this:
\<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
fix v1 v2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
assume *: "(v1,v2)\<in>edges G"
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
from blp *
[PROOF STATE]
proof (chain)
picking this:
\<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)
(v1, v2) \<in> edges G
[PROOF STEP]
have "card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP)
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)
[PROOF STEP]
unfolding extract_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A. SINVAR_BLPbasic.sinvar G ((\<lambda>ts. card (A \<inter> ts)) \<circ> nP)
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>A. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> card (A \<inter> nP e1) \<le> card (A \<inter> nP e2); (v1, v2) \<in> edges G\<rbrakk> \<Longrightarrow> card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)
[PROOF STEP]
apply(erule_tac x=A in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v1, v2) \<in> edges G; \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> card (A \<inter> nP e1) \<le> card (A \<inter> nP e2)\<rbrakk> \<Longrightarrow> card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)
[PROOF STEP]
apply(erule_tac x="(v1, v2)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(v1, v2) \<in> edges G; case (v1, v2) of (e1, e2) \<Rightarrow> card (A \<inter> nP e1) \<le> card (A \<inter> nP e2)\<rbrakk> \<Longrightarrow> card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)
 2. \<lbrakk>(v1, v2) \<in> edges G; (v1, v2) \<notin> edges G\<rbrakk> \<Longrightarrow> card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
card (A \<inter> nP v1) \<le> card (A \<inter> nP v2)

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
card (?A2 \<inter> nP v1) \<le> card (?A2 \<inter> nP v2)

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
from this finite card_seteq
[PROOF STATE]
proof (chain)
picking this:
card (?A2 \<inter> nP v1) \<le> card (?A2 \<inter> nP v2)
\<forall>ts v. nP v = ts \<longrightarrow> finite ts
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?B \<le> card ?A\<rbrakk> \<Longrightarrow> ?A = ?B
[PROOF STEP]
have "nP v1 \<subseteq> nP v2"
[PROOF STATE]
proof (prove)
using this:
card (?A2 \<inter> nP v1) \<le> card (?A2 \<inter> nP v2)
\<forall>ts v. nP v = ts \<longrightarrow> finite ts
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?B \<le> card ?A\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. nP v1 \<subseteq> nP v2
[PROOF STEP]
by (metis Int_absorb Int_lower1 inf.orderI)
[PROOF STATE]
proof (state)
this:
nP v1 \<subseteq> nP v2

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?v1.2, ?v2.2) \<in> edges G \<Longrightarrow> nP ?v1.2 \<subseteq> nP ?v2.2

goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPbasic.sinvar G (extract A \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
thus "SINVAR_Tainting.sinvar G nP"
[PROOF STATE]
proof (prove)
using this:
(?v1.2, ?v2.2) \<in> edges G \<Longrightarrow> nP ?v1.2 \<subseteq> nP ?v2.2

goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP
[PROOF STEP]
unfolding SINVAR_Tainting.sinvar_def
[PROOF STATE]
proof (prove)
using this:
(?v1.2, ?v2.2) \<in> edges G \<Longrightarrow> nP ?v1.2 \<subseteq> nP ?v2.2

goal (1 subgoal):
 1. \<forall>(v1, v2)\<in>edges G. nP v1 \<subseteq> nP v2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SINVAR_Tainting.sinvar G nP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "\<forall>ts v. nP v = ts \<longrightarrow> finite (taints ts) \<Longrightarrow>
  SINVAR_TaintingTrusted.sinvar G nP \<Longrightarrow>
    SINVAR_BLPtrusted.sinvar G ((\<lambda> ts. \<lparr>security_level = card (taints ts - untaints ts), trusted = (untaints ts \<noteq> {})\<rparr> ) \<circ> nP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts v. nP v = ts \<longrightarrow> finite (taints ts); SINVAR_TaintingTrusted.sinvar G nP\<rbrakk> \<Longrightarrow> SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = card (taints ts - untaints ts), trusted = untaints ts \<noteq> {}\<rparr>) \<circ> nP)
[PROOF STEP]
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> untaints (nP e2) = {} \<longrightarrow> card (taints (nP e1) - untaints (nP e1)) \<le> card (taints (nP e2))
[PROOF STEP]
apply(clarify, rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); \<forall>(v1, v2)\<in>edges G. taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2); (a, b) \<in> edges G; untaints (nP b) = {}\<rbrakk> \<Longrightarrow> card (taints (nP a) - untaints (nP a)) \<le> card (taints (nP b))
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; case (a, b) of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2)\<rbrakk> \<Longrightarrow> card (taints (nP a) - untaints (nP a)) \<le> card (taints (nP b))
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> card (taints (nP a) - untaints (nP a)) \<le> card (taints (nP b))
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> card (taints (nP a) - untaints (nP a)) \<le> card (taints (nP b))
[PROOF STEP]
apply(subgoal_tac "finite (taints (nP a) - untaints (nP a))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b); finite (taints (nP a) - untaints (nP a))\<rbrakk> \<Longrightarrow> card (taints (nP a) - untaints (nP a)) \<le> card (taints (nP b))
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> finite (taints (nP a) - untaints (nP a))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> finite (taints (nP a) - untaints (nP a))
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b); finite (taints (nP a) - untaints (nP a))\<rbrakk> \<Longrightarrow> card (taints (nP a) - untaints (nP a)) \<le> card (taints (nP b))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a_, b_) \<in> edges G; untaints (nP b_) = {}; taints (nP a_) - untaints (nP a_) \<subseteq> taints (nP b_)\<rbrakk> \<Longrightarrow> finite (taints (nP a_) - untaints (nP a_))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b); finite (taints (nP a) - untaints (nP a))\<rbrakk> \<Longrightarrow> card (taints (nP a) - untaints (nP a)) \<le> card (taints (nP b))
[PROOF STEP]
apply(rule card_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b); finite (taints (nP a) - untaints (nP a))\<rbrakk> \<Longrightarrow> finite (taints (nP b))
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite (taints ts); (a, b) \<in> edges G; untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b); finite (taints (nP a) - untaints (nP a))\<rbrakk> \<Longrightarrow> taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)
[PROOF STEP]
by blast+


[STATEMENT]
lemma tainting_iff_blp_trusted:
  defines "project \<equiv> \<lambda>a ts. \<lparr>
      security_level =
        if
          a \<in> (taints ts - untaints ts)
        then
          1::security_level
        else
          0::security_level
      , trusted = a \<in> untaints ts\<rparr>"
  shows "SINVAR_TaintingTrusted.sinvar G nP \<longleftrightarrow> (\<forall>a. SINVAR_BLPtrusted.sinvar G (project a \<circ> nP))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_TaintingTrusted.sinvar G nP = (\<forall>a. SINVAR_BLPtrusted.sinvar G (project a \<circ> nP))
[PROOF STEP]
unfolding project_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_TaintingTrusted.sinvar G nP = (\<forall>a. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts - untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP))
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. SINVAR_TaintingTrusted.sinvar G nP \<Longrightarrow> \<forall>a. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts - untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP)
 2. \<forall>a. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts - untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) \<Longrightarrow> SINVAR_TaintingTrusted.sinvar G nP
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_TaintingTrusted.sinvar G nP \<Longrightarrow> \<forall>a. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts - untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP)
[PROOF STEP]
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2) \<Longrightarrow> \<forall>a. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> (a \<in> taints (nP e2) \<longrightarrow> a \<notin> untaints (nP e2) \<longrightarrow> (if a \<in> taints (nP e1) \<and> a \<notin> untaints (nP e1) then 1 else 0) \<le> Suc 0) \<and> (a \<notin> taints (nP e2) \<longrightarrow> a \<notin> untaints (nP e2) \<longrightarrow> (if a \<in> taints (nP e1) \<and> a \<notin> untaints (nP e1) then 1 else 0) = 0)
[PROOF STEP]
apply(clarify, rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa a b. \<lbrakk>\<forall>(v1, v2)\<in>edges G. taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2); (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> (aa \<in> taints (nP b) \<longrightarrow> aa \<notin> untaints (nP b) \<longrightarrow> (if aa \<in> taints (nP a) \<and> aa \<notin> untaints (nP a) then 1 else 0) \<le> Suc 0) \<and> (aa \<notin> taints (nP b) \<longrightarrow> aa \<notin> untaints (nP b) \<longrightarrow> (if aa \<in> taints (nP a) \<and> aa \<notin> untaints (nP a) then 1 else 0) = 0)
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa a b. \<lbrakk>(a, b) \<in> edges G; case (a, b) of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2)\<rbrakk> \<Longrightarrow> (aa \<in> taints (nP b) \<longrightarrow> aa \<notin> untaints (nP b) \<longrightarrow> (if aa \<in> taints (nP a) \<and> aa \<notin> untaints (nP a) then 1 else 0) \<le> Suc 0) \<and> (aa \<notin> taints (nP b) \<longrightarrow> aa \<notin> untaints (nP b) \<longrightarrow> (if aa \<in> taints (nP a) \<and> aa \<notin> untaints (nP a) then 1 else 0) = 0)
 2. \<And>aa a b. \<lbrakk>(a, b) \<in> edges G; (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> (aa \<in> taints (nP b) \<longrightarrow> aa \<notin> untaints (nP b) \<longrightarrow> (if aa \<in> taints (nP a) \<and> aa \<notin> untaints (nP a) then 1 else 0) \<le> Suc 0) \<and> (aa \<notin> taints (nP b) \<longrightarrow> aa \<notin> untaints (nP b) \<longrightarrow> (if aa \<in> taints (nP a) \<and> aa \<notin> untaints (nP a) then 1 else 0) = 0)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa a b. \<lbrakk>(a, b) \<in> edges G; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> aa \<in> taints (nP a) \<and> aa \<notin> untaints (nP a) \<longrightarrow> aa \<notin> taints (nP b) \<longrightarrow> aa \<in> untaints (nP b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts - untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) \<Longrightarrow> SINVAR_TaintingTrusted.sinvar G nP
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> if a \<in> untaints (nP e2) then True else security_level (((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts \<and> a \<notin> untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts \<and> a \<notin> untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) e2) \<Longrightarrow> SINVAR_TaintingTrusted.sinvar G nP
[PROOF STEP]
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> if a \<in> untaints (nP e2) then True else security_level (((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts \<and> a \<notin> untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts \<and> a \<notin> untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) e2) \<Longrightarrow> \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2)
[PROOF STEP]
apply(clarify, rename_tac a b taintlabel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>\<forall>a. \<forall>(e1, e2)\<in>edges G. if a \<in> untaints (nP e2) then True else security_level (((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts \<and> a \<notin> untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = if a \<in> taints ts \<and> a \<notin> untaints ts then 1 else 0, trusted = a \<in> untaints ts\<rparr>) \<circ> nP) e2); (a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(erule_tac x=taintlabel in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); \<forall>(e1, e2)\<in>edges G. if taintlabel \<in> untaints (nP e2) then True else security_level (((\<lambda>ts. \<lparr>security_level = if taintlabel \<in> taints ts \<and> taintlabel \<notin> untaints ts then 1 else 0, trusted = taintlabel \<in> untaints ts\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = if taintlabel \<in> taints ts \<and> taintlabel \<notin> untaints ts then 1 else 0, trusted = taintlabel \<in> untaints ts\<rparr>) \<circ> nP) e2)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); case (a, b) of (e1, e2) \<Rightarrow> if taintlabel \<in> untaints (nP e2) then True else security_level (((\<lambda>ts. \<lparr>security_level = if taintlabel \<in> taints ts \<and> taintlabel \<notin> untaints ts then 1 else 0, trusted = taintlabel \<in> untaints ts\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = if taintlabel \<in> taints ts \<and> taintlabel \<notin> untaints ts then 1 else 0, trusted = taintlabel \<in> untaints ts\<rparr>) \<circ> nP) e2)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
 2. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); if taintlabel \<in> untaints (nP b) then True else security_level (((\<lambda>ts. \<lparr>security_level = if taintlabel \<in> taints ts \<and> taintlabel \<notin> untaints ts then 1 else 0, trusted = taintlabel \<in> untaints ts\<rparr>) \<circ> nP) a) \<le> security_level (((\<lambda>ts. \<lparr>security_level = if taintlabel \<in> taints ts \<and> taintlabel \<notin> untaints ts then 1 else 0, trusted = taintlabel \<in> untaints ts\<rparr>) \<circ> nP) b)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(simp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<in> untaints (nP b)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
using taints_wellformedness
[PROOF STATE]
proof (prove)
using this:
untaints ?ts \<subseteq> taints ?ts

goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<in> untaints (nP b)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
by blast


[STATEMENT]
lemma tainting_iff_blp_trusted_extended:
  defines "project \<equiv> \<lambda>A ts.
      \<lparr>
          security_level = card (A \<inter> (taints ts - untaints ts))
        , trusted = (A \<inter> untaints ts) \<noteq> {}
      \<rparr>"
  assumes finite: "\<forall>ts v. nP v = ts \<longrightarrow> finite (taints ts)"
  shows "SINVAR_TaintingTrusted.sinvar G nP \<longleftrightarrow> (\<forall>A. SINVAR_BLPtrusted.sinvar G (project A \<circ> nP))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_TaintingTrusted.sinvar G nP = (\<forall>A. SINVAR_BLPtrusted.sinvar G (project A \<circ> nP))
[PROOF STEP]
unfolding project_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_TaintingTrusted.sinvar G nP = (\<forall>A. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP))
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. SINVAR_TaintingTrusted.sinvar G nP \<Longrightarrow> \<forall>A. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP)
 2. \<forall>A. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) \<Longrightarrow> SINVAR_TaintingTrusted.sinvar G nP
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_TaintingTrusted.sinvar G nP \<Longrightarrow> \<forall>A. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP)
[PROOF STEP]
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2) \<Longrightarrow> \<forall>A. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> A \<inter> untaints (nP e2) = {} \<longrightarrow> card (A \<inter> (taints (nP e1) - untaints (nP e1))) \<le> card (A \<inter> (taints (nP e2) - untaints (nP e2)))
[PROOF STEP]
apply(clarify, rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>\<forall>(v1, v2)\<in>edges G. taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2); (a, b) \<in> edges G; A \<inter> untaints (nP b) = {}\<rbrakk> \<Longrightarrow> card (A \<inter> (taints (nP a) - untaints (nP a))) \<le> card (A \<inter> (taints (nP b) - untaints (nP b)))
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; case (a, b) of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2)\<rbrakk> \<Longrightarrow> card (A \<inter> (taints (nP a) - untaints (nP a))) \<le> card (A \<inter> (taints (nP b) - untaints (nP b)))
 2. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> card (A \<inter> (taints (nP a) - untaints (nP a))) \<le> card (A \<inter> (taints (nP b) - untaints (nP b)))
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> card (A \<inter> (taints (nP a) - untaints (nP a))) \<le> card (A \<inter> (taints (nP b) - untaints (nP b)))
[PROOF STEP]
apply(rule card_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> finite (A \<inter> (taints (nP b) - untaints (nP b)))
 2. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> A \<inter> (taints (nP a) - untaints (nP a)) \<subseteq> A \<inter> (taints (nP b) - untaints (nP b))
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
\<forall>ts v. nP v = ts \<longrightarrow> finite (taints ts)

goal (2 subgoals):
 1. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> finite (A \<inter> (taints (nP b) - untaints (nP b)))
 2. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> A \<inter> (taints (nP a) - untaints (nP a)) \<subseteq> A \<inter> (taints (nP b) - untaints (nP b))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A a b. \<lbrakk>(a, b) \<in> edges G; A \<inter> untaints (nP b) = {}; taints (nP a) - untaints (nP a) \<subseteq> taints (nP b)\<rbrakk> \<Longrightarrow> A \<inter> (taints (nP a) - untaints (nP a)) \<subseteq> A \<inter> (taints (nP b) - untaints (nP b))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. SINVAR_BLPtrusted.sinvar G ((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) \<Longrightarrow> SINVAR_TaintingTrusted.sinvar G nP
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> if A \<inter> untaints (nP e2) \<noteq> {} then True else security_level (((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e2) \<Longrightarrow> SINVAR_TaintingTrusted.sinvar G nP
[PROOF STEP]
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> if A \<inter> untaints (nP e2) \<noteq> {} then True else security_level (((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e2) \<Longrightarrow> \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> taints (nP v1) - untaints (nP v1) \<subseteq> taints (nP v2)
[PROOF STEP]
apply(clarify, rename_tac a b taintlabel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>\<forall>A. \<forall>(e1, e2)\<in>edges G. if A \<inter> untaints (nP e2) \<noteq> {} then True else security_level (((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = card (A \<inter> (taints ts - untaints ts)), trusted = A \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e2); (a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(erule_tac x="{taintlabel}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); \<forall>(e1, e2)\<in>edges G. if {taintlabel} \<inter> untaints (nP e2) \<noteq> {} then True else security_level (((\<lambda>ts. \<lparr>security_level = card ({taintlabel} \<inter> (taints ts - untaints ts)), trusted = {taintlabel} \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = card ({taintlabel} \<inter> (taints ts - untaints ts)), trusted = {taintlabel} \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e2)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); case (a, b) of (e1, e2) \<Rightarrow> if {taintlabel} \<inter> untaints (nP e2) \<noteq> {} then True else security_level (((\<lambda>ts. \<lparr>security_level = card ({taintlabel} \<inter> (taints ts - untaints ts)), trusted = {taintlabel} \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e1) \<le> security_level (((\<lambda>ts. \<lparr>security_level = card ({taintlabel} \<inter> (taints ts - untaints ts)), trusted = {taintlabel} \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) e2)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
 2. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); if taintlabel \<in> untaints (nP b) then True else security_level (((\<lambda>ts. \<lparr>security_level = card ({taintlabel} \<inter> (taints ts - untaints ts)), trusted = {taintlabel} \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) a) \<le> security_level (((\<lambda>ts. \<lparr>security_level = card ({taintlabel} \<inter> (taints ts - untaints ts)), trusted = {taintlabel} \<inter> untaints ts \<noteq> {}\<rparr>) \<circ> nP) b)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply(simp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<in> untaints (nP b)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
 2. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<notin> untaints (nP b); Suc 0 \<le> card ({taintlabel} \<inter> (taints (nP b) - untaints (nP b)))\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
using taints_wellformedness
[PROOF STATE]
proof (prove)
using this:
untaints ?ts \<subseteq> taints ?ts

goal (2 subgoals):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<in> untaints (nP b)\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
 2. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<notin> untaints (nP b); Suc 0 \<le> card ({taintlabel} \<inter> (taints (nP b) - untaints (nP b)))\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<notin> untaints (nP b); Suc 0 \<le> card ({taintlabel} \<inter> (taints (nP b) - untaints (nP b)))\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
using Diff_insert_absorb
[PROOF STATE]
proof (prove)
using this:
?x \<notin> ?A \<Longrightarrow> insert ?x ?A - {?x} = ?A

goal (1 subgoal):
 1. \<And>a b taintlabel. \<lbrakk>(a, b) \<in> edges G; taintlabel \<in> taints (nP a); taintlabel \<notin> untaints (nP a); taintlabel \<notin> untaints (nP b); Suc 0 \<le> card ({taintlabel} \<inter> (taints (nP b) - untaints (nP b)))\<rbrakk> \<Longrightarrow> taintlabel \<in> taints (nP b)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma coprime_iff_prime_factors_disjoint:
  fixes x y :: "'a :: factorial_semiring"
  assumes "x \<noteq> 0" "y \<noteq> 0"
  shows "coprime x y \<longleftrightarrow> prime_factors x \<inter> prime_factors y = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime x y = (prime_factors x \<inter> prime_factors y = {})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. coprime x y \<Longrightarrow> prime_factors x \<inter> prime_factors y = {}
 2. prime_factors x \<inter> prime_factors y = {} \<Longrightarrow> coprime x y
[PROOF STEP]
assume "coprime x y"
[PROOF STATE]
proof (state)
this:
coprime x y

goal (2 subgoals):
 1. coprime x y \<Longrightarrow> prime_factors x \<inter> prime_factors y = {}
 2. prime_factors x \<inter> prime_factors y = {} \<Longrightarrow> coprime x y
[PROOF STEP]
have False if "p \<in> prime_factors x" "p \<in> prime_factors y" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from that assms
[PROOF STATE]
proof (chain)
picking this:
p \<in># prime_factorization x
p \<in># prime_factorization y
x \<noteq> (0::'a)
y \<noteq> (0::'a)
[PROOF STEP]
have "p dvd x" "p dvd y"
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization x
p \<in># prime_factorization y
x \<noteq> (0::'a)
y \<noteq> (0::'a)

goal (1 subgoal):
 1. p dvd x &&& p dvd y
[PROOF STEP]
by (auto simp: prime_factors_dvd)
[PROOF STATE]
proof (state)
this:
p dvd x
p dvd y

goal (1 subgoal):
 1. False
[PROOF STEP]
with \<open>coprime x y\<close>
[PROOF STATE]
proof (chain)
picking this:
coprime x y
p dvd x
p dvd y
[PROOF STEP]
have "p dvd 1"
[PROOF STATE]
proof (prove)
using this:
coprime x y
p dvd x
p dvd y

goal (1 subgoal):
 1. is_unit p
[PROOF STEP]
using coprime_common_divisor
[PROOF STATE]
proof (prove)
using this:
coprime x y
p dvd x
p dvd y
\<lbrakk>coprime ?a ?b; ?c dvd ?a; ?c dvd ?b\<rbrakk> \<Longrightarrow> is_unit ?c

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

goal (1 subgoal):
 1. False
[PROOF STEP]
with that assms
[PROOF STATE]
proof (chain)
picking this:
p \<in># prime_factorization x
p \<in># prime_factorization y
x \<noteq> (0::'a)
y \<noteq> (0::'a)
is_unit p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p \<in># prime_factorization x
p \<in># prime_factorization y
x \<noteq> (0::'a)
y \<noteq> (0::'a)
is_unit p

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p \<in># prime_factorization x; ?p \<in># prime_factorization y\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. coprime x y \<Longrightarrow> prime_factors x \<inter> prime_factors y = {}
 2. prime_factors x \<inter> prime_factors y = {} \<Longrightarrow> coprime x y
[PROOF STEP]
thus "prime_factors x \<inter> prime_factors y = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<in># prime_factorization x; ?p \<in># prime_factorization y\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. prime_factors x \<inter> prime_factors y = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime_factors x \<inter> prime_factors y = {}

goal (1 subgoal):
 1. prime_factors x \<inter> prime_factors y = {} \<Longrightarrow> coprime x y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_factors x \<inter> prime_factors y = {} \<Longrightarrow> coprime x y
[PROOF STEP]
assume disjoint: "prime_factors x \<inter> prime_factors y = {}"
[PROOF STATE]
proof (state)
this:
prime_factors x \<inter> prime_factors y = {}

goal (1 subgoal):
 1. prime_factors x \<inter> prime_factors y = {} \<Longrightarrow> coprime x y
[PROOF STEP]
show "coprime x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime x y
[PROOF STEP]
proof (rule coprimeI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd x; c dvd y\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd x; c dvd y\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
assume d: "d dvd x" "d dvd y"
[PROOF STATE]
proof (state)
this:
d dvd x
d dvd y

goal (1 subgoal):
 1. \<And>c. \<lbrakk>c dvd x; c dvd y\<rbrakk> \<Longrightarrow> is_unit c
[PROOF STEP]
show "is_unit d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_unit d
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
assume "\<not>is_unit d"
[PROOF STATE]
proof (state)
this:
\<not> is_unit d

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> is_unit d

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
from this and d assms
[PROOF STATE]
proof (chain)
picking this:
\<not> is_unit d
d dvd x
d dvd y
x \<noteq> (0::'a)
y \<noteq> (0::'a)
[PROOF STEP]
have "d \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> is_unit d
d dvd x
d dvd y
x \<noteq> (0::'a)
y \<noteq> (0::'a)

goal (1 subgoal):
 1. d \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<noteq> (0::'a)

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> is_unit d
d \<noteq> (0::'a)
[PROOF STEP]
obtain p where p: "prime p" "p dvd d"
[PROOF STATE]
proof (prove)
using this:
\<not> is_unit d
d \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_divisor_exists
[PROOF STATE]
proof (prove)
using this:
\<not> is_unit d
d \<noteq> (0::'a)
\<lbrakk>?a \<noteq> (0::?'a); \<not> is_unit ?a\<rbrakk> \<Longrightarrow> \<exists>b. b dvd ?a \<and> prime b

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p
p dvd d

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
with d and assms
[PROOF STATE]
proof (chain)
picking this:
d dvd x
d dvd y
x \<noteq> (0::'a)
y \<noteq> (0::'a)
prime p
p dvd d
[PROOF STEP]
have "p \<in> prime_factors x \<inter> prime_factors y"
[PROOF STATE]
proof (prove)
using this:
d dvd x
d dvd y
x \<noteq> (0::'a)
y \<noteq> (0::'a)
prime p
p dvd d

goal (1 subgoal):
 1. p \<in> prime_factors x \<inter> prime_factors y
[PROOF STEP]
by (auto simp: prime_factors_dvd)
[PROOF STATE]
proof (state)
this:
p \<in> prime_factors x \<inter> prime_factors y

goal (1 subgoal):
 1. \<not> is_unit d \<Longrightarrow> False
[PROOF STEP]
with disjoint
[PROOF STATE]
proof (chain)
picking this:
prime_factors x \<inter> prime_factors y = {}
p \<in> prime_factors x \<inter> prime_factors y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
prime_factors x \<inter> prime_factors y = {}
p \<in> prime_factors x \<inter> prime_factors y

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_dvd_irreducibleD:
  fixes a b x :: "'a :: algebraic_semidom"
  assumes "irreducible x"
  assumes "a * b dvd x"
  shows "a dvd 1 \<or> b dvd 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
irreducible x
a * b dvd x
[PROOF STEP]
obtain c where "x = a * b * c"
[PROOF STATE]
proof (prove)
using this:
irreducible x
a * b dvd x

goal (1 subgoal):
 1. (\<And>c. x = a * b * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = a * b * c

goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
hence "x = a * (b * c)"
[PROOF STATE]
proof (prove)
using this:
x = a * b * c

goal (1 subgoal):
 1. x = a * (b * c)
[PROOF STEP]
by (simp add: mult_ac)
[PROOF STATE]
proof (state)
this:
x = a * (b * c)

goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
from irreducibleD[OF assms(1) this]
[PROOF STATE]
proof (chain)
picking this:
is_unit a \<or> is_unit (b * c)
[PROOF STEP]
show "a dvd 1 \<or> b dvd 1"
[PROOF STATE]
proof (prove)
using this:
is_unit a \<or> is_unit (b * c)

goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
by (auto simp: is_unit_mult_iff)
[PROOF STATE]
proof (state)
this:
is_unit a \<or> is_unit b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_elem_mult_dvdI:
  assumes "prime_elem p" "p dvd c" "b dvd c" "\<not>p dvd b"
  shows   "p * b dvd c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * b dvd c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p * b dvd c
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
b dvd c
[PROOF STEP]
obtain a where c: "c = a * b"
[PROOF STATE]
proof (prove)
using this:
b dvd c

goal (1 subgoal):
 1. (\<And>a. c = a * b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mult.commute
[PROOF STATE]
proof (prove)
using this:
b dvd c
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. (\<And>a. c = a * b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c = a * b

goal (1 subgoal):
 1. p * b dvd c
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
p dvd c
c = a * b
[PROOF STEP]
have "p dvd a * b"
[PROOF STATE]
proof (prove)
using this:
p dvd c
c = a * b

goal (1 subgoal):
 1. p dvd a * b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p dvd a * b

goal (1 subgoal):
 1. p * b dvd c
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
prime_elem p
p dvd c
b dvd c
\<not> p dvd b
p dvd a * b
[PROOF STEP]
have "p dvd a"
[PROOF STATE]
proof (prove)
using this:
prime_elem p
p dvd c
b dvd c
\<not> p dvd b
p dvd a * b

goal (1 subgoal):
 1. p dvd a
[PROOF STEP]
by (subst (asm) prime_elem_dvd_mult_iff) auto
[PROOF STATE]
proof (state)
this:
p dvd a

goal (1 subgoal):
 1. p * b dvd c
[PROOF STEP]
with c
[PROOF STATE]
proof (chain)
picking this:
c = a * b
p dvd a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = a * b
p dvd a

goal (1 subgoal):
 1. p * b dvd c
[PROOF STEP]
by (auto intro: mult_dvd_mono)
[PROOF STATE]
proof (state)
this:
p * b dvd c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_elem_power_mult_dvdI:
  fixes p :: "'a :: algebraic_semidom"
  assumes "prime_elem p" "p ^ n dvd c" "b dvd c" "\<not>p dvd b"
  shows   "p ^ n * b dvd c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ^ n * b dvd c
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> p ^ n * b dvd c
 2. n \<noteq> 0 \<Longrightarrow> p ^ n * b dvd c
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> p ^ n * b dvd c
 2. n \<noteq> 0 \<Longrightarrow> p ^ n * b dvd c
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
b dvd c
[PROOF STEP]
obtain a where c: "c = a * b"
[PROOF STATE]
proof (prove)
using this:
b dvd c

goal (1 subgoal):
 1. (\<And>a. c = a * b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mult.commute
[PROOF STATE]
proof (prove)
using this:
b dvd c
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. (\<And>a. c = a * b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c = a * b

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> p ^ n * b dvd c
 2. n \<noteq> 0 \<Longrightarrow> p ^ n * b dvd c
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
p ^ n dvd c
c = a * b
[PROOF STEP]
have "p ^ n dvd b * a"
[PROOF STATE]
proof (prove)
using this:
p ^ n dvd c
c = a * b

goal (1 subgoal):
 1. p ^ n dvd b * a
[PROOF STEP]
by (simp add: mult_ac)
[PROOF STATE]
proof (state)
this:
p ^ n dvd b * a

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> p ^ n * b dvd c
 2. n \<noteq> 0 \<Longrightarrow> p ^ n * b dvd c
[PROOF STEP]
hence "p ^ n dvd a"
[PROOF STATE]
proof (prove)
using this:
p ^ n dvd b * a

goal (1 subgoal):
 1. p ^ n dvd a
[PROOF STEP]
by (rule prime_power_dvd_multD[OF assms(1)]) (use assms False in auto)
[PROOF STATE]
proof (state)
this:
p ^ n dvd a

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> p ^ n * b dvd c
 2. n \<noteq> 0 \<Longrightarrow> p ^ n * b dvd c
[PROOF STEP]
with c
[PROOF STATE]
proof (chain)
picking this:
c = a * b
p ^ n dvd a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = a * b
p ^ n dvd a

goal (1 subgoal):
 1. p ^ n * b dvd c
[PROOF STEP]
by (auto intro: mult_dvd_mono)
[PROOF STATE]
proof (state)
this:
p ^ n * b dvd c

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> p ^ n * b dvd c
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma prime_mod_4_cases:
  fixes p :: nat
  assumes "prime p"
  shows   "p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
proof (cases "p = 2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> 2

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
with prime_gt_1_nat[of p] assms
[PROOF STATE]
proof (chain)
picking this:
prime p \<Longrightarrow> 1 < p
prime p
p \<noteq> 2
[PROOF STEP]
have "p > 2"
[PROOF STATE]
proof (prove)
using this:
prime p \<Longrightarrow> 1 < p
prime p
p \<noteq> 2

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

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
have "\<not>4 dvd p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 4 dvd p
[PROOF STEP]
using assms product_dvd_irreducibleD[of p 2 2]
[PROOF STATE]
proof (prove)
using this:
prime p
\<lbrakk>irreducible p; 2 * 2 dvd p\<rbrakk> \<Longrightarrow> is_unit 2 \<or> is_unit 2

goal (1 subgoal):
 1. \<not> 4 dvd p
[PROOF STEP]
by (auto simp: prime_elem_iff_irreducible simp flip: prime_elem_nat_iff)
[PROOF STATE]
proof (state)
this:
\<not> 4 dvd p

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
hence "p mod 4 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 4 dvd p

goal (1 subgoal):
 1. p mod 4 \<noteq> 0
[PROOF STEP]
by (auto simp: mod_eq_0_iff_dvd)
[PROOF STATE]
proof (state)
this:
p mod 4 \<noteq> 0

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p mod 4 \<noteq> 0

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
have "p mod 4 \<noteq> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p mod 4 \<noteq> 2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p mod 4 = 2 \<Longrightarrow> False
[PROOF STEP]
assume "p mod 4 = 2"
[PROOF STATE]
proof (state)
this:
p mod 4 = 2

goal (1 subgoal):
 1. p mod 4 = 2 \<Longrightarrow> False
[PROOF STEP]
hence "p mod 4 mod 2 = 0"
[PROOF STATE]
proof (prove)
using this:
p mod 4 = 2

goal (1 subgoal):
 1. p mod 4 mod 2 = 0
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
p mod 4 mod 2 = 0

goal (1 subgoal):
 1. p mod 4 = 2 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
p mod 4 mod 2 = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>prime p\<close> \<open>p > 2\<close> prime_odd_nat[of p]
[PROOF STATE]
proof (prove)
using this:
p mod 4 mod 2 = 0
prime p
2 < p
\<lbrakk>prime p; 2 < p\<rbrakk> \<Longrightarrow> odd p

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p mod 4 \<noteq> 2

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p mod 4 \<noteq> 2

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
have "p mod 4 \<in> {0,1,2,3}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p mod 4 \<in> {0, 1, 2, 3}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p mod 4 \<in> {0, 1, 2, 3}

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
 2. p \<noteq> 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p mod 4 \<noteq> 0
p mod 4 \<noteq> 2
p mod 4 \<in> {0, 1, 2, 3}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p mod 4 \<noteq> 0
p mod 4 \<noteq> 2
p mod 4 \<in> {0, 1, 2, 3}

goal (1 subgoal):
 1. p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
by (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)

goal (1 subgoal):
 1. p = 2 \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
[PROOF STEP]
qed auto


[STATEMENT]
lemma of_nat_prod_mset: "of_nat (prod_mset A) = prod_mset (image_mset of_nat A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (\<Prod>\<^sub># A) = \<Prod>\<^sub># (image_mset of_nat A)
[PROOF STEP]
by (induction A) auto


[STATEMENT]
lemma multiplicity_0_left [simp]: "multiplicity 0 x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (0::'a) x = 0
[PROOF STEP]
by (cases "x = 0") (auto simp: not_dvd_imp_multiplicity_0)


[STATEMENT]
lemma is_unit_power [intro]: "is_unit x \<Longrightarrow> is_unit (x ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_unit x \<Longrightarrow> is_unit (x ^ n)
[PROOF STEP]
by (subst is_unit_power_iff) auto


[STATEMENT]
lemma (in factorial_semiring) pow_divides_pow_iff:
  assumes "n > 0"
  shows   "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ^ n dvd b ^ n) = (a dvd b)
[PROOF STEP]
proof (cases "b = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = (0::'a) \<Longrightarrow> (a ^ n dvd b ^ n) = (a dvd b)
 2. b \<noteq> (0::'a) \<Longrightarrow> (a ^ n dvd b ^ n) = (a dvd b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> (0::'a)

goal (2 subgoals):
 1. b = (0::'a) \<Longrightarrow> (a ^ n dvd b ^ n) = (a dvd b)
 2. b \<noteq> (0::'a) \<Longrightarrow> (a ^ n dvd b ^ n) = (a dvd b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ^ n dvd b ^ n) = (a dvd b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a ^ n dvd b ^ n \<Longrightarrow> a dvd b
 2. a dvd b \<Longrightarrow> a ^ n dvd b ^ n
[PROOF STEP]
assume dvd: "a ^ n dvd b ^ n"
[PROOF STATE]
proof (state)
this:
a ^ n dvd b ^ n

goal (2 subgoals):
 1. a ^ n dvd b ^ n \<Longrightarrow> a dvd b
 2. a dvd b \<Longrightarrow> a ^ n dvd b ^ n
[PROOF STEP]
with \<open>b \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> (0::'a)
a ^ n dvd b ^ n
[PROOF STEP]
have "a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> (0::'a)
a ^ n dvd b ^ n

goal (1 subgoal):
 1. a \<noteq> (0::'a)
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
b \<noteq> (0::'a)
a ^ n dvd b ^ n
0 < n

goal (1 subgoal):
 1. a \<noteq> (0::'a)
[PROOF STEP]
by (auto simp: power_0_left)
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a)

goal (2 subgoals):
 1. a ^ n dvd b ^ n \<Longrightarrow> a dvd b
 2. a dvd b \<Longrightarrow> a ^ n dvd b ^ n
[PROOF STEP]
show "a dvd b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a dvd b
[PROOF STEP]
proof (rule multiplicity_le_imp_dvd)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> (0::'a)
 2. \<And>p. prime p \<Longrightarrow> multiplicity p a \<le> multiplicity p b
[PROOF STEP]
fix p :: 'a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> (0::'a)
 2. \<And>p. prime p \<Longrightarrow> multiplicity p a \<le> multiplicity p b
[PROOF STEP]
assume p: "prime p"
[PROOF STATE]
proof (state)
this:
prime p

goal (2 subgoals):
 1. a \<noteq> (0::'a)
 2. \<And>p. prime p \<Longrightarrow> multiplicity p a \<le> multiplicity p b
[PROOF STEP]
from dvd \<open>b \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
a ^ n dvd b ^ n
b \<noteq> (0::'a)
[PROOF STEP]
have "multiplicity p (a ^ n) \<le> multiplicity p (b ^ n)"
[PROOF STATE]
proof (prove)
using this:
a ^ n dvd b ^ n
b \<noteq> (0::'a)

goal (1 subgoal):
 1. multiplicity p (a ^ n) \<le> multiplicity p (b ^ n)
[PROOF STEP]
by (intro dvd_imp_multiplicity_le) auto
[PROOF STATE]
proof (state)
this:
multiplicity p (a ^ n) \<le> multiplicity p (b ^ n)

goal (2 subgoals):
 1. a \<noteq> (0::'a)
 2. \<And>p. prime p \<Longrightarrow> multiplicity p a \<le> multiplicity p b
[PROOF STEP]
thus "multiplicity p a \<le> multiplicity p b"
[PROOF STATE]
proof (prove)
using this:
multiplicity p (a ^ n) \<le> multiplicity p (b ^ n)

goal (1 subgoal):
 1. multiplicity p a \<le> multiplicity p b
[PROOF STEP]
using p \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
multiplicity p (a ^ n) \<le> multiplicity p (b ^ n)
prime p
a \<noteq> (0::'a)
b \<noteq> (0::'a)
0 < n

goal (1 subgoal):
 1. multiplicity p a \<le> multiplicity p b
[PROOF STEP]
by (simp add: prime_elem_multiplicity_power_distrib)
[PROOF STATE]
proof (state)
this:
multiplicity p a \<le> multiplicity p b

goal (1 subgoal):
 1. a \<noteq> (0::'a)
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
a dvd b

goal (1 subgoal):
 1. a dvd b \<Longrightarrow> a ^ n dvd b ^ n
[PROOF STEP]
qed (auto intro: dvd_power_same)
[PROOF STATE]
proof (state)
this:
(a ^ n dvd b ^ n) = (a dvd b)

goal (1 subgoal):
 1. b = (0::'a) \<Longrightarrow> (a ^ n dvd b ^ n) = (a dvd b)
[PROOF STEP]
qed (use assms in \<open>auto simp: power_0_left\<close>)


[STATEMENT]
lemma multiplicity_power_power:
  fixes p :: "'a :: {factorial_semiring, algebraic_semidom}"
  assumes "n > 0"
  shows   "multiplicity (p ^ n) (x ^ n) = multiplicity p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
proof (cases "x = 0 \<or> p = 0 \<or> is_unit p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = (0::'a) \<or> p = (0::'a) \<or> is_unit p \<Longrightarrow> multiplicity (p ^ n) (x ^ n) = multiplicity p x
 2. \<not> (x = (0::'a) \<or> p = (0::'a) \<or> is_unit p) \<Longrightarrow> multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = (0::'a) \<or> p = (0::'a) \<or> is_unit p

goal (2 subgoals):
 1. x = (0::'a) \<or> p = (0::'a) \<or> is_unit p \<Longrightarrow> multiplicity (p ^ n) (x ^ n) = multiplicity p x
 2. \<not> (x = (0::'a) \<or> p = (0::'a) \<or> is_unit p) \<Longrightarrow> multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = (0::'a) \<or> p = (0::'a) \<or> is_unit p

goal (1 subgoal):
 1. multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
x = (0::'a) \<or> p = (0::'a) \<or> is_unit p
0 < n

goal (1 subgoal):
 1. multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
by (auto simp: power_0_left is_unit_power_iff multiplicity_unit_left)
[PROOF STATE]
proof (state)
this:
multiplicity (p ^ n) (x ^ n) = multiplicity p x

goal (1 subgoal):
 1. \<not> (x = (0::'a) \<or> p = (0::'a) \<or> is_unit p) \<Longrightarrow> multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (x = (0::'a) \<or> p = (0::'a) \<or> is_unit p) \<Longrightarrow> multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (x = (0::'a) \<or> p = (0::'a) \<or> is_unit p)

goal (1 subgoal):
 1. \<not> (x = (0::'a) \<or> p = (0::'a) \<or> is_unit p) \<Longrightarrow> multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (p ^ n) (x ^ n) = multiplicity p x
[PROOF STEP]
proof (intro antisym multiplicity_geI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. x \<noteq> (0::'a)
 2. \<not> is_unit p
 3. p ^ multiplicity (p ^ n) (x ^ n) dvd x
 4. x ^ n \<noteq> (0::'a)
 5. \<not> is_unit (p ^ n)
 6. (p ^ n) ^ multiplicity p x dvd x ^ n
[PROOF STEP]
have "(p ^ multiplicity p x) ^ n dvd x ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p ^ multiplicity p x) ^ n dvd x ^ n
[PROOF STEP]
by (intro dvd_power_same) (simp add: multiplicity_dvd)
[PROOF STATE]
proof (state)
this:
(p ^ multiplicity p x) ^ n dvd x ^ n

goal (6 subgoals):
 1. x \<noteq> (0::'a)
 2. \<not> is_unit p
 3. p ^ multiplicity (p ^ n) (x ^ n) dvd x
 4. x ^ n \<noteq> (0::'a)
 5. \<not> is_unit (p ^ n)
 6. (p ^ n) ^ multiplicity p x dvd x ^ n
[PROOF STEP]
thus "(p ^ n) ^ multiplicity p x dvd x ^ n"
[PROOF STATE]
proof (prove)
using this:
(p ^ multiplicity p x) ^ n dvd x ^ n

goal (1 subgoal):
 1. (p ^ n) ^ multiplicity p x dvd x ^ n
[PROOF STEP]
by (simp add: mult_ac flip: power_mult)
[PROOF STATE]
proof (state)
this:
(p ^ n) ^ multiplicity p x dvd x ^ n

goal (5 subgoals):
 1. x \<noteq> (0::'a)
 2. \<not> is_unit p
 3. p ^ multiplicity (p ^ n) (x ^ n) dvd x
 4. x ^ n \<noteq> (0::'a)
 5. \<not> is_unit (p ^ n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. x \<noteq> (0::'a)
 2. \<not> is_unit p
 3. p ^ multiplicity (p ^ n) (x ^ n) dvd x
 4. x ^ n \<noteq> (0::'a)
 5. \<not> is_unit (p ^ n)
[PROOF STEP]
have "(p ^ n) ^ multiplicity (p ^ n) (x ^ n) dvd x ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p ^ n) ^ multiplicity (p ^ n) (x ^ n) dvd x ^ n
[PROOF STEP]
by (simp add: multiplicity_dvd)
[PROOF STATE]
proof (state)
this:
(p ^ n) ^ multiplicity (p ^ n) (x ^ n) dvd x ^ n

goal (5 subgoals):
 1. x \<noteq> (0::'a)
 2. \<not> is_unit p
 3. p ^ multiplicity (p ^ n) (x ^ n) dvd x
 4. x ^ n \<noteq> (0::'a)
 5. \<not> is_unit (p ^ n)
[PROOF STEP]
hence "(p ^ multiplicity (p ^ n) (x ^ n)) ^ n dvd x ^ n"
[PROOF STATE]
proof (prove)
using this:
(p ^ n) ^ multiplicity (p ^ n) (x ^ n) dvd x ^ n

goal (1 subgoal):
 1. (p ^ multiplicity (p ^ n) (x ^ n)) ^ n dvd x ^ n
[PROOF STEP]
by (simp add: mult_ac flip: power_mult)
[PROOF STATE]
proof (state)
this:
(p ^ multiplicity (p ^ n) (x ^ n)) ^ n dvd x ^ n

goal (5 subgoals):
 1. x \<noteq> (0::'a)
 2. \<not> is_unit p
 3. p ^ multiplicity (p ^ n) (x ^ n) dvd x
 4. x ^ n \<noteq> (0::'a)
 5. \<not> is_unit (p ^ n)
[PROOF STEP]
thus "p ^ multiplicity (p ^ n) (x ^ n) dvd x"
[PROOF STATE]
proof (prove)
using this:
(p ^ multiplicity (p ^ n) (x ^ n)) ^ n dvd x ^ n

goal (1 subgoal):
 1. p ^ multiplicity (p ^ n) (x ^ n) dvd x
[PROOF STEP]
by (subst (asm) pow_divides_pow_iff) (use assms in auto)
[PROOF STATE]
proof (state)
this:
p ^ multiplicity (p ^ n) (x ^ n) dvd x

goal (4 subgoals):
 1. x \<noteq> (0::'a)
 2. \<not> is_unit p
 3. x ^ n \<noteq> (0::'a)
 4. \<not> is_unit (p ^ n)
[PROOF STEP]
qed (use False \<open>n > 0\<close> in \<open>auto simp: is_unit_power_iff\<close>)
[PROOF STATE]
proof (state)
this:
multiplicity (p ^ n) (x ^ n) = multiplicity p x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma even_square_cong_4_int:
  fixes x :: int
  assumes "even x"
  shows   "[x ^ 2 = 0] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
even x
[PROOF STEP]
have "even \<bar>x\<bar>"
[PROOF STATE]
proof (prove)
using this:
even x

goal (1 subgoal):
 1. even \<bar>x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even \<bar>x\<bar>

goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
hence [simp]: "\<bar>x\<bar> mod 2 = 0"
[PROOF STATE]
proof (prove)
using this:
even \<bar>x\<bar>

goal (1 subgoal):
 1. \<bar>x\<bar> mod 2 = 0
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> mod 2 = 0

goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
have "(\<bar>x\<bar> ^ 2) mod 4 = ((\<bar>x\<bar> mod 4) ^ 2) mod 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar>\<^sup>2 mod 4 = (\<bar>x\<bar> mod 4)\<^sup>2 mod 4
[PROOF STEP]
by (simp add: power_mod)
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar>\<^sup>2 mod 4 = (\<bar>x\<bar> mod 4)\<^sup>2 mod 4

goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar>\<^sup>2 mod 4 = (\<bar>x\<bar> mod 4)\<^sup>2 mod 4

goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
even x
[PROOF STEP]
have "\<bar>x\<bar> mod 4 = 0 \<or> \<bar>x\<bar> mod 4 = 2"
[PROOF STATE]
proof (prove)
using this:
even x

goal (1 subgoal):
 1. \<bar>x\<bar> mod 4 = 0 \<or> \<bar>x\<bar> mod 4 = 2
[PROOF STEP]
using mod_double_modulus[of 2 "\<bar>x\<bar>"]
[PROOF STATE]
proof (prove)
using this:
even x
\<lbrakk>0 < 2; 0 \<le> \<bar>x\<bar>\<rbrakk> \<Longrightarrow> \<bar>x\<bar> mod (2 * 2) = \<bar>x\<bar> mod 2 \<or> \<bar>x\<bar> mod (2 * 2) = \<bar>x\<bar> mod 2 + 2

goal (1 subgoal):
 1. \<bar>x\<bar> mod 4 = 0 \<or> \<bar>x\<bar> mod 4 = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> mod 4 = 0 \<or> \<bar>x\<bar> mod 4 = 2

goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
hence "((\<bar>x\<bar> mod 4) ^ 2) mod 4 = 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> mod 4 = 0 \<or> \<bar>x\<bar> mod 4 = 2

goal (1 subgoal):
 1. (\<bar>x\<bar> mod 4)\<^sup>2 mod 4 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<bar>x\<bar> mod 4)\<^sup>2 mod 4 = 0

goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar>\<^sup>2 mod 4 = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar>\<^sup>2 mod 4 = 0

goal (1 subgoal):
 1. [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[x\<^sup>2 = 0] (mod 4)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma even_square_cong_4_nat: "even (x::nat) \<Longrightarrow> [x ^ 2 = 0] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even x \<Longrightarrow> [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
using even_square_cong_4_int[of "int x"]
[PROOF STATE]
proof (prove)
using this:
even (int x) \<Longrightarrow> [(int x)\<^sup>2 = 0] (mod 4)

goal (1 subgoal):
 1. even x \<Longrightarrow> [x\<^sup>2 = 0] (mod 4)
[PROOF STEP]
by (auto simp flip: cong_int_iff)


[STATEMENT]
lemma odd_square_cong_4_int:
  fixes x :: int
  assumes "odd x"
  shows   "[x ^ 2 = 1] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
odd x
[PROOF STEP]
have "odd \<bar>x\<bar>"
[PROOF STATE]
proof (prove)
using this:
odd x

goal (1 subgoal):
 1. odd \<bar>x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
odd \<bar>x\<bar>

goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
hence [simp]: "\<bar>x\<bar> mod 2 = 1"
[PROOF STATE]
proof (prove)
using this:
odd \<bar>x\<bar>

goal (1 subgoal):
 1. \<bar>x\<bar> mod 2 = 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> mod 2 = 1

goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
have "(\<bar>x\<bar> ^ 2) mod 4 = ((\<bar>x\<bar> mod 4) ^ 2) mod 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar>\<^sup>2 mod 4 = (\<bar>x\<bar> mod 4)\<^sup>2 mod 4
[PROOF STEP]
by (simp add: power_mod)
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar>\<^sup>2 mod 4 = (\<bar>x\<bar> mod 4)\<^sup>2 mod 4

goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar>\<^sup>2 mod 4 = (\<bar>x\<bar> mod 4)\<^sup>2 mod 4

goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
odd x
[PROOF STEP]
have "\<bar>x\<bar> mod 4 = 1 \<or> \<bar>x\<bar> mod 4 = 3"
[PROOF STATE]
proof (prove)
using this:
odd x

goal (1 subgoal):
 1. \<bar>x\<bar> mod 4 = 1 \<or> \<bar>x\<bar> mod 4 = 3
[PROOF STEP]
using mod_double_modulus[of 2 "\<bar>x\<bar>"]
[PROOF STATE]
proof (prove)
using this:
odd x
\<lbrakk>0 < 2; 0 \<le> \<bar>x\<bar>\<rbrakk> \<Longrightarrow> \<bar>x\<bar> mod (2 * 2) = \<bar>x\<bar> mod 2 \<or> \<bar>x\<bar> mod (2 * 2) = \<bar>x\<bar> mod 2 + 2

goal (1 subgoal):
 1. \<bar>x\<bar> mod 4 = 1 \<or> \<bar>x\<bar> mod 4 = 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> mod 4 = 1 \<or> \<bar>x\<bar> mod 4 = 3

goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
hence "((\<bar>x\<bar> mod 4) ^ 2) mod 4 = 1"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> mod 4 = 1 \<or> \<bar>x\<bar> mod 4 = 3

goal (1 subgoal):
 1. (\<bar>x\<bar> mod 4)\<^sup>2 mod 4 = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<bar>x\<bar> mod 4)\<^sup>2 mod 4 = 1

goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar>\<^sup>2 mod 4 = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar>\<^sup>2 mod 4 = 1

goal (1 subgoal):
 1. [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[x\<^sup>2 = 1] (mod 4)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma odd_square_cong_4_nat: "odd (x::nat) \<Longrightarrow> [x ^ 2 = 1] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd x \<Longrightarrow> [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
using odd_square_cong_4_int[of "int x"]
[PROOF STATE]
proof (prove)
using this:
odd (int x) \<Longrightarrow> [(int x)\<^sup>2 = 1] (mod 4)

goal (1 subgoal):
 1. odd x \<Longrightarrow> [x\<^sup>2 = 1] (mod 4)
[PROOF STEP]
by (auto simp flip: cong_int_iff)


[STATEMENT]
lemma is_nth_power_upto_unit_base: "is_nth_power n x \<Longrightarrow> is_nth_power_upto_unit n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power n x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_def intro: exI[of _ 1])


[STATEMENT]
lemma is_nth_power_upto_unitI:
  assumes "normalize (x ^ n) = normalize y"
  shows   "is_nth_power_upto_unit n y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit n y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_nth_power_upto_unit n y
[PROOF STEP]
from associatedE1[OF assms]
[PROOF STATE]
proof (chain)
picking this:
(\<And>u. \<lbrakk>is_unit u; x ^ n = u * y\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain u where "is_unit u" "u * y = x ^ n"
[PROOF STATE]
proof (prove)
using this:
(\<And>u. \<lbrakk>is_unit u; x ^ n = u * y\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>is_unit u; u * y = x ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_unit u
u * y = x ^ n

goal (1 subgoal):
 1. is_nth_power_upto_unit n y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_unit u
u * y = x ^ n

goal (1 subgoal):
 1. is_nth_power_upto_unit n y
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_def intro!: exI[of _ u])
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_nth_power_upto_unit_conv_multiplicity:
  fixes x :: "'a :: factorial_semiring"
  assumes "n > 0"
  shows   "is_nth_power_upto_unit n x \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = (0::'a) \<Longrightarrow> is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)
 2. x \<noteq> (0::'a) \<Longrightarrow> is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'a)

goal (2 subgoals):
 1. x = (0::'a) \<Longrightarrow> is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)
 2. x \<noteq> (0::'a) \<Longrightarrow> is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
fix p :: 'a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
assume p: "prime p"
[PROOF STATE]
proof (state)
this:
prime p

goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
assume "is_nth_power_upto_unit n x"
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x

goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_nth_power_upto_unit n x
[PROOF STEP]
obtain u y where uy: "is_unit u" "u * x = y ^ n"
[PROOF STATE]
proof (prove)
using this:
is_nth_power_upto_unit n x

goal (1 subgoal):
 1. (\<And>u y. \<lbrakk>is_unit u; u * x = y ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_def elim!: is_nth_powerE)
[PROOF STATE]
proof (state)
this:
is_unit u
u * x = y ^ n

goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
from p uy assms False
[PROOF STATE]
proof (chain)
picking this:
prime p
is_unit u
u * x = y ^ n
0 < n
x \<noteq> (0::'a)
[PROOF STEP]
have [simp]: "y \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
prime p
is_unit u
u * x = y ^ n
0 < n
x \<noteq> (0::'a)

goal (1 subgoal):
 1. y \<noteq> (0::'a)
[PROOF STEP]
by (auto simp: power_0_left)
[PROOF STATE]
proof (state)
this:
y \<noteq> (0::'a)

goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
have "multiplicity p (u * x) = multiplicity p (y ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (u * x) = multiplicity p (y ^ n)
[PROOF STEP]
by (subst uy(2) [symmetric]) simp
[PROOF STATE]
proof (state)
this:
multiplicity p (u * x) = multiplicity p (y ^ n)

goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity p (u * x) = multiplicity p (y ^ n)

goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
have "multiplicity p (u * x) = multiplicity p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (u * x) = multiplicity p x
[PROOF STEP]
by (simp add: multiplicity_times_unit_right uy(1))
[PROOF STATE]
proof (state)
this:
multiplicity p (u * x) = multiplicity p x

goal (2 subgoals):
 1. \<And>p. \<lbrakk>is_nth_power_upto_unit n x; prime p\<rbrakk> \<Longrightarrow> n dvd multiplicity p x
 2. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicity p x = multiplicity p (y ^ n)
[PROOF STEP]
show "n dvd multiplicity p x"
[PROOF STATE]
proof (prove)
using this:
multiplicity p x = multiplicity p (y ^ n)

goal (1 subgoal):
 1. n dvd multiplicity p x
[PROOF STEP]
using False and p and uy and assms
[PROOF STATE]
proof (prove)
using this:
multiplicity p x = multiplicity p (y ^ n)
x \<noteq> (0::'a)
prime p
is_unit u
u * x = y ^ n
0 < n

goal (1 subgoal):
 1. n dvd multiplicity p x
[PROOF STEP]
by (auto simp: prime_elem_multiplicity_power_distrib)
[PROOF STATE]
proof (state)
this:
n dvd multiplicity p x

goal (1 subgoal):
 1. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
assume *: "\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x"
[PROOF STATE]
proof (state)
this:
\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x

goal (1 subgoal):
 1. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
have "multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) =
            multiplicity p x" if "prime p" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity p x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity p x
[PROOF STEP]
from that and *
[PROOF STATE]
proof (chain)
picking this:
prime p
\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x
[PROOF STEP]
have "n dvd multiplicity p x"
[PROOF STATE]
proof (prove)
using this:
prime p
\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x

goal (1 subgoal):
 1. n dvd multiplicity p x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n dvd multiplicity p x

goal (1 subgoal):
 1. multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity p x
[PROOF STEP]
have "multiplicity p x = 0" if "p \<notin> prime_factors x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p x = 0
[PROOF STEP]
using that and \<open>prime p\<close>
[PROOF STATE]
proof (prove)
using this:
p \<notin> prime_factors x
prime p

goal (1 subgoal):
 1. multiplicity p x = 0
[PROOF STEP]
by (simp add: prime_factors_multiplicity)
[PROOF STATE]
proof (state)
this:
p \<notin> prime_factors x \<Longrightarrow> multiplicity p x = 0

goal (1 subgoal):
 1. multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity p x
[PROOF STEP]
with that and * and assms
[PROOF STATE]
proof (chain)
picking this:
prime p
\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x
0 < n
p \<notin> prime_factors x \<Longrightarrow> multiplicity p x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime p
\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x
0 < n
p \<notin> prime_factors x \<Longrightarrow> multiplicity p x = 0

goal (1 subgoal):
 1. multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity p x
[PROOF STEP]
unfolding prod_power_distrib power_mult [symmetric]
[PROOF STATE]
proof (prove)
using this:
prime p
\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x
0 < n
p \<notin> prime_factors x \<Longrightarrow> multiplicity p x = 0

goal (1 subgoal):
 1. multiplicity p (\<Prod>xa\<in>prime_factors x. xa ^ (multiplicity xa x div n * n)) = multiplicity p x
[PROOF STEP]
by (subst multiplicity_prod_prime_powers) (auto simp: in_prime_factors_imp_prime elim: dvdE)
[PROOF STATE]
proof (state)
this:
multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity p x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime ?p \<Longrightarrow> multiplicity ?p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity ?p x

goal (1 subgoal):
 1. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
with assms False
[PROOF STATE]
proof (chain)
picking this:
0 < n
x \<noteq> (0::'a)
prime ?p \<Longrightarrow> multiplicity ?p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity ?p x
[PROOF STEP]
have "normalize ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = normalize x"
[PROOF STATE]
proof (prove)
using this:
0 < n
x \<noteq> (0::'a)
prime ?p \<Longrightarrow> multiplicity ?p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = multiplicity ?p x

goal (1 subgoal):
 1. normalize ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = normalize x
[PROOF STEP]
by (intro multiplicity_eq_imp_eq) (auto simp: multiplicity_prod_prime_powers)
[PROOF STATE]
proof (state)
this:
normalize ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = normalize x

goal (1 subgoal):
 1. \<forall>p. prime p \<longrightarrow> n dvd multiplicity p x \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
thus "is_nth_power_upto_unit n x"
[PROOF STATE]
proof (prove)
using this:
normalize ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = normalize x

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
by (auto intro: is_nth_power_upto_unitI)
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)

goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> is_nth_power_upto_unit n x = (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)
[PROOF STEP]
qed (use assms in \<open>auto simp: is_nth_power_upto_unit_def\<close>)


[STATEMENT]
lemma is_nth_power_upto_unit_0_left [simp, intro]: "is_nth_power_upto_unit 0 x \<longleftrightarrow> is_unit x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit 0 x = is_unit x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_nth_power_upto_unit 0 x \<Longrightarrow> is_unit x
 2. is_unit x \<Longrightarrow> is_nth_power_upto_unit 0 x
[PROOF STEP]
assume "is_unit x"
[PROOF STATE]
proof (state)
this:
is_unit x

goal (2 subgoals):
 1. is_nth_power_upto_unit 0 x \<Longrightarrow> is_unit x
 2. is_unit x \<Longrightarrow> is_nth_power_upto_unit 0 x
[PROOF STEP]
thus "is_nth_power_upto_unit 0 x"
[PROOF STATE]
proof (prove)
using this:
is_unit x

goal (1 subgoal):
 1. is_nth_power_upto_unit 0 x
[PROOF STEP]
unfolding is_nth_power_upto_unit_def
[PROOF STATE]
proof (prove)
using this:
is_unit x

goal (1 subgoal):
 1. \<exists>u. is_unit u \<and> is_nth_power 0 (u * x)
[PROOF STEP]
by (intro exI[of _ "1 div x"]) auto
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit 0 x

goal (1 subgoal):
 1. is_nth_power_upto_unit 0 x \<Longrightarrow> is_unit x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_nth_power_upto_unit 0 x \<Longrightarrow> is_unit x
[PROOF STEP]
assume "is_nth_power_upto_unit 0 x"
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit 0 x

goal (1 subgoal):
 1. is_nth_power_upto_unit 0 x \<Longrightarrow> is_unit x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_nth_power_upto_unit 0 x
[PROOF STEP]
obtain u where "is_unit u" "u * x = 1"
[PROOF STATE]
proof (prove)
using this:
is_nth_power_upto_unit 0 x

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>is_unit u; u * x = (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_def)
[PROOF STATE]
proof (state)
this:
is_unit u
u * x = (1::'a)

goal (1 subgoal):
 1. is_nth_power_upto_unit 0 x \<Longrightarrow> is_unit x
[PROOF STEP]
thus "is_unit x"
[PROOF STATE]
proof (prove)
using this:
is_unit u
u * x = (1::'a)

goal (1 subgoal):
 1. is_unit x
[PROOF STEP]
by (metis dvd_triv_right)
[PROOF STATE]
proof (state)
this:
is_unit x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_nth_power_upto_unit_unit [simp, intro]:
  assumes "is_unit x"
  shows   "is_nth_power_upto_unit n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_unit x

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_def intro!: exI[of _ "1 div x"])


[STATEMENT]
lemma is_nth_power_upto_unit_1_left [simp, intro]: "is_nth_power_upto_unit 1 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit 1 x
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_def intro: exI[of _ 1])