src/ZF/UNITY/Monotonicity.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/Monotonicity.thy
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     3
    Copyright   2002  University of Cambridge
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26059
diff changeset
     5
Monotonicity of an operator (meta-function) with respect to arbitrary
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26059
diff changeset
     6
set relations.
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     7
*)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     8
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
     9
header{*Monotonicity of an Operator WRT a Relation*}
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    10
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    11
theory Monotonicity imports GenPrefix MultisetSum
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    12
begin
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    13
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
  mono1 :: "[i, i, i, i, i=>i] => o"  where
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    16
  "mono1(A, r, B, s, f) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    17
    (\<forall>x \<in> A. \<forall>y \<in> A. <x,y> \<in> r \<longrightarrow> <f(x), f(y)> \<in> s) & (\<forall>x \<in> A. f(x) \<in> B)"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    18
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    19
  (* monotonicity of a 2-place meta-function f *)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    20
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    21
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    22
  mono2 :: "[i, i, i, i, i, i, [i,i]=>i] => o"  where
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    23
  "mono2(A, r, B, s, C, t, f) == 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    24
    (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B.
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    25
              <x,y> \<in> r & <u,v> \<in> s \<longrightarrow> <f(x,u), f(y,v)> \<in> t) &
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    26
    (\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    27
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    28
 (* Internalized relations on sets and multisets *)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    29
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    30
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    31
  SetLe :: "i =>i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    32
  "SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x \<subseteq> y}"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    33
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    34
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    35
  MultLe :: "[i,i] =>i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    36
  "MultLe(A, r) == multirel(A, r - id(A)) \<union> id(Mult(A))"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    37
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    38
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    39
lemma mono1D: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    40
  "[| mono1(A, r, B, s, f); <x, y> \<in> r; x \<in> A; y \<in> A |] ==> <f(x), f(y)> \<in> s"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    41
by (unfold mono1_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    42
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    43
lemma mono2D: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    44
     "[| mono2(A, r, B, s, C, t, f);  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    45
         <x, y> \<in> r; <u,v> \<in> s; x \<in> A; y \<in> A; u \<in> B; v \<in> B |] 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    46
      ==> <f(x, u), f(y,v)> \<in> t"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    47
by (unfold mono2_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    48
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    49
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    50
(** Monotonicity of take **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    51
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    52
lemma take_mono_left_lemma:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    53
     "[| i \<le> j; xs \<in> list(A); i \<in> nat; j \<in> nat |] 
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    54
      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    55
apply (case_tac "length (xs) \<le> i")
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    56
 apply (subgoal_tac "length (xs) \<le> j")
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    57
  apply (simp)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    58
 apply (blast intro: le_trans)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    59
apply (drule not_lt_imp_le, auto)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    60
apply (case_tac "length (xs) \<le> j")
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    61
 apply (auto simp add: take_prefix)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    62
apply (drule not_lt_imp_le, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    63
apply (drule_tac m = i in less_imp_succ_add, auto)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    64
apply (subgoal_tac "i #+ k \<le> length (xs) ")
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    65
 apply (simp add: take_add prefix_iff take_type drop_type)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    66
apply (blast intro: leI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    67
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    68
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    69
lemma take_mono_left:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    70
     "[| i \<le> j; xs \<in> list(A); j \<in> nat |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    71
      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
26059
b67a225b50fd removed unnecessary theory qualifiers;
wenzelm
parents: 26056
diff changeset
    72
by (blast intro: le_in_nat take_mono_left_lemma) 
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    73
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    74
lemma take_mono_right:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    75
     "[| <xs,ys> \<in> prefix(A); i \<in> nat |] 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    76
      ==> <take(i, xs), take(i, ys)> \<in> prefix(A)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    77
by (auto simp add: prefix_iff)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    78
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    79
lemma take_mono:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    80
     "[| i \<le> j; <xs, ys> \<in> prefix(A); j \<in> nat |]
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    81
      ==> <take(i, xs), take(j, ys)> \<in> prefix(A)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    82
apply (rule_tac b = "take (j, xs) " in prefix_trans)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    83
apply (auto dest: prefix_type [THEN subsetD] intro: take_mono_left take_mono_right)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    84
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    85
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    86
lemma mono_take [iff]:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    87
     "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    88
apply (unfold mono2_def Le_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    89
apply (blast intro: take_mono)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    90
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    91
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    92
(** Monotonicity of length **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    93
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    94
lemmas length_mono = prefix_length_le
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    95
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    96
lemma mono_length [iff]:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    97
     "mono1(list(A), prefix(A), nat, Le, length)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    98
apply (unfold mono1_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
    99
apply (auto dest: prefix_length_le simp add: Le_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   100
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   101
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   102
(** Monotonicity of \<union> **)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   103
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   104
lemma mono_Un [iff]: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   105
     "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   106
by (unfold mono2_def SetLe_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   107
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   108
(* Monotonicity of multiset union *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   109
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   110
lemma mono_munion [iff]: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   111
     "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   112
apply (unfold mono2_def MultLe_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   113
apply (auto simp add: Mult_iff_multiset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   114
apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   115
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   116
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   117
lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   118
by (unfold mono1_def Le_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14052
diff changeset
   119
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
   120
end