kings-crown/FVELER_Isabelle huggingface dataset:
theory ListLibLemmas

lemma psort_psorted: "R_list xs \<Longrightarrow> psorted (psort xs)" apply (simp add: psort_def) apply (induct xs) apply simp apply simp apply (cut_tac xs =xs in psort_set) apply (simp add: psort_def) apply (rule pinsort_sorted) apply simp apply (simp add: R_set_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R_list xs \<Longrightarrow> psorted (psort xs) proof (prove)
goal (1 subgoal):
 1. R_list xs \<Longrightarrow> psorted (foldr pinsort xs []) proof (prove)
goal (2 subgoals):
 1. R_list [] \<Longrightarrow> psorted (foldr pinsort [] [])
 2. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_list (a # xs)\<rbrakk> \<Longrightarrow> psorted (foldr pinsort (a # xs) []) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_list (a # xs)\<rbrakk> \<Longrightarrow> psorted (foldr pinsort (a # xs) []) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_set (insert a (set xs))\<rbrakk> \<Longrightarrow> psorted (pinsort a (foldr pinsort xs [])) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_set (insert a (set xs)); set (psort xs) = set xs\<rbrakk> \<Longrightarrow> psorted (pinsort a (foldr pinsort xs [])) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_set (insert a (set xs)); set (foldr pinsort xs []) = set xs\<rbrakk> \<Longrightarrow> psorted (pinsort a (foldr pinsort xs [])) proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_set (insert a (set xs)); set (foldr pinsort xs []) = set xs\<rbrakk> \<Longrightarrow> R_set (insert a (set (foldr pinsort xs [])))
 2. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_set (insert a (set xs)); set (foldr pinsort xs []) = set xs\<rbrakk> \<Longrightarrow> psorted (foldr pinsort xs []) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>R_list xs \<Longrightarrow> psorted (foldr pinsort xs []); R_set (insert a (set xs)); set (foldr pinsort xs []) = set xs\<rbrakk> \<Longrightarrow> psorted (foldr pinsort xs []) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma insort_length: "length (pinsort a xs) = Suc (length xs)" apply (induct xs) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (pinsort a xs) = Suc (length xs) proof (prove)
goal (2 subgoals):
 1. length (pinsort a []) = Suc (length [])
 2. \<And>aa xs. length (pinsort a xs) = Suc (length xs) \<Longrightarrow> length (pinsort a (aa # xs)) = Suc (length (aa # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. length (pinsort a xs) = Suc (length xs) \<Longrightarrow> length (pinsort a (aa # xs)) = Suc (length (aa # xs)) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma pinsort_distinct: "\<lbrakk>a \<notin> set xs; distinct xs\<rbrakk>
       \<Longrightarrow> distinct (pinsort a xs)" apply (induct xs) apply simp apply (clarsimp simp add: pinsort_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> distinct (pinsort a xs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<notin> set []; distinct []\<rbrakk> \<Longrightarrow> distinct (pinsort a [])
 2. \<And>aa xs. \<lbrakk>\<lbrakk>a \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> distinct (pinsort a xs); a \<notin> set (aa # xs); distinct (aa # xs)\<rbrakk> \<Longrightarrow> distinct (pinsort a (aa # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>a \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> distinct (pinsort a xs); a \<notin> set (aa # xs); distinct (aa # xs)\<rbrakk> \<Longrightarrow> distinct (pinsort a (aa # xs)) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma in_can_split: "y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ (y # ys)" apply (induct list) apply simp apply clarsimp apply (elim disjE) apply simp apply force apply simp apply (elim exE) apply simp apply (rule_tac x=ys in exI) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys proof (prove)
goal (2 subgoals):
 1. y \<in> set [] \<Longrightarrow> \<exists>ys xs. [] = xs @ y # ys
 2. \<And>a list. \<lbrakk>y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys; y \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys; y \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys; y = a \<or> y \<in> set list\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys; y = a\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys
 2. \<And>a list. \<lbrakk>y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys; y \<in> set list\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>a \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ a # ys; y = a\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ a # ys
 2. \<And>a list. \<lbrakk>y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys; y \<in> set list\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ y # ys; y \<in> set list\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<exists>ys xs. list = xs @ y # ys; y \<in> set list\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (1 subgoal):
 1. \<And>a list ys xs. \<lbrakk>y \<in> set list; list = xs @ y # ys\<rbrakk> \<Longrightarrow> \<exists>ys xs. a # list = xs @ y # ys proof (prove)
goal (1 subgoal):
 1. \<And>a list ys xs. list = xs @ y # ys \<Longrightarrow> \<exists>ysa xsa. a # xs @ y # ys = xsa @ y # ysa proof (prove)
goal (1 subgoal):
 1. \<And>a list ys xs. list = xs @ y # ys \<Longrightarrow> \<exists>xsa. a # xs @ y # ys = xsa @ y # ys proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma psorted_set: "finite A \<Longrightarrow> R_set A \<Longrightarrow> \<exists>!xs. set xs = A \<and> psorted xs \<and> distinct xs" apply (drule finite_distinct_list) apply clarify apply (rule_tac a="psort xs" in ex1I) apply (auto simp: psorted_distinct_set_unique psort_set psort_psorted psort_distinct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; R_set A\<rbrakk> \<Longrightarrow> \<exists>!xs. set xs = A \<and> psorted xs \<and> distinct xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R_set A; \<exists>xs. set xs = A \<and> distinct xs\<rbrakk> \<Longrightarrow> \<exists>!xs. set xs = A \<and> psorted xs \<and> distinct xs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>R_list xs; distinct xs; A = set xs\<rbrakk> \<Longrightarrow> \<exists>!xsa. set xsa = set xs \<and> psorted xsa \<and> distinct xsa proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>R_list xs; distinct xs; A = set xs\<rbrakk> \<Longrightarrow> set (psort xs) = set xs \<and> psorted (psort xs) \<and> distinct (psort xs)
 2. \<And>xs x. \<lbrakk>R_list xs; distinct xs; A = set xs; set x = set xs \<and> psorted x \<and> distinct x\<rbrakk> \<Longrightarrow> x = psort xs proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma after_can_split: "after_in_list list x = Some y \<Longrightarrow> \<exists>ys xs. list = xs @ (x # y # ys)" apply (induct list x rule: after_in_list.induct) apply simp+ apply (simp split: if_split_asm) apply force apply (elim exE) apply simp apply (rule_tac x="ys" in exI) apply simp done

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

lemma after_ignore_head: "x \<notin> set list \<Longrightarrow> after_in_list (list @ list') x = after_in_list list' x" apply (induct list x rule: after_in_list.induct) apply simp apply simp apply (case_tac list',simp+) done

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

lemma (in partial_sort) after_order_sorted:
assumes after_order: "\<And>x y. after_in_list list x = Some y \<Longrightarrow> less x y"
assumes distinct: "distinct list"
shows "psorted list" apply (rule lsorted_sorted) apply (rule after_order) apply (erule after_distinct_one_sibling[OF distinct]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. psorted list proof (prove)
goal (1 subgoal):
 1. \<And>x y xs ys. list = xs @ x # y # ys \<Longrightarrow> less x y proof (prove)
goal (1 subgoal):
 1. \<And>x y xs ys. list = xs @ x # y # ys \<Longrightarrow> after_in_list list x = Some y proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma hd_not_after_in_list:
  "\<lbrakk>distinct xs; x \<notin> set xs\<rbrakk> \<Longrightarrow> after_in_list (x # xs) a \<noteq> Some x" apply (induct xs a rule: after_in_list.induct) apply simp+ apply fastforce done

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

lemma list_replace_ignore:"a \<notin> set list \<Longrightarrow> list_replace list a b = list" apply (simp add: list_replace_def) apply (induct list,clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<notin> set list \<Longrightarrow> list_replace list a b = list proof (prove)
goal (1 subgoal):
 1. a \<notin> set list \<Longrightarrow> map (\<lambda>x. if x = a then b else x) list = list proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_replace_empty[simp]: "list_replace [] a b = []" by (simp add: list_replace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_replace [] a b = []
theory ListLibLemmas

lemma list_replace_empty2[simp]:
  "(list_replace list a b = []) = (list = [])" by (simp add: list_replace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (list_replace list a b = []) = (list = [])
theory ListLibLemmas

lemma replace_list_preserve_after: "dest \<notin> set list \<Longrightarrow> distinct list \<Longrightarrow>  after_in_list (list_replace list src dest) dest = after_in_list list src" apply (simp add: list_replace_def) apply (induct list src rule: after_in_list.induct) apply (simp+) apply fastforce done

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

lemma replace_list_preserve_after': "\<lbrakk>p \<noteq> dest; p \<noteq> src;
         after_in_list list p \<noteq> Some src\<rbrakk>
        \<Longrightarrow> after_in_list (list_replace list src dest) p = after_in_list list p" apply (simp add: list_replace_def) apply (induct list p rule: after_in_list.induct) apply (simp+) apply fastforce done

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

lemma distinct_after_in_list_not_self:
  "distinct list \<Longrightarrow> after_in_list list src \<noteq> Some src" apply (induct list,simp+) apply (case_tac list,clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> after_in_list list src \<noteq> Some src proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>after_in_list list src \<noteq> Some src; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> after_in_list (a # list) src \<noteq> Some src proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma set_list_insert_after:
  "set (list_insert_after list a b) = set list \<union> (if a \<in> set list then {b} else {})" apply(induct list) apply(simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (list_insert_after list a b) = set list \<union> (if a \<in> set list then {b} else {}) proof (prove)
goal (2 subgoals):
 1. set (list_insert_after [] a b) = set [] \<union> (if a \<in> set [] then {b} else {})
 2. \<And>aa list. set (list_insert_after list a b) = set list \<union> (if a \<in> set list then {b} else {}) \<Longrightarrow> set (list_insert_after (aa # list) a b) = set (aa # list) \<union> (if a \<in> set (aa # list) then {b} else {}) proof (prove)
goal (1 subgoal):
 1. \<And>aa list. set (list_insert_after list a b) = set list \<union> (if a \<in> set list then {b} else {}) \<Longrightarrow> set (list_insert_after (aa # list) a b) = set (aa # list) \<union> (if a \<in> set (aa # list) then {b} else {}) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma distinct_list_insert_after:
  "\<lbrakk>distinct list; b \<notin> set list \<or> a \<notin> set list\<rbrakk> \<Longrightarrow> distinct (list_insert_after list a b)" apply(induct list) apply(simp) apply(fastforce simp: set_list_insert_after) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; b \<notin> set list \<or> a \<notin> set list\<rbrakk> \<Longrightarrow> distinct (list_insert_after list a b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct []; b \<notin> set [] \<or> a \<notin> set []\<rbrakk> \<Longrightarrow> distinct (list_insert_after [] a b)
 2. \<And>aa list. \<lbrakk>\<lbrakk>distinct list; b \<notin> set list \<or> a \<notin> set list\<rbrakk> \<Longrightarrow> distinct (list_insert_after list a b); distinct (aa # list); b \<notin> set (aa # list) \<or> a \<notin> set (aa # list)\<rbrakk> \<Longrightarrow> distinct (list_insert_after (aa # list) a b) proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<lbrakk>distinct list; b \<notin> set list \<or> a \<notin> set list\<rbrakk> \<Longrightarrow> distinct (list_insert_after list a b); distinct (aa # list); b \<notin> set (aa # list) \<or> a \<notin> set (aa # list)\<rbrakk> \<Longrightarrow> distinct (list_insert_after (aa # list) a b) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_insert_before_not_found:
  "a \<notin> set ls \<Longrightarrow> list_insert_before ls a new = ls" by (induct ls; fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<notin> set ls \<Longrightarrow> list_insert_before ls a new = ls
theory ListLibLemmas

lemma list_insert_before_nonempty:
  "ls \<noteq> [] \<Longrightarrow> list_insert_before ls a new \<noteq> []" by (induct ls; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ls \<noteq> [] \<Longrightarrow> list_insert_before ls a new \<noteq> []
theory ListLibLemmas

lemma list_insert_before_head:
  "xs \<noteq> [] \<Longrightarrow> list_insert_before xs (hd xs) new = new # xs" by (induct xs; fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_insert_before xs (hd xs) new = new # xs