[STATEMENT]
lemma weakSimStatEq:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   \<Psi>'  :: 'b

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto><Rel> Q"
  and     "eqvt Rel'"
  and     "\<Psi> \<simeq> \<Psi>'"
  and     C1: "\<And>\<Psi>' R S \<Psi>''. \<lbrakk>(\<Psi>', R, S) \<in> Rel; \<Psi>' \<simeq> \<Psi>''\<rbrakk> \<Longrightarrow> (\<Psi>'', R, S) \<in> Rel'"

  shows "\<Psi>' \<rhd> P \<leadsto><Rel'> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<leadsto><Rel'> Q
[PROOF STEP]
using \<open>eqvt Rel'\<close>
[PROOF STATE]
proof (prove)
using this:
eqvt Rel'

goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<leadsto><Rel'> Q
[PROOF STEP]
proof(induct rule: weakSimI[of _ _ _ _ \<Psi>])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
case(cAct \<Psi>'' \<alpha> Q')
[PROOF STATE]
proof (state)
this:
\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>'
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* Q
bn \<alpha> \<sharp>* subject \<alpha>
bn \<alpha> \<sharp>* \<Psi>
distinct (bn \<alpha>)
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
from \<open>\<Psi>' \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'"
[PROOF STATE]
proof (prove)
using this:
\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
by(metis statEqTransition AssertionStatEqSym)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
with PSimQ \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
obtain P'' P' where PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''" and P''Chain: "\<Psi> \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
                  and P'RelQ': "(\<Psi> \<otimes> \<Psi>'', P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>'', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi> \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>'', P', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
from PTrans \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
[PROOF STEP]
by(rule weakTransitionStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
from P''Chain \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
by(metis tauChainStatEq Composition)
[PROOF STATE]
proof (state)
this:
\<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
from P'RelQ' \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> \<Psi>'', P', Q') \<in> Rel
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "(\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> \<Psi>'', P', Q') \<in> Rel
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel'
[PROOF STEP]
by(metis C1 Composition)
[PROOF STATE]
proof (state)
this:
(\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel'

goal (2 subgoals):
 1. \<And>\<Psi>'' \<alpha> Q'. \<lbrakk>\<Psi>' \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
 2. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel'

goal (1 subgoal):
 1. \<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi>' \<otimes> \<Psi>'' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>' \<otimes> \<Psi>'', P', Q') \<in> Rel')

goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
case(cTau Q')
[PROOF STATE]
proof (state)
this:
\<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
from \<open>\<Psi>' \<rhd> Q \<longmapsto>\<tau> \<prec> Q'\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'"
[PROOF STATE]
proof (prove)
using this:
\<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
by(metis statEqTransition AssertionStatEqSym)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
with PSimQ
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
obtain P' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
from PChain \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
by(rule tauChainStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
from \<open>(\<Psi>, P', Q') \<in> Rel\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "(\<Psi>', P', Q') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
by(rule C1)
[PROOF STATE]
proof (state)
this:
(\<Psi>', P', Q') \<in> Rel'

goal (1 subgoal):
 1. \<And>Q'. \<Psi>' \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>', P', Q') \<in> Rel'

goal (1 subgoal):
 1. \<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>', P', Q') \<in> Rel'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakSimMonotonic:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   A :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q :: "('a, 'b, 'c) psi"
  and   B :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes "\<Psi> \<rhd> P \<leadsto><A> Q"
  and     "A \<subseteq> B"

  shows "\<Psi> \<rhd> P \<leadsto><B> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><B> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><A> Q
A \<subseteq> B

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><B> Q
[PROOF STEP]
by(simp (no_asm) add: weakSimulation_def) (blast dest: weakSimE)+


[STATEMENT]
lemma strongSimWeakSim:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes PRelQ: "(\<Psi>, P, Q) \<in> Rel"
  and     StatImp: "\<And>\<Psi>' R S. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> insertAssertion(extractFrame S) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion(extractFrame R) \<Psi>'"
  and     Sim:     "\<And>\<Psi>' R S. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> \<Psi>' \<rhd> R \<leadsto>[Rel] S"
  and     Ext:     "\<And>\<Psi>' R S \<Psi>''. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> (\<Psi>' \<otimes> \<Psi>'', R, S) \<in> Rel"

  shows "\<Psi> \<rhd> P \<leadsto><Rel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> Q
[PROOF STEP]
proof(induct rule: weakSimI2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cAct \<Psi>' \<alpha> Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> Rel
[PROOF STEP]
have "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto>[Rel] Q
[PROOF STEP]
by(rule Sim)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<leadsto>[Rel] Q

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<Psi> \<rhd> P \<leadsto>[Rel] Q
[PROOF STEP]
obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<Psi> \<rhd> P \<leadsto>[Rel] Q

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
(\<Psi>, P', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> Rel
[PROOF STEP]
have "insertAssertion(extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame P) \<Psi>"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> Rel

goal (1 subgoal):
 1. insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P) \<Psi>
[PROOF STEP]
by(rule StatImp)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P) \<Psi>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P) \<Psi>
[PROOF STEP]
have "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P) \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(rule transitionWeakTransition)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from P'RelQ'
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
have "\<forall>\<Psi>'. \<exists>P''. \<Psi> \<otimes> \<Psi>' \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<and> (\<Psi> \<otimes> \<Psi>', P'', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<forall>\<Psi>'. \<exists>P''. \<Psi> \<otimes> \<Psi>' \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<and> (\<Psi> \<otimes> \<Psi>', P'', Q') \<in> Rel
[PROOF STEP]
by(force intro: Ext)
[PROOF STATE]
proof (state)
this:
\<forall>\<Psi>'. \<exists>P''. \<Psi> \<otimes> \<Psi>' \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<and> (\<Psi> \<otimes> \<Psi>', P'', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
\<forall>\<Psi>'. \<exists>P''. \<Psi> \<otimes> \<Psi>' \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<and> (\<Psi> \<otimes> \<Psi>', P'', Q') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
\<forall>\<Psi>'. \<exists>P''. \<Psi> \<otimes> \<Psi>' \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<and> (\<Psi> \<otimes> \<Psi>', P'', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cTau Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> Rel
[PROOF STEP]
have "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto>[Rel] Q
[PROOF STEP]
by(rule Sim)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<leadsto>[Rel] Q

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with \<open>\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
\<Psi> \<rhd> P \<leadsto>[Rel] Q
[PROOF STEP]
obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
\<Psi> \<rhd> P \<leadsto>[Rel] Q

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force dest: simE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
(\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
have "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
using P'RelQ'
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strongAppend:
  fixes \<Psi>    :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   Q     :: "('a, 'b, 'c) psi"
  and   R     :: "('a, 'b, 'c) psi"
  and   Rel   :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Rel'  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Rel'' :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto><Rel> Q"
  and     QSimR: "\<Psi> \<rhd> Q \<leadsto>[Rel'] R"
  and     Eqvt'': "eqvt Rel''"
  and     RimpQ: "insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>"
  and     Set: "{(\<Psi>, P, R) | \<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''"
  and     C1: "\<And>\<Psi> P Q \<Psi>'. (\<Psi>, P, Q) \<in> Rel' \<Longrightarrow> (\<Psi> \<otimes> \<Psi>', P, Q) \<in> Rel'"

  shows "\<Psi> \<rhd> P \<leadsto><Rel''> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel''> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel''> R
[PROOF STEP]
from Eqvt''
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqvt Rel''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel''> R
[PROOF STEP]
proof(induct rule: weakSimI[of _ _ _ _ Q])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
case(cAct \<Psi>' \<alpha> R')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> R'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* R
bn \<alpha> \<sharp>* subject \<alpha>
bn \<alpha> \<sharp>* Q
distinct (bn \<alpha>)
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<leadsto>[Rel'] R\<close> \<open>\<Psi> \<rhd> R \<longmapsto>\<alpha> \<prec> R'\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* Q\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<leadsto>[Rel'] R
\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> R'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* Q
[PROOF STEP]
obtain Q' where QTrans: "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'" and "(\<Psi>, Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<leadsto>[Rel'] R
\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> R'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* Q

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; (\<Psi>, Q', R') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
(\<Psi>, Q', R') \<in> Rel'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from \<open>(\<Psi>, Q', R') \<in> Rel'\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, Q', R') \<in> Rel'
[PROOF STEP]
have Q'RelR': "(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, Q', R') \<in> Rel'

goal (1 subgoal):
 1. (\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'
[PROOF STEP]
by(rule C1)
[PROOF STATE]
proof (state)
this:
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<leadsto><Rel> Q\<close> QTrans \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>
[PROOF STEP]
obtain P'' P' where PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''" and P''Chain: "\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
                    and P'RelQ': "(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from PTrans RimpQ
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>
[PROOF STEP]
have "\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>

goal (1 subgoal):
 1. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
[PROOF STEP]
by(rule weakTransitionFrameImp)
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
note P''Chain
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from P'RelQ' Q'RelR' Set
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''
[PROOF STEP]
have "(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''

goal (1 subgoal):
 1. (\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel'')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel'')

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
case(cTau R')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> R'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<leadsto>[Rel'] R\<close> \<open>\<Psi> \<rhd> R \<longmapsto>\<tau> \<prec> R'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<leadsto>[Rel'] R
\<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> R'
[PROOF STEP]
obtain Q' where QTrans: "\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'" and Q'RelR': "(\<Psi>, Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<leadsto>[Rel'] R
\<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> R'

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; (\<Psi>, Q', R') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force dest: simE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
(\<Psi>, Q', R') \<in> Rel'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<leadsto><Rel> Q\<close> QTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
obtain P' where PTrans: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
note PTrans
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from P'RelQ' Q'RelR' Set
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
(\<Psi>, Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''
[PROOF STEP]
have "(\<Psi>, P', R') \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel
(\<Psi>, Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''

goal (1 subgoal):
 1. (\<Psi>, P', R') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Psi>, P', R') \<in> Rel''

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', R') \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', R') \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', R') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', R') \<in> Rel''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<leadsto><Rel''> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quietSim:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"

  assumes "quiet P"
  and     "eqvt Rel"
  and     cQuiet: "\<And>P. quiet P \<Longrightarrow> (\<Psi>, \<zero>, P) \<in> Rel"

  shows "\<Psi> \<rhd> \<zero> \<leadsto><Rel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<zero> \<leadsto><Rel> P
[PROOF STEP]
using \<open>eqvt Rel\<close>
[PROOF STATE]
proof (prove)
using this:
eqvt Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> \<zero> \<leadsto><Rel> P
[PROOF STEP]
proof(induct rule: weakSimI[of _ _ _ _ "()"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* \<zero>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : P \<rhd> \<zero> \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cAct \<Psi>' \<alpha> P')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* \<zero>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* subject \<alpha>
bn \<alpha> \<sharp>* ()
distinct (bn \<alpha>)
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* \<zero>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : P \<rhd> \<zero> \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close> \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
\<alpha> \<noteq> \<tau>
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
\<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>quiet P\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
\<alpha> \<noteq> \<tau>
quiet P

goal (1 subgoal):
 1. False
[PROOF STEP]
by(cases rule: actionCases[where \<alpha>=\<alpha>]) (auto intro: quietOutput quietInput)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* \<zero>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : P \<rhd> \<zero> \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : P \<rhd> \<zero> \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'a. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'a \<and> (\<Psi> \<otimes> \<Psi>', P'a, P') \<in> Rel)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : P \<rhd> \<zero> \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'a. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'a \<and> (\<Psi> \<otimes> \<Psi>', P'a, P') \<in> Rel)

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cTau P')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'\<close> \<open>quiet P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
quiet P
[PROOF STEP]
have "quiet P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
quiet P

goal (1 subgoal):
 1. quiet P'
[PROOF STEP]
by(erule_tac quiet.cases) (force simp add: residualInject)
[PROOF STATE]
proof (state)
this:
quiet P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
have "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>quiet P'\<close>
[PROOF STATE]
proof (chain)
picking this:
quiet P'
[PROOF STEP]
have "(\<Psi>, \<zero>, P') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
quiet P'

goal (1 subgoal):
 1. (\<Psi>, \<zero>, P') \<in> Rel
[PROOF STEP]
by(rule cQuiet)
[PROOF STATE]
proof (state)
this:
(\<Psi>, \<zero>, P') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P
(\<Psi>, \<zero>, P') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P
(\<Psi>, \<zero>, P') \<in> Rel

goal (1 subgoal):
 1. \<exists>P'a. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, P') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'a. \<Psi> \<rhd> \<zero> \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, P') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measure_parity:
  "(strict{(x::parity,y). x \<sqsubseteq> y})^-1 \<subseteq> measure m_parity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (strict {(x, y). x \<sqsubseteq> y})\<inverse> \<subseteq> measure m_parity
[PROOF STEP]
by(auto simp add: m_parity_def le_parity_def)


[STATEMENT]
lemma measure_parity_eq:
  "\<forall>x y::parity. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m_parity x = m_parity y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m_parity x = m_parity y
[PROOF STEP]
by(auto simp add: m_parity_def le_parity_def)


[STATEMENT]
lemma AI_parity_Some: "\<exists>c'. AI_parity c = Some c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c'. AI_parity c = Some c'
[PROOF STEP]
by(rule AI_Some_measure[OF measure_parity measure_parity_eq])


[STATEMENT]
lemma Suc_0 [simp]: "f (Suc 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc 0) = (1::'a)
[PROOF STEP]
using one
[PROOF STATE]
proof (prove)
using this:
f 1 = (1::'a)

goal (1 subgoal):
 1. f (Suc 0) = (1::'a)
[PROOF STEP]
by (simp del: one)


[STATEMENT]
lemma mult_coprime:
  assumes "coprime a b"
  shows   "f (a * b) = f a * f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
consider "n = 0" | "n = 1" | "n > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; n = 1 \<Longrightarrow> thesis; 1 < n \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n3 = 0 \<Longrightarrow> ?thesis; ?n3 = 1 \<Longrightarrow> ?thesis; 1 < ?n3 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
note P = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n3 = 0 \<Longrightarrow> ?thesis; ?n3 = 1 \<Longrightarrow> ?thesis; 1 < ?n3 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
by (cases a rule: P; cases b rule: P) (simp_all add: mult_coprime_aux assms)
[PROOF STATE]
proof (state)
this:
f (a * b) = f a * f b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_coprime:
  assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime (g x) (g y)"
  shows   "f (prod g A) = (\<Prod>x\<in>A. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (prod g A) = (\<Prod>x\<in>A. f (g x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> A; ?y \<in> A; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> coprime (g ?x) (g ?y)

goal (1 subgoal):
 1. f (prod g A) = (\<Prod>x\<in>A. f (g x))
[PROOF STEP]
proof (induction rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x y. \<lbrakk>x \<in> F; y \<in> F; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g F) = (\<Prod>x\<in>F. f (g x)); \<And>xa y. \<lbrakk>xa \<in> insert x F; y \<in> insert x F; xa \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g xa) (g y)\<rbrakk> \<Longrightarrow> f (prod g (insert x F)) = (\<Prod>x\<in>insert x F. f (g x))
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
\<lbrakk>?x \<in> insert x A; ?y \<in> insert x A; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> coprime (g ?x) (g ?y)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x y. \<lbrakk>x \<in> F; y \<in> F; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g F) = (\<Prod>x\<in>F. f (g x)); \<And>xa y. \<lbrakk>xa \<in> insert x F; y \<in> insert x F; xa \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g xa) (g y)\<rbrakk> \<Longrightarrow> f (prod g (insert x F)) = (\<Prod>x\<in>insert x F. f (g x))
[PROOF STEP]
from insert
[PROOF STATE]
proof (chain)
picking this:
finite A
x \<notin> A
(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
\<lbrakk>?x \<in> insert x A; ?y \<in> insert x A; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> coprime (g ?x) (g ?y)
[PROOF STEP]
have "f (prod g (insert x A)) = f (g x * prod g A)"
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
\<lbrakk>?x \<in> insert x A; ?y \<in> insert x A; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> coprime (g ?x) (g ?y)

goal (1 subgoal):
 1. f (prod g (insert x A)) = f (g x * prod g A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (prod g (insert x A)) = f (g x * prod g A)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x y. \<lbrakk>x \<in> F; y \<in> F; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g F) = (\<Prod>x\<in>F. f (g x)); \<And>xa y. \<lbrakk>xa \<in> insert x F; y \<in> insert x F; xa \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g xa) (g y)\<rbrakk> \<Longrightarrow> f (prod g (insert x F)) = (\<Prod>x\<in>insert x F. f (g x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (prod g (insert x A)) = f (g x * prod g A)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x y. \<lbrakk>x \<in> F; y \<in> F; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g F) = (\<Prod>x\<in>F. f (g x)); \<And>xa y. \<lbrakk>xa \<in> insert x F; y \<in> insert x F; xa \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g xa) (g y)\<rbrakk> \<Longrightarrow> f (prod g (insert x F)) = (\<Prod>x\<in>insert x F. f (g x))
[PROOF STEP]
have "\<dots> = f (g x) * f (prod g A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (g x * prod g A) = f (g x) * f (prod g A)
[PROOF STEP]
using insert.prems insert.hyps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> insert x A; ?y \<in> insert x A; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> coprime (g ?x) (g ?y)
finite A
x \<notin> A

goal (1 subgoal):
 1. f (g x * prod g A) = f (g x) * f (prod g A)
[PROOF STEP]
by (auto intro: mult_coprime prod_coprime_right)
[PROOF STATE]
proof (state)
this:
f (g x * prod g A) = f (g x) * f (prod g A)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x y. \<lbrakk>x \<in> F; y \<in> F; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g F) = (\<Prod>x\<in>F. f (g x)); \<And>xa y. \<lbrakk>xa \<in> insert x F; y \<in> insert x F; xa \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g xa) (g y)\<rbrakk> \<Longrightarrow> f (prod g (insert x F)) = (\<Prod>x\<in>insert x F. f (g x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (g x * prod g A) = f (g x) * f (prod g A)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x y. \<lbrakk>x \<in> F; y \<in> F; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g F) = (\<Prod>x\<in>F. f (g x)); \<And>xa y. \<lbrakk>xa \<in> insert x F; y \<in> insert x F; xa \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g xa) (g y)\<rbrakk> \<Longrightarrow> f (prod g (insert x F)) = (\<Prod>x\<in>insert x F. f (g x))
[PROOF STEP]
have "\<dots> = (\<Prod>x\<in>insert x A. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (g x) * f (prod g A) = (\<Prod>x\<in>insert x A. f (g x))
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
\<lbrakk>?x \<in> insert x A; ?y \<in> insert x A; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> coprime (g ?x) (g ?y)

goal (1 subgoal):
 1. f (g x) * f (prod g A) = (\<Prod>x\<in>insert x A. f (g x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (g x) * f (prod g A) = (\<Prod>x\<in>insert x A. f (g x))

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x y. \<lbrakk>x \<in> F; y \<in> F; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g F) = (\<Prod>x\<in>F. f (g x)); \<And>xa y. \<lbrakk>xa \<in> insert x F; y \<in> insert x F; xa \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g xa) (g y)\<rbrakk> \<Longrightarrow> f (prod g (insert x F)) = (\<Prod>x\<in>insert x F. f (g x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (prod g (insert x A)) = (\<Prod>x\<in>insert x A. f (g x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f (prod g (insert x A)) = (\<Prod>x\<in>insert x A. f (g x))

goal (1 subgoal):
 1. f (prod g (insert x A)) = (\<Prod>x\<in>insert x A. f (g x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f (prod g (insert x A)) = (\<Prod>x\<in>insert x A. f (g x))

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)\<rbrakk> \<Longrightarrow> f (prod g A) = (\<Prod>x\<in>A. f (g x))
 2. (\<And>x y. \<lbrakk>x \<in> {}; y \<in> {}; x \<noteq> y\<rbrakk> \<Longrightarrow> coprime (g x) (g y)) \<Longrightarrow> f (prod g {}) = (\<Prod>x\<in>{}. f (g x))
[PROOF STEP]
qed auto


[STATEMENT]
lemma prod_prime_factors:
  assumes "n > 0"
  shows   "f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
have "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)
[PROOF STEP]
using Primes.prime_factorization_nat assms
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> ?n = (\<Prod>p\<in>prime_factors ?n. p ^ multiplicity p ?n)
0 < n

goal (1 subgoal):
 1. n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)

goal (1 subgoal):
 1. f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)

goal (1 subgoal):
 1. f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
have "f \<dots> = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
by (rule prod_coprime) (auto simp add: in_prime_factors_imp_prime primes_coprime)
[PROOF STATE]
proof (state)
this:
f (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))

goal (1 subgoal):
 1. f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))

goal (1 subgoal):
 1. f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicative_sum_divisors: "multiplicative_function (\<lambda>n. \<Sum>d | d dvd n. f d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. \<Sum>d | d dvd n. f d)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
assume ab: "a > 1" "b > 1" "coprime a b"
[PROOF STATE]
proof (state)
this:
1 < a
1 < b
coprime a b

goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
hence "(\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s))"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b
coprime a b

goal (1 subgoal):
 1. (\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s))
[PROOF STEP]
by (intro sum_divisors_coprime_mult)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s))

goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s))

goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
have "\<dots> = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f 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. f r * f s)
[PROOF STEP]
using ab(3)
[PROOF STATE]
proof (prove)
using this:
coprime a b

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. f r * f s)
[PROOF STEP]
by (auto intro!: sum.cong intro: mult_coprime coprime_imp_coprime dvd_trans)
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s)) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s)

goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>s | s dvd b. f (r * s)) = (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s)

goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
have "\<dots> = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s) = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)
[PROOF STEP]
by (subst sum_distrib_right, subst sum_distrib_left) simp_all
[PROOF STATE]
proof (state)
this:
(\<Sum>r | r dvd a. \<Sum>s | s dvd b. f r * f s) = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)

goal (3 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd a * b. f d) = (\<Sum>d | d dvd a. f d) * (\<Sum>d | d dvd b. f d)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)
[PROOF STEP]
show "(\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)

goal (1 subgoal):
 1. (\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd a * b. f d) = (\<Sum>r | r dvd a. f r) * (\<Sum>s | s dvd b. f s)

goal (2 subgoals):
 1. (\<Sum>d | d dvd 0. f d) = (0::'a)
 2. (\<Sum>d | is_unit d. f d) = (1::'a)
[PROOF STEP]
qed auto


[STATEMENT]
lemma prime: "prime p \<Longrightarrow> f p = f_prime p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> f p = f_prime p
[PROOF STEP]
using prime_power[of p 1] prime_aux[of p]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime p; 0 < 1\<rbrakk> \<Longrightarrow> f (p ^ 1) = f_prime_power p 1
prime p \<Longrightarrow> f_prime_power p 1 = f_prime p

goal (1 subgoal):
 1. prime p \<Longrightarrow> f p = f_prime p
[PROOF STEP]
by simp


[STATEMENT]
lemma prod_prime_factors':
  assumes "n > 0"
  shows   "f n = (\<Prod>p\<in>prime_factors n. f_prime_power p (multiplicity p n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = (\<Prod>p\<in>prime_factors n. f_prime_power p (multiplicity p n))
[PROOF STEP]
by (subst prod_prime_factors[OF assms(1)])
     (intro prod.cong refl prime_power, auto simp: prime_factors_multiplicity)


[STATEMENT]
lemma efficient_code_aux:
  assumes "n > 0" "set ps = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n" "distinct ps"
  shows   "f n = (\<Prod>(p,d) \<leftarrow> ps. f_prime_power p (Suc d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
set ps = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n
distinct ps
[PROOF STEP]
have
    "(\<Prod>(p,d) \<leftarrow> ps. f_prime_power p (Suc d)) =
       (\<Prod>(p,d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d))"
[PROOF STATE]
proof (prove)
using this:
0 < n
set ps = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n
distinct ps

goal (1 subgoal):
 1. (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d)) = (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d))
[PROOF STEP]
by (subst prod.distinct_set_conv_list [symmetric]) simp_all
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d)) = (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d))

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d)) = (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d))

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
have "\<dots> = (\<Prod>x\<in>prime_factors n. f_prime_power x (multiplicity x n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d)) = (\<Prod>x\<in>prime_factors n. f_prime_power x (multiplicity x n))
[PROOF STEP]
by (subst prod.reindex) (auto simp: inj_on_def prime_factors_multiplicity intro!: prod.cong)
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d)) = (\<Prod>x\<in>prime_factors n. f_prime_power x (multiplicity x n))

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d)) = (\<Prod>x\<in>prime_factors n. f_prime_power x (multiplicity x n))

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
have "\<dots> = f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x\<in>prime_factors n. f_prime_power x (multiplicity x n)) = f n
[PROOF STEP]
by (rule prod_prime_factors' [symmetric]) fact+
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>prime_factors n. f_prime_power x (multiplicity x n)) = f n

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d)) = f n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d)) = f n

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime_power p (Suc d))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma efficient_code:
  assumes "set (ps ()) = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n" "distinct (ps ())"
  shows   "f n = (if n = 0 then 0 else (\<Prod>(p,d) \<leftarrow> ps (). f_prime_power p (Suc d)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = (if n = 0 then 0::'a else \<Prod>(p, d)\<leftarrow>ps (). f_prime_power p (Suc d))
[PROOF STEP]
using efficient_code_aux[of n "ps ()"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < n; set (ps ()) = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n; distinct (ps ())\<rbrakk> \<Longrightarrow> f n = (\<Prod>(p, d)\<leftarrow>ps (). f_prime_power p (Suc d))
set (ps ()) = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n
distinct (ps ())

goal (1 subgoal):
 1. f n = (if n = 0 then 0::'a else \<Prod>(p, d)\<leftarrow>ps (). f_prime_power p (Suc d))
[PROOF STEP]
by simp


[STATEMENT]
lemma mult: "f (a * b) = f a * f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
consider "n = 0" | "n = 1" | "n > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; n = 1 \<Longrightarrow> thesis; 1 < n \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; n = 1 \<Longrightarrow> ?thesis; 1 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n3 = 0 \<Longrightarrow> ?thesis; ?n3 = 1 \<Longrightarrow> ?thesis; 1 < ?n3 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
note P = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n3 = 0 \<Longrightarrow> ?thesis; ?n3 = 1 \<Longrightarrow> ?thesis; 1 < ?n3 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a * b) = f a * f b
[PROOF STEP]
by (cases a rule: P; cases b rule: P) (simp_all add: zero_aux one_aux mult_aux)
[PROOF STATE]
proof (state)
this:
f (a * b) = f a * f b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod: "f (prod g A) = (\<Prod>x\<in>A. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (prod g A) = (\<Prod>x\<in>A. f (g x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) (simp_all add: mult)


[STATEMENT]
lemma power: "f (n ^ m) = f n ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (n ^ m) = f n ^ m
[PROOF STEP]
by (induction m) (simp_all add: mult)


[STATEMENT]
lemma prod_prime_factors': "n > 0 \<Longrightarrow> f n = (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> f n = (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n)
[PROOF STEP]
by (subst prime_factorization_nat) (simp_all add: prod power)


[STATEMENT]
lemma prod_prime_factors'': "n > 0 \<Longrightarrow> f n = (\<Prod>p\<in>prime_factors n. f_prime p ^ multiplicity p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> f n = (\<Prod>p\<in>prime_factors n. f_prime p ^ multiplicity p n)
[PROOF STEP]
by (subst prod_prime_factors') (auto simp: f_prime prime_factors_multiplicity intro!: prod.cong)


[STATEMENT]
lemma efficient_code_aux:
  assumes "n > 0" "set ps = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n" "distinct ps"
  shows   "f n = (\<Prod>(p,d) \<leftarrow> ps. f_prime p ^ Suc d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
set ps = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n
distinct ps
[PROOF STEP]
have
    "(\<Prod>(p,d) \<leftarrow> ps. f_prime p ^ Suc d) =
       (\<Prod>(p,d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d)"
[PROOF STATE]
proof (prove)
using this:
0 < n
set ps = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n
distinct ps

goal (1 subgoal):
 1. (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d) = (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d)
[PROOF STEP]
by (subst prod.distinct_set_conv_list [symmetric]) simp_all
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d) = (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d)

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d) = (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d)

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
have "\<dots> = (\<Prod>x\<in>prime_factors n. f_prime x ^ multiplicity x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d) = (\<Prod>x\<in>prime_factors n. f_prime x ^ multiplicity x n)
[PROOF STEP]
by (subst prod.reindex) (auto simp: inj_on_def prime_factors_multiplicity
                                  simp del: power_Suc intro!: prod.cong)
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d) = (\<Prod>x\<in>prime_factors n. f_prime x ^ multiplicity x n)

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>(p, d)\<in>(\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d) = (\<Prod>x\<in>prime_factors n. f_prime x ^ multiplicity x n)

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
have "\<dots> = f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x\<in>prime_factors n. f_prime x ^ multiplicity x n) = f n
[PROOF STEP]
by (rule prod_prime_factors'' [symmetric]) fact+
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>prime_factors n. f_prime x ^ multiplicity x n) = f n

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d) = f n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d) = f n

goal (1 subgoal):
 1. f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f n = (\<Prod>(p, d)\<leftarrow>ps. f_prime p ^ Suc d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma efficient_code:
  assumes "set (ps ()) = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n" "distinct (ps ())"
  shows   "f n = (if n = 0 then 0 else (\<Prod>(p,d) \<leftarrow> ps (). f_prime p ^ Suc d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = (if n = 0 then 0::'a else \<Prod>(p, d)\<leftarrow>ps (). f_prime p ^ Suc d)
[PROOF STEP]
using efficient_code_aux[of n "ps ()"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < n; set (ps ()) = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n; distinct (ps ())\<rbrakk> \<Longrightarrow> f n = (\<Prod>(p, d)\<leftarrow>ps (). f_prime p ^ Suc d)
set (ps ()) = (\<lambda>p. (p, multiplicity p n - 1)) ` prime_factors n
distinct (ps ())

goal (1 subgoal):
 1. f n = (if n = 0 then 0::'a else \<Prod>(p, d)\<leftarrow>ps (). f_prime p ^ Suc d)
[PROOF STEP]
by simp


[STATEMENT]
lemma multiplicative_function_eqI:
  assumes "multiplicative_function f" "multiplicative_function g"
  assumes "\<And>p k. prime p \<Longrightarrow> k > 0 \<Longrightarrow> f (p ^ k) = g (p ^ k)"
  shows   "f n = g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = g n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n = g n
[PROOF STEP]
interpret f: multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n = g n
[PROOF STEP]
interpret g: multiplicative_function g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n = g n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = g n
[PROOF STEP]
proof (cases "n > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> f n = g n
 2. \<not> 0 < n \<Longrightarrow> f n = g n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> f n = g n
 2. \<not> 0 < n \<Longrightarrow> f n = g n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. f n = g n
[PROOF STEP]
using f.prod_prime_factors[OF True] g.prod_prime_factors[OF True]
[PROOF STATE]
proof (prove)
using this:
0 < n
f n = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
g n = (\<Prod>p\<in>prime_factors n. g (p ^ multiplicity p n))

goal (1 subgoal):
 1. f n = g n
[PROOF STEP]
by (auto intro!: prod.cong assms simp: prime_factors_multiplicity)
[PROOF STATE]
proof (state)
this:
f n = g n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicative_function_of_natI:
  "multiplicative_function f \<Longrightarrow> multiplicative_function (\<lambda>n. of_nat (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f \<Longrightarrow> multiplicative_function (\<lambda>n. of_nat (f n))
[PROOF STEP]
unfolding multiplicative_function_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 = 0 \<and> f 1 = 1 \<and> (\<forall>a b. 1 < a \<longrightarrow> 1 < b \<longrightarrow> coprime a b \<longrightarrow> f (a * b) = f a * f b) \<Longrightarrow> of_nat (f 0) = (0::'a) \<and> of_nat (f 1) = (1::'a) \<and> (\<forall>a b. 1 < a \<longrightarrow> 1 < b \<longrightarrow> coprime a b \<longrightarrow> of_nat (f (a * b)) = of_nat (f a) * of_nat (f b))
[PROOF STEP]
by auto


[STATEMENT]
lemma multiplicative_function_of_natD:
  "multiplicative_function (\<lambda>n. of_nat (f n) :: 'a :: {ring_char_0, comm_semiring_1}) \<Longrightarrow>
     multiplicative_function f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. of_nat (f n)) \<Longrightarrow> multiplicative_function f
[PROOF STEP]
unfolding multiplicative_function_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (f 0) = (0::'a) \<and> of_nat (f 1) = (1::'a) \<and> (\<forall>a b. 1 < a \<longrightarrow> 1 < b \<longrightarrow> coprime a b \<longrightarrow> of_nat (f (a * b)) = of_nat (f a) * of_nat (f b)) \<Longrightarrow> f 0 = 0 \<and> f 1 = 1 \<and> (\<forall>a b. 1 < a \<longrightarrow> 1 < b \<longrightarrow> coprime a b \<longrightarrow> f (a * b) = f a * f b)
[PROOF STEP]
by (auto simp: of_nat_mult [symmetric] of_nat_eq_1_iff simp del: of_nat_mult)