wneuper/isa: src/HOL/UNITY/ListOrder.thy@e5438c5797ae

     1 (*  Title:      HOL/UNITY/ListOrder.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1998  University of Cambridge

     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

    10 Also overloads <= and < for lists!

    11 *)

    13 header {*The Prefix Ordering on Lists*}

    15 theory ListOrder

    16 imports Main

    17 begin

    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)"

    25  | prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>

    26              (x#xs, y#ys) : genPrefix(r)"

    28  | append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"

    30 instantiation list :: (type) ord

    31 begin

    33 definition

    34   prefix_def:        "xs <= zs \<longleftrightarrow>  (xs, zs) : genPrefix Id"

    36 definition

    37   strict_prefix_def: "xs < zs  \<longleftrightarrow>  xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)"

    39 instance ..

    41 (*Constants for the <= and >= relations, used below in translations*)

    43 end

    45 definition Le :: "(nat*nat) set" where

    46     "Le == {(x,y). x <= y}"

    48 definition  Ge :: "(nat*nat) set" where

    49     "Ge == {(x,y). y <= x}"

    51 abbreviation

    52   pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where

    53   "xs pfixLe ys == (xs,ys) : genPrefix Le"

    55 abbreviation

    56   pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where

    57   "xs pfixGe ys == (xs,ys) : genPrefix Ge"

    60 subsection{*preliminary lemmas*}

    62 lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"

    63 by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)

    65 lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys"

    66 by (erule genPrefix.induct, auto)

    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

    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)

    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)

    87 subsection{*genPrefix is a partial order*}

    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

    96 lemma genPrefix_refl [simp]: "refl r ==> (l,l) : genPrefix r"

    97 by (erule refl_onD [OF refl_genPrefix UNIV_I])

    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

   106 (** Transitivity **)

   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

   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

   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

   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

   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

   147 lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"

   148 by (blast intro: transI genPrefix_trans)

   151 (** Antisymmetry **)

   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

   175 lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"

   176   by (blast intro: antisymI genPrefix_antisym)

   179 subsection{*recursion equations*}

   181 lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"

   182 apply (induct_tac "xs")

   183 prefer 2 apply blast

   184 apply simp

   185 done

   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

   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)

   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 [3] genPrefix_length_le)

   204 apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])

   205 done

   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

   212 done

   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

   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

   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])

   240 (** Proving the equivalence with Charpentier's definition **)

   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

   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

   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

   267 subsection{*The type of lists is partially ordered*}

   269 declare refl_Id [iff]

   270         antisym_Id [iff]

   271         trans_Id [iff]

   273 lemma prefix_refl [iff]: "xs <= (xs::'a list)"

   274 by (simp add: prefix_def)

   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

   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

   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)

   289 instance list :: (type) order

   290   by (intro_classes,

   291       (assumption | rule prefix_refl prefix_trans prefix_antisym

   292                      prefix_less_le_not_le)+)

   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

   301 (** recursion equations **)

   303 lemma Nil_prefix [iff]: "[] <= xs"

   304 by (simp add: prefix_def)

   306 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"

   307 by (simp add: prefix_def)

   309 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"

   310 by (simp add: prefix_def)

   312 lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"

   313 by (simp add: prefix_def)

   315 lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"

   316 by (insert same_prefix_prefix [of xs ys "[]"], simp)

   318 lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"

   319 apply (unfold prefix_def)

   320 apply (erule genPrefix.append)

   321 done

   323 lemma prefix_Cons:

   324    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"

   325 by (simp add: prefix_def genPrefix_Cons)

   327 lemma append_one_prefix:

   328   "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"

   329 apply (unfold prefix_def)

   330 apply (simp add: append_one_genPrefix)

   331 done

   333 lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"

   334 apply (unfold prefix_def)

   335 apply (erule genPrefix_length_le)

   336 done

   338 lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"

   339 apply (unfold prefix_def)

   340 apply (erule genPrefix.induct, auto)

   341 done

   343 lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"

   344 apply (unfold strict_prefix_def)

   345 apply (blast intro: splemma [THEN mp])

   346 done

   348 lemma mono_length: "mono length"

   349 by (blast intro: monoI prefix_length_le)

   351 (*Equivalence to the definition used in Lex/Prefix.thy*)

   352 lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"

   353 apply (unfold prefix_def)

   354 apply (auto simp add: genPrefix_iff_nth nth_append)

   355 apply (rule_tac x = "drop (length xs) zs" in exI)

   356 apply (rule nth_equalityI)

   357 apply (simp_all (no_asm_simp) add: nth_append)

   358 done

   360 lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"

   361 apply (simp add: prefix_iff)

   362 apply (rule iffI)

   363  apply (erule exE)

   364  apply (rename_tac "zs")

   365  apply (rule_tac xs = zs in rev_exhaust)

   366   apply simp

   367  apply clarify

   368  apply (simp del: append_assoc add: append_assoc [symmetric], force)

   369 done

   371 lemma prefix_append_iff:

   372      "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"

   373 apply (rule_tac xs = zs in rev_induct)

   374  apply force

   375 apply (simp del: append_assoc add: append_assoc [symmetric], force)

   376 done

   378 (*Although the prefix ordering is not linear, the prefixes of a list

   379   are linearly ordered.*)

   380 lemma common_prefix_linear:

   381   fixes xs ys zs :: "'a list"

   382   shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs"

   383   by (induct zs rule: rev_induct) auto

   385 subsection{*pfixLe, pfixGe: properties inherited from the translations*}

   387 (** pfixLe **)

   389 lemma refl_Le [iff]: "refl Le"

   390 by (unfold refl_on_def Le_def, auto)

   392 lemma antisym_Le [iff]: "antisym Le"

   393 by (unfold antisym_def Le_def, auto)

   395 lemma trans_Le [iff]: "trans Le"

   396 by (unfold trans_def Le_def, auto)

   398 lemma pfixLe_refl [iff]: "x pfixLe x"

   399 by simp

   401 lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"

   402 by (blast intro: genPrefix_trans)

   404 lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"

   405 by (blast intro: genPrefix_antisym)

   407 lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"

   408 apply (unfold prefix_def Le_def)

   409 apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])

   410 done

   412 lemma refl_Ge [iff]: "refl Ge"

   413 by (unfold refl_on_def Ge_def, auto)

   415 lemma antisym_Ge [iff]: "antisym Ge"

   416 by (unfold antisym_def Ge_def, auto)

   418 lemma trans_Ge [iff]: "trans Ge"

   419 by (unfold trans_def Ge_def, auto)

   421 lemma pfixGe_refl [iff]: "x pfixGe x"

   422 by simp

   424 lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"

   425 by (blast intro: genPrefix_trans)

   427 lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"

   428 by (blast intro: genPrefix_antisym)

   430 lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"

   431 apply (unfold prefix_def Ge_def)

   432 apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])

   433 done

   435 end

author	wenzelm
	Tue, 21 Feb 2012 17:09:17 +0100
changeset 47448	e5438c5797ae
parent 46348	11d9c2768729
child 47782	6d2a2f0e904e
permissions	-rw-r--r--