kings-crown/FVELER_Isabelle huggingface dataset:
theory ListLibLemmas

lemma last_of_list_insert_before:
  "xs \<noteq> [] \<Longrightarrow> last (list_insert_before xs a new) = last xs" by (induct xs; clarsimp simp: list_insert_before_nonempty)

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

lemma list_insert_before_distinct:
  "\<lbrakk>distinct (xs @ ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> list_insert_before (xs @ ys) (hd ys) new = xs @ new # ys" by (induct xs; fastforce simp add: list_insert_before_head)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (xs @ ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> list_insert_before (xs @ ys) (hd ys) new = xs @ new # ys
theory ListLibLemmas

lemma set_list_insert_before:
  "\<lbrakk>new \<notin> set ls; before \<in> set ls\<rbrakk> \<Longrightarrow> set (list_insert_before ls before new) = set ls \<union> {new}" apply (induct ls; clarsimp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new \<notin> set ls; before \<in> set ls\<rbrakk> \<Longrightarrow> set (list_insert_before ls before new) = set ls \<union> {new} proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>set (list_insert_before ls before new) = insert new (set ls); before \<in> set ls; new \<noteq> a; new \<notin> set ls; a \<noteq> before\<rbrakk> \<Longrightarrow> insert a (insert new (set ls)) = insert new (insert a (set ls)) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_remove_removed:
  "set (list_remove list x) = (set list) - {x}" apply (induct list,simp+) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (list_remove list x) = set list - {x} proof (prove)
goal (1 subgoal):
 1. \<And>a list. set (list_remove list x) = set list - {x} \<Longrightarrow> a \<noteq> x \<longrightarrow> insert a (set list - {x}) = insert a (set list) - {x} proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma remove_distinct_helper: "\<lbrakk>distinct (list_remove list x); a \<noteq> x; a \<notin> set list;
        distinct list\<rbrakk>
       \<Longrightarrow> a \<notin> set (list_remove list x)" apply (induct list) apply (simp split: if_split_asm)+ done

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

lemma list_remove_distinct:
  "distinct list \<Longrightarrow>  distinct (list_remove list x)" apply (induct list) apply (simp add: remove_distinct_helper split: if_split_asm)+ done

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

lemma list_remove_none: "x \<notin> set list \<Longrightarrow> list_remove list x = list" apply (induct list) apply clarsimp+ done

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

lemma list_remove_append[simp]:
  "list_remove (xs @ ys) t = list_remove xs t @ list_remove ys t" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_remove (xs @ ys) t = list_remove xs t @ list_remove ys t
theory ListLibLemmas

lemma list_remove_middle_distinct:
  "\<lbrakk>distinct q; q = ys @ t # zs\<rbrakk> \<Longrightarrow> list_remove q t = ys @ zs" apply (induct q rule: length_induct) apply (simp add: list_remove_none) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct q; q = ys @ t # zs\<rbrakk> \<Longrightarrow> list_remove q t = ys @ zs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ysa. length ysa < length xs \<longrightarrow> distinct ysa \<longrightarrow> ysa = ys @ t # zs \<longrightarrow> list_remove ysa t = ys @ zs; distinct xs; xs = ys @ t # zs\<rbrakk> \<Longrightarrow> list_remove xs t = ys @ zs proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma replace_distinct: "x \<notin> set list \<Longrightarrow> distinct list \<Longrightarrow> distinct (list_replace list y x)" apply (induct list) apply (simp add: list_replace_def)+ apply blast done

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

lemma set_list_replace_list:
  "\<lbrakk>distinct list; slot \<in> set list; slot \<notin> set list'\<rbrakk>
    \<Longrightarrow> set (list_replace_list list slot list') = set list \<union> set list' - {slot}" apply (induct list) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; slot \<in> set list; slot \<notin> set list'\<rbrakk> \<Longrightarrow> set (list_replace_list list slot list') = set list \<union> set list' - {slot} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct []; slot \<in> set []; slot \<notin> set list'\<rbrakk> \<Longrightarrow> set (list_replace_list [] slot list') = set [] \<union> set list' - {slot}
 2. \<And>a list. \<lbrakk>\<lbrakk>distinct list; slot \<in> set list; slot \<notin> set list'\<rbrakk> \<Longrightarrow> set (list_replace_list list slot list') = set list \<union> set list' - {slot}; distinct (a # list); slot \<in> set (a # list); slot \<notin> set list'\<rbrakk> \<Longrightarrow> set (list_replace_list (a # list) slot list') = set (a # list) \<union> set list' - {slot} proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma after_in_list_in_list:
  "after_in_list list a = Some b \<Longrightarrow> b \<in> set list" apply(induct list a arbitrary: b rule: after_in_list.induct) apply (simp split: if_split_asm)+ done

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

lemma after_in_list_append_notin_hd:
  "p \<notin> set list' \<Longrightarrow> after_in_list (list' @ list) p = after_in_list list p" apply(induct list', simp, simp) apply(case_tac list', simp) apply(case_tac list, simp+) done

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

lemma after_in_list_append_last_hd:
  "\<lbrakk>p \<in> set list'; after_in_list list' p = None\<rbrakk>
    \<Longrightarrow> after_in_list (list' @ x # xs) p = Some x" apply(induct list' p rule: after_in_list.induct) apply(simp) apply(simp) apply(simp split: if_split_asm) done

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

lemma after_in_list_append_in_hd:
  "after_in_list list p = Some a \<Longrightarrow> after_in_list (list @ list') p = Some a" apply(induct list p rule: after_in_list.induct) apply(simp split: if_split_asm)+ done

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

lemma after_in_list_in_list': "after_in_list list a = Some y \<Longrightarrow> a \<in> set list" apply (induct list a rule: after_in_list.induct) apply simp+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. after_in_list list a = Some y \<Longrightarrow> a \<in> set list proof (prove)
goal (3 subgoals):
 1. \<And>a. after_in_list [] a = Some y \<Longrightarrow> a \<in> set []
 2. \<And>x a. after_in_list [x] a = Some y \<Longrightarrow> a \<in> set [x]
 3. \<And>x ya xs a. \<lbrakk>\<lbrakk>a \<noteq> x; after_in_list (ya # xs) a = Some y\<rbrakk> \<Longrightarrow> a \<in> set (ya # xs); after_in_list (x # ya # xs) a = Some y\<rbrakk> \<Longrightarrow> a \<in> set (x # ya # xs) 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> a = ya \<or> a \<in> set xs; (if a = x then Some ya else after_in_list (ya # xs) a) = Some y\<rbrakk> \<Longrightarrow> a = x \<or> a = ya \<or> a \<in> set xs proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_replace_set: "x \<in> set list \<Longrightarrow> set (list_replace list x y) = insert y (set (list) - {x})" apply (induct list) apply (simp add: list_replace_def)+ apply (intro impI conjI) apply blast+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set list \<Longrightarrow> set (list_replace list x y) = insert y (set list - {x}) proof (prove)
goal (2 subgoals):
 1. x \<in> set [] \<Longrightarrow> set (list_replace [] x y) = insert y (set [] - {x})
 2. \<And>a list. \<lbrakk>x \<in> set list \<Longrightarrow> set (list_replace list x y) = insert y (set list - {x}); x \<in> set (a # list)\<rbrakk> \<Longrightarrow> set (list_replace (a # list) x y) = insert y (set (a # list) - {x}) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>x \<in> set list \<Longrightarrow> insert y (set list \<inter> {xa. xa \<noteq> x}) = insert y (set list - {x}); x = a \<or> x \<in> set list\<rbrakk> \<Longrightarrow> (a = x \<longrightarrow> insert y ((\<lambda>a. y) ` (set list \<inter> {x}) \<union> set list \<inter> {xa. xa \<noteq> x}) = insert y (set list - {x})) \<and> (a \<noteq> x \<longrightarrow> insert a ((\<lambda>a. y) ` (set list \<inter> {x}) \<union> set list \<inter> {xa. xa \<noteq> x}) = insert y (insert a (set list) - {x})) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>x \<in> set list \<Longrightarrow> insert y (set list \<inter> {xa. xa \<noteq> x}) = insert y (set list - {x}); x = a \<or> x \<in> set list; a = x\<rbrakk> \<Longrightarrow> insert y ((\<lambda>a. y) ` (set list \<inter> {x}) \<union> set list \<inter> {xa. xa \<noteq> x}) = insert y (set list - {x})
 2. \<And>a list. \<lbrakk>x \<in> set list \<Longrightarrow> insert y (set list \<inter> {xa. xa \<noteq> x}) = insert y (set list - {x}); x = a \<or> x \<in> set list; a \<noteq> x\<rbrakk> \<Longrightarrow> insert a ((\<lambda>a. y) ` (set list \<inter> {x}) \<union> set list \<inter> {xa. xa \<noteq> x}) = insert y (insert a (set list) - {x}) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma map_ignore: "x \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = x then y else xa)
             list) = list" apply (induct list) apply simp+ apply blast done

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

lemma map_ignore2: "y \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa)
             list) = (map (\<lambda>xa. if xa = x then y else xa) list)" apply (simp add: map_ignore) done

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

lemma map_ignore2': "y \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = y then x else if xa = x then y else xa)
             list) = (map (\<lambda>xa. if xa = x then y else xa) list)" apply (simp add: map_ignore) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<notin> set list \<Longrightarrow> map (\<lambda>xa. if xa = y then x else if xa = x then y else xa) list = map (\<lambda>xa. if xa = x then y else xa) list proof (prove)
goal (1 subgoal):
 1. y \<notin> set list \<Longrightarrow> x \<noteq> y \<longrightarrow> (\<forall>x\<in>set list. x \<noteq> y) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma swap_distinct_helper: "\<lbrakk>x \<in> set list; y \<noteq> x; y \<notin> set list; distinct list\<rbrakk>
       \<Longrightarrow> distinct (map (\<lambda>xa. if xa = x then y else xa) list)" apply (induct list) apply (simp add: map_ignore | elim conjE | intro impI conjI | blast)+ done

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

lemma list_swap_none: "x \<notin> set list \<Longrightarrow> y \<notin> set list \<Longrightarrow> list_swap list x y = list" apply (induct list) apply (simp add: list_swap_def)+ apply blast done

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

lemma in_swapped_list: "y \<in> set list \<Longrightarrow> x \<in> set (list_swap list x y)" apply (case_tac "x \<in> set list") apply (simp add: list_swap_both) apply (simp add: list_swap_one') apply (intro notI,simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<in> set list \<Longrightarrow> x \<in> set (list_swap list x y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y \<in> set list; x \<in> set list\<rbrakk> \<Longrightarrow> x \<in> set (list_swap list x y)
 2. \<lbrakk>y \<in> set list; x \<notin> set list\<rbrakk> \<Longrightarrow> x \<in> set (list_swap list x y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set list; x \<notin> set list\<rbrakk> \<Longrightarrow> x \<in> set (list_swap list x y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set list; x \<notin> set list\<rbrakk> \<Longrightarrow> x \<noteq> y proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma list_swap_empty : "(list_swap list x y = []) = (list = [])" by(simp add: list_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (list_swap list x y = []) = (list = [])
theory ListLibLemmas

lemma distinct_after_in_list_antisym:
  "distinct list \<Longrightarrow> after_in_list list a = Some b \<Longrightarrow> after_in_list list b \<noteq> Some a" apply (induct list b arbitrary: a rule: after_in_list.induct) apply simp+ apply (case_tac xs) apply (clarsimp split: if_split_asm | intro impI conjI)+ done

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