theory ListLibLemmas

lemma pinsort_sorted: "R_set (insert a (set xs)) \<Longrightarrow> psorted xs \<Longrightarrow> psorted (pinsort a xs)" apply (induct xs arbitrary: a) apply (simp add: psorted_Cons) apply (simp add: psorted_Cons) apply clarsimp apply (simp add: pinsort_set) apply (intro impI conjI) apply (intro ballI) apply (drule_tac x=x in bspec) apply simp apply (frule(1) trans) apply simp apply (simp add: R_set_def) apply (rule all_comp') apply (simp add: R_set_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R_set (insert a (set xs)); psorted xs\<rbrakk> \<Longrightarrow> psorted (pinsort a xs) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>R_set (insert a (set [])); psorted []\<rbrakk> \<Longrightarrow> psorted (pinsort a [])
 2. \<And>a xs aa. \<lbrakk>\<And>a. \<lbrakk>R_set (insert a (set xs)); psorted xs\<rbrakk> \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (set (a # xs))); psorted (a # xs)\<rbrakk> \<Longrightarrow> psorted (pinsort aa (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. \<lbrakk>R_set (insert a (set xs)); psorted xs\<rbrakk> \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (set (a # xs))); psorted (a # xs)\<rbrakk> \<Longrightarrow> psorted (pinsort aa (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs \<and> (\<forall>y\<in>set xs. less a y)\<rbrakk> \<Longrightarrow> (less aa a \<longrightarrow> Ball (set xs) (less aa)) \<and> (\<not> less aa a \<longrightarrow> psorted (pinsort aa xs) \<and> (\<forall>y\<in>set (pinsort aa xs). less a y)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y\<rbrakk> \<Longrightarrow> (less aa a \<longrightarrow> (\<forall>x\<in>set xs. less aa x)) \<and> (\<not> less aa a \<longrightarrow> psorted (pinsort aa xs) \<and> (\<forall>y\<in>set (pinsort aa xs). less a y)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y\<rbrakk> \<Longrightarrow> (less aa a \<longrightarrow> (\<forall>x\<in>set xs. less aa x)) \<and> (\<not> less aa a \<longrightarrow> psorted (pinsort aa xs) \<and> less a aa) proof (prove)
goal (3 subgoals):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; less aa a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. less aa x
 2. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> psorted (pinsort aa xs)
 3. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> less a aa proof (prove)
goal (3 subgoals):
 1. \<And>a xs aa x. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; less aa a; x \<in> set xs\<rbrakk> \<Longrightarrow> less aa x
 2. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> psorted (pinsort aa xs)
 3. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> less a aa proof (prove)
goal (4 subgoals):
 1. \<And>a xs aa x. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; less aa a; x \<in> set xs\<rbrakk> \<Longrightarrow> x \<in> set xs
 2. \<And>a xs aa x. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; less aa a; x \<in> set xs; less a x\<rbrakk> \<Longrightarrow> less aa x
 3. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> psorted (pinsort aa xs)
 4. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> less a aa proof (prove)
goal (3 subgoals):
 1. \<And>a xs aa x. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; less aa a; x \<in> set xs; less a x\<rbrakk> \<Longrightarrow> less aa x
 2. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> psorted (pinsort aa xs)
 3. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> less a aa proof (prove)
goal (3 subgoals):
 1. \<And>a xs aa x. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; less aa a; x \<in> set xs; less a x; less aa x\<rbrakk> \<Longrightarrow> less aa x
 2. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> psorted (pinsort aa xs)
 3. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> less a aa proof (prove)
goal (2 subgoals):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> psorted (pinsort aa xs)
 2. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> less a aa proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> less a aa proof (prove)
goal (2 subgoals):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> R aa a
 2. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> \<not> less aa a proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. R_set (insert a (set xs)) \<Longrightarrow> psorted (pinsort a xs); R_set (insert aa (insert a (set xs))); psorted xs; \<forall>y\<in>set xs. less a y; \<not> less aa a\<rbrakk> \<Longrightarrow> \<not> less aa a proof (prove)
goal:
No subgoals!