theory ListLibLemmas

lemma psorted_distinct_set_unique:
assumes "psorted xs" "distinct xs" "psorted ys" "distinct ys" "set xs = set ys"
        "R_list xs"
shows "xs = ys" proof - from assms have 1: "length xs = length ys" by (auto dest!: distinct_card) from assms show ?thesis proof(induct rule:list_induct2[OF 1]) case 1 show ?case by simp next case 2 thus ?case by (simp add: psorted_Cons R_set_def)
         (metis Diff_insert_absorb antisym insertE insert_iff) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs = ys proof (state)
goal (1 subgoal):
 1. xs = ys proof (chain)
picking this:
psorted xs
distinct xs
psorted ys
distinct ys
set xs = set ys
R_list xs proof (prove)
using this:
psorted xs
distinct xs
psorted ys
distinct ys
set xs = set ys
R_list xs

goal (1 subgoal):
 1. length xs = length ys proof (state)
this:
length xs = length ys

goal (1 subgoal):
 1. xs = ys proof (chain)
picking this:
psorted xs
distinct xs
psorted ys
distinct ys
set xs = set ys
R_list xs proof (prove)
using this:
psorted xs
distinct xs
psorted ys
distinct ys
set xs = set ys
R_list xs

goal (1 subgoal):
 1. xs = ys proof (state)
goal (2 subgoals):
 1. \<lbrakk>psorted []; distinct []; psorted []; distinct []; set [] = set []; R_list []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>psorted xs; distinct xs; psorted ys; distinct ys; set xs = set ys; R_list xs\<rbrakk> \<Longrightarrow> xs = ys; psorted (x # xs); distinct (x # xs); psorted (y # ys); distinct (y # ys); set (x # xs) = set (y # ys); R_list (x # xs)\<rbrakk> \<Longrightarrow> x # xs = y # ys proof (state)
this:
psorted []
distinct []
psorted []
distinct []
set [] = set []
R_list []

goal (2 subgoals):
 1. \<lbrakk>psorted []; distinct []; psorted []; distinct []; set [] = set []; R_list []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>psorted xs; distinct xs; psorted ys; distinct ys; set xs = set ys; R_list xs\<rbrakk> \<Longrightarrow> xs = ys; psorted (x # xs); distinct (x # xs); psorted (y # ys); distinct (y # ys); set (x # xs) = set (y # ys); R_list (x # xs)\<rbrakk> \<Longrightarrow> x # xs = y # ys proof (prove)
goal (1 subgoal):
 1. [] = [] proof (state)
this:
[] = []

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>psorted xs; distinct xs; psorted ys; distinct ys; set xs = set ys; R_list xs\<rbrakk> \<Longrightarrow> xs = ys; psorted (x # xs); distinct (x # xs); psorted (y # ys); distinct (y # ys); set (x # xs) = set (y # ys); R_list (x # xs)\<rbrakk> \<Longrightarrow> x # xs = y # ys proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>psorted xs; distinct xs; psorted ys; distinct ys; set xs = set ys; R_list xs\<rbrakk> \<Longrightarrow> xs = ys; psorted (x # xs); distinct (x # xs); psorted (y # ys); distinct (y # ys); set (x # xs) = set (y # ys); R_list (x # xs)\<rbrakk> \<Longrightarrow> x # xs = y # ys proof (state)
this:
length xs_ = length ys_
\<lbrakk>psorted xs_; distinct xs_; psorted ys_; distinct ys_; set xs_ = set ys_; R_list xs_\<rbrakk> \<Longrightarrow> xs_ = ys_
psorted (x_ # xs_)
distinct (x_ # xs_)
psorted (y_ # ys_)
distinct (y_ # ys_)
set (x_ # xs_) = set (y_ # ys_)
R_list (x_ # xs_)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>psorted xs; distinct xs; psorted ys; distinct ys; set xs = set ys; R_list xs\<rbrakk> \<Longrightarrow> xs = ys; psorted (x # xs); distinct (x # xs); psorted (y # ys); distinct (y # ys); set (x # xs) = set (y # ys); R_list (x # xs)\<rbrakk> \<Longrightarrow> x # xs = y # ys proof (prove)
using this:
length xs_ = length ys_
\<lbrakk>psorted xs_; distinct xs_; psorted ys_; distinct ys_; set xs_ = set ys_; R_list xs_\<rbrakk> \<Longrightarrow> xs_ = ys_
psorted (x_ # xs_)
distinct (x_ # xs_)
psorted (y_ # ys_)
distinct (y_ # ys_)
set (x_ # xs_) = set (y_ # ys_)
R_list (x_ # xs_)

goal (1 subgoal):
 1. x_ # xs_ = y_ # ys_ proof (state)
this:
x_ # xs_ = y_ # ys_

goal:
No subgoals! proof (state)
this:
xs = ys

goal:
No subgoals!