Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: file.vdmpp Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/UNITY/ListOrder.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Lists are partially ordered by Charpentier's Generalized Prefix Relation
   (xs,ys) : genPrefix(r)
     if ys = xs' @ zs where length xs = length xs'
     and corresponding elements of xs, xs' are pairwise related by r

Also overloads <= and < for lists!
*)

section \<open>The Prefix Ordering on Lists\<close>

theory ListOrder
imports Main
begin

inductive_set
  genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
  for r :: "('a * 'a)set"
where
   Nil:     "([],[]) \ genPrefix(r)"

| prepend: "[| (xs,ys) \ genPrefix(r); (x,y) \ r |] ==>
             (x#xs, y#ys) \<in> genPrefix(r)"

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

instantiation list :: (type) ord
begin

definition
  prefix_def:        "xs <= zs \ (xs, zs) \ genPrefix Id"

definition
  strict_prefix_def: "xs < zs \ xs \ zs \ \ zs \ (xs :: 'a list)"

instance ..

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

end

definition Le :: "(nat*nat) set" where
    "Le == {(x,y). x <= y}"

definition  Ge :: "(nat*nat) set" where
    "Ge == {(x,y). y <= x}"

abbreviation
  pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
  "xs pfixLe ys == (xs,ys) \ genPrefix Le"

abbreviation
  pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
  "xs pfixGe ys == (xs,ys) \ genPrefix Ge"

subsection\<open>preliminary lemmas\<close>

lemma Nil_genPrefix [iff]: "([], xs) \ genPrefix r"
by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)

lemma genPrefix_length_le: "(xs,ys) \ genPrefix r \ length xs <= length ys"
by (erule genPrefix.induct, auto)

lemma cdlemma:
     "[| (xs', ys') \ genPrefix r |]
      ==> (\<forall>x xs. xs' = x#xs \<longrightarrow> (\<exists>y ys. ys' = y#ys & (x,y) \<in> r & (xs, ys) \<in> genPrefix r))"
apply (erule genPrefix.induct, blast, blast)
apply (force intro: genPrefix.append)
done

(*As usual converting it to an elimination rule is tiresome*)
lemma cons_genPrefixE [elim!]:
     "[| (x#xs, zs) \ genPrefix r;
         !!y ys. [| zs = y#ys;  (x,y) \<in> r;  (xs, ys) \<in> genPrefix r |] ==> P
      |] ==> P"
by (drule cdlemma, simp, blast)

lemma Cons_genPrefix_Cons [iff]:
     "((x#xs,y#ys) \ genPrefix r) = ((x,y) \ r \ (xs,ys) \ genPrefix r)"
by (blast intro: genPrefix.prepend)

subsection\<open>genPrefix is a partial order\<close>

lemma refl_genPrefix: "refl r ==> refl (genPrefix r)"
apply (unfold refl_on_def, auto)
apply (induct_tac "x")
prefer 2 apply (blast intro: genPrefix.prepend)
apply (blast intro: genPrefix.Nil)
done

lemma genPrefix_refl [simp]: "refl r \ (l,l) \ genPrefix r"
by (erule refl_onD [OF refl_genPrefix UNIV_I])

lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
apply clarify
apply (erule genPrefix.induct)
apply (auto intro: genPrefix.append)
done

(** Transitivity **)

(*A lemma for proving genPrefix_trans_O*)
lemma append_genPrefix:
     "(xs @ ys, zs) \ genPrefix r \ (xs, zs) \ genPrefix r"
  by (induct xs arbitrary: zs) auto

(*Lemma proving transitivity and more*)
lemma genPrefix_trans_O:
  assumes "(x, y) \ genPrefix r"
  shows "\z. (y, z) \ genPrefix s \ (x, z) \ genPrefix (r O s)"
  apply (atomize (full))
  using assms
  apply induct
    apply blast
   apply (blast intro: genPrefix.prepend)
  apply (blast dest: append_genPrefix)
  done

lemma genPrefix_trans:
  "(x, y) \ genPrefix r \ (y, z) \ genPrefix r \ trans r
    \<Longrightarrow> (x, z) \<in> genPrefix r"
  apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
   apply assumption
  apply (blast intro: genPrefix_trans_O)
  done

lemma prefix_genPrefix_trans:
  "[| x<=y; (y,z) \ genPrefix r |] ==> (x, z) \ genPrefix r"
apply (unfold prefix_def)
apply (drule genPrefix_trans_O, assumption)
apply simp
done

lemma genPrefix_prefix_trans:
  "[| (x,y) \ genPrefix r; y<=z |] ==> (x,z) \ genPrefix r"
apply (unfold prefix_def)
apply (drule genPrefix_trans_O, assumption)
apply simp
done

lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
by (blast intro: transI genPrefix_trans)

(** Antisymmetry **)

lemma genPrefix_antisym:
  assumes 1: "(xs, ys) \ genPrefix r"
    and 2: "antisym r"
    and 3: "(ys, xs) \ genPrefix r"
  shows "xs = ys"
  using 1 3
proof induct
  case Nil
  then show ?case by blast
next
  case prepend
  then show ?case using 2 by (simp add: antisym_def)
next
  case (append xs ys zs)
  then show ?case
    apply -
    apply (subgoal_tac "length zs = 0", force)
    apply (drule genPrefix_length_le)+
    apply (simp del: length_0_conv)
    done
qed

lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
  by (blast intro: antisymI genPrefix_antisym)

subsection\<open>recursion equations\<close>

lemma genPrefix_Nil [simp]: "((xs, []) \ genPrefix r) = (xs = [])"
  by (induct xs) auto

lemma same_genPrefix_genPrefix [simp]:
    "refl r \ ((xs@ys, xs@zs) \ genPrefix r) = ((ys,zs) \ genPrefix r)"
  by (induct xs) (simp_all add: refl_on_def)

lemma genPrefix_Cons:
     "((xs, y#ys) \ genPrefix r) =
      (xs=[] | (\<exists>z zs. xs=z#zs & (z,y) \<in> r & (zs,ys) \<in> genPrefix r))"
  by (cases xs) auto

lemma genPrefix_take_append:
     "[| refl r; (xs,ys) \ genPrefix r |]
      ==>  (xs@zs, take (length xs) ys @ zs) \<in> genPrefix r"
apply (erule genPrefix.induct)
apply (frule_tac [3] genPrefix_length_le)
apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
done

lemma genPrefix_append_both:
     "[| refl r; (xs,ys) \ genPrefix r; length xs = length ys |]
      ==>  (xs@zs, ys @ zs) \<in> genPrefix r"
apply (drule genPrefix_take_append, assumption)
apply simp
done

(*NOT suitable for rewriting since [y] has the form y#ys*)
lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
by auto

lemma aolemma:
     "[| (xs,ys) \ genPrefix r; refl r |]
      ==> length xs < length ys \<longrightarrow> (xs @ [ys ! length xs], ys) \<in> genPrefix r"
apply (erule genPrefix.induct)
  apply blast
apply simp
txt\<open>Append case is hardest\<close>
apply simp
apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
apply (erule disjE)
apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
apply (blast intro: genPrefix.append, auto)
apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append)
done

lemma append_one_genPrefix:
     "[| (xs,ys) \ genPrefix r; length xs < length ys; refl r |]
      ==> (xs @ [ys ! length xs], ys) \<in> genPrefix r"
by (blast intro: aolemma [THEN mp])

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

lemma genPrefix_imp_nth:
    "i < length xs \ (xs, ys) \ genPrefix r \ (xs ! i, ys ! i) \ r"
  apply (induct xs arbitrary: i ys)
   apply auto
  apply (case_tac i)
   apply auto
  done

lemma nth_imp_genPrefix:
  "length xs <= length ys \
     (\<forall>i. i < length xs \<longrightarrow> (xs ! i, ys ! i) \<in> r) \<Longrightarrow>
     (xs, ys) \<in> genPrefix r"
  apply (induct xs arbitrary: ys)
   apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib)
  apply (case_tac ys)
   apply (force+)
  done

lemma genPrefix_iff_nth:
     "((xs,ys) \ genPrefix r) =
      (length xs <= length ys & (\<forall>i. i < length xs \<longrightarrow> (xs!i, ys!i) \<in> r))"
apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
done

subsection\<open>The type of lists is partially ordered\<close>

declare refl_Id [iff]
        antisym_Id [iff]
        trans_Id [iff]

lemma prefix_refl [iff]: "xs <= (xs::'a list)"
by (simp add: prefix_def)

lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
apply (unfold prefix_def)
apply (blast intro: genPrefix_trans)
done

lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
apply (unfold prefix_def)
apply (blast intro: genPrefix_antisym)
done

lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \ zs \ xs)"
by (unfold strict_prefix_def, auto)

instance list :: (type) order
  by (intro_classes,
      (assumption | rule prefix_refl prefix_trans prefix_antisym
                     prefix_less_le_not_le)+)

(*Monotonicity of "set" operator WRT prefix*)
lemma set_mono: "xs <= ys ==> set xs <= set ys"
apply (unfold prefix_def)
apply (erule genPrefix.induct, auto)
done

(** recursion equations **)

lemma Nil_prefix [iff]: "[] <= xs"
by (simp add: prefix_def)

lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
by (simp add: prefix_def)

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

lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
by (simp add: prefix_def)

lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
by (insert same_prefix_prefix [of xs ys "[]"], simp)

lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
apply (unfold prefix_def)
apply (erule genPrefix.append)
done

lemma prefix_Cons:
   "(xs <= y#ys) = (xs=[] | (\zs. xs=y#zs \ zs <= ys))"
by (simp add: prefix_def genPrefix_Cons)

lemma append_one_prefix:
  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
apply (unfold prefix_def)
apply (simp add: append_one_genPrefix)
done

lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
apply (unfold prefix_def)
apply (erule genPrefix_length_le)
done

lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
apply (unfold prefix_def)
apply (erule genPrefix.induct, auto)
done

lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
apply (unfold strict_prefix_def)
apply (blast intro: splemma [THEN mp])
done

lemma mono_length: "mono length"
by (blast intro: monoI prefix_length_le)

(*Equivalence to the definition used in Lex/Prefix.thy*)
lemma prefix_iff: "(xs <= zs) = (\ys. zs = xs@ys)"
apply (unfold prefix_def)
apply (auto simp add: genPrefix_iff_nth nth_append)
apply (rule_tac x = "drop (length xs) zs" in exI)
apply (rule nth_equalityI)
apply (simp_all (no_asm_simp) add: nth_append)
done

lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
apply (simp add: prefix_iff)
apply (rule iffI)
apply (erule exE)
apply (rename_tac "zs")
apply (rule_tac xs = zs in rev_exhaust)
  apply simp
apply clarify
apply (simp del: append_assoc add: append_assoc [symmetric], force)
done

lemma prefix_append_iff:
     "(xs <= ys@zs) = (xs <= ys | (\us. xs = ys@us & us <= zs))"
apply (rule_tac xs = zs in rev_induct)
apply force
apply (simp del: append_assoc add: append_assoc [symmetric], force)
done

(*Although the prefix ordering is not linear, the prefixes of a list
  are linearly ordered.*)
lemma common_prefix_linear:
  fixes xs ys zs :: "'a list"
  shows "xs <= zs \ ys <= zs \ xs <= ys | ys <= xs"
  by (induct zs rule: rev_induct) auto

subsection\<open>pfixLe, pfixGe: properties inherited from the translations\<close>

(** pfixLe **)

lemma refl_Le [iff]: "refl Le"
by (unfold refl_on_def Le_def, auto)

lemma antisym_Le [iff]: "antisym Le"
by (unfold antisym_def Le_def, auto)

lemma trans_Le [iff]: "trans Le"
by (unfold trans_def Le_def, auto)

lemma pfixLe_refl [iff]: "x pfixLe x"
by simp

lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
by (blast intro: genPrefix_trans)

lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
by (blast intro: genPrefix_antisym)

lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
apply (unfold prefix_def Le_def)
apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
done

lemma refl_Ge [iff]: "refl Ge"
by (unfold refl_on_def Ge_def, auto)

lemma antisym_Ge [iff]: "antisym Ge"
by (unfold antisym_def Ge_def, auto)

lemma trans_Ge [iff]: "trans Ge"
by (unfold trans_def Ge_def, auto)

lemma pfixGe_refl [iff]: "x pfixGe x"
by simp

lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
by (blast intro: genPrefix_trans)

lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
by (blast intro: genPrefix_antisym)

lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
apply (unfold prefix_def Ge_def)
apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
done

end

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.