1(*  Title:      ZF/UNITY/Monotonicity.thy
2    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
3    Copyright   2002  University of Cambridge
4
5Monotonicity of an operator (meta-function) with respect to arbitrary
6set relations.
7*)
8
9section\<open>Monotonicity of an Operator WRT a Relation\<close>
10
11theory Monotonicity imports GenPrefix MultisetSum
12begin
13
14definition
15  mono1 :: "[i, i, i, i, i=>i] => o"  where
16  "mono1(A, r, B, s, f) ==
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)"
18
19  (* monotonicity of a 2-place meta-function f *)
20
21definition
22  mono2 :: "[i, i, i, i, i, i, [i,i]=>i] => o"  where
23  "mono2(A, r, B, s, C, t, f) == 
24    (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B.
25              <x,y> \<in> r & <u,v> \<in> s \<longrightarrow> <f(x,u), f(y,v)> \<in> t) &
26    (\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)"
27
28 (* Internalized relations on sets and multisets *)
29
30definition
31  SetLe :: "i =>i"  where
32  "SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x \<subseteq> y}"
33
34definition
35  MultLe :: "[i,i] =>i"  where
36  "MultLe(A, r) == multirel(A, r - id(A)) \<union> id(Mult(A))"
37
38
39lemma mono1D: 
40  "[| mono1(A, r, B, s, f); <x, y> \<in> r; x \<in> A; y \<in> A |] ==> <f(x), f(y)> \<in> s"
41by (unfold mono1_def, auto)
42
43lemma mono2D: 
44     "[| mono2(A, r, B, s, C, t, f);  
45         <x, y> \<in> r; <u,v> \<in> s; x \<in> A; y \<in> A; u \<in> B; v \<in> B |] 
46      ==> <f(x, u), f(y,v)> \<in> t"
47by (unfold mono2_def, auto)
48
49
50(** Monotonicity of take **)
51
52lemma take_mono_left_lemma:
53     "[| i \<le> j; xs \<in> list(A); i \<in> nat; j \<in> nat |] 
54      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
55apply (case_tac "length (xs) \<le> i")
56 apply (subgoal_tac "length (xs) \<le> j")
57  apply (simp)
58 apply (blast intro: le_trans)
59apply (drule not_lt_imp_le, auto)
60apply (case_tac "length (xs) \<le> j")
61 apply (auto simp add: take_prefix)
62apply (drule not_lt_imp_le, auto)
63apply (drule_tac m = i in less_imp_succ_add, auto)
64apply (subgoal_tac "i #+ k \<le> length (xs) ")
65 apply (simp add: take_add prefix_iff take_type drop_type)
66apply (blast intro: leI)
67done
68
69lemma take_mono_left:
70     "[| i \<le> j; xs \<in> list(A); j \<in> nat |]
71      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
72by (blast intro: le_in_nat take_mono_left_lemma) 
73
74lemma take_mono_right:
75     "[| <xs,ys> \<in> prefix(A); i \<in> nat |] 
76      ==> <take(i, xs), take(i, ys)> \<in> prefix(A)"
77by (auto simp add: prefix_iff)
78
79lemma take_mono:
80     "[| i \<le> j; <xs, ys> \<in> prefix(A); j \<in> nat |]
81      ==> <take(i, xs), take(j, ys)> \<in> prefix(A)"
82apply (rule_tac b = "take (j, xs) " in prefix_trans)
83apply (auto dest: prefix_type [THEN subsetD] intro: take_mono_left take_mono_right)
84done
85
86lemma mono_take [iff]:
87     "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)"
88apply (unfold mono2_def Le_def, auto)
89apply (blast intro: take_mono)
90done
91
92(** Monotonicity of length **)
93
94lemmas length_mono = prefix_length_le
95
96lemma mono_length [iff]:
97     "mono1(list(A), prefix(A), nat, Le, length)"
98apply (unfold mono1_def)
99apply (auto dest: prefix_length_le simp add: Le_def)
100done
101
102(** Monotonicity of \<union> **)
103
104lemma mono_Un [iff]: 
105     "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), (Un))"
106by (unfold mono2_def SetLe_def, auto)
107
108(* Monotonicity of multiset union *)
109
110lemma mono_munion [iff]: 
111     "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
112apply (unfold mono2_def MultLe_def)
113apply (auto simp add: Mult_iff_multiset)
114apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
115done
116
117lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)"
118by (unfold mono1_def Le_def, auto)
119
120end
121