1.1 --- a/src/HOL/List.thy	Wed Nov 20 08:56:54 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Nov 20 10:59:12 2013 +0100
     1.3 @@ -5390,6 +5390,176 @@
     1.4    apply (rule allI, case_tac x, simp, simp) 
     1.5    by blast
     1.6  
     1.7 +text {*
     1.8 +  Predicate version of lexicographic order integrated with Isabelle's order type classes.
     1.9 +  Author: Andreas Lochbihler
    1.10 +*}
    1.11 +
    1.12 +thm not_less
    1.13 +context ord begin
    1.14 +
    1.15 +inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.16 +where
    1.17 +  Nil: "lexordp [] (y # ys)"
    1.18 +| Cons: "x < y \<Longrightarrow> lexordp (x # xs) (y # ys)"
    1.19 +| Cons_eq:
    1.20 +  "\<lbrakk> \<not> x < y; \<not> y < x; lexordp xs ys \<rbrakk> \<Longrightarrow> lexordp (x # xs) (y # ys)"
    1.21 +
    1.22 +lemma lexordp_simps [simp]:
    1.23 +  "lexordp [] ys = (ys \<noteq> [])"
    1.24 +  "lexordp xs [] = False"
    1.25 +  "lexordp (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp xs ys"
    1.26 +by(subst lexordp.simps, fastforce simp add: neq_Nil_conv)+
    1.27 +
    1.28 +inductive lexordp_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.29 +  Nil: "lexordp_eq [] ys"
    1.30 +| Cons: "x < y \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
    1.31 +| Cons_eq: "\<lbrakk> \<not> x < y; \<not> y < x; lexordp_eq xs ys \<rbrakk> \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
    1.32 +
    1.33 +lemma lexordp_eq_simps [simp]:
    1.34 +  "lexordp_eq [] ys = True"
    1.35 +  "lexordp_eq xs [] \<longleftrightarrow> xs = []"
    1.36 +  "lexordp_eq (x # xs) [] = False"
    1.37 +  "lexordp_eq (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp_eq xs ys"
    1.38 +by(subst lexordp_eq.simps, fastforce)+
    1.39 +
    1.40 +lemma lexordp_append_rightI: "ys \<noteq> Nil \<Longrightarrow> lexordp xs (xs @ ys)"
    1.41 +by(induct xs)(auto simp add: neq_Nil_conv)
    1.42 +
    1.43 +lemma lexordp_append_left_rightI: "x < y \<Longrightarrow> lexordp (us @ x # xs) (us @ y # ys)"
    1.44 +by(induct us) auto
    1.45 +
    1.46 +lemma lexordp_eq_refl: "lexordp_eq xs xs"
    1.47 +by(induct xs) simp_all
    1.48 +
    1.49 +lemma lexordp_append_leftI: "lexordp us vs \<Longrightarrow> lexordp (xs @ us) (xs @ vs)"
    1.50 +by(induct xs) auto
    1.51 +
    1.52 +lemma lexordp_append_leftD: "\<lbrakk> lexordp (xs @ us) (xs @ vs); \<forall>a. \<not> a < a \<rbrakk> \<Longrightarrow> lexordp us vs"
    1.53 +by(induct xs) auto
    1.54 +
    1.55 +lemma lexordp_irreflexive: 
    1.56 +  assumes irrefl: "\<forall>x. \<not> x < x"
    1.57 +  shows "\<not> lexordp xs xs"
    1.58 +proof
    1.59 +  assume "lexordp xs xs"
    1.60 +  thus False by(induct xs ys\<equiv>xs)(simp_all add: irrefl)
    1.61 +qed
    1.62 +
    1.63 +lemma lexordp_into_lexordp_eq:
    1.64 +  assumes "lexordp xs ys"
    1.65 +  shows "lexordp_eq xs ys"
    1.66 +using assms by induct simp_all
    1.67 +
    1.68 +end
    1.69 +
    1.70 +declare ord.lexordp_simps [simp, code]
    1.71 +declare ord.lexordp_eq_simps [code, simp]
    1.72 +
    1.73 +lemma lexord_code [code, code_unfold]: "lexordp = ord.lexordp less"
    1.74 +unfolding lexordp_def ord.lexordp_def ..
    1.75 +
    1.76 +context order begin
    1.77 +
    1.78 +lemma lexordp_antisym:
    1.79 +  assumes "lexordp xs ys" "lexordp ys xs"
    1.80 +  shows False
    1.81 +using assms by induct auto
    1.82 +
    1.83 +lemma lexordp_irreflexive': "\<not> lexordp xs xs"
    1.84 +by(rule lexordp_irreflexive) simp
    1.85 +
    1.86 +end
    1.87 +
    1.88 +context linorder begin
    1.89 +
    1.90 +lemma lexordp_cases [consumes 1, case_names Nil Cons Cons_eq, cases pred: lexordp]:
    1.91 +  assumes "lexordp xs ys"
    1.92 +  obtains (Nil) y ys' where "xs = []" "ys = y # ys'"
    1.93 +  | (Cons) x xs' y ys' where "xs = x # xs'" "ys = y # ys'" "x < y"
    1.94 +  | (Cons_eq) x xs' ys' where "xs = x # xs'" "ys = x # ys'" "lexordp xs' ys'"
    1.95 +using assms by cases (fastforce simp add: not_less_iff_gr_or_eq)+
    1.96 +
    1.97 +lemma lexordp_induct [consumes 1, case_names Nil Cons Cons_eq, induct pred: lexordp]:
    1.98 +  assumes major: "lexordp xs ys"
    1.99 +  and Nil: "\<And>y ys. P [] (y # ys)"
   1.100 +  and Cons: "\<And>x xs y ys. x < y \<Longrightarrow> P (x # xs) (y # ys)"
   1.101 +  and Cons_eq: "\<And>x xs ys. \<lbrakk> lexordp xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x # xs) (x # ys)"
   1.102 +  shows "P xs ys"
   1.103 +using major by induct (simp_all add: Nil Cons not_less_iff_gr_or_eq Cons_eq)
   1.104 +
   1.105 +lemma lexordp_iff:
   1.106 +  "lexordp xs ys \<longleftrightarrow> (\<exists>x vs. ys = xs @ x # vs) \<or> (\<exists>us a b vs ws. a < b \<and> xs = us @ a # vs \<and> ys = us @ b # ws)"
   1.107 +  (is "?lhs = ?rhs")
   1.108 +proof
   1.109 +  assume ?lhs thus ?rhs
   1.110 +  proof induct
   1.111 +    case Cons_eq thus ?case by simp (metis append.simps(2))
   1.112 +  qed(fastforce intro: disjI2 del: disjCI intro: exI[where x="[]"])+
   1.113 +next
   1.114 +  assume ?rhs thus ?lhs
   1.115 +    by(auto intro: lexordp_append_leftI[where us="[]", simplified] lexordp_append_leftI)
   1.116 +qed
   1.117 +
   1.118 +lemma lexordp_conv_lexord:
   1.119 +  "lexordp xs ys \<longleftrightarrow> (xs, ys) \<in> lexord {(x, y). x < y}"
   1.120 +by(simp add: lexordp_iff lexord_def)
   1.121 +
   1.122 +lemma lexordp_eq_antisym: 
   1.123 +  assumes "lexordp_eq xs ys" "lexordp_eq ys xs" 
   1.124 +  shows "xs = ys"
   1.125 +using assms by induct simp_all
   1.126 +
   1.127 +lemma lexordp_eq_trans:
   1.128 +  assumes "lexordp_eq xs ys" and "lexordp_eq ys zs"
   1.129 +  shows "lexordp_eq xs zs"
   1.130 +using assms
   1.131 +apply(induct arbitrary: zs)
   1.132 +apply(case_tac [2-3] zs)
   1.133 +apply auto
   1.134 +done
   1.135 +
   1.136 +lemma lexordp_trans:
   1.137 +  assumes "lexordp xs ys" "lexordp ys zs"
   1.138 +  shows "lexordp xs zs"
   1.139 +using assms
   1.140 +apply(induct arbitrary: zs)
   1.141 +apply(case_tac [2-3] zs)
   1.142 +apply auto
   1.143 +done
   1.144 +
   1.145 +lemma lexordp_linear: "lexordp xs ys \<or> xs = ys \<or> lexordp ys xs"
   1.146 +proof(induct xs arbitrary: ys)
   1.147 +  case Nil thus ?case by(cases ys) simp_all
   1.148 +next
   1.149 +  case Cons thus ?case by(cases ys) auto
   1.150 +qed
   1.151 +
   1.152 +lemma lexordp_conv_lexordp_eq: "lexordp xs ys \<longleftrightarrow> lexordp_eq xs ys \<and> \<not> lexordp_eq ys xs"
   1.153 +  (is "?lhs \<longleftrightarrow> ?rhs")
   1.154 +proof
   1.155 +  assume ?lhs
   1.156 +  moreover hence "\<not> lexordp_eq ys xs" by induct simp_all
   1.157 +  ultimately show ?rhs by(simp add: lexordp_into_lexordp_eq)
   1.158 +next
   1.159 +  assume ?rhs
   1.160 +  hence "lexordp_eq xs ys" "\<not> lexordp_eq ys xs" by simp_all
   1.161 +  thus ?lhs by induct simp_all
   1.162 +qed
   1.163 +
   1.164 +lemma lexordp_eq_conv_lexord: "lexordp_eq xs ys \<longleftrightarrow> xs = ys \<or> lexordp xs ys"
   1.165 +by(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl dest: lexordp_eq_antisym)
   1.166 +
   1.167 +lemma lexordp_eq_linear: "lexordp_eq xs ys \<or> lexordp_eq ys xs"
   1.168 +apply(induct xs arbitrary: ys)
   1.169 +apply(case_tac [!] ys)
   1.170 +apply auto
   1.171 +done
   1.172 +
   1.173 +lemma lexordp_linorder: "class.linorder lexordp_eq lexordp"
   1.174 +by unfold_locales(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl lexordp_eq_antisym intro: lexordp_eq_trans del: disjCI intro: lexordp_eq_linear)
   1.175 +
   1.176 +end
   1.177  
   1.178  subsubsection {* Lexicographic combination of measure functions *}
   1.179