--- a/src/ZF/Induct/FoldSet.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/FoldSet.thy Tue Mar 06 16:46:27 2012 +0000
@@ -11,10 +11,10 @@
consts fold_set :: "[i, i, [i,i]=>i, i] => i"
inductive
- domains "fold_set(A, B, f,e)" <= "Fin(A)*B"
+ domains "fold_set(A, B, f,e)" \<subseteq> "Fin(A)*B"
intros
emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)"
- consI: "[| x\<in>A; x \<notin>C; <C,y> : fold_set(A, B,f,e); f(x,y):B |]
+ consI: "[| x\<in>A; x \<notin>C; <C,y> \<in> fold_set(A, B,f,e); f(x,y):B |]
==> <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)"
type_intros Fin.intros
@@ -29,12 +29,12 @@
(** foldSet **)
-inductive_cases empty_fold_setE: "<0, x> : fold_set(A, B, f,e)"
-inductive_cases cons_fold_setE: "<cons(x,C), y> : fold_set(A, B, f,e)"
+inductive_cases empty_fold_setE: "<0, x> \<in> fold_set(A, B, f,e)"
+inductive_cases cons_fold_setE: "<cons(x,C), y> \<in> fold_set(A, B, f,e)"
(* add-hoc lemmas *)
-lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) <-> B = C"
+lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) \<longleftrightarrow> B = C"
by (auto elim: equalityE)
lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |]
@@ -44,13 +44,13 @@
(* fold_set monotonicity *)
lemma fold_set_mono_lemma:
- "<C, x> : fold_set(A, B, f, e)
- ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)"
+ "<C, x> \<in> fold_set(A, B, f, e)
+ ==> \<forall>D. A<=D \<longrightarrow> <C, x> \<in> fold_set(D, B, f, e)"
apply (erule fold_set.induct)
apply (auto intro: fold_set.intros)
done
-lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"
+lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) \<subseteq> fold_set(A, B, f, e)"
apply clarify
apply (frule fold_set.dom_subset [THEN subsetD], clarify)
apply (auto dest: fold_set_mono_lemma)
@@ -64,8 +64,8 @@
(* Proving that fold_set is deterministic *)
lemma Diff1_fold_set:
- "[| <C-{x},y> : fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |]
- ==> <C, f(x, y)> : fold_set(A, B, f, e)"
+ "[| <C-{x},y> \<in> fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |]
+ ==> <C, f(x, y)> \<in> fold_set(A, B, f, e)"
apply (frule fold_set.dom_subset [THEN subsetD])
apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto)
done
@@ -79,7 +79,7 @@
lemma (in fold_typing) Fin_imp_fold_set:
- "C\<in>Fin(A) ==> (EX x. <C, x> : fold_set(A, B, f,e))"
+ "C\<in>Fin(A) ==> (\<exists>x. <C, x> \<in> fold_set(A, B, f,e))"
apply (erule Fin_induct)
apply (auto dest: fold_set.dom_subset [THEN subsetD]
intro: fold_set.intros etype ftype)
@@ -91,9 +91,9 @@
lemma (in fold_typing) fold_set_determ_lemma [rule_format]:
"n\<in>nat
- ==> ALL C. |C|<n -->
- (ALL x. <C, x> : fold_set(A, B, f,e)-->
- (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))"
+ ==> \<forall>C. |C|<n \<longrightarrow>
+ (\<forall>x. <C, x> \<in> fold_set(A, B, f,e)\<longrightarrow>
+ (\<forall>y. <C, y> \<in> fold_set(A, B, f,e) \<longrightarrow> y=x))"
apply (erule nat_induct)
apply (auto simp add: le_iff)
apply (erule fold_set.cases)
@@ -110,7 +110,7 @@
apply (drule cons_lemma2, safe)
apply (frule Diff_sing_imp, assumption+)
txt{** LEVEL 17*}
-apply (subgoal_tac "|Ca| le |Cb|")
+apply (subgoal_tac "|Ca| \<le> |Cb|")
prefer 2
apply (rule succ_le_imp_le)
apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff
@@ -122,7 +122,7 @@
apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD])
apply (subgoal_tac "ya = f(xb,xa) ")
prefer 2 apply (blast del: equalityCE)
-apply (subgoal_tac "<Cb-{x}, xa> : fold_set(A,B,f,e)")
+apply (subgoal_tac "<Cb-{x}, xa> \<in> fold_set(A,B,f,e)")
prefer 2 apply simp
apply (subgoal_tac "yb = f (x, xa) ")
apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all)
@@ -143,7 +143,7 @@
(** The fold function **)
lemma (in fold_typing) fold_equality:
- "<C,y> : fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
+ "<C,y> \<in> fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
apply (unfold fold_def)
apply (frule fold_set.dom_subset [THEN subsetD], clarify)
apply (rule the_equality)
@@ -154,15 +154,15 @@
apply (auto dest: fold_set_lemma intro: ftype etype fcomm)
done
-lemma fold_0 [simp]: "e : B ==> fold[B](f,e,0) = e"
+lemma fold_0 [simp]: "e \<in> B ==> fold[B](f,e,0) = e"
apply (unfold fold_def)
apply (blast elim!: empty_fold_setE intro: fold_set.intros)
done
text{*This result is the right-to-left direction of the subsequent result*}
lemma (in fold_typing) fold_set_imp_cons:
- "[| <C, y> : fold_set(C, B, f, e); C : Fin(A); c : A; c\<notin>C |]
- ==> <cons(c, C), f(c,y)> : fold_set(cons(c, C), B, f, e)"
+ "[| <C, y> \<in> fold_set(C, B, f, e); C \<in> Fin(A); c \<in> A; c\<notin>C |]
+ ==> <cons(c, C), f(c,y)> \<in> fold_set(cons(c, C), B, f, e)"
apply (frule FinD [THEN fold_set_mono, THEN subsetD])
apply assumption
apply (frule fold_set.dom_subset [of A, THEN subsetD])
@@ -170,9 +170,9 @@
done
lemma (in fold_typing) fold_cons_lemma [rule_format]:
-"[| C : Fin(A); c : A; c\<notin>C |]
- ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->
- (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))"
+"[| C \<in> Fin(A); c \<in> A; c\<notin>C |]
+ ==> <cons(c, C), v> \<in> fold_set(cons(c, C), B, f, e) \<longleftrightarrow>
+ (\<exists>y. <C, y> \<in> fold_set(C, B, f, e) & v = f(c, y))"
apply auto
prefer 2 apply (blast intro: fold_set_imp_cons)
apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+)
@@ -220,7 +220,7 @@
lemma (in fold_typing) fold_nest_Un_Int:
"[| C\<in>Fin(A); D\<in>Fin(A) |]
==> fold[B](f, fold[B](f, e, D), C) =
- fold[B](f, fold[B](f, e, (C Int D)), C Un D)"
+ fold[B](f, fold[B](f, e, (C \<inter> D)), C \<union> D)"
apply (erule Fin_induct, auto)
apply (simp add: Un_cons Int_cons_left fold_type fold_commute
fold_typing.fold_cons [of A _ _ f]
@@ -228,8 +228,8 @@
done
lemma (in fold_typing) fold_nest_Un_disjoint:
- "[| C\<in>Fin(A); D\<in>Fin(A); C Int D = 0 |]
- ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)"
+ "[| C\<in>Fin(A); D\<in>Fin(A); C \<inter> D = 0 |]
+ ==> fold[B](f,e,C \<union> D) = fold[B](f, fold[B](f,e,D), C)"
by (simp add: fold_nest_Un_Int)
lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))"
@@ -245,7 +245,7 @@
lemma setsum_cons [simp]:
"Finite(C) ==>
setsum(g, cons(c,C)) =
- (if c : C then setsum(g,C) else g(c) $+ setsum(g,C))"
+ (if c \<in> C then setsum(g,C) else g(c) $+ setsum(g,C))"
apply (auto simp add: setsum_def Finite_cons cons_absorb)
apply (rule_tac A = "cons (c, C)" in fold_typing.fold_cons)
apply (auto intro: fold_typing.intro Finite_cons_lemma)
@@ -260,7 +260,7 @@
(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
lemma setsum_Un_Int:
"[| Finite(C); Finite(D) |]
- ==> setsum(g, C Un D) $+ setsum(g, C Int D)
+ ==> setsum(g, C \<union> D) $+ setsum(g, C \<inter> D)
= setsum(g, C) $+ setsum(g, D)"
apply (erule Finite_induct)
apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un
@@ -274,27 +274,27 @@
done
lemma setsum_Un_disjoint:
- "[| Finite(C); Finite(D); C Int D = 0 |]
- ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)"
+ "[| Finite(C); Finite(D); C \<inter> D = 0 |]
+ ==> setsum(g, C \<union> D) = setsum(g, C) $+ setsum(g,D)"
apply (subst setsum_Un_Int [symmetric])
-apply (subgoal_tac [3] "Finite (C Un D) ")
+apply (subgoal_tac [3] "Finite (C \<union> D) ")
apply (auto intro: Finite_Un)
done
lemma Finite_RepFun [rule_format (no_asm)]:
- "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) --> Finite(RepFun(I, C))"
+ "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow> Finite(RepFun(I, C))"
apply (erule Finite_induct, auto)
done
lemma setsum_UN_disjoint [rule_format (no_asm)]:
"Finite(I)
- ==> (\<forall>i\<in>I. Finite(C(i))) -->
- (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> C(i) Int C(j) = 0) -->
+ ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow>
+ (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> C(i) \<inter> C(j) = 0) \<longrightarrow>
setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)"
apply (erule Finite_induct, auto)
apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i")
prefer 2 apply blast
-apply (subgoal_tac "C (x) Int (\<Union>i\<in>B. C (i)) = 0")
+apply (subgoal_tac "C (x) \<inter> (\<Union>i\<in>B. C (i)) = 0")
prefer 2 apply blast
apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ")
apply (simp (no_asm_simp) add: setsum_Un_disjoint)
@@ -332,21 +332,21 @@
lemma setsum_Un:
"[| Finite(A); Finite(B) |]
- ==> setsum(f, A Un B) =
- setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)"
+ ==> setsum(f, A \<union> B) =
+ setsum(f, A) $+ setsum(f, B) $- setsum(f, A \<inter> B)"
apply (subst setsum_Un_Int [symmetric], auto)
done
lemma setsum_zneg_or_0 [rule_format (no_asm)]:
- "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) --> setsum(g, A) $<= #0"
+ "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) \<longrightarrow> setsum(g, A) $<= #0"
apply (erule Finite_induct)
apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0)
done
lemma setsum_succD_lemma [rule_format]:
"Finite(A)
- ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) --> (\<exists>a\<in>A. #0 $< f(a))"
+ ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) \<longrightarrow> (\<exists>a\<in>A. #0 $< f(a))"
apply (erule Finite_induct)
apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric])
apply (subgoal_tac "setsum (f, B) $<= #0")
@@ -368,7 +368,7 @@
done
lemma g_zpos_imp_setsum_zpos [rule_format]:
- "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) --> #0 $<= setsum(g, A)"
+ "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) \<longrightarrow> #0 $<= setsum(g, A)"
apply (erule Finite_induct)
apply (simp (no_asm))
apply (auto intro: zpos_add_zpos_imp_zpos)
@@ -382,13 +382,13 @@
lemma g_zspos_imp_setsum_zspos [rule_format]:
"Finite(A)
- ==> (\<forall>x\<in>A. #0 $< g(x)) --> A \<noteq> 0 --> (#0 $< setsum(g, A))"
+ ==> (\<forall>x\<in>A. #0 $< g(x)) \<longrightarrow> A \<noteq> 0 \<longrightarrow> (#0 $< setsum(g, A))"
apply (erule Finite_induct)
apply (auto intro: zspos_add_zspos_imp_zspos)
done
lemma setsum_Diff [rule_format]:
- "Finite(A) ==> \<forall>a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})"
+ "Finite(A) ==> \<forall>a. M(a) = #0 \<longrightarrow> setsum(M, A) = setsum(M, A-{a})"
apply (erule Finite_induct)
apply (simp_all add: Diff_cons_eq Finite_Diff)
done