[STATEMENT]
lemma (in dom_sl) decomp_propa: "\<And>ss w.
   (\<forall>(q,t)\<in>set qs. q < size ss \<and> t \<in> A ) \<Longrightarrow>
   sorted w \<Longrightarrow>
   set ss \<subseteq> A \<Longrightarrow>
   propa f qs ss w = (merges f qs ss, (sorted_list_of_set ({q. \<exists>t.(q,t)\<in>set qs \<and> t \<squnion>\<^bsub>f\<^esub> (ss!q) \<noteq> ss!q} \<union> set w)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply (induct qs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set []. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f [] ss w = (merges f [] ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set [] \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
 2. \<And>a qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); \<forall>(q, t)\<in>set (a # qs). q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f (a # qs) ss w = (merges f (a # qs) ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (a # qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply (fastforce intro:sorted_less_set_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); \<forall>(q, t)\<in>set (a # qs). q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f (a # qs) ss w = (merges f (a # qs) ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (a # qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply (simp (no_asm))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); \<forall>(q, t)\<in>set (a # qs). q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> (case a of (q, \<tau>) \<Rightarrow> propa f qs (ss[q := \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q]) (if \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q = ss ! q then w else insort q (remove1 q w))) = (case a of (p, \<tau>) \<Rightarrow> merges f qs (ss[p := \<tau> \<squnion>\<^bsub>f\<^esub> ss ! p]), sorted_list_of_set ({q. \<exists>t. ((q, t) = a \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); \<forall>(q, t)\<in>set ((a, b) # qs). q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]) (if b \<squnion>\<^bsub>f\<^esub> ss ! a = ss ! a then w else insort a (remove1 a w)) = (merges f qs (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]), sorted_list_of_set ({q. \<exists>t. ((q, t) = (a, b) \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply (subst sorted_insort_remove1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); \<forall>(q, t)\<in>set ((a, b) # qs). q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> Sorted_Less.sorted w
 2. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); \<forall>(q, t)\<in>set ((a, b) # qs). q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]) (if b \<squnion>\<^bsub>f\<^esub> ss ! a = ss ! a then w else sorted_list_of_set (insert a (set w))) = (merges f qs (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]), sorted_list_of_set ({q. \<exists>t. ((q, t) = (a, b) \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>(q, t)\<in>set qs. q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); \<forall>(q, t)\<in>set ((a, b) # qs). q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]) (if b \<squnion>\<^bsub>f\<^esub> ss ! a = ss ! a then w else sorted_list_of_set (insert a (set w))) = (merges f qs (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]), sorted_list_of_set ({q. \<exists>t. ((q, t) = (a, b) \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply (simp add: sorted_less_sorted_list_of_set Semilat.closed_f[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); a < length ss \<and> b \<in> A \<and> (\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A); Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> (b \<squnion>\<^bsub>f\<^esub> ss ! a = ss ! a \<longrightarrow> sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w) = sorted_list_of_set ({q. \<exists>t. (q = a \<and> t = b \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)) \<and> (b \<squnion>\<^bsub>f\<^esub> ss ! a \<noteq> ss ! a \<longrightarrow> sorted_list_of_set (insert a ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] ! q \<noteq> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] ! q} \<union> set w)) = sorted_list_of_set ({q. \<exists>t. (q = a \<and> t = b \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); a < length ss \<and> b \<in> A \<and> (\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A); Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> b \<squnion>\<^bsub>f\<^esub> ss ! a = ss ! a \<longrightarrow> sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w) = sorted_list_of_set ({q. \<exists>t. (q = a \<and> t = b \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)
 2. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); a < length ss \<and> b \<in> A \<and> (\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A); Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> b \<squnion>\<^bsub>f\<^esub> ss ! a \<noteq> ss ! a \<longrightarrow> sorted_list_of_set (insert a ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] ! q \<noteq> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] ! q} \<union> set w)) = sorted_list_of_set ({q. \<exists>t. (q = a \<and> t = b \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)
[PROOF STEP]
apply (blast intro: arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); a < length ss \<and> b \<in> A \<and> (\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A); Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> b \<squnion>\<^bsub>f\<^esub> ss ! a \<noteq> ss ! a \<longrightarrow> sorted_list_of_set (insert a ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] ! q \<noteq> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] ! q} \<union> set w)) = sorted_list_of_set ({q. \<exists>t. (q = a \<and> t = b \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)
[PROOF STEP]
apply(simp add: nth_list_update)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b qs ss w. \<lbrakk>\<And>ss w. \<lbrakk>\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f qs ss w = (merges f qs ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)); a < length ss \<and> b \<in> A \<and> (\<forall>x\<in>set qs. case x of (q, t) \<Rightarrow> q < length ss \<and> t \<in> A); Sorted_Less.sorted w; set ss \<subseteq> A\<rbrakk> \<Longrightarrow> b \<squnion>\<^bsub>f\<^esub> ss ! a \<noteq> ss ! a \<longrightarrow> sorted_list_of_set (insert a ({q. (a = q \<longrightarrow> (\<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> (b \<squnion>\<^bsub>f\<^esub> ss ! q) \<noteq> b \<squnion>\<^bsub>f\<^esub> ss ! q)) \<and> (a \<noteq> q \<longrightarrow> (\<exists>t. (q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q))} \<union> set w)) = sorted_list_of_set ({q. \<exists>t. (q = a \<and> t = b \<or> (q, t) \<in> set qs) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set w)
[PROOF STEP]
by (auto intro: arg_cong)


[STATEMENT]
lemma distinct_pair_filter_n: "distinct (map fst xs) \<Longrightarrow> a \<notin> set (map fst xs) \<Longrightarrow> (map snd (filter (\<lambda>(x,y). x = a) xs)) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst xs); a \<notin> set (map fst xs)\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = a) xs) = []
[PROOF STEP]
by (induct xs) (auto simp add: distinct_map_filter image_def)


[STATEMENT]
lemma map_fst: "map fst (map (\<lambda>pc. (pc, x)) xs) =  xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (map (\<lambda>pc. (pc, x)) xs) = xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma distinct_p: "p < n \<longrightarrow> distinct (map fst (step p (ss!p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p < n \<longrightarrow> distinct (map fst (step p (ss ! p)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p < n \<longrightarrow> distinct (map fst (step p (ss ! p)))
[PROOF STEP]
let ?qs = "step p (ss!p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p < n \<longrightarrow> distinct (map fst (step p (ss ! p)))
[PROOF STEP]
have "map fst ?qs = (rev (sorted_list_of_set(succs p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (step p (ss ! p)) = rev (sorted_list_of_set (succs p))
[PROOF STEP]
using map_fst[of _ "(rev (sorted_list_of_set(succs p)))"]
[PROOF STATE]
proof (prove)
using this:
map fst (map (\<lambda>pc. (pc, ?x)) (rev (sorted_list_of_set (succs p)))) = rev (sorted_list_of_set (succs p))

goal (1 subgoal):
 1. map fst (step p (ss ! p)) = rev (sorted_list_of_set (succs p))
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
map fst (step p (ss ! p)) = rev (sorted_list_of_set (succs p))

goal (1 subgoal):
 1. p < n \<longrightarrow> distinct (map fst (step p (ss ! p)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map fst (step p (ss ! p)) = rev (sorted_list_of_set (succs p))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map fst (step p (ss ! p)) = rev (sorted_list_of_set (succs p))

goal (1 subgoal):
 1. p < n \<longrightarrow> distinct (map fst (step p (ss ! p)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p < n \<longrightarrow> distinct (map fst (step p (ss ! p)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_pair_filter: "distinct (map fst xs) \<Longrightarrow> (a,b)\<in> set xs \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst xs); (a, b) \<in> set xs\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct (map fst []); (a, b) \<in> set []\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) []) = [b]
 2. \<And>aa xs. \<lbrakk>\<lbrakk>distinct (map fst xs); (a, b) \<in> set xs\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]; distinct (map fst (aa # xs)); (a, b) \<in> set (aa # xs)\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) (aa # xs)) = [b]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>distinct (map fst xs); (a, b) \<in> set xs\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]; distinct (map fst (aa # xs)); (a, b) \<in> set (aa # xs)\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) (aa # xs)) = [b]
[PROOF STEP]
apply (auto simp add: distinct_map_filter image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>(a, b) \<in> set xs \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]; \<forall>x\<in>set xs. a \<noteq> fst x; distinct (map fst xs)\<rbrakk> \<Longrightarrow> filter (\<lambda>x. fst x = a) xs = []
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>(a, b) \<in> set xs \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]; \<forall>x\<in>set xs. a \<noteq> fst x; distinct (map fst xs)\<rbrakk> \<Longrightarrow> filter (\<lambda>x. fst x = a) xs = []
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>(a, b) \<in> set xs \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]; \<forall>x\<in>set xs. a \<noteq> fst x; distinct (map fst xs)\<rbrakk> \<Longrightarrow> filter (\<lambda>x. fst x = a) xs = []
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>(a, b) \<in> set xs \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]; \<forall>x\<in>set xs. a \<noteq> fst x; distinct (map fst xs)\<rbrakk> \<Longrightarrow> filter (\<lambda>x. fst x = a) xs = []
[PROOF STEP]
assume "\<forall>x\<in>set xs. a \<noteq> fst x " and " distinct (map fst xs)"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set xs. a \<noteq> fst x
distinct (map fst xs)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>(a, b) \<in> set xs \<Longrightarrow> map snd (filter (\<lambda>x. fst x = a) xs) = [b]; \<forall>x\<in>set xs. a \<noteq> fst x; distinct (map fst xs)\<rbrakk> \<Longrightarrow> filter (\<lambda>x. fst x = a) xs = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set xs. a \<noteq> fst x
distinct (map fst xs)
[PROOF STEP]
show "filter (\<lambda>x. fst x = a) xs = []"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set xs. a \<noteq> fst x
distinct (map fst xs)

goal (1 subgoal):
 1. filter (\<lambda>x. fst x = a) xs = []
[PROOF STEP]
by (induct xs)  auto
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. fst x = a) xs = []

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>set ?xsa2. a \<noteq> fst x; distinct (map fst ?xsa2)\<rbrakk> \<Longrightarrow> filter (\<lambda>x. fst x = a) ?xsa2 = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma split_comp_eq_pair: "(\<lambda>x. fst x = a) = (\<lambda>(x,y). x = a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. fst x = a) = (\<lambda>(x, y). x = a)
[PROOF STEP]
by (rule split_comp_eq)


[STATEMENT]
lemma merges_property1:
  fixes ss w qs
  assumes step_bounded_pres: "\<forall>(q, \<tau>) \<in> set qs. q < size ss \<and> \<tau> \<in> A"
      and subset_ss_A:       "set ss \<subseteq> A "
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
    shows "\<forall>(q, \<tau>) \<in> set qs. merges f qs ss!q = \<tau> \<squnion>\<^bsub>f\<^esub>ss!q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set qs \<Longrightarrow> case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set qs \<Longrightarrow> case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
assume "x \<in> set qs"
[PROOF STATE]
proof (state)
this:
x \<in> set qs

goal (1 subgoal):
 1. \<And>x. x \<in> set qs \<Longrightarrow> case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst qs)
[PROOF STEP]
have \<tau>: "\<forall>(q, \<tau>) \<in> set qs. (map snd (filter (\<lambda>(x,y). x = q) qs)) = [\<tau>]"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst qs)

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set qs. map snd (filter (\<lambda>(x, y). x = q) qs) = [\<tau>]
[PROOF STEP]
using distinct_pair_filter'
[PROOF STATE]
proof (prove)
using this:
distinct (map fst qs)
\<lbrakk>distinct (map fst ?xs); (?a, ?b) \<in> set ?xs\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = ?a) ?xs) = [?b]

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set qs. map snd (filter (\<lambda>(x, y). x = q) qs) = [\<tau>]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set qs. map snd (filter (\<lambda>(x, y). x = q) qs) = [\<tau>]

goal (1 subgoal):
 1. \<And>x. x \<in> set qs \<Longrightarrow> case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
from len_ss_n subset_ss_A
[PROOF STATE]
proof (chain)
picking this:
length ss = n
set ss \<subseteq> A
[PROOF STEP]
have "ss \<in> nlists n A"
[PROOF STATE]
proof (prove)
using this:
length ss = n
set ss \<subseteq> A

goal (1 subgoal):
 1. ss \<in> nlists n A
[PROOF STEP]
by (rule nlistsI)
[PROOF STATE]
proof (state)
this:
ss \<in> nlists n A

goal (1 subgoal):
 1. \<And>x. x \<in> set qs \<Longrightarrow> case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
with step_bounded_pres
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A
ss \<in> nlists n A
[PROOF STEP]
have merge_nth: "\<forall>(q, \<tau>) \<in> set qs. (merges f qs ss)!q = map snd [(p',t') \<leftarrow> qs. p'=q] \<Squnion>\<^bsub>f\<^esub> ss!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A
ss \<in> nlists n A

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by (fastforce intro:Semilat.nth_merges[OF Semilat.intro, OF is_semi]) \<comment> \<open>use lemma:  listE_length\<close>
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<And>x. x \<in> set qs \<Longrightarrow> case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
with \<tau>
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set qs. map snd (filter (\<lambda>(x, y). x = q) qs) = [\<tau>]
\<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
have "\<forall>(q, \<tau>) \<in> set qs. (merges f qs ss)!q = [\<tau>]\<Squnion>\<^bsub>f\<^esub> ss!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set qs. map snd (filter (\<lambda>(x, y). x = q) qs) = [\<tau>]
\<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = [\<tau>] \<Squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = [\<tau>] \<Squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<And>x. x \<in> set qs \<Longrightarrow> case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = [\<tau>] \<Squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
show "case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = [\<tau>] \<Squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
using \<open>x \<in> set qs\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set qs. merges f qs ss ! q = [\<tau>] \<Squnion>\<^bsub>f\<^esub> ss ! q
x \<in> set qs

goal (1 subgoal):
 1. case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
case x of (q, \<tau>) \<Rightarrow> merges f qs ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma propa_property1:
  fixes ss w qs
  assumes step_bounded_pres: "\<forall>(q, \<tau>) \<in> set qs. q < size ss \<and> \<tau> \<in> A  "
      and sorted_w:          "sorted (w ::nat list)"
      and subset_ss_A:       "set ss \<subseteq> A "
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
    shows "\<forall>(q, \<tau>) \<in> set qs. (fst(propa f qs ss w))!q = \<tau> \<squnion>\<^bsub>f\<^esub>ss!q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set qs. fst (propa f qs ss w) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted w
set ss \<subseteq> A
length ss = n
distinct (map fst qs)

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set qs. fst (propa f qs ss w) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
apply (subgoal_tac "fst (propa f qs ss w) = merges f qs ss")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A; length ss = n; distinct (map fst qs); fst (propa f qs ss w) = merges f qs ss\<rbrakk> \<Longrightarrow> \<forall>(q, \<tau>)\<in>set qs. fst (propa f qs ss w) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
 2. \<lbrakk>\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A; length ss = n; distinct (map fst qs)\<rbrakk> \<Longrightarrow> fst (propa f qs ss w) = merges f qs ss
[PROOF STEP]
apply(simp add: merges_property1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A; length ss = n; distinct (map fst qs)\<rbrakk> \<Longrightarrow> fst (propa f qs ss w) = merges f qs ss
[PROOF STEP]
by (auto dest:decomp_propa)


[STATEMENT]
lemma merges_property2:
  fixes ss w qs q
  assumes step_bounded_pres: "\<forall>(q, \<tau>) \<in> set qs. q < size ss \<and> \<tau> \<in> A"
      and subset_ss_A:       "set ss \<subseteq> A"
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
      and q_nin:             "q \<notin> set(map fst qs) "
      and q_lt_len_ss:       "q < length ss "
    shows "(merges f qs ss)!q = ss!q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merges f qs ss ! q = ss ! q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. merges f qs ss ! q = ss ! q
[PROOF STEP]
from len_ss_n subset_ss_A
[PROOF STATE]
proof (chain)
picking this:
length ss = n
set ss \<subseteq> A
[PROOF STEP]
have "ss \<in> nlists n A"
[PROOF STATE]
proof (prove)
using this:
length ss = n
set ss \<subseteq> A

goal (1 subgoal):
 1. ss \<in> nlists n A
[PROOF STEP]
by (rule nlistsI)
[PROOF STATE]
proof (state)
this:
ss \<in> nlists n A

goal (1 subgoal):
 1. merges f qs ss ! q = ss ! q
[PROOF STEP]
with step_bounded_pres q_lt_len_ss
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A
q < length ss
ss \<in> nlists n A
[PROOF STEP]
have merge_nth: "(merges f qs ss)!q = map snd [(p',t') \<leftarrow> qs. p'=q] \<Squnion>\<^bsub>f\<^esub> ss!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A
q < length ss
ss \<in> nlists n A

goal (1 subgoal):
 1. merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by (fastforce intro:Semilat.nth_merges[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. merges f qs ss ! q = ss ! q
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst qs)
[PROOF STEP]
have "q \<notin> set(map fst qs) \<Longrightarrow> (map snd (filter (\<lambda>(x,y). x = q) qs)) = []"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst qs)

goal (1 subgoal):
 1. q \<notin> set (map fst qs) \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = q) qs) = []
[PROOF STEP]
using distinct_pair_filter_n
[PROOF STATE]
proof (prove)
using this:
distinct (map fst qs)
\<lbrakk>distinct (map fst ?xs); ?a \<notin> set (map fst ?xs)\<rbrakk> \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = ?a) ?xs) = []

goal (1 subgoal):
 1. q \<notin> set (map fst qs) \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = q) qs) = []
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
q \<notin> set (map fst qs) \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = q) qs) = []

goal (1 subgoal):
 1. merges f qs ss ! q = ss ! q
[PROOF STEP]
with merge_nth q_nin
[PROOF STATE]
proof (chain)
picking this:
merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q
q \<notin> set (map fst qs)
q \<notin> set (map fst qs) \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = q) qs) = []
[PROOF STEP]
have "(merges f qs ss)!q = []\<Squnion>\<^bsub>f\<^esub> ss!q"
[PROOF STATE]
proof (prove)
using this:
merges f qs ss ! q = map snd (filter (\<lambda>(p', t'). p' = q) qs) \<Squnion>\<^bsub>f\<^esub> ss ! q
q \<notin> set (map fst qs)
q \<notin> set (map fst qs) \<Longrightarrow> map snd (filter (\<lambda>(x, y). x = q) qs) = []

goal (1 subgoal):
 1. merges f qs ss ! q = [] \<Squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
merges f qs ss ! q = [] \<Squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. merges f qs ss ! q = ss ! q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
merges f qs ss ! q = [] \<Squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
show "(merges f qs ss)!q =  ss ! q"
[PROOF STATE]
proof (prove)
using this:
merges f qs ss ! q = [] \<Squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. merges f qs ss ! q = ss ! q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merges f qs ss ! q = ss ! q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma propa_property2:
  fixes ss w qs q
  assumes step_bounded_pres: "\<forall>(q, \<tau>) \<in> set qs. q < size ss \<and> \<tau> \<in> A"
      and sorted_w:          "sorted (w ::nat list)"
      and subset_ss_A:       "set ss \<subseteq> A"
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
      and q_nin:             "q \<notin> set(map fst qs) "
      and q_lt_len_ss:       "q < length ss "
    shows "(fst(propa f qs ss w))!q = ss!q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (propa f qs ss w) ! q = ss ! q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted w
set ss \<subseteq> A
length ss = n
distinct (map fst qs)
q \<notin> set (map fst qs)
q < length ss

goal (1 subgoal):
 1. fst (propa f qs ss w) ! q = ss ! q
[PROOF STEP]
apply (subgoal_tac "fst (propa f qs ss w) = merges f qs ss")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A; length ss = n; distinct (map fst qs); q \<notin> set (map fst qs); q < length ss; fst (propa f qs ss w) = merges f qs ss\<rbrakk> \<Longrightarrow> fst (propa f qs ss w) ! q = ss ! q
 2. \<lbrakk>\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A; length ss = n; distinct (map fst qs); q \<notin> set (map fst qs); q < length ss\<rbrakk> \<Longrightarrow> fst (propa f qs ss w) = merges f qs ss
[PROOF STEP]
apply(simp add: merges_property2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>(q, \<tau>)\<in>set qs. q < length ss \<and> \<tau> \<in> A; Sorted_Less.sorted w; set ss \<subseteq> A; length ss = n; distinct (map fst qs); q \<notin> set (map fst qs); q < length ss\<rbrakk> \<Longrightarrow> fst (propa f qs ss w) = merges f qs ss
[PROOF STEP]
by (auto dest:decomp_propa)


[STATEMENT]
lemma merges_incr_lemma_dom:
 "\<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst ps) \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst ps) \<longrightarrow> (\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A) \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
assume xs_inA: "xs \<in> nlists n A "
     and step_bounded_pres: "\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A"
     and dist: "distinct (map fst ps)"
[PROOF STATE]
proof (state)
this:
xs \<in> nlists n A
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> nlists n A
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)
[PROOF STEP]
have len_xs_n: "length xs = n" and subset_xs_inA: "set xs \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
xs \<in> nlists n A
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)

goal (1 subgoal):
 1. length xs = n &&& set xs \<subseteq> A
[PROOF STEP]
by (auto simp add:nlistsE_length)
[PROOF STATE]
proof (state)
this:
length xs = n
set xs \<subseteq> A

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
with step_bounded_pres dist
[PROOF STATE]
proof (chain)
picking this:
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)
length xs = n
set xs \<subseteq> A
[PROOF STEP]
have merge1: "\<forall>(q, \<tau>) \<in> set ps. (merges f ps xs)!q = \<tau> \<squnion>\<^bsub>f\<^esub>xs!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)
length xs = n
set xs \<subseteq> A

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set ps. merges f ps xs ! q = \<tau> \<squnion>\<^bsub>f\<^esub> xs ! q
[PROOF STEP]
using merges_property1
[PROOF STATE]
proof (prove)
using this:
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)
length xs = n
set xs \<subseteq> A
\<lbrakk>\<forall>(q, \<tau>)\<in>set ?qs. q < length ?ss \<and> \<tau> \<in> A; set ?ss \<subseteq> A; length ?ss = n; distinct (map fst ?qs)\<rbrakk> \<Longrightarrow> \<forall>(q, \<tau>)\<in>set ?qs. merges f ?qs ?ss ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ?ss ! q

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set ps. merges f ps xs ! q = \<tau> \<squnion>\<^bsub>f\<^esub> xs ! q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set ps. merges f ps xs ! q = \<tau> \<squnion>\<^bsub>f\<^esub> xs ! q

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
from step_bounded_pres dist len_xs_n subset_xs_inA
[PROOF STATE]
proof (chain)
picking this:
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)
length xs = n
set xs \<subseteq> A
[PROOF STEP]
have merge2: "\<And>q. q \<notin> set(map fst ps) \<longrightarrow> q < length xs \<longrightarrow> (merges f ps xs)!q = xs!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)
length xs = n
set xs \<subseteq> A

goal (1 subgoal):
 1. \<And>q. q \<notin> set (map fst ps) \<longrightarrow> q < length xs \<longrightarrow> merges f ps xs ! q = xs ! q
[PROOF STEP]
using merges_property2
[PROOF STATE]
proof (prove)
using this:
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
distinct (map fst ps)
length xs = n
set xs \<subseteq> A
\<lbrakk>\<forall>(q, \<tau>)\<in>set ?qs. q < length ?ss \<and> \<tau> \<in> A; set ?ss \<subseteq> A; length ?ss = n; distinct (map fst ?qs); ?q \<notin> set (map fst ?qs); ?q < length ?ss\<rbrakk> \<Longrightarrow> merges f ?qs ?ss ! ?q = ?ss ! ?q

goal (1 subgoal):
 1. \<And>q. q \<notin> set (map fst ps) \<longrightarrow> q < length xs \<longrightarrow> merges f ps xs ! q = xs ! q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?q \<notin> set (map fst ps) \<longrightarrow> ?q < length xs \<longrightarrow> merges f ps xs ! ?q = xs ! ?q

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
have len_eq: "length xs = length (merges f ps xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length (merges f ps xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length xs = length (merges f ps xs)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
have "\<forall>i<length xs. xs!i \<sqsubseteq>\<^bsub>r\<^esub> (merges f ps xs)!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length xs \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length xs \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
assume i_lt_len_xs: "i < length xs"
[PROOF STATE]
proof (state)
this:
i < length xs

goal (1 subgoal):
 1. \<And>i. i < length xs \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
with xs_inA
[PROOF STATE]
proof (chain)
picking this:
xs \<in> nlists n A
i < length xs
[PROOF STEP]
have xs_i_inA: "xs!i \<in> A"
[PROOF STATE]
proof (prove)
using this:
xs \<in> nlists n A
i < length xs

goal (1 subgoal):
 1. xs ! i \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs ! i \<in> A

goal (1 subgoal):
 1. \<And>i. i < length xs \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
show " xs ! i \<sqsubseteq>\<^bsub>r\<^esub> (merges f ps xs) ! i "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
proof(cases "i \<in> set (map fst ps)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
 2. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> set (map fst ps)

goal (2 subgoals):
 1. i \<in> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
 2. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (map fst ps)
[PROOF STEP]
obtain s' where s': "(i, s') \<in> set ps"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (map fst ps)

goal (1 subgoal):
 1. (\<And>s'. (i, s') \<in> set ps \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i, s') \<in> set ps

goal (2 subgoals):
 1. i \<in> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
 2. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
with merge1
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set ps. merges f ps xs ! q = \<tau> \<squnion>\<^bsub>f\<^esub> xs ! q
(i, s') \<in> set ps
[PROOF STEP]
have merge1': "(merges f ps xs)!i = s' \<squnion>\<^bsub>f\<^esub> xs ! i"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set ps. merges f ps xs ! q = \<tau> \<squnion>\<^bsub>f\<^esub> xs ! q
(i, s') \<in> set ps

goal (1 subgoal):
 1. merges f ps xs ! i = s' \<squnion>\<^bsub>f\<^esub> xs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merges f ps xs ! i = s' \<squnion>\<^bsub>f\<^esub> xs ! i

goal (2 subgoals):
 1. i \<in> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
 2. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
from s' step_bounded_pres
[PROOF STATE]
proof (chain)
picking this:
(i, s') \<in> set ps
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A
[PROOF STEP]
have "s' \<in> A"
[PROOF STATE]
proof (prove)
using this:
(i, s') \<in> set ps
\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A

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

goal (2 subgoals):
 1. i \<in> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
 2. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
with xs_i_inA merge1'
[PROOF STATE]
proof (chain)
picking this:
xs ! i \<in> A
merges f ps xs ! i = s' \<squnion>\<^bsub>f\<^esub> xs ! i
s' \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs ! i \<in> A
merges f ps xs ! i = s' \<squnion>\<^bsub>f\<^esub> xs ! i
s' \<in> A

goal (1 subgoal):
 1. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
by (auto intro: Semilat.ub2[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> set (map fst ps)

goal (1 subgoal):
 1. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
note i_nin = this
[PROOF STATE]
proof (state)
this:
i \<notin> set (map fst ps)

goal (1 subgoal):
 1. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
with i_lt_len_xs merge2
[PROOF STATE]
proof (chain)
picking this:
i < length xs
?q \<notin> set (map fst ps) \<longrightarrow> ?q < length xs \<longrightarrow> merges f ps xs ! ?q = xs ! ?q
i \<notin> set (map fst ps)
[PROOF STEP]
have "(merges f ps xs)!i = xs!i"
[PROOF STATE]
proof (prove)
using this:
i < length xs
?q \<notin> set (map fst ps) \<longrightarrow> ?q < length xs \<longrightarrow> merges f ps xs ! ?q = xs ! ?q
i \<notin> set (map fst ps)

goal (1 subgoal):
 1. merges f ps xs ! i = xs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merges f ps xs ! i = xs ! i

goal (1 subgoal):
 1. i \<notin> set (map fst ps) \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
with xs_i_inA
[PROOF STATE]
proof (chain)
picking this:
xs ! i \<in> A
merges f ps xs ! i = xs ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs ! i \<in> A
merges f ps xs ! i = xs ! i

goal (1 subgoal):
 1. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
by (auto simp add:Semilat.refl_r[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
have "\<forall>i<length xs. xs!i \<sqsubseteq>\<^bsub>r\<^esub> (merges f ps xs)!i"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
have "\<forall>i<length xs. lesub (xs!i) r  ((merges f ps xs)!i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
by (auto simp add:lesssub_def lesub_def)
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
have  "\<forall>i<length xs. (\<lambda>x y. lesub x r y) (xs!i)((merges f ps xs)!i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
have nth_lt: "\<And>i. i <length xs \<Longrightarrow>  (\<lambda>x y. lesub x r y) (xs!i)((merges f ps xs)!i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length xs. xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i

goal (1 subgoal):
 1. \<And>i. i < length xs \<Longrightarrow> xs ! i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?i < length xs \<Longrightarrow> xs ! ?i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! ?i

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
with len_eq
[PROOF STATE]
proof (chain)
picking this:
length xs = length (merges f ps xs)
?i < length xs \<Longrightarrow> xs ! ?i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! ?i
[PROOF STEP]
show "xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs"
[PROOF STATE]
proof (prove)
using this:
length xs = length (merges f ps xs)
?i < length xs \<Longrightarrow> xs ! ?i \<sqsubseteq>\<^bsub>r\<^esub> merges f ps xs ! ?i

goal (1 subgoal):
 1. xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
by (auto simp only:list_all2_conv_all_nth Listn.le_def lesssub_def lesub_def)
[PROOF STATE]
proof (state)
this:
xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma merges_incr_dom:
 "\<lbrakk> xs \<in> nlists n A; distinct (map fst ps); \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> nlists n A; distinct (map fst ps); \<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs
[PROOF STEP]
by (simp add: merges_incr_lemma_dom)


[STATEMENT]
lemma merges_same_conv_dom [rule_format]:
 "(\<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst ps) \<longrightarrow>
        (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow>
        (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x \<sqsubseteq>\<^bsub>r\<^esub> xs!p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst ps) \<longrightarrow> (\<forall>(p, x)\<in>set ps. p < length xs \<and> x \<in> A) \<longrightarrow> (merges f ps xs = xs) = (\<forall>(p, x)\<in>set ps. x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)
[PROOF STEP]
apply (induct_tac ps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst []) \<longrightarrow> (\<forall>a\<in>set []. case a of (p, x) \<Rightarrow> p < length xs \<and> x \<in> A) \<longrightarrow> (merges f [] xs = xs) = (\<forall>a\<in>set []. case a of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)
 2. \<And>a list. \<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst list) \<longrightarrow> (\<forall>a\<in>set list. case a of (p, x) \<Rightarrow> p < length xs \<and> x \<in> A) \<longrightarrow> (merges f list xs = xs) = (\<forall>a\<in>set list. case a of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p) \<Longrightarrow> \<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst (a # list)) \<longrightarrow> (\<forall>a\<in>set (a # list). case a of (p, x) \<Rightarrow> p < length xs \<and> x \<in> A) \<longrightarrow> (merges f (a # list) xs = xs) = (\<forall>a\<in>set (a # list). case a of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst list) \<longrightarrow> (\<forall>a\<in>set list. case a of (p, x) \<Rightarrow> p < length xs \<and> x \<in> A) \<longrightarrow> (merges f list xs = xs) = (\<forall>a\<in>set list. case a of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p) \<Longrightarrow> \<forall>xs. xs \<in> nlists n A \<longrightarrow> distinct (map fst (a # list)) \<longrightarrow> (\<forall>a\<in>set (a # list). case a of (p, x) \<Rightarrow> p < length xs \<and> x \<in> A) \<longrightarrow> (merges f (a # list) xs = xs) = (\<forall>a\<in>set (a # list). case a of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b list xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f list xs = xs) = (\<forall>x\<in>set list. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; a \<notin> fst ` set list; distinct (map fst list); \<forall>x\<in>set list. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; a < n; b \<in> A\<rbrakk> \<Longrightarrow> (merges f list (xs[a := b \<squnion>\<^bsub>f\<^esub> xs ! a]) = xs) = (b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a \<and> (\<forall>x\<in>set list. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p))
[PROOF STEP]
apply (rename_tac p x ps xs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A\<rbrakk> \<Longrightarrow> (merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs) = (x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (rule context_conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (subgoal_tac "xs[p := x \<squnion>\<^bsub>f\<^esub> xs!p] [\<sqsubseteq>\<^bsub>r\<^esub>] xs")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p] [\<sqsubseteq>\<^bsub>r\<^esub>] xs\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs\<rbrakk> \<Longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p] [\<sqsubseteq>\<^bsub>r\<^esub>] xs
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 4. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (fastforce dest!: le_listD
            simp add: nth_list_update Semilat.plus_le_conv[OF Semilat.intro,OF is_semi]
                      Semilat.ub1[OF Semilat.intro,OF is_semi]
                      Semilat.ub2[OF Semilat.intro,OF is_semi]
Semilat.lub[OF Semilat.intro,OF is_semi]
 )
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs\<rbrakk> \<Longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p] [\<sqsubseteq>\<^bsub>r\<^esub>] xs
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (erule subst, rule merges_incr_dom)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A\<rbrakk> \<Longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p] \<in> nlists n A
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A\<rbrakk> \<Longrightarrow> distinct (map fst ps)
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A\<rbrakk> \<Longrightarrow> \<forall>(pa, xa)\<in>set ps. pa < length (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) \<and> xa \<in> A
 4. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 5. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (blast intro!: nlistsE_set intro: closedD nlistsE_length [THEN nth_in]
                            Semilat.closed_f[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A\<rbrakk> \<Longrightarrow> distinct (map fst ps)
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A\<rbrakk> \<Longrightarrow> \<forall>(pa, xa)\<in>set ps. pa < length (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) \<and> xa \<in> A
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 4. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A\<rbrakk> \<Longrightarrow> \<forall>(pa, xa)\<in>set ps. pa < length (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) \<and> xa \<in> A
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply(intro strip)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x ps xs xa. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; xa \<in> set ps\<rbrakk> \<Longrightarrow> case xa of (pa, xa) \<Rightarrow> pa < length (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) \<and> xa \<in> A
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p \<and> (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x ps xs a b. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (erule allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps; ?xs57 p x ps xs a b \<in> nlists n A \<longrightarrow> (merges f ps (?xs57 p x ps xs a b) = ?xs57 p x ps xs a b) = (\<forall>xa\<in>set ps. case xa of (pa, xa) \<Rightarrow> xa \<sqsubseteq>\<^bsub>r\<^esub> ?xs57 p x ps xs a b ! pa)\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps\<rbrakk> \<Longrightarrow> ?xs57 p x ps xs a b \<in> nlists n A
 2. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps; (merges f ps (?xs57 p x ps xs a b) = ?xs57 p x ps xs a b) = (\<forall>xa\<in>set ps. case xa of (pa, xa) \<Rightarrow> xa \<sqsubseteq>\<^bsub>r\<^esub> ?xs57 p x ps xs a b ! pa)\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps; (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (drule bspec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps; (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p)\<rbrakk> \<Longrightarrow> ?x62 p x ps xs a b \<in> set ps
 2. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps; (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); case ?x62 p x ps xs a b of (p, x) \<Rightarrow> p < n \<and> x \<in> A\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a
 3. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); p < n; x \<in> A; merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps; (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); case (a, b) of (p, x) \<Rightarrow> p < n \<and> x \<in> A\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (simp add: Semilat.le_iff_plus_unchanged [OF Semilat.intro, OF is_semi, THEN iffD1] list_update_same_conv [THEN iffD2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x ps xs a b. \<lbrakk>xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); p < n; x \<in> A; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; (a, b) \<in> set ps; merges f ps xs = xs; a < n \<and> b \<in> A\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> xs ! a
 2. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p x ps xs. \<lbrakk>\<forall>xs. xs \<in> nlists n A \<longrightarrow> (merges f ps xs = xs) = (\<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p); xs \<in> nlists n A; p \<notin> fst ` set ps; distinct (map fst ps); \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> p < n \<and> x \<in> A; p < n; x \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p; \<forall>x\<in>set ps. case x of (p, x) \<Rightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> xs ! p\<rbrakk> \<Longrightarrow> merges f ps (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) = xs
[PROOF STEP]
apply (simp add: Semilat.le_iff_plus_unchanged[OF Semilat.intro, OF is_semi, THEN iffD1] list_update_same_conv [THEN iffD2])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  (in Semilat)list_update_le_listI [rule_format]:
  "set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> xs [\<sqsubseteq>\<^sub>r] ys \<longrightarrow> p < size xs \<longrightarrow>
   x \<sqsubseteq>\<^sub>r ys!p \<longrightarrow> x\<in>A \<longrightarrow>
   xs[p := x \<squnion>\<^sub>f xs!p] [\<sqsubseteq>\<^sub>r] ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<longrightarrow> p < length xs \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> ys ! p \<longrightarrow> x \<in> A \<longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p] [\<sqsubseteq>\<^bsub>r\<^esub>] ys
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<longrightarrow> p < length xs \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> ys ! p \<longrightarrow> x \<in> A \<longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p] [\<sqsubseteq>\<^bsub>r\<^esub>] ys
[PROOF STEP]
apply (insert semilat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (A, r, f) \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<longrightarrow> p < length xs \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> ys ! p \<longrightarrow> x \<in> A \<longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p] [\<sqsubseteq>\<^bsub>r\<^esub>] ys
[PROOF STEP]
apply (simp only: Listn.le_def lesub_def semilat_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (A, r, f) of (A, r, f) \<Rightarrow> order r A \<and> closed A f \<and> (\<forall>x\<in>A. \<forall>y\<in>A. r x (x \<squnion>\<^bsub>f\<^esub> y)) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. r y (x \<squnion>\<^bsub>f\<^esub> y)) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. r x z \<and> r y z \<longrightarrow> r (x \<squnion>\<^bsub>f\<^esub> y) z) \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> list_all2 r xs ys \<longrightarrow> p < length xs \<longrightarrow> r x (ys ! p) \<longrightarrow> x \<in> A \<longrightarrow> list_all2 r (xs[p := x \<squnion>\<^bsub>f\<^esub> xs ! p]) ys
[PROOF STEP]
apply (simp add: list_all2_conv_all_nth nth_list_update)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Semilat) merges_pres_le_ub:
  assumes "set ts \<subseteq> A"
          "set ss \<subseteq> A"
          "\<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p < size ts"
          "ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
  shows "merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
fix t ts ps
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
have
    "\<And>qs. \<lbrakk>set ts \<subseteq> A; \<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
          set qs \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>qs. \<lbrakk>set ts \<subseteq> A; \<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts\<rbrakk> \<Longrightarrow> set qs \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
apply (induct_tac qs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>qs. \<lbrakk>set ts \<subseteq> A; \<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts\<rbrakk> \<Longrightarrow> set [] \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f [] ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 2. \<And>qs a list. \<lbrakk>set ts \<subseteq> A; \<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts; set list \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f list ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)\<rbrakk> \<Longrightarrow> set (a # list) \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f (a # list) ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>qs a list. \<lbrakk>set ts \<subseteq> A; \<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts; set list \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f list ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)\<rbrakk> \<Longrightarrow> set (a # list) \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f (a # list) ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
apply (simp (no_asm_simp))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>set ts \<subseteq> A; \<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts; set list \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f list ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)\<rbrakk> \<Longrightarrow> a \<in> set ps \<and> set list \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> (case a of (p, \<tau>) \<Rightarrow> merges f list (ss[p := \<tau> \<squnion>\<^bsub>f\<^esub> ss ! p])) [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; \<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; \<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f list ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> merges f list (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]) [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; \<forall>x\<in>set ps. case x of (p, t) \<Rightarrow> t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ss; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; \<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f list ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> merges f list (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]) [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
apply (erule allE, erule impE, erule_tac [2] mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; \<forall>x\<in>set ps. case x of (p, t) \<Rightarrow> t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ss; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> set (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]) \<subseteq> A
 2. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; \<forall>x\<in>set ps. case x of (p, t) \<Rightarrow> t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ss; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
apply (drule bspec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; case (a, b) of (p, t) \<Rightarrow> t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ss\<rbrakk> \<Longrightarrow> set (ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a]) \<subseteq> A
 2. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; \<forall>x\<in>set ps. case x of (p, t) \<Rightarrow> t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ss; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
apply (simp add: closedD  Semilat.closed_f)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; \<forall>x\<in>set ps. case x of (p, t) \<Rightarrow> t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ss; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
apply (drule bspec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; case (a, b) of (p, t) \<Rightarrow> t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ss\<rbrakk> \<Longrightarrow> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
apply (simp )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a \<and> b \<in> A \<and> a < length ss\<rbrakk> \<Longrightarrow> ss[a := b \<squnion>\<^bsub>f\<^esub> ss ! a] [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
apply(rule list_update_le_listI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a \<and> b \<in> A \<and> a < length ss\<rbrakk> \<Longrightarrow> set ss \<subseteq> A
 2. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a \<and> b \<in> A \<and> a < length ss\<rbrakk> \<Longrightarrow> set ts \<subseteq> A
 3. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a \<and> b \<in> A \<and> a < length ss\<rbrakk> \<Longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
 4. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a \<and> b \<in> A \<and> a < length ss\<rbrakk> \<Longrightarrow> a < length ss
 5. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a \<and> b \<in> A \<and> a < length ss\<rbrakk> \<Longrightarrow> b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a
 6. \<And>a b list ss. \<lbrakk>set ts \<subseteq> A; (a, b) \<in> set ps; set list \<subseteq> set ps; set ss \<subseteq> A; ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts; b \<sqsubseteq>\<^bsub>r\<^esub> ts ! a \<and> b \<in> A \<and> a < length ss\<rbrakk> \<Longrightarrow> b \<in> A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>set ts \<subseteq> A; \<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts\<rbrakk> \<Longrightarrow> set ?qs \<subseteq> set ps \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f ?qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)

goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>set ?tsa3 \<subseteq> A; \<forall>(p, t)\<in>set ?psa3. t \<sqsubseteq>\<^bsub>r\<^esub> ?tsa3 ! p \<and> t \<in> A \<and> p < length ?tsa3\<rbrakk> \<Longrightarrow> set ?qs \<subseteq> set ?psa3 \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ?tsa3 \<longrightarrow> merges f ?qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ?tsa3)

goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
note this [dest]
[PROOF STATE]
proof (state)
this:
\<lbrakk>set ?tsa3 \<subseteq> A; \<forall>(p, t)\<in>set ?psa3. t \<sqsubseteq>\<^bsub>r\<^esub> ?tsa3 ! p \<and> t \<in> A \<and> p < length ?tsa3\<rbrakk> \<Longrightarrow> set ?qs \<subseteq> set ?psa3 \<longrightarrow> (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ?tsa3 \<longrightarrow> merges f ?qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ?tsa3)

goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
set ts \<subseteq> A
set ss \<subseteq> A
\<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set ts \<subseteq> A
set ss \<subseteq> A
\<forall>(p, t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts ! p \<and> t \<in> A \<and> p < length ts
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts

goal (1 subgoal):
 1. merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_exec: "bounded step n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded step n
[PROOF STEP]
apply (insert is_semi,unfold semilat_def bounded_def step_def exec_def transf_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (A, r, f) of (A, r, f) \<Rightarrow> order r A \<and> closed A f \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> x \<squnion>\<^bsub>f\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> x \<squnion>\<^bsub>f\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z \<longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<sqsubseteq>\<^bsub>r\<^esub> z) \<Longrightarrow> \<forall>p<n. \<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (map (\<lambda>pc. (pc, p # \<tau>)) (rev (sorted_list_of_set (succs p)))). q < n
[PROOF STEP]
by (auto simp add: n_def nodes_def verts_set fin_succs' succ_range)