Theory Monotonicity

(*  Title:      ZF/UNITY/Monotonicity.thy
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    Copyright   2002  University of Cambridge

Monotonicity of an operator (meta-function) with respect to arbitrary
set relations.
*)

section‹Monotonicity of an Operator WRT a Relation›

theory Monotonicity imports GenPrefix MultisetSum
begin

definition
  mono1 :: "[i, i, i, i, i⇒i] ⇒ o"  where
  "mono1(A, r, B, s, f) ≡
    (∀x ∈ A. ∀y ∈ A. ⟨x,y⟩ ∈ r ⟶ <f(x), f(y)> ∈ s) ∧ (∀x ∈ A. f(x) ∈ B)"

  (* monotonicity of a 2-place meta-function f *)

definition
  mono2 :: "[i, i, i, i, i, i, [i,i]⇒i] ⇒ o"  where
  "mono2(A, r, B, s, C, t, f) ≡ 
    (∀x ∈ A. ∀y ∈ A. ∀u ∈ B. ∀v ∈ B.
              ⟨x,y⟩ ∈ r ∧ ⟨u,v⟩ ∈ s ⟶ <f(x,u), f(y,v)> ∈ t) ∧
    (∀x ∈ A. ∀y ∈ B. f(x,y) ∈ C)"

 (* Internalized relations on sets and multisets *)

definition
  SetLe :: "i ⇒i"  where
  "SetLe(A) ≡ {⟨x,y⟩ ∈ Pow(A)*Pow(A). x ⊆ y}"

definition
  MultLe :: "[i,i] ⇒i"  where
  "MultLe(A, r) ≡ multirel(A, r - id(A)) ∪ id(Mult(A))"


lemma mono1D: 
  "⟦mono1(A, r, B, s, f); ⟨x, y⟩ ∈ r; x ∈ A; y ∈ A⟧ ⟹ <f(x), f(y)> ∈ s"
by (unfold mono1_def, auto)

lemma mono2D: 
     "⟦mono2(A, r, B, s, C, t, f);  
         ⟨x, y⟩ ∈ r; ⟨u,v⟩ ∈ s; x ∈ A; y ∈ A; u ∈ B; v ∈ B⟧ 
      ⟹ <f(x, u), f(y,v)> ∈ t"
by (unfold mono2_def, auto)


(** Monotonicity of take **)

lemma take_mono_left_lemma:
     "⟦i ≤ j; xs ∈ list(A); i ∈ nat; j ∈ nat⟧ 
      ⟹ <take(i, xs), take(j, xs)> ∈ prefix(A)"
apply (case_tac "length (xs) ≤ i")
 apply (subgoal_tac "length (xs) ≤ j")
  apply (simp)
 apply (blast intro: le_trans)
apply (drule not_lt_imp_le, auto)
apply (case_tac "length (xs) ≤ j")
 apply (auto simp add: take_prefix)
apply (drule not_lt_imp_le, auto)
apply (drule_tac m = i in less_imp_succ_add, auto)
apply (subgoal_tac "i #+ k ≤ length (xs) ")
 apply (simp add: take_add prefix_iff take_type drop_type)
apply (blast intro: leI)
done

lemma take_mono_left:
     "⟦i ≤ j; xs ∈ list(A); j ∈ nat⟧
      ⟹ <take(i, xs), take(j, xs)> ∈ prefix(A)"
by (blast intro: le_in_nat take_mono_left_lemma) 

lemma take_mono_right:
     "⟦⟨xs,ys⟩ ∈ prefix(A); i ∈ nat⟧ 
      ⟹ <take(i, xs), take(i, ys)> ∈ prefix(A)"
by (auto simp add: prefix_iff)

lemma take_mono:
     "⟦i ≤ j; ⟨xs, ys⟩ ∈ prefix(A); j ∈ nat⟧
      ⟹ <take(i, xs), take(j, ys)> ∈ prefix(A)"
apply (rule_tac b = "take (j, xs) " in prefix_trans)
apply (auto dest: prefix_type [THEN subsetD] intro: take_mono_left take_mono_right)
done

lemma mono_take [iff]:
     "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)"
apply (unfold mono2_def Le_def, auto)
apply (blast intro: take_mono)
done

(** Monotonicity of length **)

lemmas length_mono = prefix_length_le

lemma mono_length [iff]:
     "mono1(list(A), prefix(A), nat, Le, length)"
  unfolding mono1_def
apply (auto dest: prefix_length_le simp add: Le_def)
done

(** Monotonicity of ∪ **)

lemma mono_Un [iff]: 
     "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), (Un))"
by (unfold mono2_def SetLe_def, auto)

(* Monotonicity of multiset union *)

lemma mono_munion [iff]: 
     "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
  unfolding mono2_def MultLe_def
apply (auto simp add: Mult_iff_multiset)
apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
done

lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)"
by (unfold mono1_def Le_def, auto)

end