author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
14052  1 
(* Title: ZF/UNITY/Monotonicity.thy 
2 
Author: Sidi O Ehmety, Cambridge University Computer Laboratory 

3 
Copyright 2002 University of Cambridge 

4 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26059
diff
changeset

5 
Monotonicity of an operator (metafunction) with respect to arbitrary 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26059
diff
changeset

6 
set relations. 
14052  7 
*) 
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  11 
theory Monotonicity imports GenPrefix MultisetSum 
12 
begin 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset

13 

24893  14 
definition 
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  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  18 

19 
(* monotonicity of a 2place metafunction f *) 

20 

24893  21 
definition 
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  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  27 

28 
(* Internalized relations on sets and multisets *) 

29 

24893  30 
definition 
31 
SetLe :: "i =>i" where 

46823  32 
"SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x \<subseteq> y}" 
14052  33 

24893  34 
definition 
35 
MultLe :: "[i,i] =>i" where 

46823  36 
"MultLe(A, r) == multirel(A, r  id(A)) \<union> id(Mult(A))" 
14052  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  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  55 
apply (case_tac "length (xs) \<le> i") 
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  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  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  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  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  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  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  120 
end 