[STATEMENT]
theorem Subject_reductions:
assumes wf: "wf_C_prog P" and reds: "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>"
shows "\<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> P,E,(hp s') \<turnstile> e' :\<^bsub>NT\<^esub> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
using reds
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>

goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. P,E,s' \<turnstile> e' : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
P,E,s' \<turnstile> e' : T \<surd>

goal (2 subgoals):
 1. \<And>T. P,E,s' \<turnstile> e' : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E,s' \<turnstile> e' : T \<surd>

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
by (fastforce intro:wt_same_type_typeconf simp:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case (step e s e'' s'' T)
[PROOF STATE]
proof (state)
this:
((e, s), e'', s'') \<in> Red P E
P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
P,E,s'' \<turnstile> e'' : ?T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> ?T
P,E,s \<turnstile> e : T \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
have Red:"((e, s), e'', s'') \<in> Red P E"
    and IH:"\<And>T. P,E,s'' \<turnstile> e'' : T \<surd> \<Longrightarrow> P,E,(hp s') \<turnstile> e' :\<^bsub>NT\<^esub> T"
    and wte:"P,E,s \<turnstile> e : T \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((e, s), e'', s'') \<in> Red P E &&& (\<And>T. P,E,s'' \<turnstile> e'' : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T) &&& P,E,s \<turnstile> e : T \<surd>
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
((e, s), e'', s'') \<in> Red P E
P,E,s'' \<turnstile> e'' : ?T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> ?T
P,E,s \<turnstile> e : T \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from Red
[PROOF STATE]
proof (chain)
picking this:
((e, s), e'', s'') \<in> Red P E
[PROOF STEP]
have red:"P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
((e, s), e'', s'') \<in> Red P E

goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from red_preserves_sconf[OF red] wte wf
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P,E,hp s \<turnstile> e : ?T; P,E \<turnstile> s \<surd>; wwf_prog P\<rbrakk> \<Longrightarrow> P,E \<turnstile> s'' \<surd>
P,E,s \<turnstile> e : T \<surd>
wf_C_prog P
[PROOF STEP]
have sconf:"P,E \<turnstile> s'' \<surd>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P,E,hp s \<turnstile> e : ?T; P,E \<turnstile> s \<surd>; wwf_prog P\<rbrakk> \<Longrightarrow> P,E \<turnstile> s'' \<surd>
P,E,s \<turnstile> e : T \<surd>
wf_C_prog P

goal (1 subgoal):
 1. P,E \<turnstile> s'' \<surd>
[PROOF STEP]
by(fastforce dest:wf_prog_wwf_prog simp:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s'' \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from wf red wte
[PROOF STATE]
proof (chain)
picking this:
wf_C_prog P
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>
P,E,s \<turnstile> e : T \<surd>
[PROOF STEP]
have type_conf:"P,E,(hp s'') \<turnstile> e'' :\<^bsub>NT\<^esub> T"
[PROOF STATE]
proof (prove)
using this:
wf_C_prog P
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>
P,E,s \<turnstile> e : T \<surd>

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
[PROOF STEP]
by(rule Subject_reduction)
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,ba \<turnstile> aa : T \<surd> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E,b \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
proof(cases T)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. T = Void \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 5. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case Void
[PROOF STATE]
proof (state)
this:
T = Void

goal (5 subgoals):
 1. T = Void \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 5. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with type_conf
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Void
[PROOF STEP]
have "P,E,hp s'' \<turnstile> e'' : T"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Void

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' : T

goal (5 subgoals):
 1. T = Void \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 5. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with sconf
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
have "P,E,s'' \<turnstile> e'' : T \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T

goal (1 subgoal):
 1. P,E,s'' \<turnstile> e'' : T \<surd>
[PROOF STEP]
by(simp add:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E,s'' \<turnstile> e'' : T \<surd>

goal (5 subgoals):
 1. T = Void \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 5. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (4 subgoals):
 1. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case Boolean
[PROOF STATE]
proof (state)
this:
T = Boolean

goal (4 subgoals):
 1. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with type_conf
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Boolean
[PROOF STEP]
have "P,E,hp s'' \<turnstile> e'' : T"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Boolean

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' : T

goal (4 subgoals):
 1. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with sconf
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
have "P,E,s'' \<turnstile> e'' : T \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T

goal (1 subgoal):
 1. P,E,s'' \<turnstile> e'' : T \<surd>
[PROOF STEP]
by(simp add:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E,s'' \<turnstile> e'' : T \<surd>

goal (4 subgoals):
 1. T = Boolean \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (3 subgoals):
 1. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case Integer
[PROOF STATE]
proof (state)
this:
T = Integer

goal (3 subgoals):
 1. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with type_conf
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Integer
[PROOF STEP]
have "P,E,hp s'' \<turnstile> e'' : T"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Integer

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' : T

goal (3 subgoals):
 1. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with sconf
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
have "P,E,s'' \<turnstile> e'' : T \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T

goal (1 subgoal):
 1. P,E,s'' \<turnstile> e'' : T \<surd>
[PROOF STEP]
by(simp add:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E,s'' \<turnstile> e'' : T \<surd>

goal (3 subgoals):
 1. T = Integer \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (2 subgoals):
 1. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case NT
[PROOF STATE]
proof (state)
this:
T = NT

goal (2 subgoals):
 1. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with type_conf
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = NT
[PROOF STEP]
have "P,E,hp s'' \<turnstile> e'' : T"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = NT

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' : T

goal (2 subgoals):
 1. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with sconf
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
have "P,E,s'' \<turnstile> e'' : T \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T

goal (1 subgoal):
 1. P,E,s'' \<turnstile> e'' : T \<surd>
[PROOF STEP]
by(simp add:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E,s'' \<turnstile> e'' : T \<surd>

goal (2 subgoals):
 1. T = NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case (Class C)
[PROOF STATE]
proof (state)
this:
T = Class C

goal (1 subgoal):
 1. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with type_conf
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Class C
[PROOF STEP]
have "P,E,hp s'' \<turnstile> e'' : T \<or> P,E,hp s'' \<turnstile> e'' : NT"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T
T = Class C

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : T \<or> P,E,hp s'' \<turnstile> e'' : NT
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' : T \<or> P,E,hp s'' \<turnstile> e'' : NT

goal (1 subgoal):
 1. \<And>x5. T = Class x5 \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> e'' : T \<or> P,E,hp s'' \<turnstile> e'' : NT

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
proof(rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P,E,hp s'' \<turnstile> e'' : T \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
assume "P,E,hp s'' \<turnstile> e'' : T"
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' : T

goal (2 subgoals):
 1. P,E,hp s'' \<turnstile> e'' : T \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with sconf
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T
[PROOF STEP]
have "P,E,s'' \<turnstile> e'' : T \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : T

goal (1 subgoal):
 1. P,E,s'' \<turnstile> e'' : T \<surd>
[PROOF STEP]
by(simp add:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E,s'' \<turnstile> e'' : T \<surd>

goal (2 subgoals):
 1. P,E,hp s'' \<turnstile> e'' : T \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
assume "P,E,hp s'' \<turnstile> e'' : NT"
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> e'' : NT

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with sconf
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : NT
[PROOF STEP]
have "P,E,s'' \<turnstile> e'' : NT \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s'' \<surd>
P,E,hp s'' \<turnstile> e'' : NT

goal (1 subgoal):
 1. P,E,s'' \<turnstile> e'' : NT \<surd>
[PROOF STEP]
by(simp add:wf_config_def)
[PROOF STATE]
proof (state)
this:
P,E,s'' \<turnstile> e'' : NT \<surd>

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> NT
[PROOF STEP]
have "P,E,hp s' \<turnstile> e' : NT"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> NT

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' : NT
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' : NT

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> e'' : NT \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
with Class
[PROOF STATE]
proof (chain)
picking this:
T = Class C
P,E,hp s' \<turnstile> e' : NT
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T = Class C
P,E,hp s' \<turnstile> e' : NT

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma productdivides: "\<lbrakk>x mod a = (0::nat); x mod b = 0; prime a; prime b; a \<noteq> b\<rbrakk> \<Longrightarrow> x mod (a*b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x mod a = 0; x mod b = 0; prime a; prime b; a \<noteq> b\<rbrakk> \<Longrightarrow> x mod (a * b) = 0
[PROOF STEP]
by (simp add: mod_eq_0_iff_dvd primes_coprime divides_mult)


[STATEMENT]
lemma specializedtoprimes1:
  fixes p::nat
  shows "\<lbrakk>prime p; prime q; p \<noteq> q; a mod p = b mod p ; a mod q = b mod q\<rbrakk>
         \<Longrightarrow> a mod (p*q) = b mod (p*q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; a mod p = b mod p; a mod q = b mod q\<rbrakk> \<Longrightarrow> a mod (p * q) = b mod (p * q)
[PROOF STEP]
by (metis equalmodstrick1 equalmodstrick2 productdivides)


[STATEMENT]
lemma specializedtoprimes1a:
  fixes p::nat
  shows "\<lbrakk>prime p; prime q; p \<noteq> q; a mod p = b mod p; a mod q = b mod q; b < p*q \<rbrakk>
    \<Longrightarrow> a mod (p*q) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; a mod p = b mod p; a mod q = b mod q; b < p * q\<rbrakk> \<Longrightarrow> a mod (p * q) = b
[PROOF STEP]
by (simp add: specializedtoprimes1)


[STATEMENT]
lemma lsided_fres: "(lsd x) = (\<top> \<le> x \<leftarrow> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd x = (\<top> \<le> x \<leftarrow> x)
[PROOF STEP]
by (simp add: fres_galois lsd_def)


[STATEMENT]
lemma lsided_fres_eq: "(lsd x) = (x \<leftarrow> x = \<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd x = (x \<leftarrow> x = \<top>)
[PROOF STEP]
using fres_galois top_le lsd_def
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> ?y \<le> ?z) = (?x \<le> ?z \<leftarrow> ?y)
\<top> \<le> ?a \<Longrightarrow> ?a = \<top>
lsd ?x = (\<top> \<cdot> ?x \<le> ?x)

goal (1 subgoal):
 1. lsd x = (x \<leftarrow> x = \<top>)
[PROOF STEP]
by force


[STATEMENT]
lemma lsided_slsided: "lsd x \<Longrightarrow> x \<cdot> x = x \<Longrightarrow> slsd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lsd x; x \<cdot> x = x\<rbrakk> \<Longrightarrow> slsd x
[PROOF STEP]
using fres_sol lsided_fres_eq slsd_def
[PROOF STATE]
proof (prove)
using this:
((?y \<leftarrow> ?x) \<cdot> ?x = ?y) = (\<exists>z. z \<cdot> ?x = ?y)
lsd ?x = (?x \<leftarrow> ?x = \<top>)
slsd ?x = (\<top> \<cdot> ?x = ?x)

goal (1 subgoal):
 1. \<lbrakk>lsd x; x \<cdot> x = x\<rbrakk> \<Longrightarrow> slsd x
[PROOF STEP]
by force


[STATEMENT]
lemma lsided_prop: "lsd x \<Longrightarrow> y \<cdot> x \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd x \<Longrightarrow> y \<cdot> x \<le> x
[PROOF STEP]
by (simp add: fres_galois lsided_fres_eq)


[STATEMENT]
lemma rsided_fres: "(rsd x) = (x \<le> x \<leftarrow> \<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rsd x = (x \<le> x \<leftarrow> \<top>)
[PROOF STEP]
by (simp add: fres_galois rsd_def)


[STATEMENT]
lemma rsided_bres: "(rsd x) = (\<top> \<le> x \<rightarrow> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rsd x = (\<top> \<le> x \<rightarrow> x)
[PROOF STEP]
by (simp add: bres_galois rsd_def)


[STATEMENT]
lemma rsided_bres_eq: "(rsd x) = (x \<rightarrow> x = \<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rsd x = (x \<rightarrow> x = \<top>)
[PROOF STEP]
using top_le rsided_bres
[PROOF STATE]
proof (prove)
using this:
\<top> \<le> ?a \<Longrightarrow> ?a = \<top>
rsd ?x = (\<top> \<le> ?x \<rightarrow> ?x)

goal (1 subgoal):
 1. rsd x = (x \<rightarrow> x = \<top>)
[PROOF STEP]
by blast


[STATEMENT]
lemma rsided_srsided: "rsd x \<Longrightarrow> x \<cdot> x = x \<Longrightarrow> srsd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rsd x; x \<cdot> x = x\<rbrakk> \<Longrightarrow> srsd x
[PROOF STEP]
using bres_sol rsided_bres_eq srsd_def
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> (?x \<rightarrow> ?y) = ?y) = (\<exists>z. ?x \<cdot> z = ?y)
rsd ?x = (?x \<rightarrow> ?x = \<top>)
srsd ?x = (?x \<cdot> \<top> = ?x)

goal (1 subgoal):
 1. \<lbrakk>rsd x; x \<cdot> x = x\<rbrakk> \<Longrightarrow> srsd x
[PROOF STEP]
by auto


[STATEMENT]
lemma rsided_prop: "rsd x \<Longrightarrow> x \<cdot> y \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rsd x \<Longrightarrow> x \<cdot> y \<le> x
[PROOF STEP]
by (simp add: bres_galois rsided_bres_eq)


[STATEMENT]
lemma lsided_top: "lsd \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd \<top>
[PROOF STEP]
by (simp add: lsd_def)


[STATEMENT]
lemma lsided_bot: "lsd \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd \<bottom>
[PROOF STEP]
by (simp add: lsd_def)


[STATEMENT]
lemma rsided_top: "rsd \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rsd \<top>
[PROOF STEP]
by (simp add: rsd_def)


[STATEMENT]
lemma rsided_bot: "rsd \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rsd \<bottom>
[PROOF STEP]
by (simp add: rsd_def)


[STATEMENT]
lemma ls_galois: "\<nu> \<stileturn> \<nu>\<^sup>\<natural>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<stileturn> \<nu>\<^sup>\<natural>
[PROOF STEP]
by (simp add: adj_def bres_galois lsl_def lsu_def)


[STATEMENT]
lemma lsl_iso: "mono \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono \<nu>
[PROOF STEP]
using adj_iso1 ls_galois
[PROOF STATE]
proof (prove)
using this:
?f \<stileturn> ?g \<Longrightarrow> mono ?f
\<nu> \<stileturn> \<nu>\<^sup>\<natural>

goal (1 subgoal):
 1. mono \<nu>
[PROOF STEP]
by blast


[STATEMENT]
lemma lsl_iso_var: "x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y
[PROOF STEP]
by (simp add: lsl_iso monoD)


[STATEMENT]
lemma lsu_iso: "mono \<nu>\<^sup>\<natural>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono \<nu>\<^sup>\<natural>
[PROOF STEP]
using adj_iso2 ls_galois
[PROOF STATE]
proof (prove)
using this:
?f \<stileturn> ?g \<Longrightarrow> mono ?g
\<nu> \<stileturn> \<nu>\<^sup>\<natural>

goal (1 subgoal):
 1. mono \<nu>\<^sup>\<natural>
[PROOF STEP]
by blast


[STATEMENT]
lemma lsu_iso_var: "x \<le> y \<Longrightarrow> \<nu>\<^sup>\<natural> x \<le> \<nu>\<^sup>\<natural> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<nu>\<^sup>\<natural> x \<le> \<nu>\<^sup>\<natural> y
[PROOF STEP]
by (simp add: lsu_iso monoD)


[STATEMENT]
lemma lsl_bot [simp]: "\<nu> \<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot_pres \<nu>
[PROOF STEP]
by (simp add: lsl_def)


[STATEMENT]
lemma lsu_top [simp]: "\<nu>\<^sup>\<natural> \<top> = \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top_pres \<nu>\<^sup>\<natural>
[PROOF STEP]
by (simp add: lsu_def bres_galois_imp top_le)


[STATEMENT]
lemma lsu_Inf_pres: "Inf_pres \<nu>\<^sup>\<natural>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf_pres \<nu>\<^sup>\<natural>
[PROOF STEP]
unfolding fun_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<nu>\<^sup>\<natural> \<circ> Inf) x = (Inf \<circ> (`) \<nu>\<^sup>\<natural>) x
[PROOF STEP]
by (metis ls_galois radj_Inf_pres)


[STATEMENT]
lemma lsl_Sup_pres: "Sup_pres (\<nu>::'a::quantale \<Rightarrow> 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_pres \<nu>
[PROOF STEP]
by (simp add: fun_eq_iff, metis SUP_cong Sup_distl lsl_def)


[STATEMENT]
lemma lsu_Inf_closed: "Inf_closed_set (range \<nu>\<^sup>\<natural>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf_closed_set (range \<nu>\<^sup>\<natural>)
[PROOF STEP]
by (simp add: Inf_pres_Inf_closed lsu_Inf_pres)


[STATEMENT]
lemma lsl_Sup_closed: "Sup_closed_set (range (\<nu>::'a::quantale \<Rightarrow> 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_closed_set (range \<nu>)
[PROOF STEP]
by (simp add: Sup_pres_Sup_closed lsl_Sup_pres)


[STATEMENT]
lemma lsl_lsu_canc1: "\<nu> \<circ> \<nu>\<^sup>\<natural> \<le> id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<circ> \<nu>\<^sup>\<natural> \<le> id
[PROOF STEP]
by (simp add: adj_cancel1 ls_galois)


[STATEMENT]
lemma lsl_lsu_canc2: "id \<le> \<nu>\<^sup>\<natural> \<circ> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id \<le> \<nu>\<^sup>\<natural> \<circ> \<nu>
[PROOF STEP]
by (simp add: adj_cancel2 ls_galois)


[STATEMENT]
lemma clop_lsu_lsl: "clop (\<nu>\<^sup>\<natural> \<circ> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clop (\<nu>\<^sup>\<natural> \<circ> \<nu>)
[PROOF STEP]
by (simp add: clop_adj ls_galois)


[STATEMENT]
lemma coclop_lsl_lsu: "coclop (\<nu> \<circ> \<nu>\<^sup>\<natural>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coclop (\<nu> \<circ> \<nu>\<^sup>\<natural>)
[PROOF STEP]
by (simp add: coclop_adj ls_galois)


[STATEMENT]
lemma dang1: "\<nu> (\<nu> x \<sqinter> y) \<le> \<nu> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<sqinter> y) \<le> \<nu> x
[PROOF STEP]
unfolding lsl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> \<cdot> (\<top> \<cdot> x \<sqinter> y) \<le> \<top> \<cdot> x
[PROOF STEP]
by (metis bres_galois bres_interchange bres_top_top inf.coboundedI1)


[STATEMENT]
lemma lsl_trans: "\<nu> \<circ> \<nu> \<le> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<circ> \<nu> \<le> \<nu>
[PROOF STEP]
unfolding lsl_def fun_eq_iff comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<top> \<cdot> (\<top> \<cdot> x)) \<le> (\<cdot>) \<top>
[PROOF STEP]
by (metis (no_types, lifting) bres_galois bres_interchange bres_top_top le_funI)


[STATEMENT]
lemma lsl_lsu_prop: "\<nu> \<circ> \<nu>\<^sup>\<natural> \<le> \<nu>\<^sup>\<natural>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<circ> \<nu>\<^sup>\<natural> \<le> \<nu>\<^sup>\<natural>
[PROOF STEP]
unfolding le_fun_def comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<nu> (\<nu>\<^sup>\<natural> x) \<le> \<nu>\<^sup>\<natural> x
[PROOF STEP]
by (metis adj_def dang1 dual_order.trans le_iff_inf ls_galois order_refl top_greatest)


[STATEMENT]
lemma lsu_lsl_prop: "\<nu> \<le> \<nu>\<^sup>\<natural> \<circ> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<le> \<nu>\<^sup>\<natural> \<circ> \<nu>
[PROOF STEP]
unfolding le_fun_def comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<nu> x \<le> \<nu>\<^sup>\<natural> (\<nu> x)
[PROOF STEP]
by (metis adj_def comp_def le_fun_def ls_galois lsl_trans)


[STATEMENT]
lemma lsided_eq: "lsd = slsd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd = slsd
[PROOF STEP]
unfolding fun_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. lsd x = slsd x
[PROOF STEP]
by (simp add: order.eq_iff le_top lsd_def slsd_def)


[STATEMENT]
lemma lsided_eq_var1:  "(x \<le> \<top> \<rightarrow> x) = (x = \<top> \<rightarrow> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> \<top> \<rightarrow> x) = (x = \<top> \<rightarrow> x)
[PROOF STEP]
using bres_galois dual_order.trans order.eq_iff le_top
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> ?y \<le> ?z) = (?y \<le> ?x \<rightarrow> ?z)
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
(?a = ?b) = (?a \<le> ?b \<and> ?b \<le> ?a)
?x \<le> \<top> \<cdot> ?x

goal (1 subgoal):
 1. (x \<le> \<top> \<rightarrow> x) = (x = \<top> \<rightarrow> x)
[PROOF STEP]
by blast


[STATEMENT]
lemma lsided_eq_var2: "lsd x = (x = \<top> \<rightarrow> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd x = (x = \<top> \<rightarrow> x)
[PROOF STEP]
using bres_galois lsided_eq lsided_eq_var1 lsd_def
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> ?y \<le> ?z) = (?y \<le> ?x \<rightarrow> ?z)
lsd = slsd
(?x \<le> \<top> \<rightarrow> ?x) = (?x = \<top> \<rightarrow> ?x)
lsd ?x = (\<top> \<cdot> ?x \<le> ?x)

goal (1 subgoal):
 1. lsd x = (x = \<top> \<rightarrow> x)
[PROOF STEP]
by simp


[STATEMENT]
lemma lsided_def3: "(\<nu> (x::'a::unital_quantale) = x) = (\<nu>\<^sup>\<natural> x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> x = x) = (\<nu>\<^sup>\<natural> x = x)
[PROOF STEP]
unfolding lsl_def lsu_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<top> \<cdot> x = x) = (\<top> \<rightarrow> x = x)
[PROOF STEP]
by (metis lsided_eq lsided_eq_var2 slsd_def)


[STATEMENT]
lemma Fix_lsl_lsu: "Fix (\<nu>::'a::unital_quantale \<Rightarrow> 'a) = Fix \<nu>\<^sup>\<natural>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fix \<nu> = Fix \<nu>\<^sup>\<natural>
[PROOF STEP]
unfolding Fix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<nu> x = x} = {x. \<nu>\<^sup>\<natural> x = x}
[PROOF STEP]
by (simp add: lsided_def3)


[STATEMENT]
lemma Fix_lsl_left_slsided: "Fix \<nu> = {(x::'a::unital_quantale). lsd x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fix \<nu> = {x. lsd x}
[PROOF STEP]
unfolding Fix_def lsl_def lsd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<top> \<cdot> x = x} = {x. \<top> \<cdot> x \<le> x}
[PROOF STEP]
using order.eq_iff le_top
[PROOF STATE]
proof (prove)
using this:
(?a = ?b) = (?a \<le> ?b \<and> ?b \<le> ?a)
?x \<le> \<top> \<cdot> ?x

goal (1 subgoal):
 1. {x. \<top> \<cdot> x = x} = {x. \<top> \<cdot> x \<le> x}
[PROOF STEP]
by blast


[STATEMENT]
lemma Fix_lsl_iff [simp]: "(x \<in> Fix \<nu>) = (\<nu> x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> Fix \<nu>) = (\<nu> x = x)
[PROOF STEP]
by (simp add: Fix_def)


[STATEMENT]
lemma lsl_lsu_prop_eq [simp]: "(\<nu>::'a::unital_quantale \<Rightarrow> 'a) \<circ> \<nu>\<^sup>\<natural> = \<nu>\<^sup>\<natural>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<circ> \<nu>\<^sup>\<natural> = \<nu>\<^sup>\<natural>
[PROOF STEP]
by (smt antisym clop_extensive_var clop_lsu_lsl comp_apply le_fun_def lsided_eq_var1 lsl_lsu_prop lsu_def lsu_lsl_prop)


[STATEMENT]
lemma lsu_lsl_prop_eq [simp]: "\<nu>\<^sup>\<natural> \<circ> \<nu> = (\<nu>::'a::unital_quantale \<Rightarrow> 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> \<circ> \<nu> = \<nu>
[PROOF STEP]
by (metis adj_cancel_eq1 ls_galois lsl_lsu_prop_eq)


[STATEMENT]
lemma lsl_clop: "clop (\<nu>::'a::unital_quantale \<Rightarrow> 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clop \<nu>
[PROOF STEP]
by (metis clop_lsu_lsl lsu_lsl_prop_eq)


[STATEMENT]
lemma lsu_coclop: "coclop (\<nu>\<^sup>\<natural>::'a::unital_quantale \<Rightarrow> 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coclop \<nu>\<^sup>\<natural>
[PROOF STEP]
by (metis coclop_lsl_lsu lsl_lsu_prop_eq)


[STATEMENT]
lemma lsl_range_fix: "range (\<nu>::'a::unital_quantale \<Rightarrow> 'a) = Fix \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range \<nu> = Fix \<nu>
[PROOF STEP]
by (simp add: clop_closure_set lsl_clop)


[STATEMENT]
lemma lsu_range_fix: "range (\<nu>\<^sup>\<natural>::'a::unital_quantale \<Rightarrow> 'a) = Fix \<nu>\<^sup>\<natural>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range \<nu>\<^sup>\<natural> = Fix \<nu>\<^sup>\<natural>
[PROOF STEP]
by (simp add: coclop_coclosure_set lsu_coclop)


[STATEMENT]
lemma range_lsl_iff [simp]: "((x::'a::unital_quantale) \<in> range \<nu>) = (\<nu> x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> range \<nu>) = (\<nu> x = x)
[PROOF STEP]
by (simp add: lsl_range_fix)


[STATEMENT]
lemma range_lsu_iff [simp]: "((x::'a::unital_quantale) \<in> range \<nu>\<^sup>\<natural>) = (\<nu>\<^sup>\<natural> x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> range \<nu>\<^sup>\<natural>) = (\<nu>\<^sup>\<natural> x = x)
[PROOF STEP]
by (simp add: lsu_range_fix)


[STATEMENT]
lemma lsu_Sup_closed: "Sup_closed_set (Fix (\<nu>\<^sup>\<natural>::'a::unital_quantale \<Rightarrow> 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_closed_set (Fix \<nu>\<^sup>\<natural>)
[PROOF STEP]
by (metis Fix_lsl_lsu lsl_Sup_closed lsl_range_fix)


[STATEMENT]
lemma lsl_Inf_closed: "Inf_closed_set (Fix (\<nu>::'a::unital_quantale \<Rightarrow> 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf_closed_set (Fix \<nu>)
[PROOF STEP]
by (metis Fix_lsl_lsu lsu_Inf_closed lsu_range_fix)


[STATEMENT]
lemma lsu_lax: "\<nu>\<^sup>\<natural> (x::'a::unital_quantale) \<cdot> \<nu>\<^sup>\<natural> y \<le> \<nu>\<^sup>\<natural> (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> y \<le> \<nu>\<^sup>\<natural> (x \<cdot> y)
[PROOF STEP]
unfolding lsu_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<top> \<rightarrow> x) \<cdot> (\<top> \<rightarrow> y) \<le> \<top> \<rightarrow> x \<cdot> y
[PROOF STEP]
by (meson bres_canc1 bres_galois bres_interchange le_top order_trans)


[STATEMENT]
lemma lsu_one: "\<nu>\<^sup>\<natural> 1 \<le> (1::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (1::'a) \<le> (1::'a)
[PROOF STEP]
unfolding lsu_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> \<rightarrow> (1::'a) \<le> (1::'a)
[PROOF STEP]
using bres_canc1 dual_order.trans le_top
[PROOF STATE]
proof (prove)
using this:
?x \<cdot> (?x \<rightarrow> ?y) \<le> ?y
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
?x \<le> \<top> \<cdot> ?x

goal (1 subgoal):
 1. \<top> \<rightarrow> (1::'a) \<le> (1::'a)
[PROOF STEP]
by blast


[STATEMENT]
lemma lsl_one: "1 \<le> \<nu> (1::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> \<nu> (1::'a)
[PROOF STEP]
unfolding lsl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> \<top> \<cdot> (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma lsu_conuc: "conucleus (\<nu>\<^sup>\<natural>::'a::unital_quantale \<Rightarrow> 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conucleus \<nu>\<^sup>\<natural>
[PROOF STEP]
by (simp add: lsu_coclop conucleus_def lsu_lax)


[STATEMENT]
lemma lsu_comp_closed_var [simp]: "\<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> (y::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> y
[PROOF STEP]
by (simp add: conuc_comp_closed lsu_conuc)


[STATEMENT]
lemma lsu_comp_closed: "comp_closed_set (Fix (\<nu>\<^sup>\<natural>::'a::unital_quantale \<Rightarrow> 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_closed_set (Fix \<nu>\<^sup>\<natural>)
[PROOF STEP]
by (simp add: conuc_Sup_qclosed lsu_conuc)


[STATEMENT]
lemma "\<nu> x \<cdot> \<nu> y \<le> \<nu> (x \<cdot> (y::'a::unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<cdot> \<nu> y \<le> \<nu> (x \<cdot> y)
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<cdot> \<nu> y \<le> \<nu> (x \<cdot> y)
[PROOF STEP]
oops


[STATEMENT]
lemma lsl_comp_closed: "comp_closed_set (Fix (\<nu>::'a::unital_quantale \<Rightarrow> 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_closed_set (Fix \<nu>)
[PROOF STEP]
by (simp add: Fix_lsl_lsu lsu_comp_closed)


[STATEMENT]
lemma lsl_comp_closed_var [simp]: "\<nu> (\<nu> x \<cdot> \<nu> (y::'a::unital_quantale)) = \<nu> x \<cdot> \<nu> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<cdot> \<nu> y) = \<nu> x \<cdot> \<nu> y
[PROOF STEP]
by (metis Fix_lsl_iff lsl_def lsl_range_fix mult.assoc rangeI)


[STATEMENT]
lemma lsl_lsu_ran: "range \<nu>\<^sup>\<natural> = range (\<nu>::'a::unital_quantale \<Rightarrow> 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range \<nu>\<^sup>\<natural> = range \<nu>
[PROOF STEP]
by (simp add: Fix_lsl_lsu lsl_range_fix lsu_range_fix)


[STATEMENT]
lemma lsl_top [simp]: "\<nu> \<top> = (\<top>::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top_pres \<nu>
[PROOF STEP]
by (simp add: clop_top lsl_clop)


[STATEMENT]
lemma lsu_bot [simp]: "\<nu>\<^sup>\<natural> \<bottom> = (\<bottom>::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot_pres \<nu>\<^sup>\<natural>
[PROOF STEP]
using lsided_def3 lsl_bot
[PROOF STATE]
proof (prove)
using this:
(\<nu> ?x = ?x) = (\<nu>\<^sup>\<natural> ?x = ?x)
bot_pres \<nu>

goal (1 subgoal):
 1. bot_pres \<nu>\<^sup>\<natural>
[PROOF STEP]
by blast


[STATEMENT]
lemma lsu_inj_on: "inj_on \<nu>\<^sup>\<natural> (Fix (\<nu>\<^sup>\<natural>::'a::unital_quantale \<Rightarrow> 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on \<nu>\<^sup>\<natural> (Fix \<nu>\<^sup>\<natural>)
[PROOF STEP]
by (metis coclop_coclosure inj_onI lsu_coclop lsu_range_fix)


[STATEMENT]
lemma lsl_inj_on: "inj_on \<nu> (Fix (\<nu>::'a::unital_quantale \<Rightarrow> 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on \<nu> (Fix \<nu>)
[PROOF STEP]
by (metis clop_closure inj_onI lsl_clop lsl_range_fix)


[STATEMENT]
lemma lsl_Inf_closed_var [simp]: "\<nu> (\<Sqinter>x \<in> X. \<nu> x) = (\<Sqinter>x \<in> X.  \<nu> (x::'a::unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<Sqinter> (\<nu> ` X)) = \<Sqinter> (\<nu> ` X)
[PROOF STEP]
by (metis (no_types, opaque_lifting) INF_image lsided_def3 lsu_Inf_pres lsu_lsl_prop_eq o_apply)


[STATEMENT]
lemma lsl_Sup_closed_var [simp]: "\<nu> (\<Squnion>x \<in> X. \<nu> x) = (\<Squnion>x \<in> X. \<nu> (x::'a::unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<Squnion> (\<nu> ` X)) = \<Squnion> (\<nu> ` X)
[PROOF STEP]
unfolding lsl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> \<cdot> \<Squnion> ((\<cdot>) \<top> ` X) = \<Squnion> ((\<cdot>) \<top> ` X)
[PROOF STEP]
by (metis Sup_distl mult.assoc top_times_top)


[STATEMENT]
lemma lsu_Inf_closed_var [simp]: "\<nu>\<^sup>\<natural> (\<Sqinter>x \<in> X. \<nu>\<^sup>\<natural> x) = (\<Sqinter>x \<in> X. \<nu>\<^sup>\<natural> (x::'a::unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<Sqinter> (\<nu>\<^sup>\<natural> ` X)) = \<Sqinter> (\<nu>\<^sup>\<natural> ` X)
[PROOF STEP]
by (metis INF_image lsided_def3 lsl_Inf_closed_var lsl_lsu_prop_eq)


[STATEMENT]
lemma lsu_Sup_closed_var [simp]: "\<nu>\<^sup>\<natural> (\<Squnion>x \<in> X. \<nu>\<^sup>\<natural> x) = (\<Squnion>x \<in> X. \<nu>\<^sup>\<natural> (x::'a::unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<Squnion> (\<nu>\<^sup>\<natural> ` X)) = \<Squnion> (\<nu>\<^sup>\<natural> ` X)
[PROOF STEP]
by (metis SUP_image lsided_def3 lsl_Sup_closed_var lsl_lsu_prop_eq)


[STATEMENT]
lemma lsl_inf_closed_var [simp]: "\<nu> (\<nu> x \<sqinter> \<nu> y) = \<nu> (x::'a::unital_quantale) \<sqinter> \<nu> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<sqinter> \<nu> y) = \<nu> x \<sqinter> \<nu> y
[PROOF STEP]
by (smt antisym clop_extensive_var dang1 inf_sup_aci(1) le_inf_iff lsl_clop)


[STATEMENT]
lemma lsl_sup_closed_var [simp]: "\<nu> (\<nu> x \<squnion> \<nu> y) = \<nu> (x::'a::unital_quantale) \<squnion> \<nu> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<squnion> \<nu> y) = \<nu> x \<squnion> \<nu> y
[PROOF STEP]
by (meson Sup_sup_closed lsl_Sup_closed range_eqI range_lsl_iff sup_closed_set_def)


[STATEMENT]
lemma lsu_inf_closed_var [simp]: "\<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<sqinter> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> (x::'a::unital_quantale) \<sqinter> \<nu>\<^sup>\<natural> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<sqinter> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<sqinter> \<nu>\<^sup>\<natural> y
[PROOF STEP]
by (metis (no_types, lifting) lsided_def3 lsl_inf_closed_var lsl_lsu_prop_eq o_apply)


[STATEMENT]
lemma lsu_sup_closed_var [simp]: "\<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> (x::'a::unital_quantale) \<squnion> \<nu>\<^sup>\<natural> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y
[PROOF STEP]
by (metis (no_types, lifting) lsided_def3 lsl_lsu_prop_eq lsl_sup_closed_var o_def)


[STATEMENT]
lemma lsu_fres_closed [simp]: "\<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<leftarrow> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<leftarrow> \<nu>\<^sup>\<natural> (y::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<leftarrow> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<leftarrow> \<nu>\<^sup>\<natural> y
[PROOF STEP]
unfolding lsu_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> \<rightarrow> \<top> \<rightarrow> x \<leftarrow> (\<top> \<rightarrow> y) = \<top> \<rightarrow> x \<leftarrow> (\<top> \<rightarrow> y)
[PROOF STEP]
by (simp add: bres_curry fres_bres)


[STATEMENT]
lemma lsl_fres_closed [simp]: "\<nu> (\<nu> x \<leftarrow> \<nu> y) = \<nu> x \<leftarrow> \<nu> (y::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<leftarrow> \<nu> y) = \<nu> x \<leftarrow> \<nu> y
[PROOF STEP]
unfolding lsl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> \<cdot> (\<top> \<cdot> x \<leftarrow> \<top> \<cdot> y) = \<top> \<cdot> x \<leftarrow> \<top> \<cdot> y
[PROOF STEP]
by (metis fres_interchange lsd_def lsided_eq mult.assoc slsd_def top_times_top)


[STATEMENT]
lemma lsl_almost_lax: "x \<cdot> \<nu> y \<le> \<nu> (y::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> \<nu> y \<le> \<nu> y
[PROOF STEP]
by (metis inf_top.right_neutral lsided_eq lsided_prop lsl_def lsl_inf_closed_var mult.right_neutral slsd_def)


[STATEMENT]
lemma "\<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> (y::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu> (\<nu> x \<rightarrow> \<nu> y) = \<nu> x \<rightarrow> \<nu> (y::'a::unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<rightarrow> \<nu> y) = \<nu> x \<rightarrow> \<nu> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<rightarrow> \<nu> y) = \<nu> x \<rightarrow> \<nu> y
[PROOF STEP]
oops


[STATEMENT]
lemma lsided_times_top: "lsd (\<top> \<cdot> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd (\<top> \<cdot> x)
[PROOF STEP]
by (metis lsd_def mult_isor top_greatest mult_assoc)


[STATEMENT]
lemma lsided_le2: "lsd x \<Longrightarrow> x \<cdot> y \<le> x \<sqinter> (y \<cdot> \<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd x \<Longrightarrow> x \<cdot> y \<le> x \<sqinter> (y \<cdot> \<top>)
[PROOF STEP]
using lsided_prop psrpq.mult_isol mult_commute
[PROOF STATE]
proof (prove)
using this:
lsd ?x \<Longrightarrow> ?y \<cdot> ?x \<le> ?x
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y
?a \<cdot> ?b = ?b \<cdot> ?a

goal (1 subgoal):
 1. lsd x \<Longrightarrow> x \<cdot> y \<le> x \<sqinter> (y \<cdot> \<top>)
[PROOF STEP]
by auto


[STATEMENT]
lemma lsided_le3: "lsd x \<Longrightarrow> (x \<sqinter> y) \<cdot> z \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd x \<Longrightarrow> x \<sqinter> y \<cdot> z \<le> x
[PROOF STEP]
by (metis inf_le1 lsided_prop mult_isol order_trans mult_commute)


[STATEMENT]
lemma lsided_le4: "lsd x \<Longrightarrow> (x \<sqinter> y) \<cdot> z \<le> x \<sqinter> (y \<cdot> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsd x \<Longrightarrow> x \<sqinter> y \<cdot> z \<le> x \<sqinter> (y \<cdot> z)
[PROOF STEP]
by (simp add: mult_isor lsided_le3)


[STATEMENT]
lemma lsided_times_le_inf: "lsd x \<Longrightarrow> lsd y \<Longrightarrow> x \<cdot> y \<le> x \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lsd x; lsd y\<rbrakk> \<Longrightarrow> x \<cdot> y \<le> x \<sqinter> y
[PROOF STEP]
using lsided_prop lsided_le2
[PROOF STATE]
proof (prove)
using this:
lsd ?x \<Longrightarrow> ?y \<cdot> ?x \<le> ?x
lsd ?x \<Longrightarrow> ?x \<cdot> ?y \<le> ?x \<sqinter> (?y \<cdot> \<top>)

goal (1 subgoal):
 1. \<lbrakk>lsd x; lsd y\<rbrakk> \<Longrightarrow> x \<cdot> y \<le> x \<sqinter> y
[PROOF STEP]
by force


[STATEMENT]
lemma lsl_lax: "\<nu> x \<cdot> \<nu> y \<le> \<nu> (x \<cdot> (y::'aa::ab_unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<cdot> \<nu> y \<le> \<nu> (x \<cdot> y)
[PROOF STEP]
by (metis (no_types, opaque_lifting) lsl_almost_lax lsl_def mult.commute mult.left_commute)


[STATEMENT]
lemma lsl_nuc: "nucleus (\<nu>::'a::ab_unital_quantale \<Rightarrow> 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nucleus \<nu>
[PROOF STEP]
by (simp add: lsl_clop nucleus_def lsl_lax)


[STATEMENT]
lemma lsl_comp_pres: "\<nu> (x \<cdot> y) = \<nu> x \<cdot> \<nu> (y::'a::ab_unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (x \<cdot> y) = \<nu> x \<cdot> \<nu> y
[PROOF STEP]
by (metis (no_types, lifting) lsl_comp_closed_var lsl_nuc nuc_prop1 nuc_prop2)


[STATEMENT]
lemma lsl_bres_closed [simp]: "\<nu> (\<nu> x \<rightarrow> \<nu> y) = \<nu> x \<rightarrow> \<nu> (y::'a::ab_unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (\<nu> x \<rightarrow> \<nu> y) = \<nu> x \<rightarrow> \<nu> y
[PROOF STEP]
by (simp add: lsl_nuc nuc_bres_closed)


[STATEMENT]
lemma lsu_bres_pres [simp]: "\<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> (y::'a::ab_unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y) = \<nu>\<^sup>\<natural> x \<rightarrow> \<nu>\<^sup>\<natural> y
[PROOF STEP]
by (simp add: bres_fres_eq)


[STATEMENT]
lemma lsl_prelocalic_var: "\<nu> x \<cdot> y \<le> \<nu> x \<sqinter> \<nu> (y::'a::ab_unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<cdot> y \<le> \<nu> x \<sqinter> \<nu> y
[PROOF STEP]
by (metis inf_top.right_neutral lsided_le4 lsided_times_top lsl_def)


[STATEMENT]
lemma dang3: "(\<nu> x \<sqinter> y) \<cdot> z \<le> \<nu> x \<sqinter> (y \<cdot> (z::'a::ab_unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<sqinter> y \<cdot> z \<le> \<nu> x \<sqinter> (y \<cdot> z)
[PROOF STEP]
by (metis lsided_le4 lsided_times_top lsl_def)


[STATEMENT]
lemma lsl_prelocalic: "\<nu> x \<cdot> \<nu> y \<le> \<nu> x \<sqinter> \<nu> (y::'a::ab_unital_quantale)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<cdot> \<nu> y \<le> \<nu> x \<sqinter> \<nu> y
[PROOF STEP]
by (metis lsided_times_le_inf lsided_times_top lsl_def)


[STATEMENT]
lemma lsl_local: "x \<cdot> \<nu> y \<le> \<nu> (x \<cdot> (y::'a::ab_unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> \<nu> y \<le> \<nu> (x \<cdot> y)
[PROOF STEP]
by (simp add: lsl_def mult.left_commute)


[STATEMENT]
lemma lsl_rpc [simp]: "\<nu> (rpc x y) = rpc x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (rpc x y) = rpc x y
[PROOF STEP]
by (metis lsl_lsu_prop_eq o_apply rpc_def)


[STATEMENT]
lemma lsu_rpc [simp]: "\<nu>\<^sup>\<natural> (rpc x y) = rpc x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (rpc x y) = rpc x y
[PROOF STEP]
using lsided_def3 lsl_rpc
[PROOF STATE]
proof (prove)
using this:
(\<nu> ?x = ?x) = (\<nu>\<^sup>\<natural> ?x = ?x)
\<nu> (rpc ?x ?y) = rpc ?x ?y

goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (rpc x y) = rpc x y
[PROOF STEP]
by blast


[STATEMENT]
lemma lsl_rpc_galois: "(x \<sqinter> \<nu> z \<le> y) = (z \<le> rpc x (y::'a::bool_unital_quantale))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> \<nu> z \<le> y) = (z \<le> rpc x y)
[PROOF STEP]
unfolding rpc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> \<nu> z \<le> y) = (z \<le> \<nu>\<^sup>\<natural> (- x \<squnion> y))
[PROOF STEP]
by (metis adj_def inf_commute ls_galois shunt1)


[STATEMENT]
lemma lsl_rpc_galois_var: "x \<sqinter> \<nu> z \<le> y \<longleftrightarrow> \<nu> z \<le> rpc x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> \<nu> z \<le> y) = (\<nu> z \<le> rpc x y)
[PROOF STEP]
by (metis adj_def ls_galois lsl_rpc_galois lsu_rpc)


[STATEMENT]
lemma rpc_expl_aux: "\<Squnion>{z. x \<sqinter> \<nu> z \<le> y} = \<Squnion>{z. x \<sqinter> z \<le> y \<and> \<nu> z = (z::'a::bool_unital_quantale)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {z. x \<sqinter> \<nu> z \<le> y} = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Squnion> {z. x \<sqinter> \<nu> z \<le> y} \<le> \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
 2. \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z} \<le> \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}
[PROOF STEP]
show "\<Squnion>{z. x \<sqinter> \<nu> z \<le> y} \<le> \<Squnion>{z. x \<sqinter> z \<le> y \<and> \<nu> z = z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {z. x \<sqinter> \<nu> z \<le> y} \<le> \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
apply (rule Sup_mono, safe)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. x \<sqinter> \<nu> a \<le> y \<Longrightarrow> \<exists>b\<in>{z. x \<sqinter> z \<le> y \<and> \<nu> z = z}. a \<le> b
[PROOF STEP]
by (smt lsided_eq lsided_prop lsl_def lsl_lsu_prop_eq lsl_rpc_galois mem_Collect_eq o_apply rpc_def slsd_def)
[PROOF STATE]
proof (state)
this:
\<Squnion> {z. x \<sqinter> \<nu> z \<le> y} \<le> \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}

goal (1 subgoal):
 1. \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z} \<le> \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}
[PROOF STEP]
show " \<Squnion>{z. x \<sqinter> z \<le> y \<and> \<nu> z = z} \<le> \<Squnion>{z. x \<sqinter> \<nu> z \<le> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z} \<le> \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}
[PROOF STEP]
by (simp add: Collect_mono_iff Sup_subset_mono)
[PROOF STATE]
proof (state)
this:
\<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z} \<le> \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rpc_expl: "rpc x y = \<Squnion>{z. x \<sqinter> z \<le> y \<and> \<nu> z = (z::'a::bool_unital_quantale)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
have "rpc x y = \<Squnion>{z. z \<le> rpc x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. z \<le> rpc x y}
[PROOF STEP]
using Sup_atMost atMost_def
[PROOF STATE]
proof (prove)
using this:
\<Squnion> {..?y} = ?y
{..?u} \<equiv> {x. x \<le> ?u}

goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. z \<le> rpc x y}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
rpc x y = \<Squnion> {z. z \<le> rpc x y}

goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rpc x y = \<Squnion> {z. z \<le> rpc x y}

goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
have "... = \<Squnion>{z. x \<sqinter> \<nu> z \<le> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {z. z \<le> rpc x y} = \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}
[PROOF STEP]
using lsl_rpc_galois
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> \<nu> ?z \<le> ?y) = (?z \<le> rpc ?x ?y)

goal (1 subgoal):
 1. \<Squnion> {z. z \<le> rpc x y} = \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<Squnion> {z. z \<le> rpc x y} = \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}

goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rpc x y = \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rpc x y = \<Squnion> {z. x \<sqinter> \<nu> z \<le> y}

goal (1 subgoal):
 1. rpc x y = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}
[PROOF STEP]
by (simp add: rpc_expl_aux)
[PROOF STATE]
proof (state)
this:
rpc x y = \<Squnion> {z. x \<sqinter> z \<le> y \<and> \<nu> z = z}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "\<nu>\<^sup>\<natural> (x \<cdot> y) = \<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (x \<cdot> y) = \<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> y
[PROOF STEP]
(*nitpick    *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (x \<cdot> y) = \<nu>\<^sup>\<natural> x \<cdot> \<nu>\<^sup>\<natural> y
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu> 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. un_pres \<nu>
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. un_pres \<nu>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu>\<^sup>\<natural> x = \<nu> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> x = \<nu> x
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> x = \<nu> x
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu>\<^sup>\<natural> (\<Squnion> P) = \<Squnion>{\<nu>\<^sup>\<natural> p |p. p \<in> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<Squnion> P) = \<Squnion> {\<nu>\<^sup>\<natural> p |p. p \<in> P}
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (\<Squnion> P) = \<Squnion> {\<nu>\<^sup>\<natural> p |p. p \<in> P}
[PROOF STEP]
oops


[STATEMENT]
lemma "rpc (\<nu>\<^sup>\<natural> x) (\<nu>\<^sup>\<natural> y) = -(\<nu>\<^sup>\<natural> x) \<squnion> (\<nu>\<^sup>\<natural> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rpc (\<nu>\<^sup>\<natural> x) (\<nu>\<^sup>\<natural> y) = - \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rpc (\<nu>\<^sup>\<natural> x) (\<nu>\<^sup>\<natural> y) = - \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y
[PROOF STEP]
oops


[STATEMENT]
lemma "rpc (\<nu> x) (\<nu> y) = -(\<nu> x) \<squnion> (\<nu> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rpc (\<nu> x) (\<nu> y) = - \<nu> x \<squnion> \<nu> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rpc (\<nu> x) (\<nu> y) = - \<nu> x \<squnion> \<nu> y
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu> (-(\<nu>\<^sup>\<natural> x) \<squnion> (\<nu>\<^sup>\<natural> y)) = -(\<nu>\<^sup>\<natural> x) \<squnion> (\<nu>\<^sup>\<natural> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y) = - \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y) = - \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu> (-(\<nu> x) \<squnion> (\<nu> y)) = -(\<nu> x) \<squnion> (\<nu> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu> x \<squnion> \<nu> y) = - \<nu> x \<squnion> \<nu> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu> x \<squnion> \<nu> y) = - \<nu> x \<squnion> \<nu> y
[PROOF STEP]
oops


[STATEMENT]
lemma  "\<nu> x \<cdot> \<nu> y = \<nu> x \<sqinter> \<nu> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<cdot> \<nu> y = \<nu> x \<sqinter> \<nu> y
[PROOF STEP]
(*nitpick this rules out localic nuclei.*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> x \<cdot> \<nu> y = \<nu> x \<sqinter> \<nu> y
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu> (- (\<nu> x)) = - (\<nu> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu> x) = - \<nu> x
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu> x) = - \<nu> x
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu>\<^sup>\<natural> (- (\<nu>\<^sup>\<natural> x)) = - (\<nu>\<^sup>\<natural> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (- \<nu>\<^sup>\<natural> x) = - \<nu>\<^sup>\<natural> x
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (- \<nu>\<^sup>\<natural> x) = - \<nu>\<^sup>\<natural> x
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu> (- (\<nu> x) \<squnion> (\<nu> y)) = - (\<nu> x) \<squnion> (\<nu> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu> x \<squnion> \<nu> y) = - \<nu> x \<squnion> \<nu> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> (- \<nu> x \<squnion> \<nu> y) = - \<nu> x \<squnion> \<nu> y
[PROOF STEP]
oops


[STATEMENT]
lemma "\<nu>\<^sup>\<natural> (- (\<nu>\<^sup>\<natural> x) \<squnion> (\<nu>\<^sup>\<natural> y)) = - (\<nu>\<^sup>\<natural> x) \<squnion> (\<nu>\<^sup>\<natural> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (- \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y) = - \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>\<^sup>\<natural> (- \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y) = - \<nu>\<^sup>\<natural> x \<squnion> \<nu>\<^sup>\<natural> y
[PROOF STEP]
oops


[STATEMENT]
lemma Conversion_props [simp]: "LengthF c > 0" "MassF c > 0" "TimeF c > 0" "CurrentF c > 0"
  "TemperatureF c > 0" "AmountF c > 0" "IntensityF c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < LengthF c &&& 0 < MassF c &&& 0 < TimeF c) &&& (0 < CurrentF c &&& 0 < TemperatureF c) &&& 0 < AmountF c &&& 0 < IntensityF c
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma convinv_inverse [simp]: "convinv (convinv c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv\<^sub>C (inv\<^sub>C c) = c
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma convcomp_inv [simp]: "c \<circ>\<^sub>C inv\<^sub>C c = id\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<circ>\<^sub>C inv\<^sub>C c = id\<^sub>C
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma inv_convcomp [simp]: "inv\<^sub>C c \<circ>\<^sub>C c = id\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv\<^sub>C c \<circ>\<^sub>C c = id\<^sub>C
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma Conversion_invs [simp]: "LengthF (inv\<^sub>C x) = inverse (LengthF x)" "MassF (inv\<^sub>C x) = inverse (MassF x)"
  "TimeF (inv\<^sub>C x) = inverse (TimeF x)" "CurrentF (inv\<^sub>C x) = inverse (CurrentF x)"
  "TemperatureF (inv\<^sub>C x) = inverse (TemperatureF x)" "AmountF (inv\<^sub>C x) = inverse (AmountF x)"
  "IntensityF (inv\<^sub>C x) = inverse (IntensityF x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LengthF (inv\<^sub>C x) = inverse (LengthF x) &&& MassF (inv\<^sub>C x) = inverse (MassF x) &&& TimeF (inv\<^sub>C x) = inverse (TimeF x)) &&& (CurrentF (inv\<^sub>C x) = inverse (CurrentF x) &&& TemperatureF (inv\<^sub>C x) = inverse (TemperatureF x)) &&& AmountF (inv\<^sub>C x) = inverse (AmountF x) &&& IntensityF (inv\<^sub>C x) = inverse (IntensityF x)
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma Conversion_comps [simp]: "LengthF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = LengthF c\<^sub>1 * LengthF c\<^sub>2"
  "MassF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = MassF c\<^sub>1 * MassF c\<^sub>2"
  "TimeF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = TimeF c\<^sub>1 * TimeF c\<^sub>2"
  "CurrentF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = CurrentF c\<^sub>1 * CurrentF c\<^sub>2"
  "TemperatureF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = TemperatureF c\<^sub>1 * TemperatureF c\<^sub>2"
  "AmountF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = AmountF c\<^sub>1 * AmountF c\<^sub>2"
  "IntensityF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = IntensityF c\<^sub>1 * IntensityF c\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LengthF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = LengthF c\<^sub>1 \<cdot> LengthF c\<^sub>2 &&& MassF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = MassF c\<^sub>1 \<cdot> MassF c\<^sub>2 &&& TimeF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = TimeF c\<^sub>1 \<cdot> TimeF c\<^sub>2) &&& (CurrentF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = CurrentF c\<^sub>1 \<cdot> CurrentF c\<^sub>2 &&& TemperatureF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = TemperatureF c\<^sub>1 \<cdot> TemperatureF c\<^sub>2) &&& AmountF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = AmountF c\<^sub>1 \<cdot> AmountF c\<^sub>2 &&& IntensityF (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) = IntensityF c\<^sub>1 \<cdot> IntensityF c\<^sub>2
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma dconvfactor_pos [simp]: "dconvfactor c d > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < dconvfactor c d
[PROOF STEP]
by (simp add: dconvfactor_def)


[STATEMENT]
lemma dconvfactor_nz [simp]: "dconvfactor c d \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dconvfactor c d \<noteq> 0
[PROOF STEP]
by (metis dconvfactor_pos less_numeral_extra(3))


[STATEMENT]
lemma dconvfactor_convinv: "dconvfactor (convinv c) d = inverse (dconvfactor c d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dconvfactor (inv\<^sub>C c) d = inverse (dconvfactor c d)
[PROOF STEP]
by (simp add: dconvfactor_def intpow_inverse[THEN sym])


[STATEMENT]
lemma dconvfactor_id [simp]: "dconvfactor id\<^sub>C d = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dconvfactor id\<^sub>C d = 1
[PROOF STEP]
by (simp add: dconvfactor_def, transfer, simp)


[STATEMENT]
lemma dconvfactor_compose:
  "dconvfactor (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) d = dconvfactor c\<^sub>1 d * dconvfactor c\<^sub>2 d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dconvfactor (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) d = dconvfactor c\<^sub>1 d \<cdot> dconvfactor c\<^sub>2 d
[PROOF STEP]
by (simp add: dconvfactor_def, transfer, simp add: mult_ac intpow_mult_distrib)


[STATEMENT]
lemma dconvfactor_inverse:
  "dconvfactor c (inverse d) = inverse (dconvfactor c d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dconvfactor c (inverse d) = inverse (dconvfactor c d)
[PROOF STEP]
by (simp add: dconvfactor_def inverse_dimvec_def intpow_uminus)


[STATEMENT]
lemma dconvfactor_times:
  "dconvfactor c (x \<cdot> y) = dconvfactor c x \<cdot> dconvfactor c y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dconvfactor c (x \<cdot> y) = dconvfactor c x \<cdot> dconvfactor c y
[PROOF STEP]
by (auto simp add: dconvfactor_def  mult_ac intpow_mult_combine times_dimvec_def)


[STATEMENT]
lemma magQ_qconv: "\<lbrakk>qconv c q\<rbrakk>\<^sub>Q = of_rat (dconvfactor c (dimQ q)) * \<lbrakk>q\<rbrakk>\<^sub>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qconv c q\<rbrakk>\<^sub>Q = of_rat (dconvfactor c (dimQ q)) \<cdot> \<lbrakk>q\<rbrakk>\<^sub>Q
[PROOF STEP]
by (simp add: si_def, transfer, simp)


[STATEMENT]
lemma qconv_id [simp]: "qconv id\<^sub>C x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv id\<^sub>C x = x
[PROOF STEP]
by (transfer', simp add: Measurement_System_eq_intro)


[STATEMENT]
lemma qconv_comp: "qconv (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) x = qconv c\<^sub>1 (qconv c\<^sub>2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv (c\<^sub>1 \<circ>\<^sub>C c\<^sub>2) x = qconv c\<^sub>1 (qconv c\<^sub>2 x)
[PROOF STEP]
by (transfer, simp add: dconvfactor_compose of_rat_mult)


[STATEMENT]
lemma qconv_convinv [simp]: "qconv (convinv c) (qconv c x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv (inv\<^sub>C c) (qconv c x) = x
[PROOF STEP]
by (transfer, simp add: dconvfactor_convinv mult.assoc[THEN sym] of_rat_mult[THEN sym] Measurement_System_eq_intro)


[STATEMENT]
lemma qconv_scaleQ [simp]: "qconv c (d *\<^sub>Q x) = d *\<^sub>Q qconv c x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c (d *\<^sub>Q x) = d *\<^sub>Q qconv c x
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma qconv_plus [simp]: "qconv c (x + y) = qconv c x + qconv c y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c (x + y) = qconv c x + qconv c y
[PROOF STEP]
by (transfer, auto simp add: plus_Quantity_ext_def mult.commute ring_class.ring_distribs)


[STATEMENT]
lemma qconv_minus [simp]: "qconv c (x - y) = qconv c x - qconv c y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c (x - y) = qconv c x - qconv c y
[PROOF STEP]
by (transfer, auto simp add: plus_Quantity_ext_def mult.commute ring_class.ring_distribs)


[STATEMENT]
lemma qconv_qmult [simp]: "qconv c (x \<^bold>\<cdot> y) = qconv c x \<^bold>\<cdot> qconv c y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c (x \<^bold>\<cdot> y) = qconv c x \<^bold>\<cdot> qconv c y
[PROOF STEP]
by (transfer, simp add: times_Quantity_ext_def times_Measurement_System_ext_def dconvfactor_times of_rat_mult)


[STATEMENT]
lemma qconv_qinverse [simp]: "qconv c (x\<^sup>-\<^sup>\<one>) = (qconv c x)\<^sup>-\<^sup>\<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c (x\<^sup>-\<^sup>\<one>) = qconv c x\<^sup>-\<^sup>\<one>
[PROOF STEP]
by (transfer, simp add: inverse_Quantity_ext_def inverse_Measurement_System_ext_def dconvfactor_inverse of_rat_inverse)


[STATEMENT]
lemma qconv_Length [simp]: "qconv c BUNIT(L, _) = LengthF c *\<^sub>Q BUNIT(L, _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c BUNIT(L, 'b) = LengthF c *\<^sub>Q BUNIT(L, 'a)
[PROOF STEP]
by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)


[STATEMENT]
lemma qconv_Mass [simp]: "qconv c BUNIT(M, _) = MassF c *\<^sub>Q BUNIT(M, _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c BUNIT(M, 'b) = MassF c *\<^sub>Q BUNIT(M, 'a)
[PROOF STEP]
by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)


[STATEMENT]
lemma qconv_Time [simp]: "qconv c BUNIT(T, _) = TimeF c *\<^sub>Q BUNIT(T, _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c BUNIT(T, 'b) = TimeF c *\<^sub>Q BUNIT(T, 'a)
[PROOF STEP]
by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)


[STATEMENT]
lemma qconv_Current [simp]: "qconv c BUNIT(I, _) = CurrentF c *\<^sub>Q BUNIT(I, _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c BUNIT(I, 'b) = CurrentF c *\<^sub>Q BUNIT(I, 'a)
[PROOF STEP]
by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)


[STATEMENT]
lemma qconv_Temperature [simp]: "qconv c BUNIT(\<Theta>, _) = TemperatureF c *\<^sub>Q BUNIT(\<Theta>, _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c BUNIT(\<Theta>, 'b) = TemperatureF c *\<^sub>Q BUNIT(\<Theta>, 'a)
[PROOF STEP]
by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)


[STATEMENT]
lemma qconv_Amount [simp]: "qconv c BUNIT(N, _) = AmountF c *\<^sub>Q BUNIT(N, _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c BUNIT(N, 'b) = AmountF c *\<^sub>Q BUNIT(N, 'a)
[PROOF STEP]
by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)


[STATEMENT]
lemma qconv_Intensity [simp]: "qconv c BUNIT(J, _) = IntensityF c *\<^sub>Q BUNIT(J, _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qconv c BUNIT(J, 'b) = IntensityF c *\<^sub>Q BUNIT(J, 'a)
[PROOF STEP]
by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)


[STATEMENT]
lemma consensus_then_weak_consensus:
  assumes "consensus vals dec rho"
  shows "weak_consensus vals dec rho"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_consensus vals dec rho
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consensus vals dec rho

goal (1 subgoal):
 1. weak_consensus vals dec rho
[PROOF STEP]
by (auto simp: consensus_def weak_consensus_def image_def)


[STATEMENT]
lemma binary_weak_consensus_then_consensus:
  assumes bc: "weak_consensus (vals::'proc \<Rightarrow> bool) dec rho"
  shows "consensus vals dec rho"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
{ \<comment> \<open>Show the Integrity property, the other conjuncts are the same.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
fix n p v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
assume dec: "dec (rho n p) = Some v"
[PROOF STATE]
proof (state)
this:
dec (rho n p) = Some v

goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
have "v \<in> range vals"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> range vals
[PROOF STEP]
proof (cases "\<exists>w. \<forall>p. vals p = w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
 2. \<nexists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>w. \<forall>p. vals p = w

goal (2 subgoals):
 1. \<exists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
 2. \<nexists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>w. \<forall>p. vals p = w
[PROOF STEP]
obtain w where w: "\<forall>p. vals p = w"
[PROOF STATE]
proof (prove)
using this:
\<exists>w. \<forall>p. vals p = w

goal (1 subgoal):
 1. (\<And>w. \<forall>p. vals p = w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>p. vals p = w

goal (2 subgoals):
 1. \<exists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
 2. \<nexists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
[PROOF STEP]
with bc
[PROOF STATE]
proof (chain)
picking this:
weak_consensus vals dec rho
\<forall>p. vals p = w
[PROOF STEP]
have "dec (rho n p) \<in> {Some w, None}"
[PROOF STATE]
proof (prove)
using this:
weak_consensus vals dec rho
\<forall>p. vals p = w

goal (1 subgoal):
 1. dec (rho n p) \<in> {Some w, None}
[PROOF STEP]
by (auto simp: weak_consensus_def)
[PROOF STATE]
proof (state)
this:
dec (rho n p) \<in> {Some w, None}

goal (2 subgoals):
 1. \<exists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
 2. \<nexists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
[PROOF STEP]
with dec w
[PROOF STATE]
proof (chain)
picking this:
dec (rho n p) = Some v
\<forall>p. vals p = w
dec (rho n p) \<in> {Some w, None}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dec (rho n p) = Some v
\<forall>p. vals p = w
dec (rho n p) \<in> {Some w, None}

goal (1 subgoal):
 1. v \<in> range vals
[PROOF STEP]
by (auto simp: image_def)
[PROOF STATE]
proof (state)
this:
v \<in> range vals

goal (1 subgoal):
 1. \<nexists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
[PROOF STEP]
case False
      \<comment> \<open>In this case both possible values occur in @{text "vals"}, and the result is trivial.\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>w. \<forall>p. vals p = w

goal (1 subgoal):
 1. \<nexists>w. \<forall>p. vals p = w \<Longrightarrow> v \<in> range vals
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>w. \<forall>p. vals p = w

goal (1 subgoal):
 1. v \<in> range vals
[PROOF STEP]
by (auto simp: image_def)
[PROOF STATE]
proof (state)
this:
v \<in> range vals

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<in> range vals

goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
dec (rho ?n2 ?p2) = Some ?v2 \<Longrightarrow> ?v2 \<in> range vals

goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
note integrity = this
[PROOF STATE]
proof (state)
this:
dec (rho ?n2 ?p2) = Some ?v2 \<Longrightarrow> ?v2 \<in> range vals

goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
from bc
[PROOF STATE]
proof (chain)
picking this:
weak_consensus vals dec rho
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
weak_consensus vals dec rho

goal (1 subgoal):
 1. consensus vals dec rho
[PROOF STEP]
unfolding consensus_def weak_consensus_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>v. (\<forall>p. vals p = v) \<longrightarrow> (\<forall>n p w. dec (rho n p) = Some w \<longrightarrow> w = v)) \<and> (\<forall>m n p q v w. dec (rho m p) = Some v \<and> dec (rho n q) = Some w \<longrightarrow> v = w) \<and> (\<forall>p. \<exists>n. dec (rho n p) \<noteq> None)

goal (1 subgoal):
 1. (\<forall>n p v. dec (rho n p) = Some v \<longrightarrow> v \<in> range vals) \<and> (\<forall>m n p q v w. dec (rho m p) = Some v \<and> dec (rho n q) = Some w \<longrightarrow> v = w) \<and> (\<forall>p. \<exists>n. dec (rho n p) \<noteq> None)
[PROOF STEP]
by (auto elim!: integrity)
[PROOF STATE]
proof (state)
this:
consensus vals dec rho

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HOinitConfig_eq:
  "HOinitConfig A cfg = (\<forall>p. initState A p (cfg p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOinitConfig A cfg = (\<forall>p. initState A p (cfg p))
[PROOF STEP]
by (auto simp: HOinitConfig_def CHOinitConfig_def initState_def)


[STATEMENT]
lemma SHOnextConfig_eq:
  "SHOnextConfig A r cfg HO SHO cfg' =
   (\<forall>p. \<exists>\<mu> \<in> SHOmsgVectors A r p cfg (HO p) (SHO p).
             nextState A r p (cfg p) \<mu> (cfg' p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SHOnextConfig A r cfg HO SHO cfg' = (\<forall>p. \<exists>\<mu>\<in>SHOmsgVectors A r p cfg (HO p) (SHO p). nextState A r p (cfg p) \<mu> (cfg' p))
[PROOF STEP]
by (auto simp: SHOnextConfig_def CSHOnextConfig_def SHOmsgVectors_def nextState_def)


[STATEMENT]
lemma SHORun_eq:
  "SHORun A rho HOs SHOs =
     (HOinitConfig A (rho 0)
   \<and> (\<forall>r. SHOnextConfig A r (rho r) (HOs r) (SHOs r) (rho (Suc r))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SHORun A rho HOs SHOs = (HOinitConfig A (rho 0) \<and> (\<forall>r. SHOnextConfig A r (rho r) (HOs r) (SHOs r) (rho (Suc r))))
[PROOF STEP]
by (auto simp: SHORun_def CSHORun_def HOinitConfig_def SHOnextConfig_def)


[STATEMENT]
lemma SHOmsgVectors_HO:
  "SHOmsgVectors A r p cfg HO HO = {HOrcvdMsgs A r p HO cfg}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SHOmsgVectors A r p cfg HO HO = {HOrcvdMsgs A r p HO cfg}
[PROOF STEP]
unfolding SHOmsgVectors_def HOrcvdMsgs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<mu>. (\<forall>q. (q \<in> HO) = (\<mu> q \<noteq> None)) \<and> (\<forall>q. q \<in> HO \<inter> HO \<longrightarrow> \<mu> q = Some (sendMsg A r q p (cfg q)))} = {\<lambda>q. if q \<in> HO then Some (sendMsg A r q p (cfg q)) else None}
[PROOF STEP]
by auto


[STATEMENT]
lemma CHOnextConfig_eq:
  "CHOnextConfig A r cfg HO coord cfg' =
   (\<forall>p. CnextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg)
                   (coord p) (cfg' p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CHOnextConfig A r cfg HO coord cfg' = (\<forall>p. CnextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg) (coord p) (cfg' p))
[PROOF STEP]
by (auto simp: CHOnextConfig_def CSHOnextConfig_def SHOmsgVectors_HO)


[STATEMENT]
lemma CHORun_eq:
  "CHORun A rho HOs coords =
     (CHOinitConfig A (rho 0) (coords 0)
      \<and> (\<forall>r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CHORun A rho HOs coords = (CHOinitConfig A (rho 0) (coords 0) \<and> (\<forall>r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r))))
[PROOF STEP]
by (auto simp: CHORun_def CSHORun_def CHOinitConfig_def CHOnextConfig_def)


[STATEMENT]
lemma HOnextConfig_eq:
  "HOnextConfig A r cfg HO cfg' =
   (\<forall>p. nextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg) (cfg' p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOnextConfig A r cfg HO cfg' = (\<forall>p. nextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg) (cfg' p))
[PROOF STEP]
by (auto simp: HOnextConfig_def SHOnextConfig_eq SHOmsgVectors_HO)


[STATEMENT]
lemma HORun_eq:
  "HORun A rho HOs =
   (  HOinitConfig A (rho 0)
    \<and> (\<forall>r. HOnextConfig A r (rho r) (HOs r) (rho (Suc r))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HORun A rho HOs = (HOinitConfig A (rho 0) \<and> (\<forall>r. HOnextConfig A r (rho r) (HOs r) (rho (Suc r))))
[PROOF STEP]
by (auto simp: HORun_def SHORun_eq HOnextConfig_def)


[STATEMENT]
lemma CHORun_0:
  assumes "CHORun A rho HOs coords"
      and "\<And>cfg. CHOinitConfig A cfg (coords 0) \<Longrightarrow> P cfg"
  shows "P (rho 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (rho 0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CHORun A rho HOs coords
CHOinitConfig A ?cfg (coords 0) \<Longrightarrow> P ?cfg

goal (1 subgoal):
 1. P (rho 0)
[PROOF STEP]
unfolding CHORun_eq
[PROOF STATE]
proof (prove)
using this:
CHOinitConfig A (rho 0) (coords 0) \<and> (\<forall>r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r)))
CHOinitConfig A ?cfg (coords 0) \<Longrightarrow> P ?cfg

goal (1 subgoal):
 1. P (rho 0)
[PROOF STEP]
by blast


[STATEMENT]
lemma CHORun_Suc:
  assumes "CHORun A rho HOs coords"
  and "\<And>r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r))
            \<Longrightarrow> P r"
  shows "P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CHORun A rho HOs coords
CHOnextConfig A ?r (rho ?r) (HOs ?r) (coords (Suc ?r)) (rho (Suc ?r)) \<Longrightarrow> P ?r

goal (1 subgoal):
 1. P n
[PROOF STEP]
unfolding CHORun_eq
[PROOF STATE]
proof (prove)
using this:
CHOinitConfig A (rho 0) (coords 0) \<and> (\<forall>r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r)))
CHOnextConfig A ?r (rho ?r) (HOs ?r) (coords (Suc ?r)) (rho (Suc ?r)) \<Longrightarrow> P ?r

goal (1 subgoal):
 1. P n
[PROOF STEP]
by blast


[STATEMENT]
lemma CHORun_induct:
  assumes run: "CHORun A rho HOs coords"
  and init: "CHOinitConfig A (rho 0) (coords 0) \<Longrightarrow> P 0"
  and step: "\<And>r. \<lbrakk> P r; CHOnextConfig A r (rho r) (HOs r) (coords (Suc r))
                                      (rho (Suc r)) \<rbrakk> \<Longrightarrow> P (Suc r)"
  shows "P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P n
[PROOF STEP]
using run
[PROOF STATE]
proof (prove)
using this:
CHORun A rho HOs coords

goal (1 subgoal):
 1. P n
[PROOF STEP]
unfolding CHORun_eq
[PROOF STATE]
proof (prove)
using this:
CHOinitConfig A (rho 0) (coords 0) \<and> (\<forall>r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r)))

goal (1 subgoal):
 1. P n
[PROOF STEP]
by (induct n, auto elim: init step)


[STATEMENT]
lemma rel_fun_mono: "(A ===> B) \<le> (A' ===> B')" if "A' \<le> A" "B \<le> B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ===> B \<le> A' ===> B'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
A' \<le> A
B \<le> B'

goal (1 subgoal):
 1. A ===> B \<le> A' ===> B'
[PROOF STEP]
by(auto simp add: rel_fun_def)


[STATEMENT]
lemma rel_fun_eq: "((=) ===> (=)) = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (=) ===> (=) = (=)
[PROOF STEP]
by(fact fun.rel_eq)


[STATEMENT]
lemma rel_fun_conversep: "(A\<inverse>\<inverse> ===> B\<inverse>\<inverse>) = (A ===> B)\<inverse>\<inverse>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<inverse>\<inverse> ===> B\<inverse>\<inverse> = (A ===> B)\<inverse>\<inverse>
[PROOF STEP]
by(auto simp add: rel_fun_def)


[STATEMENT]
lemma map_fun_id0: "(id ---> id) = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id ---> id = id
[PROOF STEP]
by(fact map_fun.id)


[STATEMENT]
lemma map_fun_comp: "(f ---> g) \<circ> (f' ---> g') = ((f' \<circ> f) ---> (g \<circ> g'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ---> g \<circ> (f' ---> g') = (f' \<circ> f) ---> g \<circ> g'
[PROOF STEP]
by(fact map_fun.comp)


[STATEMENT]
lemma map_fun_parametric: "((A ===> A') ===> (B ===> B') ===> (A' ===> B) ===> (A ===> B')) (--->) (--->)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A') ===> (B ===> B') ===> (A' ===> B) ===> A ===> B') (--->) (--->)
[PROOF STEP]
by(fact map_fun_parametric)


[STATEMENT]
lemma rel_fun_pos_distr_iff [simp]: "rel_fun_pos_distr_cond A A' tytok = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun_pos_distr_cond A A' tytok = True
[PROOF STEP]
unfolding rel_fun_pos_distr_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>B B'. (A ===> B) OO (A' ===> B') \<le> A OO A' ===> B OO B') = True
[PROOF STEP]
by (blast intro!: pos_fun_distr)


[STATEMENT]
lemma rel_fun_neg_distr_imp: "\<lbrakk> left_unique A; right_total A; right_unique A'; left_total A' \<rbrakk> \<Longrightarrow>
  rel_fun_neg_distr_cond A A' tytok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_unique A; right_total A; right_unique A'; left_total A'\<rbrakk> \<Longrightarrow> rel_fun_neg_distr_cond A A' tytok
[PROOF STEP]
unfolding rel_fun_neg_distr_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_unique A; right_total A; right_unique A'; left_total A'\<rbrakk> \<Longrightarrow> \<forall>B B'. A OO A' ===> B OO B' \<le> (A ===> B) OO (A' ===> B')
[PROOF STEP]
by (fast elim!: neg_fun_distr1[THEN predicate2D])


[STATEMENT]
lemma rel_fun_pos_distr_cond_eq: "rel_fun_pos_distr_cond (=) (=) tytok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun_pos_distr_cond (=) (=) tytok
[PROOF STEP]
by simp


[STATEMENT]
lemma rel_fun_neg_distr_cond_eq: "rel_fun_neg_distr_cond (=) (=) tytok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun_neg_distr_cond (=) (=) tytok
[PROOF STEP]
by (blast intro: rel_fun_neg_distr_imp left_unique_eq right_unique_eq right_total_eq left_total_eq)


[STATEMENT]
lemma rel_set_mono: "A \<le> A' \<Longrightarrow> rel_set A \<le> rel_set A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<le> A' \<Longrightarrow> rel_set A \<le> rel_set A'
[PROOF STEP]
by(fact rel_set_mono)


[STATEMENT]
lemma rel_set_eq: "rel_set (=) = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set (=) = (=)
[PROOF STEP]
by(fact rel_set_eq)


[STATEMENT]
lemma rel_set_conversep: "rel_set A\<inverse>\<inverse> = (rel_set A)\<inverse>\<inverse>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set A\<inverse>\<inverse> = (rel_set A)\<inverse>\<inverse>
[PROOF STEP]
by(fact rel_set_conversep)


[STATEMENT]
lemma map_set_id0: "image id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) id = id
[PROOF STEP]
by(fact image_id)


[STATEMENT]
lemma map_set_comp: "image f \<circ> image g = image (f \<circ> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) f \<circ> (`) g = (`) (f \<circ> g)
[PROOF STEP]
by(simp add: fun_eq_iff image_image o_def)


[STATEMENT]
lemma map_set_parametric: includes lifting_syntax shows
  "((A ===> B) ===> rel_set A ===> rel_set B) image image"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> B) ===> rel_set A ===> rel_set B) (`) (`)
[PROOF STEP]
by(fact image_transfer)


[STATEMENT]
lemma rel_set_pos_distr_iff [simp]: "rel_set_pos_distr_cond A A' = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set_pos_distr_cond A A' = True
[PROOF STEP]
unfolding rel_set_pos_distr_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A OO rel_set A' \<le> rel_set (A OO A')) = True
[PROOF STEP]
by(simp add: rel_set_OO)


[STATEMENT]
lemma rel_set_neg_distr_iff [simp]: "rel_set_neg_distr_cond A A' = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set_neg_distr_cond A A' = True
[PROOF STEP]
unfolding rel_set_neg_distr_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set (A OO A') \<le> rel_set A OO rel_set A') = True
[PROOF STEP]
by(simp add: rel_set_OO)


[STATEMENT]
lemma rel_set_pos_distr_eq: "rel_set_pos_distr_cond (=) (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set_pos_distr_cond (=) (=)
[PROOF STEP]
by simp


[STATEMENT]
lemma rel_set_neg_distr_eq: "rel_set_neg_distr_cond (=) (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set_neg_distr_cond (=) (=)
[PROOF STEP]
by simp


[STATEMENT]
lemma bset_map_closed:
  fixes f A
  defines "B \<equiv> image f A"
  assumes "finite A \<and> card A \<le> CARD('k)"
  shows "finite B \<and> card B \<le> CARD('k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite B \<and> card B \<le> CARD('k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B \<equiv> f ` A
finite A \<and> card A \<le> CARD('k)

goal (1 subgoal):
 1. finite B \<and> card B \<le> CARD('k)
[PROOF STEP]
by(auto intro: card_image_le[THEN order_trans])