author | paulson |
Wed, 09 Jul 2003 11:39:34 +0200 | |
changeset 14093 | 24382760fd89 |
parent 14052 | e9c9f69e4f63 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
14052 | 1 |
(* Title: ZF/UNITY/Monotonicity.thy |
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
2 |
ID: $Id \<in> Monotonicity.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $ |
14052 | 3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4 |
Copyright 2002 University of Cambridge |
|
5 |
||
6 |
Monotonicity of an operator (meta-function) with respect to arbitrary set relations. |
|
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 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
11 |
theory Monotonicity = GenPrefix + MultisetSum: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
12 |
|
14052 | 13 |
constdefs |
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
14 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
15 |
mono1 :: "[i, i, i, i, i=>i] => o" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
16 |
"mono1(A, r, B, s, f) == |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
17 |
(\<forall>x \<in> A. \<forall>y \<in> A. <x,y> \<in> r --> <f(x), f(y)> \<in> s) & (\<forall>x \<in> A. f(x) \<in> B)" |
14052 | 18 |
|
19 |
(* monotonicity of a 2-place meta-function f *) |
|
20 |
||
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
21 |
mono2 :: "[i, i, i, i, i, i, [i,i]=>i] => o" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
22 |
"mono2(A, r, B, s, C, t, f) == |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
23 |
(\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B. |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
24 |
<x,y> \<in> r & <u,v> \<in> s --> <f(x,u), f(y,v)> \<in> t) & |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
25 |
(\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)" |
14052 | 26 |
|
27 |
(* Internalized relations on sets and multisets *) |
|
28 |
||
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
29 |
SetLe :: "i =>i" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
30 |
"SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x <= y}" |
14052 | 31 |
|
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
32 |
MultLe :: "[i,i] =>i" |
14052 | 33 |
"MultLe(A, r) == multirel(A, r - id(A)) Un id(Mult(A))" |
34 |
||
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
35 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
36 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
37 |
lemma mono1D: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
38 |
"[| 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
|
39 |
by (unfold mono1_def, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
40 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
41 |
lemma mono2D: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
42 |
"[| mono2(A, r, B, s, C, t, f); |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
43 |
<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
|
44 |
==> <f(x, u), f(y,v)> \<in> t" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
45 |
by (unfold mono2_def, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
46 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
47 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
48 |
(** Monotonicity of take **) |
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 |
lemma take_mono_left_lemma: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
51 |
"[| i le j; xs \<in> list(A); i \<in> nat; j \<in> nat |] |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
52 |
==> <take(i, xs), take(j, xs)> \<in> prefix(A)" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
53 |
apply (case_tac "length (xs) le i") |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
54 |
apply (subgoal_tac "length (xs) le j") |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
55 |
apply (simp) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
56 |
apply (blast intro: le_trans) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
57 |
apply (drule not_lt_imp_le, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
58 |
apply (case_tac "length (xs) le j") |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
59 |
apply (auto simp add: take_prefix) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
60 |
apply (drule not_lt_imp_le, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
61 |
apply (drule_tac m = i in less_imp_succ_add, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
62 |
apply (subgoal_tac "i #+ k le length (xs) ") |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
63 |
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
|
64 |
apply (blast intro: leI) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
65 |
done |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
66 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
67 |
lemma take_mono_left: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
68 |
"[| i le j; xs \<in> list(A); j \<in> nat |] |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
69 |
==> <take(i, xs), take(j, xs)> \<in> prefix(A)" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
70 |
by (blast intro: Nat.le_in_nat take_mono_left_lemma) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
71 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
72 |
lemma take_mono_right: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
73 |
"[| <xs,ys> \<in> prefix(A); i \<in> nat |] |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
74 |
==> <take(i, xs), take(i, ys)> \<in> prefix(A)" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
75 |
by (auto simp add: prefix_iff) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
76 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
77 |
lemma take_mono: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
78 |
"[| i le j; <xs, ys> \<in> prefix(A); j \<in> nat |] |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
79 |
==> <take(i, xs), take(j, ys)> \<in> prefix(A)" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
80 |
apply (rule_tac b = "take (j, xs) " in prefix_trans) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
81 |
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
|
82 |
done |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
83 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
84 |
lemma mono_take [iff]: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
85 |
"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
|
86 |
apply (unfold mono2_def Le_def, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
87 |
apply (blast intro: take_mono) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
88 |
done |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
89 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
90 |
(** Monotonicity of length **) |
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 |
lemmas length_mono = prefix_length_le |
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 |
lemma mono_length [iff]: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
95 |
"mono1(list(A), prefix(A), nat, Le, length)" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
96 |
apply (unfold mono1_def) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
97 |
apply (auto dest: prefix_length_le simp add: Le_def) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
98 |
done |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
99 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
100 |
(** Monotonicity of Un **) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
101 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
102 |
lemma mono_Un [iff]: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
103 |
"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
|
104 |
by (unfold mono2_def SetLe_def, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
105 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
106 |
(* Monotonicity of multiset union *) |
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 |
lemma mono_munion [iff]: |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
109 |
"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
|
110 |
apply (unfold mono2_def MultLe_def) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
111 |
apply (auto simp add: Mult_iff_multiset) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
112 |
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
|
113 |
done |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
114 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
115 |
lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)" |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
116 |
by (unfold mono1_def Le_def, auto) |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
117 |
|
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
118 |
ML{* |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
119 |
val mono1D = thm "mono1D"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
120 |
val mono2D = thm "mono2D"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
121 |
val take_mono_left_lemma = thm "take_mono_left_lemma"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
122 |
val take_mono_left = thm "take_mono_left"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
123 |
val take_mono_right = thm "take_mono_right"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
124 |
val take_mono = thm "take_mono"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
125 |
val mono_take = thm "mono_take"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
126 |
val length_mono = thm "length_mono"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
127 |
val mono_length = thm "mono_length"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
128 |
val mono_Un = thm "mono_Un"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
129 |
val mono_munion = thm "mono_munion"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
130 |
val mono_succ = thm "mono_succ"; |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
131 |
*} |
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14052
diff
changeset
|
132 |
|
14052 | 133 |
end |