[STATEMENT]
lemma kmin_prop:
fixes f :: "nat \<Rightarrow> Clocktime"
  shows
"(kmin f PR) \<subseteq> PR \<and> card (kmin f PR) = khl \<and>
                (\<forall>i\<in>(kmin f PR). \<forall>j\<in>PR - (kmin f PR). f i \<le> f j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)
[PROOF STEP]
have "khl <= np \<longrightarrow>
    (\<exists> S. S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))"
    ( is "khl <= np \<longrightarrow> ?P khl" )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. khl \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
proof(induct (khl))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = 0 \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
 2. \<And>n. n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)) \<Longrightarrow> Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
have "?P 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S\<subseteq>PR. card S = 0 \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>PR. card S = 0 \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (2 subgoals):
 1. 0 \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = 0 \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
 2. \<And>n. n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)) \<Longrightarrow> Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
thus "0 <= np \<longrightarrow> ?P 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>S\<subseteq>PR. card S = 0 \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. 0 \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = 0 \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
0 \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = 0 \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))

goal (1 subgoal):
 1. \<And>n. n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)) \<Longrightarrow> Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)) \<Longrightarrow> Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)) \<Longrightarrow> Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
assume asm: "n <= np \<longrightarrow> ?P n"
[PROOF STATE]
proof (state)
this:
n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))

goal (1 subgoal):
 1. \<And>n. n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)) \<Longrightarrow> Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
show "Suc n <= np \<longrightarrow> ?P (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
assume asm2: "Suc n <= np"
[PROOF STATE]
proof (state)
this:
Suc n \<le> np

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
with asm
[PROOF STATE]
proof (chain)
picking this:
n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
Suc n \<le> np
[PROOF STEP]
have "?P n"
[PROOF STATE]
proof (prove)
using this:
n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
Suc n \<le> np

goal (1 subgoal):
 1. \<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
obtain S where
        SinPR : "S\<subseteq>PR" and
        cardS: "card S = n" and
        HI: "(\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>S\<subseteq>PR. card S = n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>S \<subseteq> PR; card S = n; \<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<subseteq> PR
card S = n
\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
let ?e = "SOME i. i\<in>PR-S \<and>
        (\<forall>j\<in>PR-S. f i \<le> f j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
let ?S = "insert  ?e S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
have "\<exists>i. i\<in>PR-S \<and> (\<forall>j\<in>PR-S. f i \<le> f j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
from SinPR and finite_subset
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> PR
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
[PROOF STEP]
have "finite (PR-S)"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> PR
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (PR - S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (PR - S)

goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (PR - S)

goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
from cardS and asm2 SinPR
[PROOF STATE]
proof (chain)
picking this:
card S = n
Suc n \<le> np
S \<subseteq> PR
[PROOF STEP]
have "S\<subset>PR"
[PROOF STATE]
proof (prove)
using this:
card S = n
Suc n \<le> np
S \<subseteq> PR

goal (1 subgoal):
 1. S \<subset> PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<subset> PR

goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
hence "PR-S \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
S \<subset> PR

goal (1 subgoal):
 1. PR - S \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PR - S \<noteq> {}

goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (PR - S)
PR - S \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (PR - S)
PR - S \<noteq> {}

goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
using ex_Minf
[PROOF STATE]
proof (prove)
using this:
finite (PR - S)
PR - S \<noteq> {}
\<lbrakk>finite ?S; ?S \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>?S. \<forall>s\<in>?S. ?f m \<le> ?f s

goal (1 subgoal):
 1. \<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
hence
        ePRS: "?e \<in> PR-S" and minH: "(\<forall>j \<in> PR-S. f ?e \<le> f j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<in> PR - S &&& \<forall>j\<in>PR - S. f (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<le> f j
[PROOF STEP]
by (auto dest!: someI_ex)
[PROOF STATE]
proof (state)
this:
(SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<in> PR - S
\<forall>j\<in>PR - S. f (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<le> f j

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
from minH and  HI
[PROOF STATE]
proof (chain)
picking this:
\<forall>j\<in>PR - S. f (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<le> f j
\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j
[PROOF STEP]
have "(\<forall>i\<in>?S. \<forall>j\<in>PR - ?S. f i \<le> f j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>PR - S. f (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<le> f j
\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j

goal (1 subgoal):
 1. \<forall>i\<in>insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. \<forall>j\<in>PR - insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. f i \<le> f j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. \<forall>j\<in>PR - insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. f i \<le> f j

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. \<forall>j\<in>PR - insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. f i \<le> f j

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
from SinPR and finite_subset and
        cardS and ePRS
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> PR
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
card S = n
(SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<in> PR - S
[PROOF STEP]
have "card ?S = Suc n"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> PR
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
card S = n
(SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<in> PR - S

goal (1 subgoal):
 1. card (insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S) = Suc n
[PROOF STEP]
by (auto dest: card_insert_disjoint)
[PROOF STATE]
proof (state)
this:
card (insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S) = Suc n

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S) = Suc n

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
have "?S \<subseteq> PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S \<subseteq> PR
[PROOF STEP]
using SinPR and ePRS
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> PR
(SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) \<in> PR - S

goal (1 subgoal):
 1. insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S \<subseteq> PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S \<subseteq> PR

goal (1 subgoal):
 1. Suc n \<le> np \<Longrightarrow> \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. \<forall>j\<in>PR - insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. f i \<le> f j
card (insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S) = Suc n
insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S \<subseteq> PR
[PROOF STEP]
show "?P (Suc n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. \<forall>j\<in>PR - insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S. f i \<le> f j
card (insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S) = Suc n
insert (SOME i. i \<in> PR - S \<and> (\<forall>j\<in>PR - S. f i \<le> f j)) S \<subseteq> PR

goal (1 subgoal):
 1. \<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc n \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = Suc n \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
khl \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))

goal (1 subgoal):
 1. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)
[PROOF STEP]
hence "?P khl"
[PROOF STATE]
proof (prove)
using this:
khl \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))

goal (1 subgoal):
 1. \<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
using khl_bound
[PROOF STATE]
proof (prove)
using this:
khl \<le> np \<longrightarrow> (\<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j))
khl < np

goal (1 subgoal):
 1. \<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)
[PROOF STEP]
obtain S where
    "S\<le>PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>S\<subseteq>PR. card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. (\<And>S. S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)

goal (1 subgoal):
 1. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)
[PROOF STEP]
by (unfold kmin_def)
      (rule someI [where P="\<lambda>S. S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)"])
[PROOF STATE]
proof (state)
this:
kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_kmax:
"finite (kmax f PR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (kmax f PR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (kmax f PR)
[PROOF STEP]
have "finite PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite PR

goal (1 subgoal):
 1. finite (kmax f PR)
[PROOF STEP]
with  kmax_prop and finite_subset
[PROOF STATE]
proof (chain)
picking this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite PR

goal (1 subgoal):
 1. finite (kmax f PR)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (kmax f PR)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_kmin:
"finite (kmin f PR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (kmin f PR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (kmin f PR)
[PROOF STEP]
have "finite PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite PR

goal (1 subgoal):
 1. finite (kmin f PR)
[PROOF STEP]
with  kmin_prop and finite_subset
[PROOF STATE]
proof (chain)
picking this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite PR

goal (1 subgoal):
 1. finite (kmin f PR)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (kmin f PR)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduce_not_empty:
"reduce f PR \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
from constants_ax
[PROOF STATE]
proof (chain)
picking this:
2 * khl < np
[PROOF STEP]
have
    "0 < (np - 2 * khl)"
[PROOF STATE]
proof (prove)
using this:
2 * khl < np

goal (1 subgoal):
 1. 0 < np - 2 * khl
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 < np - 2 * khl

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 < np - 2 * khl

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < np - 2 * khl

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
from kmax_prop kmin_prop
[PROOF STATE]
proof (chain)
picking this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
[PROOF STEP]
have "card (kmax f PR) = khl \<and> card (kmin f PR) = khl"
[PROOF STATE]
proof (prove)
using this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)

goal (1 subgoal):
 1. card (kmax f PR) = khl \<and> card (kmin f PR) = khl
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (kmax f PR) = khl \<and> card (kmin f PR) = khl

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
hence "card (kmax f PR \<union> kmin f PR) <= 2 * khl"
[PROOF STATE]
proof (prove)
using this:
card (kmax f PR) = khl \<and> card (kmin f PR) = khl

goal (1 subgoal):
 1. card (kmax f PR \<union> kmin f PR) \<le> 2 * khl
[PROOF STEP]
using card_Un_le[of "kmax f PR" "kmin f PR"]
[PROOF STATE]
proof (prove)
using this:
card (kmax f PR) = khl \<and> card (kmin f PR) = khl
card (kmax f PR \<union> kmin f PR) \<le> card (kmax f PR) + card (kmin f PR)

goal (1 subgoal):
 1. card (kmax f PR \<union> kmin f PR) \<le> 2 * khl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (kmax f PR \<union> kmin f PR) \<le> 2 * khl

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
card (kmax f PR \<union> kmin f PR) \<le> 2 * khl

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
hence
    "... <= card PR - card (kmax f PR \<union> kmin f PR)"
[PROOF STATE]
proof (prove)
using this:
card (kmax f PR \<union> kmin f PR) \<le> 2 * khl

goal (1 subgoal):
 1. np - 2 * khl \<le> card PR - card (kmax f PR \<union> kmin f PR)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
np - 2 * khl \<le> card PR - card (kmax f PR \<union> kmin f PR)

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
np - 2 * khl \<le> card PR - card (kmax f PR \<union> kmin f PR)

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
np - 2 * khl \<le> card PR - card (kmax f PR \<union> kmin f PR)

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
from kmax_prop and kmin_prop
[PROOF STATE]
proof (chain)
picking this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
[PROOF STEP]
have
    "(kmax f PR \<union> kmin f PR) \<subseteq> PR"
[PROOF STATE]
proof (prove)
using this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)

goal (1 subgoal):
 1. kmax f PR \<union> kmin f PR \<subseteq> PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
kmax f PR \<union> kmin f PR \<subseteq> PR

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
kmax f PR \<union> kmin f PR \<subseteq> PR

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
hence
    "... = card (PR-(kmax f PR \<union> kmin f PR))"
[PROOF STATE]
proof (prove)
using this:
kmax f PR \<union> kmin f PR \<subseteq> PR

goal (1 subgoal):
 1. card PR - card (kmax f PR \<union> kmin f PR) = card (PR - (kmax f PR \<union> kmin f PR))
[PROOF STEP]
apply (intro card_Diff_subset[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. kmax f PR \<union> kmin f PR \<subseteq> PR \<Longrightarrow> finite (kmax f PR \<union> kmin f PR)
 2. kmax f PR \<union> kmin f PR \<subseteq> PR \<Longrightarrow> kmax f PR \<union> kmin f PR \<subseteq> PR
[PROOF STEP]
apply (rule finite_subset)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. kmax f PR \<union> kmin f PR \<subseteq> PR \<Longrightarrow> kmax f PR \<union> kmin f PR \<subseteq> ?B3
 2. kmax f PR \<union> kmin f PR \<subseteq> PR \<Longrightarrow> finite ?B3
 3. kmax f PR \<union> kmin f PR \<subseteq> PR \<Longrightarrow> kmax f PR \<union> kmin f PR \<subseteq> PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card PR - card (kmax f PR \<union> kmin f PR) = card (PR - (kmax f PR \<union> kmin f PR))

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
(* by (intro card_Diff_subset,auto) *)
[PROOF STATE]
proof (state)
this:
card PR - card (kmax f PR \<union> kmin f PR) = card (PR - (kmax f PR \<union> kmin f PR))

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < card (PR - (kmax f PR \<union> kmin f PR))
[PROOF STEP]
have "0 < card (PR-(kmax f PR \<union> kmin f PR))"
[PROOF STATE]
proof (prove)
using this:
0 < card (PR - (kmax f PR \<union> kmin f PR))

goal (1 subgoal):
 1. 0 < card (PR - (kmax f PR \<union> kmin f PR))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 < card (PR - (kmax f PR \<union> kmin f PR))

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
hence "(PR-(kmax f PR \<union> kmin f PR)) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
0 < card (PR - (kmax f PR \<union> kmin f PR))

goal (1 subgoal):
 1. PR - (kmax f PR \<union> kmin f PR) \<noteq> {}
[PROOF STEP]
by (intro notI, simp only: card_0_eq, simp)
[PROOF STATE]
proof (state)
this:
PR - (kmax f PR \<union> kmin f PR) \<noteq> {}

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
PR - (kmax f PR \<union> kmin f PR) \<noteq> {}

goal (1 subgoal):
 1. reduce f PR \<noteq> {}
[PROOF STEP]
by (auto simp add: reduce_def)
[PROOF STATE]
proof (state)
this:
reduce f PR \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduce_shift:
fixes f :: "nat \<Rightarrow> Clocktime"
  shows
  "f ` (PR - (kmax f PR \<union> kmin f PR)) =
            f ` (PR - (kmax (\<lambda> p. f p + c) PR \<union> kmin (\<lambda> p. f p + c) PR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (PR - (kmax f PR \<union> kmin f PR)) = f ` (PR - (kmax (\<lambda>p. f p + c) PR \<union> kmin (\<lambda>p. f p + c) PR))
[PROOF STEP]
apply (unfold kmin_def kmax_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (PR - ((SOME S. S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f j \<le> f i)) \<union> (SOME S. S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i \<le> f j)))) = f ` (PR - ((SOME S. S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f j + c \<le> f i + c)) \<union> (SOME S. S \<subseteq> PR \<and> card S = khl \<and> (\<forall>i\<in>S. \<forall>j\<in>PR - S. f i + c \<le> f j + c))))
[PROOF STEP]
by simp


[STATEMENT]
lemma max_shift:
fixes f :: "nat \<Rightarrow> Clocktime" and S
assumes notEmpFin: "S \<noteq> {}" "finite S"
shows
"Max (f`S) + x = Max ( (\<lambda> p. f p + x) ` S) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (f ` S) + x = (MAX p\<in>S. f p + x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Max (f ` S) + x = (MAX p\<in>S. f p + x)
[PROOF STEP]
from notEmpFin
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> {}
finite S
[PROOF STEP]
have "f`S \<noteq> {}" and "(\<lambda> p. f p + x) ` S \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}
finite S

goal (1 subgoal):
 1. f ` S \<noteq> {} &&& (\<lambda>p. f p + x) ` S \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` S \<noteq> {}
(\<lambda>p. f p + x) ` S \<noteq> {}

goal (1 subgoal):
 1. Max (f ` S) + x = (MAX p\<in>S. f p + x)
[PROOF STEP]
with notEmpFin
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> {}
finite S
f ` S \<noteq> {}
(\<lambda>p. f p + x) ` S \<noteq> {}
[PROOF STEP]
have
    "Max (f`S) \<in> f ` S " "Max ((\<lambda> p. f p + x)`S) \<in> (\<lambda> p. f p + x) ` S "
    "(\<forall>fs \<in> (f`S). fs \<le> Max (f`S))"
    "(\<forall>fs \<in> ((\<lambda> p. f p + x)`S). fs \<le> Max ((\<lambda> p. f p + x)`S))"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}
finite S
f ` S \<noteq> {}
(\<lambda>p. f p + x) ` S \<noteq> {}

goal (1 subgoal):
 1. (Max (f ` S) \<in> f ` S &&& (MAX p\<in>S. f p + x) \<in> (\<lambda>p. f p + x) ` S) &&& \<forall>fs\<in>f ` S. fs \<le> Max (f ` S) &&& \<forall>fs\<in>(\<lambda>p. f p + x) ` S. fs \<le> (MAX p\<in>S. f p + x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (f ` S) \<in> f ` S
(MAX p\<in>S. f p + x) \<in> (\<lambda>p. f p + x) ` S
\<forall>fs\<in>f ` S. fs \<le> Max (f ` S)
\<forall>fs\<in>(\<lambda>p. f p + x) ` S. fs \<le> (MAX p\<in>S. f p + x)

goal (1 subgoal):
 1. Max (f ` S) + x = (MAX p\<in>S. f p + x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Max (f ` S) \<in> f ` S
(MAX p\<in>S. f p + x) \<in> (\<lambda>p. f p + x) ` S
\<forall>fs\<in>f ` S. fs \<le> Max (f ` S)
\<forall>fs\<in>(\<lambda>p. f p + x) ` S. fs \<le> (MAX p\<in>S. f p + x)

goal (1 subgoal):
 1. Max (f ` S) + x = (MAX p\<in>S. f p + x)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Max (f ` S) + x = (MAX p\<in>S. f p + x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_shift:
fixes f :: "nat \<Rightarrow> Clocktime" and S
assumes notEmpFin: "S \<noteq> {}" "finite S"
shows
"Min (f`S) + x = Min ( (\<lambda> p. f p + x) ` S) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (f ` S) + x = (MIN p\<in>S. f p + x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min (f ` S) + x = (MIN p\<in>S. f p + x)
[PROOF STEP]
from notEmpFin
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> {}
finite S
[PROOF STEP]
have "f`S \<noteq> {}" and "(\<lambda> p. f p + x) ` S \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}
finite S

goal (1 subgoal):
 1. f ` S \<noteq> {} &&& (\<lambda>p. f p + x) ` S \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` S \<noteq> {}
(\<lambda>p. f p + x) ` S \<noteq> {}

goal (1 subgoal):
 1. Min (f ` S) + x = (MIN p\<in>S. f p + x)
[PROOF STEP]
with notEmpFin
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> {}
finite S
f ` S \<noteq> {}
(\<lambda>p. f p + x) ` S \<noteq> {}
[PROOF STEP]
have
    "Min (f`S) \<in> f ` S " "Min ((\<lambda> p. f p + x)`S) \<in> (\<lambda> p. f p + x) ` S "
    "(\<forall>fs \<in> (f`S). Min (f`S) <= fs)"
    "(\<forall>fs \<in> ((\<lambda> p. f p + x)`S). Min ((\<lambda> p. f p + x)`S) <= fs)"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}
finite S
f ` S \<noteq> {}
(\<lambda>p. f p + x) ` S \<noteq> {}

goal (1 subgoal):
 1. (Min (f ` S) \<in> f ` S &&& (MIN p\<in>S. f p + x) \<in> (\<lambda>p. f p + x) ` S) &&& \<forall>fs\<in>f ` S. Min (f ` S) \<le> fs &&& \<forall>fs\<in>(\<lambda>p. f p + x) ` S. (MIN p\<in>S. f p + x) \<le> fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (f ` S) \<in> f ` S
(MIN p\<in>S. f p + x) \<in> (\<lambda>p. f p + x) ` S
\<forall>fs\<in>f ` S. Min (f ` S) \<le> fs
\<forall>fs\<in>(\<lambda>p. f p + x) ` S. (MIN p\<in>S. f p + x) \<le> fs

goal (1 subgoal):
 1. Min (f ` S) + x = (MIN p\<in>S. f p + x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Min (f ` S) \<in> f ` S
(MIN p\<in>S. f p + x) \<in> (\<lambda>p. f p + x) ` S
\<forall>fs\<in>f ` S. Min (f ` S) \<le> fs
\<forall>fs\<in>(\<lambda>p. f p + x) ` S. (MIN p\<in>S. f p + x) \<le> fs

goal (1 subgoal):
 1. Min (f ` S) + x = (MIN p\<in>S. f p + x)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Min (f ` S) + x = (MIN p\<in>S. f p + x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem trans_inv:
fixes f :: "nat \<Rightarrow> Clocktime"
  shows
"cfnl p f + x = cfnl p (\<lambda> p. f p + x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
have "cfnl p (\<lambda> p. f p + x) =
      (Max (reduce (\<lambda> p. f p + x) PR) + Min (reduce (\<lambda> p. f p + x) PR)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfnl p (\<lambda>p. f p + x) = (Max (reduce (\<lambda>p. f p + x) PR) + Min (reduce (\<lambda>p. f p + x) PR)) / 2
[PROOF STEP]
by (unfold cfnl_def, simp)
[PROOF STATE]
proof (state)
this:
cfnl p (\<lambda>p. f p + x) = (Max (reduce (\<lambda>p. f p + x) PR) + Min (reduce (\<lambda>p. f p + x) PR)) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cfnl p (\<lambda>p. f p + x) = (Max (reduce (\<lambda>p. f p + x) PR) + Min (reduce (\<lambda>p. f p + x) PR)) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
have "... =
    (Max ((\<lambda> p. f p + x) `
             (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR))) +
     Min ((\<lambda> p. f p + x) `
             (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR)))) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Max (reduce (\<lambda>p. f p + x) PR) + Min (reduce (\<lambda>p. f p + x) PR)) / 2 = ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2
[PROOF STEP]
by (unfold reduce_def, simp)
[PROOF STATE]
proof (state)
this:
(Max (reduce (\<lambda>p. f p + x) PR) + Min (reduce (\<lambda>p. f p + x) PR)) / 2 = ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Max (reduce (\<lambda>p. f p + x) PR) + Min (reduce (\<lambda>p. f p + x) PR)) / 2 = ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
have
    "... =
    (Max (f `
             (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR))) + x +
     Min (f `
             (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR))) + x ) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2
[PROOF STEP]
have "finite (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))

goal (1 subgoal):
 1. ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))

goal (1 subgoal):
 1. ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2
[PROOF STEP]
from reduce_not_empty
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
[PROOF STEP]
have
      "PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}

goal (1 subgoal):
 1. PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR) \<noteq> {}
[PROOF STEP]
by (auto simp add: reduce_def)
[PROOF STATE]
proof (state)
this:
PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR) \<noteq> {}

goal (1 subgoal):
 1. ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))
PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR) \<noteq> {}
[PROOF STEP]
have
      "Max ((\<lambda> p. f p + x) `
       (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR)))
      =
       Max (f `
             (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR))) + x"
       and
      "Min ((\<lambda> p. f p + x) `
       (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR)))
      =
       Min (f `
             (PR - (kmax (\<lambda> p. f p + x) PR \<union> kmin (\<lambda> p. f p + x) PR))) + x"
[PROOF STATE]
proof (prove)
using this:
finite (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))
PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR) \<noteq> {}

goal (1 subgoal):
 1. (MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x &&& (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x
[PROOF STEP]
using max_shift and min_shift
[PROOF STATE]
proof (prove)
using this:
finite (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))
PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR) \<noteq> {}
\<lbrakk>?S \<noteq> {}; finite ?S\<rbrakk> \<Longrightarrow> Max (?f ` ?S) + ?x = (MAX p\<in>?S. ?f p + ?x)
\<lbrakk>?S \<noteq> {}; finite ?S\<rbrakk> \<Longrightarrow> Min (?f ` ?S) + ?x = (MIN p\<in>?S. ?f p + ?x)

goal (1 subgoal):
 1. (MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x &&& (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x
(MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x

goal (1 subgoal):
 1. ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x
(MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) = Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x

goal (1 subgoal):
 1. ((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((MAX p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x) + (MIN p\<in>PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR). f p + x)) / 2 = (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
from reduce_shift
[PROOF STATE]
proof (chain)
picking this:
?f ` (PR - (kmax ?f PR \<union> kmin ?f PR)) = ?f ` (PR - (kmax (\<lambda>p. ?f p + ?c) PR \<union> kmin (\<lambda>p. ?f p + ?c) PR))
[PROOF STEP]
have
    "... =
    (Max (f `
             (PR - (kmax f  PR \<union> kmin f PR))) + x +
     Min (f `
             (PR - (kmax f PR \<union> kmin f PR))) + x ) / 2"
[PROOF STATE]
proof (prove)
using this:
?f ` (PR - (kmax ?f PR \<union> kmin ?f PR)) = ?f ` (PR - (kmax (\<lambda>p. ?f p + ?c) PR \<union> kmin (\<lambda>p. ?f p + ?c) PR))

goal (1 subgoal):
 1. (Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2 = (Max (f ` (PR - (kmax f PR \<union> kmin f PR))) + x + Min (f ` (PR - (kmax f PR \<union> kmin f PR))) + x) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2 = (Max (f ` (PR - (kmax f PR \<union> kmin f PR))) + x + Min (f ` (PR - (kmax f PR \<union> kmin f PR))) + x) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Max (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x + Min (f ` (PR - (kmax (\<lambda>p. f p + x) PR \<union> kmin (\<lambda>p. f p + x) PR))) + x) / 2 = (Max (f ` (PR - (kmax f PR \<union> kmin f PR))) + x + Min (f ` (PR - (kmax f PR \<union> kmin f PR))) + x) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
have "... = ((Max (reduce f PR)+ x) + (Min (reduce f PR) + x)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Max (f ` (PR - (kmax f PR \<union> kmin f PR))) + x + Min (f ` (PR - (kmax f PR \<union> kmin f PR))) + x) / 2 = (Max (reduce f PR) + x + (Min (reduce f PR) + x)) / 2
[PROOF STEP]
by (auto simp add: reduce_def)
[PROOF STATE]
proof (state)
this:
(Max (f ` (PR - (kmax f PR \<union> kmin f PR))) + x + Min (f ` (PR - (kmax f PR \<union> kmin f PR))) + x) / 2 = (Max (reduce f PR) + x + (Min (reduce f PR) + x)) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Max (f ` (PR - (kmax f PR \<union> kmin f PR))) + x + Min (f ` (PR - (kmax f PR \<union> kmin f PR))) + x) / 2 = (Max (reduce f PR) + x + (Min (reduce f PR) + x)) / 2

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
have "... = (Max (reduce f PR) + Min (reduce f PR)) / 2 + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Max (reduce f PR) + x + (Min (reduce f PR) + x)) / 2 = (Max (reduce f PR) + Min (reduce f PR)) / 2 + x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Max (reduce f PR) + x + (Min (reduce f PR) + x)) / 2 = (Max (reduce f PR) + Min (reduce f PR)) / 2 + x

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cfnl p (\<lambda>p. f p + x) = (Max (reduce f PR) + Min (reduce f PR)) / 2 + x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfnl p (\<lambda>p. f p + x) = (Max (reduce f PR) + Min (reduce f PR)) / 2 + x

goal (1 subgoal):
 1. cfnl p f + x = cfnl p (\<lambda>p. f p + x)
[PROOF STEP]
by (auto simp add: cfnl_def)
[PROOF STATE]
proof (state)
this:
cfnl p f + x = cfnl p (\<lambda>p. f p + x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pigeonhole:
assumes
  finitA: "finite A" and
  Bss: "B \<subseteq> A" and Css: "C \<subseteq> A" and
  cardH: "card A + k <= card B + card C"
shows "k <= card (B \<inter> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
from Bss Css
[PROOF STATE]
proof (chain)
picking this:
B \<subseteq> A
C \<subseteq> A
[PROOF STEP]
have "B \<union> C \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
C \<subseteq> A

goal (1 subgoal):
 1. B \<union> C \<subseteq> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B \<union> C \<subseteq> A

goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
with finitA
[PROOF STATE]
proof (chain)
picking this:
finite A
B \<union> C \<subseteq> A
[PROOF STEP]
have "card (B \<union> C) <= card A"
[PROOF STATE]
proof (prove)
using this:
finite A
B \<union> C \<subseteq> A

goal (1 subgoal):
 1. card (B \<union> C) \<le> card A
[PROOF STEP]
by (simp add: card_mono)
[PROOF STATE]
proof (state)
this:
card (B \<union> C) \<le> card A

goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
with cardH
[PROOF STATE]
proof (chain)
picking this:
card A + k \<le> card B + card C
card (B \<union> C) \<le> card A
[PROOF STEP]
have
      h: "k <= card B + card C - card (B \<union> C)"
[PROOF STATE]
proof (prove)
using this:
card A + k \<le> card B + card C
card (B \<union> C) \<le> card A

goal (1 subgoal):
 1. k \<le> card B + card C - card (B \<union> C)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
k \<le> card B + card C - card (B \<union> C)

goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
from finitA Bss Css and finite_subset
[PROOF STATE]
proof (chain)
picking this:
finite A
B \<subseteq> A
C \<subseteq> A
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
[PROOF STEP]
have "finite B \<and> finite C"
[PROOF STATE]
proof (prove)
using this:
finite A
B \<subseteq> A
C \<subseteq> A
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite B \<and> finite C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite B \<and> finite C

goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite B \<and> finite C

goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
using card_Un_Int and h
[PROOF STATE]
proof (prove)
using this:
finite B \<and> finite C
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> card ?A + card ?B = card (?A \<union> ?B) + card (?A \<inter> ?B)
k \<le> card B + card C - card (B \<union> C)

goal (1 subgoal):
 1. k \<le> card (B \<inter> C)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
k \<le> card (B \<inter> C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subsets_int:
assumes
  finitA: "finite A" and
  Bss: "B \<subseteq> A" and Css: "C \<subseteq> A" and
  cardH: "card A < card B + card C"
shows
  "B \<inter> C \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<inter> C \<noteq> {}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B \<inter> C \<noteq> {}
[PROOF STEP]
from finitA Bss Css cardH
[PROOF STATE]
proof (chain)
picking this:
finite A
B \<subseteq> A
C \<subseteq> A
card A < card B + card C
[PROOF STEP]
have "1 <= card (B \<inter> C)"
[PROOF STATE]
proof (prove)
using this:
finite A
B \<subseteq> A
C \<subseteq> A
card A < card B + card C

goal (1 subgoal):
 1. 1 \<le> card (B \<inter> C)
[PROOF STEP]
by (auto intro!:  pigeonhole)
[PROOF STATE]
proof (state)
this:
1 \<le> card (B \<inter> C)

goal (1 subgoal):
 1. B \<inter> C \<noteq> {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> card (B \<inter> C)

goal (1 subgoal):
 1. B \<inter> C \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<inter> C \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exist_reduce:
"\<forall> c \<in> reduce f PR. \<exists> i\<in> PR-(kmax f PR \<union> kmin f PR). f i = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>reduce f PR. \<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> reduce f PR \<Longrightarrow> \<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = c
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> reduce f PR \<Longrightarrow> \<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = c
[PROOF STEP]
assume asm: "c \<in> reduce f PR"
[PROOF STATE]
proof (state)
this:
c \<in> reduce f PR

goal (1 subgoal):
 1. \<And>c. c \<in> reduce f PR \<Longrightarrow> \<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = c
[PROOF STEP]
thus "\<exists> i\<in> PR-(kmax f PR \<union> kmin f PR). f i = c"
[PROOF STATE]
proof (prove)
using this:
c \<in> reduce f PR

goal (1 subgoal):
 1. \<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = c
[PROOF STEP]
by (auto simp add: reduce_def kmax_def kmin_def)
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_reduce:
"finite (reduce f PR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (reduce f PR)
[PROOF STEP]
proof(unfold reduce_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (f ` (PR - (kmax f PR \<union> kmin f PR)))
[PROOF STEP]
show "finite (f ` (PR - (kmax f PR \<union> kmin f PR)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (f ` (PR - (kmax f PR \<union> kmin f PR)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (f ` (PR - (kmax f PR \<union> kmin f PR)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kmax_ge:
  "\<forall> i\<in> (kmax f PR). \<forall> r \<in> (reduce f PR). r <= f i "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>kmax f PR. \<forall>r\<in>reduce f PR. r \<le> f i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> kmax f PR \<Longrightarrow> \<forall>r\<in>reduce f PR. r \<le> f i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> kmax f PR \<Longrightarrow> \<forall>r\<in>reduce f PR. r \<le> f i
[PROOF STEP]
assume asm: "i \<in> kmax f PR"
[PROOF STATE]
proof (state)
this:
i \<in> kmax f PR

goal (1 subgoal):
 1. \<And>i. i \<in> kmax f PR \<Longrightarrow> \<forall>r\<in>reduce f PR. r \<le> f i
[PROOF STEP]
show "\<forall>r\<in>reduce f PR. r \<le> f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>reduce f PR. r \<le> f i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> reduce f PR \<Longrightarrow> r \<le> f i
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> reduce f PR \<Longrightarrow> r \<le> f i
[PROOF STEP]
assume asm2: "r \<in> reduce f PR"
[PROOF STATE]
proof (state)
this:
r \<in> reduce f PR

goal (1 subgoal):
 1. \<And>r. r \<in> reduce f PR \<Longrightarrow> r \<le> f i
[PROOF STEP]
show "r \<le> f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> f i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<le> f i
[PROOF STEP]
from asm2 and exist_reduce
[PROOF STATE]
proof (chain)
picking this:
r \<in> reduce f PR
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c
[PROOF STEP]
have
        "\<exists> j \<in> PR-(kmax f PR \<union> kmin f PR). f j = r"
[PROOF STATE]
proof (prove)
using this:
r \<in> reduce f PR
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c

goal (1 subgoal):
 1. \<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r

goal (1 subgoal):
 1. r \<le> f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r
[PROOF STEP]
obtain j
      where fjr:"j \<in> PR-(kmax f PR \<union> kmin f PR) \<and> f j = r"
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r

goal (1 subgoal):
 1. (\<And>j. j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r

goal (1 subgoal):
 1. r \<le> f i
[PROOF STEP]
hence "j \<in> (PR - kmax f PR)"
[PROOF STATE]
proof (prove)
using this:
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r

goal (1 subgoal):
 1. j \<in> PR - kmax f PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<in> PR - kmax f PR

goal (1 subgoal):
 1. r \<le> f i
[PROOF STEP]
from this fjr asm
[PROOF STATE]
proof (chain)
picking this:
j \<in> PR - kmax f PR
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r
i \<in> kmax f PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<in> PR - kmax f PR
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r
i \<in> kmax f PR

goal (1 subgoal):
 1. r \<le> f i
[PROOF STEP]
using kmax_prop
[PROOF STATE]
proof (prove)
using this:
j \<in> PR - kmax f PR
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r
i \<in> kmax f PR
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)

goal (1 subgoal):
 1. r \<le> f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<le> f i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<le> f i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>reduce f PR. r \<le> f i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kmin_le:
  "\<forall> i\<in> (kmin f PR). \<forall> r \<in> (reduce f PR). f i <= r "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>kmin f PR. \<forall>r\<in>reduce f PR. f i \<le> r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> kmin f PR \<Longrightarrow> \<forall>r\<in>reduce f PR. f i \<le> r
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> kmin f PR \<Longrightarrow> \<forall>r\<in>reduce f PR. f i \<le> r
[PROOF STEP]
assume asm: "i \<in> kmin f PR"
[PROOF STATE]
proof (state)
this:
i \<in> kmin f PR

goal (1 subgoal):
 1. \<And>i. i \<in> kmin f PR \<Longrightarrow> \<forall>r\<in>reduce f PR. f i \<le> r
[PROOF STEP]
show "\<forall>r\<in>reduce f PR. f i \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>reduce f PR. f i \<le> r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> reduce f PR \<Longrightarrow> f i \<le> r
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> reduce f PR \<Longrightarrow> f i \<le> r
[PROOF STEP]
assume asm2: "r \<in> reduce f PR"
[PROOF STATE]
proof (state)
this:
r \<in> reduce f PR

goal (1 subgoal):
 1. \<And>r. r \<in> reduce f PR \<Longrightarrow> f i \<le> r
[PROOF STEP]
show "f i <= r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i \<le> r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f i \<le> r
[PROOF STEP]
from asm2 and exist_reduce
[PROOF STATE]
proof (chain)
picking this:
r \<in> reduce f PR
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c
[PROOF STEP]
have
        "\<exists> j\<in> PR-(kmax f PR \<union> kmin f PR). f j = r"
[PROOF STATE]
proof (prove)
using this:
r \<in> reduce f PR
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c

goal (1 subgoal):
 1. \<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r

goal (1 subgoal):
 1. f i \<le> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r
[PROOF STEP]
obtain j
      where fjr:"j \<in> PR-(kmax f PR \<union> kmin f PR) \<and> f j = r"
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<in>PR - (kmax f PR \<union> kmin f PR). f j = r

goal (1 subgoal):
 1. (\<And>j. j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r

goal (1 subgoal):
 1. f i \<le> r
[PROOF STEP]
hence "j \<in> (PR - kmin f PR)"
[PROOF STATE]
proof (prove)
using this:
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r

goal (1 subgoal):
 1. j \<in> PR - kmin f PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<in> PR - kmin f PR

goal (1 subgoal):
 1. f i \<le> r
[PROOF STEP]
from this fjr asm
[PROOF STATE]
proof (chain)
picking this:
j \<in> PR - kmin f PR
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r
i \<in> kmin f PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<in> PR - kmin f PR
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r
i \<in> kmin f PR

goal (1 subgoal):
 1. f i \<le> r
[PROOF STEP]
using kmin_prop
[PROOF STATE]
proof (prove)
using this:
j \<in> PR - kmin f PR
j \<in> PR - (kmax f PR \<union> kmin f PR) \<and> f j = r
i \<in> kmin f PR
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)

goal (1 subgoal):
 1. f i \<le> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i \<le> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f i \<le> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>reduce f PR. f i \<le> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_distrib_div:
  "0 < (c::real)  \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
assume ch: "0<c"
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
fix d :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
assume dh: "0<=d"
[PROOF STATE]
proof (state)
this:
0 \<le> d

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
have "a * d - b * d = (a - b) * d "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * d - b * d = (a - b) * d
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
a * d - b * d = (a - b) * d

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
hence "\<bar>a * d - b * d\<bar> = \<bar>(a - b) * d\<bar>"
[PROOF STATE]
proof (prove)
using this:
a * d - b * d = (a - b) * d

goal (1 subgoal):
 1. \<bar>a * d - b * d\<bar> = \<bar>(a - b) * d\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>a * d - b * d\<bar> = \<bar>(a - b) * d\<bar>

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>a * d - b * d\<bar> = \<bar>(a - b) * d\<bar>

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
with dh
[PROOF STATE]
proof (chain)
picking this:
0 \<le> d
\<bar>a * d - b * d\<bar> = \<bar>(a - b) * d\<bar>
[PROOF STEP]
have
      "... = \<bar>a - b\<bar> * d"
[PROOF STATE]
proof (prove)
using this:
0 \<le> d
\<bar>a * d - b * d\<bar> = \<bar>(a - b) * d\<bar>

goal (1 subgoal):
 1. \<bar>(a - b) * d\<bar> = \<bar>a - b\<bar> * d
[PROOF STEP]
by (simp add: abs_mult)
[PROOF STATE]
proof (state)
this:
\<bar>(a - b) * d\<bar> = \<bar>a - b\<bar> * d

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>a * d - b * d\<bar> = \<bar>a - b\<bar> * d
[PROOF STEP]
have "\<bar>a * d - b * d\<bar> = \<bar>a - b\<bar> * d"
[PROOF STATE]
proof (prove)
using this:
\<bar>a * d - b * d\<bar> = \<bar>a - b\<bar> * d

goal (1 subgoal):
 1. \<bar>a * d - b * d\<bar> = \<bar>a - b\<bar> * d
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>a * d - b * d\<bar> = \<bar>a - b\<bar> * d

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
(* This sublemma is solved by ICS, file: abs_distrib_mult.ics *)
    (* It is not solved nor
       by (auto simp add: distrib_right diff_minus)(arith)
        in Isabelle  *)
[PROOF STATE]
proof (state)
this:
\<bar>a * d - b * d\<bar> = \<bar>a - b\<bar> * d

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 \<le> ?d2 \<Longrightarrow> \<bar>a * ?d2 - b * ?d2\<bar> = \<bar>a - b\<bar> * ?d2

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
with ch and divide_inverse
[PROOF STATE]
proof (chain)
picking this:
0 < c
?a / ?b = ?a * inverse ?b
0 \<le> ?d2 \<Longrightarrow> \<bar>a * ?d2 - b * ?d2\<bar> = \<bar>a - b\<bar> * ?d2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < c
?a / ?b = ?a * inverse ?b
0 \<le> ?d2 \<Longrightarrow> \<bar>a * ?d2 - b * ?d2\<bar> = \<bar>a - b\<bar> * ?d2

goal (1 subgoal):
 1. \<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c
[PROOF STEP]
by (auto simp add: divide_inverse)
[PROOF STATE]
proof (state)
this:
\<bar>a / c - b / c\<bar> = \<bar>a - b\<bar> / c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uboundmax:
assumes
  hC: "C \<subseteq> PR" and
  hCk: "np <= card C + khl"
shows
  "\<exists> i\<in>C. Max (reduce f PR) <= f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
from reduce_not_empty and finite_reduce
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
[PROOF STEP]
have maxrinr: "Max (reduce f PR) \<in> reduce f PR"
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)

goal (1 subgoal):
 1. Max (reduce f PR) \<in> reduce f PR
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Max (reduce f PR) \<in> reduce f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
with exist_reduce
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c
Max (reduce f PR) \<in> reduce f PR
[PROOF STEP]
have "\<exists> i\<in> PR-(kmax f PR \<union> kmin f PR). f i = Max (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c
Max (reduce f PR) \<in> reduce f PR

goal (1 subgoal):
 1. \<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Max (reduce f PR)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Max (reduce f PR)

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Max (reduce f PR)
[PROOF STEP]
obtain pmax where
    pmax_in_reduc: "pmax \<in> PR-(kmax f PR \<union> kmin f PR)" and
    fpmax_ismax: "f pmax = Max (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Max (reduce f PR)

goal (1 subgoal):
 1. (\<And>pmax. \<lbrakk>pmax \<in> PR - (kmax f PR \<union> kmin f PR); f pmax = Max (reduce f PR)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
pmax \<in> PR - (kmax f PR \<union> kmin f PR)
f pmax = Max (reduce f PR)

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
hence "C \<inter> insert pmax (kmax f PR)  \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
pmax \<in> PR - (kmax f PR \<union> kmin f PR)
f pmax = Max (reduce f PR)

goal (1 subgoal):
 1. C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>pmax \<in> PR - (kmax f PR \<union> kmin f PR); f pmax = Max (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
from kmax_prop and pmax_in_reduc
      and finite_kmax and hCk
[PROOF STATE]
proof (chain)
picking this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
pmax \<in> PR - (kmax f PR \<union> kmin f PR)
finite (kmax ?f PR)
np \<le> card C + khl
[PROOF STEP]
have
      "card PR < card C + card (insert pmax (kmax f PR))"
[PROOF STATE]
proof (prove)
using this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
pmax \<in> PR - (kmax f PR \<union> kmin f PR)
finite (kmax ?f PR)
np \<le> card C + khl

goal (1 subgoal):
 1. card PR < card C + card (insert pmax (kmax f PR))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card PR < card C + card (insert pmax (kmax f PR))

goal (1 subgoal):
 1. \<lbrakk>pmax \<in> PR - (kmax f PR \<union> kmin f PR); f pmax = Max (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card PR < card C + card (insert pmax (kmax f PR))

goal (1 subgoal):
 1. \<lbrakk>pmax \<in> PR - (kmax f PR \<union> kmin f PR); f pmax = Max (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
from pmax_in_reduc and kmax_prop
[PROOF STATE]
proof (chain)
picking this:
pmax \<in> PR - (kmax f PR \<union> kmin f PR)
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
[PROOF STEP]
have "insert pmax (kmax f PR) \<subseteq> PR"
[PROOF STATE]
proof (prove)
using this:
pmax \<in> PR - (kmax f PR \<union> kmin f PR)
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)

goal (1 subgoal):
 1. insert pmax (kmax f PR) \<subseteq> PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
insert pmax (kmax f PR) \<subseteq> PR

goal (1 subgoal):
 1. \<lbrakk>pmax \<in> PR - (kmax f PR \<union> kmin f PR); f pmax = Max (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert pmax (kmax f PR) \<subseteq> PR

goal (1 subgoal):
 1. \<lbrakk>pmax \<in> PR - (kmax f PR \<union> kmin f PR); f pmax = Max (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
note hC
[PROOF STATE]
proof (state)
this:
C \<subseteq> PR

goal (1 subgoal):
 1. \<lbrakk>pmax \<in> PR - (kmax f PR \<union> kmin f PR); f pmax = Max (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card PR < card C + card (insert pmax (kmax f PR))
insert pmax (kmax f PR) \<subseteq> PR
C \<subseteq> PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card PR < card C + card (insert pmax (kmax f PR))
insert pmax (kmax f PR) \<subseteq> PR
C \<subseteq> PR

goal (1 subgoal):
 1. C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
using subsets_int[of PR C "insert pmax (kmax f PR)"]
[PROOF STATE]
proof (prove)
using this:
card PR < card C + card (insert pmax (kmax f PR))
insert pmax (kmax f PR) \<subseteq> PR
C \<subseteq> PR
\<lbrakk>finite PR; C \<subseteq> PR; insert pmax (kmax f PR) \<subseteq> PR; card PR < card C + card (insert pmax (kmax f PR))\<rbrakk> \<Longrightarrow> C \<inter> insert pmax (kmax f PR) \<noteq> {}

goal (1 subgoal):
 1. C \<inter> insert pmax (kmax f PR) \<noteq> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C \<inter> insert pmax (kmax f PR) \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C \<inter> insert pmax (kmax f PR) \<noteq> {}

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
hence res: "\<exists> i\<in>C. i=pmax \<or> i \<in> kmax f PR"
[PROOF STATE]
proof (prove)
using this:
C \<inter> insert pmax (kmax f PR) \<noteq> {}

goal (1 subgoal):
 1. \<exists>i\<in>C. i = pmax \<or> i \<in> kmax f PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. i = pmax \<or> i \<in> kmax f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<in>C. i = pmax \<or> i \<in> kmax f PR
[PROOF STEP]
obtain i where
    iinC: "i\<in>C" and altern: "i=pmax \<or> i \<in> kmax f PR"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>C. i = pmax \<or> i \<in> kmax f PR

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i \<in> C
i = pmax \<or> i \<in> kmax f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> C
i = pmax \<or> i \<in> kmax f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
proof(cases "i=pmax")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i = pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
 2. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i \<noteq> pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = pmax

goal (2 subgoals):
 1. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i = pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
 2. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i \<noteq> pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
with iinC fpmax_ismax
[PROOF STATE]
proof (chain)
picking this:
i \<in> C
f pmax = Max (reduce f PR)
i = pmax
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> C
f pmax = Max (reduce f PR)
i = pmax

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. Max (reduce f PR) \<le> f i

goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i \<noteq> pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i \<noteq> pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> pmax

goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i \<noteq> pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
with altern maxrinr fpmax_ismax kmax_ge
[PROOF STATE]
proof (chain)
picking this:
i = pmax \<or> i \<in> kmax f PR
Max (reduce f PR) \<in> reduce f PR
f pmax = Max (reduce f PR)
\<forall>i\<in>kmax ?f PR. \<forall>r\<in>reduce ?f PR. r \<le> ?f i
i \<noteq> pmax
[PROOF STEP]
have "f pmax <= f i"
[PROOF STATE]
proof (prove)
using this:
i = pmax \<or> i \<in> kmax f PR
Max (reduce f PR) \<in> reduce f PR
f pmax = Max (reduce f PR)
\<forall>i\<in>kmax ?f PR. \<forall>r\<in>reduce ?f PR. r \<le> ?f i
i \<noteq> pmax

goal (1 subgoal):
 1. f pmax \<le> f i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f pmax \<le> f i

goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmax \<or> i \<in> kmax f PR; i \<noteq> pmax\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
with iinC fpmax_ismax
[PROOF STATE]
proof (chain)
picking this:
i \<in> C
f pmax = Max (reduce f PR)
f pmax \<le> f i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> C
f pmax = Max (reduce f PR)
f pmax \<le> f i

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. Max (reduce f PR) \<le> f i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. Max (reduce f PR) \<le> f i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lboundmin:
assumes
  hC: "C \<subseteq> PR" and
  hCk: "np <= card C + khl"
shows
  "\<exists> i\<in>C. f i <= Min (reduce f PR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
from reduce_not_empty and finite_reduce
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
[PROOF STEP]
have minrinr: "Min (reduce f PR) \<in> reduce f PR"
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)

goal (1 subgoal):
 1. Min (reduce f PR) \<in> reduce f PR
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<in> reduce f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
with exist_reduce
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c
Min (reduce f PR) \<in> reduce f PR
[PROOF STEP]
have "\<exists> i\<in> PR-(kmax f PR \<union> kmin f PR). f i = Min (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>reduce ?f PR. \<exists>i\<in>PR - (kmax ?f PR \<union> kmin ?f PR). ?f i = c
Min (reduce f PR) \<in> reduce f PR

goal (1 subgoal):
 1. \<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Min (reduce f PR)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Min (reduce f PR)

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Min (reduce f PR)
[PROOF STEP]
obtain pmin where
    pmin_in_reduc: "pmin \<in> PR-(kmax f PR \<union> kmin f PR)" and
    fpmin_ismin: "f pmin = Min (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>PR - (kmax f PR \<union> kmin f PR). f i = Min (reduce f PR)

goal (1 subgoal):
 1. (\<And>pmin. \<lbrakk>pmin \<in> PR - (kmax f PR \<union> kmin f PR); f pmin = Min (reduce f PR)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
pmin \<in> PR - (kmax f PR \<union> kmin f PR)
f pmin = Min (reduce f PR)

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
hence "C \<inter> insert pmin (kmin f PR)  \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
pmin \<in> PR - (kmax f PR \<union> kmin f PR)
f pmin = Min (reduce f PR)

goal (1 subgoal):
 1. C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>pmin \<in> PR - (kmax f PR \<union> kmin f PR); f pmin = Min (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
from kmin_prop and pmin_in_reduc
      and finite_kmin and hCk
[PROOF STATE]
proof (chain)
picking this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
pmin \<in> PR - (kmax f PR \<union> kmin f PR)
finite (kmin ?f PR)
np \<le> card C + khl
[PROOF STEP]
have
      "card PR < card C + card (insert pmin (kmin f PR))"
[PROOF STATE]
proof (prove)
using this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
pmin \<in> PR - (kmax f PR \<union> kmin f PR)
finite (kmin ?f PR)
np \<le> card C + khl

goal (1 subgoal):
 1. card PR < card C + card (insert pmin (kmin f PR))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card PR < card C + card (insert pmin (kmin f PR))

goal (1 subgoal):
 1. \<lbrakk>pmin \<in> PR - (kmax f PR \<union> kmin f PR); f pmin = Min (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card PR < card C + card (insert pmin (kmin f PR))

goal (1 subgoal):
 1. \<lbrakk>pmin \<in> PR - (kmax f PR \<union> kmin f PR); f pmin = Min (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
from pmin_in_reduc and kmin_prop
[PROOF STATE]
proof (chain)
picking this:
pmin \<in> PR - (kmax f PR \<union> kmin f PR)
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
[PROOF STEP]
have "insert pmin (kmin f PR) \<subseteq> PR"
[PROOF STATE]
proof (prove)
using this:
pmin \<in> PR - (kmax f PR \<union> kmin f PR)
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)

goal (1 subgoal):
 1. insert pmin (kmin f PR) \<subseteq> PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
insert pmin (kmin f PR) \<subseteq> PR

goal (1 subgoal):
 1. \<lbrakk>pmin \<in> PR - (kmax f PR \<union> kmin f PR); f pmin = Min (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert pmin (kmin f PR) \<subseteq> PR

goal (1 subgoal):
 1. \<lbrakk>pmin \<in> PR - (kmax f PR \<union> kmin f PR); f pmin = Min (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
note hC
[PROOF STATE]
proof (state)
this:
C \<subseteq> PR

goal (1 subgoal):
 1. \<lbrakk>pmin \<in> PR - (kmax f PR \<union> kmin f PR); f pmin = Min (reduce f PR)\<rbrakk> \<Longrightarrow> C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card PR < card C + card (insert pmin (kmin f PR))
insert pmin (kmin f PR) \<subseteq> PR
C \<subseteq> PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card PR < card C + card (insert pmin (kmin f PR))
insert pmin (kmin f PR) \<subseteq> PR
C \<subseteq> PR

goal (1 subgoal):
 1. C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
using subsets_int[of PR C "insert pmin (kmin f PR)"]
[PROOF STATE]
proof (prove)
using this:
card PR < card C + card (insert pmin (kmin f PR))
insert pmin (kmin f PR) \<subseteq> PR
C \<subseteq> PR
\<lbrakk>finite PR; C \<subseteq> PR; insert pmin (kmin f PR) \<subseteq> PR; card PR < card C + card (insert pmin (kmin f PR))\<rbrakk> \<Longrightarrow> C \<inter> insert pmin (kmin f PR) \<noteq> {}

goal (1 subgoal):
 1. C \<inter> insert pmin (kmin f PR) \<noteq> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C \<inter> insert pmin (kmin f PR) \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C \<inter> insert pmin (kmin f PR) \<noteq> {}

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
hence res: "\<exists> i\<in>C. i=pmin \<or> i \<in> kmin f PR"
[PROOF STATE]
proof (prove)
using this:
C \<inter> insert pmin (kmin f PR) \<noteq> {}

goal (1 subgoal):
 1. \<exists>i\<in>C. i = pmin \<or> i \<in> kmin f PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. i = pmin \<or> i \<in> kmin f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<in>C. i = pmin \<or> i \<in> kmin f PR
[PROOF STEP]
obtain i where
    iinC: "i\<in>C" and altern: "i=pmin \<or> i \<in> kmin f PR"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>C. i = pmin \<or> i \<in> kmin f PR

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i \<in> C
i = pmin \<or> i \<in> kmin f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> C
i = pmin \<or> i \<in> kmin f PR

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
proof(cases "i=pmin")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i = pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
 2. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i \<noteq> pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = pmin

goal (2 subgoals):
 1. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i = pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
 2. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i \<noteq> pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
with iinC fpmin_ismin
[PROOF STATE]
proof (chain)
picking this:
i \<in> C
f pmin = Min (reduce f PR)
i = pmin
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> C
f pmin = Min (reduce f PR)
i = pmin

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. f i \<le> Min (reduce f PR)

goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i \<noteq> pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i \<noteq> pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> pmin

goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i \<noteq> pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
with altern minrinr fpmin_ismin kmin_le
[PROOF STATE]
proof (chain)
picking this:
i = pmin \<or> i \<in> kmin f PR
Min (reduce f PR) \<in> reduce f PR
f pmin = Min (reduce f PR)
\<forall>i\<in>kmin ?f PR. \<forall>r\<in>reduce ?f PR. ?f i \<le> r
i \<noteq> pmin
[PROOF STEP]
have "f i <= f pmin"
[PROOF STATE]
proof (prove)
using this:
i = pmin \<or> i \<in> kmin f PR
Min (reduce f PR) \<in> reduce f PR
f pmin = Min (reduce f PR)
\<forall>i\<in>kmin ?f PR. \<forall>r\<in>reduce ?f PR. ?f i \<le> r
i \<noteq> pmin

goal (1 subgoal):
 1. f i \<le> f pmin
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f i \<le> f pmin

goal (1 subgoal):
 1. \<lbrakk>i \<in> C; i = pmin \<or> i \<in> kmin f PR; i \<noteq> pmin\<rbrakk> \<Longrightarrow> \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
with iinC fpmin_ismin
[PROOF STATE]
proof (chain)
picking this:
i \<in> C
f pmin = Min (reduce f PR)
f i \<le> f pmin
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> C
f pmin = Min (reduce f PR)
f i \<le> f pmin

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. f i \<le> Min (reduce f PR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. f i \<le> Min (reduce f PR)

goal:
No subgoals!
[PROOF STEP]
qed