src/HOL/UNITY/ListOrder.thy
 author kuncar Fri Dec 09 18:07:04 2011 +0100 (2011-12-09) changeset 45802 b16f976db515 parent 45477 11d9c2768729 child 46577 e5438c5797ae permissions -rw-r--r--
Quotient_Info stores only relation maps
```     1 (*  Title:      HOL/UNITY/ListOrder.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1998  University of Cambridge
```
```     4
```
```     5 Lists are partially ordered by Charpentier's Generalized Prefix Relation
```
```     6    (xs,ys) : genPrefix(r)
```
```     7      if ys = xs' @ zs where length xs = length xs'
```
```     8      and corresponding elements of xs, xs' are pairwise related by r
```
```     9
```
```    10 Also overloads <= and < for lists!
```
```    11 *)
```
```    12
```
```    13 header {*The Prefix Ordering on Lists*}
```
```    14
```
```    15 theory ListOrder
```
```    16 imports Main
```
```    17 begin
```
```    18
```
```    19 inductive_set
```
```    20   genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
```
```    21   for r :: "('a * 'a)set"
```
```    22  where
```
```    23    Nil:     "([],[]) : genPrefix(r)"
```
```    24
```
```    25  | prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
```
```    26              (x#xs, y#ys) : genPrefix(r)"
```
```    27
```
```    28  | append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
```
```    29
```
```    30 instantiation list :: (type) ord
```
```    31 begin
```
```    32
```
```    33 definition
```
```    34   prefix_def:        "xs <= zs \<longleftrightarrow>  (xs, zs) : genPrefix Id"
```
```    35
```
```    36 definition
```
```    37   strict_prefix_def: "xs < zs  \<longleftrightarrow>  xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)"
```
```    38
```
```    39 instance ..
```
```    40
```
```    41 (*Constants for the <= and >= relations, used below in translations*)
```
```    42
```
```    43 end
```
```    44
```
```    45 definition Le :: "(nat*nat) set" where
```
```    46     "Le == {(x,y). x <= y}"
```
```    47
```
```    48 definition  Ge :: "(nat*nat) set" where
```
```    49     "Ge == {(x,y). y <= x}"
```
```    50
```
```    51 abbreviation
```
```    52   pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
```
```    53   "xs pfixLe ys == (xs,ys) : genPrefix Le"
```
```    54
```
```    55 abbreviation
```
```    56   pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
```
```    57   "xs pfixGe ys == (xs,ys) : genPrefix Ge"
```
```    58
```
```    59
```
```    60 subsection{*preliminary lemmas*}
```
```    61
```
```    62 lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
```
```    63 by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)
```
```    64
```
```    65 lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys"
```
```    66 by (erule genPrefix.induct, auto)
```
```    67
```
```    68 lemma cdlemma:
```
```    69      "[| (xs', ys'): genPrefix r |]
```
```    70       ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"
```
```    71 apply (erule genPrefix.induct, blast, blast)
```
```    72 apply (force intro: genPrefix.append)
```
```    73 done
```
```    74
```
```    75 (*As usual converting it to an elimination rule is tiresome*)
```
```    76 lemma cons_genPrefixE [elim!]:
```
```    77      "[| (x#xs, zs): genPrefix r;
```
```    78          !!y ys. [| zs = y#ys;  (x,y) : r;  (xs, ys) : genPrefix r |] ==> P
```
```    79       |] ==> P"
```
```    80 by (drule cdlemma, simp, blast)
```
```    81
```
```    82 lemma Cons_genPrefix_Cons [iff]:
```
```    83      "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"
```
```    84 by (blast intro: genPrefix.prepend)
```
```    85
```
```    86
```
```    87 subsection{*genPrefix is a partial order*}
```
```    88
```
```    89 lemma refl_genPrefix: "refl r ==> refl (genPrefix r)"
```
```    90 apply (unfold refl_on_def, auto)
```
```    91 apply (induct_tac "x")
```
```    92 prefer 2 apply (blast intro: genPrefix.prepend)
```
```    93 apply (blast intro: genPrefix.Nil)
```
```    94 done
```
```    95
```
```    96 lemma genPrefix_refl [simp]: "refl r ==> (l,l) : genPrefix r"
```
```    97 by (erule refl_onD [OF refl_genPrefix UNIV_I])
```
```    98
```
```    99 lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
```
```   100 apply clarify
```
```   101 apply (erule genPrefix.induct)
```
```   102 apply (auto intro: genPrefix.append)
```
```   103 done
```
```   104
```
```   105
```
```   106 (** Transitivity **)
```
```   107
```
```   108 (*A lemma for proving genPrefix_trans_O*)
```
```   109 lemma append_genPrefix:
```
```   110      "(xs @ ys, zs) : genPrefix r \<Longrightarrow> (xs, zs) : genPrefix r"
```
```   111   by (induct xs arbitrary: zs) auto
```
```   112
```
```   113 (*Lemma proving transitivity and more*)
```
```   114 lemma genPrefix_trans_O:
```
```   115   assumes "(x, y) : genPrefix r"
```
```   116   shows "\<And>z. (y, z) : genPrefix s \<Longrightarrow> (x, z) : genPrefix (r O s)"
```
```   117   apply (atomize (full))
```
```   118   using assms
```
```   119   apply induct
```
```   120     apply blast
```
```   121    apply (blast intro: genPrefix.prepend)
```
```   122   apply (blast dest: append_genPrefix)
```
```   123   done
```
```   124
```
```   125 lemma genPrefix_trans:
```
```   126   "(x, y) : genPrefix r \<Longrightarrow> (y, z) : genPrefix r \<Longrightarrow> trans r
```
```   127     \<Longrightarrow> (x, z) : genPrefix r"
```
```   128   apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
```
```   129    apply assumption
```
```   130   apply (blast intro: genPrefix_trans_O)
```
```   131   done
```
```   132
```
```   133 lemma prefix_genPrefix_trans:
```
```   134   "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
```
```   135 apply (unfold prefix_def)
```
```   136 apply (drule genPrefix_trans_O, assumption)
```
```   137 apply simp
```
```   138 done
```
```   139
```
```   140 lemma genPrefix_prefix_trans:
```
```   141   "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
```
```   142 apply (unfold prefix_def)
```
```   143 apply (drule genPrefix_trans_O, assumption)
```
```   144 apply simp
```
```   145 done
```
```   146
```
```   147 lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
```
```   148 by (blast intro: transI genPrefix_trans)
```
```   149
```
```   150
```
```   151 (** Antisymmetry **)
```
```   152
```
```   153 lemma genPrefix_antisym:
```
```   154   assumes 1: "(xs, ys) : genPrefix r"
```
```   155     and 2: "antisym r"
```
```   156     and 3: "(ys, xs) : genPrefix r"
```
```   157   shows "xs = ys"
```
```   158   using 1 3
```
```   159 proof induct
```
```   160   case Nil
```
```   161   then show ?case by blast
```
```   162 next
```
```   163   case prepend
```
```   164   then show ?case using 2 by (simp add: antisym_def)
```
```   165 next
```
```   166   case (append xs ys zs)
```
```   167   then show ?case
```
```   168     apply -
```
```   169     apply (subgoal_tac "length zs = 0", force)
```
```   170     apply (drule genPrefix_length_le)+
```
```   171     apply (simp del: length_0_conv)
```
```   172     done
```
```   173 qed
```
```   174
```
```   175 lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
```
```   176   by (blast intro: antisymI genPrefix_antisym)
```
```   177
```
```   178
```
```   179 subsection{*recursion equations*}
```
```   180
```
```   181 lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
```
```   182 apply (induct_tac "xs")
```
```   183 prefer 2 apply blast
```
```   184 apply simp
```
```   185 done
```
```   186
```
```   187 lemma same_genPrefix_genPrefix [simp]:
```
```   188     "refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
```
```   189 apply (unfold refl_on_def)
```
```   190 apply (induct_tac "xs")
```
```   191 apply (simp_all (no_asm_simp))
```
```   192 done
```
```   193
```
```   194 lemma genPrefix_Cons:
```
```   195      "((xs, y#ys) : genPrefix r) =
```
```   196       (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
```
```   197 by (case_tac "xs", auto)
```
```   198
```
```   199 lemma genPrefix_take_append:
```
```   200      "[| refl r;  (xs,ys) : genPrefix r |]
```
```   201       ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
```
```   202 apply (erule genPrefix.induct)
```
```   203 apply (frule_tac  genPrefix_length_le)
```
```   204 apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
```
```   205 done
```
```   206
```
```   207 lemma genPrefix_append_both:
```
```   208      "[| refl r;  (xs,ys) : genPrefix r;  length xs = length ys |]
```
```   209       ==>  (xs@zs, ys @ zs) : genPrefix r"
```
```   210 apply (drule genPrefix_take_append, assumption)
```
```   211 apply (simp add: take_all)
```
```   212 done
```
```   213
```
```   214
```
```   215 (*NOT suitable for rewriting since [y] has the form y#ys*)
```
```   216 lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
```
```   217 by auto
```
```   218
```
```   219 lemma aolemma:
```
```   220      "[| (xs,ys) : genPrefix r;  refl r |]
```
```   221       ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
```
```   222 apply (erule genPrefix.induct)
```
```   223   apply blast
```
```   224  apply simp
```
```   225 txt{*Append case is hardest*}
```
```   226 apply simp
```
```   227 apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
```
```   228 apply (erule disjE)
```
```   229 apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
```
```   230 apply (blast intro: genPrefix.append, auto)
```
```   231 apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append)
```
```   232 done
```
```   233
```
```   234 lemma append_one_genPrefix:
```
```   235      "[| (xs,ys) : genPrefix r;  length xs < length ys;  refl r |]
```
```   236       ==> (xs @ [ys ! length xs], ys) : genPrefix r"
```
```   237 by (blast intro: aolemma [THEN mp])
```
```   238
```
```   239
```
```   240 (** Proving the equivalence with Charpentier's definition **)
```
```   241
```
```   242 lemma genPrefix_imp_nth:
```
```   243     "i < length xs \<Longrightarrow> (xs, ys) : genPrefix r \<Longrightarrow> (xs ! i, ys ! i) : r"
```
```   244   apply (induct xs arbitrary: i ys)
```
```   245    apply auto
```
```   246   apply (case_tac i)
```
```   247    apply auto
```
```   248   done
```
```   249
```
```   250 lemma nth_imp_genPrefix:
```
```   251   "length xs <= length ys \<Longrightarrow>
```
```   252      (\<forall>i. i < length xs --> (xs ! i, ys ! i) : r) \<Longrightarrow>
```
```   253      (xs, ys) : genPrefix r"
```
```   254   apply (induct xs arbitrary: ys)
```
```   255    apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib)
```
```   256   apply (case_tac ys)
```
```   257    apply (force+)
```
```   258   done
```
```   259
```
```   260 lemma genPrefix_iff_nth:
```
```   261      "((xs,ys) : genPrefix r) =
```
```   262       (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"
```
```   263 apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
```
```   264 done
```
```   265
```
```   266
```
```   267 subsection{*The type of lists is partially ordered*}
```
```   268
```
```   269 declare refl_Id [iff]
```
```   270         antisym_Id [iff]
```
```   271         trans_Id [iff]
```
```   272
```
```   273 lemma prefix_refl [iff]: "xs <= (xs::'a list)"
```
```   274 by (simp add: prefix_def)
```
```   275
```
```   276 lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
```
```   277 apply (unfold prefix_def)
```
```   278 apply (blast intro: genPrefix_trans)
```
```   279 done
```
```   280
```
```   281 lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
```
```   282 apply (unfold prefix_def)
```
```   283 apply (blast intro: genPrefix_antisym)
```
```   284 done
```
```   285
```
```   286 lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)"
```
```   287 by (unfold strict_prefix_def, auto)
```
```   288
```
```   289 instance list :: (type) order
```
```   290   by (intro_classes,
```
```   291       (assumption | rule prefix_refl prefix_trans prefix_antisym
```
```   292                      prefix_less_le_not_le)+)
```
```   293
```
```   294 (*Monotonicity of "set" operator WRT prefix*)
```
```   295 lemma set_mono: "xs <= ys ==> set xs <= set ys"
```
```   296 apply (unfold prefix_def)
```
```   297 apply (erule genPrefix.induct, auto)
```
```   298 done
```
```   299
```
```   300
```
```   301 (** recursion equations **)
```
```   302
```
```   303 lemma Nil_prefix [iff]: "[] <= xs"
```
```   304 apply (unfold prefix_def)
```
```   305 apply (simp add: Nil_genPrefix)
```
```   306 done
```
```   307
```
```   308 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
```
```   309 apply (unfold prefix_def)
```
```   310 apply (simp add: genPrefix_Nil)
```
```   311 done
```
```   312
```
```   313 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
```
```   314 by (simp add: prefix_def)
```
```   315
```
```   316 lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
```
```   317 by (simp add: prefix_def)
```
```   318
```
```   319 lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
```
```   320 by (insert same_prefix_prefix [of xs ys "[]"], simp)
```
```   321
```
```   322 lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
```
```   323 apply (unfold prefix_def)
```
```   324 apply (erule genPrefix.append)
```
```   325 done
```
```   326
```
```   327 lemma prefix_Cons:
```
```   328    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"
```
```   329 by (simp add: prefix_def genPrefix_Cons)
```
```   330
```
```   331 lemma append_one_prefix:
```
```   332   "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
```
```   333 apply (unfold prefix_def)
```
```   334 apply (simp add: append_one_genPrefix)
```
```   335 done
```
```   336
```
```   337 lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
```
```   338 apply (unfold prefix_def)
```
```   339 apply (erule genPrefix_length_le)
```
```   340 done
```
```   341
```
```   342 lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
```
```   343 apply (unfold prefix_def)
```
```   344 apply (erule genPrefix.induct, auto)
```
```   345 done
```
```   346
```
```   347 lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
```
```   348 apply (unfold strict_prefix_def)
```
```   349 apply (blast intro: splemma [THEN mp])
```
```   350 done
```
```   351
```
```   352 lemma mono_length: "mono length"
```
```   353 by (blast intro: monoI prefix_length_le)
```
```   354
```
```   355 (*Equivalence to the definition used in Lex/Prefix.thy*)
```
```   356 lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"
```
```   357 apply (unfold prefix_def)
```
```   358 apply (auto simp add: genPrefix_iff_nth nth_append)
```
```   359 apply (rule_tac x = "drop (length xs) zs" in exI)
```
```   360 apply (rule nth_equalityI)
```
```   361 apply (simp_all (no_asm_simp) add: nth_append)
```
```   362 done
```
```   363
```
```   364 lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
```
```   365 apply (simp add: prefix_iff)
```
```   366 apply (rule iffI)
```
```   367  apply (erule exE)
```
```   368  apply (rename_tac "zs")
```
```   369  apply (rule_tac xs = zs in rev_exhaust)
```
```   370   apply simp
```
```   371  apply clarify
```
```   372  apply (simp del: append_assoc add: append_assoc [symmetric], force)
```
```   373 done
```
```   374
```
```   375 lemma prefix_append_iff:
```
```   376      "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"
```
```   377 apply (rule_tac xs = zs in rev_induct)
```
```   378  apply force
```
```   379 apply (simp del: append_assoc add: append_assoc [symmetric], force)
```
```   380 done
```
```   381
```
```   382 (*Although the prefix ordering is not linear, the prefixes of a list
```
```   383   are linearly ordered.*)
```
```   384 lemma common_prefix_linear:
```
```   385   fixes xs ys zs :: "'a list"
```
```   386   shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs"
```
```   387   by (induct zs rule: rev_induct) auto
```
```   388
```
```   389 subsection{*pfixLe, pfixGe: properties inherited from the translations*}
```
```   390
```
```   391 (** pfixLe **)
```
```   392
```
```   393 lemma refl_Le [iff]: "refl Le"
```
```   394 by (unfold refl_on_def Le_def, auto)
```
```   395
```
```   396 lemma antisym_Le [iff]: "antisym Le"
```
```   397 by (unfold antisym_def Le_def, auto)
```
```   398
```
```   399 lemma trans_Le [iff]: "trans Le"
```
```   400 by (unfold trans_def Le_def, auto)
```
```   401
```
```   402 lemma pfixLe_refl [iff]: "x pfixLe x"
```
```   403 by simp
```
```   404
```
```   405 lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
```
```   406 by (blast intro: genPrefix_trans)
```
```   407
```
```   408 lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
```
```   409 by (blast intro: genPrefix_antisym)
```
```   410
```
```   411 lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
```
```   412 apply (unfold prefix_def Le_def)
```
```   413 apply (blast intro: genPrefix_mono [THEN  rev_subsetD])
```
```   414 done
```
```   415
```
```   416 lemma refl_Ge [iff]: "refl Ge"
```
```   417 by (unfold refl_on_def Ge_def, auto)
```
```   418
```
```   419 lemma antisym_Ge [iff]: "antisym Ge"
```
```   420 by (unfold antisym_def Ge_def, auto)
```
```   421
```
```   422 lemma trans_Ge [iff]: "trans Ge"
```
```   423 by (unfold trans_def Ge_def, auto)
```
```   424
```
```   425 lemma pfixGe_refl [iff]: "x pfixGe x"
```
```   426 by simp
```
```   427
```
```   428 lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
```
```   429 by (blast intro: genPrefix_trans)
```
```   430
```
```   431 lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
```
```   432 by (blast intro: genPrefix_antisym)
```
```   433
```
```   434 lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
```
```   435 apply (unfold prefix_def Ge_def)
```
```   436 apply (blast intro: genPrefix_mono [THEN  rev_subsetD])
```
```   437 done
```
```   438
```
```   439 end
```