kings-crown/FVELER_Isabelle huggingface dataset:
theory FastMap

lemma map_of_lookups:
  "m = map_of binds \<and> distinct (map fst binds) \<Longrightarrow>
   list_all (\<lambda>(k, v). m k = Some v) binds" apply (induct binds) apply simp apply (force simp: list_all_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m = map_of binds \<and> distinct (map fst binds) \<Longrightarrow> list_all (\<lambda>(k, v). m k = Some v) binds proof (prove)
goal (2 subgoals):
 1. m = map_of [] \<and> distinct (map fst []) \<Longrightarrow> list_all (\<lambda>(k, v). m k = Some v) []
 2. \<And>a binds. \<lbrakk>m = map_of binds \<and> distinct (map fst binds) \<Longrightarrow> list_all (\<lambda>(k, v). m k = Some v) binds; m = map_of (a # binds) \<and> distinct (map fst (a # binds))\<rbrakk> \<Longrightarrow> list_all (\<lambda>(k, v). m k = Some v) (a # binds) proof (prove)
goal (1 subgoal):
 1. \<And>a binds. \<lbrakk>m = map_of binds \<and> distinct (map fst binds) \<Longrightarrow> list_all (\<lambda>(k, v). m k = Some v) binds; m = map_of (a # binds) \<and> distinct (map fst (a # binds))\<rbrakk> \<Longrightarrow> list_all (\<lambda>(k, v). m k = Some v) (a # binds) proof (prove)
goal:
No subgoals!
theory FastMap

lemma map_of_rev:
  "distinct (map fst binds) \<Longrightarrow>
   map_of (rev binds) = map_of binds" apply (subgoal_tac "distinct (map fst (rev binds))") apply (rule ext) apply (induct binds) apply simp apply (force simp: map_add_def split: option.splits) apply (metis distinct_rev rev_map) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (map fst binds) \<Longrightarrow> map_of (rev binds) = map_of binds proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct (map fst binds); distinct (map fst (rev binds))\<rbrakk> \<Longrightarrow> map_of (rev binds) = map_of binds
 2. distinct (map fst binds) \<Longrightarrow> distinct (map fst (rev binds)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct (map fst binds); distinct (map fst (rev binds))\<rbrakk> \<Longrightarrow> map_of (rev binds) x = map_of binds x
 2. distinct (map fst binds) \<Longrightarrow> distinct (map fst (rev binds)) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>distinct (map fst []); distinct (map fst (rev []))\<rbrakk> \<Longrightarrow> map_of (rev []) x = map_of [] x
 2. \<And>a binds x. \<lbrakk>\<And>x. \<lbrakk>distinct (map fst binds); distinct (map fst (rev binds))\<rbrakk> \<Longrightarrow> map_of (rev binds) x = map_of binds x; distinct (map fst (a # binds)); distinct (map fst (rev (a # binds)))\<rbrakk> \<Longrightarrow> map_of (rev (a # binds)) x = map_of (a # binds) x
 3. distinct (map fst binds) \<Longrightarrow> distinct (map fst (rev binds)) proof (prove)
goal (2 subgoals):
 1. \<And>a binds x. \<lbrakk>\<And>x. \<lbrakk>distinct (map fst binds); distinct (map fst (rev binds))\<rbrakk> \<Longrightarrow> map_of (rev binds) x = map_of binds x; distinct (map fst (a # binds)); distinct (map fst (rev (a # binds)))\<rbrakk> \<Longrightarrow> map_of (rev (a # binds)) x = map_of (a # binds) x
 2. distinct (map fst binds) \<Longrightarrow> distinct (map fst (rev binds)) proof (prove)
goal (1 subgoal):
 1. distinct (map fst binds) \<Longrightarrow> distinct (map fst (rev binds)) proof (prove)
goal:
No subgoals!
theory FastMap

lemma list_all_dest:
  "list_all P [(x, y)] \<equiv> P (x, y)"
  "list_all P ((x, y) # z # xs) \<equiv> (P (x, y) \<and> list_all P (z # xs))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (list_all P [(x, y)] \<equiv> P (x, y)) &&& list_all P ((x, y) # z # xs) \<equiv> P (x, y) \<and> list_all P (z # xs)
theory FastMap

lemma lookup_tree_simps':
  "lookup_tree key Leaf x = None"
  "key x = key k \<Longrightarrow> lookup_tree key (Node k v l r) x = Some v"
  "key x < key k \<Longrightarrow> lookup_tree key (Node k v l r) x = lookup_tree key l x"
  "key x > key k \<Longrightarrow> lookup_tree key (Node k v l r) x = lookup_tree key r x" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lookup_tree key Leaf x = None &&& (key x = key k \<Longrightarrow> lookup_tree key (Node k v l r) x = Some v)) &&& (key x < key k \<Longrightarrow> lookup_tree key (Node k v l r) x = lookup_tree key l x) &&& (key k < key x \<Longrightarrow> lookup_tree key (Node k v l r) x = lookup_tree key r x)
theory FP_Eval

lemma bool_prop_eq_True:
  "Trueprop P \<equiv> (P \<equiv> True)" by (simp add: atomize_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<equiv> (P \<equiv> True)
theory FP_Eval

lemma bool_prop_eq_False:
  "Trueprop (\<not>P) \<equiv> (P \<equiv> False)" by (simp add: atomize_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> P \<equiv> (P \<equiv> False)
theory FP_Eval

lemma (in FP_Eval) let_weak_cong':
  "a = b \<Longrightarrow> Let a t = Let b t" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a = b \<Longrightarrow> Let a t = Let b t
theory RangeMap

lemma map_of_to_lookup_map_of:
  "map_of kvs = map_option snd o lookup_map_of (=) kvs" by (induct kvs; auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_of kvs = map_option snd \<circ> lookup_map_of (=) kvs
theory RangeMap

lemma lookup_map_of_Some:
  "lookup_map_of eq kvs k = Some (k', v') \<Longrightarrow> (k', v') \<in> set kvs \<and> eq k' k" by (induct kvs; fastforce split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_map_of eq kvs k = Some (k', v') \<Longrightarrow> (k', v') \<in> set kvs \<and> eq k' k
theory RangeMap

lemma lookup_map_of_None:
  "lookup_map_of eq kvs k = None \<Longrightarrow> \<forall>(k', v') \<in> set kvs. \<not> eq k' k" by (induct kvs; fastforce split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_map_of eq kvs k = None \<Longrightarrow> \<forall>(k', v')\<in>set kvs. \<not> eq k' k
theory RangeMap

lemma list_pairwise_snoc:
  "list_pairwise P (xs @ [x]) = ((\<forall>y \<in> set xs. P y x) \<and> list_pairwise P xs)" by (induct xs; auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_pairwise P (xs @ [x]) = ((\<forall>y\<in>set xs. P y x) \<and> list_pairwise P xs)
theory RangeMap

lemma list_pairwise_append:
  "list_pairwise P (xs @ ys) =
   (list_pairwise P xs \<and> list_pairwise P ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. P x y))" by (induct xs; auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_pairwise P (xs @ ys) = (list_pairwise P xs \<and> list_pairwise P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y))
theory RangeMap

lemma index_rev_rev_eq:
  fixes i :: nat and n :: nat
  shows "i < n \<Longrightarrow> n - (n - i - 1) - 1 = i" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> n - (n - i - 1) - 1 = i
theory RangeMap

lemma list_pairwise_rev:
  "list_pairwise P (rev xs) = list_pairwise (swp P) xs" apply (simp add: list_pairwise_as_indices swp_def) apply (case_tac "xs = []") apply simp apply (rule iffI) apply (intro allI impI) apply (drule_tac x="length xs - j - 1" in spec, drule_tac x="length xs - i - 1" in spec) apply (clarsimp simp: rev_nth) apply (clarsimp simp: rev_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_pairwise P (rev xs) = list_pairwise (swp P) xs proof (prove)
goal (1 subgoal):
 1. (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j)) = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)) proof (prove)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j)) = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i))
 2. xs \<noteq> [] \<Longrightarrow> (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j)) = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)) proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j)) = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xs \<noteq> []; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j)\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)
 2. \<lbrakk>xs \<noteq> []; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j) proof (prove)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>xs \<noteq> []; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j); i < j \<and> j < length xs\<rbrakk> \<Longrightarrow> P (xs ! j) (xs ! i)
 2. \<lbrakk>xs \<noteq> []; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j) proof (prove)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>xs \<noteq> []; i < j \<and> j < length xs; length xs - j - 1 < length xs - i - 1 \<and> length xs - i - 1 < length xs \<longrightarrow> P (rev xs ! (length xs - j - 1)) (rev xs ! (length xs - i - 1))\<rbrakk> \<Longrightarrow> P (xs ! j) (xs ! i)
 2. \<lbrakk>xs \<noteq> []; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> []; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! j) (xs ! i)\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (rev xs ! i) (rev xs ! j) proof (prove)
goal:
No subgoals!
theory RangeMap

lemma list_pairwise_imp:
  "\<lbrakk> \<And>i j. \<lbrakk> i < j; P (xs ! i) (xs ! j) \<rbrakk> \<Longrightarrow> Q (xs ! i) (xs ! j) \<rbrakk> \<Longrightarrow>
   list_pairwise P xs \<Longrightarrow> list_pairwise Q xs" by (simp add: list_pairwise_as_indices)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i j. \<lbrakk>i < j; P (xs ! i) (xs ! j)\<rbrakk> \<Longrightarrow> Q (xs ! i) (xs ! j); list_pairwise P xs\<rbrakk> \<Longrightarrow> list_pairwise Q xs
theory RangeMap

lemma list_pairwise_imp_weak:
  "\<lbrakk> \<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs; P x y \<rbrakk> \<Longrightarrow> Q x y \<rbrakk> \<Longrightarrow>
   list_pairwise P xs \<Longrightarrow> list_pairwise Q xs" by (simp add: list_pairwise_as_indices)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs; P x y\<rbrakk> \<Longrightarrow> Q x y; list_pairwise P xs\<rbrakk> \<Longrightarrow> list_pairwise Q xs
theory RangeMap

lemma list_pairwise_commute:
  "symp P \<Longrightarrow> list_pairwise P (xs @ ys) = list_pairwise P (ys @ xs)" by (fastforce simp: list_pairwise_append symp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. symp P \<Longrightarrow> list_pairwise P (xs @ ys) = list_pairwise P (ys @ xs)
theory RangeMap

lemma ran_lookup_map_of_disjoint:
  "ran (lookup_map_of eq []) = {}"
  "\<forall>(k', v') \<in> set kvs. \<forall>x. eq k x \<longrightarrow> \<not>eq k' x
   \<Longrightarrow> ran (lookup_map_of eq ((k, v)#kvs)) =
         (if Collect (eq k) \<noteq> {} then {(k, v)} else {})
         \<union> ran (lookup_map_of eq kvs)" apply simp apply (subst ran_lookup_map_of) apply (clarsimp simp: restrict_map_def pred_neg_def) apply (rule arg_cong[where f="insert _"]) apply (force simp: ran_def dest: lookup_map_of_Some) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran (lookup_map_of eq []) = {} &&& (\<forall>(k', v')\<in>set kvs. \<forall>x. eq k x \<longrightarrow> \<not> eq k' x \<Longrightarrow> ran (lookup_map_of eq ((k, v) # kvs)) = (if Collect (eq k) \<noteq> {} then {(k, v)} else {}) \<union> ran (lookup_map_of eq kvs)) proof (prove)
goal (1 subgoal):
 1. \<forall>(k', v')\<in>set kvs. \<forall>x. eq k x \<longrightarrow> \<not> eq k' x \<Longrightarrow> ran (lookup_map_of eq ((k, v) # kvs)) = (if Collect (eq k) \<noteq> {} then {(k, v)} else {}) \<union> ran (lookup_map_of eq kvs) proof (prove)
goal (1 subgoal):
 1. \<forall>(k', v')\<in>set kvs. \<forall>x. eq k x \<longrightarrow> \<not> eq k' x \<Longrightarrow> (if Collect (eq k) \<noteq> {} then {(k, v)} else {}) \<union> ran (lookup_map_of eq kvs |` Collect (not eq k)) = (if Collect (eq k) \<noteq> {} then {(k, v)} else {}) \<union> ran (lookup_map_of eq kvs) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>set kvs. case x of (k', v') \<Rightarrow> \<forall>x. eq k x \<longrightarrow> \<not> eq k' x; eq k x\<rbrakk> \<Longrightarrow> insert (k, v) (ran (\<lambda>x. if \<not> eq k x then lookup_map_of eq kvs x else None)) = insert (k, v) (ran (lookup_map_of eq kvs)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>set kvs. case x of (k', v') \<Rightarrow> \<forall>x. eq k x \<longrightarrow> \<not> eq k' x; eq k x\<rbrakk> \<Longrightarrow> ran (\<lambda>x. if \<not> eq k x then lookup_map_of eq kvs x else None) = ran (lookup_map_of eq kvs) proof (prove)
goal:
No subgoals!
theory RangeMap

lemma Collect_in_range_atLeastLessThan[simp]:
  "Collect (in_range r) = {fst r ..< snd r}" by (cases r; fastforce simp: in_range.simps ord_class.atLeastLessThan_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Collect (in_range r) = {fst r..<snd r}
theory RangeMap

lemma range_map_of_SomeD:
  "range_map_of kvs k = Some ((start, end), v) \<Longrightarrow>
   ((start, end), v) \<in> set kvs \<and> start \<le> k \<and> k < end" by (fastforce simp: in_range.simps dest: range_map_of_Some')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_map_of kvs k = Some ((start, end), v) \<Longrightarrow> ((start, end), v) \<in> set kvs \<and> start \<le> k \<and> k < end
theory RangeMap

lemma monotonic_key_ranges_disjoint:
  "monotonic_key_ranges kvs \<Longrightarrow> disjoint_key_ranges kvs" apply (simp add: monotonic_key_ranges_alt_def
                   disjoint_key_ranges_def lookup_map_disjoint_keys_def disjnt_def) apply (induct kvs; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monotonic_key_ranges kvs \<Longrightarrow> disjoint_key_ranges kvs proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>((start, end), uu_). start \<le> end) kvs \<and> list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') kvs \<Longrightarrow> list_pairwise (\<lambda>(k, uu_) (k', uu_). fst k < snd k' \<longrightarrow> fst k' < snd k \<longrightarrow> fst k < snd k \<longrightarrow> \<not> fst k' < snd k') kvs proof (prove)
goal:
No subgoals!
theory RangeMap

lemma lookup_range_tree_valid_empty:
  "lookup_range_tree_valid tree = (True, None) \<Longrightarrow> tree = Leaf" apply (induct tree) apply simp apply (fastforce split: prod.splits option.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_range_tree_valid tree = (True, None) \<Longrightarrow> tree = Leaf proof (prove)
goal (2 subgoals):
 1. lookup_range_tree_valid Leaf = (True, None) \<Longrightarrow> Leaf = Leaf
 2. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>lookup_range_tree_valid tree1 = (True, None) \<Longrightarrow> tree1 = Leaf; lookup_range_tree_valid tree2 = (True, None) \<Longrightarrow> tree2 = Leaf; lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2) = (True, None)\<rbrakk> \<Longrightarrow> Node x1 x2 x3 tree1 tree2 = Leaf proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>lookup_range_tree_valid tree1 = (True, None) \<Longrightarrow> tree1 = Leaf; lookup_range_tree_valid tree2 = (True, None) \<Longrightarrow> tree2 = Leaf; lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2) = (True, None)\<rbrakk> \<Longrightarrow> Node x1 x2 x3 tree1 tree2 = Leaf proof (prove)
goal:
No subgoals!
theory RangeMap

lemma lookup_range_tree_valid_range:
  "lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow> low \<le> high" apply (induct tree arbitrary: low high) apply simp apply (fastforce split: prod.splits option.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow> low \<le> high proof (prove)
goal (2 subgoals):
 1. \<And>low high. lookup_range_tree_valid Leaf = (True, Some (low, high)) \<Longrightarrow> low \<le> high
 2. \<And>x1 x2 x3 tree1 tree2 low high. \<lbrakk>\<And>low high. lookup_range_tree_valid tree1 = (True, Some (low, high)) \<Longrightarrow> low \<le> high; \<And>low high. lookup_range_tree_valid tree2 = (True, Some (low, high)) \<Longrightarrow> low \<le> high; lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2) = (True, Some (low, high))\<rbrakk> \<Longrightarrow> low \<le> high proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2 low high. \<lbrakk>\<And>low high. lookup_range_tree_valid tree1 = (True, Some (low, high)) \<Longrightarrow> low \<le> high; \<And>low high. lookup_range_tree_valid tree2 = (True, Some (low, high)) \<Longrightarrow> low \<le> high; lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2) = (True, Some (low, high))\<rbrakk> \<Longrightarrow> low \<le> high proof (prove)
goal:
No subgoals!
theory RangeMap

lemma lookup_range_tree_valid_in_range:
  "lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow>
   lookup_range_tree tree k = Some ((start, end), v) \<Longrightarrow>
   in_range (start, end) k \<and> low \<le> start \<and> end \<le> high" apply (induct tree arbitrary: k v low high) apply simp apply (fastforce simp: in_range.simps
                   split: prod.splits option.splits if_split_asm
                   dest: lookup_range_tree_valid_empty lookup_range_tree_valid_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_range_tree_valid tree = (True, Some (low, high)); lookup_range_tree tree k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high proof (prove)
goal (2 subgoals):
 1. \<And>k v low high. \<lbrakk>lookup_range_tree_valid Leaf = (True, Some (low, high)); lookup_range_tree Leaf k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high
 2. \<And>x1 x2 x3 tree1 tree2 k v low high. \<lbrakk>\<And>k v low high. \<lbrakk>lookup_range_tree_valid tree1 = (True, Some (low, high)); lookup_range_tree tree1 k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high; \<And>k v low high. \<lbrakk>lookup_range_tree_valid tree2 = (True, Some (low, high)); lookup_range_tree tree2 k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high; lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2) = (True, Some (low, high)); lookup_range_tree (Node x1 x2 x3 tree1 tree2) k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2 k v low high. \<lbrakk>\<And>k v low high. \<lbrakk>lookup_range_tree_valid tree1 = (True, Some (low, high)); lookup_range_tree tree1 k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high; \<And>k v low high. \<lbrakk>lookup_range_tree_valid tree2 = (True, Some (low, high)); lookup_range_tree tree2 k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high; lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2) = (True, Some (low, high)); lookup_range_tree (Node x1 x2 x3 tree1 tree2) k = Some ((start, end), v)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> low \<le> start \<and> end \<le> high proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>:000 :001 :002 :003 :004 :005. ?x974 :000 :001 :002 :003 :004 :005 True True \<equiv>\<^sup>? \<lambda>:000 :001 :002 :003 :004 :005. ?x957 :000 :001 :002 :003 :004 :005 True True
\<lambda>:000 :001 :002 :003 :004 :005. ?kb617 :000 :001 :002 :003 :004 :005 True True \<equiv>\<^sup>? \<lambda>:000 :001 :002 :003 :004 :005. ?k600 :000 :001 :002 :003 :004 :005 True True
theory RangeMap

lemma lookup_range_tree_valid_in_range_None:
  "lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow>
   \<not> in_range (low, high) k \<Longrightarrow>
   lookup_range_tree tree k = None" apply (erule contrapos_np) apply (fastforce simp: in_range.simps dest: lookup_range_tree_valid_in_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_range_tree_valid tree = (True, Some (low, high)); \<not> in_range (low, high) k\<rbrakk> \<Longrightarrow> lookup_range_tree tree k = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_range_tree_valid tree = (True, Some (low, high)); lookup_range_tree tree k \<noteq> None\<rbrakk> \<Longrightarrow> in_range (low, high) k proof (prove)
goal:
No subgoals!
theory RangeMap

lemma monotonic_ranges_each_valid:
  "monotonic_key_ranges xs \<Longrightarrow> ((start, end), v) \<in> set xs \<Longrightarrow> start \<le> end" by (fastforce simp: monotonic_key_ranges_alt_def list_all_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monotonic_key_ranges xs; ((start, end), v) \<in> set xs\<rbrakk> \<Longrightarrow> start \<le> end
theory RangeMap

lemma lookup_map_of_append_to_map_add:
  "lookup_map_of eq (xs @ ys) = lookup_map_of eq ys ++ lookup_map_of eq xs" unfolding map_add_def apply (induct xs) apply simp apply (rule ext) apply (clarsimp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_map_of eq (xs @ ys) = lookup_map_of eq ys ++ lookup_map_of eq xs proof (prove)
goal (1 subgoal):
 1. lookup_map_of eq (xs @ ys) = (\<lambda>x. case lookup_map_of eq xs x of None \<Rightarrow> lookup_map_of eq ys x | Some x \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. lookup_map_of eq ([] @ ys) = (\<lambda>x. case lookup_map_of eq [] x of None \<Rightarrow> lookup_map_of eq ys x | Some a \<Rightarrow> Some a)
 2. \<And>a xs. lookup_map_of eq (xs @ ys) = (\<lambda>x. case lookup_map_of eq xs x of None \<Rightarrow> lookup_map_of eq ys x | Some a \<Rightarrow> Some a) \<Longrightarrow> lookup_map_of eq ((a # xs) @ ys) = (\<lambda>x. case lookup_map_of eq (a # xs) x of None \<Rightarrow> lookup_map_of eq ys x | Some a \<Rightarrow> Some a) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. lookup_map_of eq (xs @ ys) = (\<lambda>x. case lookup_map_of eq xs x of None \<Rightarrow> lookup_map_of eq ys x | Some a \<Rightarrow> Some a) \<Longrightarrow> lookup_map_of eq ((a # xs) @ ys) = (\<lambda>x. case lookup_map_of eq (a # xs) x of None \<Rightarrow> lookup_map_of eq ys x | Some a \<Rightarrow> Some a) proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. lookup_map_of eq (xs @ ys) = (\<lambda>x. case lookup_map_of eq xs x of None \<Rightarrow> lookup_map_of eq ys x | Some a \<Rightarrow> Some a) \<Longrightarrow> lookup_map_of eq ((a # xs) @ ys) x = (case lookup_map_of eq (a # xs) x of None \<Rightarrow> lookup_map_of eq ys x | Some a \<Rightarrow> Some a) proof (prove)
goal:
No subgoals!
theory RangeMap

lemma lookup_map_of_append_cong:
  "\<lbrakk> lookup_map_of eq xs = lookup_map_of eq xs';
     lookup_map_of eq ys = lookup_map_of eq ys'
   \<rbrakk> \<Longrightarrow> lookup_map_of eq (xs @ ys) = lookup_map_of eq (xs' @ ys')" by (simp add: lookup_map_of_append_to_map_add)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_map_of eq xs = lookup_map_of eq xs'; lookup_map_of eq ys = lookup_map_of eq ys'\<rbrakk> \<Longrightarrow> lookup_map_of eq (xs @ ys) = lookup_map_of eq (xs' @ ys')