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