theory Invariants_H

lemma lookupAround2_char2:
  "(snd (lookupAround2 x s) = Some y) = (x < y \<and> s y \<noteq> None \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None))" apply (simp add: lookupAround2_def Let_def split_def o_def
              del: maybe_def
              split: option.splits) apply (simp add: o_def map_option_is_None [where f=fst, unfolded map_option_case]) apply (simp add: lookupAround_def Let_def) apply (rule conjI) apply fastforce apply clarsimp apply (rule iffI) apply (frule subst[where P="\<lambda>x. x \<in> y2" for y2, OF _ Min_in]) apply simp apply fastforce apply clarsimp apply (subst(asm) Min_gr_iff, simp, fastforce, simp(no_asm_use), fastforce) apply clarsimp apply (rule order_antisym) apply (fastforce intro: Min_le) apply (subst Min_ge_iff) apply simp apply fastforce apply clarsimp apply (rule ccontr, simp add: linorder_not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (snd (lookupAround2 x s) = Some y) = (x < y \<and> s y \<noteq> None \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)) proof (prove)
goal (1 subgoal):
 1. (maybe None (\<lambda>x. Some (fst x)) (snd (snd (lookupAround x s))) = Some y) = (x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)) proof (prove)
goal (1 subgoal):
 1. ((case snd (snd (lookupAround x s)) of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x)) = Some y) = (x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)) proof (prove)
goal (1 subgoal):
 1. ((\<forall>xa. xa \<in> dom s \<longrightarrow> \<not> x < xa) \<longrightarrow> x < y \<longrightarrow> s y = None \<or> (\<exists>z>x. z < y \<and> (\<exists>y. s z = Some y))) \<and> ((\<exists>xa. xa \<in> dom s \<and> x < xa) \<longrightarrow> (Min {k \<in> dom s. x < k} = y) = (x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None))) proof (prove)
goal (2 subgoals):
 1. (\<forall>xa. xa \<in> dom s \<longrightarrow> \<not> x < xa) \<longrightarrow> x < y \<longrightarrow> s y = None \<or> (\<exists>z>x. z < y \<and> (\<exists>y. s z = Some y))
 2. (\<exists>xa. xa \<in> dom s \<and> x < xa) \<longrightarrow> (Min {k \<in> dom s. x < k} = y) = (x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)) proof (prove)
goal (1 subgoal):
 1. (\<exists>xa. xa \<in> dom s \<and> x < xa) \<longrightarrow> (Min {k \<in> dom s. x < k} = y) = (x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)) proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya\<rbrakk> \<Longrightarrow> (Min {k \<in> dom s. x < k} = y) = (x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)) proof (prove)
goal (2 subgoals):
 1. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; Min {k \<in> dom s. x < k} = y\<rbrakk> \<Longrightarrow> x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)
 2. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} = y proof (prove)
goal (4 subgoals):
 1. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; Min {k \<in> dom s. x < k} = y\<rbrakk> \<Longrightarrow> finite {k \<in> dom s. x < k}
 2. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; Min {k \<in> dom s. x < k} = y\<rbrakk> \<Longrightarrow> {k \<in> dom s. x < k} \<noteq> {}
 3. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; Min {k \<in> dom s. x < k} = y; y \<in> {k \<in> dom s. x < k}\<rbrakk> \<Longrightarrow> x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)
 4. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} = y proof (prove)
goal (3 subgoals):
 1. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; Min {k \<in> dom s. x < k} = y\<rbrakk> \<Longrightarrow> {k \<in> dom s. x < k} \<noteq> {}
 2. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; Min {k \<in> dom s. x < k} = y; y \<in> {k \<in> dom s. x < k}\<rbrakk> \<Longrightarrow> x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)
 3. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} = y proof (prove)
goal (2 subgoals):
 1. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; Min {k \<in> dom s. x < k} = y; y \<in> {k \<in> dom s. x < k}\<rbrakk> \<Longrightarrow> x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)
 2. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} = y proof (prove)
goal (2 subgoals):
 1. \<And>xa ya yaa z. \<lbrakk>x < xa; s xa = Some ya; y = Min {k \<in> dom s. x < k}; x < Min {k \<in> dom s. x < k}; s (Min {k \<in> dom s. x < k}) = Some yaa; x < z; z < Min {k \<in> dom s. x < k}\<rbrakk> \<Longrightarrow> s z = None
 2. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} = y proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. \<lbrakk>x < xa; s xa = Some ya; x < y \<and> (\<exists>ya. s y = Some ya) \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} = y proof (prove)
goal (1 subgoal):
 1. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} = y proof (prove)
goal (2 subgoals):
 1. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> Min {k \<in> dom s. x < k} \<le> y
 2. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> y \<le> Min {k \<in> dom s. x < k} proof (prove)
goal (1 subgoal):
 1. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> y \<le> Min {k \<in> dom s. x < k} proof (prove)
goal (3 subgoals):
 1. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> finite {k \<in> dom s. x < k}
 2. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> {k \<in> dom s. x < k} \<noteq> {}
 3. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> Ball {k \<in> dom s. x < k} ((\<le>) y) proof (prove)
goal (2 subgoals):
 1. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> {k \<in> dom s. x < k} \<noteq> {}
 2. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> Ball {k \<in> dom s. x < k} ((\<le>) y) proof (prove)
goal (1 subgoal):
 1. \<And>xa ya yaa. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa\<rbrakk> \<Longrightarrow> Ball {k \<in> dom s. x < k} ((\<le>) y) proof (prove)
goal (1 subgoal):
 1. \<And>xa ya yaa xaa yb. \<lbrakk>x < xa; s xa = Some ya; x < y; \<forall>z. x < z \<and> z < y \<longrightarrow> s z = None; s y = Some yaa; x < xaa; s xaa = Some yb\<rbrakk> \<Longrightarrow> y \<le> xaa proof (prove)
goal:
No subgoals!