src/HOL/UNITY/ListOrder.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35416 d8d7d1b785af
child 45477 11d9c2768729
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     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 [rule_format]:
   110      "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
   111 by (induct_tac "xs", auto)
   112 
   113 (*Lemma proving transitivity and more*)
   114 lemma genPrefix_trans_O [rule_format]: 
   115      "(x, y) : genPrefix r  
   116       ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
   117 apply (erule genPrefix.induct)
   118   prefer 3 apply (blast dest: append_genPrefix)
   119  prefer 2 apply (blast intro: genPrefix.prepend, blast)
   120 done
   121 
   122 lemma genPrefix_trans [rule_format]:
   123      "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]  
   124       ==> (x,z) : genPrefix r"
   125 apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
   126  apply assumption
   127 apply (blast intro: genPrefix_trans_O)
   128 done
   129 
   130 lemma prefix_genPrefix_trans [rule_format]: 
   131      "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
   132 apply (unfold prefix_def)
   133 apply (drule genPrefix_trans_O, assumption)
   134 apply simp
   135 done
   136 
   137 lemma genPrefix_prefix_trans [rule_format]: 
   138      "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
   139 apply (unfold prefix_def)
   140 apply (drule genPrefix_trans_O, assumption)
   141 apply simp
   142 done
   143 
   144 lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
   145 by (blast intro: transI genPrefix_trans)
   146 
   147 
   148 (** Antisymmetry **)
   149 
   150 lemma genPrefix_antisym [rule_format]:
   151      "[| (xs,ys) : genPrefix r;  antisym r |]  
   152       ==> (ys,xs) : genPrefix r --> xs = ys"
   153 apply (erule genPrefix.induct)
   154   txt{*Base case*}
   155   apply blast
   156  txt{*prepend case*}
   157  apply (simp add: antisym_def)
   158 txt{*append case is the hardest*}
   159 apply clarify
   160 apply (subgoal_tac "length zs = 0", force)
   161 apply (drule genPrefix_length_le)+
   162 apply (simp del: length_0_conv)
   163 done
   164 
   165 lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
   166 by (blast intro: antisymI genPrefix_antisym)
   167 
   168 
   169 subsection{*recursion equations*}
   170 
   171 lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
   172 apply (induct_tac "xs")
   173 prefer 2 apply blast
   174 apply simp
   175 done
   176 
   177 lemma same_genPrefix_genPrefix [simp]: 
   178     "refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
   179 apply (unfold refl_on_def)
   180 apply (induct_tac "xs")
   181 apply (simp_all (no_asm_simp))
   182 done
   183 
   184 lemma genPrefix_Cons:
   185      "((xs, y#ys) : genPrefix r) =  
   186       (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
   187 by (case_tac "xs", auto)
   188 
   189 lemma genPrefix_take_append:
   190      "[| refl r;  (xs,ys) : genPrefix r |]  
   191       ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
   192 apply (erule genPrefix.induct)
   193 apply (frule_tac [3] genPrefix_length_le)
   194 apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
   195 done
   196 
   197 lemma genPrefix_append_both:
   198      "[| refl r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
   199       ==>  (xs@zs, ys @ zs) : genPrefix r"
   200 apply (drule genPrefix_take_append, assumption)
   201 apply (simp add: take_all)
   202 done
   203 
   204 
   205 (*NOT suitable for rewriting since [y] has the form y#ys*)
   206 lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
   207 by auto
   208 
   209 lemma aolemma:
   210      "[| (xs,ys) : genPrefix r;  refl r |]  
   211       ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
   212 apply (erule genPrefix.induct)
   213   apply blast
   214  apply simp
   215 txt{*Append case is hardest*}
   216 apply simp
   217 apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
   218 apply (erule disjE)
   219 apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
   220 apply (blast intro: genPrefix.append, auto)
   221 apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append)
   222 done
   223 
   224 lemma append_one_genPrefix:
   225      "[| (xs,ys) : genPrefix r;  length xs < length ys;  refl r |]  
   226       ==> (xs @ [ys ! length xs], ys) : genPrefix r"
   227 by (blast intro: aolemma [THEN mp])
   228 
   229 
   230 (** Proving the equivalence with Charpentier's definition **)
   231 
   232 lemma genPrefix_imp_nth [rule_format]:
   233      "ALL i ys. i < length xs  
   234                 --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
   235 apply (induct_tac "xs", auto)
   236 apply (case_tac "i", auto)
   237 done
   238 
   239 lemma nth_imp_genPrefix [rule_format]:
   240      "ALL ys. length xs <= length ys   
   241       --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)   
   242       --> (xs, ys) : genPrefix r"
   243 apply (induct_tac "xs")
   244 apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
   245 apply clarify
   246 apply (case_tac "ys")
   247 apply (force+)
   248 done
   249 
   250 lemma genPrefix_iff_nth:
   251      "((xs,ys) : genPrefix r) =  
   252       (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"
   253 apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
   254 done
   255 
   256 
   257 subsection{*The type of lists is partially ordered*}
   258 
   259 declare refl_Id [iff] 
   260         antisym_Id [iff] 
   261         trans_Id [iff]
   262 
   263 lemma prefix_refl [iff]: "xs <= (xs::'a list)"
   264 by (simp add: prefix_def)
   265 
   266 lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
   267 apply (unfold prefix_def)
   268 apply (blast intro: genPrefix_trans)
   269 done
   270 
   271 lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
   272 apply (unfold prefix_def)
   273 apply (blast intro: genPrefix_antisym)
   274 done
   275 
   276 lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)"
   277 by (unfold strict_prefix_def, auto)
   278 
   279 instance list :: (type) order
   280   by (intro_classes,
   281       (assumption | rule prefix_refl prefix_trans prefix_antisym
   282                      prefix_less_le_not_le)+)
   283 
   284 (*Monotonicity of "set" operator WRT prefix*)
   285 lemma set_mono: "xs <= ys ==> set xs <= set ys"
   286 apply (unfold prefix_def)
   287 apply (erule genPrefix.induct, auto)
   288 done
   289 
   290 
   291 (** recursion equations **)
   292 
   293 lemma Nil_prefix [iff]: "[] <= xs"
   294 apply (unfold prefix_def)
   295 apply (simp add: Nil_genPrefix)
   296 done
   297 
   298 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
   299 apply (unfold prefix_def)
   300 apply (simp add: genPrefix_Nil)
   301 done
   302 
   303 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
   304 by (simp add: prefix_def)
   305 
   306 lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
   307 by (simp add: prefix_def)
   308 
   309 lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
   310 by (insert same_prefix_prefix [of xs ys "[]"], simp)
   311 
   312 lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
   313 apply (unfold prefix_def)
   314 apply (erule genPrefix.append)
   315 done
   316 
   317 lemma prefix_Cons: 
   318    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"
   319 by (simp add: prefix_def genPrefix_Cons)
   320 
   321 lemma append_one_prefix: 
   322   "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
   323 apply (unfold prefix_def)
   324 apply (simp add: append_one_genPrefix)
   325 done
   326 
   327 lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
   328 apply (unfold prefix_def)
   329 apply (erule genPrefix_length_le)
   330 done
   331 
   332 lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
   333 apply (unfold prefix_def)
   334 apply (erule genPrefix.induct, auto)
   335 done
   336 
   337 lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
   338 apply (unfold strict_prefix_def)
   339 apply (blast intro: splemma [THEN mp])
   340 done
   341 
   342 lemma mono_length: "mono length"
   343 by (blast intro: monoI prefix_length_le)
   344 
   345 (*Equivalence to the definition used in Lex/Prefix.thy*)
   346 lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"
   347 apply (unfold prefix_def)
   348 apply (auto simp add: genPrefix_iff_nth nth_append)
   349 apply (rule_tac x = "drop (length xs) zs" in exI)
   350 apply (rule nth_equalityI)
   351 apply (simp_all (no_asm_simp) add: nth_append)
   352 done
   353 
   354 lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
   355 apply (simp add: prefix_iff)
   356 apply (rule iffI)
   357  apply (erule exE)
   358  apply (rename_tac "zs")
   359  apply (rule_tac xs = zs in rev_exhaust)
   360   apply simp
   361  apply clarify
   362  apply (simp del: append_assoc add: append_assoc [symmetric], force)
   363 done
   364 
   365 lemma prefix_append_iff:
   366      "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"
   367 apply (rule_tac xs = zs in rev_induct)
   368  apply force
   369 apply (simp del: append_assoc add: append_assoc [symmetric], force)
   370 done
   371 
   372 (*Although the prefix ordering is not linear, the prefixes of a list
   373   are linearly ordered.*)
   374 lemma common_prefix_linear [rule_format]:
   375      "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
   376 by (rule_tac xs = zs in rev_induct, auto)
   377 
   378 
   379 subsection{*pfixLe, pfixGe: properties inherited from the translations*}
   380 
   381 (** pfixLe **)
   382 
   383 lemma refl_Le [iff]: "refl Le"
   384 by (unfold refl_on_def Le_def, auto)
   385 
   386 lemma antisym_Le [iff]: "antisym Le"
   387 by (unfold antisym_def Le_def, auto)
   388 
   389 lemma trans_Le [iff]: "trans Le"
   390 by (unfold trans_def Le_def, auto)
   391 
   392 lemma pfixLe_refl [iff]: "x pfixLe x"
   393 by simp
   394 
   395 lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
   396 by (blast intro: genPrefix_trans)
   397 
   398 lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
   399 by (blast intro: genPrefix_antisym)
   400 
   401 lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
   402 apply (unfold prefix_def Le_def)
   403 apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
   404 done
   405 
   406 lemma refl_Ge [iff]: "refl Ge"
   407 by (unfold refl_on_def Ge_def, auto)
   408 
   409 lemma antisym_Ge [iff]: "antisym Ge"
   410 by (unfold antisym_def Ge_def, auto)
   411 
   412 lemma trans_Ge [iff]: "trans Ge"
   413 by (unfold trans_def Ge_def, auto)
   414 
   415 lemma pfixGe_refl [iff]: "x pfixGe x"
   416 by simp
   417 
   418 lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
   419 by (blast intro: genPrefix_trans)
   420 
   421 lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
   422 by (blast intro: genPrefix_antisym)
   423 
   424 lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
   425 apply (unfold prefix_def Ge_def)
   426 apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
   427 done
   428 
   429 end