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