[STATEMENT]
lemma generaliseTrans:
  assumes i1: "PROP Pure.prop (PROP P \<Longrightarrow> PROP Q)"
  assumes i2: "PROP Pure.prop (PROP Q \<Longrightarrow> PROP R)"
  shows "PROP Pure.prop (PROP P \<Longrightarrow> PROP R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP P \<Longrightarrow> PROP R
[PROOF STEP]
using i1 i2
[PROOF STATE]
proof (prove)
using this:
PROP P \<Longrightarrow> PROP Q
PROP Q \<Longrightarrow> PROP R

goal (1 subgoal):
 1. PROP P \<Longrightarrow> PROP R
[PROOF STEP]
proof (unfold prop_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP Q \<Longrightarrow> PROP R; PROP P\<rbrakk> \<Longrightarrow> PROP R
[PROOF STEP]
assume P_Q: "PROP P \<Longrightarrow> PROP Q"
[PROOF STATE]
proof (state)
this:
PROP P \<Longrightarrow> PROP Q

goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP Q \<Longrightarrow> PROP R; PROP P\<rbrakk> \<Longrightarrow> PROP R
[PROOF STEP]
assume Q_R: "PROP Q \<Longrightarrow> PROP R"
[PROOF STATE]
proof (state)
this:
PROP Q \<Longrightarrow> PROP R

goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP Q \<Longrightarrow> PROP R; PROP P\<rbrakk> \<Longrightarrow> PROP R
[PROOF STEP]
assume P: "PROP P"
[PROOF STATE]
proof (state)
this:
PROP P

goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP Q \<Longrightarrow> PROP R; PROP P\<rbrakk> \<Longrightarrow> PROP R
[PROOF STEP]
show "PROP R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP R
[PROOF STEP]
by (rule Q_R [OF P_Q [OF P]])
[PROOF STATE]
proof (state)
this:
PROP R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma meta_spec:
  assumes "\<And>x. PROP P x"
  shows "PROP P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP P x
[PROOF STEP]
by fact


[STATEMENT]
lemma meta_spec_protect:
  assumes g: "\<And>x. PROP P x"
  shows "PROP Pure.prop (PROP P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP P x
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
PROP P ?x

goal (1 subgoal):
 1. PROP P x
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generaliseImp:
  assumes i: "PROP Pure.prop (PROP Pure.prop (Trueprop P) \<Longrightarrow> PROP Pure.prop (Trueprop Q))"
  shows "PROP Pure.prop (PROP Pure.prop (Trueprop (X \<longrightarrow> P)) \<Longrightarrow> PROP Pure.prop (Trueprop (X \<longrightarrow> Q)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<longrightarrow> P) \<Longrightarrow> (X \<longrightarrow> Q)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
(P) \<Longrightarrow> (Q)

goal (1 subgoal):
 1. (X \<longrightarrow> P) \<Longrightarrow> (X \<longrightarrow> Q)
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generaliseEx:
 assumes i: "PROP Pure.prop (\<And>s. PROP Pure.prop (Trueprop (P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (Q s)))"
 shows "PROP Pure.prop (PROP Pure.prop (Trueprop (\<exists>s. P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (\<exists>s. Q s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s. P s) \<Longrightarrow> (\<exists>s. Q s)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<And>s. (P s) \<Longrightarrow> (Q s)

goal (1 subgoal):
 1. (\<exists>s. P s) \<Longrightarrow> (\<exists>s. Q s)
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generaliseRefl: "PROP Pure.prop (PROP Pure.prop (Trueprop P) \<Longrightarrow> PROP Pure.prop (Trueprop P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P) \<Longrightarrow> (P)
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generaliseRefl': "PROP Pure.prop (PROP P \<Longrightarrow> PROP P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP P \<Longrightarrow> PROP P
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generaliseAllShift:
  assumes i: "PROP Pure.prop (\<And>s. P \<Longrightarrow> Q s)"
  shows "PROP Pure.prop (PROP Pure.prop (Trueprop P) \<Longrightarrow> PROP Pure.prop (Trueprop (\<forall>s. Q s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P) \<Longrightarrow> (\<forall>s. Q s)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<And>s. P \<Longrightarrow> Q s

goal (1 subgoal):
 1. (P) \<Longrightarrow> (\<forall>s. Q s)
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generalise_allShift:
  assumes i: "PROP Pure.prop (\<And>s. PROP P \<Longrightarrow> PROP Q s)"
  shows "PROP Pure.prop (PROP Pure.prop (PROP P) \<Longrightarrow> PROP Pure.prop (\<And>s. PROP Q s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (\<And>s. PROP Q s)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<And>s. PROP P \<Longrightarrow> PROP Q s

goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (\<And>s. PROP Q s)
[PROOF STEP]
proof (unfold prop_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. PROP P \<Longrightarrow> PROP Q s; PROP P\<rbrakk> \<Longrightarrow> Pure.all Q
[PROOF STEP]
assume P_Q: "\<And>s. PROP P \<Longrightarrow> PROP Q s"
[PROOF STATE]
proof (state)
this:
PROP P \<Longrightarrow> PROP Q ?s

goal (1 subgoal):
 1. \<lbrakk>\<And>s. PROP P \<Longrightarrow> PROP Q s; PROP P\<rbrakk> \<Longrightarrow> Pure.all Q
[PROOF STEP]
assume P: "PROP P"
[PROOF STATE]
proof (state)
this:
PROP P

goal (1 subgoal):
 1. \<lbrakk>\<And>s. PROP P \<Longrightarrow> PROP Q s; PROP P\<rbrakk> \<Longrightarrow> Pure.all Q
[PROOF STEP]
show "\<And>s. PROP Q s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. PROP Q s
[PROOF STEP]
by (rule P_Q [OF P])
[PROOF STATE]
proof (state)
this:
PROP Q ?s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma generaliseImpl:
  assumes i: "PROP Pure.prop (PROP Pure.prop P \<Longrightarrow> PROP Pure.prop Q)"
  shows "PROP Pure.prop ((PROP Pure.prop (PROP X \<Longrightarrow> PROP P)) \<Longrightarrow> (PROP Pure.prop (PROP X \<Longrightarrow> PROP Q)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PROP X \<Longrightarrow> PROP P) \<Longrightarrow> (PROP X \<Longrightarrow> PROP Q)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
(PROP P) \<Longrightarrow> (PROP Q)

goal (1 subgoal):
 1. (PROP X \<Longrightarrow> PROP P) \<Longrightarrow> (PROP X \<Longrightarrow> PROP Q)
[PROOF STEP]
proof (unfold prop_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP X \<Longrightarrow> PROP P; PROP X\<rbrakk> \<Longrightarrow> PROP Q
[PROOF STEP]
assume i1: "PROP P \<Longrightarrow> PROP Q"
[PROOF STATE]
proof (state)
this:
PROP P \<Longrightarrow> PROP Q

goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP X \<Longrightarrow> PROP P; PROP X\<rbrakk> \<Longrightarrow> PROP Q
[PROOF STEP]
assume i2: "PROP X \<Longrightarrow> PROP P"
[PROOF STATE]
proof (state)
this:
PROP X \<Longrightarrow> PROP P

goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP X \<Longrightarrow> PROP P; PROP X\<rbrakk> \<Longrightarrow> PROP Q
[PROOF STEP]
assume X: "PROP X"
[PROOF STATE]
proof (state)
this:
PROP X

goal (1 subgoal):
 1. \<lbrakk>PROP P \<Longrightarrow> PROP Q; PROP X \<Longrightarrow> PROP P; PROP X\<rbrakk> \<Longrightarrow> PROP Q
[PROOF STEP]
show "PROP Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
by (rule i1 [OF i2 [OF X]])
[PROOF STATE]
proof (state)
this:
PROP Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_resources_suffice:
  assumes "f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>"
  obtains n where "f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume "\<forall>n. f\<cdot>(C\<^bsup>n\<^esup>) = \<bottom>"
[PROOF STATE]
proof (state)
this:
\<forall>n. f\<cdot>C\<^bsup>n\<^esup> = \<bottom>

goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "f\<cdot>C\<^sup>\<infinity> \<sqsubseteq> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f\<cdot>C\<^bsup>n\<^esup> = \<bottom>

goal (1 subgoal):
 1. f\<cdot>C\<^sup>\<infinity> \<sqsubseteq> \<bottom>
[PROOF STEP]
by (auto intro: lub_below[OF ch2ch_Rep_cfunR[OF chain_iterate]]
             simp add: Cinf_def fix_def2 contlub_cfun_arg[OF chain_iterate])
[PROOF STATE]
proof (state)
this:
f\<cdot>C\<^sup>\<infinity> \<sqsubseteq> \<bottom>

goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>
f\<cdot>C\<^sup>\<infinity> \<sqsubseteq> \<bottom>
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>
f\<cdot>C\<^sup>\<infinity> \<sqsubseteq> \<bottom>

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

goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>n. f\<cdot>C\<^bsup>n\<^esup> = \<bottom> \<Longrightarrow> False

goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f\<cdot>C\<^bsup>n\<^esup> = \<bottom> \<Longrightarrow> False

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f\<cdot>C\<^bsup>n\<^esup> = \<bottom> \<Longrightarrow> False
f\<cdot>C\<^bsup>?n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma more_resources_suffice:
  assumes "f\<cdot>r \<noteq> \<bottom>" and "r \<sqsubseteq> r'"
  shows "f\<cdot>r' \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>r' \<noteq> \<bottom>
[PROOF STEP]
using assms(1) monofun_cfun_arg[OF assms(2), where  f = f]
[PROOF STATE]
proof (prove)
using this:
f\<cdot>r \<noteq> \<bottom>
f\<cdot>r \<sqsubseteq> f\<cdot>r'

goal (1 subgoal):
 1. f\<cdot>r' \<noteq> \<bottom>
[PROOF STEP]
by auto


[STATEMENT]
lemma infinite_resources_suffice:
  shows "f\<cdot>r \<noteq> \<bottom> \<Longrightarrow> f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>r \<noteq> \<bottom> \<Longrightarrow> f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>
[PROOF STEP]
by (erule more_resources_suffice[OF _ below_Cinf])


[STATEMENT]
lemma demand_suffices:
  assumes "f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>"
  shows "f\<cdot>(demand f) \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>(demand f) \<noteq> \<bottom>
[PROOF STEP]
apply (simp add: assms demand_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> \<noteq> \<bottom>
[PROOF STEP]
apply (rule finite_resources_suffice[OF assms])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> f\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> \<noteq> \<bottom>
[PROOF STEP]
apply (rule LeastI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> f\<cdot>C\<^bsup>?k4 n\<^esup> \<noteq> \<bottom>
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_bot_demand:
  "f\<cdot>r \<noteq> \<bottom> \<longleftrightarrow> demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f\<cdot>r \<noteq> \<bottom>) = (demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r)
[PROOF STEP]
proof(intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f\<cdot>r \<noteq> \<bottom> \<Longrightarrow> demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r
 2. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
assume "f\<cdot>r \<noteq> \<bottom>"
[PROOF STATE]
proof (state)
this:
f\<cdot>r \<noteq> \<bottom>

goal (2 subgoals):
 1. f\<cdot>r \<noteq> \<bottom> \<Longrightarrow> demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r
 2. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
thus "demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>r \<noteq> \<bottom>

goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r
[PROOF STEP]
apply (cases r rule:C_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>f\<cdot>r \<noteq> \<bottom>; r = C\<^bsup>n\<^esup>\<rbrakk> \<Longrightarrow> demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r
 2. \<lbrakk>f\<cdot>r \<noteq> \<bottom>; r = C\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r
[PROOF STEP]
apply (auto intro: Least_le simp add: demand_def dest: infinite_resources_suffice)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r

goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
assume *: "demand f \<noteq> C\<^sup>\<infinity>  \<and> demand f \<sqsubseteq> r"
[PROOF STATE]
proof (state)
this:
demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r

goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r
[PROOF STEP]
have "f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r

goal (1 subgoal):
 1. f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>
[PROOF STEP]
by (auto intro: Least_le simp add: demand_def dest: infinite_resources_suffice)
[PROOF STATE]
proof (state)
this:
f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>

goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
hence "f\<cdot>(demand f) \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom>

goal (1 subgoal):
 1. f\<cdot>(demand f) \<noteq> \<bottom>
[PROOF STEP]
by (rule demand_suffices)
[PROOF STATE]
proof (state)
this:
f\<cdot>(demand f) \<noteq> \<bottom>

goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f\<cdot>(demand f) \<noteq> \<bottom>

goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r
[PROOF STEP]
have "demand f \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
using this:
demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r

goal (1 subgoal):
 1. demand f \<sqsubseteq> r
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
demand f \<sqsubseteq> r

goal (1 subgoal):
 1. demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<Longrightarrow> f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f\<cdot>(demand f) \<noteq> \<bottom>
demand f \<sqsubseteq> r
[PROOF STEP]
show "f\<cdot>r \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>(demand f) \<noteq> \<bottom>
demand f \<sqsubseteq> r

goal (1 subgoal):
 1. f\<cdot>r \<noteq> \<bottom>
[PROOF STEP]
by (rule more_resources_suffice)
[PROOF STATE]
proof (state)
this:
f\<cdot>r \<noteq> \<bottom>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinity_bot_demand:
  "f\<cdot>C\<^sup>\<infinity> = \<bottom> \<longleftrightarrow> demand f = C\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f\<cdot>C\<^sup>\<infinity> = \<bottom>) = (demand f = C\<^sup>\<infinity>)
[PROOF STEP]
by (metis below_Cinf not_bot_demand)


[STATEMENT]
lemma demand_suffices':
  assumes "demand f = C\<^bsup>n\<^esup>"
  shows "f\<cdot>(demand f) \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>(demand f) \<noteq> \<bottom>
[PROOF STEP]
by (metis C_eq_Cinf assms demand_suffices infinity_bot_demand)


[STATEMENT]
lemma demand_Suc_Least:
  assumes [simp]: "f\<cdot>\<bottom> = \<bottom>"
  assumes "demand f \<noteq> C\<^sup>\<infinity>"
  shows "demand f = C\<^bsup>(Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>))\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
f\<cdot>\<bottom> = \<bottom>
demand f \<noteq> C\<^sup>\<infinity>
[PROOF STEP]
have "demand f = C\<^bsup>(LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>)\<^esup>"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>\<bottom> = \<bottom>
demand f \<noteq> C\<^sup>\<infinity>

goal (1 subgoal):
 1. demand f = C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>
[PROOF STEP]
by (auto simp add: demand_def)
[PROOF STATE]
proof (state)
this:
demand f = C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>

goal (1 subgoal):
 1. demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
demand f = C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>

goal (1 subgoal):
 1. demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
demand f = C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>
[PROOF STEP]
obtain n where "f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
demand f = C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>

goal (1 subgoal):
 1. (\<And>n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis  demand_suffices')
[PROOF STATE]
proof (state)
this:
f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>

goal (1 subgoal):
 1. demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
hence "(LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>) = Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>

goal (1 subgoal):
 1. (LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>) = Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)
[PROOF STEP]
apply (rule Least_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> f\<cdot>C\<^bsup>0\<^esup> \<noteq> \<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>) = Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)

goal (1 subgoal):
 1. demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>

goal (1 subgoal):
 1. demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
demand f = C\<^bsup>Suc (LEAST n. f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma demand_C_case[simp]: "demand (C_case\<cdot>f) = C \<cdot> (demand f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
proof(cases "demand (C_case\<cdot>f) = C\<^sup>\<infinity>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. demand (C_case\<cdot>f) = C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
 2. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
demand (C_case\<cdot>f) = C\<^sup>\<infinity>

goal (2 subgoals):
 1. demand (C_case\<cdot>f) = C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
 2. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
demand (C_case\<cdot>f) = C\<^sup>\<infinity>
[PROOF STEP]
have "C_case\<cdot>f\<cdot>C\<^sup>\<infinity> = \<bottom>"
[PROOF STATE]
proof (prove)
using this:
demand (C_case\<cdot>f) = C\<^sup>\<infinity>

goal (1 subgoal):
 1. C_case\<cdot>f\<cdot>C\<^sup>\<infinity> = \<bottom>
[PROOF STEP]
by (metis infinity_bot_demand)
[PROOF STATE]
proof (state)
this:
C_case\<cdot>f\<cdot>C\<^sup>\<infinity> = \<bottom>

goal (2 subgoals):
 1. demand (C_case\<cdot>f) = C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
 2. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
demand (C_case\<cdot>f) = C\<^sup>\<infinity>
C_case\<cdot>f\<cdot>C\<^sup>\<infinity> = \<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
demand (C_case\<cdot>f) = C\<^sup>\<infinity>
C_case\<cdot>f\<cdot>C\<^sup>\<infinity> = \<bottom>

goal (1 subgoal):
 1. demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>demand (C_case\<cdot>f) = C\<^sup>\<infinity>; f\<cdot>C\<^sup>\<infinity> = \<bottom>\<rbrakk> \<Longrightarrow> C\<^sup>\<infinity> = demand f
[PROOF STEP]
by (metis infinity_bot_demand)
[PROOF STATE]
proof (state)
this:
demand (C_case\<cdot>f) = C\<cdot>(demand f)

goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity>

goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
hence "demand (C_case\<cdot>f) = C\<^bsup>Suc (LEAST n. (C_case\<cdot>f)\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>"
[PROOF STATE]
proof (prove)
using this:
demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity>

goal (1 subgoal):
 1. demand (C_case\<cdot>f) = C\<^bsup>Suc (LEAST n. C_case\<cdot>f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>
[PROOF STEP]
by (rule demand_Suc_Least[OF C.case_rews(1)])
[PROOF STATE]
proof (state)
this:
demand (C_case\<cdot>f) = C\<^bsup>Suc (LEAST n. C_case\<cdot>f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>

goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
demand (C_case\<cdot>f) = C\<^bsup>Suc (LEAST n. C_case\<cdot>f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup>

goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
have "\<dots> = C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^bsup>Suc (LEAST n. C_case\<cdot>f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup> = C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C\<^bsup>Suc (LEAST n. C_case\<cdot>f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup> = C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>

goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C\<^bsup>Suc (LEAST n. C_case\<cdot>f\<cdot>C\<^bsup>Suc n\<^esup> \<noteq> \<bottom>)\<^esup> = C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup>

goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
have "\<dots> = C\<cdot>(demand  f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> = C\<cdot>(demand f)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity>

goal (1 subgoal):
 1. C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> = C\<cdot>(demand f)
[PROOF STEP]
unfolding demand_def
[PROOF STATE]
proof (prove)
using this:
(if C_case\<cdot>f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom> then C\<^bsup>LEAST n. C_case\<cdot>f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> else C\<^sup>\<infinity>) \<noteq> C\<^sup>\<infinity>

goal (1 subgoal):
 1. C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> = C\<cdot>(if f\<cdot>C\<^sup>\<infinity> \<noteq> \<bottom> then C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> else C\<^sup>\<infinity>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<cdot>C\<^bsup>LEAST n. f\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>\<^esup> = C\<cdot>(demand f)

goal (1 subgoal):
 1. demand (C_case\<cdot>f) \<noteq> C\<^sup>\<infinity> \<Longrightarrow> demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
demand (C_case\<cdot>f) = C\<cdot>(demand f)

goal (1 subgoal):
 1. demand (C_case\<cdot>f) = C\<cdot>(demand f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
demand (C_case\<cdot>f) = C\<cdot>(demand f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma demand_contravariant:
  assumes "f \<sqsubseteq> g"
  shows "demand g \<sqsubseteq> demand f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. demand g \<sqsubseteq> demand f
[PROOF STEP]
proof(cases "demand f" rule:C_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. demand f = C\<^bsup>n\<^esup> \<Longrightarrow> demand g \<sqsubseteq> demand f
 2. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. demand f = C\<^bsup>n\<^esup> \<Longrightarrow> demand g \<sqsubseteq> demand f
 2. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
assume "demand f = C\<^bsup>n\<^esup>"
[PROOF STATE]
proof (state)
this:
demand f = C\<^bsup>n\<^esup>

goal (2 subgoals):
 1. \<And>n. demand f = C\<^bsup>n\<^esup> \<Longrightarrow> demand g \<sqsubseteq> demand f
 2. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
hence "f\<cdot>(demand f) \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
demand f = C\<^bsup>n\<^esup>

goal (1 subgoal):
 1. f\<cdot>(demand f) \<noteq> \<bottom>
[PROOF STEP]
by (metis demand_suffices')
[PROOF STATE]
proof (state)
this:
f\<cdot>(demand f) \<noteq> \<bottom>

goal (2 subgoals):
 1. \<And>n. demand f = C\<^bsup>n\<^esup> \<Longrightarrow> demand g \<sqsubseteq> demand f
 2. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f\<cdot>(demand f) \<noteq> \<bottom>

goal (2 subgoals):
 1. \<And>n. demand f = C\<^bsup>n\<^esup> \<Longrightarrow> demand g \<sqsubseteq> demand f
 2. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
note monofun_cfun_fun[OF assms]
[PROOF STATE]
proof (state)
this:
f\<cdot>?x \<sqsubseteq> g\<cdot>?x

goal (2 subgoals):
 1. \<And>n. demand f = C\<^bsup>n\<^esup> \<Longrightarrow> demand g \<sqsubseteq> demand f
 2. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cont (\<lambda>a. a) \<Longrightarrow> g\<cdot>(demand f) \<noteq> \<bottom>
[PROOF STEP]
have "g\<cdot>(demand f) \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>a. a) \<Longrightarrow> g\<cdot>(demand f) \<noteq> \<bottom>

goal (1 subgoal):
 1. g\<cdot>(demand f) \<noteq> \<bottom>
[PROOF STEP]
by this (intro cont2cont)
[PROOF STATE]
proof (state)
this:
g\<cdot>(demand f) \<noteq> \<bottom>

goal (2 subgoals):
 1. \<And>n. demand f = C\<^bsup>n\<^esup> \<Longrightarrow> demand g \<sqsubseteq> demand f
 2. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
thus "demand g \<sqsubseteq> demand f"
[PROOF STATE]
proof (prove)
using this:
g\<cdot>(demand f) \<noteq> \<bottom>

goal (1 subgoal):
 1. demand g \<sqsubseteq> demand f
[PROOF STEP]
unfolding not_bot_demand
[PROOF STATE]
proof (prove)
using this:
demand g \<noteq> C\<^sup>\<infinity> \<and> demand g \<sqsubseteq> demand f

goal (1 subgoal):
 1. demand g \<sqsubseteq> demand f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
demand g \<sqsubseteq> demand f

goal (1 subgoal):
 1. demand f = C\<^sup>\<infinity> \<Longrightarrow> demand g \<sqsubseteq> demand f
[PROOF STEP]
qed auto


[STATEMENT]
lemma [simp]: "\<bottom>|\<^bsub>r\<^esub> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom>|\<^bsub>r\<^esub> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma [simp]: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> f|\<^bsub>\<bottom>\<^esub> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> f|\<^bsub>\<bottom>\<^esub> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma C_restr_C_restr[simp]: "(v|\<^bsub>r'\<^esub>)|\<^bsub>r\<^esub> = v|\<^bsub>(r' \<sqinter> r)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v|\<^bsub>r'\<^esub>)|\<^bsub>r\<^esub> = v|\<^bsub>(r' \<sqinter> r)\<^esub>
[PROOF STEP]
by (rule cfun_eqI) simp


[STATEMENT]
lemma C_restr_eqD:
  assumes "f|\<^bsub>r\<^esub> = g|\<^bsub>r\<^esub>"
  assumes "r' \<sqsubseteq> r"
  shows "f\<cdot>r' = g\<cdot>r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>r' = g\<cdot>r'
[PROOF STEP]
by (metis C_restr.simps assms below_refl is_meetI)


[STATEMENT]
lemma C_restr_eq_lower:
  assumes "f|\<^bsub>r\<^esub> = g|\<^bsub>r\<^esub>"
  assumes "r' \<sqsubseteq> r"
  shows "f|\<^bsub>r'\<^esub> = g|\<^bsub>r'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f|\<^bsub>r'\<^esub> = g|\<^bsub>r'\<^esub>
[PROOF STEP]
by (metis C_restr_C_restr assms below_refl is_meetI)


[STATEMENT]
lemma C_restr_below[intro, simp]:
  "x|\<^bsub>r\<^esub> \<sqsubseteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x|\<^bsub>r\<^esub> \<sqsubseteq> x
[PROOF STEP]
apply (rule cfun_belowI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. (x|\<^bsub>r\<^esub>)\<cdot>xa \<sqsubseteq> x\<cdot>xa
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. x\<cdot>(r \<sqinter> xa) \<sqsubseteq> x\<cdot>xa
[PROOF STEP]
by (metis below_refl meet_below2 monofun_cfun_arg)


[STATEMENT]
lemma C_restr_below_cong:
  "(\<And> r'. r' \<sqsubseteq> r \<Longrightarrow> f \<cdot> r' \<sqsubseteq> g \<cdot> r') \<Longrightarrow> f|\<^bsub>r\<^esub> \<sqsubseteq> g|\<^bsub>r\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>r' \<sqsubseteq> g\<cdot>r') \<Longrightarrow> f|\<^bsub>r\<^esub> \<sqsubseteq> g|\<^bsub>r\<^esub>
[PROOF STEP]
apply (rule cfun_belowI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>r' \<sqsubseteq> g\<cdot>r') \<Longrightarrow> (f|\<^bsub>r\<^esub>)\<cdot>x \<sqsubseteq> (g|\<^bsub>r\<^esub>)\<cdot>x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>r' \<sqsubseteq> g\<cdot>r') \<Longrightarrow> f\<cdot>(r \<sqinter> x) \<sqsubseteq> g\<cdot>(r \<sqinter> x)
[PROOF STEP]
by (metis below_refl meet_below1)


[STATEMENT]
lemma C_restr_cong:
  "(\<And> r'. r' \<sqsubseteq> r \<Longrightarrow> f \<cdot> r' = g \<cdot> r') \<Longrightarrow> f|\<^bsub>r\<^esub> = g|\<^bsub>r\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>r' = g\<cdot>r') \<Longrightarrow> f|\<^bsub>r\<^esub> = g|\<^bsub>r\<^esub>
[PROOF STEP]
apply (intro below_antisym C_restr_below_cong )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r'. \<lbrakk>\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>r' = g\<cdot>r'; r' \<sqsubseteq> r\<rbrakk> \<Longrightarrow> f\<cdot>r' \<sqsubseteq> g\<cdot>r'
 2. \<And>r'. \<lbrakk>\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>r' = g\<cdot>r'; r' \<sqsubseteq> r\<rbrakk> \<Longrightarrow> g\<cdot>r' \<sqsubseteq> f\<cdot>r'
[PROOF STEP]
by (metis below_refl)+


[STATEMENT]
lemma C_restr_C_cong:
  "(\<And> r'. r' \<sqsubseteq> r \<Longrightarrow> f \<cdot> (C\<cdot>r') = g \<cdot> (C\<cdot>r')) \<Longrightarrow> f\<cdot>\<bottom>=g\<cdot>\<bottom> \<Longrightarrow> f|\<^bsub>C\<cdot>r\<^esub> = g|\<^bsub>C\<cdot>r\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>(C\<cdot>r') = g\<cdot>(C\<cdot>r'); f\<cdot>\<bottom> = g\<cdot>\<bottom>\<rbrakk> \<Longrightarrow> f|\<^bsub>C\<cdot>r\<^esub> = g|\<^bsub>C\<cdot>r\<^esub>
[PROOF STEP]
apply (rule C_restr_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r'. \<lbrakk>\<And>r'. r' \<sqsubseteq> r \<Longrightarrow> f\<cdot>(C\<cdot>r') = g\<cdot>(C\<cdot>r'); f\<cdot>\<bottom> = g\<cdot>\<bottom>; r' \<sqsubseteq> C\<cdot>r\<rbrakk> \<Longrightarrow> f\<cdot>r' = g\<cdot>r'
[PROOF STEP]
by (case_tac r', auto)


[STATEMENT]
lemma C_restr_C_case[simp]:
  "(C_case\<cdot>f)|\<^bsub>C\<cdot>r\<^esub> = C_case\<cdot>(f|\<^bsub>r\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C_case\<cdot>f|\<^bsub>C\<cdot>r\<^esub> = C_case\<cdot>(f|\<^bsub>r\<^esub>)
[PROOF STEP]
apply (rule cfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (C_case\<cdot>f|\<^bsub>C\<cdot>r\<^esub>)\<cdot>x = C_case\<cdot>(f|\<^bsub>r\<^esub>)\<cdot>x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. C_case\<cdot>f\<cdot>(C\<cdot>r \<sqinter> x) = C_case\<cdot>(f|\<^bsub>r\<^esub>)\<cdot>x
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x = \<bottom> \<Longrightarrow> C_case\<cdot>f\<cdot>(C\<cdot>r \<sqinter> x) = C_case\<cdot>(f|\<^bsub>r\<^esub>)\<cdot>x
 2. \<And>x Ca. x = C\<cdot>Ca \<Longrightarrow> C_case\<cdot>f\<cdot>(C\<cdot>r \<sqinter> x) = C_case\<cdot>(f|\<^bsub>r\<^esub>)\<cdot>x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x Ca. x = C\<cdot>Ca \<Longrightarrow> C_case\<cdot>f\<cdot>(C\<cdot>r \<sqinter> x) = C_case\<cdot>(f|\<^bsub>r\<^esub>)\<cdot>x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma C_restr_bot_demand:
  assumes "C\<cdot>r \<sqsubseteq> demand f"
  shows "f|\<^bsub>r\<^esub> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f|\<^bsub>r\<^esub> = \<bottom>
[PROOF STEP]
proof(rule cfun_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (f|\<^bsub>r\<^esub>)\<cdot>x = \<bottom>\<cdot>x
[PROOF STEP]
fix r'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (f|\<^bsub>r\<^esub>)\<cdot>x = \<bottom>\<cdot>x
[PROOF STEP]
have "f\<cdot>(r \<sqinter> r') = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
proof(rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
have "r \<sqsubseteq> C \<cdot> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<sqsubseteq> C\<cdot>r
[PROOF STEP]
by (rule below_C)
[PROOF STATE]
proof (state)
this:
r \<sqsubseteq> C\<cdot>r

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r \<sqsubseteq> C\<cdot>r

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
note assms
[PROOF STATE]
proof (state)
this:
C\<cdot>r \<sqsubseteq> demand f

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C\<cdot>r \<sqsubseteq> demand f

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
assume *: "f\<cdot>(r \<sqinter> r') \<noteq> \<bottom>"
[PROOF STATE]
proof (state)
this:
f\<cdot>(r \<sqinter> r') \<noteq> \<bottom>

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
hence "demand f \<sqsubseteq> (r \<sqinter> r')"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>(r \<sqinter> r') \<noteq> \<bottom>

goal (1 subgoal):
 1. demand f \<sqsubseteq> r \<sqinter> r'
[PROOF STEP]
unfolding not_bot_demand
[PROOF STATE]
proof (prove)
using this:
demand f \<noteq> C\<^sup>\<infinity> \<and> demand f \<sqsubseteq> r \<sqinter> r'

goal (1 subgoal):
 1. demand f \<sqsubseteq> r \<sqinter> r'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
demand f \<sqsubseteq> r \<sqinter> r'

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
hence "demand f \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
using this:
demand f \<sqsubseteq> r \<sqinter> r'

goal (1 subgoal):
 1. demand f \<sqsubseteq> r
[PROOF STEP]
by (metis below_refl meet_below1 below_trans)
[PROOF STATE]
proof (state)
this:
demand f \<sqsubseteq> r

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
finally (below_antisym)
[PROOF STATE]
proof (chain)
picking this:
cont (\<lambda>a. a) \<Longrightarrow> r = demand f
[PROOF STEP]
have "r = demand f"
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>a. a) \<Longrightarrow> r = demand f

goal (1 subgoal):
 1. r = demand f
[PROOF STEP]
by this (intro cont2cont)
[PROOF STATE]
proof (state)
this:
r = demand f

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
C\<cdot>r \<sqsubseteq> demand f
r = demand f
[PROOF STEP]
have "demand f = C\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
C\<cdot>r \<sqsubseteq> demand f
r = demand f

goal (1 subgoal):
 1. demand f = C\<^sup>\<infinity>
[PROOF STEP]
by (cases "demand f" rule:C_cases) (auto simp add: iterate_Suc[symmetric] simp del: iterate_Suc)
[PROOF STATE]
proof (state)
this:
demand f = C\<^sup>\<infinity>

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') \<noteq> \<bottom> \<Longrightarrow> f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
thus "f\<cdot>(r \<sqinter> r') = \<bottom>"
[PROOF STATE]
proof (prove)
using this:
demand f = C\<^sup>\<infinity>

goal (1 subgoal):
 1. f\<cdot>(r \<sqinter> r') = \<bottom>
[PROOF STEP]
by (metis not_bot_demand)
[PROOF STATE]
proof (state)
this:
f\<cdot>(r \<sqinter> r') = \<bottom>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f\<cdot>(r \<sqinter> r') = \<bottom>

goal (1 subgoal):
 1. \<And>x. (f|\<^bsub>r\<^esub>)\<cdot>x = \<bottom>\<cdot>x
[PROOF STEP]
thus "(f|\<^bsub>r\<^esub>)\<cdot>r' = \<bottom>\<cdot>r'"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>(r \<sqinter> r') = \<bottom>

goal (1 subgoal):
 1. (f|\<^bsub>r\<^esub>)\<cdot>r' = \<bottom>\<cdot>r'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f|\<^bsub>r\<^esub>)\<cdot>r' = \<bottom>\<cdot>r'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma env_C_restr_upd[simp]: "(\<rho>(x := v))|\<^sup>\<circ>\<^bsub>r\<^esub> = (\<rho>|\<^sup>\<circ>\<^bsub>r\<^esub>)(x := v|\<^bsub>r\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho>(x := v)|\<^sup>\<circ>\<^bsub>r\<^esub> = (\<rho>|\<^sup>\<circ>\<^bsub>r\<^esub>)(x := v|\<^bsub>r\<^esub>)
[PROOF STEP]
unfolding env_C_restr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r\<cdot>(\<rho>(x := v)) = ((\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r\<cdot>\<rho>)(x := v|\<^bsub>r\<^esub>)
[PROOF STEP]
by simp


[STATEMENT]
lemma env_C_restr_lookup[simp]: "(\<rho>|\<^sup>\<circ>\<^bsub>r\<^esub>) v = \<rho> v|\<^bsub>r\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<rho>|\<^sup>\<circ>\<^bsub>r\<^esub>) v = \<rho> v|\<^bsub>r\<^esub>
[PROOF STEP]
unfolding env_C_restr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r\<cdot>\<rho>) v = \<rho> v|\<^bsub>r\<^esub>
[PROOF STEP]
by simp


[STATEMENT]
lemma env_C_restr_bot[simp]: " \<bottom>|\<^sup>\<circ>\<^bsub>r\<^esub> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom>|\<^sup>\<circ>\<^bsub>r\<^esub> = \<bottom>
[PROOF STEP]
unfolding env_C_restr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by auto


[STATEMENT]
lemma env_C_restr_restr_below[intro]: "\<rho>|\<^sup>\<circ>\<^bsub>r\<^esub> \<sqsubseteq> \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho>|\<^sup>\<circ>\<^bsub>r\<^esub> \<sqsubseteq> \<rho>
[PROOF STEP]
by (auto intro: fun_belowI)


[STATEMENT]
lemma env_C_restr_env_C_restr[simp]: "(v|\<^sup>\<circ>\<^bsub>r'\<^esub>)|\<^sup>\<circ>\<^bsub>r\<^esub> = v|\<^sup>\<circ>\<^bsub>(r' \<sqinter> r)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v|\<^sup>\<circ>\<^bsub>r'\<^esub>)|\<^sup>\<circ>\<^bsub>r\<^esub> = v|\<^sup>\<circ>\<^bsub>(r' \<sqinter> r)\<^esub>
[PROOF STEP]
unfolding env_C_restr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r\<cdot>((\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r'\<cdot>v) = (\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>(r' \<sqinter> r)\<cdot>v
[PROOF STEP]
by auto


[STATEMENT]
lemma env_C_restr_cong:
  "(\<And> x r'. r' \<sqsubseteq> r \<Longrightarrow> f x \<cdot> r' = g x \<cdot> r') \<Longrightarrow> f|\<^sup>\<circ>\<^bsub>r\<^esub> = g|\<^sup>\<circ>\<^bsub>r\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x r'. r' \<sqsubseteq> r \<Longrightarrow> f x\<cdot>r' = g x\<cdot>r') \<Longrightarrow> f|\<^sup>\<circ>\<^bsub>r\<^esub> = g|\<^sup>\<circ>\<^bsub>r\<^esub>
[PROOF STEP]
unfolding env_C_restr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x r'. r' \<sqsubseteq> r \<Longrightarrow> f x\<cdot>r' = g x\<cdot>r') \<Longrightarrow> (\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r\<cdot>f = (\<Lambda> r. Abs_cfun (Rep_cfun (cfun_comp\<cdot>(C_restr\<cdot>r))))\<cdot>r\<cdot>g
[PROOF STEP]
by (rule ext) (auto intro: C_restr_cong)


[STATEMENT]
lemma in_rangeC: "f \<in> A \<Longrightarrow> f x \<in> rangeC A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> A \<Longrightarrow> f x \<in> rangeC A
[PROOF STEP]
by(auto simp add: rangeC_def)


[STATEMENT]
lemma in_rangeCE: assumes "y \<in> rangeC A"
  obtains f x where "f \<in> A" "y = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f x. \<lbrakk>f \<in> A; y = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> rangeC A

goal (1 subgoal):
 1. (\<And>f x. \<lbrakk>f \<in> A; y = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: rangeC_def)


[STATEMENT]
lemma in_rangeC_singleton: "f x \<in> rangeC {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<in> rangeC {f}
[PROOF STEP]
by(auto simp add: rangeC_def)


[STATEMENT]
lemma in_rangeC_singleton_const: "x \<in> rangeC {\<lambda>_. x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> rangeC {\<lambda>_. x}
[PROOF STEP]
by(rule in_rangeC_singleton)


[STATEMENT]
lemma rangeC_rangeC: "f \<in> rangeC A \<Longrightarrow> f x \<in> rangeC (rangeC A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> rangeC A \<Longrightarrow> f x \<in> rangeC (rangeC A)
[PROOF STEP]
by(auto simp add: rangeC_def)


[STATEMENT]
lemma rangeC_eq_empty: "rangeC A = {} \<longleftrightarrow> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rangeC A = {}) = (A = {})
[PROOF STEP]
by(auto simp add: rangeC_def)


[STATEMENT]
lemma Ball_rangeC_iff:
  "(\<forall>x \<in> rangeC A. P x) \<longleftrightarrow> (\<forall>f \<in> A. \<forall>x. P (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>rangeC A. P x) = (\<forall>f\<in>A. \<forall>x. P (f x))
[PROOF STEP]
by(auto intro: in_rangeC elim: in_rangeCE)


[STATEMENT]
lemma Ball_rangeC_singleton:
  "(\<forall>x \<in> rangeC {f}. P x) \<longleftrightarrow> (\<forall>x. P (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>rangeC {f}. P x) = (\<forall>x. P (f x))
[PROOF STEP]
by(simp add: Ball_rangeC_iff)


[STATEMENT]
lemma Ball_rangeC_rangeC:
  "(\<forall>x \<in> rangeC (rangeC A). P x) \<longleftrightarrow> (\<forall>f \<in> rangeC A. \<forall>x. P (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>rangeC (rangeC A). P x) = (\<forall>f\<in>rangeC A. \<forall>x. P (f x))
[PROOF STEP]
by(simp add: Ball_rangeC_iff)


[STATEMENT]
lemma finite_rangeC:
  assumes inj: "\<forall>f \<in> A. inj f"
  and disjoint: "\<forall>f \<in> A. \<forall>g \<in> A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)"
  shows "finite (rangeC (A :: ('a \<Rightarrow> 'b) set)) \<longleftrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite (UNIV :: 'a set))"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (rangeC A) = (finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (rangeC A) \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
 2. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV) \<Longrightarrow> finite (rangeC A)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
finite (rangeC A)

goal (2 subgoals):
 1. finite (rangeC A) \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
 2. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV) \<Longrightarrow> finite (rangeC A)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
finite (rangeC A)

goal (1 subgoal):
 1. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
using inj disjoint
[PROOF STATE]
proof (prove)
using this:
finite (rangeC A)
\<forall>f\<in>A. inj f
\<forall>f\<in>A. \<forall>g\<in>A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)

goal (1 subgoal):
 1. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
proof(induct "rangeC A" arbitrary: A rule: finite_psubset_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>finite (rangeC A); \<And>Aa. \<lbrakk>rangeC Aa \<subset> rangeC A; \<forall>f\<in>Aa. inj f; \<forall>f\<in>Aa. \<forall>g\<in>Aa. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)\<rbrakk> \<Longrightarrow> finite Aa \<and> (Aa \<noteq> {} \<longrightarrow> finite UNIV); \<forall>f\<in>A. inj f; \<forall>f\<in>A. \<forall>g\<in>A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)\<rbrakk> \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
case (psubset A)
[PROOF STATE]
proof (state)
this:
finite (rangeC A)
\<lbrakk>rangeC ?A \<subset> rangeC A; \<forall>f\<in>?A. inj f; \<forall>f\<in>?A. \<forall>g\<in>?A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)\<rbrakk> \<Longrightarrow> finite ?A \<and> (?A \<noteq> {} \<longrightarrow> finite UNIV)
\<forall>f\<in>A. inj f
\<forall>f\<in>A. \<forall>g\<in>A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)

goal (1 subgoal):
 1. \<And>A. \<lbrakk>finite (rangeC A); \<And>Aa. \<lbrakk>rangeC Aa \<subset> rangeC A; \<forall>f\<in>Aa. inj f; \<forall>f\<in>Aa. \<forall>g\<in>Aa. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)\<rbrakk> \<Longrightarrow> finite Aa \<and> (Aa \<noteq> {} \<longrightarrow> finite UNIV); \<forall>f\<in>A. inj f; \<forall>f\<in>A. \<forall>g\<in>A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)\<rbrakk> \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
proof(cases "A = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
 2. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = {}

goal (2 subgoals):
 1. A = {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
 2. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = {}

goal (1 subgoal):
 1. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
[PROOF STEP]
obtain f A' where A: "A = insert f A'" and f: "f \<in> A" "f \<notin> A'"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. (\<And>f A'. \<lbrakk>A = insert f A'; f \<in> A; f \<notin> A'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest: mk_disjoint_insert)
[PROOF STATE]
proof (state)
this:
A = insert f A'
f \<in> A
f \<notin> A'

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A = insert f A'
[PROOF STEP]
have rA: "rangeC A = rangeC A' \<union> range f"
[PROOF STATE]
proof (prove)
using this:
A = insert f A'

goal (1 subgoal):
 1. rangeC A = rangeC A' \<union> range f
[PROOF STEP]
by(auto simp add: rangeC_def)
[PROOF STATE]
proof (state)
this:
rangeC A = rangeC A' \<union> range f

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
have "\<not> range f \<subseteq> rangeC A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> range f \<subseteq> rangeC A'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
assume "range f \<subseteq> rangeC A'"
[PROOF STATE]
proof (state)
this:
range f \<subseteq> rangeC A'

goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
range f \<subseteq> rangeC A'

goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
obtain x where x: "x \<in> range f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> range f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> range f

goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
range f \<subseteq> rangeC A'
x \<in> range f
[PROOF STEP]
have "x \<in> rangeC A'"
[PROOF STATE]
proof (prove)
using this:
range f \<subseteq> rangeC A'
x \<in> range f

goal (1 subgoal):
 1. x \<in> rangeC A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> rangeC A'

goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> rangeC A'
[PROOF STEP]
obtain g where "g \<in> A'" "x \<in> range g"
[PROOF STATE]
proof (prove)
using this:
x \<in> rangeC A'

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> A'; x \<in> range g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: rangeC_def)
[PROOF STATE]
proof (state)
this:
g \<in> A'
x \<in> range g

goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
with \<open>f \<notin> A'\<close> A
[PROOF STATE]
proof (chain)
picking this:
f \<notin> A'
A = insert f A'
g \<in> A'
x \<in> range g
[PROOF STEP]
have "g \<in> A" "f \<noteq> g"
[PROOF STATE]
proof (prove)
using this:
f \<notin> A'
A = insert f A'
g \<in> A'
x \<in> range g

goal (1 subgoal):
 1. g \<in> A &&& f \<noteq> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> A
f \<noteq> g

goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
with \<open>f \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> A
g \<in> A
f \<noteq> g
[PROOF STEP]
have "\<And>x y. f x \<noteq> g y"
[PROOF STATE]
proof (prove)
using this:
f \<in> A
g \<in> A
f \<noteq> g

goal (1 subgoal):
 1. \<And>x y. f x \<noteq> g y
[PROOF STEP]
by(rule psubset.prems[rule_format])
[PROOF STATE]
proof (state)
this:
f ?x \<noteq> g ?y

goal (1 subgoal):
 1. range f \<subseteq> rangeC A' \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
f ?x \<noteq> g ?y

goal (1 subgoal):
 1. False
[PROOF STEP]
using x \<open>x \<in> range g\<close>
[PROOF STATE]
proof (prove)
using this:
f ?x \<noteq> g ?y
x \<in> range f
x \<in> range g

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> range f \<subseteq> rangeC A'

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
hence "rangeC A' \<subset> rangeC A"
[PROOF STATE]
proof (prove)
using this:
\<not> range f \<subseteq> rangeC A'

goal (1 subgoal):
 1. rangeC A' \<subset> rangeC A
[PROOF STEP]
unfolding rA
[PROOF STATE]
proof (prove)
using this:
\<not> range f \<subseteq> rangeC A'

goal (1 subgoal):
 1. rangeC A' \<subset> rangeC A' \<union> range f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rangeC A' \<subset> rangeC A

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
hence "finite A' \<and> (A' \<noteq> {} \<longrightarrow> finite (UNIV :: 'a set))"
[PROOF STATE]
proof (prove)
using this:
rangeC A' \<subset> rangeC A

goal (1 subgoal):
 1. finite A' \<and> (A' \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
using psubset.prems
[PROOF STATE]
proof (prove)
using this:
rangeC A' \<subset> rangeC A
\<forall>f\<in>A. inj f
\<forall>f\<in>A. \<forall>g\<in>A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)

goal (1 subgoal):
 1. finite A' \<and> (A' \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
by -(erule psubset.hyps, auto simp add: A)
[PROOF STATE]
proof (state)
this:
finite A' \<and> (A' \<noteq> {} \<longrightarrow> finite UNIV)

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
A = insert f A'
finite A' \<and> (A' \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
have "finite A"
[PROOF STATE]
proof (prove)
using this:
A = insert f A'
finite A' \<and> (A' \<noteq> {} \<longrightarrow> finite UNIV)

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
with \<open>finite (rangeC A)\<close> A \<open>\<forall>f \<in> A. inj f\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (rangeC A)
A = insert f A'
\<forall>f\<in>A. inj f
finite A
[PROOF STEP]
have "finite (UNIV :: 'a set)"
[PROOF STATE]
proof (prove)
using this:
finite (rangeC A)
A = insert f A'
\<forall>f\<in>A. inj f
finite A

goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
by(auto simp add: rangeC_def dest: finite_imageD)
[PROOF STATE]
proof (state)
this:
finite UNIV

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite A
finite UNIV
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A
finite UNIV

goal (1 subgoal):
 1. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV)

goal (1 subgoal):
 1. finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV) \<Longrightarrow> finite (rangeC A)
[PROOF STEP]
qed(auto simp add: rangeC_def)


[STATEMENT]
lemma finite_rangeC_singleton_const:
  "finite (rangeC {\<lambda>_. x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (rangeC {\<lambda>_. x})
[PROOF STEP]
by(auto simp add: rangeC_def image_def)


[STATEMENT]
lemma card_Un:
  "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> card (A \<union> B) = card (A) + card (B) - card(A \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> card (A \<union> B) = card A + card B - card (A \<inter> B)
[PROOF STEP]
by(subst card_Un_Int) simp_all


[STATEMENT]
lemma card_rangeC_singleton_const:
  "card (rangeC {\<lambda>_. f}) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (rangeC {\<lambda>_. f}) = 1
[PROOF STEP]
by(simp add: rangeC_def image_def)


[STATEMENT]
lemma card_rangeC:
  assumes inj: "\<forall>f \<in> A. inj f"
  and disjoint: "\<forall>f \<in> A. \<forall>g \<in> A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)"
  shows "card (rangeC (A :: ('a \<Rightarrow> 'b) set)) = CARD('a) * card A"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (rangeC A) = CARD('a) * card A
[PROOF STEP]
proof(cases "finite (UNIV :: 'a set) \<and> finite A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
 2. \<not> (finite UNIV \<and> finite A) \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (finite UNIV \<and> finite A)

goal (2 subgoals):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
 2. \<not> (finite UNIV \<and> finite A) \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (finite UNIV \<and> finite A)

goal (1 subgoal):
 1. card (rangeC A) = CARD('a) * card A
[PROOF STEP]
using False finite_rangeC[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<not> (finite UNIV \<and> finite A)
\<not> (finite UNIV \<and> finite A)
finite (rangeC A) = (finite A \<and> (A \<noteq> {} \<longrightarrow> finite UNIV))

goal (1 subgoal):
 1. card (rangeC A) = CARD('a) * card A
[PROOF STEP]
by(auto simp add: card_eq_0_iff rangeC_eq_empty)
[PROOF STATE]
proof (state)
this:
card (rangeC A) = CARD('a) * card A

goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite UNIV \<and> finite A

goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite UNIV \<and> finite A

goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
assume "f \<in> A"
[PROOF STATE]
proof (state)
this:
f \<in> A

goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
hence "card (range f) = CARD('a)"
[PROOF STATE]
proof (prove)
using this:
f \<in> A

goal (1 subgoal):
 1. card (range f) = CARD('a)
[PROOF STEP]
using inj
[PROOF STATE]
proof (prove)
using this:
f \<in> A
\<forall>f\<in>A. inj f

goal (1 subgoal):
 1. card (range f) = CARD('a)
[PROOF STEP]
by(simp add: card_image)
[PROOF STATE]
proof (state)
this:
card (range f) = CARD('a)

goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?f2 \<in> A \<Longrightarrow> card (range ?f2) = CARD('a)

goal (1 subgoal):
 1. finite UNIV \<and> finite A \<Longrightarrow> card (rangeC A) = CARD('a) * card A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?f2 \<in> A \<Longrightarrow> card (range ?f2) = CARD('a)

goal (1 subgoal):
 1. card (rangeC A) = CARD('a) * card A
[PROOF STEP]
using disjoint True
[PROOF STATE]
proof (prove)
using this:
?f2 \<in> A \<Longrightarrow> card (range ?f2) = CARD('a)
\<forall>f\<in>A. \<forall>g\<in>A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)
finite UNIV \<and> finite A

goal (1 subgoal):
 1. card (rangeC A) = CARD('a) * card A
[PROOF STEP]
unfolding rangeC_def
[PROOF STATE]
proof (prove)
using this:
?f2 \<in> A \<Longrightarrow> card (range ?f2) = CARD('a)
\<forall>f\<in>A. \<forall>g\<in>A. f \<noteq> g \<longrightarrow> (\<forall>x y. f x \<noteq> g y)
finite UNIV \<and> finite A

goal (1 subgoal):
 1. card (\<Union> (range ` A)) = CARD('a) * card A
[PROOF STEP]
by(subst card_UN_disjoint) auto
[PROOF STATE]
proof (state)
this:
card (rangeC A) = CARD('a) * card A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rangeC_Int_rangeC:
  "\<lbrakk> \<forall>f \<in> A. \<forall>g \<in> B. \<forall>x y. f x \<noteq> g y \<rbrakk> \<Longrightarrow> rangeC A \<inter> rangeC B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>A. \<forall>g\<in>B. \<forall>x y. f x \<noteq> g y \<Longrightarrow> rangeC A \<inter> rangeC B = {}
[PROOF STEP]
by(auto simp add: rangeC_def)


[STATEMENT]
lemma CARD_fun [card_simps]:
  "CARD('a \<Rightarrow> 'b) = card_fun CARD('a) CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a \<Rightarrow> 'b) = card_fun CARD('a) CARD('b)
[PROOF STEP]
by(simp add: card_fun card_fun_def)


[STATEMENT]
lemma CARD_sum [card_simps]:
  "CARD('a + 'b) = card_sum CARD('a) CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a + 'b) = card_sum CARD('a) CARD('b)
[PROOF STEP]
by(simp add: card_UNIV_sum card_sum_def)


[STATEMENT]
lemma CARD_option [card_simps]:
  "CARD('a option) = card_option CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a option) = card_option CARD('a)
[PROOF STEP]
by(simp add: card_option_def card_UNIV_option)


[STATEMENT]
lemma CARD_prod [card_simps]:
  "CARD('a * 'b) = card_prod CARD('a) CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a \<times> 'b) = card_prod CARD('a) CARD('b)
[PROOF STEP]
by(simp add: card_prod_def)


[STATEMENT]
lemma CARD_list [card_simps]: "CARD('a list) = card_list CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('a list) = card_list CARD('a)
[PROOF STEP]
by(simp add: card_list_def infinite_UNIV_listI)


[STATEMENT]
lemma conflict_free:
":G:\<lbrakk>A_Lbl l\<rbrakk> = {} \<longleftrightarrow> (\<forall> (l',x,y)\<in>edges G. l' \<noteq> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (:G:\<lbrakk>A_Lbl l\<rbrakk> = {}) = (\<forall>(l', x, y)\<in>edges G. l' \<noteq> l)
[PROOF STEP]
by (auto simp:getRel_def)


[STATEMENT]
lemma top_rule[simp]:
  assumes "graph G"
  shows "maintained (top_rule r) G \<longleftrightarrow> vertices G \<times> vertices G = getRel r G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (top_rule r) G = (vertices G \<times> vertices G = getRel r G)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
assume a:"maintained (top_rule r) G"
[PROOF STATE]
proof (state)
this:
maintained (top_rule r) G

goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
maintained (top_rule r) G

goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
assume "a \<in> vertices G" "b \<in> vertices G"
[PROOF STATE]
proof (state)
this:
a \<in> vertices G
b \<in> vertices G

goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
hence "graph_homomorphism (LG {} {0, 1}) G {(0::nat,a),(1,b)}"
[PROOF STATE]
proof (prove)
using this:
a \<in> vertices G
b \<in> vertices G

goal (1 subgoal):
 1. graph_homomorphism (LG {} {0, 1}) G {(0, a), (1, b)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> vertices G
b \<in> vertices G
graph G

goal (1 subgoal):
 1. graph_homomorphism (LG {} {0, 1}) G {(0, a), (1, b)}
[PROOF STEP]
unfolding graph_homomorphism_def univalent_def
[PROOF STATE]
proof (prove)
using this:
a \<in> vertices G
b \<in> vertices G
graph G

goal (1 subgoal):
 1. vertices (LG {} {0, 1}) = Domain {(0, a), (1, b)} \<and> graph (LG {} {0, 1}) \<and> graph G \<and> {(0, a), (1, b)} `` vertices (LG {} {0, 1}) \<subseteq> vertices G \<and> (\<forall>x y z. (x, y) \<in> {(0, a), (1, b)} \<and> (x, z) \<in> {(0, a), (1, b)} \<longrightarrow> z = y) \<and> edge_preserving {(0, a), (1, b)} (edges (LG {} {0, 1})) (edges G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {} {0, 1}) G {(0, a), (1, b)}

goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
with a[unfolded maintained_def top_rule_def] extensible_refl_concr
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. graph_homomorphism (fst (LG {} {0, 1}, LG {(r, 0, 1)} {0, 1})) G f \<longrightarrow> extensible (LG {} {0, 1}, LG {(r, 0, 1)} {0, 1}) G f
graph_homomorphism (LG ?e\<^sub>1 ?v) ?G ?f \<Longrightarrow> extensible (LG ?e\<^sub>1 ?v, LG ?e\<^sub>2 ?v) ?G ?f = graph_homomorphism (LG ?e\<^sub>2 ?v) ?G ?f
graph_homomorphism (LG {} {0, 1}) G {(0, a), (1, b)}
[PROOF STEP]
have "graph_homomorphism (LG {(r, 0, 1)} {0::nat, 1}) G {(0::nat, a), (1, b)}"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. graph_homomorphism (fst (LG {} {0, 1}, LG {(r, 0, 1)} {0, 1})) G f \<longrightarrow> extensible (LG {} {0, 1}, LG {(r, 0, 1)} {0, 1}) G f
graph_homomorphism (LG ?e\<^sub>1 ?v) ?G ?f \<Longrightarrow> extensible (LG ?e\<^sub>1 ?v, LG ?e\<^sub>2 ?v) ?G ?f = graph_homomorphism (LG ?e\<^sub>2 ?v) ?G ?f
graph_homomorphism (LG {} {0, 1}) G {(0, a), (1, b)}

goal (1 subgoal):
 1. graph_homomorphism (LG {(r, 0, 1)} {0, 1}) G {(0, a), (1, b)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {(r, 0, 1)} {0, 1}) G {(0, a), (1, b)}

goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
hence "(a, b) \<in> getRel r G"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG {(r, 0, 1)} {0, 1}) G {(0, a), (1, b)}

goal (1 subgoal):
 1. (a, b) \<in> getRel r G
[PROOF STEP]
unfolding graph_homomorphism_def2 graph_union_iff getRel_def
[PROOF STATE]
proof (prove)
using this:
vertices (LG {(r, 0, 1)} {0, 1}) = Domain {(0, a), (1, b)} \<and> univalent {(0, a), (1, b)} \<and> graph (LG {(r, 0, 1)} {0, 1}) \<and> graph G \<and> edges (map_graph {(0, a), (1, b)} (LG {(r, 0, 1)} {0, 1})) \<subseteq> edges G \<and> vertices (map_graph {(0, a), (1, b)} (LG {(r, 0, 1)} {0, 1})) \<subseteq> vertices G

goal (1 subgoal):
 1. (a, b) \<in> {(x, y). (r, x, y) \<in> edges G}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, b) \<in> getRel r G

goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<in> vertices G; ?b2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?a2, ?b2) \<in> getRel r G

goal (2 subgoals):
 1. maintained (top_rule r) G \<Longrightarrow> vertices G \<times> vertices G = getRel r G
 2. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
thus "vertices G \<times> vertices G = getRel r G"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a2 \<in> vertices G; ?b2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?a2, ?b2) \<in> getRel r G

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G
[PROOF STEP]
using getRel_dom[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a2 \<in> vertices G; ?b2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?a2, ?b2) \<in> getRel r G
(?a, ?b) \<in> getRel ?l G \<Longrightarrow> ?a \<in> vertices G
(?a, ?b) \<in> getRel ?l G \<Longrightarrow> ?b \<in> vertices G

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vertices G \<times> vertices G = getRel r G

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
assume a:"vertices G \<times> vertices G = getRel r G"
[PROOF STATE]
proof (state)
this:
vertices G \<times> vertices G = getRel r G

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
vertices G \<times> vertices G = getRel r G

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
assume a2:"graph_homomorphism (fst (top_rule r)) G f"
[PROOF STATE]
proof (state)
this:
graph_homomorphism (fst (top_rule r)) G f

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
hence f:"f `` {0, 1} \<subseteq> vertices G" "on_triple f `` {} \<subseteq> edges G"
          "univalent f" "Domain f = {0, 1}"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst (top_rule r)) G f

goal (1 subgoal):
 1. (f `` {0, 1} \<subseteq> vertices G &&& on_triple f `` {} \<subseteq> edges G) &&& univalent f &&& Domain f = {0, 1}
[PROOF STEP]
unfolding top_rule_def prod.sel graph_homomorphism_concr_graph[OF assms graph_empty_e]
[PROOF STATE]
proof (prove)
using this:
f `` {0, 1} \<subseteq> vertices G \<and> on_triple f `` {} \<subseteq> edges G \<and> univalent f \<and> Domain f = {0, 1}

goal (1 subgoal):
 1. (f `` {0, 1} \<subseteq> vertices G &&& on_triple f `` {} \<subseteq> edges G) &&& univalent f &&& Domain f = {0, 1}
[PROOF STEP]
by argo+
[PROOF STATE]
proof (state)
this:
f `` {0, 1} \<subseteq> vertices G
on_triple f `` {} \<subseteq> edges G
univalent f
Domain f = {0, 1}

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
from a2
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (fst (top_rule r)) G f
[PROOF STEP]
have ih:"graph_homomorphism (LG {} {0, 1}) G f"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst (top_rule r)) G f

goal (1 subgoal):
 1. graph_homomorphism (LG {} {0, 1}) G f
[PROOF STEP]
unfolding top_rule_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst (LG {} {0, 1}, LG {(r, 0, 1)} {0, 1})) G f

goal (1 subgoal):
 1. graph_homomorphism (LG {} {0, 1}) G f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {} {0, 1}) G f

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
have "extensible (top_rule r) G f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible (top_rule r) G f
[PROOF STEP]
unfolding top_rule_def extensible_refl_concr[OF ih]
      graph_homomorphism_concr_graph[OF assms graph_single]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f `` {0, 1} \<subseteq> vertices G \<and> on_triple f `` {(r, 0, 1)} \<subseteq> edges G \<and> univalent f \<and> Domain f = {0, 1}
[PROOF STEP]
using f a[unfolded getRel_def]
[PROOF STATE]
proof (prove)
using this:
f `` {0, 1} \<subseteq> vertices G
on_triple f `` {} \<subseteq> edges G
univalent f
Domain f = {0, 1}
vertices G \<times> vertices G = {(x, y). (r, x, y) \<in> edges G}

goal (1 subgoal):
 1. f `` {0, 1} \<subseteq> vertices G \<and> on_triple f `` {(r, 0, 1)} \<subseteq> edges G \<and> univalent f \<and> Domain f = {0, 1}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
extensible (top_rule r) G f

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
graph_homomorphism (fst (top_rule r)) G ?f2 \<Longrightarrow> extensible (top_rule r) G ?f2

goal (1 subgoal):
 1. vertices G \<times> vertices G = getRel r G \<Longrightarrow> maintained (top_rule r) G
[PROOF STEP]
thus "maintained (top_rule r) G"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst (top_rule r)) G ?f2 \<Longrightarrow> extensible (top_rule r) G ?f2

goal (1 subgoal):
 1. maintained (top_rule r) G
[PROOF STEP]
unfolding maintained_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst (top_rule r)) G ?f2 \<Longrightarrow> extensible (top_rule r) G ?f2

goal (1 subgoal):
 1. \<forall>f. graph_homomorphism (fst (top_rule r)) G f \<longrightarrow> extensible (top_rule r) G f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maintained (top_rule r) G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonempty_rule[simp]:
  assumes "graph G"
  shows "maintained nonempty_rule G \<longleftrightarrow> vertices G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained nonempty_rule G = (vertices G \<noteq> {})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained nonempty_rule G = (vertices G \<noteq> {})
[PROOF STEP]
have "vertices G = {} \<Longrightarrow> graph_homomorphism (LG {} {0}) G x \<Longrightarrow> False"
       "v \<in> vertices G \<Longrightarrow> graph_homomorphism (LG {} {0}) G {(0,v)}"
       for v::"'b" and x::"(nat \<times> 'b) set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>vertices G = {}; graph_homomorphism (LG {} {0}) G x\<rbrakk> \<Longrightarrow> False) &&& (v \<in> vertices G \<Longrightarrow> graph_homomorphism (LG {} {0::'c}) G {(0::'c, v)})
[PROOF STEP]
unfolding graph_homomorphism_concr_graph[OF assms graph_empty_e] univalent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>vertices G = {}; x `` {0} \<subseteq> vertices G \<and> on_triple x `` {} \<subseteq> edges G \<and> (\<forall>xa y z. (xa, y) \<in> x \<and> (xa, z) \<in> x \<longrightarrow> z = y) \<and> Domain x = {0}\<rbrakk> \<Longrightarrow> False) &&& (v \<in> vertices G \<Longrightarrow> {(0::'c, v)} `` {0::'c} \<subseteq> vertices G \<and> on_triple {(0::'c, v)} `` {} \<subseteq> edges G \<and> (\<forall>x y z. (x, y) \<in> {(0::'c, v)} \<and> (x, z) \<in> {(0::'c, v)} \<longrightarrow> z = y) \<and> Domain {(0::'c, v)} = {0::'c})
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<lbrakk>vertices G = {}; graph_homomorphism (LG {} {0}) G ?x1\<rbrakk> \<Longrightarrow> False
?v1 \<in> vertices G \<Longrightarrow> graph_homomorphism (LG {} {0::?'c2}) G {(0::?'c2, ?v1)}

goal (1 subgoal):
 1. maintained nonempty_rule G = (vertices G \<noteq> {})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vertices G = {}; graph_homomorphism (LG {} {0}) G ?x1\<rbrakk> \<Longrightarrow> False
?v1 \<in> vertices G \<Longrightarrow> graph_homomorphism (LG {} {0::?'c2}) G {(0::?'c2, ?v1)}

goal (1 subgoal):
 1. maintained nonempty_rule G = (vertices G \<noteq> {})
[PROOF STEP]
unfolding nonempty_rule_def maintained_def extensible_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vertices G = {}; graph_homomorphism (LG {} {0}) G ?x1\<rbrakk> \<Longrightarrow> False
?v1 \<in> vertices G \<Longrightarrow> graph_homomorphism (LG {} {0::?'c2}) G {(0::?'c2, ?v1)}

goal (1 subgoal):
 1. (\<forall>f. graph_homomorphism (fst (LG {} {}, LG {} {0})) G f \<longrightarrow> (\<exists>g. graph_homomorphism (snd (LG {} {}, LG {} {0})) G g \<and> agree_on (fst (LG {} {}, LG {} {0})) f g)) = (vertices G \<noteq> {})
[PROOF STEP]
by (auto intro:assms)
[PROOF STATE]
proof (state)
this:
maintained nonempty_rule G = (vertices G \<noteq> {})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma are_rules[intro]:
"graph_rule nonempty_rule"
"graph_rule (top_rule t)"
"graph_rule (reflexivity_rule i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_rule nonempty_rule &&& graph_rule (top_rule t) &&& graph_rule (reflexivity_rule i)
[PROOF STEP]
unfolding reflexivity_rule_def top_rule_def nonempty_rule_def graph_homomorphism_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vertices (fst (LG {} {}, LG {} {0})) = Domain (Id_on (vertices (fst (LG {} {}, LG {} {0})))) \<and> graph (fst (LG {} {}, LG {} {0})) \<and> graph (snd (LG {} {}, LG {} {0})) \<and> Id_on (vertices (fst (LG {} {}, LG {} {0}))) `` vertices (fst (LG {} {}, LG {} {0})) \<subseteq> vertices (snd (LG {} {}, LG {} {0})) \<and> univalent (Id_on (vertices (fst (LG {} {}, LG {} {0})))) \<and> edge_preserving (Id_on (vertices (fst (LG {} {}, LG {} {0})))) (edges (fst (LG {} {}, LG {} {0}))) (edges (snd (LG {} {}, LG {} {0})))) \<and> finite_graph (snd (LG {} {}, LG {} {0})) &&& (vertices (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})) = Domain (Id_on (vertices (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})))) \<and> graph (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})) \<and> graph (snd (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})) \<and> Id_on (vertices (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1}))) `` vertices (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})) \<subseteq> vertices (snd (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})) \<and> univalent (Id_on (vertices (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})))) \<and> edge_preserving (Id_on (vertices (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})))) (edges (fst (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1}))) (edges (snd (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})))) \<and> finite_graph (snd (LG {} {0, 1}, LG {(t, 0, 1)} {0, 1})) &&& (vertices (fst (LG {} {0}, LG {(i, 0, 0)} {0})) = Domain (Id_on (vertices (fst (LG {} {0}, LG {(i, 0, 0)} {0})))) \<and> graph (fst (LG {} {0}, LG {(i, 0, 0)} {0})) \<and> graph (snd (LG {} {0}, LG {(i, 0, 0)} {0})) \<and> Id_on (vertices (fst (LG {} {0}, LG {(i, 0, 0)} {0}))) `` vertices (fst (LG {} {0}, LG {(i, 0, 0)} {0})) \<subseteq> vertices (snd (LG {} {0}, LG {(i, 0, 0)} {0})) \<and> univalent (Id_on (vertices (fst (LG {} {0}, LG {(i, 0, 0)} {0})))) \<and> edge_preserving (Id_on (vertices (fst (LG {} {0}, LG {(i, 0, 0)} {0})))) (edges (fst (LG {} {0}, LG {(i, 0, 0)} {0}))) (edges (snd (LG {} {0}, LG {(i, 0, 0)} {0})))) \<and> finite_graph (snd (LG {} {0}, LG {(i, 0, 0)} {0}))
[PROOF STEP]
by auto


[STATEMENT]
lemma ident_rel_refl:
  assumes "graph G" "ident_rel idt G"
  shows "maintained (reflexivity_rule idt) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (reflexivity_rule idt) G
[PROOF STEP]
unfolding reflexivity_rule_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (LG {} {0}, LG {(idt, 0, 0)} {0}) G
[PROOF STEP]
proof(rule maintainedI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. graph_homomorphism (LG {} {0}) G f \<Longrightarrow> extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. graph_homomorphism (LG {} {0}) G f \<Longrightarrow> extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f
[PROOF STEP]
assume "graph_homomorphism (LG {} {0::nat}) G f"
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {} {0}) G f

goal (1 subgoal):
 1. \<And>f. graph_homomorphism (LG {} {0}) G f \<Longrightarrow> extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f
[PROOF STEP]
hence f:"Domain f = {0}" "graph G" "f `` {0} \<subseteq> vertices G" "univalent f"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG {} {0}) G f

goal (1 subgoal):
 1. (Domain f = {0} &&& graph G) &&& f `` {0} \<subseteq> vertices G &&& univalent f
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices (LG {} {0}) = Domain f \<and> graph (LG {} {0}) \<and> graph G \<and> f `` vertices (LG {} {0}) \<subseteq> vertices G \<and> univalent f \<and> edge_preserving f (edges (LG {} {0})) (edges G)

goal (1 subgoal):
 1. (Domain f = {0} &&& graph G) &&& f `` {0} \<subseteq> vertices G &&& univalent f
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
Domain f = {0}
graph G
f `` {0} \<subseteq> vertices G
univalent f

goal (1 subgoal):
 1. \<And>f. graph_homomorphism (LG {} {0}) G f \<Longrightarrow> extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f
[PROOF STEP]
from assms(2) univalentD[OF f(4)] f(3)
[PROOF STATE]
proof (chain)
picking this:
ident_rel idt G
\<lbrakk>(?x, ?y) \<in> f; (?x, ?z) \<in> f\<rbrakk> \<Longrightarrow> ?z = ?y
f `` {0} \<subseteq> vertices G
[PROOF STEP]
have "edge_preserving f {(idt, 0, 0)} (edges G)"
[PROOF STATE]
proof (prove)
using this:
ident_rel idt G
\<lbrakk>(?x, ?y) \<in> f; (?x, ?z) \<in> f\<rbrakk> \<Longrightarrow> ?z = ?y
f `` {0} \<subseteq> vertices G

goal (1 subgoal):
 1. edge_preserving f {(idt, 0, 0)} (edges G)
[PROOF STEP]
unfolding edge_preserving
[PROOF STATE]
proof (prove)
using this:
ident_rel idt G
\<lbrakk>(?x, ?y) \<in> f; (?x, ?z) \<in> f\<rbrakk> \<Longrightarrow> ?z = ?y
f `` {0} \<subseteq> vertices G

goal (1 subgoal):
 1. on_triple f `` {(idt, 0, 0)} \<subseteq> edges G
[PROOF STEP]
by (auto simp:getRel_def set_eq_iff image_def)
[PROOF STATE]
proof (state)
this:
edge_preserving f {(idt, 0, 0)} (edges G)

goal (1 subgoal):
 1. \<And>f. graph_homomorphism (LG {} {0}) G f \<Longrightarrow> extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
Domain f = {0}
graph G
f `` {0} \<subseteq> vertices G
univalent f
edge_preserving f {(idt, 0, 0)} (edges G)
[PROOF STEP]
have "graph_homomorphism (LG {(idt, 0, 0)} {0}) G f"
              "agree_on (LG {} {0}) f f"
[PROOF STATE]
proof (prove)
using this:
Domain f = {0}
graph G
f `` {0} \<subseteq> vertices G
univalent f
edge_preserving f {(idt, 0, 0)} (edges G)

goal (1 subgoal):
 1. graph_homomorphism (LG {(idt, 0, 0)} {0}) G f &&& agree_on (LG {} {0}) f f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Domain f = {0}
graph G
f `` {0} \<subseteq> vertices G
univalent f
edge_preserving f {(idt, 0, 0)} (edges G)
graph G
ident_rel idt G

goal (1 subgoal):
 1. graph_homomorphism (LG {(idt, 0, 0)} {0}) G f &&& agree_on (LG {} {0}) f f
[PROOF STEP]
unfolding graph_homomorphism_def labeled_graph.sel agree_on_def univalent_def
[PROOF STATE]
proof (prove)
using this:
Domain f = {0}
graph G
f `` {0} \<subseteq> vertices G
\<forall>x y z. (x, y) \<in> f \<and> (x, z) \<in> f \<longrightarrow> z = y
edge_preserving f {(idt, 0, 0)} (edges G)
graph G
ident_rel idt G

goal (1 subgoal):
 1. {0} = Domain f \<and> graph (LG {(idt, 0, 0)} {0}) \<and> graph G \<and> f `` {0} \<subseteq> vertices G \<and> (\<forall>x y z. (x, y) \<in> f \<and> (x, z) \<in> f \<longrightarrow> z = y) \<and> edge_preserving f {(idt, 0, 0)} (edges G) &&& \<forall>v\<in>{0}. f `` {v} = f `` {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {(idt, 0, 0)} {0}) G f
agree_on (LG {} {0}) f f

goal (1 subgoal):
 1. \<And>f. graph_homomorphism (LG {} {0}) G f \<Longrightarrow> extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (LG {(idt, 0, 0)} {0}) G f
agree_on (LG {} {0}) f f
[PROOF STEP]
show "extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG {(idt, 0, 0)} {0}) G f
agree_on (LG {} {0}) f f

goal (1 subgoal):
 1. extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f
[PROOF STEP]
unfolding extensible_def prod.sel
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG {(idt, 0, 0)} {0}) G f
agree_on (LG {} {0}) f f

goal (1 subgoal):
 1. \<exists>g. graph_homomorphism (LG {(idt, 0, 0)} {0}) G g \<and> agree_on (LG {} {0}) f g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma identity_rules_graph_rule:
  assumes "x \<in> identity_rules L"
  shows "graph_rule x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
from graph_rule_translation
[PROOF STATE]
proof (chain)
picking this:
graph_rule (translation ?X, translation (A_Int ?X ?Y))
[PROOF STEP]
have gr:"\<And> u v . graph_rule (transl_rule (u \<sqsubseteq> v))"
[PROOF STATE]
proof (prove)
using this:
graph_rule (translation ?X, translation (A_Int ?X ?Y))

goal (1 subgoal):
 1. \<And>u v. graph_rule (transl_rule (u \<sqsubseteq> v))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_rule (transl_rule (?u \<sqsubseteq> ?v))

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
consider "x = reflexivity_rule S_Idt" | "x = transitive_rule S_Idt" | "x = symmetry_rule S_Idt"
    |  "\<exists> v w. x = congruence_rule v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> thesis; x = transitive_rule S_Idt \<Longrightarrow> thesis; x = symmetry_rule S_Idt \<Longrightarrow> thesis; \<exists>v w. x = congruence_rule v w \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> identity_rules L

goal (1 subgoal):
 1. \<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> thesis; x = transitive_rule S_Idt \<Longrightarrow> thesis; x = symmetry_rule S_Idt \<Longrightarrow> thesis; \<exists>v w. x = congruence_rule v w \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding identity_rules_def Un_iff
[PROOF STATE]
proof (prove)
using this:
x \<in> {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} \<or> x \<in> congruence_rules S_Idt L

goal (1 subgoal):
 1. \<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> thesis; x = transitive_rule S_Idt \<Longrightarrow> thesis; x = symmetry_rule S_Idt \<Longrightarrow> thesis; \<exists>v w. x = congruence_rule v w \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> ?thesis1; x = transitive_rule S_Idt \<Longrightarrow> ?thesis1; x = symmetry_rule S_Idt \<Longrightarrow> ?thesis1; \<exists>v w. x = congruence_rule v w \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> ?thesis1; x = transitive_rule S_Idt \<Longrightarrow> ?thesis1; x = symmetry_rule S_Idt \<Longrightarrow> ?thesis1; \<exists>v w. x = congruence_rule v w \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
using gr are_rules(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> ?thesis1; x = transitive_rule S_Idt \<Longrightarrow> ?thesis1; x = symmetry_rule S_Idt \<Longrightarrow> ?thesis1; \<exists>v w. x = congruence_rule v w \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1
graph_rule (transl_rule (?u \<sqsubseteq> ?v))
graph_rule (reflexivity_rule ?i)

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
unfolding congruence_rule_def transitive_rule_def symmetry_rule_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> ?thesis1; x = transl_rule (A_Cmp \<one> \<one> \<sqsubseteq> \<one>) \<Longrightarrow> ?thesis1; x = transl_rule (A_Cnv \<one> \<sqsubseteq> \<one>) \<Longrightarrow> ?thesis1; \<exists>v w. x = transl_rule (A_Cmp (A_Cmp (A_Lbl v) (A_Lbl w)) (A_Lbl v) \<sqsubseteq> A_Lbl w) \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1
graph_rule (transl_rule (?u \<sqsubseteq> ?v))
graph_rule (reflexivity_rule ?i)

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
by cases fast+
[PROOF STATE]
proof (state)
this:
graph_rule x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_identity_rules[intro]:
  assumes "finite L"
  shows "finite (identity_rules L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (identity_rules L)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite L

goal (1 subgoal):
 1. finite (identity_rules L)
[PROOF STEP]
unfolding identity_rules_def
[PROOF STATE]
proof (prove)
using this:
finite L

goal (1 subgoal):
 1. finite ({reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} \<union> congruence_rules S_Idt L)
[PROOF STEP]
by auto


[STATEMENT]
lemma equivalence:
  assumes gr:"graph G" and m:"maintainedA {reflexivity_rule I,transitive_rule I,symmetry_rule I} G"
  shows "equiv (vertices G) (getRel I G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv (vertices G) (getRel I G)
[PROOF STEP]
proof(rule equivI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. refl_on (vertices G) (getRel I G)
 2. sym (getRel I G)
 3. trans (getRel I G)
[PROOF STEP]
show "refl_on (vertices G) (getRel I G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on (vertices G) (getRel I G)
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
maintainedA {reflexivity_rule I, transitive_rule I, symmetry_rule I} G

goal (1 subgoal):
 1. refl_on (vertices G) (getRel I G)
[PROOF STEP]
by(intro reflexivity_rule[OF gr],auto)
[PROOF STATE]
proof (state)
this:
refl_on (vertices G) (getRel I G)

goal (2 subgoals):
 1. sym (getRel I G)
 2. trans (getRel I G)
[PROOF STEP]
show "sym (getRel I G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (getRel I G)
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
maintainedA {reflexivity_rule I, transitive_rule I, symmetry_rule I} G

goal (1 subgoal):
 1. sym (getRel I G)
[PROOF STEP]
by(intro symmetry_rule[OF gr],auto)
[PROOF STATE]
proof (state)
this:
sym (getRel I G)

goal (1 subgoal):
 1. trans (getRel I G)
[PROOF STEP]
show "trans (getRel I G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (getRel I G)
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
maintainedA {reflexivity_rule I, transitive_rule I, symmetry_rule I} G

goal (1 subgoal):
 1. trans (getRel I G)
[PROOF STEP]
by(intro transitive_rule[OF gr],auto)
[PROOF STATE]
proof (state)
this:
trans (getRel I G)

goal:
No subgoals!
[PROOF STEP]
qed