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