theory ListLibLemmas

lemma lsorted_sorted:
assumes lsorted: "\<And>x y xs ys . list = xs @ (x # y # ys) \<Longrightarrow> less x y"
shows "psorted list" apply (insert lsorted) apply atomize apply simp apply (induct list) apply simp apply (simp add: psorted_Cons) apply (rule context_conjI) apply (erule meta_mp) apply clarsimp apply (drule_tac x="a#xs" in spec) apply (drule_tac x=x in spec) apply (drule_tac x=y in spec) apply (erule mp) apply force apply (intro ballI) apply clarsimp apply (drule in_can_split) apply (elim exE) apply (drule_tac x="[]" in spec) apply simp apply (case_tac xs) apply simp apply (clarsimp simp add: psorted_Cons) apply (blast intro: trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. psorted list proof (prove)
goal (1 subgoal):
 1. (\<And>xs x y ys. list = xs @ x # y # ys \<Longrightarrow> less x y) \<Longrightarrow> psorted list proof (prove)
goal (1 subgoal):
 1. \<forall>xs x y ys. list = xs @ x # y # ys \<longrightarrow> less x y \<Longrightarrow> psorted list proof (prove)
goal (1 subgoal):
 1. \<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list proof (prove)
goal (2 subgoals):
 1. \<forall>xs x y. (\<exists>ys. [] = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted []
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y\<rbrakk> \<Longrightarrow> psorted (a # list) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y\<rbrakk> \<Longrightarrow> psorted (a # list) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y\<rbrakk> \<Longrightarrow> psorted list \<and> (\<forall>y\<in>set list. less a y) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y\<rbrakk> \<Longrightarrow> psorted list
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> \<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (2 subgoals):
 1. \<And>a xs x y ys. \<forall>xsa xa ya. (\<exists>ysa. a # xs @ x # y # ys = xsa @ xa # ya # ysa) \<longrightarrow> less xa ya \<Longrightarrow> less x y
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (2 subgoals):
 1. \<And>a xs x y ys. \<forall>xa ya. (\<exists>ysa. a # xs @ x # y # ys = (a # xs) @ xa # ya # ysa) \<longrightarrow> less xa ya \<Longrightarrow> less x y
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (2 subgoals):
 1. \<And>a xs x y ys. \<forall>ya. (\<exists>ysa. a # xs @ x # y # ys = (a # xs) @ x # ya # ysa) \<longrightarrow> less x ya \<Longrightarrow> less x y
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (2 subgoals):
 1. \<And>a xs x y ys. (\<exists>ysa. a # xs @ x # y # ys = (a # xs) @ x # y # ysa) \<longrightarrow> less x y \<Longrightarrow> less x y
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (2 subgoals):
 1. \<And>a xs x y ys. \<exists>ysa. a # xs @ x # y # ys = (a # xs) @ x # y # ysa
 2. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set list. less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list y. \<lbrakk>\<forall>xs x y. (\<exists>ys. list = xs @ x # y # ys) \<longrightarrow> less x y \<Longrightarrow> psorted list; \<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list; y \<in> set list\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list y. \<lbrakk>\<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list; y \<in> set list\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list y. \<lbrakk>\<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list; \<exists>ys xs. list = xs @ y # ys\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list y ys xs. \<lbrakk>\<forall>xs x y. (\<exists>ys. a # list = xs @ x # y # ys) \<longrightarrow> less x y; psorted list; list = xs @ y # ys\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list y ys xs. \<lbrakk>psorted list; list = xs @ y # ys; \<forall>x y. (\<exists>ys. a # list = [] @ x # y # ys) \<longrightarrow> less x y\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list y ys xs. \<lbrakk>psorted (xs @ y # ys); list = xs @ y # ys; \<forall>ya. (\<exists>ysa. xs @ y # ys = ya # ysa) \<longrightarrow> less a ya\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (2 subgoals):
 1. \<And>a list y ys xs. \<lbrakk>psorted (xs @ y # ys); list = xs @ y # ys; \<forall>ya. (\<exists>ysa. xs @ y # ys = ya # ysa) \<longrightarrow> less a ya; xs = []\<rbrakk> \<Longrightarrow> less a y
 2. \<And>a list y ys xs aa lista. \<lbrakk>psorted (xs @ y # ys); list = xs @ y # ys; \<forall>ya. (\<exists>ysa. xs @ y # ys = ya # ysa) \<longrightarrow> less a ya; xs = aa # lista\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (1 subgoal):
 1. \<And>a list y ys xs aa lista. \<lbrakk>psorted (xs @ y # ys); list = xs @ y # ys; \<forall>ya. (\<exists>ysa. xs @ y # ys = ya # ysa) \<longrightarrow> less a ya; xs = aa # lista\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal (1 subgoal):
 1. \<And>a y ys aa lista. \<lbrakk>less a aa; psorted (lista @ y # ys); less aa y; \<forall>x\<in>set lista \<union> set ys. less aa x\<rbrakk> \<Longrightarrow> less a y proof (prove)
goal:
No subgoals!