kings-crown/FVELER_Isabelle huggingface dataset:
theory RangeMap

lemma lookup_map_of_append1_commute:
  "lookup_map_disjoint_keys eq (xs @ [y]) \<Longrightarrow>
   lookup_map_of eq (xs @ [y]) = lookup_map_of eq ([y] @ xs)" apply (induct xs arbitrary: y) apply simp apply (rule ext) apply clarify apply (simp add: disjnt_def lookup_map_disjoint_keys_def flip: Collect_conj_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_map_disjoint_keys eq (xs @ [y]) \<Longrightarrow> lookup_map_of eq (xs @ [y]) = lookup_map_of eq ([y] @ xs) proof (prove)
goal (2 subgoals):
 1. \<And>y. lookup_map_disjoint_keys eq ([] @ [y]) \<Longrightarrow> lookup_map_of eq ([] @ [y]) = lookup_map_of eq ([y] @ [])
 2. \<And>a xs y. \<lbrakk>\<And>y. lookup_map_disjoint_keys eq (xs @ [y]) \<Longrightarrow> lookup_map_of eq (xs @ [y]) = lookup_map_of eq ([y] @ xs); lookup_map_disjoint_keys eq ((a # xs) @ [y])\<rbrakk> \<Longrightarrow> lookup_map_of eq ((a # xs) @ [y]) = lookup_map_of eq ([y] @ a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs y. \<lbrakk>\<And>y. lookup_map_disjoint_keys eq (xs @ [y]) \<Longrightarrow> lookup_map_of eq (xs @ [y]) = lookup_map_of eq ([y] @ xs); lookup_map_disjoint_keys eq ((a # xs) @ [y])\<rbrakk> \<Longrightarrow> lookup_map_of eq ((a # xs) @ [y]) = lookup_map_of eq ([y] @ a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs y x. \<lbrakk>\<And>y. lookup_map_disjoint_keys eq (xs @ [y]) \<Longrightarrow> lookup_map_of eq (xs @ [y]) = lookup_map_of eq ([y] @ xs); lookup_map_disjoint_keys eq ((a # xs) @ [y])\<rbrakk> \<Longrightarrow> lookup_map_of eq ((a # xs) @ [y]) x = lookup_map_of eq ([y] @ a # xs) x proof (prove)
goal (1 subgoal):
 1. \<And>a b xs aa ba x. \<lbrakk>\<And>a b. lookup_map_disjoint_keys eq (xs @ [(a, b)]) \<Longrightarrow> lookup_map_of eq (xs @ [(a, b)]) = lookup_map_of eq ([(a, b)] @ xs); lookup_map_disjoint_keys eq (((a, b) # xs) @ [(aa, ba)])\<rbrakk> \<Longrightarrow> lookup_map_of eq (((a, b) # xs) @ [(aa, ba)]) x = lookup_map_of eq ([(aa, ba)] @ (a, b) # xs) x proof (prove)
goal:
No subgoals!
theory RangeMap

lemma Cons_to_append:
  "x # xs = [x] @ xs" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x # xs = [x] @ xs
theory RangeMap

lemma map_add_alt_cond:
  "\<lbrakk>\<And>x. g x \<noteq> None \<Longrightarrow> \<not> cond x; \<And>x. f x \<noteq> None \<Longrightarrow> cond x\<rbrakk> \<Longrightarrow>
   f ++ g = (\<lambda>x. if cond x then f x else g x)" by (fastforce simp: map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. g x \<noteq> None \<Longrightarrow> \<not> cond x; \<And>x. f x \<noteq> None \<Longrightarrow> cond x\<rbrakk> \<Longrightarrow> f ++ g = (\<lambda>x. if cond x then f x else g x)
theory RangeMap

lemma map_add_alt_cond':
  "\<lbrakk>\<And>x. f x \<noteq> None \<Longrightarrow> \<not> cond x; \<And>x. g x \<noteq> None \<Longrightarrow> cond x\<rbrakk> \<Longrightarrow>
   f ++ g = (\<lambda>x. if cond x then g x else f x)" by (fastforce simp: map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. f x \<noteq> None \<Longrightarrow> \<not> cond x; \<And>x. g x \<noteq> None \<Longrightarrow> cond x\<rbrakk> \<Longrightarrow> f ++ g = (\<lambda>x. if cond x then g x else f x)
theory RangeMap

lemma fst_lookup_range_tree_validD:
  "fst (lookup_range_tree_valid (Node start end v l r)) \<Longrightarrow>
   fst (lookup_range_tree_valid l) \<and> fst (lookup_range_tree_valid r)" by (simp split: option.splits prod.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (lookup_range_tree_valid (Node start end v l r)) \<Longrightarrow> fst (lookup_range_tree_valid l) \<and> fst (lookup_range_tree_valid r)
theory RangeMap

lemma lookup_range_tree_Some:
  "lookup_range_tree tree k = Some ((start, end), v) \<Longrightarrow>
   fst (lookup_range_tree_valid tree) \<Longrightarrow>
   in_range (start, end) k
   \<and> (\<exists>low high. lookup_range_tree_valid tree = (True, Some (low, high))
                  \<and> low \<le> start \<and> end \<le> high)" apply (cases "lookup_range_tree_valid tree") apply clarsimp apply (rename_tac r, case_tac r) apply (fastforce dest: lookup_range_tree_valid_empty) apply (fastforce dest: lookup_range_tree_valid_in_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_range_tree tree k = Some ((start, end), v); fst (lookup_range_tree_valid tree)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> (\<exists>low high. lookup_range_tree_valid tree = (True, Some (low, high)) \<and> low \<le> start \<and> end \<le> high) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>lookup_range_tree tree k = Some ((start, end), v); fst (lookup_range_tree_valid tree); lookup_range_tree_valid tree = (a, b)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> (\<exists>low high. lookup_range_tree_valid tree = (True, Some (low, high)) \<and> low \<le> start \<and> end \<le> high) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>lookup_range_tree tree k = Some ((start, end), v); a; lookup_range_tree_valid tree = (True, b)\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> (\<exists>low high. b = Some (low, high) \<and> low \<le> start \<and> end \<le> high) proof (prove)
goal (2 subgoals):
 1. \<And>a r. \<lbrakk>lookup_range_tree tree k = Some ((start, end), v); a; lookup_range_tree_valid tree = (True, r); r = None\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> (\<exists>low high. r = Some (low, high) \<and> low \<le> start \<and> end \<le> high)
 2. \<And>a r aa. \<lbrakk>lookup_range_tree tree k = Some ((start, end), v); a; lookup_range_tree_valid tree = (True, r); r = Some aa\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> (\<exists>low high. r = Some (low, high) \<and> low \<le> start \<and> end \<le> high) proof (prove)
goal (1 subgoal):
 1. \<And>a r aa. \<lbrakk>lookup_range_tree tree k = Some ((start, end), v); a; lookup_range_tree_valid tree = (True, r); r = Some aa\<rbrakk> \<Longrightarrow> in_range (start, end) k \<and> (\<exists>low high. r = Some (low, high) \<and> low \<le> start \<and> end \<le> high) proof (prove)
goal:
No subgoals!
theory RangeMap

lemma lookup_range_tree_to_list_of_gen:
  "\<lbrakk> fst (lookup_range_tree_valid tree);
     lookup_range_tree_to_list tree = binds
   \<rbrakk> \<Longrightarrow> lookup_range_tree tree = range_map_of binds
         \<and> monotonic_key_ranges binds" using lookup_range_tree_to_list_of apply (fastforce dest: lookup_range_tree_list_monotonic) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (lookup_range_tree_valid tree); lookup_range_tree_to_list tree = binds\<rbrakk> \<Longrightarrow> lookup_range_tree tree = range_map_of binds \<and> monotonic_key_ranges binds proof (prove)
using this:
fst (lookup_range_tree_valid ?tree) \<Longrightarrow> lookup_range_tree ?tree = range_map_of (lookup_range_tree_to_list ?tree)

goal (1 subgoal):
 1. \<lbrakk>fst (lookup_range_tree_valid tree); lookup_range_tree_to_list tree = binds\<rbrakk> \<Longrightarrow> lookup_range_tree tree = range_map_of binds \<and> monotonic_key_ranges binds proof (prove)
goal:
No subgoals!
theory RangeMap

lemma Collect_in_range_rewrite:
  "Collect o in_range o fst = (\<lambda>((start, end), v). {start ..< end})" by (fastforce simp: in_range.simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Collect \<circ> in_range \<circ> fst = (\<lambda>((start, end), v). {start..<end})
theory RangeMap

lemma ran_add_if:
  "\<lbrakk> \<forall>x. P x \<longrightarrow> z x = None \<rbrakk>
   \<Longrightarrow> ran (\<lambda>x. if P x then y x else z x) = ran (y |` Collect P) \<union> ran z" by (auto simp: ran_def restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. P x \<longrightarrow> z x = None \<Longrightarrow> ran (\<lambda>x. if P x then y x else z x) = ran (y |` Collect P) \<union> ran z
theory RangeMap

lemma atLeastLessThan_union_contiguous:
  "\<lbrakk>(l::'a::linorder) \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> {l..<m} \<union> {m..<u} = {l..<u}"
  "\<lbrakk>(l::'a::linorder) \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> ({l..<m} \<union> {m..<u}) \<union> x = {l..<u} \<union> x"
  "\<lbrakk>(l::'a::linorder) \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> {l..<m} \<union> ({m..<u} \<union> x) = {l..<u} \<union> x" by (auto simp: ivl_disj_un)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>l \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> {l..<m} \<union> {m..<u} = {l..<u}) &&& (\<lbrakk>l \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> {l..<m} \<union> {m..<u} \<union> x = {l..<u} \<union> x) &&& (\<lbrakk>l \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> {l..<m} \<union> ({m..<u} \<union> x) = {l..<u} \<union> x)
theory RangeMap

lemma combine_contiguous_ranges_both:
  "combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs" apply (induct xs rule: length_induct) apply (case_tac xs) apply clarsimp apply (rename_tac xs') apply (case_tac xs') apply clarsimp apply (clarsimp split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys; xs = []\<rbrakk> \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs
 2. \<And>xs a list. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys; xs = a # list\<rbrakk> \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs proof (prove)
goal (1 subgoal):
 1. \<And>xs a list. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys; xs = a # list\<rbrakk> \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs proof (prove)
goal (1 subgoal):
 1. \<And>xs a xs'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys; xs = a # xs'\<rbrakk> \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs proof (prove)
goal (2 subgoals):
 1. \<And>xs a xs'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys; xs = a # xs'; xs' = []\<rbrakk> \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs
 2. \<And>xs a xs' aa list. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys; xs = a # xs'; xs' = aa # list\<rbrakk> \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs proof (prove)
goal (1 subgoal):
 1. \<And>xs a xs' aa list. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> combine_contiguous_ranges ys = combine_contiguous_ranges_rev ys; xs = a # xs'; xs' = aa # list\<rbrakk> \<Longrightarrow> combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs proof (prove)
goal:
No subgoals!
theory RangeMap

lemma lookup_map_of_single:
  "\<lbrakk> lookup_map_disjoint_keys eq binds;
     (k, v) \<in> set binds; eq k x \<rbrakk>
   \<Longrightarrow> lookup_map_of eq binds x = Some (k, v)" by (induct binds;
      fastforce simp: lookup_map_disjoint_keys_def disjnt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_map_disjoint_keys eq binds; (k, v) \<in> set binds; eq k x\<rbrakk> \<Longrightarrow> lookup_map_of eq binds x = Some (k, v)
theory RangeMap

lemma range_map_of_single':
  "\<lbrakk> disjoint_key_ranges binds;
     ((start, end), v) \<in> set binds; in_range (start, end) k \<rbrakk>
   \<Longrightarrow> range_map_of binds k = Some ((start, end), v)" unfolding range_map_of_def disjoint_key_ranges_def by (fastforce intro: lookup_map_of_single)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>disjoint_key_ranges binds; ((start, end), v) \<in> set binds; in_range (start, end) k\<rbrakk> \<Longrightarrow> range_map_of binds k = Some ((start, end), v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_map_disjoint_keys in_range binds; ((start, end), v) \<in> set binds; in_range (start, end) k\<rbrakk> \<Longrightarrow> lookup_map_of in_range binds k = Some ((start, end), v)
theory RangeMap

lemma range_map_of_lookups__gen_all':
  "\<lbrakk> m = range_map_of binds; disjoint_key_ranges binds \<rbrakk> \<Longrightarrow>
   list_all (\<lambda>((start, end), v). \<forall>k. in_range (start, end) k = (m k = Some ((start, end), v))) binds" by (fastforce simp: list_all_iff intro: range_map_of_single' dest: range_map_of_Some')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = range_map_of binds; disjoint_key_ranges binds\<rbrakk> \<Longrightarrow> list_all (\<lambda>((start, end), v). \<forall>k. in_range (start, end) k = (m k = Some ((start, end), v))) binds
theory RangeMap

lemma range_map_of_start:
  "\<lbrakk> disjoint_key_ranges binds; ((start, end), v) \<in> set binds; start < end \<rbrakk>
   \<Longrightarrow> range_map_of binds start = Some ((start, end), v)" by (fastforce simp: in_range.simps intro: range_map_of_single)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>disjoint_key_ranges binds; ((start, end), v) \<in> set binds; start < end\<rbrakk> \<Longrightarrow> range_map_of binds start = Some ((start, end), v)
theory RangeMap

lemma range_map_of_start_lookups__gen_all':
  "\<lbrakk> m = range_map_of binds; disjoint_key_ranges binds \<rbrakk> \<Longrightarrow>
   list_all (\<lambda>((start, end), v). start < end \<longrightarrow> m start = Some ((start, end), v)) binds" by (fastforce simp: list_all_iff intro: range_map_of_start)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = range_map_of binds; disjoint_key_ranges binds\<rbrakk> \<Longrightarrow> list_all (\<lambda>((start, end), v). start < end \<longrightarrow> m start = Some ((start, end), v)) binds
theory RangeMap

lemma hold_quote:
  "quote x = quote x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. quote x = quote x
theory RangeMap

lemma spec_FO:
  "All P \<Longrightarrow> P x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. All P \<Longrightarrow> P x
theory RangeMap

lemma lookup_range_tree_simps':
  "lookup_range_tree Leaf x = None"
  "\<lbrakk> start \<le> x; x < end \<rbrakk> \<Longrightarrow>
     lookup_range_tree (Node start end v l r) x = Some ((start, end), v)"
  "\<lbrakk> x < start \<rbrakk> \<Longrightarrow>
     lookup_range_tree (Node start end v l r) x = lookup_range_tree l x"
  "\<lbrakk> start \<le> end; end \<le> x \<rbrakk> \<Longrightarrow>
     lookup_range_tree (Node start end v l r) x = lookup_range_tree r x" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lookup_range_tree Leaf x = None &&& (\<lbrakk>start \<le> x; x < end\<rbrakk> \<Longrightarrow> lookup_range_tree (Node start end v l r) x = Some ((start, end), v))) &&& (x < start \<Longrightarrow> lookup_range_tree (Node start end v l r) x = lookup_range_tree l x) &&& (\<lbrakk>start \<le> end; end \<le> x\<rbrakk> \<Longrightarrow> lookup_range_tree (Node start end v l r) x = lookup_range_tree r x)
theory Eval_CAMKES_CDL

lemma split_Collect_graph_edge:
  "Collect P = Collect (\<lambda>(from, auth, to). P (from, auth, to))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Collect P = {(from, auth, to). P (from, auth, to)}
theory Eval_CAMKES_CDL

lemma Collect_graph_cong_helper:
  "(\<And>x y z. P x y z = P' x y z) \<Longrightarrow>
   Collect (\<lambda>(x, y, z). P x y z) = Collect (\<lambda>(x, y, z). P' x y z)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y z. P x y z = P' x y z) \<Longrightarrow> {(x, y, z). P x y z} = {(x, y, z). P' x y z}
theory Eval_CAMKES_CDL

lemma proj_Collect_prod:
  "fst ` {(a, b). f a b} = {a. \<exists>b. f a b}"
  "snd ` {(a, b). f a b} = {b. \<exists>a. f a b}" by force+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst ` {(a, b). f a b} = {a. \<exists>b. f a b} &&& snd ` {(a, b). f a b} = {b. \<exists>a. f a b}
theory Eval_CAMKES_CDL

lemma complete_graph_is_transitive[rotated 1, consumes 2]:
  "\<lbrakk> let edges = {(v, u). G v e u};
         verts = fst ` edges \<union> snd ` edges
     in \<forall>u \<in> verts. \<forall>v \<in> verts. G v e u;
     G u e v; G v e w \<rbrakk>
   \<Longrightarrow> G u e w" apply (simp (no_asm_use) add: proj_Collect_prod flip: Collect_disj_eq) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>let edges = {(v, u). G v e u}; verts = fst ` edges \<union> snd ` edges in \<forall>u\<in>verts. \<forall>v\<in>verts. G v e u; G u e v; G v e w\<rbrakk> \<Longrightarrow> G u e w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u. (Ex (G u e) \<longrightarrow> (\<forall>v. (Ex (G v e) \<longrightarrow> G v e u) \<and> ((\<exists>va. G va e v) \<longrightarrow> G v e u))) \<and> ((\<exists>v. G v e u) \<longrightarrow> (\<forall>v. (Ex (G v e) \<longrightarrow> G v e u) \<and> ((\<exists>va. G va e v) \<longrightarrow> G v e u))); G u e v; G v e w\<rbrakk> \<Longrightarrow> G u e w
theory Eval_CAMKES_CDL

lemma complete_graph_is_transitive'[rotated 1, consumes 2]:
  "\<lbrakk> let edges = {(v, u). G v e u};
         verts = fst ` edges \<union> snd ` edges
     in \<forall>u \<in> verts. \<forall>v \<in> verts. u \<noteq> v \<longrightarrow> G v e u;
     G u e v; G v e w; u \<noteq> v; v \<noteq> w; u \<noteq> w \<rbrakk>
   \<Longrightarrow> G u e w" apply (simp (no_asm_use) add: proj_Collect_prod flip: Collect_disj_eq) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>let edges = {(v, u). G v e u}; verts = fst ` edges \<union> snd ` edges in \<forall>u\<in>verts. \<forall>v\<in>verts. u \<noteq> v \<longrightarrow> G v e u; G u e v; G v e w; u \<noteq> v; v \<noteq> w; u \<noteq> w\<rbrakk> \<Longrightarrow> G u e w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u. (Ex (G u e) \<longrightarrow> (\<forall>v. (Ex (G v e) \<longrightarrow> u \<noteq> v \<longrightarrow> G v e u) \<and> ((\<exists>va. G va e v) \<longrightarrow> u \<noteq> v \<longrightarrow> G v e u))) \<and> ((\<exists>v. G v e u) \<longrightarrow> (\<forall>v. (Ex (G v e) \<longrightarrow> u \<noteq> v \<longrightarrow> G v e u) \<and> ((\<exists>va. G va e v) \<longrightarrow> u \<noteq> v \<longrightarrow> G v e u))); G u e v; G v e w; u \<noteq> v; v \<noteq> w; u \<noteq> w\<rbrakk> \<Longrightarrow> G u e w
theory Eval_CAMKES_CDL

lemma Collect_case_prod_dnf:
  "{(a, b). a = x \<and> b = y} = {(x, y)}"
  "{(a, b). a = x \<and> b = y \<or> P a b} = insert (x, y) {(a, b). P a b}"
  "{(a, b). b = y \<and> a = x} = set [(x, y)]"
  "{(a, b). b = y \<and> a = x \<or> P a b} = insert (x, y) {(a, b). P a b}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({(a, b). a = x \<and> b = y} = {(x, y)} &&& {(a, b). a = x \<and> b = y \<or> P a b} = insert (x, y) {(a, b). P a b}) &&& {(a, b). b = y \<and> a = x} = set [(x, y)] &&& {(a, b). b = y \<and> a = x \<or> P a b} = insert (x, y) {(a, b). P a b}
theory Eval_CAMKES_CDL

lemma ptr_range_in_range:
  "0 < (p :: 'a::len word) + 2^sz \<Longrightarrow>
   (x \<in> ptr_range p sz) = (RangeMap.in_range (p, p + 2^sz) x)" apply (simp add: ptr_range_def RangeMap.in_range.simps) apply uint_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < p + 2 ^ sz \<Longrightarrow> (x \<in> ptr_range p sz) = RangeMap.in_range (p, p + 2 ^ sz) x proof (prove)
goal (1 subgoal):
 1. 0 < p + 2 ^ sz \<Longrightarrow> (p \<le> x \<and> x \<le> p + 2 ^ sz - 1) = (p \<le> x \<and> x < p + 2 ^ sz) proof (prove)
goal:
No subgoals!
theory Eval_CAMKES_CDL

lemma fun_upds_to_map_of[THEN eq_reflection]:
  "Map.empty = map_of []"
  "((map_of xs)(k \<mapsto> v)) = map_of ((k, v) # xs)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. None) = map_of [] &&& (map_of xs)(k \<mapsto> v) = map_of ((k, v) # xs)
theory Eval_CAMKES_CDL

lemma subst_eqn_helper:
  "(\<And>s. s = t \<longrightarrow> P s) \<Longrightarrow> P t" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s = t \<longrightarrow> P s) \<Longrightarrow> P t
theory Eval_CAMKES_CDL

lemma iterate_labelling_helper:
  "\<lbrakk> m = map_of binds;
     distinct (map fst binds)
   \<rbrakk> \<Longrightarrow>
   (\<forall>obj label. m obj = Some label \<longrightarrow> label_of obj = label)
    = list_all (\<lambda>(k, v). label_of k = v) binds" apply (rule iffI) apply (blast intro: list_allI FastMap.map_of_lookups) apply (fastforce simp: list_all_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = map_of binds; distinct (map fst binds)\<rbrakk> \<Longrightarrow> (\<forall>obj label. m obj = Some label \<longrightarrow> label_of obj = label) = list_all (\<lambda>(k, v). label_of k = v) binds proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m = map_of binds; distinct (map fst binds); \<forall>obj label. m obj = Some label \<longrightarrow> label_of obj = label\<rbrakk> \<Longrightarrow> list_all (\<lambda>(k, v). label_of k = v) binds
 2. \<lbrakk>m = map_of binds; distinct (map fst binds); list_all (\<lambda>(k, v). label_of k = v) binds\<rbrakk> \<Longrightarrow> \<forall>obj label. m obj = Some label \<longrightarrow> label_of obj = label proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = map_of binds; distinct (map fst binds); list_all (\<lambda>(k, v). label_of k = v) binds\<rbrakk> \<Longrightarrow> \<forall>obj label. m obj = Some label \<longrightarrow> label_of obj = label proof (prove)
goal:
No subgoals!
theory Eval_CAMKES_CDL

lemma helper_pcs_refined_policyI:
  assumes cdt_policy: "\<And>p slot p' slot'.
                          cdl_cdt s (p, slot) = Some (p', slot') \<Longrightarrow>
                          (pasObjectAbs aag p', Control, pasObjectAbs aag p) \<in> pasPolicy aag"
      and delete_derived_policy: "\<And>p slot p' slot'.
                          cdl_cdt s (p, slot) = Some (p', slot') \<Longrightarrow>
                          (pasObjectAbs aag p', DeleteDerived, pasObjectAbs aag p) \<in> pasPolicy aag"
      and obj_policy: "\<And>p p_obj p_idx cap auth oref.
                          \<lbrakk> cdl_objects s p = Some p_obj;
                            object_slots p_obj p_idx = Some cap;
                            auth \<in> cdl_cap_auth_conferred cap;
                            oref \<in> cdl_obj_refs cap
                          \<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, auth, pasObjectAbs aag oref) \<in> pasPolicy aag"
  shows "auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> (pasPolicy aag)" apply (clarsimp simp: cdl_state_objs_to_policy_def auth_graph_map_def) by (fastforce elim: cdl_state_bits_to_policy.cases
                intro: obj_policy cdt_policy delete_derived_policy
                simp: opt_cap_def slots_of_def
                split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>x auth y. (x, auth, y) \<in> cdl_state_bits_to_policy (\<lambda>ref. opt_cap ref s) (cdl_cdt s) \<Longrightarrow> (pasObjectAbs aag x, auth, pasObjectAbs aag y) \<in> pasPolicy aag
theory Eval_CAMKES_CDL

lemma sorted_distinct:
  "sorted_distinct xs \<Longrightarrow> sorted xs \<and> distinct xs" by (induct xs rule: sorted_distinct.induct; fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sorted_distinct xs \<Longrightarrow> sorted xs \<and> distinct xs