[STATEMENT]
lemma nn_contains_Inf:
  fixes S :: "nat set"
  assumes nn: "S \<noteq> {}"
  shows "Inf S \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> S \<in> S
[PROOF STEP]
using assms Inf_nat_def LeastI
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}
\<Sqinter> ?X = (LEAST n. n \<in> ?X)
?P ?k \<Longrightarrow> ?P (LEAST x. ?P x)

goal (1 subgoal):
 1. \<Sqinter> S \<in> S
[PROOF STEP]
by force


[STATEMENT]
lemma steps_length: "length qs = length as \<Longrightarrow> length (steps s qs as) = length s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length qs = length as \<Longrightarrow> length (Partial_Cost_Model.steps s qs as) = length s
[PROOF STEP]
apply(induct qs as arbitrary: s rule: list_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. length (Partial_Cost_Model.steps s [] []) = length s
 2. \<And>x xs y ys s. \<lbrakk>length xs = length ys; \<And>s. length (Partial_Cost_Model.steps s xs ys) = length s\<rbrakk> \<Longrightarrow> length (Partial_Cost_Model.steps s (x # xs) (y # ys)) = length s
[PROOF STEP]
by simp_all


[STATEMENT]
lemma OPT_noStupid:
  fixes Strat
  assumes [simp]: "length Strat = length qs"
  assumes opt: "T\<^sub>p init qs Strat = T\<^sub>p_opt init qs"
  assumes init_nempty: "init\<noteq>[]"
  shows "\<And>x l. x < length Strat \<Longrightarrow>
        l < length (snd (Strat ! x)) \<Longrightarrow>
       Suc ((snd (Strat ! x))!l) < length init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x))\<rbrakk> \<Longrightarrow> Suc (snd (Strat ! x) ! l) < length init
[PROOF STEP]
proof (rule ccontr, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (1 x l)
[PROOF STATE]
proof (state)
this:
x < length Strat
l < length (snd (Strat ! x))
\<not> Suc (snd (Strat ! x) ! l) < length init

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
(* construct a Stratgy that leaves out that paid exchange *)
[PROOF STATE]
proof (state)
this:
x < length Strat
l < length (snd (Strat ! x))
\<not> Suc (snd (Strat ! x) ! l) < length init

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?sws' = "take l (snd (Strat!x)) @ drop (Suc l) (snd (Strat!x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?Strat' = "take x Strat @ (fst (Strat!x),?sws') # drop (Suc x) Strat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from 1(1)
[PROOF STATE]
proof (chain)
picking this:
x < length Strat
[PROOF STEP]
have valid: "length ?Strat' = length qs"
[PROOF STATE]
proof (prove)
using this:
x < length Strat

goal (1 subgoal):
 1. length (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = length qs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = length qs

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from valid
[PROOF STATE]
proof (chain)
picking this:
length (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = length qs
[PROOF STEP]
have isin: "T\<^sub>p init qs ?Strat' \<in> {T\<^sub>p init qs as |as. length as = length qs}"
[PROOF STATE]
proof (prove)
using this:
length (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = length qs

goal (1 subgoal):
 1. T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) \<in> {T\<^sub>p init qs as |as. length as = length qs}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) \<in> {T\<^sub>p init qs as |as. length as = length qs}

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from 1(1,2)
[PROOF STATE]
proof (chain)
picking this:
x < length Strat
l < length (snd (Strat ! x))
[PROOF STEP]
have lsws': "length (snd (Strat!x)) = length ?sws' + 1"
[PROOF STATE]
proof (prove)
using this:
x < length Strat
l < length (snd (Strat ! x))

goal (1 subgoal):
 1. length (snd (Strat ! x)) = length (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) + 1
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
length (snd (Strat ! x)) = length (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have a: "(take x ?Strat') = (take x Strat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = take x Strat
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
x < length Strat

goal (1 subgoal):
 1. take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = take x Strat
[PROOF STEP]
by(auto simp add: min_def take_Suc_conv_app_nth)
[PROOF STATE]
proof (state)
this:
take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = take x Strat

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have b: "(drop (Suc x) Strat) = (drop (Suc x) ?Strat')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (Suc x) Strat = drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
x < length Strat

goal (1 subgoal):
 1. drop (Suc x) Strat = drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)
[PROOF STEP]
by(auto simp add: min_def take_Suc_conv_app_nth)
[PROOF STATE]
proof (state)
this:
drop (Suc x) Strat = drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have aa: "(take l (snd (Strat!x))) = (take l (snd (?Strat'!x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take l (snd (Strat ! x)) = take l (snd ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x))
[PROOF STEP]
using 1(1,2)
[PROOF STATE]
proof (prove)
using this:
x < length Strat
l < length (snd (Strat ! x))

goal (1 subgoal):
 1. take l (snd (Strat ! x)) = take l (snd ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x))
[PROOF STEP]
by(auto simp add: min_def take_Suc_conv_app_nth nth_append)
[PROOF STATE]
proof (state)
this:
take l (snd (Strat ! x)) = take l (snd ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have bb: "(drop (Suc l) (snd (Strat!x))) = (drop l (snd (?Strat'!x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (Suc l) (snd (Strat ! x)) = drop l (snd ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x))
[PROOF STEP]
using 1(1,2)
[PROOF STATE]
proof (prove)
using this:
x < length Strat
l < length (snd (Strat ! x))

goal (1 subgoal):
 1. drop (Suc l) (snd (Strat ! x)) = drop l (snd ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x))
[PROOF STEP]
by(auto simp add: min_def take_Suc_conv_app_nth nth_append )
[PROOF STATE]
proof (state)
this:
drop (Suc l) (snd (Strat ! x)) = drop l (snd ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(swaps (snd (Strat ! x)) (steps init (take x qs) (take x Strat)))
      = (swaps (take l (snd (Strat ! x)) @ (snd (Strat ! x))!l # drop (Suc l) (snd (Strat ! x))) (steps init (take x qs) (take x Strat)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ snd (Strat ! x) ! l # drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))
[PROOF STEP]
unfolding id_take_nth_drop[OF 1(2), symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ snd (Strat ! x) ! l # drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ snd (Strat ! x) ! l # drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "...
      = (swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (steps init (take x qs) (take x Strat)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaps (take l (snd (Strat ! x)) @ snd (Strat ! x) ! l # drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))
[PROOF STEP]
using 1(3)
[PROOF STATE]
proof (prove)
using this:
\<not> Suc (snd (Strat ! x) ! l) < length init

goal (1 subgoal):
 1. swaps (take l (snd (Strat ! x)) @ snd (Strat ! x) ! l # drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))
[PROOF STEP]
by(simp add: swap_def steps_length)
[PROOF STATE]
proof (state)
this:
swaps (take l (snd (Strat ! x)) @ snd (Strat ! x) ! l # drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))
[PROOF STEP]
have noeffect: "(swaps (snd (Strat ! x)) (steps init (take x qs) (take x Strat)))
      = (swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (steps init (take x qs) (take x Strat)))"
[PROOF STATE]
proof (prove)
using this:
swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))

goal (1 subgoal):
 1. swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have c: "t\<^sub>p (steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x) =
        t\<^sub>p (steps init (take x qs) (take x ?Strat')) (qs ! x) (?Strat' ! x) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x) = t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1
[PROOF STEP]
unfolding a t\<^sub>p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let (mf, sws) = Strat ! x in index (swaps sws (Partial_Cost_Model.steps init (take x qs) (take x Strat))) (qs ! x) + length sws) = (let (mf, sws) = (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x in index (swaps sws (Partial_Cost_Model.steps init (take x qs) (take x Strat))) (qs ! x) + length sws) + 1
[PROOF STEP]
using 1(1,2)
[PROOF STATE]
proof (prove)
using this:
x < length Strat
l < length (snd (Strat ! x))

goal (1 subgoal):
 1. (let (mf, sws) = Strat ! x in index (swaps sws (Partial_Cost_Model.steps init (take x qs) (take x Strat))) (qs ! x) + length sws) = (let (mf, sws) = (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x in index (swaps sws (Partial_Cost_Model.steps init (take x qs) (take x Strat))) (qs ! x) + length sws) + 1
[PROOF STEP]
apply(simp add: min_def split_def nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < length qs; l < length (snd (Strat ! x))\<rbrakk> \<Longrightarrow> index (swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat))) (qs ! x) + length (snd (Strat ! x)) = Suc (index (swaps (take l (snd (Strat ! x))) (swaps (drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat)))) (qs ! x) + length (snd (Strat ! x)) - Suc 0)
[PROOF STEP]
unfolding noeffect
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < length qs; l < length (snd (Strat ! x))\<rbrakk> \<Longrightarrow> index (swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))) (qs ! x) + length (snd (Strat ! x)) = Suc (index (swaps (take l (snd (Strat ! x))) (swaps (drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat)))) (qs ! x) + length (snd (Strat ! x)) - Suc 0)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x) = t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat)
        = T\<^sub>p init (take x qs) (take x ?Strat') +
              t\<^sub>p (steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x)
[PROOF STEP]
using 1(1) a
[PROOF STATE]
proof (prove)
using this:
x < length Strat
take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = take x Strat

goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x)
[PROOF STEP]
by(simp add: take_Suc_conv_app_nth T_append)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = T\<^sub>p init (take x qs) (take x ?Strat')  +
              t\<^sub>p (steps init (take x qs) (take x ?Strat')) (qs ! x) (?Strat' ! x) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1
[PROOF STEP]
unfolding c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + (t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x Strat)) (qs ! x) (Strat ! x) = T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = T\<^sub>p init (take (Suc x) qs) (take (Suc x) ?Strat')  + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1 = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
using 1(1) a
[PROOF STATE]
proof (prove)
using this:
x < length Strat
take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) = take x Strat

goal (1 subgoal):
 1. T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1 = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
by(simp add: min_def take_Suc_conv_app_nth T_append nth_append)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + t\<^sub>p (Partial_Cost_Model.steps init (take x qs) (take x (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (qs ! x) ((take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) ! x) + 1 = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
have bef: "T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat)
      = T\<^sub>p init (take (Suc x) qs) (take (Suc x) ?Strat') + 1"
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1

goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?interstate = "(steps init (take (Suc x) qs) (take (Suc x) Strat))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?interstate' = "(steps init (take (Suc x) qs) (take (Suc x) ?Strat'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have state: "?interstate' = ?interstate"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) = Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
x < length Strat

goal (1 subgoal):
 1. Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) = Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)
[PROOF STEP]
apply(simp add: take_Suc_conv_app_nth min_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < length qs \<Longrightarrow> Partial_Cost_Model.steps init (take x qs @ [qs ! x]) (take x Strat @ [(fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x)))]) = Partial_Cost_Model.steps init (take x qs @ [qs ! x]) (take x Strat @ [Strat ! x])
[PROOF STEP]
apply(simp add: steps_append step_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < length qs \<Longrightarrow> mtf2 (fst (Strat ! x)) (qs ! x) (swaps (take l (snd (Strat ! x))) (swaps (drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat)))) = mtf2 (fst (Strat ! x)) (qs ! x) (swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)))
[PROOF STEP]
using noeffect
[PROOF STATE]
proof (prove)
using this:
swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)) = swaps (take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat))

goal (1 subgoal):
 1. x < length qs \<Longrightarrow> mtf2 (fst (Strat ! x)) (qs ! x) (swaps (take l (snd (Strat ! x))) (swaps (drop (Suc l) (snd (Strat ! x))) (Partial_Cost_Model.steps init (take x qs) (take x Strat)))) = mtf2 (fst (Strat ! x)) (qs ! x) (swaps (snd (Strat ! x)) (Partial_Cost_Model.steps init (take x qs) (take x Strat)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) = Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "T\<^sub>p init qs Strat
      = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs)  (take (Suc x) Strat @ drop (Suc x) Strat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init qs Strat = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) Strat @ drop (Suc x) Strat)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) Strat @ drop (Suc x) Strat)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) Strat @ drop (Suc x) Strat)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat)
            + T\<^sub>p ?interstate (drop (Suc x) qs) (drop (Suc x) Strat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) Strat @ drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat)
[PROOF STEP]
apply(subst T_append2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (take (Suc x) qs) = length (take (Suc x) Strat)
 2. T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat)
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) Strat @ drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) Strat @ drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> =  T\<^sub>p init (take (Suc x) qs) (take (Suc x) ?Strat')
            + T\<^sub>p ?interstate' (drop (Suc x) qs) (drop (Suc x) ?Strat') + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
unfolding bef state
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
x < length Strat

goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
by(simp add: min_def nth_append)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) Strat) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) Strat)) (drop (Suc x) qs) (drop (Suc x) Strat) = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs)  (take (Suc x) ?Strat' @ drop (Suc x) ?Strat') + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) @ drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
apply(subst T_append2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (take (Suc x) qs) = length (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))
 2. T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
x < length Strat

goal (2 subgoals):
 1. length (take (Suc x) qs) = length (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))
 2. T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 = T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1
[PROOF STEP]
by(simp_all add: min_def)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) @ drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + T\<^sub>p (Partial_Cost_Model.steps init (take (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat))) (drop (Suc x) qs) (drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 = T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) @ drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = T\<^sub>p init qs ?Strat' + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) @ drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 = T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>p init (take (Suc x) qs @ drop (Suc x) qs) (take (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) @ drop (Suc x) (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)) + 1 = T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p init qs Strat = T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1
[PROOF STEP]
have better: "T\<^sub>p init qs ?Strat' + 1 = T\<^sub>p init qs Strat"
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p init qs Strat = T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1

goal (1 subgoal):
 1. T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 = T\<^sub>p init qs Strat
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 = T\<^sub>p init qs Strat

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "T\<^sub>p init qs ?Strat' + 1 = T\<^sub>p init qs Strat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 = T\<^sub>p init qs Strat
[PROOF STEP]
by (fact better)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 = T\<^sub>p init qs Strat

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 = T\<^sub>p init qs Strat

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = T\<^sub>p_opt init qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init qs Strat = T\<^sub>p_opt init qs
[PROOF STEP]
by (fact opt)
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = T\<^sub>p_opt init qs

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = T\<^sub>p_opt init qs

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from cInf_lower[OF isin]
[PROOF STATE]
proof (chain)
picking this:
bdd_below {T\<^sub>p init qs as |as. length as = length qs} \<Longrightarrow> \<Sqinter> {T\<^sub>p init qs as |as. length as = length qs} \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)
[PROOF STEP]
have "\<dots>  \<le>  T\<^sub>p init qs ?Strat'"
[PROOF STATE]
proof (prove)
using this:
bdd_below {T\<^sub>p init qs as |as. length as = length qs} \<Longrightarrow> \<Sqinter> {T\<^sub>p init qs as |as. length as = length qs} \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)

goal (1 subgoal):
 1. T\<^sub>p_opt init qs \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)
[PROOF STEP]
unfolding T_opt_def
[PROOF STATE]
proof (prove)
using this:
bdd_below {T\<^sub>p init qs as |as. length as = length qs} \<Longrightarrow> \<Sqinter> {T\<^sub>p init qs as |as. length as = length qs} \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)

goal (1 subgoal):
 1. \<Sqinter> {T\<^sub>p init qs as |as. length as = length qs} \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>p_opt init qs \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x)); \<not> Suc (snd (Strat ! x) ! l) < length init\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)

goal (1 subgoal):
 1. False
[PROOF STEP]
using init_nempty
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat) + 1 \<le> T\<^sub>p init qs (take x Strat @ (fst (Strat ! x), take l (snd (Strat ! x)) @ drop (Suc l) (snd (Strat ! x))) # drop (Suc x) Strat)
init \<noteq> []

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma umformung_OPT:
  assumes inlist: "set qs \<subseteq> set init"
  assumes dist: "distinct init"
  assumes a: "T\<^sub>p_opt init qs = T\<^sub>p init qs Strat"
  assumes b: " length qs = length Strat"
  assumes c: "init\<noteq>[]"
  shows "T\<^sub>p_opt init qs =
    (\<Sum>(x,y)\<in>{(x,y::('a::linorder)). x \<in> set init \<and> y\<in>set init \<and> x<y}.
          ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "T\<^sub>p_opt init qs = T\<^sub>p init qs Strat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_opt init qs = T\<^sub>p init qs Strat
[PROOF STEP]
by(fact a)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_opt init qs = T\<^sub>p init qs Strat

goal (1 subgoal):
 1. T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_opt init qs = T\<^sub>p init qs Strat

goal (1 subgoal):
 1. T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "\<dots> =
    (\<Sum>(x,y)\<in>{(x,y::('a::linorder)). x \<in> set init \<and> y\<in>set init \<and> x<y}.
          ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
apply(rule umformung_OPT')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. set qs \<subseteq> set init
 2. distinct init
 3. length qs = length Strat
 4. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x))\<rbrakk> \<Longrightarrow> Suc (snd (Strat ! x) ! l) < length init
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x))\<rbrakk> \<Longrightarrow> Suc (snd (Strat ! x) ! l) < length init
[PROOF STEP]
using OPT_noStupid[OF b[symmetric] a[symmetric] c]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x < length Strat; ?l < length (snd (Strat ! ?x))\<rbrakk> \<Longrightarrow> Suc (snd (Strat ! ?x) ! ?l) < length init

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>x < length Strat; l < length (snd (Strat ! x))\<rbrakk> \<Longrightarrow> Suc (snd (Strat ! x) ! l) < length init
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
T\<^sub>p_opt init qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cardofpairs: "S \<noteq> [] \<Longrightarrow> sorted S \<Longrightarrow> distinct S \<Longrightarrow> card {(x,y). x \<in> set S \<and> y\<in>set S \<and> x<y} = ((length S)*(length S-1)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<noteq> []; sorted S; distinct S\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set S \<and> y \<in> set S \<and> x < y}) = real (length S * (length S - 1)) / 2
[PROOF STEP]
proof (induct S rule: list_nonempty_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
case (cons s ss)
[PROOF STATE]
proof (state)
this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)
[PROOF STEP]
have "sorted ss" "distinct ss"
[PROOF STATE]
proof (prove)
using this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)

goal (1 subgoal):
 1. sorted ss &&& distinct ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sorted ss
distinct ss

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
from cons(2)[OF this(1) this(2)]
[PROOF STATE]
proof (chain)
picking this:
real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
[PROOF STEP]
have iH: "card {(x, y) . x \<in> set ss \<and> y \<in> set ss \<and> x < y}
    = (length ss * (length ss-1)) / 2"
[PROOF STATE]
proof (prove)
using this:
real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2

goal (1 subgoal):
 1. real (card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
from cons
[PROOF STATE]
proof (chain)
picking this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)
[PROOF STEP]
have sss: "s \<notin> set ss"
[PROOF STATE]
proof (prove)
using this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)

goal (1 subgoal):
 1. s \<notin> set ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<notin> set ss

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
from cons
[PROOF STATE]
proof (chain)
picking this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)
[PROOF STEP]
have tt: "(\<forall>y\<in>set (s#ss). s \<le> y)"
[PROOF STATE]
proof (prove)
using this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)

goal (1 subgoal):
 1. \<forall>y\<in>set (s # ss). s \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (s # ss). s \<le> y

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
with cons
[PROOF STATE]
proof (chain)
picking this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)
\<forall>y\<in>set (s # ss). s \<le> y
[PROOF STEP]
have tt': "(\<forall>y\<in>set ss. s < y)"
[PROOF STATE]
proof (prove)
using this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)
\<forall>y\<in>set (s # ss). s \<le> y

goal (1 subgoal):
 1. \<forall>y\<in>set ss. s < y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ss \<noteq> []; \<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2; sorted (s # ss); distinct (s # ss); \<forall>y\<in>set (s # ss). s \<le> y\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ss. s < y
[PROOF STEP]
from sss
[PROOF STATE]
proof (chain)
picking this:
s \<notin> set ss
[PROOF STEP]
have "(\<forall>y\<in>set ss. s \<noteq> y)"
[PROOF STATE]
proof (prove)
using this:
s \<notin> set ss

goal (1 subgoal):
 1. \<forall>y\<in>set ss. s \<noteq> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ss. s \<noteq> y

goal (1 subgoal):
 1. \<lbrakk>ss \<noteq> []; \<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2; sorted (s # ss); distinct (s # ss); \<forall>y\<in>set (s # ss). s \<le> y\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ss. s < y
[PROOF STEP]
with tt
[PROOF STATE]
proof (chain)
picking this:
\<forall>y\<in>set (s # ss). s \<le> y
\<forall>y\<in>set ss. s \<noteq> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set (s # ss). s \<le> y
\<forall>y\<in>set ss. s \<noteq> y

goal (1 subgoal):
 1. \<forall>y\<in>set ss. s < y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ss. s < y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ss. s < y

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y\<in>set ss. s < y
[PROOF STEP]
have "{(x, y) . x = s \<and> y \<in> set ss \<and> x < y}
          = {(x, y) . x = s \<and> y \<in> set ss}"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set ss. s < y

goal (1 subgoal):
 1. {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {(x, y). x = s \<and> y \<in> set ss}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {(x, y). x = s \<and> y \<in> set ss}

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {(x, y). x = s \<and> y \<in> set ss}

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = {s}\<times>(set ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x = s \<and> y \<in> set ss} = {s} \<times> set ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x = s \<and> y \<in> set ss} = {s} \<times> set ss

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {s} \<times> set ss
[PROOF STEP]
have "{(x, y) . x = s \<and> y \<in> set ss \<and> x < y} = {s}\<times>(set ss)"
[PROOF STATE]
proof (prove)
using this:
{(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {s} \<times> set ss

goal (1 subgoal):
 1. {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {s} \<times> set ss
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {s} \<times> set ss

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {s} \<times> set ss
[PROOF STEP]
have "card {(x, y) . x = s \<and> y \<in> set ss \<and> x < y}
          = card (set ss)"
[PROOF STATE]
proof (prove)
using this:
{(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {s} \<times> set ss

goal (1 subgoal):
 1. card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = card (set ss)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = card (set ss)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = card (set ss)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
from cons distinct_card
[PROOF STATE]
proof (chain)
picking this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)
distinct ?xs \<Longrightarrow> card (set ?xs) = length ?xs
[PROOF STEP]
have "\<dots> = length ss"
[PROOF STATE]
proof (prove)
using this:
ss \<noteq> []
\<lbrakk>sorted ss; distinct ss\<rbrakk> \<Longrightarrow> real (card {a. case a of (x, y) \<Rightarrow> x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
sorted (s # ss)
distinct (s # ss)
distinct ?xs \<Longrightarrow> card (set ?xs) = length ?xs

goal (1 subgoal):
 1. card (set ss) = length ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (set ss) = length ss

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = length ss
[PROOF STEP]
have step: "card {(x, y) . x = s \<and> y \<in> set ss \<and> x < y} =
            length ss"
[PROOF STATE]
proof (prove)
using this:
card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = length ss

goal (1 subgoal):
 1. card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = length ss
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = length ss

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have uni: "{(x, y) . x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y}
      = {(x, y) . x \<in> set ss \<and> y \<in> set ss \<and> x < y}
        \<union> {(x, y) . x = s \<and> y \<in> set ss \<and> x < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y}
[PROOF STEP]
using tt
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set (s # ss). s \<le> y

goal (1 subgoal):
 1. {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y}

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have disj: "{(x, y) . x \<in> set ss \<and> y \<in> set ss \<and> x < y}
        \<inter> {(x, y) . x = s \<and> y \<in> set ss \<and> x < y} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
using sss
[PROOF STATE]
proof (prove)
using this:
s \<notin> set ss

goal (1 subgoal):
 1. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "card {(x, y) . x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y}
    = card ({(x, y) . x \<in> set ss \<and> y \<in> set ss \<and> x < y}
        \<union> {(x, y) . x = s \<and> y \<in> set ss \<and> x < y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = card ({(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y})
[PROOF STEP]
using uni
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y}

goal (1 subgoal):
 1. card {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = card ({(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = card ({(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y})

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y} = card ({(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y})

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = card {(x, y) . x \<in> set ss \<and> y \<in> set ss \<and> x < y}
          + card {(x, y) . x = s \<and> y \<in> set ss \<and> x < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y}) = card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} + card {(x, y). x = s \<and> y \<in> set ss \<and> x < y}
[PROOF STEP]
apply(rule card_Un_disjoint)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y}
 2. finite {(x, y). x = s \<and> y \<in> set ss \<and> x < y}
 3. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
apply(rule finite_subset[where B="(set ss) \<times> (set ss)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<subseteq> set ss \<times> set ss
 2. finite (set ss \<times> set ss)
 3. finite {(x, y). x = s \<and> y \<in> set ss \<and> x < y}
 4. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
apply(force)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (set ss \<times> set ss)
 2. finite {(x, y). x = s \<and> y \<in> set ss \<and> x < y}
 3. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {(x, y). x = s \<and> y \<in> set ss \<and> x < y}
 2. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
apply(rule finite_subset[where B="{s} \<times> (set ss)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {(x, y). x = s \<and> y \<in> set ss \<and> x < y} \<subseteq> {s} \<times> set ss
 2. finite ({s} \<times> set ss)
 3. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
apply(force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite ({s} \<times> set ss)
 2. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
using disj
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}

goal (1 subgoal):
 1. {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<inter> {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = {}
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
card ({(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y}) = card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} + card {(x, y). x = s \<and> y \<in> set ss \<and> x < y}

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} \<union> {(x, y). x = s \<and> y \<in> set ss \<and> x < y}) = card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} + card {(x, y). x = s \<and> y \<in> set ss \<and> x < y}

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = (length ss * (length ss-1)) / 2
                  + length ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} + card {(x, y). x = s \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2 + real (length ss)
[PROOF STEP]
using iH step
[PROOF STATE]
proof (prove)
using this:
real (card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2
card {(x, y). x = s \<and> y \<in> set ss \<and> x < y} = length ss

goal (1 subgoal):
 1. real (card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} + card {(x, y). x = s \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2 + real (length ss)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} + card {(x, y). x = s \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2 + real (length ss)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (card {(x, y). x \<in> set ss \<and> y \<in> set ss \<and> x < y} + card {(x, y). x = s \<and> y \<in> set ss \<and> x < y}) = real (length ss * (length ss - 1)) / 2 + real (length ss)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = (length ss * (length ss-1) + 2*length ss) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (length ss * (length ss - 1)) / 2 + real (length ss) = real (length ss * (length ss - 1) + 2 * length ss) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1)) / 2 + real (length ss) = real (length ss * (length ss - 1) + 2 * length ss) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1)) / 2 + real (length ss) = real (length ss * (length ss - 1) + 2 * length ss) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = (length ss * (length ss-1) + length ss * 2) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (length ss * (length ss - 1) + 2 * length ss) / 2 = real (length ss * (length ss - 1) + length ss * 2) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1) + 2 * length ss) / 2 = real (length ss * (length ss - 1) + length ss * 2) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1) + 2 * length ss) / 2 = real (length ss * (length ss - 1) + length ss * 2) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = (length ss * (length ss-1+2)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (length ss * (length ss - 1) + length ss * 2) / 2 = real (length ss * (length ss - 1 + 2)) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1) + length ss * 2) / 2 = real (length ss * (length ss - 1 + 2)) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1) + length ss * 2) / 2 = real (length ss * (length ss - 1 + 2)) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = (length ss * (length ss+1)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (length ss * (length ss - 1 + 2)) / 2 = real (length ss * (length ss + 1)) / 2
[PROOF STEP]
using cons(1)
[PROOF STATE]
proof (prove)
using this:
ss \<noteq> []

goal (1 subgoal):
 1. real (length ss * (length ss - 1 + 2)) / 2 = real (length ss * (length ss + 1)) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1 + 2)) / 2 = real (length ss * (length ss + 1)) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss - 1 + 2)) / 2 = real (length ss * (length ss + 1)) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = ((length ss+1) * length ss) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (length ss * (length ss + 1)) / 2 = real ((length ss + 1) * length ss) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss + 1)) / 2 = real ((length ss + 1) * length ss) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (length ss * (length ss + 1)) / 2 = real ((length ss + 1) * length ss) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
have "\<dots> = (length (s#ss) * (length (s#ss)-1)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real ((length ss + 1) * length ss) / 2 = real (length (s # ss) * (length (s # ss) - 1)) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real ((length ss + 1) * length ss) / 2 = real (length (s # ss) * (length (s # ss) - 1)) / 2

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
 2. \<And>x xs. \<lbrakk>xs \<noteq> []; \<lbrakk>sorted xs; distinct xs\<rbrakk> \<Longrightarrow> real (card {(x, y). x \<in> set xs \<and> y \<in> set xs \<and> x < y}) = real (length xs * (length xs - 1)) / 2; sorted (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set (x # xs) \<and> y \<in> set (x # xs) \<and> xa < y}) = real (length (x # xs) * (length (x # xs) - 1)) / 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (card {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y}) = real (length (s # ss) * (length (s # ss) - 1)) / 2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
real (card {(x, y). x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y}) = real (length (s # ss) * (length (s # ss) - 1)) / 2

goal (1 subgoal):
 1. real (card {a. case a of (x, y) \<Rightarrow> x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y}) = real (length (s # ss) * (length (s # ss) - 1)) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (card {a. case a of (x, y) \<Rightarrow> x \<in> set (s # ss) \<and> y \<in> set (s # ss) \<and> x < y}) = real (length (s # ss) * (length (s # ss) - 1)) / 2

goal (1 subgoal):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
[PROOF STEP]
case single
[PROOF STATE]
proof (state)
this:
sorted [x_]
distinct [x_]

goal (1 subgoal):
 1. \<And>x. \<lbrakk>sorted [x]; distinct [x]\<rbrakk> \<Longrightarrow> real (card {(xa, y). xa \<in> set [x] \<and> y \<in> set [x] \<and> xa < y}) = real (length [x] * (length [x] - 1)) / 2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted [x_]
distinct [x_]

goal (1 subgoal):
 1. real (card {a. case a of (xa, y) \<Rightarrow> xa \<in> set [x_] \<and> y \<in> set [x_] \<and> xa < y}) = real (length [x_] * (length [x_] - 1)) / 2
[PROOF STEP]
by(simp cong: conj_cong)
[PROOF STATE]
proof (state)
this:
real (card {a. case a of (xa, y) \<Rightarrow> xa \<in> set [x_] \<and> y \<in> set [x_] \<and> xa < y}) = real (length [x_] * (length [x_] - 1)) / 2

goal:
No subgoals!
[PROOF STEP]
qed