[STATEMENT]
lemma mod_or_dist[simp]: "h\<Turnstile>P\<or>\<^sub>AQ \<longleftrightarrow> h\<Turnstile>P \<or> h\<Turnstile>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> P \<or>\<^sub>A Q) = (h \<Turnstile> P \<or> h \<Turnstile> Q)
[PROOF STEP]
unfolding sup_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P \<or> h \<Turnstile> Q)) = (h \<Turnstile> P \<or> h \<Turnstile> Q)
[PROOF STEP]
by (simp add: Abs_assn_inverse)


[STATEMENT]
lemma mod_not_dist[simp]: "h\<Turnstile>(\<not>\<^sub>AP) \<longleftrightarrow> in_range h \<and> \<not> h\<Turnstile>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> \<not>\<^sub>A P) = (in_range h \<and> \<not> h \<Turnstile> P)
[PROOF STEP]
unfolding uminus_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn (\<lambda>h. in_range h \<and> \<not> h \<Turnstile> P)) = (in_range h \<and> \<not> h \<Turnstile> P)
[PROOF STEP]
by (simp add: Abs_assn_inverse)


[STATEMENT]
lemma mod_pure_star_dist[simp]: "h\<Turnstile>P*\<up>b \<longleftrightarrow> h\<Turnstile>P \<and> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> P * \<up> b) = (h \<Turnstile> P \<and> b)
[PROOF STEP]
by (metis (full_types) mod_false mult_1_right pure_false
    pure_true star_false_right)


[STATEMENT]
lemma mod_star_trueI: "h\<Turnstile>P \<Longrightarrow> h\<Turnstile>P*true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> P \<Longrightarrow> h \<Turnstile> P * true
[PROOF STEP]
unfolding times_assn_def top_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> P \<Longrightarrow> h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn (Abs_assn in_range)))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> P \<Longrightarrow> times_assn_raw (Rep_assn P) in_range h
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>h \<Turnstile> P; h = (a, b)\<rbrakk> \<Longrightarrow> times_assn_raw (Rep_assn P) in_range h
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mod_star_trueE': assumes "h\<Turnstile>P*true" obtains h' where
  "fst h' = fst h" and "snd h' \<subseteq> snd h" and "h'\<Turnstile>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h'. \<lbrakk>fst h' = fst h; snd h' \<subseteq> snd h; h' \<Turnstile> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> P * true

goal (1 subgoal):
 1. (\<And>h'. \<lbrakk>fst h' = fst h; snd h' \<subseteq> snd h; h' \<Turnstile> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding times_assn_def top_assn_def
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn (Abs_assn in_range)))

goal (1 subgoal):
 1. (\<And>h'. \<lbrakk>fst h' = fst h; snd h' \<subseteq> snd h; h' \<Turnstile> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>h'. \<lbrakk>fst h' = fst h; snd h' \<subseteq> snd h; h' \<Turnstile> P\<rbrakk> \<Longrightarrow> thesis; h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn (Abs_assn in_range))); h = (a, b)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (fastforce simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mod_star_trueE: assumes "h\<Turnstile>P*true" obtains h' where "h'\<Turnstile>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h'. h' \<Turnstile> P \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> P * true

goal (1 subgoal):
 1. (\<And>h'. h' \<Turnstile> P \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast elim: mod_star_trueE')


[STATEMENT]
lemma mod_h_bot_iff[simp]:
  "(h,{}) \<Turnstile> \<up>b \<longleftrightarrow> b"
  "(h,{}) \<Turnstile> true"
  "(h,{}) \<Turnstile> p\<mapsto>\<^sub>rx \<longleftrightarrow> False"
  "(h,{}) \<Turnstile> q\<mapsto>\<^sub>ay \<longleftrightarrow> False"
  "(h,{}) \<Turnstile> P*Q \<longleftrightarrow> ((h,{}) \<Turnstile> P) \<and> ((h,{}) \<Turnstile> Q)"
  "(h,{}) \<Turnstile> P\<and>\<^sub>AQ \<longleftrightarrow> ((h,{}) \<Turnstile> P) \<and> ((h,{}) \<Turnstile> Q)"
  "(h,{}) \<Turnstile> P\<or>\<^sub>AQ \<longleftrightarrow> ((h,{}) \<Turnstile> P) \<or> ((h,{}) \<Turnstile> Q)"
  "(h,{}) \<Turnstile> (\<exists>\<^sub>Ax. R x) \<longleftrightarrow> (\<exists>x. (h,{}) \<Turnstile> R x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((((h, {}) \<Turnstile> \<up> b) = b &&& (h, {}) \<Turnstile> true) &&& ((h, {}) \<Turnstile> p \<mapsto>\<^sub>r x) = False &&& ((h, {}) \<Turnstile> q \<mapsto>\<^sub>a y) = False) &&& (((h, {}) \<Turnstile> P * Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q) &&& ((h, {}) \<Turnstile> P \<and>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)) &&& ((h, {}) \<Turnstile> P \<or>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<or> (h, {}) \<Turnstile> Q) &&& ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply (simp add: pure_assn_def Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. (h, {}) \<Turnstile> true
 2. ((h, {}) \<Turnstile> p \<mapsto>\<^sub>r x) = False
 3. ((h, {}) \<Turnstile> q \<mapsto>\<^sub>a y) = False
 4. ((h, {}) \<Turnstile> P * Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 5. ((h, {}) \<Turnstile> P \<and>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 6. ((h, {}) \<Turnstile> P \<or>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<or> (h, {}) \<Turnstile> Q)
 7. ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. ((h, {}) \<Turnstile> p \<mapsto>\<^sub>r x) = False
 2. ((h, {}) \<Turnstile> q \<mapsto>\<^sub>a y) = False
 3. ((h, {}) \<Turnstile> P * Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 4. ((h, {}) \<Turnstile> P \<and>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 5. ((h, {}) \<Turnstile> P \<or>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<or> (h, {}) \<Turnstile> Q)
 6. ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply (simp add: sngr_assn_def Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. ((h, {}) \<Turnstile> q \<mapsto>\<^sub>a y) = False
 2. ((h, {}) \<Turnstile> P * Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 3. ((h, {}) \<Turnstile> P \<and>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 4. ((h, {}) \<Turnstile> P \<or>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<or> (h, {}) \<Turnstile> Q)
 5. ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply (simp add: snga_assn_def Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. ((h, {}) \<Turnstile> P * Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 2. ((h, {}) \<Turnstile> P \<and>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 3. ((h, {}) \<Turnstile> P \<or>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<or> (h, {}) \<Turnstile> Q)
 4. ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply (simp add: times_assn_def Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ((h, {}) \<Turnstile> P \<and>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<and> (h, {}) \<Turnstile> Q)
 2. ((h, {}) \<Turnstile> P \<or>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<or> (h, {}) \<Turnstile> Q)
 3. ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply (simp add: inf_assn_def Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((h, {}) \<Turnstile> P \<or>\<^sub>A Q) = ((h, {}) \<Turnstile> P \<or> (h, {}) \<Turnstile> Q)
 2. ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply (simp add: sup_assn_def Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((h, {}) \<Turnstile> (\<exists>\<^sub>Ax. R x)) = (\<exists>x. (h, {}) \<Turnstile> R x)
[PROOF STEP]
apply (simp add: ex_assn_def Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma entailsI:
  assumes "\<And>h. h\<Turnstile>P \<Longrightarrow> h\<Turnstile>Q"
  shows "P \<Longrightarrow>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> P \<Longrightarrow> ?h \<Turnstile> Q

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> P \<Longrightarrow> ?h \<Turnstile> Q

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q
[PROOF STEP]
by auto


[STATEMENT]
lemma entailsD:
  assumes "P \<Longrightarrow>\<^sub>A Q"
  assumes "h\<Turnstile>P"
  shows "h\<Turnstile>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>A Q
h \<Turnstile> P

goal (1 subgoal):
 1. h \<Turnstile> Q
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q
h \<Turnstile> P

goal (1 subgoal):
 1. h \<Turnstile> Q
[PROOF STEP]
by blast


[STATEMENT]
lemma ent_fwd:
  assumes "h\<Turnstile>P"
  assumes "P \<Longrightarrow>\<^sub>A Q"
  shows "h\<Turnstile>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> Q
[PROOF STEP]
using assms(2,1)
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>A Q
h \<Turnstile> P

goal (1 subgoal):
 1. h \<Turnstile> Q
[PROOF STEP]
by (rule entailsD)


[STATEMENT]
lemma ent_refl[simp]: "P \<Longrightarrow>\<^sub>A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A P
[PROOF STEP]
by (auto simp: entailsI)


[STATEMENT]
lemma ent_trans[trans]: "\<lbrakk> P \<Longrightarrow>\<^sub>A Q; Q \<Longrightarrow>\<^sub>AR \<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<^sub>A R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow>\<^sub>A Q; Q \<Longrightarrow>\<^sub>A R\<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<^sub>A R
[PROOF STEP]
by (auto intro: entailsI dest: entailsD)


[STATEMENT]
lemma ent_iffI:
  assumes "A\<Longrightarrow>\<^sub>AB"
  assumes "B\<Longrightarrow>\<^sub>AA"
  shows "A=B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
apply (subst Rep_assn_inject[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_assn A = Rep_assn B
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<Turnstile> A) = (x \<Turnstile> B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<Longrightarrow>\<^sub>A B
B \<Longrightarrow>\<^sub>A A

goal (1 subgoal):
 1. \<And>x. (x \<Turnstile> A) = (x \<Turnstile> B)
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> A \<longrightarrow> h \<Turnstile> B
\<forall>h. h \<Turnstile> B \<longrightarrow> h \<Turnstile> A

goal (1 subgoal):
 1. \<And>x. (x \<Turnstile> A) = (x \<Turnstile> B)
[PROOF STEP]
by blast


[STATEMENT]
lemma ent_false[simp]: "false \<Longrightarrow>\<^sub>A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false \<Longrightarrow>\<^sub>A P
[PROOF STEP]
by (auto intro: entailsI)


[STATEMENT]
lemma ent_true[simp]: "P \<Longrightarrow>\<^sub>A true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A true
[PROOF STEP]
by (auto intro!: entailsI simp: models_in_range)


[STATEMENT]
lemma ent_false_iff[simp]: "(P \<Longrightarrow>\<^sub>A false) \<longleftrightarrow> (\<forall>h. \<not>h\<Turnstile>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A false) = (\<forall>h. \<not> h \<Turnstile> P)
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> false) = (\<forall>h. \<not> h \<Turnstile> P)
[PROOF STEP]
by auto


[STATEMENT]
lemma ent_pure_pre_iff[simp]: "(P*\<up>b \<Longrightarrow>\<^sub>A Q) \<longleftrightarrow> (b \<longrightarrow> (P \<Longrightarrow>\<^sub>A Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P * \<up> b \<Longrightarrow>\<^sub>A Q) = (b \<longrightarrow> (P \<Longrightarrow>\<^sub>A Q))
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h. h \<Turnstile> P * \<up> b \<longrightarrow> h \<Turnstile> Q) = (b \<longrightarrow> (\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q))
[PROOF STEP]
by (auto simp add: mod_dist)


[STATEMENT]
lemma ent_pure_pre_iff_sng[simp]:
  "(\<up>b \<Longrightarrow>\<^sub>A Q) \<longleftrightarrow> (b \<longrightarrow> (emp \<Longrightarrow>\<^sub>A Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<up> b \<Longrightarrow>\<^sub>A Q) = (b \<longrightarrow> (emp \<Longrightarrow>\<^sub>A Q))
[PROOF STEP]
using ent_pure_pre_iff[where P=emp]
[PROOF STATE]
proof (prove)
using this:
(emp * \<up> ?b \<Longrightarrow>\<^sub>A ?Q) = (?b \<longrightarrow> (emp \<Longrightarrow>\<^sub>A ?Q))

goal (1 subgoal):
 1. (\<up> b \<Longrightarrow>\<^sub>A Q) = (b \<longrightarrow> (emp \<Longrightarrow>\<^sub>A Q))
[PROOF STEP]
by simp


[STATEMENT]
lemma ent_pure_post_iff[simp]:
  "(P \<Longrightarrow>\<^sub>A Q*\<up>b) \<longleftrightarrow> ((\<forall>h. h\<Turnstile>P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A Q * \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A Q))
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q * \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q))
[PROOF STEP]
by (auto simp add: mod_dist)


[STATEMENT]
lemma ent_pure_post_iff_sng[simp]:
  "(P \<Longrightarrow>\<^sub>A \<up>b) \<longleftrightarrow> ((\<forall>h. h\<Turnstile>P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))
[PROOF STEP]
using ent_pure_post_iff[where Q=emp]
[PROOF STATE]
proof (prove)
using this:
(?P \<Longrightarrow>\<^sub>A emp * \<up> ?b) = ((\<forall>h. h \<Turnstile> ?P \<longrightarrow> ?b) \<and> (?P \<Longrightarrow>\<^sub>A emp))

goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))
[PROOF STEP]
by simp


[STATEMENT]
lemma ent_ex_preI: "(\<And>x. P x \<Longrightarrow>\<^sub>A Q) \<Longrightarrow> \<exists>\<^sub>Ax. P x \<Longrightarrow>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. P x \<Longrightarrow>\<^sub>A Q) \<Longrightarrow> \<exists>\<^sub>Ax. P x \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
unfolding entails_def ex_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<forall>h. h \<Turnstile> P x \<longrightarrow> h \<Turnstile> Q) \<Longrightarrow> \<forall>h. h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x) \<longrightarrow> h \<Turnstile> Q
[PROOF STEP]
by (auto simp: Abs_assn_inverse)


[STATEMENT]
lemma ent_ex_postI: "(P \<Longrightarrow>\<^sub>A Q x) \<Longrightarrow> P \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax. Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q x \<Longrightarrow> P \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax. Q x
[PROOF STEP]
unfolding entails_def ex_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q x \<Longrightarrow> \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Q x)
[PROOF STEP]
by (auto simp: Abs_assn_inverse)


[STATEMENT]
lemma ent_mp: "(P * (P -* Q)) \<Longrightarrow>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * (P -* Q) \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
apply (rule entailsI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. h \<Turnstile> P * (P -* Q) \<Longrightarrow> h \<Turnstile> Q
[PROOF STEP]
unfolding times_assn_def wand_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn (Abs_assn (wand_raw (Rep_assn P) (Rep_assn Q))))) \<Longrightarrow> h \<Turnstile> Q
[PROOF STEP]
apply (clarsimp simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as1 as2. \<lbrakk>as1 \<inter> as2 = {}; (a, as1) \<Turnstile> P; in_range (a, as2); \<forall>h' as'. as2 \<inter> as' = {} \<and> relH as2 a h' \<and> in_range (h', as2) \<and> (h', as') \<Turnstile> P \<longrightarrow> (h', as2 \<union> as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (a, as1 \<union> as2) \<Turnstile> Q
[PROOF STEP]
apply (drule_tac x="a" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as1 as2. \<lbrakk>as1 \<inter> as2 = {}; (a, as1) \<Turnstile> P; in_range (a, as2); \<forall>as'. as2 \<inter> as' = {} \<and> relH as2 a a \<and> in_range (a, as2) \<and> (a, as') \<Turnstile> P \<longrightarrow> (a, as2 \<union> as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (a, as1 \<union> as2) \<Turnstile> Q
[PROOF STEP]
apply (drule_tac x="as1" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as1 as2. \<lbrakk>as1 \<inter> as2 = {}; (a, as1) \<Turnstile> P; in_range (a, as2); as2 \<inter> as1 = {} \<and> relH as2 a a \<and> in_range (a, as2) \<and> (a, as1) \<Turnstile> P \<longrightarrow> (a, as2 \<union> as1) \<Turnstile> Q\<rbrakk> \<Longrightarrow> (a, as1 \<union> as2) \<Turnstile> Q
[PROOF STEP]
apply (auto simp: Un_ac relH_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ent_star_mono: "\<lbrakk> P \<Longrightarrow>\<^sub>A P'; Q \<Longrightarrow>\<^sub>A Q'\<rbrakk> \<Longrightarrow> P*Q \<Longrightarrow>\<^sub>A P'*Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow>\<^sub>A P'; Q \<Longrightarrow>\<^sub>A Q'\<rbrakk> \<Longrightarrow> P * Q \<Longrightarrow>\<^sub>A P' * Q'
[PROOF STEP]
unfolding entails_def times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> P'; \<forall>h. h \<Turnstile> Q \<longrightarrow> h \<Turnstile> Q'\<rbrakk> \<Longrightarrow> \<forall>h. h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q)) \<longrightarrow> h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P') (Rep_assn Q'))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> P'; \<forall>a b. (a, b) \<Turnstile> Q \<longrightarrow> (a, b) \<Turnstile> Q'\<rbrakk> \<Longrightarrow> \<forall>a b. (\<exists>as1 as2. b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> P \<and> (a, as2) \<Turnstile> Q) \<longrightarrow> (\<exists>as1 as2. b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> P' \<and> (a, as2) \<Turnstile> Q')
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ent_wandI:
  assumes IMP: "Q*P \<Longrightarrow>\<^sub>A R"
  shows "P \<Longrightarrow>\<^sub>A (Q -* R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q -* R
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q -* R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> (a, b) \<Turnstile> Q -* R
[PROOF STEP]
apply (rule wand_assnI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> in_range (a, b)
 2. \<And>a b h' as'. \<lbrakk>(a, b) \<Turnstile> P; b \<inter> as' = {}; relH b a h'; in_range (h', b); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', b \<union> as') \<Turnstile> R
[PROOF STEP]
apply (blast intro: models_in_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b h' as'. \<lbrakk>(a, b) \<Turnstile> P; b \<inter> as' = {}; relH b a h'; in_range (h', b); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', b \<union> as') \<Turnstile> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b h' as'. \<lbrakk>(a, b) \<Turnstile> P; b \<inter> as' = {}; relH b a h'; in_range (h', b); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', b \<union> as') \<Turnstile> R
[PROOF STEP]
fix h as h' as'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b h' as'. \<lbrakk>(a, b) \<Turnstile> P; b \<inter> as' = {}; relH b a h'; in_range (h', b); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', b \<union> as') \<Turnstile> R
[PROOF STEP]
assume "(h,as)\<Turnstile>P"
    and "as\<inter>as'={}"
    and "relH as h h'"
    and "in_range (h',as)"
    and "(h',as') \<Turnstile> Q"
[PROOF STATE]
proof (state)
this:
(h, as) \<Turnstile> P
as \<inter> as' = {}
relH as h h'
in_range (h', as)
(h', as') \<Turnstile> Q

goal (1 subgoal):
 1. \<And>a b h' as'. \<lbrakk>(a, b) \<Turnstile> P; b \<inter> as' = {}; relH b a h'; in_range (h', b); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', b \<union> as') \<Turnstile> R
[PROOF STEP]
from \<open>(h,as)\<Turnstile>P\<close> and \<open>relH as h h'\<close>
[PROOF STATE]
proof (chain)
picking this:
(h, as) \<Turnstile> P
relH as h h'
[PROOF STEP]
have "(h',as)\<Turnstile>P"
[PROOF STATE]
proof (prove)
using this:
(h, as) \<Turnstile> P
relH as h h'

goal (1 subgoal):
 1. (h', as) \<Turnstile> P
[PROOF STEP]
by (simp add: mod_relH)
[PROOF STATE]
proof (state)
this:
(h', as) \<Turnstile> P

goal (1 subgoal):
 1. \<And>a b h' as'. \<lbrakk>(a, b) \<Turnstile> P; b \<inter> as' = {}; relH b a h'; in_range (h', b); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', b \<union> as') \<Turnstile> R
[PROOF STEP]
with \<open>(h',as') \<Turnstile> Q\<close> and \<open>as\<inter>as'={}\<close>
[PROOF STATE]
proof (chain)
picking this:
(h', as') \<Turnstile> Q
as \<inter> as' = {}
(h', as) \<Turnstile> P
[PROOF STEP]
have "(h',as\<union>as')\<Turnstile>Q*P"
[PROOF STATE]
proof (prove)
using this:
(h', as') \<Turnstile> Q
as \<inter> as' = {}
(h', as) \<Turnstile> P

goal (1 subgoal):
 1. (h', as \<union> as') \<Turnstile> Q * P
[PROOF STEP]
by (metis star_assnI Int_commute Un_commute)
[PROOF STATE]
proof (state)
this:
(h', as \<union> as') \<Turnstile> Q * P

goal (1 subgoal):
 1. \<And>a b h' as'. \<lbrakk>(a, b) \<Turnstile> P; b \<inter> as' = {}; relH b a h'; in_range (h', b); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', b \<union> as') \<Turnstile> R
[PROOF STEP]
with IMP
[PROOF STATE]
proof (chain)
picking this:
Q * P \<Longrightarrow>\<^sub>A R
(h', as \<union> as') \<Turnstile> Q * P
[PROOF STEP]
show "(h',as\<union>as') \<Turnstile> R"
[PROOF STATE]
proof (prove)
using this:
Q * P \<Longrightarrow>\<^sub>A R
(h', as \<union> as') \<Turnstile> Q * P

goal (1 subgoal):
 1. (h', as \<union> as') \<Turnstile> R
[PROOF STEP]
by (blast dest: ent_fwd)
[PROOF STATE]
proof (state)
this:
(h', as \<union> as') \<Turnstile> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ent_disjI1:
  assumes "P \<or>\<^sub>A Q \<Longrightarrow>\<^sub>A R"
  shows "P \<Longrightarrow>\<^sub>A R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<or>\<^sub>A Q \<Longrightarrow>\<^sub>A R

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A R
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> P \<or>\<^sub>A Q \<longrightarrow> h \<Turnstile> R

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> R
[PROOF STEP]
by simp


[STATEMENT]
lemma ent_disjI2:
  assumes "P \<or>\<^sub>A Q \<Longrightarrow>\<^sub>A R"
  shows "Q \<Longrightarrow>\<^sub>A R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<Longrightarrow>\<^sub>A R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<or>\<^sub>A Q \<Longrightarrow>\<^sub>A R

goal (1 subgoal):
 1. Q \<Longrightarrow>\<^sub>A R
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> P \<or>\<^sub>A Q \<longrightarrow> h \<Turnstile> R

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> Q \<longrightarrow> h \<Turnstile> R
[PROOF STEP]
by simp


[STATEMENT]
lemma ent_disjI1_direct[simp]: "A \<Longrightarrow>\<^sub>A A \<or>\<^sub>A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A A \<or>\<^sub>A B
[PROOF STEP]
by (simp add: entails_def)


[STATEMENT]
lemma ent_disjI2_direct[simp]: "B \<Longrightarrow>\<^sub>A A \<or>\<^sub>A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<Longrightarrow>\<^sub>A A \<or>\<^sub>A B
[PROOF STEP]
by (simp add: entails_def)


[STATEMENT]
lemma ent_disjE: "\<lbrakk> A\<Longrightarrow>\<^sub>AC; B\<Longrightarrow>\<^sub>AC \<rbrakk> \<Longrightarrow> A\<or>\<^sub>AB \<Longrightarrow>\<^sub>AC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A C; B \<Longrightarrow>\<^sub>A C\<rbrakk> \<Longrightarrow> A \<or>\<^sub>A B \<Longrightarrow>\<^sub>A C
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>h. h \<Turnstile> A \<longrightarrow> h \<Turnstile> C; \<forall>h. h \<Turnstile> B \<longrightarrow> h \<Turnstile> C\<rbrakk> \<Longrightarrow> \<forall>h. h \<Turnstile> A \<or>\<^sub>A B \<longrightarrow> h \<Turnstile> C
[PROOF STEP]
by auto


[STATEMENT]
lemma ent_conjI: "\<lbrakk> A\<Longrightarrow>\<^sub>AB; A\<Longrightarrow>\<^sub>AC \<rbrakk> \<Longrightarrow> A \<Longrightarrow>\<^sub>A B \<and>\<^sub>A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A B; A \<Longrightarrow>\<^sub>A C\<rbrakk> \<Longrightarrow> A \<Longrightarrow>\<^sub>A B \<and>\<^sub>A C
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>h. h \<Turnstile> A \<longrightarrow> h \<Turnstile> B; \<forall>h. h \<Turnstile> A \<longrightarrow> h \<Turnstile> C\<rbrakk> \<Longrightarrow> \<forall>h. h \<Turnstile> A \<longrightarrow> h \<Turnstile> B \<and>\<^sub>A C
[PROOF STEP]
by (auto simp: mod_and_dist)


[STATEMENT]
lemma ent_conjE1: "\<lbrakk>A\<Longrightarrow>\<^sub>AC\<rbrakk> \<Longrightarrow> A\<and>\<^sub>AB\<Longrightarrow>\<^sub>AC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A C \<Longrightarrow> A \<and>\<^sub>A B \<Longrightarrow>\<^sub>A C
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> A \<longrightarrow> h \<Turnstile> C \<Longrightarrow> \<forall>h. h \<Turnstile> A \<and>\<^sub>A B \<longrightarrow> h \<Turnstile> C
[PROOF STEP]
by (auto simp: mod_and_dist)


[STATEMENT]
lemma ent_conjE2: "\<lbrakk>B\<Longrightarrow>\<^sub>AC\<rbrakk> \<Longrightarrow> A\<and>\<^sub>AB\<Longrightarrow>\<^sub>AC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<Longrightarrow>\<^sub>A C \<Longrightarrow> A \<and>\<^sub>A B \<Longrightarrow>\<^sub>A C
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> B \<longrightarrow> h \<Turnstile> C \<Longrightarrow> \<forall>h. h \<Turnstile> A \<and>\<^sub>A B \<longrightarrow> h \<Turnstile> C
[PROOF STEP]
by (auto simp: mod_and_dist)


[STATEMENT]
lemma star_or_dist1:
  "(A \<or>\<^sub>A B)*C = (A*C \<or>\<^sub>A B*C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<or>\<^sub>A B) * C = A * C \<or>\<^sub>A B * C
[PROOF STEP]
apply (rule ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (A \<or>\<^sub>A B) * C \<Longrightarrow>\<^sub>A A * C \<or>\<^sub>A B * C
 2. A * C \<or>\<^sub>A B * C \<Longrightarrow>\<^sub>A (A \<or>\<^sub>A B) * C
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>h. h \<Turnstile> (A \<or>\<^sub>A B) * C \<longrightarrow> h \<Turnstile> A * C \<or>\<^sub>A B * C
 2. \<forall>h. h \<Turnstile> A * C \<or>\<^sub>A B * C \<longrightarrow> h \<Turnstile> (A \<or>\<^sub>A B) * C
[PROOF STEP]
by (auto simp add: mod_star_conv)


[STATEMENT]
lemma star_or_dist2:
  "C*(A \<or>\<^sub>A B) = (C*A \<or>\<^sub>A C*B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C * (A \<or>\<^sub>A B) = C * A \<or>\<^sub>A C * B
[PROOF STEP]
apply (rule ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. C * (A \<or>\<^sub>A B) \<Longrightarrow>\<^sub>A C * A \<or>\<^sub>A C * B
 2. C * A \<or>\<^sub>A C * B \<Longrightarrow>\<^sub>A C * (A \<or>\<^sub>A B)
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>h. h \<Turnstile> C * (A \<or>\<^sub>A B) \<longrightarrow> h \<Turnstile> C * A \<or>\<^sub>A C * B
 2. \<forall>h. h \<Turnstile> C * A \<or>\<^sub>A C * B \<longrightarrow> h \<Turnstile> C * (A \<or>\<^sub>A B)
[PROOF STEP]
by (auto simp add: mod_star_conv)


[STATEMENT]
lemma ent_disjI1': "A\<Longrightarrow>\<^sub>AB \<Longrightarrow> A\<Longrightarrow>\<^sub>AB\<or>\<^sub>AC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A B \<Longrightarrow> A \<Longrightarrow>\<^sub>A B \<or>\<^sub>A C
[PROOF STEP]
by (auto simp: entails_def star_or_dist)


[STATEMENT]
lemma ent_disjI2': "A\<Longrightarrow>\<^sub>AC \<Longrightarrow> A\<Longrightarrow>\<^sub>AB\<or>\<^sub>AC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A C \<Longrightarrow> A \<Longrightarrow>\<^sub>A B \<or>\<^sub>A C
[PROOF STEP]
by (auto simp: entails_def star_or_dist)


[STATEMENT]
lemma triv_exI[simp, intro!]: "Q x \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax. Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q x \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax. Q x
[PROOF STEP]
by (meson ent_ex_postI ent_refl)


[STATEMENT]
lemma enttI: "A\<Longrightarrow>\<^sub>AB*true \<Longrightarrow> A\<Longrightarrow>\<^sub>tB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A \<Longrightarrow>\<^sub>t B
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
.


[STATEMENT]
lemma enttD: "A\<Longrightarrow>\<^sub>tB \<Longrightarrow> A\<Longrightarrow>\<^sub>AB*true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t B \<Longrightarrow> A \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
.


[STATEMENT]
lemma entt_trans:
  "entailst A B \<Longrightarrow> entailst B C \<Longrightarrow> entailst A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>t B; B \<Longrightarrow>\<^sub>t C\<rbrakk> \<Longrightarrow> A \<Longrightarrow>\<^sub>t C
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A B * true; B \<Longrightarrow>\<^sub>A C * true\<rbrakk> \<Longrightarrow> A \<Longrightarrow>\<^sub>A C * true
[PROOF STEP]
apply (erule ent_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<Longrightarrow>\<^sub>A C * true \<Longrightarrow> B * true \<Longrightarrow>\<^sub>A C * true
[PROOF STEP]
by (metis assn_times_assoc ent_star_mono ent_true merge_true_star)


[STATEMENT]
lemma entt_refl[simp, intro!]: "entailst A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t A
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A A * true
[PROOF STEP]
by (simp add: entailsI mod_star_trueI)


[STATEMENT]
lemma entt_true[simp, intro!]:
  "entailst A true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t true
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A true * true
[PROOF STEP]
by simp


[STATEMENT]
lemma entt_emp[simp, intro!]:
  "entailst A emp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t emp
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A emp * true
[PROOF STEP]
by simp


[STATEMENT]
lemma entt_star_true_simp[simp]:
  "entailst A (B*true) \<longleftrightarrow> entailst A B"
  "entailst (A*true) B \<longleftrightarrow> entailst A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<Longrightarrow>\<^sub>t B * true) = (A \<Longrightarrow>\<^sub>t B) &&& (A * true \<Longrightarrow>\<^sub>t B) = (A \<Longrightarrow>\<^sub>t B)
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<Longrightarrow>\<^sub>A B * true * true) = (A \<Longrightarrow>\<^sub>A B * true) &&& (A * true \<Longrightarrow>\<^sub>A B * true) = (A \<Longrightarrow>\<^sub>A B * true)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<Longrightarrow>\<^sub>A B * true * true) = (A \<Longrightarrow>\<^sub>A B * true)
[PROOF STEP]
by (auto simp: assn_times_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A * true \<Longrightarrow>\<^sub>A B * true) = (A \<Longrightarrow>\<^sub>A B * true)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A * true \<Longrightarrow>\<^sub>A B * true) = (A \<Longrightarrow>\<^sub>A B * true)
[PROOF STEP]
apply (intro iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A * true \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A \<Longrightarrow>\<^sub>A B * true
 2. A \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A * true \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * true \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
using entails_def mod_star_trueI
[PROOF STATE]
proof (prove)
using this:
?P \<Longrightarrow>\<^sub>A ?Q \<equiv> \<forall>h. h \<Turnstile> ?P \<longrightarrow> h \<Turnstile> ?Q
?h \<Turnstile> ?P \<Longrightarrow> ?h \<Turnstile> ?P * true

goal (1 subgoal):
 1. A * true \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A * true \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>A B * true \<Longrightarrow> A * true \<Longrightarrow>\<^sub>A B * true
[PROOF STEP]
by (metis assn_times_assoc ent_refl ent_star_mono merge_true_star)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma entt_star_mono: "\<lbrakk>entailst A B; entailst C D\<rbrakk> \<Longrightarrow> entailst (A*C) (B*D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>t B; C \<Longrightarrow>\<^sub>t D\<rbrakk> \<Longrightarrow> A * C \<Longrightarrow>\<^sub>t B * D
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A B * true; C \<Longrightarrow>\<^sub>A D * true\<rbrakk> \<Longrightarrow> A * C \<Longrightarrow>\<^sub>A B * D * true
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A B * true; C \<Longrightarrow>\<^sub>A D * true\<rbrakk> \<Longrightarrow> A * C \<Longrightarrow>\<^sub>A B * D * true
[PROOF STEP]
assume a1: "A \<Longrightarrow>\<^sub>A B * true"
[PROOF STATE]
proof (state)
this:
A \<Longrightarrow>\<^sub>A B * true

goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A B * true; C \<Longrightarrow>\<^sub>A D * true\<rbrakk> \<Longrightarrow> A * C \<Longrightarrow>\<^sub>A B * D * true
[PROOF STEP]
assume "C \<Longrightarrow>\<^sub>A D * true"
[PROOF STATE]
proof (state)
this:
C \<Longrightarrow>\<^sub>A D * true

goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A B * true; C \<Longrightarrow>\<^sub>A D * true\<rbrakk> \<Longrightarrow> A * C \<Longrightarrow>\<^sub>A B * D * true
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<Longrightarrow>\<^sub>A D * true
[PROOF STEP]
have "A * C \<Longrightarrow>\<^sub>A true * B * (true * D)"
[PROOF STATE]
proof (prove)
using this:
C \<Longrightarrow>\<^sub>A D * true

goal (1 subgoal):
 1. A * C \<Longrightarrow>\<^sub>A true * B * (true * D)
[PROOF STEP]
using a1 assn_times_comm ent_star_mono
[PROOF STATE]
proof (prove)
using this:
C \<Longrightarrow>\<^sub>A D * true
A \<Longrightarrow>\<^sub>A B * true
?P * ?Q = ?Q * ?P
\<lbrakk>?P \<Longrightarrow>\<^sub>A ?P'; ?Q \<Longrightarrow>\<^sub>A ?Q'\<rbrakk> \<Longrightarrow> ?P * ?Q \<Longrightarrow>\<^sub>A ?P' * ?Q'

goal (1 subgoal):
 1. A * C \<Longrightarrow>\<^sub>A true * B * (true * D)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
A * C \<Longrightarrow>\<^sub>A true * B * (true * D)

goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>A B * true; C \<Longrightarrow>\<^sub>A D * true\<rbrakk> \<Longrightarrow> A * C \<Longrightarrow>\<^sub>A B * D * true
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A * C \<Longrightarrow>\<^sub>A true * B * (true * D)
[PROOF STEP]
show "A * C \<Longrightarrow>\<^sub>A B * D * true"
[PROOF STATE]
proof (prove)
using this:
A * C \<Longrightarrow>\<^sub>A true * B * (true * D)

goal (1 subgoal):
 1. A * C \<Longrightarrow>\<^sub>A B * D * true
[PROOF STEP]
by (simp add: ab_semigroup_mult_class.mult.left_commute assn_times_comm)
[PROOF STATE]
proof (state)
this:
A * C \<Longrightarrow>\<^sub>A B * D * true

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma entt_frame_fwd:
  assumes "entailst P Q"
  assumes "entailst A (P*F)"
  assumes "entailst (Q*F) B"
  shows "entailst A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>t Q
A \<Longrightarrow>\<^sub>t P * F
Q * F \<Longrightarrow>\<^sub>t B

goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t B
[PROOF STEP]
by (metis entt_refl entt_star_mono entt_trans)


[STATEMENT]
lemma enttI_true: "P*true \<Longrightarrow>\<^sub>A Q*true \<Longrightarrow> P\<Longrightarrow>\<^sub>tQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * true \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>t Q
[PROOF STEP]
by (drule enttI) simp


[STATEMENT]
lemma entt_def_true: "(P\<Longrightarrow>\<^sub>tQ) \<equiv> (P*true \<Longrightarrow>\<^sub>A Q*true)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>t Q \<equiv> P * true \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
unfolding entailst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q * true \<equiv> P * true \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A Q * true) = (P * true \<Longrightarrow>\<^sub>A Q * true)
[PROOF STEP]
using entailst_def entt_star_true_simp(2)
[PROOF STATE]
proof (prove)
using this:
?A \<Longrightarrow>\<^sub>t ?B \<equiv> ?A \<Longrightarrow>\<^sub>A ?B * true
(?A * true \<Longrightarrow>\<^sub>t ?B) = (?A \<Longrightarrow>\<^sub>t ?B)

goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A Q * true) = (P * true \<Longrightarrow>\<^sub>A Q * true)
[PROOF STEP]
by auto


[STATEMENT]
lemma ent_imp_entt: "P\<Longrightarrow>\<^sub>AQ \<Longrightarrow> P\<Longrightarrow>\<^sub>tQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P \<Longrightarrow>\<^sub>t Q
[PROOF STEP]
apply (rule enttI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
apply (erule ent_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
by (simp add: entailsI mod_star_trueI)


[STATEMENT]
lemma entt_disjI1_direct[simp]: "A \<Longrightarrow>\<^sub>t A \<or>\<^sub>A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t A \<or>\<^sub>A B
[PROOF STEP]
by (rule ent_imp_entt[OF ent_disjI1_direct])


[STATEMENT]
lemma entt_disjI2_direct[simp]: "B \<Longrightarrow>\<^sub>t A \<or>\<^sub>A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<Longrightarrow>\<^sub>t A \<or>\<^sub>A B
[PROOF STEP]
by (rule ent_imp_entt[OF ent_disjI2_direct])


[STATEMENT]
lemma entt_disjI1': "A\<Longrightarrow>\<^sub>tB \<Longrightarrow> A\<Longrightarrow>\<^sub>tB\<or>\<^sub>AC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t B \<Longrightarrow> A \<Longrightarrow>\<^sub>t B \<or>\<^sub>A C
[PROOF STEP]
by (auto simp: entailst_def entails_def star_or_dist)


[STATEMENT]
lemma entt_disjI2': "A\<Longrightarrow>\<^sub>tC \<Longrightarrow> A\<Longrightarrow>\<^sub>tB\<or>\<^sub>AC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Longrightarrow>\<^sub>t C \<Longrightarrow> A \<Longrightarrow>\<^sub>t B \<or>\<^sub>A C
[PROOF STEP]
by (auto simp: entailst_def entails_def star_or_dist)


[STATEMENT]
lemma entt_disjE: "\<lbrakk> A\<Longrightarrow>\<^sub>tM; B\<Longrightarrow>\<^sub>tM \<rbrakk> \<Longrightarrow> A\<or>\<^sub>AB \<Longrightarrow>\<^sub>t M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>t M; B \<Longrightarrow>\<^sub>t M\<rbrakk> \<Longrightarrow> A \<or>\<^sub>A B \<Longrightarrow>\<^sub>t M
[PROOF STEP]
using ent_disjE enttD enttI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<Longrightarrow>\<^sub>A ?C; ?B \<Longrightarrow>\<^sub>A ?C\<rbrakk> \<Longrightarrow> ?A \<or>\<^sub>A ?B \<Longrightarrow>\<^sub>A ?C
?A \<Longrightarrow>\<^sub>t ?B \<Longrightarrow> ?A \<Longrightarrow>\<^sub>A ?B * true
?A \<Longrightarrow>\<^sub>A ?B * true \<Longrightarrow> ?A \<Longrightarrow>\<^sub>t ?B

goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow>\<^sub>t M; B \<Longrightarrow>\<^sub>t M\<rbrakk> \<Longrightarrow> A \<or>\<^sub>A B \<Longrightarrow>\<^sub>t M
[PROOF STEP]
by blast


[STATEMENT]
lemma entt_disjD1: "A\<or>\<^sub>AB\<Longrightarrow>\<^sub>tC \<Longrightarrow> A\<Longrightarrow>\<^sub>tC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<or>\<^sub>A B \<Longrightarrow>\<^sub>t C \<Longrightarrow> A \<Longrightarrow>\<^sub>t C
[PROOF STEP]
using entt_disjI1_direct entt_trans
[PROOF STATE]
proof (prove)
using this:
?A \<Longrightarrow>\<^sub>t ?A \<or>\<^sub>A ?B
\<lbrakk>?A \<Longrightarrow>\<^sub>t ?B; ?B \<Longrightarrow>\<^sub>t ?C\<rbrakk> \<Longrightarrow> ?A \<Longrightarrow>\<^sub>t ?C

goal (1 subgoal):
 1. A \<or>\<^sub>A B \<Longrightarrow>\<^sub>t C \<Longrightarrow> A \<Longrightarrow>\<^sub>t C
[PROOF STEP]
by blast


[STATEMENT]
lemma entt_disjD2: "A\<or>\<^sub>AB\<Longrightarrow>\<^sub>tC \<Longrightarrow> B\<Longrightarrow>\<^sub>tC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<or>\<^sub>A B \<Longrightarrow>\<^sub>t C \<Longrightarrow> B \<Longrightarrow>\<^sub>t C
[PROOF STEP]
using entt_disjI2_direct entt_trans
[PROOF STATE]
proof (prove)
using this:
?B \<Longrightarrow>\<^sub>t ?A \<or>\<^sub>A ?B
\<lbrakk>?A \<Longrightarrow>\<^sub>t ?B; ?B \<Longrightarrow>\<^sub>t ?C\<rbrakk> \<Longrightarrow> ?A \<Longrightarrow>\<^sub>t ?C

goal (1 subgoal):
 1. A \<or>\<^sub>A B \<Longrightarrow>\<^sub>t C \<Longrightarrow> B \<Longrightarrow>\<^sub>t C
[PROOF STEP]
by blast


[STATEMENT]
lemma preciseI[intro?]:
  assumes "\<And>a a' h p F F'. h \<Turnstile> R a p * F \<and>\<^sub>A R a' p * F' \<Longrightarrow> a = a'"
  shows "precise R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> R ?a ?p * ?F \<and>\<^sub>A R ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'

goal (1 subgoal):
 1. precise R
[PROOF STEP]
unfolding precise_def
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> R ?a ?p * ?F \<and>\<^sub>A R ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'

goal (1 subgoal):
 1. \<forall>a a' h p F F'. h \<Turnstile> R a p * F \<and>\<^sub>A R a' p * F' \<longrightarrow> a = a'
[PROOF STEP]
by blast


[STATEMENT]
lemma preciseD:
  assumes "precise R"
  assumes "h \<Turnstile> R a p * F \<and>\<^sub>A R a' p * F'"
  shows "a=a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = a'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
precise R
h \<Turnstile> R a p * F \<and>\<^sub>A R a' p * F'

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
unfolding precise_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a a' h p F F'. h \<Turnstile> R a p * F \<and>\<^sub>A R a' p * F' \<longrightarrow> a = a'
h \<Turnstile> R a p * F \<and>\<^sub>A R a' p * F'

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
by blast


[STATEMENT]
lemma preciseD':
  assumes "precise R"
  assumes "h \<Turnstile> R a p * F"
  assumes "h \<Turnstile> R a' p * F'"
  shows "a=a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = a'
[PROOF STEP]
apply (rule preciseD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. precise ?R
 2. ?h \<Turnstile> ?R a ?p * ?F \<and>\<^sub>A ?R a' ?p * ?F'
[PROOF STEP]
apply (rule assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?h \<Turnstile> R a ?p * ?F \<and>\<^sub>A R a' ?p * ?F'
[PROOF STEP]
apply (simp only: mod_and_dist)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?h \<Turnstile> R a ?p * ?F \<and> ?h \<Turnstile> R a' ?p * ?F'
[PROOF STEP]
apply (blast intro: assms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma precise_extr_pure[simp]:
  "precise (\<lambda>x y. \<up>P * R x y) \<longleftrightarrow> (P \<longrightarrow> precise R)"
  "precise (\<lambda>x y. R x y * \<up>P) \<longleftrightarrow> (P \<longrightarrow> precise R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise (\<lambda>x y. \<up> P * R x y) = (P \<longrightarrow> precise R) &&& precise (\<lambda>x y. R x y * \<up> P) = (P \<longrightarrow> precise R)
[PROOF STEP]
apply (cases P, (auto intro!: preciseI) [2])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sngr_prec: "precise (\<lambda>x p. p\<mapsto>\<^sub>rx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise (\<lambda>x p. p \<mapsto>\<^sub>r x)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> p \<mapsto>\<^sub>r a * F \<and>\<^sub>A p \<mapsto>\<^sub>r a' * F' \<Longrightarrow> a = a'
[PROOF STEP]
apply (clarsimp simp: mod_and_dist)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa b p F F'. \<lbrakk>(aa, b) \<Turnstile> p \<mapsto>\<^sub>r a * F; (aa, b) \<Turnstile> p \<mapsto>\<^sub>r a' * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
unfolding sngr_assn_def times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa b p F F'. \<lbrakk>(aa, b) \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p a))) (Rep_assn F)); (aa, b) \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p a'))) (Rep_assn F'))\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa b p F F'. \<lbrakk>\<exists>as2. b = insert (addr_of_ref p) as2 \<and> addr_of_ref p \<notin> as2 \<and> Ref_Time.get aa p = a \<and> addr_of_ref p < lim aa \<and> (aa, as2) \<Turnstile> F; \<exists>as2. b = insert (addr_of_ref p) as2 \<and> addr_of_ref p \<notin> as2 \<and> Ref_Time.get aa p = a' \<and> addr_of_ref p < lim aa \<and> (aa, as2) \<Turnstile> F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma snga_prec: "precise (\<lambda>x p. p\<mapsto>\<^sub>ax)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise (\<lambda>x p. p \<mapsto>\<^sub>a x)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> p \<mapsto>\<^sub>a a * F \<and>\<^sub>A p \<mapsto>\<^sub>a a' * F' \<Longrightarrow> a = a'
[PROOF STEP]
apply (clarsimp simp: mod_and_dist)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa b p F F'. \<lbrakk>(aa, b) \<Turnstile> p \<mapsto>\<^sub>a a * F; (aa, b) \<Turnstile> p \<mapsto>\<^sub>a a' * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
unfolding snga_assn_def times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa b p F F'. \<lbrakk>(aa, b) \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (snga_assn_raw p a))) (Rep_assn F)); (aa, b) \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (snga_assn_raw p a'))) (Rep_assn F'))\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa b p F F'. \<lbrakk>\<exists>as2. b = insert (addr_of_array p) as2 \<and> addr_of_array p \<notin> as2 \<and> Array_Time.get aa p = a \<and> addr_of_array p < lim aa \<and> (aa, as2) \<Turnstile> F; \<exists>as2. b = insert (addr_of_array p) as2 \<and> addr_of_array p \<notin> as2 \<and> Array_Time.get aa p = a' \<and> addr_of_array p < lim aa \<and> (aa, as2) \<Turnstile> F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_coprime_dvd_cong:
  "(\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r s) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. g r s)"
  if "coprime a b" "\<And>r s. coprime r s \<Longrightarrow> r dvd a \<Longrightarrow> s dvd b \<Longrightarrow> f r s = g r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r s) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. g r s)
[PROOF STEP]
using refl
[PROOF STATE]
proof (prove)
using this:
?t = ?t

goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r s) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. g r s)
[PROOF STEP]
proof (rule sum.cong, rule sum.cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> {r. r dvd a}; xa \<in> {s. s dvd b}\<rbrakk> \<Longrightarrow> f x xa = g x xa
[PROOF STEP]
fix r s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> {r. r dvd a}; xa \<in> {s. s dvd b}\<rbrakk> \<Longrightarrow> f x xa = g x xa
[PROOF STEP]
assume "r \<in> {r. r dvd a}" and "s \<in> {s. s dvd b}"
[PROOF STATE]
proof (state)
this:
r \<in> {r. r dvd a}
s \<in> {s. s dvd b}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> {r. r dvd a}; xa \<in> {s. s dvd b}\<rbrakk> \<Longrightarrow> f x xa = g x xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> {r. r dvd a}
s \<in> {s. s dvd b}
[PROOF STEP]
have "r dvd a" and "s dvd b"
[PROOF STATE]
proof (prove)
using this:
r \<in> {r. r dvd a}
s \<in> {s. s dvd b}

goal (1 subgoal):
 1. r dvd a &&& s dvd b
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
r dvd a
s dvd b

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> {r. r dvd a}; xa \<in> {s. s dvd b}\<rbrakk> \<Longrightarrow> f x xa = g x xa
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r dvd a
s dvd b

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> {r. r dvd a}; xa \<in> {s. s dvd b}\<rbrakk> \<Longrightarrow> f x xa = g x xa
[PROOF STEP]
from \<open>coprime a b\<close>
[PROOF STATE]
proof (chain)
picking this:
coprime a b
[PROOF STEP]
have "coprime r s"
[PROOF STATE]
proof (prove)
using this:
coprime a b

goal (1 subgoal):
 1. coprime r s
[PROOF STEP]
using \<open>r dvd a\<close> \<open>s dvd b\<close>
[PROOF STATE]
proof (prove)
using this:
coprime a b
r dvd a
s dvd b

goal (1 subgoal):
 1. coprime r s
[PROOF STEP]
by (auto intro: coprime_imp_coprime dvd_trans)
[PROOF STATE]
proof (state)
this:
coprime r s

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> {r. r dvd a}; xa \<in> {s. s dvd b}\<rbrakk> \<Longrightarrow> f x xa = g x xa
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r dvd a
s dvd b
coprime r s
[PROOF STEP]
show "f r s = g r s"
[PROOF STATE]
proof (prove)
using this:
r dvd a
s dvd b
coprime r s

goal (1 subgoal):
 1. f r s = g r s
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
r dvd a
s dvd b
coprime r s
coprime a b
\<lbrakk>coprime ?r ?s; ?r dvd a; ?s dvd b\<rbrakk> \<Longrightarrow> f ?r ?s = g ?r ?s

goal (1 subgoal):
 1. f r s = g r s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f r s = g r s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_divisors_code:
  assumes "n > (0::nat)"
  shows   "(\<Sum>d | d dvd n. f d) =
             fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
have "(\<lambda>d acc. if d dvd n then f d + acc else acc) = (\<lambda>d acc. (if d dvd n then f d else 0) + acc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>d acc. if d dvd n then f d + acc else acc) = (\<lambda>d. (+) (if d dvd n then f d else (0::'a)))
[PROOF STEP]
by (simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>d acc. if d dvd n then f d + acc else acc) = (\<lambda>d. (+) (if d dvd n then f d else (0::'a)))

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
hence "fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n 0 =
           fold_atLeastAtMost_nat (\<lambda>d acc. (if d dvd n then f d else 0) + acc) 1 n 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>d acc. if d dvd n then f d + acc else acc) = (\<lambda>d. (+) (if d dvd n then f d else (0::'a)))

goal (1 subgoal):
 1. fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a) = fold_atLeastAtMost_nat (\<lambda>d. (+) (if d dvd n then f d else (0::'a))) 1 n (0::'a)
[PROOF STEP]
by (simp only: )
[PROOF STATE]
proof (state)
this:
fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a) = fold_atLeastAtMost_nat (\<lambda>d. (+) (if d dvd n then f d else (0::'a))) 1 n (0::'a)

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a) = fold_atLeastAtMost_nat (\<lambda>d. (+) (if d dvd n then f d else (0::'a))) 1 n (0::'a)

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
have "\<dots> = (\<Sum>d = 1..n. if d dvd n then f d else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_atLeastAtMost_nat (\<lambda>d. (+) (if d dvd n then f d else (0::'a))) 1 n (0::'a) = (\<Sum>d = 1..n. if d dvd n then f d else (0::'a))
[PROOF STEP]
by (rule sum_atLeastAtMost_code [symmetric])
[PROOF STATE]
proof (state)
this:
fold_atLeastAtMost_nat (\<lambda>d. (+) (if d dvd n then f d else (0::'a))) 1 n (0::'a) = (\<Sum>d = 1..n. if d dvd n then f d else (0::'a))

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fold_atLeastAtMost_nat (\<lambda>d. (+) (if d dvd n then f d else (0::'a))) 1 n (0::'a) = (\<Sum>d = 1..n. if d dvd n then f d else (0::'a))

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "\<dots> = (\<Sum>d | d dvd n. f d)"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>d = 1..n. if d dvd n then f d else (0::'a)) = (\<Sum>d | d dvd n. f d)
[PROOF STEP]
by (intro sum.mono_neutral_cong_right) (auto elim: dvdE dest: dvd_imp_le)
[PROOF STATE]
proof (state)
this:
(\<Sum>d = 1..n. if d dvd n then f d else (0::'a)) = (\<Sum>d | d dvd n. f d)

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a) = (\<Sum>d | d dvd n. f d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a) = (\<Sum>d | d dvd n. f d)

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. f d) = fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d + acc else acc) 1 n (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_code [code]:
  "dirichlet_prod f g n = (if n = 0 then 0 else
     fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d * g (n div d) + acc else acc) 1 n 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g n = (if n = 0 then 0::'a else fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d * g (n div d) + acc else acc) 1 n (0::'a))
[PROOF STEP]
unfolding dirichlet_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d * g (n div d)) = (if n = 0 then 0::'a else fold_atLeastAtMost_nat (\<lambda>d acc. if d dvd n then f d * g (n div d) + acc else acc) 1 n (0::'a))
[PROOF STEP]
by (simp add: sum_divisors_code)


[STATEMENT]
lemma dirichlet_prod_0 [simp]: "dirichlet_prod f g 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g 0 = (0::'a)
[PROOF STEP]
by (simp add: dirichlet_prod_def)


[STATEMENT]
lemma dirichlet_prod_Suc_0 [simp]: "dirichlet_prod f g (Suc 0) = f (Suc 0) * g (Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g (Suc 0) = f (Suc 0) * g (Suc 0)
[PROOF STEP]
by (simp add: dirichlet_prod_def)


[STATEMENT]
lemma dirichlet_prod_cong [cong]:
  assumes "(\<And>n. n > 0 \<Longrightarrow> f n = f' n)" "(\<And>n. n > 0 \<Longrightarrow> g n = g' n)"
  shows   "dirichlet_prod f g = dirichlet_prod f' g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g = dirichlet_prod f' g'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dirichlet_prod f g x = dirichlet_prod f' g' x
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dirichlet_prod f g x = dirichlet_prod f' g' x
[PROOF STEP]
show "dirichlet_prod f g n = dirichlet_prod f' g' n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g n = dirichlet_prod f' g' n
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod f' g' n
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod f' g' n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod f' g' n
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod f' g' n
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < ?n \<Longrightarrow> f ?n = f' ?n
0 < ?n \<Longrightarrow> g ?n = g' ?n
n \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> f ?n = f' ?n
0 < ?n \<Longrightarrow> g ?n = g' ?n
n \<noteq> 0

goal (1 subgoal):
 1. dirichlet_prod f g n = dirichlet_prod f' g' n
[PROOF STEP]
unfolding dirichlet_prod_def
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> f ?n = f' ?n
0 < ?n \<Longrightarrow> g ?n = g' ?n
n \<noteq> 0

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>d | d dvd n. f' d * g' (n div d))
[PROOF STEP]
by (intro ext sum.cong refl) (auto elim!: dvdE)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = dirichlet_prod f' g' n

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod f' g' n
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = dirichlet_prod f' g' n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_altdef1:
  "dirichlet_prod f g = (\<lambda>n. \<Sum>d | d dvd n. f (n div d) * g d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g = (\<lambda>n. \<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
show "dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
hence "dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div (n div d)) * g (n div d))"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div (n div d)) * g (n div d))
[PROOF STEP]
unfolding dirichlet_prod_def
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>d | d dvd n. f (n div (n div d)) * g (n div d))
[PROOF STEP]
by (intro sum.cong refl) (auto elim!: dvdE)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div (n div d)) * g (n div d))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div (n div d)) * g (n div d))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have "\<dots> = (\<Sum>d | d dvd n. f (n div d) * g d)"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f (n div (n div d)) * g (n div d)) = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
by (intro sum.reindex_bij_witness[of _ "(div) n" "(div) n"]) (auto elim!: dvdE)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. f (n div (n div d)) * g (n div d)) = (\<Sum>d | d dvd n. f (n div d) * g d)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)

goal (1 subgoal):
 1. dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = (\<Sum>d | d dvd n. f (n div d) * g d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_altdef2:
  "dirichlet_prod f g = (\<lambda>n. \<Sum>(r,d) | r * d = n. f r * g d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g = (\<lambda>n. \<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
show "dirichlet_prod f g n = (\<Sum>(r,d) | r * d = n. f r * g d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
have "(\<lambda>n::nat. (0, n)) ` UNIV \<subseteq> {(r,d). r * d = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (Pair 0) \<subseteq> {(r, d). r * d = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range (Pair 0) \<subseteq> {(r, d). r * d = 0}

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
range (Pair 0) \<subseteq> {(r, d). r * d = 0}

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
have "\<not>finite ((\<lambda>n::nat. (0, n)) ` UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (range (Pair (0::'b)))
[PROOF STEP]
by (subst finite_image_iff) (auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
infinite (range (Pair (0::?'b1)))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
range (Pair 0) \<subseteq> {(r, d). r * d = 0}
infinite (range (Pair (0::?'b1)))
[PROOF STEP]
have "infinite {(r,d). r * d = (0::nat)}"
[PROOF STATE]
proof (prove)
using this:
range (Pair 0) \<subseteq> {(r, d). r * d = 0}
infinite (range (Pair (0::?'b1)))

goal (1 subgoal):
 1. infinite {(r, d). r * d = 0}
[PROOF STEP]
by (blast dest: finite_subset)
[PROOF STATE]
proof (state)
this:
infinite {(r, d). r * d = 0}

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
n = 0
infinite {(r, d). r * d = 0}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0
infinite {(r, d). r * d = 0}

goal (1 subgoal):
 1. dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
have "(\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>r | r dvd n. (\<Sum>d | d = n div r. f r * g d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>r | r dvd n. \<Sum>d | d = n div r. f r * g d)
[PROOF STEP]
by (intro sum.cong refl) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>r | r dvd n. \<Sum>d | d = n div r. f r * g d)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>r | r dvd n. \<Sum>d | d = n div r. f r * g d)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have "\<dots> = (\<Sum>(r,d)\<in>(SIGMA x:{r. r dvd n}. {d. d = n div x}). f r * g d)"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (\<Sum>r | r dvd n. \<Sum>d | d = n div r. f r * g d) = (\<Sum>(r, d)\<in>(SIGMA x:{r. r dvd n}. {d. d = n div x}). f r * g d)
[PROOF STEP]
by (intro sum.Sigma) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd n. \<Sum>d | d = n div r. f r * g d) = (\<Sum>(r, d)\<in>(SIGMA x:{r. r dvd n}. {d. d = n div x}). f r * g d)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd n. \<Sum>d | d = n div r. f r * g d) = (\<Sum>(r, d)\<in>(SIGMA x:{r. r dvd n}. {d. d = n div x}). f r * g d)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have "(SIGMA x:{r. r dvd n}. {d. d = n div x}) = {(r,d). r * d = n}"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (SIGMA x:{r. r dvd n}. {d. d = n div x}) = {(r, d). r * d = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(SIGMA x:{r. r dvd n}. {d. d = n div x}) = {(r, d). r * d = n}

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>a\<in>{(r, d). r * d = n}. case a of (r, d) \<Rightarrow> f r * g d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d | d dvd n. f d * g (n div d)) = (\<Sum>a\<in>{(r, d). r * d = n}. case a of (r, d) \<Rightarrow> f r * g d)

goal (1 subgoal):
 1. dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)
[PROOF STEP]
by (simp add: dirichlet_prod_def)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_commutes:
  "dirichlet_prod (f :: nat \<Rightarrow> 'a :: comm_semiring_0) g = dirichlet_prod g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g = dirichlet_prod g f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dirichlet_prod f g x = dirichlet_prod g f x
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dirichlet_prod f g x = dirichlet_prod g f x
[PROOF STEP]
show "dirichlet_prod f g n = dirichlet_prod g f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f g n = dirichlet_prod g f n
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod g f n
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod g f n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod g f n
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod g f n
[PROOF STEP]
have "(\<Sum>(r,d) | r * d = n. f r * g d) = (\<Sum>(d,r) | r * d = n. f r * g d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d) = (\<Sum>(d, r)\<in>{(d, r). r * d = n}. f r * g d)
[PROOF STEP]
by (rule sum.reindex_bij_witness [of _ "\<lambda>(x,y). (y,x)" "\<lambda>(x,y). (y,x)"]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d) = (\<Sum>(d, r)\<in>{(d, r). r * d = n}. f r * g d)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod g f n
 2. n \<noteq> 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod g f n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(r, d)\<in>{(r, d). r * d = n}. f r * g d) = (\<Sum>(d, r)\<in>{(d, r). r * d = n}. f r * g d)

goal (1 subgoal):
 1. dirichlet_prod f g n = dirichlet_prod g f n
[PROOF STEP]
by (simp add: dirichlet_prod_altdef2 mult.commute)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = dirichlet_prod g f n

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> dirichlet_prod f g n = dirichlet_prod g f n
[PROOF STEP]
qed (simp add: dirichlet_prod_def)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f g n = dirichlet_prod g f n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_divisors_nat': "n > (0 :: nat) \<Longrightarrow> finite {(a,b). a * b = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> finite {(a, b). a * b = n}
[PROOF STEP]
by (rule finite_subset[of _ "{0<..n} \<times> {0<..n}"]) auto


[STATEMENT]
lemma dirichlet_prod_assoc_aux1:
  assumes "n > 0"
  shows "dirichlet_prod f (dirichlet_prod g h) n =
           (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
have "dirichlet_prod f (dirichlet_prod g h) n =
          (\<Sum>x\<in>{(a,b). a * b = n}. (\<Sum>(c,d) | c * d = snd x. f (fst x) * g c * h d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = snd x}. f (fst x) * g c * h d)
[PROOF STEP]
by (auto intro!: sum.cong simp: dirichlet_prod_altdef2 sum_distrib_left mult.assoc)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = snd x}. f (fst x) * g c * h d)

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = snd x}. f (fst x) * g c * h d)

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}).
                               case x of (x, c, d) \<Rightarrow> f (fst x) * g c * h d)"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = snd x}. f (fst x) * g c * h d) = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}). case x of (x, c, d) \<Rightarrow> f (fst x) * g c * h d)
[PROOF STEP]
by (intro sum.Sigma finite_divisors_nat' ballI) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = snd x}. f (fst x) * g c * h d) = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}). case x of (x, c, d) \<Rightarrow> f (fst x) * g c * h d)

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = snd x}. f (fst x) * g c * h d) = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}). case x of (x, c, d) \<Rightarrow> f (fst x) * g c * h d)

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
have "\<dots> = (\<Sum>(a,b,c) | a * b * c = n. f a * g b * h c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}). case x of (x, c, d) \<Rightarrow> f (fst x) * g c * h d) = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
by (rule sum.reindex_bij_witness
               [of _ "\<lambda>(a,b,c). ((a, b*c), (b,c))" "\<lambda>((a,b),(c,d)). (a, c, d)"])
       (auto simp: mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}). case x of (x, c, d) \<Rightarrow> f (fst x) * g c * h d) = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)

goal (1 subgoal):
 1. dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (dirichlet_prod g h) n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_assoc_aux2:
  assumes "n > 0"
  shows "dirichlet_prod (dirichlet_prod f g) h n =
           (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
have "dirichlet_prod (dirichlet_prod f g) h n =
          (\<Sum>x\<in>{(a,b). a * b = n}. (\<Sum>(c,d) | c * d = fst x. f c * g d * h (snd x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = fst x}. f c * g d * h (snd x))
[PROOF STEP]
by (auto intro!: sum.cong simp: dirichlet_prod_altdef2 sum_distrib_right mult.assoc)
[PROOF STATE]
proof (state)
this:
dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = fst x}. f c * g d * h (snd x))

goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = fst x}. f c * g d * h (snd x))

goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}).
                               case x of (x, c, d) \<Rightarrow> f c * g d * h (snd x))"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = fst x}. f c * g d * h (snd x)) = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}). case x of (x, c, d) \<Rightarrow> f c * g d * h (snd x))
[PROOF STEP]
by (intro sum.Sigma finite_divisors_nat' ballI) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = fst x}. f c * g d * h (snd x)) = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}). case x of (x, c, d) \<Rightarrow> f c * g d * h (snd x))

goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{(a, b). a * b = n}. \<Sum>(c, d)\<in>{(c, d). c * d = fst x}. f c * g d * h (snd x)) = (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}). case x of (x, c, d) \<Rightarrow> f c * g d * h (snd x))

goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
have "\<dots> = (\<Sum>(a,b,c) | a * b * c = n. f a * g b * h c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}). case x of (x, c, d) \<Rightarrow> f c * g d * h (snd x)) = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
by (rule sum.reindex_bij_witness
               [of _ "\<lambda>(a,b,c). ((a*b, c), (a,b))" "\<lambda>((a,b),(c,d)). (c, d, b)"])
       (auto simp: mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}). case x of (x, c, d) \<Rightarrow> f c * g d * h (snd x)) = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)

goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)

goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dirichlet_prod (dirichlet_prod f g) h n = (\<Sum>(a, b, c)\<in>{(a, b, c). a * b * c = n}. f a * g b * h c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_assoc:
  "dirichlet_prod (dirichlet_prod f g) h = dirichlet_prod f (dirichlet_prod g h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h = dirichlet_prod f (dirichlet_prod g h)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dirichlet_prod (dirichlet_prod f g) h x = dirichlet_prod f (dirichlet_prod g h) x
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dirichlet_prod (dirichlet_prod f g) h x = dirichlet_prod f (dirichlet_prod g h) x
[PROOF STEP]
show "dirichlet_prod (dirichlet_prod f g) h n = dirichlet_prod f (dirichlet_prod g h) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (dirichlet_prod f g) h n = dirichlet_prod f (dirichlet_prod g h) n
[PROOF STEP]
by (cases "n = 0") (simp_all add: dirichlet_prod_assoc_aux1 dirichlet_prod_assoc_aux2)
[PROOF STATE]
proof (state)
this:
dirichlet_prod (dirichlet_prod f g) h n = dirichlet_prod f (dirichlet_prod g h) n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_const_right [simp]:
  assumes "n > 0"
  shows   "dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else 0) n = f n * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c
[PROOF STEP]
have "dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else 0) n =
          (\<Sum>d | d dvd n. (if d = n then f n * c else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = (\<Sum>d | d dvd n. if d = n then f n * c else (0::'a))
[PROOF STEP]
unfolding dirichlet_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d * (if n div d = Suc 0 then c else (0::'a))) = (\<Sum>d | d dvd n. if d = n then f n * c else (0::'a))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. f d * (if n div d = Suc 0 then c else (0::'a))) = (\<Sum>d | d dvd n. if d = n then f n * c else (0::'a))
[PROOF STEP]
by (intro sum.cong refl) (auto elim!: dvdE split: if_splits)
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = (\<Sum>d | d dvd n. if d = n then f n * c else (0::'a))

goal (1 subgoal):
 1. dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = (\<Sum>d | d dvd n. if d = n then f n * c else (0::'a))

goal (1 subgoal):
 1. dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c
[PROOF STEP]
have "\<dots> = f n * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. if d = n then f n * c else (0::'a)) = f n * c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. if d = n then f n * c else (0::'a)) = f n * c
[PROOF STEP]
by (subst sum.delta) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. if d = n then f n * c else (0::'a)) = f n * c

goal (1 subgoal):
 1. dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c

goal (1 subgoal):
 1. dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dirichlet_prod f (\<lambda>n. if n = Suc 0 then c else (0::'a)) n = f n * c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_const_left [simp]:
  assumes "n > 0"
  shows   "dirichlet_prod (\<lambda>n. if n = Suc 0 then c else 0) g n = c * g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n
[PROOF STEP]
have "dirichlet_prod (\<lambda>n. if n = Suc 0 then c else 0) g n =
          (\<Sum>d | d dvd n. (if d = 1 then c * g n else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = (\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a))
[PROOF STEP]
unfolding dirichlet_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. (if d = Suc 0 then c else (0::'a)) * g (n div d)) = (\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. (if d = Suc 0 then c else (0::'a)) * g (n div d)) = (\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a))
[PROOF STEP]
by (intro sum.cong refl) (auto elim!: dvdE split: if_splits)
[PROOF STATE]
proof (state)
this:
dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = (\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a))

goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = (\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a))

goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n
[PROOF STEP]
have "\<dots> = c * g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a)) = c * g n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a)) = c * g n
[PROOF STEP]
by (subst sum.delta) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. if d = 1 then c * g n else (0::'a)) = c * g n

goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n

goal (1 subgoal):
 1. dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dirichlet_prod (\<lambda>n. if n = Suc 0 then c else (0::'a)) g n = c * g n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_inverse_induct [case_names 0 1 gt1]:
  "P 0 \<Longrightarrow> P (Suc 0) \<Longrightarrow> (\<And>n. n > 1 \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> P k) \<Longrightarrow> P n) \<Longrightarrow> P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P 0; P (Suc 0); \<And>n. \<lbrakk>1 < n; \<And>k. k < n \<Longrightarrow> P k\<rbrakk> \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
by induction_schema (force, rule wf_measure [of id], simp)


[STATEMENT]
lemma dirichlet_inverse_0 [simp]: "dirichlet_inverse f i 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i 0 = (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma dirichlet_inverse_Suc_0 [simp]: "dirichlet_inverse f i (Suc 0) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_inverse f i (Suc 0) = i
[PROOF STEP]
by simp


[STATEMENT]
lemma dirichlet_inverse_gt_1:
  "n > 1 \<Longrightarrow> dirichlet_inverse f i n =
     -i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> dirichlet_inverse f i n = - i * (\<Sum>d | d dvd n \<and> d < n. f (n div d) * dirichlet_inverse f i d)
[PROOF STEP]
by (simp add: dirichlet_inverse.simps)