wenzelm@32960: (*  Title:      HOL/UNITY/ListOrder.thy
paulson@6708:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6708:     Copyright   1998  University of Cambridge
paulson@6708: 
paulson@13798: Lists are partially ordered by Charpentier's Generalized Prefix Relation
paulson@13798:    (xs,ys) : genPrefix(r)
paulson@13798:      if ys = xs' @ zs where length xs = length xs'
paulson@13798:      and corresponding elements of xs, xs' are pairwise related by r
paulson@13798: 
paulson@13798: Also overloads <= and < for lists!
paulson@6708: *)
paulson@6708: 
paulson@13798: header {*The Prefix Ordering on Lists*}
paulson@13798: 
haftmann@27682: theory ListOrder
haftmann@27682: imports Main
haftmann@27682: begin
paulson@13798: 
berghofe@23767: inductive_set
paulson@13798:   genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
berghofe@23767:   for r :: "('a * 'a)set"
berghofe@23767:  where
paulson@13798:    Nil:     "([],[]) : genPrefix(r)"
paulson@13798: 
berghofe@23767:  | prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
wenzelm@32960:              (x#xs, y#ys) : genPrefix(r)"
paulson@13798: 
berghofe@23767:  | append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
paulson@13798: 
haftmann@27682: instantiation list :: (type) ord 
haftmann@27682: begin
paulson@13798: 
haftmann@27682: definition
haftmann@27682:   prefix_def:        "xs <= zs \<longleftrightarrow>  (xs, zs) : genPrefix Id"
paulson@13798: 
haftmann@27682: definition
haftmann@27682:   strict_prefix_def: "xs < zs  \<longleftrightarrow>  xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)"
haftmann@27682: 
haftmann@27682: instance ..  
paulson@13798: 
paulson@13798: (*Constants for the <= and >= relations, used below in translations*)
haftmann@27682: 
haftmann@27682: end
haftmann@27682: 
haftmann@35416: definition Le :: "(nat*nat) set" where
paulson@13798:     "Le == {(x,y). x <= y}"
paulson@13798: 
haftmann@35416: definition  Ge :: "(nat*nat) set" where
paulson@13798:     "Ge == {(x,y). y <= x}"
paulson@13798: 
berghofe@23767: abbreviation
berghofe@23767:   pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
berghofe@23767:   "xs pfixLe ys == (xs,ys) : genPrefix Le"
paulson@13798: 
berghofe@23767: abbreviation
berghofe@23767:   pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
berghofe@23767:   "xs pfixGe ys == (xs,ys) : genPrefix Ge"
paulson@13798: 
paulson@13798: 
paulson@13798: subsection{*preliminary lemmas*}
paulson@13798: 
paulson@13798: lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
paulson@13798: by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)
paulson@13798: 
paulson@13798: lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys"
paulson@13798: by (erule genPrefix.induct, auto)
paulson@13798: 
paulson@13798: lemma cdlemma:
paulson@13798:      "[| (xs', ys'): genPrefix r |]  
paulson@13798:       ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"
paulson@13798: apply (erule genPrefix.induct, blast, blast)
paulson@13798: apply (force intro: genPrefix.append)
paulson@13798: done
paulson@13798: 
paulson@13798: (*As usual converting it to an elimination rule is tiresome*)
paulson@13798: lemma cons_genPrefixE [elim!]: 
paulson@13798:      "[| (x#xs, zs): genPrefix r;   
paulson@13798:          !!y ys. [| zs = y#ys;  (x,y) : r;  (xs, ys) : genPrefix r |] ==> P  
paulson@13798:       |] ==> P"
paulson@13798: by (drule cdlemma, simp, blast)
paulson@13798: 
paulson@13798: lemma Cons_genPrefix_Cons [iff]:
paulson@13798:      "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"
paulson@13798: by (blast intro: genPrefix.prepend)
paulson@13798: 
paulson@13798: 
paulson@13798: subsection{*genPrefix is a partial order*}
paulson@13798: 
nipkow@30198: lemma refl_genPrefix: "refl r ==> refl (genPrefix r)"
nipkow@30198: apply (unfold refl_on_def, auto)
paulson@13798: apply (induct_tac "x")
paulson@13798: prefer 2 apply (blast intro: genPrefix.prepend)
paulson@13798: apply (blast intro: genPrefix.Nil)
paulson@13798: done
paulson@13798: 
nipkow@30198: lemma genPrefix_refl [simp]: "refl r ==> (l,l) : genPrefix r"
nipkow@30198: by (erule refl_onD [OF refl_genPrefix UNIV_I])
paulson@13798: 
paulson@13798: lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
paulson@13798: apply clarify
paulson@13798: apply (erule genPrefix.induct)
paulson@13798: apply (auto intro: genPrefix.append)
paulson@13798: done
paulson@13798: 
paulson@13798: 
paulson@13798: (** Transitivity **)
paulson@13798: 
paulson@13798: (*A lemma for proving genPrefix_trans_O*)
paulson@13798: lemma append_genPrefix [rule_format]:
paulson@13798:      "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
paulson@13798: by (induct_tac "xs", auto)
paulson@13798: 
paulson@13798: (*Lemma proving transitivity and more*)
paulson@13798: lemma genPrefix_trans_O [rule_format]: 
paulson@13798:      "(x, y) : genPrefix r  
krauss@32235:       ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
paulson@13798: apply (erule genPrefix.induct)
paulson@13798:   prefer 3 apply (blast dest: append_genPrefix)
paulson@13798:  prefer 2 apply (blast intro: genPrefix.prepend, blast)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma genPrefix_trans [rule_format]:
paulson@13798:      "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]  
paulson@13798:       ==> (x,z) : genPrefix r"
paulson@13798: apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
paulson@13798:  apply assumption
paulson@13798: apply (blast intro: genPrefix_trans_O)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma prefix_genPrefix_trans [rule_format]: 
paulson@13798:      "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
paulson@13798: apply (unfold prefix_def)
krauss@32235: apply (drule genPrefix_trans_O, assumption)
krauss@32235: apply simp
paulson@13798: done
paulson@13798: 
paulson@13798: lemma genPrefix_prefix_trans [rule_format]: 
paulson@13798:      "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
paulson@13798: apply (unfold prefix_def)
krauss@32235: apply (drule genPrefix_trans_O, assumption)
krauss@32235: apply simp
paulson@13798: done
paulson@13798: 
paulson@13798: lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
paulson@13798: by (blast intro: transI genPrefix_trans)
paulson@13798: 
paulson@13798: 
paulson@13798: (** Antisymmetry **)
paulson@13798: 
paulson@13798: lemma genPrefix_antisym [rule_format]:
paulson@13798:      "[| (xs,ys) : genPrefix r;  antisym r |]  
paulson@13798:       ==> (ys,xs) : genPrefix r --> xs = ys"
paulson@13798: apply (erule genPrefix.induct)
paulson@13798:   txt{*Base case*}
paulson@13798:   apply blast
paulson@13798:  txt{*prepend case*}
paulson@13798:  apply (simp add: antisym_def)
paulson@13798: txt{*append case is the hardest*}
paulson@13798: apply clarify
paulson@13798: apply (subgoal_tac "length zs = 0", force)
paulson@13798: apply (drule genPrefix_length_le)+
paulson@13798: apply (simp del: length_0_conv)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
paulson@13798: by (blast intro: antisymI genPrefix_antisym)
paulson@13798: 
paulson@13798: 
paulson@13798: subsection{*recursion equations*}
paulson@13798: 
paulson@13798: lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
paulson@13798: apply (induct_tac "xs")
paulson@13798: prefer 2 apply blast
paulson@13798: apply simp
paulson@13798: done
paulson@13798: 
paulson@13798: lemma same_genPrefix_genPrefix [simp]: 
nipkow@30198:     "refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
nipkow@30198: apply (unfold refl_on_def)
paulson@13798: apply (induct_tac "xs")
paulson@13798: apply (simp_all (no_asm_simp))
paulson@13798: done
paulson@13798: 
paulson@13798: lemma genPrefix_Cons:
paulson@13798:      "((xs, y#ys) : genPrefix r) =  
paulson@13798:       (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
paulson@13798: by (case_tac "xs", auto)
paulson@13798: 
paulson@13798: lemma genPrefix_take_append:
nipkow@30198:      "[| refl r;  (xs,ys) : genPrefix r |]  
paulson@13798:       ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
paulson@13798: apply (erule genPrefix.induct)
paulson@13798: apply (frule_tac [3] genPrefix_length_le)
paulson@13798: apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
paulson@13798: done
paulson@13798: 
paulson@13798: lemma genPrefix_append_both:
nipkow@30198:      "[| refl r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
paulson@13798:       ==>  (xs@zs, ys @ zs) : genPrefix r"
paulson@13798: apply (drule genPrefix_take_append, assumption)
paulson@13798: apply (simp add: take_all)
paulson@13798: done
paulson@13798: 
paulson@13798: 
paulson@13798: (*NOT suitable for rewriting since [y] has the form y#ys*)
paulson@13798: lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
paulson@13798: by auto
paulson@13798: 
paulson@13798: lemma aolemma:
nipkow@30198:      "[| (xs,ys) : genPrefix r;  refl r |]  
paulson@13798:       ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
paulson@13798: apply (erule genPrefix.induct)
paulson@13798:   apply blast
paulson@13798:  apply simp
paulson@13798: txt{*Append case is hardest*}
paulson@13798: apply simp
paulson@13798: apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
paulson@13798: apply (erule disjE)
paulson@13798: apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
paulson@13798: apply (blast intro: genPrefix.append, auto)
paulson@15481: apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma append_one_genPrefix:
nipkow@30198:      "[| (xs,ys) : genPrefix r;  length xs < length ys;  refl r |]  
paulson@13798:       ==> (xs @ [ys ! length xs], ys) : genPrefix r"
paulson@13798: by (blast intro: aolemma [THEN mp])
paulson@13798: 
paulson@13798: 
paulson@13798: (** Proving the equivalence with Charpentier's definition **)
paulson@13798: 
paulson@13798: lemma genPrefix_imp_nth [rule_format]:
paulson@13798:      "ALL i ys. i < length xs  
paulson@13798:                 --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
paulson@13798: apply (induct_tac "xs", auto)
paulson@13798: apply (case_tac "i", auto)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma nth_imp_genPrefix [rule_format]:
paulson@13798:      "ALL ys. length xs <= length ys   
paulson@13798:       --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)   
paulson@13798:       --> (xs, ys) : genPrefix r"
paulson@13798: apply (induct_tac "xs")
paulson@13798: apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
paulson@13798: apply clarify
paulson@13798: apply (case_tac "ys")
paulson@13798: apply (force+)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma genPrefix_iff_nth:
paulson@13798:      "((xs,ys) : genPrefix r) =  
paulson@13798:       (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"
paulson@13798: apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
paulson@13798: done
paulson@13798: 
paulson@13798: 
paulson@13798: subsection{*The type of lists is partially ordered*}
paulson@13798: 
nipkow@30198: declare refl_Id [iff] 
paulson@13798:         antisym_Id [iff] 
paulson@13798:         trans_Id [iff]
paulson@13798: 
paulson@13798: lemma prefix_refl [iff]: "xs <= (xs::'a list)"
paulson@13798: by (simp add: prefix_def)
paulson@13798: 
paulson@13798: lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (blast intro: genPrefix_trans)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (blast intro: genPrefix_antisym)
paulson@13798: done
paulson@13798: 
haftmann@27682: lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)"
paulson@13798: by (unfold strict_prefix_def, auto)
paulson@6708: 
wenzelm@12338: instance list :: (type) order
paulson@13798:   by (intro_classes,
paulson@13798:       (assumption | rule prefix_refl prefix_trans prefix_antisym
haftmann@27682:                      prefix_less_le_not_le)+)
paulson@13798: 
paulson@13798: (*Monotonicity of "set" operator WRT prefix*)
paulson@13798: lemma set_mono: "xs <= ys ==> set xs <= set ys"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (erule genPrefix.induct, auto)
paulson@13798: done
paulson@13798: 
paulson@13798: 
paulson@13798: (** recursion equations **)
paulson@13798: 
paulson@13798: lemma Nil_prefix [iff]: "[] <= xs"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (simp add: Nil_genPrefix)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (simp add: genPrefix_Nil)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
paulson@13798: by (simp add: prefix_def)
paulson@13798: 
paulson@13798: lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
paulson@13798: by (simp add: prefix_def)
paulson@13798: 
paulson@13798: lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
paulson@13798: by (insert same_prefix_prefix [of xs ys "[]"], simp)
paulson@13798: 
paulson@13798: lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (erule genPrefix.append)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma prefix_Cons: 
paulson@13798:    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"
paulson@13798: by (simp add: prefix_def genPrefix_Cons)
paulson@13798: 
paulson@13798: lemma append_one_prefix: 
paulson@13798:   "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (simp add: append_one_genPrefix)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (erule genPrefix_length_le)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (erule genPrefix.induct, auto)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
paulson@13798: apply (unfold strict_prefix_def)
paulson@13798: apply (blast intro: splemma [THEN mp])
paulson@13798: done
paulson@13798: 
paulson@13798: lemma mono_length: "mono length"
paulson@13798: by (blast intro: monoI prefix_length_le)
paulson@13798: 
paulson@13798: (*Equivalence to the definition used in Lex/Prefix.thy*)
paulson@13798: lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"
paulson@13798: apply (unfold prefix_def)
paulson@13798: apply (auto simp add: genPrefix_iff_nth nth_append)
paulson@13798: apply (rule_tac x = "drop (length xs) zs" in exI)
paulson@13798: apply (rule nth_equalityI)
paulson@13798: apply (simp_all (no_asm_simp) add: nth_append)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
paulson@13798: apply (simp add: prefix_iff)
paulson@13798: apply (rule iffI)
paulson@13798:  apply (erule exE)
paulson@13798:  apply (rename_tac "zs")
paulson@13798:  apply (rule_tac xs = zs in rev_exhaust)
paulson@13798:   apply simp
paulson@13798:  apply clarify
paulson@13798:  apply (simp del: append_assoc add: append_assoc [symmetric], force)
paulson@13798: done
paulson@13798: 
paulson@13798: lemma prefix_append_iff:
paulson@13798:      "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"
paulson@13798: apply (rule_tac xs = zs in rev_induct)
paulson@13798:  apply force
paulson@13798: apply (simp del: append_assoc add: append_assoc [symmetric], force)
paulson@13798: done
paulson@13798: 
paulson@13798: (*Although the prefix ordering is not linear, the prefixes of a list
paulson@13798:   are linearly ordered.*)
paulson@13798: lemma common_prefix_linear [rule_format]:
paulson@13798:      "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
paulson@13798: by (rule_tac xs = zs in rev_induct, auto)
paulson@13798: 
paulson@13798: 
paulson@13798: subsection{*pfixLe, pfixGe: properties inherited from the translations*}
paulson@13798: 
paulson@13798: (** pfixLe **)
paulson@13798: 
nipkow@30198: lemma refl_Le [iff]: "refl Le"
nipkow@30198: by (unfold refl_on_def Le_def, auto)
paulson@13798: 
paulson@13798: lemma antisym_Le [iff]: "antisym Le"
paulson@13798: by (unfold antisym_def Le_def, auto)
paulson@13798: 
paulson@13798: lemma trans_Le [iff]: "trans Le"
paulson@13798: by (unfold trans_def Le_def, auto)
paulson@13798: 
paulson@13798: lemma pfixLe_refl [iff]: "x pfixLe x"
paulson@13798: by simp
paulson@13798: 
paulson@13798: lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
paulson@13798: by (blast intro: genPrefix_trans)
paulson@13798: 
paulson@13798: lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
paulson@13798: by (blast intro: genPrefix_antisym)
paulson@13798: 
paulson@13798: lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
paulson@13798: apply (unfold prefix_def Le_def)
paulson@13798: apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
paulson@13798: done
paulson@13798: 
nipkow@30198: lemma refl_Ge [iff]: "refl Ge"
nipkow@30198: by (unfold refl_on_def Ge_def, auto)
paulson@13798: 
paulson@13798: lemma antisym_Ge [iff]: "antisym Ge"
paulson@13798: by (unfold antisym_def Ge_def, auto)
paulson@13798: 
paulson@13798: lemma trans_Ge [iff]: "trans Ge"
paulson@13798: by (unfold trans_def Ge_def, auto)
paulson@13798: 
paulson@13798: lemma pfixGe_refl [iff]: "x pfixGe x"
paulson@13798: by simp
paulson@13798: 
paulson@13798: lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
paulson@13798: by (blast intro: genPrefix_trans)
paulson@13798: 
paulson@13798: lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
paulson@13798: by (blast intro: genPrefix_antisym)
paulson@13798: 
paulson@13798: lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
paulson@13798: apply (unfold prefix_def Ge_def)
paulson@13798: apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
paulson@13798: done
paulson@6708: 
paulson@6708: end