kings-crown/FVELER_Isabelle huggingface dataset:
theory ListLibLemmas

lemma after_in_listD: "after_in_list list x = Some y \<Longrightarrow> \<exists>xs ys. list = xs @ (x # y # ys) \<and> x \<notin> set xs" apply (induct list x arbitrary: a rule: after_in_list.induct) apply (simp split: if_split_asm | elim exE | force)+ apply (rule_tac x="x # xsa" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. after_in_list list x = Some y \<Longrightarrow> \<exists>xs ys. list = xs @ x # y # ys \<and> x \<notin> set xs proof (prove)
goal (3 subgoals):
 1. \<And>a. after_in_list [] a = Some y \<Longrightarrow> \<exists>xs ys. [] = xs @ a # y # ys \<and> a \<notin> set xs
 2. \<And>x a. after_in_list [x] a = Some y \<Longrightarrow> \<exists>xs ys. [x] = xs @ a # y # ys \<and> a \<notin> set xs
 3. \<And>x ya xs a. \<lbrakk>\<lbrakk>a \<noteq> x; after_in_list (ya # xs) a = Some y\<rbrakk> \<Longrightarrow> \<exists>xsa ys. ya # xs = xsa @ a # y # ys \<and> a \<notin> set xsa; after_in_list (x # ya # xs) a = Some y\<rbrakk> \<Longrightarrow> \<exists>xsa ys. x # ya # xs = xsa @ a # y # ys \<and> a \<notin> set xsa proof (prove)
goal (1 subgoal):
 1. \<And>x ya xs a xsa. \<lbrakk>a \<noteq> x; after_in_list (ya # xs) a = Some y; (\<exists>ys. ya # xs = xsa @ a # y # ys) \<and> a \<notin> set xsa\<rbrakk> \<Longrightarrow> \<exists>xsa. (\<exists>ys. x # ya # xs = xsa @ a # y # ys) \<and> a \<notin> set xsa proof (prove)
goal (1 subgoal):
 1. \<And>x ya xs a xsa. \<lbrakk>a \<noteq> x; after_in_list (ya # xs) a = Some y; (\<exists>ys. ya # xs = xsa @ a # y # ys) \<and> a \<notin> set xsa\<rbrakk> \<Longrightarrow> (\<exists>ys. x # ya # xs = (x # xsa) @ a # y # ys) \<and> a \<notin> set (x # xsa) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_swap_symmetric: "list_swap list a b = list_swap list b a" apply (simp add: list_swap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_swap list a b = list_swap list b a proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_swap_preserve_after:
  "\<lbrakk>desta \<notin> set list; distinct list\<rbrakk>
\<Longrightarrow> after_in_list (list_swap list srca desta) desta =
   after_in_list list srca" apply (induct list desta rule: after_in_list.induct) apply (simp add: list_swap_def)+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>desta \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> after_in_list (list_swap list srca desta) desta = after_in_list list srca proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>a \<notin> set []; distinct []\<rbrakk> \<Longrightarrow> after_in_list (list_swap [] srca a) a = after_in_list [] srca
 2. \<And>x a. \<lbrakk>a \<notin> set [x]; distinct [x]\<rbrakk> \<Longrightarrow> after_in_list (list_swap [x] srca a) a = after_in_list [x] srca
 3. \<And>x y xs a. \<lbrakk>\<lbrakk>a \<noteq> x; a \<notin> set (y # xs); distinct (y # xs)\<rbrakk> \<Longrightarrow> after_in_list (list_swap (y # xs) srca a) a = after_in_list (y # xs) srca; a \<notin> set (x # y # xs); distinct (x # y # xs)\<rbrakk> \<Longrightarrow> after_in_list (list_swap (x # y # xs) srca a) a = after_in_list (x # y # xs) srca proof (prove)
goal (1 subgoal):
 1. \<And>x y xs a. \<lbrakk>after_in_list ((if y = srca then a else if y = a then srca else y) # map (\<lambda>x. if x = srca then a else if x = a then srca else x) xs) a = after_in_list (y # xs) srca; a \<noteq> x \<and> a \<noteq> y \<and> a \<notin> set xs; x \<noteq> y \<and> x \<notin> set xs \<and> y \<notin> set xs \<and> distinct xs\<rbrakk> \<Longrightarrow> (y = srca \<longrightarrow> srca \<noteq> a \<longrightarrow> srca = x \<longrightarrow> x = a) \<and> (y \<noteq> srca \<longrightarrow> (y = a \<longrightarrow> x \<noteq> a \<longrightarrow> srca \<noteq> x) \<and> (y \<noteq> a \<longrightarrow> y = x \<longrightarrow> x \<noteq> a \<longrightarrow> srca \<noteq> x)) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_swap_preserve_None:
 "\<lbrakk>after_in_list list srca = None\<rbrakk>
\<Longrightarrow> after_in_list (list_swap list desta srca) desta = None" apply (induct list srca rule: after_in_list.induct) apply (simp add: list_swap_def)+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. after_in_list list srca = None \<Longrightarrow> after_in_list (list_swap list desta srca) desta = None proof (prove)
goal (3 subgoals):
 1. \<And>a. after_in_list [] a = None \<Longrightarrow> after_in_list (list_swap [] desta a) desta = None
 2. \<And>x a. after_in_list [x] a = None \<Longrightarrow> after_in_list (list_swap [x] desta a) desta = None
 3. \<And>x y xs a. \<lbrakk>\<lbrakk>a \<noteq> x; after_in_list (y # xs) a = None\<rbrakk> \<Longrightarrow> after_in_list (list_swap (y # xs) desta a) desta = None; after_in_list (x # y # xs) a = None\<rbrakk> \<Longrightarrow> after_in_list (list_swap (x # y # xs) desta a) desta = None proof (prove)
goal (1 subgoal):
 1. \<And>x y xs a. \<lbrakk>\<lbrakk>a \<noteq> x; after_in_list (y # xs) a = None\<rbrakk> \<Longrightarrow> after_in_list ((if y = desta then a else if y = a then desta else y) # map (\<lambda>x. if x = desta then a else if x = a then desta else x) xs) desta = None; (if a = x then Some y else after_in_list (y # xs) a) = None\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = desta \<longrightarrow> x \<noteq> desta \<and> (x \<noteq> desta \<longrightarrow> after_in_list (desta # map (\<lambda>x. if x = desta then a else if x = a then desta else x) xs) desta = None)) \<and> (a \<noteq> desta \<longrightarrow> x \<noteq> a \<and> (x \<noteq> a \<longrightarrow> after_in_list (desta # map (\<lambda>x. if x = desta then a else if x = a then desta else x) xs) desta = None))) \<and> (y \<noteq> a \<longrightarrow> (y = desta \<longrightarrow> x \<noteq> a \<and> (x \<noteq> a \<longrightarrow> (x = desta \<longrightarrow> desta \<noteq> a \<and> (desta \<noteq> a \<longrightarrow> after_in_list (a # map (\<lambda>x. if x = desta then a else if x = a then desta else x) xs) desta = None)) \<and> (x \<noteq> desta \<longrightarrow> after_in_list (a # map (\<lambda>x. if x = desta then a else if x = a then desta else x) xs) desta = None))) \<and> (y \<noteq> desta \<longrightarrow> x \<noteq> a \<and> (x \<noteq> a \<longrightarrow> (x = desta \<longrightarrow> desta \<noteq> a \<and> (desta \<noteq> a \<longrightarrow> after_in_list (y # map (\<lambda>x. if x = desta then a else if x = a then desta else x) xs) desta = None)) \<and> (x \<noteq> desta \<longrightarrow> after_in_list (y # map (\<lambda>x. if x = desta then a else if x = a then desta else x) xs) desta = None)))) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_swap_preserve_None':
 "\<lbrakk>after_in_list list srca = None\<rbrakk>
\<Longrightarrow> after_in_list (list_swap list srca desta) desta = None" apply (subst list_swap_symmetric) apply (erule list_swap_preserve_None) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. after_in_list list srca = None \<Longrightarrow> after_in_list (list_swap list srca desta) desta = None proof (prove)
goal (1 subgoal):
 1. after_in_list list srca = None \<Longrightarrow> after_in_list (list_swap list desta srca) desta = None proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_swap_preserve_Some_other_distinct:
 "\<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk>
\<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z" apply (rule list_swap_preserve_Some_other) apply simp+ apply (rule notI) apply simp apply (frule distinct_after_in_list_not_self[where src=srca]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> z \<noteq> desta
 2. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> z \<noteq> srca
 3. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> after_in_list list srca = Some z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> z \<noteq> srca
 2. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> after_in_list list srca = Some z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z; z = srca\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> after_in_list list srca = Some z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct list; srca \<noteq> desta; after_in_list list srca = Some srca; z = srca\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> after_in_list list srca = Some z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct list; srca \<noteq> desta; after_in_list list srca = Some srca; z = srca; after_in_list list srca \<noteq> Some srca\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> after_in_list list srca = Some z proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_swap_preserve_separate:
 "\<lbrakk>p \<noteq> desta; p \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list list p = Some z\<rbrakk>
\<Longrightarrow> after_in_list (list_swap list srca desta) p = Some z" apply (induct list p rule: after_in_list.induct) apply (simp add: list_swap_def split: if_split_asm)+ apply (intro impI conjI) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> desta; p \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list list p = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap list srca desta) p = Some z proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>a \<noteq> desta; a \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list [] a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap [] srca desta) a = Some z
 2. \<And>x a. \<lbrakk>a \<noteq> desta; a \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list [x] a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap [x] srca desta) a = Some z
 3. \<And>x y xs a. \<lbrakk>\<lbrakk>a \<noteq> x; a \<noteq> desta; a \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list (y # xs) a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap (y # xs) srca desta) a = Some z; a \<noteq> desta; a \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list (x # y # xs) a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap (x # y # xs) srca desta) a = Some z proof (prove)
goal (1 subgoal):
 1. \<And>x y xs a. \<lbrakk>a \<noteq> desta; a \<noteq> srca; z \<noteq> desta; z \<noteq> srca; a \<noteq> x; after_in_list (srca # xs) a = Some z; y = srca; after_in_list (desta # map (\<lambda>x. if x = srca then desta else if x = desta then srca else x) xs) a = Some z\<rbrakk> \<Longrightarrow> (x = desta \<longrightarrow> desta = srca \<longrightarrow> after_in_list (srca # map (\<lambda>x. if x = srca then desta else if x = desta then srca else x) xs) a = Some z) \<and> (x \<noteq> desta \<longrightarrow> srca = desta \<longrightarrow> after_in_list (desta # xs) a = Some z) proof (prove)
goal (2 subgoals):
 1. \<And>x y xs a. \<lbrakk>a \<noteq> desta; a \<noteq> srca; z \<noteq> desta; z \<noteq> srca; a \<noteq> x; after_in_list (srca # xs) a = Some z; y = srca; after_in_list (desta # map (\<lambda>x. if x = srca then desta else if x = desta then srca else x) xs) a = Some z; x = desta; desta = srca\<rbrakk> \<Longrightarrow> after_in_list (srca # map (\<lambda>x. if x = srca then desta else if x = desta then srca else x) xs) a = Some z
 2. \<And>x y xs a. \<lbrakk>a \<noteq> desta; a \<noteq> srca; z \<noteq> desta; z \<noteq> srca; a \<noteq> x; after_in_list (srca # xs) a = Some z; y = srca; after_in_list (desta # map (\<lambda>x. if x = srca then desta else if x = desta then srca else x) xs) a = Some z; x \<noteq> desta; srca = desta\<rbrakk> \<Longrightarrow> after_in_list (desta # xs) a = Some z proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma after_in_list_list_in_list:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "y \<in> set (after_in_list_list list x) \<Longrightarrow> y \<in> set list" apply(induct list arbitrary:x y) apply(simp) apply(case_tac "x=a", simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<in> set (after_in_list_list list x) \<Longrightarrow> y \<in> set list proof (prove)
goal (2 subgoals):
 1. \<And>x y. y \<in> set (after_in_list_list [] x) \<Longrightarrow> y \<in> set []
 2. \<And>a list x y. \<lbrakk>\<And>x y. y \<in> set (after_in_list_list list x) \<Longrightarrow> y \<in> set list; y \<in> set (after_in_list_list (a # list) x)\<rbrakk> \<Longrightarrow> y \<in> set (a # list) proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>\<And>x y. y \<in> set (after_in_list_list list x) \<Longrightarrow> y \<in> set list; y \<in> set (after_in_list_list (a # list) x)\<rbrakk> \<Longrightarrow> y \<in> set (a # list) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma indexed_trancl_irrefl: "distinct list \<Longrightarrow> (x,x) \<notin> {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+" apply (frule indexed_trancl_as_set [THEN sym]) apply (simp) apply (intro allI impI notI) apply (frule_tac xs = list and i = p and j = q in nth_eq_iff_index_eq) apply (simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> (x, x) \<notin> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ = {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j}\<rbrakk> \<Longrightarrow> (x, x) \<notin> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ = {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j}\<rbrakk> \<Longrightarrow> \<forall>p. list ! p = x \<longrightarrow> (\<forall>q<length list. p < q \<longrightarrow> list ! q \<noteq> x) proof (prove)
goal (1 subgoal):
 1. \<And>p q. \<lbrakk>distinct list; {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ = {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j}; list ! p = x; q < length list; p < q; list ! q = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>p q. \<lbrakk>distinct list; {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ = {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j}; list ! p = x; q < length list; p < q; list ! q = x\<rbrakk> \<Longrightarrow> p < length list
 2. \<And>p q. \<lbrakk>distinct list; {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ = {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j}; list ! p = x; q < length list; p < q; list ! q = x\<rbrakk> \<Longrightarrow> q < length list
 3. \<And>p q. \<lbrakk>distinct list; {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ = {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j}; list ! p = x; q < length list; p < q; list ! q = x; (list ! p = list ! q) = (p = q)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma distinct_after_in_list_not_self_trancl:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "distinct list \<Longrightarrow> (x, x) \<notin> {(p, q). after_in_list list p = Some q}\<^sup>+" by (simp add: after_in_list_trancl_indexed_trancl indexed_trancl_irrefl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> (x, x) \<notin> {(p, q). after_in_list list p = Some q}\<^sup>+
theory ListLibLemmas

lemma distinct_after_in_list_in_list_trancl:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>distinct list; (x, y) \<in> {(p, q). after_in_list list q = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> set list" by(erule tranclE2, (drule CollectD, simp, drule after_in_list_in_list, simp)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; (x, y) \<in> {(p, q). after_in_list list q = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> set list
theory ListLibLemmas

lemma after_in_list_append_not_hd:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "a \<noteq> x \<Longrightarrow> after_in_list (a # list) x = after_in_list list x" by (case_tac list, simp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> x \<Longrightarrow> after_in_list (a # list) x = after_in_list list x
theory ListLibLemmas

lemma trancl_Collect_rev:
  "(a, b) \<in> {(x, y). P x y}\<^sup>+ \<Longrightarrow> (b, a) \<in> {(x, y). P y x}\<^sup>+" apply(induct rule: trancl_induct) apply(fastforce intro: trancl_into_trancl2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> {(x, y). P x y}\<^sup>+ \<Longrightarrow> (b, a) \<in> {(x, y). P y x}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>y. (a, y) \<in> {(x, y). P x y} \<Longrightarrow> (y, a) \<in> {a. case a of (x, y) \<Rightarrow> P y x}\<^sup>+
 2. \<And>y z. \<lbrakk>(a, y) \<in> {(x, y). P x y}\<^sup>+; (y, z) \<in> {(x, y). P x y}; (y, a) \<in> {a. case a of (x, y) \<Rightarrow> P y x}\<^sup>+\<rbrakk> \<Longrightarrow> (z, a) \<in> {a. case a of (x, y) \<Rightarrow> P y x}\<^sup>+ proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma after_in_list_in_cons:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>after_in_list (x # xs) y = Some z; distinct (x # xs); y \<in> set xs\<rbrakk> \<Longrightarrow> z \<in> set xs" apply(case_tac "y=x") apply(simp) apply(simp add:after_in_list_append_not_hd after_in_list_in_list) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>after_in_list (x # xs) y = Some z; distinct (x # xs); y \<in> set xs\<rbrakk> \<Longrightarrow> z \<in> set xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>after_in_list (x # xs) y = Some z; distinct (x # xs); y \<in> set xs; y = x\<rbrakk> \<Longrightarrow> z \<in> set xs
 2. \<lbrakk>after_in_list (x # xs) y = Some z; distinct (x # xs); y \<in> set xs; y \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>after_in_list (x # xs) y = Some z; distinct (x # xs); y \<in> set xs; y \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set xs proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma after_in_list_None_last:
  "\<lbrakk>after_in_list list x = None; x \<in> set list\<rbrakk> \<Longrightarrow> x = last list" by (induct list x rule: after_in_list.induct,(simp split: if_split_asm)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>after_in_list list x = None; x \<in> set list\<rbrakk> \<Longrightarrow> x = last list
theory ListLibLemmas

lemma sorted_lastD:
  "\<lbrakk> sorted xs; xs \<noteq> [] \<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. x \<le> last xs" by (induct xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. x \<le> last xs
theory ListLibLemmas

lemma sorted_last_leD:
  "\<lbrakk> sorted xs; y \<ge> last xs ; xs \<noteq> [] \<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. x \<le> y" by (fastforce dest: sorted_lastD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; last xs \<le> y; xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. x \<le> y
theory ListLibLemmas

lemma length_gt_1_imp_butlast_nonempty:
  "Suc 0 < length xs \<Longrightarrow> butlast xs \<noteq> []" by (cases xs; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length xs \<Longrightarrow> butlast xs \<noteq> []
theory ListLibLemmas

lemma not_last_in_set_butlast:
  "\<lbrakk>ptr \<in> set ls; ptr \<noteq> last ls\<rbrakk> \<Longrightarrow> ptr \<in> set (butlast ls)" apply (induct ls; simp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<in> set ls; ptr \<noteq> last ls\<rbrakk> \<Longrightarrow> ptr \<in> set (butlast ls) proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>\<lbrakk>ptr \<in> set ls; ptr \<noteq> last ls\<rbrakk> \<Longrightarrow> ptr \<in> set (butlast ls); ptr = a \<or> ptr \<in> set ls; ptr \<noteq> (if ls = [] then a else last ls)\<rbrakk> \<Longrightarrow> ls \<noteq> [] \<and> (ls \<noteq> [] \<longrightarrow> ptr = a \<or> ptr \<in> set (butlast ls)) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma distinct_in_butlast_not_last:
  "\<lbrakk>distinct ls; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<noteq> last ls" apply (induct ls; simp) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct ls; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<noteq> last ls proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>x \<in> set (butlast ls) \<Longrightarrow> x \<noteq> last ls; a \<notin> set ls \<and> distinct ls; x \<in> set (if ls = [] then [] else a # butlast ls)\<rbrakk> \<Longrightarrow> (ls = [] \<longrightarrow> x \<noteq> a) \<and> (ls \<noteq> [] \<longrightarrow> x \<noteq> last ls) proof (prove)
goal:
No subgoals!
theory Rights_AI

lemma validate_vm_rights_idem[simp]:
  "validate_vm_rights (validate_vm_rights rights) = validate_vm_rights rights" by (clarsimp simp: validate_vm_rights_def vm_kernel_only_def vm_read_only_def vm_read_write_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. validate_vm_rights (validate_vm_rights rights) = validate_vm_rights rights
theory Rights_AI

lemma validate_vm_rights_inter_rw:
  "validate_vm_rights (vm_read_write \<inter> rights) = validate_vm_rights rights" apply (rule set_eqI) apply (clarsimp simp: validate_vm_rights_def vm_read_write_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. validate_vm_rights (vm_read_write \<inter> rights) = validate_vm_rights rights proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> validate_vm_rights (vm_read_write \<inter> rights)) = (x \<in> validate_vm_rights rights) proof (prove)
goal:
No subgoals!
theory Rights_AI

lemma valid_validate_vm_rights[simp]:
  "validate_vm_rights rs \<in> valid_vm_rights"
and validate_vm_rights_subseteq[simp]:
  "validate_vm_rights rs \<subseteq> rs"
and validate_vm_rights_simps[simp]:
  "validate_vm_rights vm_read_write = vm_read_write"
  "validate_vm_rights vm_read_only = vm_read_only"
  "validate_vm_rights vm_kernel_only = vm_kernel_only" by (simp_all add: validate_vm_rights_def valid_vm_rights_def
                    vm_read_write_def vm_read_only_def vm_kernel_only_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. validate_vm_rights rs \<in> valid_vm_rights &&& validate_vm_rights rs \<subseteq> rs &&& validate_vm_rights vm_read_write = vm_read_write &&& validate_vm_rights vm_read_only = vm_read_only &&& validate_vm_rights vm_kernel_only = vm_kernel_only