Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: FoldSet.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      ZF/Induct/FoldSet.thy
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory

A "fold" functional for finite sets.  For n non-negative we have
fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at
least left-commutative.
*)

theory FoldSet imports ZF begin

consts fold_set :: "[i, i, [i,i]=>i, i] => i"

inductive
  domains "fold_set(A, B, f,e)" \<subseteq> "Fin(A)*B"
  intros
    emptyI: "e\B ==> <0, e>\fold_set(A, B, f,e)"
    consI:  "[| x\A; x \C; \ 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

definition
  fold :: "[i, [i,i]=>i, i, i] => i"  (\<open>fold[_]'(_,_,_')\<close>)  where
   "fold[B](f,e, A) == THE x. \fold_set(A, B, f,e)"

definition
   setsum :: "[i=>i, i] => i"  where
   "setsum(g, C) == if Finite(C) then
                     fold[int](%x y. g(x) $+ y, #0, C) else #0"

(** foldSet **)

inductive_cases empty_fold_setE: "<0, x> \ fold_set(A, B, f,e)"
inductive_cases cons_fold_setE: " \ fold_set(A, B, f,e)"

(* add-hoc lemmas *)

lemma cons_lemma1: "[| x\C; x\B |] ==> cons(x,B)=cons(x,C) \ B = C"
by (auto elim: equalityE)

lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\y; x\B; y\C |]
    ==>  B - {y} = C-{x} & x\<in>C & y\<in>B"
apply (auto elim: equalityE)
done

(* fold_set monotonicity *)
lemma fold_set_mono_lemma:
     " \ 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)"
apply clarify
apply (frule fold_set.dom_subset [THEN subsetD], clarify)
apply (auto dest: fold_set_mono_lemma)
done

lemma fold_set_lemma:
     "\fold_set(A, B, f, e) ==> \fold_set(C, B, f, e) & C<=A"
apply (erule fold_set.induct)
apply (auto intro!: fold_set.intros intro: fold_set_mono [THEN subsetD])
done

(* Proving that fold_set is deterministic *)
lemma Diff1_fold_set:
     "[| \ fold_set(A, B, f,e); x\C; x\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

locale fold_typing =
fixes A and B and e and f
assumes ftype [intro,simp]:  "[|x \ A; y \ B|] ==> f(x,y) \ B"
     and etype [intro,simp]:  "e \ B"
     and fcomm:  "[|x \ A; y \ A; z \ B|] ==> f(x, f(y, z))=f(y, f(x, z))"

lemma (in fold_typing) Fin_imp_fold_set:
     "C\Fin(A) ==> (\x. \ 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)
done

lemma Diff_sing_imp:
     "[|C - {b} = D - {a}; a \ b; b \ C|] ==> C = cons(b,D) - {a}"
by (blast elim: equalityE)

lemma (in fold_typing) fold_set_determ_lemma [rule_format]:
"n\nat
==> \<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)
apply (force elim!: empty_fold_setE)
apply (erule fold_set.cases)
apply (force elim!: empty_fold_setE, clarify)
(*force simplification of "|C| < |cons(...)|"*)
apply (frule_tac a = Ca in fold_set.dom_subset [THEN subsetD, THEN SigmaD1])
apply (frule_tac a = Cb in fold_set.dom_subset [THEN subsetD, THEN SigmaD1])
apply (simp add: Fin_into_Finite [THEN Finite_imp_cardinal_cons])
apply (case_tac "x=xb", auto)
apply (simp add: cons_lemma1, blast)
txt\<open>case \<^term>\<open>x\<noteq>xb\<close>\<close>
apply (drule cons_lemma2, safe)
apply (frule Diff_sing_imp, assumption+)
txt\<open>* LEVEL 17\<close>
apply (subgoal_tac "|Ca| \ |Cb|")
prefer 2
apply (rule succ_le_imp_le)
apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff
                  Fin_into_Finite [THEN Finite_imp_cardinal_cons])
apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE])
apply (blast intro: Diff_subset [THEN Fin_subset])
txt\<open>* LEVEL 24 *\<close>
apply (frule Diff1_fold_set, blast, blast)
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 " \ 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)
  apply (blast intro: fcomm dest!: fold_set.dom_subset [THEN subsetD])
apply (blast intro: ftype dest!: fold_set.dom_subset [THEN subsetD], blast)
done

lemma (in fold_typing) fold_set_determ:
     "[| \fold_set(A, B, f, e);
         <C, y>\<in>fold_set(A, B, f, e)|] ==> y=x"
apply (frule fold_set.dom_subset [THEN subsetD], clarify)
apply (drule Fin_into_Finite)
apply (unfold Finite_def, clarify)
apply (rule_tac n = "succ (n)" in fold_set_determ_lemma)
apply (auto intro: eqpoll_imp_lepoll [THEN lepoll_cardinal_le])
done

(** The fold function **)

lemma (in fold_typing) fold_equality:
     " \ 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)
apply (rule_tac [2] A=C in fold_typing.fold_set_determ)
apply (force dest: fold_set_lemma)
apply (auto dest: fold_set_lemma)
apply (simp add: fold_typing_def, auto)
apply (auto dest: fold_set_lemma intro: ftype etype fcomm)
done

lemma fold_0 [simp]: "e \ B ==> fold[B](f,e,0) = e"
apply (unfold fold_def)
apply (blast elim!: empty_fold_setE intro: fold_set.intros)
done

text\<open>This result is the right-to-left direction of the subsequent result\<close>
lemma (in fold_typing) fold_set_imp_cons:
     "[| \ fold_set(C, B, f, e); C \ Fin(A); c \ A; c\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])
apply (blast intro!: fold_set.consI intro: fold_set_mono [THEN subsetD])
done

lemma (in fold_typing) fold_cons_lemma [rule_format]:
"[| C \ Fin(A); c \ A; c\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+)
apply (frule_tac fold_set.dom_subset [of A, THEN subsetD])
apply (drule FinD)
apply (rule_tac A1 = "cons(c,C)" and f1=f and B1=B and C1=C and e1=e in fold_typing.Fin_imp_fold_set [THEN exE])
apply (blast intro: fold_typing.intro ftype etype fcomm)
apply (blast intro: Fin_subset [of _ "cons(c,C)"] Finite_into_Fin
             dest: Fin_into_Finite)
apply (rule_tac x = x in exI)
apply (auto intro: fold_set.intros)
apply (drule_tac fold_set_lemma [of C], blast)
apply (blast intro!: fold_set.consI
             intro: fold_set_determ fold_set_mono [THEN subsetD]
             dest: fold_set.dom_subset [THEN subsetD])
done

lemma (in fold_typing) fold_cons:
     "[| C\Fin(A); c\A; c\C|]
      ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))"
apply (unfold fold_def)
apply (simp add: fold_cons_lemma)
apply (rule the_equality, auto)
apply (subgoal_tac [2] "\C, y\ \ fold_set(A, B, f, e)")
  apply (drule Fin_imp_fold_set)
apply (auto dest: fold_set_lemma  simp add: fold_def [symmetric] fold_equality)
apply (blast intro: fold_set_mono [THEN subsetD] dest!: FinD)
done

lemma (in fold_typing) fold_type [simp,TC]:
     "C\Fin(A) ==> fold[B](f,e,C):B"
apply (erule Fin_induct)
apply (simp_all add: fold_cons ftype etype)
done

lemma (in fold_typing) fold_commute [rule_format]:
     "[| C\Fin(A); c\A |]
      ==> (\<forall>y\<in>B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))"
apply (erule Fin_induct)
apply (simp_all add: fold_typing.fold_cons [of A B _ f]
                     fold_typing.fold_type [of A B _ f]
                     fold_typing_def fcomm)
done

lemma (in fold_typing) fold_nest_Un_Int:
     "[| C\Fin(A); D\Fin(A) |]
      ==> fold[B](f, fold[B](f, e, D), C) =
          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]
                 fold_typing_def fcomm cons_absorb)
done

lemma (in fold_typing) fold_nest_Un_disjoint:
     "[| C\Fin(A); D\Fin(A); C \ 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\Fin(cons(c, C))"
apply (drule Finite_into_Fin)
apply (blast intro: Fin_mono [THEN subsetD])
done

subsection\<open>The Operator \<^term>\<open>setsum\<close>\<close>

lemma setsum_0 [simp]: "setsum(g, 0) = #0"
by (simp add: setsum_def)

lemma setsum_cons [simp]:
     "Finite(C) ==>
      setsum(g, cons(c,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)
done

lemma setsum_K0: "setsum((%i. #0), C) = #0"
apply (case_tac "Finite (C) ")
prefer 2 apply (simp add: setsum_def)
apply (erule Finite_induct, auto)
done

(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
lemma setsum_Un_Int:
     "[| Finite(C); Finite(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
                     Int_lower1 [THEN subset_Finite])
done

lemma setsum_type [simp,TC]: "setsum(g, C):int"
apply (case_tac "Finite (C) ")
prefer 2 apply (simp add: setsum_def)
apply (erule Finite_induct, auto)
done

lemma setsum_Un_disjoint:
     "[| Finite(C); Finite(D); C \ 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 \ D) ")
apply (auto intro: Finite_Un)
done

lemma Finite_RepFun [rule_format (no_asm)]:
     "Finite(I) ==> (\i\I. Finite(C(i))) \ 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))) \<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 "\i\B. x \ i")
prefer 2 apply blast
apply (subgoal_tac "C (x) \ (\i\B. C (i)) = 0")
prefer 2 apply blast
apply (subgoal_tac "Finite (\i\B. C (i)) & Finite (C (x)) & Finite (B) ")
apply (simp (no_asm_simp) add: setsum_Un_disjoint)
apply (auto intro: Finite_Union Finite_RepFun)
done

lemma setsum_addf: "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)"
apply (case_tac "Finite (C) ")
prefer 2 apply (simp add: setsum_def)
apply (erule Finite_induct, auto)
done

lemma fold_set_cong:
     "[| A=A'; B=B'; e=e'; (\x\A'. \y\B'. f(x,y) = f'(x,y)) |]
      ==> fold_set(A,B,f,e) = fold_set(A',B',f',e')"
apply (simp add: fold_set_def)
apply (intro refl iff_refl lfp_cong Collect_cong disj_cong ex_cong, auto)
done

lemma fold_cong:
"[| B=B'; A=A'; e=e';
    !!x y. [|x\<in>A'; y\<in>B'|] ==> f(x,y) = f'(x,y) |] ==>
   fold[B](f,e,A) = fold[B'](f', e', A')"
apply (simp add: fold_def)
apply (subst fold_set_cong)
apply (rule_tac [5] refl, simp_all)
done

lemma setsum_cong:
"[| A=B; !!x. x\B ==> f(x) = g(x) |] ==>
     setsum(f, A) = setsum(g, B)"
by (simp add: setsum_def cong add: fold_cong)

lemma setsum_Un:
     "[| Finite(A); Finite(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) ==> (\x\A. g(x) $\ #0) \ 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) \<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")
apply simp_all
prefer 2 apply (blast intro: setsum_zneg_or_0)
apply (subgoal_tac "$# 1 $\ f (x) $+ setsum (f, B) ")
apply (drule zdiff_zle_iff [THEN iffD2])
apply (subgoal_tac "$# 1 $\ $# 1 $- setsum (f,B) ")
apply (drule_tac x = "$# 1" in zle_trans)
apply (rule_tac [2] j = "#1" in zless_zle_trans, auto)
done

lemma setsum_succD:
     "[| setsum(f, A) = $# succ(n); n\nat |]==> \a\A. #0 $< f(a)"
apply (case_tac "Finite (A) ")
apply (blast intro: setsum_succD_lemma)
apply (unfold setsum_def)
apply (auto simp del: int_of_0 int_of_succ simp add: int_succ_int_1 [symmetric] int_of_0 [symmetric])
done

lemma g_zpos_imp_setsum_zpos [rule_format]:
     "Finite(A) ==> (\x\A. #0 $\ g(x)) \ #0 $\ setsum(g, A)"
apply (erule Finite_induct)
apply (simp (no_asm))
apply (auto intro: zpos_add_zpos_imp_zpos)
done

lemma g_zpos_imp_setsum_zpos2 [rule_format]:
     "[| Finite(A); \x. #0 $\ g(x) |] ==> #0 $\ setsum(g, A)"
apply (erule Finite_induct)
apply (auto intro: zpos_add_zpos_imp_zpos)
done

lemma g_zspos_imp_setsum_zspos [rule_format]:
     "Finite(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) ==> \a. M(a) = #0 \ setsum(M, A) = setsum(M, A-{a})"
apply (erule Finite_induct)
apply (simp_all add: Diff_cons_eq Finite_Diff)
done

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.