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