Quellcode-Bibliothek Monotonicity.thy Sprache: Isabelle

(*  Title:      ZF/UNITY/Monotonicity.thy
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    Copyright   2002  University of Cambridge

Monotonicity of an operator (meta-function) with respect to arbitrary
set relations.
*)

section\<open>Monotonicity of an Operator WRT a Relation\<close>

theory Monotonicity imports GenPrefix MultisetSum
begin

definition
  mono1 :: "[i, i, i, i, i\i] \ o" where
  "mono1(A, r, B, s, f) \
    (\<forall>x \<in> A. \<forall>y \<in> A. \<langle>x,y\<rangle> \<in> r \<longrightarrow> <f(x), f(y)> \<in> s) \<and> (\<forall>x \<in> A. f(x) \<in> B)"

  (* monotonicity of a 2-place meta-function f *)

definition
  mono2 :: "[i, i, i, i, i, i, [i,i]\i] \ o" where
  "mono2(A, r, B, s, C, t, f) \
    (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B.
              \<langle>x,y\<rangle> \<in> r \<and> \<langle>u,v\<rangle> \<in> s \<longrightarrow> <f(x,u), f(y,v)> \<in> t) \<and>
    (\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)"

(* Internalized relations on sets and multisets *)

definition
  SetLe :: "i \i" where
  "SetLe(A) \ {\x,y\ \ Pow(A)*Pow(A). x \ y}"

definition
  MultLe :: "[i,i] \i" where
  "MultLe(A, r) \ multirel(A, r - id(A)) \ id(Mult(A))"

lemma mono1D:
  "\mono1(A, r, B, s, f); \x, y\ \ r; x \ A; y \ A\ \ \ s"
by (unfold mono1_def, auto)

lemma mono2D:
     "\mono2(A, r, B, s, C, t, f);
         \<langle>x, y\<rangle> \<in> r; \<langle>u,v\<rangle> \<in> s; x \<in> A; y \<in> A; u \<in> B; v \<in> B\<rbrakk>
      \<Longrightarrow> <f(x, u), f(y,v)> \<in> t"
by (unfold mono2_def, auto)

(** Monotonicity of take **)

lemma take_mono_left_lemma:
     "\i \ j; xs \ list(A); i \ nat; j \ nat\
      \<Longrightarrow> <take(i, xs), take(j, xs)> \<in> prefix(A)"
apply (case_tac "length (xs) \ i")
apply (subgoal_tac "length (xs) \ j")
  apply (simp)
apply (blast intro: le_trans)
apply (drule not_lt_imp_le, auto)
apply (case_tac "length (xs) \ j")
apply (auto simp add: take_prefix)
apply (drule not_lt_imp_le, auto)
apply (drule_tac m = i in less_imp_succ_add, auto)
apply (subgoal_tac "i #+ k \ length (xs) ")
apply (simp add: take_add prefix_iff take_type drop_type)
apply (blast intro: leI)
done

lemma take_mono_left:
     "\i \ j; xs \ list(A); j \ nat\
      \<Longrightarrow> <take(i, xs), take(j, xs)> \<in> prefix(A)"
by (blast intro: le_in_nat take_mono_left_lemma)

lemma take_mono_right:
     "\\xs,ys\ \ prefix(A); i \ nat\
      \<Longrightarrow> <take(i, xs), take(i, ys)> \<in> prefix(A)"
by (auto simp add: prefix_iff)

lemma take_mono:
     "\i \ j; \xs, ys\ \ prefix(A); j \ nat\
      \<Longrightarrow> <take(i, xs), take(j, ys)> \<in> prefix(A)"
apply (rule_tac b = "take (j, xs) " in prefix_trans)
apply (auto dest: prefix_type [THEN subsetD] intro: take_mono_left take_mono_right)
done

lemma mono_take [iff]:
     "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)"
apply (unfold mono2_def Le_def, auto)
apply (blast intro: take_mono)
done

(** Monotonicity of length **)

lemmas length_mono = prefix_length_le

lemma mono_length [iff]:
     "mono1(list(A), prefix(A), nat, Le, length)"
  unfolding mono1_def
apply (auto dest: prefix_length_le simp add: Le_def)
done

(** Monotonicity of \<union> **)

lemma mono_Un [iff]:
     "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), (Un))"
by (unfold mono2_def SetLe_def, auto)

(* Monotonicity of multiset union *)

lemma mono_munion [iff]:
     "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
  unfolding mono2_def MultLe_def
apply (auto simp add: Mult_iff_multiset)
apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
done

lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)"
by (unfold mono1_def Le_def, auto)

end

quality100%

¤ 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.0.11Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.