--- a/src/ZF/UNITY/Monotonicity.thy Tue Mar 06 16:46:27 2012 +0000
+++ b/src/ZF/UNITY/Monotonicity.thy Tue Mar 06 17:01:37 2012 +0000
@@ -14,7 +14,7 @@
definition
mono1 :: "[i, i, i, i, i=>i] => o" where
"mono1(A, r, B, s, f) ==
- (\<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)"
+ (\<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)"
(* monotonicity of a 2-place meta-function f *)
@@ -22,18 +22,18 @@
mono2 :: "[i, i, i, i, i, i, [i,i]=>i] => o" where
"mono2(A, r, B, s, C, t, f) ==
(\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B.
- <x,y> \<in> r & <u,v> \<in> s --> <f(x,u), f(y,v)> \<in> t) &
+ <x,y> \<in> r & <u,v> \<in> s \<longrightarrow> <f(x,u), f(y,v)> \<in> t) &
(\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)"
(* Internalized relations on sets and multisets *)
definition
SetLe :: "i =>i" where
- "SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x <= y}"
+ "SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x \<subseteq> y}"
definition
MultLe :: "[i,i] =>i" where
- "MultLe(A, r) == multirel(A, r - id(A)) Un id(Mult(A))"
+ "MultLe(A, r) == multirel(A, r - id(A)) \<union> id(Mult(A))"
lemma mono1D:
@@ -50,24 +50,24 @@
(** Monotonicity of take **)
lemma take_mono_left_lemma:
- "[| i le j; xs \<in> list(A); i \<in> nat; j \<in> nat |]
+ "[| i \<le> j; xs \<in> list(A); i \<in> nat; j \<in> nat |]
==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
-apply (case_tac "length (xs) le i")
- apply (subgoal_tac "length (xs) le j")
+apply (case_tac "length (xs) \<le> i")
+ apply (subgoal_tac "length (xs) \<le> j")
apply (simp)
apply (blast intro: le_trans)
apply (drule not_lt_imp_le, auto)
-apply (case_tac "length (xs) le j")
+apply (case_tac "length (xs) \<le> 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 le length (xs) ")
+apply (subgoal_tac "i #+ k \<le> length (xs) ")
apply (simp add: take_add prefix_iff take_type drop_type)
apply (blast intro: leI)
done
lemma take_mono_left:
- "[| i le j; xs \<in> list(A); j \<in> nat |]
+ "[| i \<le> j; xs \<in> list(A); j \<in> nat |]
==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
by (blast intro: le_in_nat take_mono_left_lemma)
@@ -77,7 +77,7 @@
by (auto simp add: prefix_iff)
lemma take_mono:
- "[| i le j; <xs, ys> \<in> prefix(A); j \<in> nat |]
+ "[| i \<le> j; <xs, ys> \<in> prefix(A); j \<in> nat |]
==> <take(i, xs), take(j, ys)> \<in> 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)
@@ -99,7 +99,7 @@
apply (auto dest: prefix_length_le simp add: Le_def)
done
-(** Monotonicity of Un **)
+(** Monotonicity of \<union> **)
lemma mono_Un [iff]:
"mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)"