# Theory AllocBase

Up to index of Isabelle/ZF/UNITY

theory AllocBase
imports Follows MultisetSum Guar
begin

    (*  Title:      ZF/UNITY/AllocBase.thy
        ID:         $Id: AllocBase.thy,v 1.6 2005/06/17 14:15:11 haftmann Exp $
        Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
        Copyright   2001  University of Cambridge

    *)

    header{*Common declarations for Chandy and Charpentier's Allocator*}

    theory AllocBase imports Follows MultisetSum Guar begin

    consts
      tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
      NbT      :: i  (* Number of tokens in system *)
      Nclients :: i  (* Number of clients *)

    translations "tokbag" => "nat"

    axioms
      NbT_pos:      "NbT ∈ nat-{0}"
      Nclients_pos: "Nclients ∈ nat-{0}"

    text{*This function merely sums the elements of a list*}
    consts tokens :: "i =>i"
           item :: i (* Items to be merged/distributed *)
    primrec
      "tokens(Nil) = 0"
      "tokens (Cons(x,xs)) = x #+ tokens(xs)"

    consts
      bag_of :: "i => i"

    primrec
      "bag_of(Nil)    = 0"
      "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"

    text{*Definitions needed in Client.thy.  We define a recursive predicate
    using 0 and 1 to code the truth values.*}
    consts all_distinct0 :: "i=>i"
     primrec
      "all_distinct0(Nil) = 1"
      "all_distinct0(Cons(a, l)) =
         (if a ∈ set_of_list(l) then 0 else all_distinct0(l))"

    constdefs
      all_distinct  :: "i=>o"
       "all_distinct(l) == all_distinct0(l)=1"

    constdefs
      state_of :: "i =>i" --{* coersion from anyting to state *}
       "state_of(s) == if s ∈ state then s else st0"

      lift :: "i =>(i=>i)" --{* simplifies the expression of programs*}
       "lift(x) == %s. s`x"

    text{* function to show that the set of variables is infinite *}
    consts
      nat_list_inj :: "i=>i"
      nat_var_inj  :: "i=>i"
      var_inj      :: "i=>i"

    defs
      nat_var_inj_def: "nat_var_inj(n) == Var(nat_list_inj(n))"
    primrec
      "nat_list_inj(0) = Nil"
      "nat_list_inj(succ(n)) = Cons(n, nat_list_inj(n))"

    primrec
      "var_inj(Var(l)) = length(l)"

    subsection{*Various simple lemmas*}

    lemma Nclients_NbT_gt_0 [simp]: "0 < Nclients & 0 < NbT"
    apply (cut_tac Nclients_pos NbT_pos)
    apply (auto intro: Ord_0_lt)
    done

    lemma Nclients_NbT_not_0 [simp]: "Nclients ≠ 0 & NbT ≠ 0"
    by (cut_tac Nclients_pos NbT_pos, auto)

    lemma Nclients_type [simp,TC]: "Nclients∈nat"
    by (cut_tac Nclients_pos NbT_pos, auto)

    lemma NbT_type [simp,TC]: "NbT∈nat"
    by (cut_tac Nclients_pos NbT_pos, auto)

    lemma INT_Nclient_iff [iff]:
         "b∈Inter(RepFun(Nclients, B)) <-> (∀x∈Nclients. b∈B(x))"
    by (force simp add: INT_iff)

    lemma setsum_fun_mono [rule_format]:
         "n∈nat ==>
          (∀i∈nat. i<n --> f(i) $<= g(i)) -->
          setsum(f, n) $<= setsum(g,n)"
    apply (induct_tac "n", simp_all)
    apply (subgoal_tac "Finite(x) & x∉x")
     prefer 2 apply (simp add: nat_into_Finite mem_not_refl, clarify)
    apply (simp (no_asm_simp) add: succ_def)
    apply (subgoal_tac "∀i∈nat. i<x--> f(i) $<= g(i) ")
     prefer 2 apply (force dest: leI)
    apply (rule zadd_zle_mono, simp_all)
    done

    lemma tokens_type [simp,TC]: "l∈list(A) ==> tokens(l)∈nat"
    by (erule list.induct, auto)

    lemma tokens_mono_aux [rule_format]:
         "xs∈list(A) ==> ∀ys∈list(A). <xs, ys>∈prefix(A)
       --> tokens(xs) ≤ tokens(ys)"
    apply (induct_tac "xs")
    apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: prefix_def)
    done

    lemma tokens_mono: "<xs, ys>∈prefix(A) ==> tokens(xs) ≤ tokens(ys)"
    apply (cut_tac prefix_type)
    apply (blast intro: tokens_mono_aux)
    done

    lemma mono_tokens [iff]: "mono1(list(A), prefix(A), nat, Le,tokens)"
    apply (unfold mono1_def)
    apply (auto intro: tokens_mono simp add: Le_def)
    done

    lemma tokens_append [simp]:
    "[| xs∈list(A); ys∈list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)"
    apply (induct_tac "xs", auto)
    done

    subsection{*The function @{term bag_of}*}

    lemma bag_of_type [simp,TC]: "l∈list(A) ==>bag_of(l)∈Mult(A)"
    apply (induct_tac "l")
    apply (auto simp add: Mult_iff_multiset)
    done

    lemma bag_of_multiset:
         "l∈list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A"
    apply (drule bag_of_type)
    apply (auto simp add: Mult_iff_multiset)
    done

    lemma bag_of_append [simp]:
        "[| xs∈list(A); ys∈list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)"
    apply (induct_tac "xs")
    apply (auto simp add: bag_of_multiset munion_assoc)
    done

    lemma bag_of_mono_aux [rule_format]:
         "xs∈list(A) ==> ∀ys∈list(A). <xs, ys>∈prefix(A)
          --> <bag_of(xs), bag_of(ys)>∈MultLe(A, r)"
    apply (induct_tac "xs", simp_all, clarify)
    apply (frule_tac l = ys in bag_of_multiset)
    apply (auto intro: empty_le_MultLe simp add: prefix_def)
    apply (rule munion_mono)
    apply (force simp add: MultLe_def Mult_iff_multiset)
    apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
    done

    lemma bag_of_mono [intro]:
         "[|  <xs, ys>∈prefix(A); xs∈list(A); ys∈list(A) |]
          ==> <bag_of(xs), bag_of(ys)>∈MultLe(A, r)"
    apply (blast intro: bag_of_mono_aux)
    done

    lemma mono_bag_of [simp]:
         "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)"
    by (auto simp add:  mono1_def bag_of_type)

    subsection{*The function @{term msetsum}*}

    lemmas nat_into_Fin = eqpoll_refl [THEN [2] Fin_lemma]

    lemma list_Int_length_Fin: "l ∈ list(A) ==> C Int length(l) ∈ Fin(length(l))"
    apply (drule length_type)
    apply (rule Fin_subset)
    apply (rule Int_lower2)
    apply (erule nat_into_Fin)
    done

    lemma mem_Int_imp_lt_length:
         "[|xs ∈ list(A); k ∈ C ∩ length(xs)|] ==> k < length(xs)"
    by (simp add: ltI)

    lemma Int_succ_right:
         "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)"
    by auto

    lemma bag_of_sublist_lemma:
         "[|C ⊆ nat; x ∈ A; xs ∈ list(A)|]
      ==>  msetsum(λi. {#nth(i, xs @ [x])#}, C ∩ succ(length(xs)), A) =
           (if length(xs) ∈ C then
              {#x#} +# msetsum(λx. {#nth(x, xs)#}, C ∩ length(xs), A)
            else msetsum(λx. {#nth(x, xs)#}, C ∩ length(xs), A))"
    apply (simp add: subsetD nth_append lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
    apply (simp add: Int_succ_right)
    apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong, clarify)
    apply (subst msetsum_cons)
    apply (rule_tac [3] succI1)
    apply (blast intro: list_Int_length_Fin subset_succI [THEN Fin_mono, THEN subsetD])
    apply (simp add: mem_not_refl)
    apply (simp add: nth_type lt_not_refl)
    apply (blast intro: nat_into_Ord ltI length_type)
    apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
    done

    lemma bag_of_sublist_lemma2:
         "l∈list(A) ==>
      C <= nat ==>
      bag_of(sublist(l, C)) =
          msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
    apply (erule list_append_induct)
    apply (simp (no_asm))
    apply (simp (no_asm_simp) add: sublist_append nth_append bag_of_sublist_lemma munion_commute bag_of_sublist_lemma msetsum_multiset munion_0)
    done

    lemma nat_Int_length_eq: "l ∈ list(A) ==> nat ∩ length(l) = length(l)"
    apply (rule Int_absorb1)
    apply (rule OrdmemD, auto)
    done

    (*eliminating the assumption C<=nat*)
    lemma bag_of_sublist:
         "l∈list(A) ==>
      bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
    apply (subgoal_tac " bag_of (sublist (l, C Int nat)) = msetsum (%i. {#nth (i, l) #}, C Int length (l), A) ")
    apply (simp add: sublist_Int_eq)
    apply (simp add: bag_of_sublist_lemma2 Int_lower2 Int_assoc nat_Int_length_eq)
    done

    lemma bag_of_sublist_Un_Int:
    "l∈list(A) ==>
      bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) =
          bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
    apply (subgoal_tac "B Int C Int length (l) = (B Int length (l)) Int (C Int length (l))")
    prefer 2 apply blast
    apply (simp (no_asm_simp) add: bag_of_sublist Int_Un_distrib2 msetsum_Un_Int)
    apply (rule msetsum_Un_Int)
    apply (erule list_Int_length_Fin)+
     apply (simp add: ltI nth_type)
    done

    lemma bag_of_sublist_Un_disjoint:
         "[| l∈list(A); B Int C = 0  |]
          ==> bag_of(sublist(l, B Un C)) =
              bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
    by (simp add: bag_of_sublist_Un_Int [symmetric] bag_of_multiset)

    lemma bag_of_sublist_UN_disjoint [rule_format]:
         "[|Finite(I); ∀i∈I. ∀j∈I. i≠j --> A(i) ∩ A(j) = 0;
            l∈list(B) |]
          ==> bag_of(sublist(l, \<Union>i∈I. A(i))) =
              (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) "
    apply (simp (no_asm_simp) del: UN_simps
               add: UN_simps [symmetric] bag_of_sublist)
    apply (subst  msetsum_UN_disjoint [of _ _ _ "length (l)"])
    apply (drule Finite_into_Fin, assumption)
    prefer 3 apply force
    apply (auto intro!: Fin_IntI2 Finite_into_Fin simp add: ltI nth_type length_type nat_into_Finite)
    done

    lemma part_ord_Lt [simp]: "part_ord(nat, Lt)"
    apply (unfold part_ord_def Lt_def irrefl_def trans_on_def)
    apply (auto intro: lt_trans)
    done

    subsubsection{*The function @{term all_distinct}*}

    lemma all_distinct_Nil [simp]: "all_distinct(Nil)"
    by (unfold all_distinct_def, auto)

    lemma all_distinct_Cons [simp]:
        "all_distinct(Cons(a,l)) <->
          (a∈set_of_list(l) --> False) & (a ∉ set_of_list(l) --> all_distinct(l))"
    apply (unfold all_distinct_def)
    apply (auto elim: list.cases)
    done

    subsubsection{*The function @{term state_of}*}

    lemma state_of_state: "s∈state ==> state_of(s)=s"
    by (unfold state_of_def, auto)
    declare state_of_state [simp]

    lemma state_of_idem: "state_of(state_of(s))=state_of(s)"

    apply (unfold state_of_def, auto)
    done
    declare state_of_idem [simp]

    lemma state_of_type [simp,TC]: "state_of(s)∈state"
    by (unfold state_of_def, auto)

    lemma lift_apply [simp]: "lift(x, s)=s`x"
    by (simp add: lift_def)

    (** Used in ClientImp **)

    lemma gen_Increains_state_of_eq:
         "Increasing(A, r, %s. f(state_of(s))) = Increasing(A, r, f)"
    apply (unfold Increasing_def, auto)
    done

    lemmas Increasing_state_ofD1 =
          gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD, standard]
    lemmas Increasing_state_ofD2 =
          gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD, standard]

    lemma Follows_state_of_eq:
         "Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =
          Follows(A, r, f, g)"
    apply (unfold Follows_def Increasing_def, auto)
    done

    lemmas Follows_state_ofD1 =
          Follows_state_of_eq [THEN equalityD1, THEN subsetD, standard]
    lemmas Follows_state_ofD2 =
          Follows_state_of_eq [THEN equalityD2, THEN subsetD, standard]

    lemma nat_list_inj_type: "n∈nat ==> nat_list_inj(n)∈list(nat)"
    by (induct_tac "n", auto)

    lemma length_nat_list_inj: "n∈nat ==> length(nat_list_inj(n)) = n"
    by (induct_tac "n", auto)

    lemma var_infinite_lemma:
      "(λx∈nat. nat_var_inj(x))∈inj(nat, var)"
    apply (unfold nat_var_inj_def)
    apply (rule_tac d = var_inj in lam_injective)
    apply (auto simp add: var.intros nat_list_inj_type)
    apply (simp add: length_nat_list_inj)
    done

    lemma nat_lepoll_var: "nat lepoll var"
    apply (unfold lepoll_def)
    apply (rule_tac x = " (λx∈nat. nat_var_inj (x))" in exI)
    apply (rule var_infinite_lemma)
    done

    lemma var_not_Finite: "~Finite(var)"
    apply (insert nat_not_Finite)
    apply (blast intro: lepoll_Finite [OF   nat_lepoll_var])
    done

    lemma not_Finite_imp_exist: "~Finite(A) ==> ∃x. x∈A"
    apply (subgoal_tac "A≠0")
    apply (auto simp add: Finite_0)
    done

    lemma Inter_Diff_var_iff:
         "Finite(A) ==> b∈(Inter(RepFun(var-A, B))) <-> (∀x∈var-A. b∈B(x))"
    apply (subgoal_tac "∃x. x∈var-A", auto)
    apply (subgoal_tac "~Finite (var-A) ")
    apply (drule not_Finite_imp_exist, auto)
    apply (cut_tac var_not_Finite)
    apply (erule swap)
    apply (rule_tac B = A in Diff_Finite, auto)
    done

    lemma Inter_var_DiffD:
         "[| b∈Inter(RepFun(var-A, B)); Finite(A); x∈var-A |] ==> b∈B(x)"
    by (simp add: Inter_Diff_var_iff)

    (* [| Finite(A); (∀x∈var-A. b∈B(x)) |] ==> b∈Inter(RepFun(var-A, B)) *)
    lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2, standard]

    declare Inter_var_DiffI [intro!]

    lemma Acts_subset_Int_Pow_simp [simp]:
         "Acts(F)<= A ∩ Pow(state*state)  <-> Acts(F)<=A"
    by (insert Acts_type [of F], auto)

    lemma setsum_nsetsum_eq:
         "[| Finite(A); ∀x∈A. g(x)∈nat |]
          ==> setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)"
    apply (erule Finite_induct)
    apply (auto simp add: int_of_add)
    done

    lemma nsetsum_cong:
         "[| A=B;  ∀x∈A. f(x)=g(x);  ∀x∈A. g(x)∈nat;  Finite(A) |]
          ==> nsetsum(f, A) = nsetsum(g, B)"
    apply (subgoal_tac "$# nsetsum (f, A) = $# nsetsum (g, B)", simp)
    apply (simp add: setsum_nsetsum_eq [symmetric] cong: setsum_cong)
    done

    end

### Various simple lemmas

lemma Nclients_NbT_gt_0:

      0 < Nclients ∧ 0 < NbT

lemma Nclients_NbT_not_0:

      Nclients ≠ 0 ∧ NbT ≠ 0

lemma Nclients_type:

      Nclients ∈ nat

lemma NbT_type:

      NbT ∈ nat

lemma INT_Nclient_iff:

      b ∈ \<Inter>RepFun(Nclients, B) <-> (∀x∈Nclients. b ∈ B(x))

lemma setsum_fun_mono:

      [| n ∈ nat; !!i. [| i ∈ nat; i < n |] ==> f(i) $≤ g(i) |]
      ==> setsum(f, n) $≤ setsum(g, n)

lemma tokens_type:

      l ∈ list(A) ==> tokens(l) ∈ nat

lemma tokens_mono_aux:

      [| xs ∈ list(A); ys ∈ list(A); ⟨xs, ys⟩ ∈ prefix(A) |]
      ==> tokens(xs) ≤ tokens(ys)

lemma tokens_mono:

      ⟨xs, ys⟩ ∈ prefix(A) ==> tokens(xs) ≤ tokens(ys)

lemma mono_tokens:

      mono1(list(A), prefix(A), nat, Le, tokens)

lemma tokens_append:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> tokens(xs @ ys) = tokens(xs) #+ tokens(ys)

### The function @{term bag_of}

lemma bag_of_type:

      l ∈ list(A) ==> bag_of(l) ∈ A -||> nat - {0}

lemma bag_of_multiset:

      l ∈ list(A) ==> multiset(bag_of(l)) ∧ mset_of(bag_of(l)) ⊆ A

lemma bag_of_append:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> bag_of(xs @ ys) = bag_of(xs) +# bag_of(ys)

lemma bag_of_mono_aux:

      [| xs ∈ list(A); ys ∈ list(A); ⟨xs, ys⟩ ∈ prefix(A) |]
      ==> ⟨bag_of(xs), bag_of(ys)⟩ ∈ MultLe(A, r)

lemma bag_of_mono:

      [| ⟨xs, ys⟩ ∈ prefix(A); xs ∈ list(A); ys ∈ list(A) |]
      ==> ⟨bag_of(xs), bag_of(ys)⟩ ∈ MultLe(A, r)

lemma mono_bag_of:

      mono1(list(A), prefix(A), A -||> nat - {0}, MultLe(A, r), bag_of)

### The function @{term msetsum}

lemmas nat_into_Fin:

      A ∈ nat ==> A ∈ Fin(A)

lemmas nat_into_Fin:

      A ∈ nat ==> A ∈ Fin(A)

lemma list_Int_length_Fin:

      l ∈ list(A) ==> C ∩ length(l) ∈ Fin(length(l))

lemma mem_Int_imp_lt_length:

      [| xs ∈ list(A); k ∈ C ∩ length(xs) |] ==> k < length(xs)

lemma Int_succ_right:

      A ∩ succ(k) = (if k ∈ A then cons(k, A ∩ k) else A ∩ k)

lemma bag_of_sublist_lemma:

      [| C ⊆ nat; x ∈ A; xs ∈ list(A) |]
      ==> msetsum(%i. {#nth(i, xs @ [x])#}, C ∩ succ(length(xs)), A) =
          (if length(xs) ∈ C
           then {#x#} +# msetsum(%x. {#nth(x, xs)#}, C ∩ length(xs), A)
           else msetsum(%x. {#nth(x, xs)#}, C ∩ length(xs), A))

lemma bag_of_sublist_lemma2:

      [| l ∈ list(A); C ⊆ nat |]
      ==> bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C ∩ length(l), A)

lemma nat_Int_length_eq:

      l ∈ list(A) ==> nat ∩ length(l) = length(l)

lemma bag_of_sublist:

      l ∈ list(A)
      ==> bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C ∩ length(l), A)

lemma bag_of_sublist_Un_Int:

      l ∈ list(A)
      ==> bag_of(sublist(l, B ∪ C)) +# bag_of(sublist(l, B ∩ C)) =
          bag_of(sublist(l, B)) +# bag_of(sublist(l, C))

lemma bag_of_sublist_Un_disjoint:

      [| l ∈ list(A); B ∩ C = 0 |]
      ==> bag_of(sublist(l, B ∪ C)) = bag_of(sublist(l, B)) +# bag_of(sublist(l, C))

lemma bag_of_sublist_UN_disjoint:

      [| Finite(I); !!i j. [| i ∈ I; j ∈ I; i ≠ j |] ==> A(i) ∩ A(j) = 0;
         l ∈ list(B) |]
      ==> bag_of(sublist(l, \<Union>i∈I. A(i))) =
          msetsum(%i. bag_of(sublist(l, A(i))), I, B)

lemma part_ord_Lt:

      part_ord(nat, Lt)

#### The function @{term all_distinct}

lemma all_distinct_Nil:

      all_distinct([])

lemma all_distinct_Cons:

      all_distinct(Cons(a, l)) <->
      (a ∈ set_of_list(l) --> False) ∧ (a ∉ set_of_list(l) --> all_distinct(l))

#### The function @{term state_of}

lemma state_of_state:

      s ∈ state ==> state_of(s) = s

lemma state_of_idem:

      state_of(state_of(s)) = state_of(s)

lemma state_of_type:

      state_of(s) ∈ state

lemma lift_apply:

      lift(x, s) = s ` x

lemma gen_Increains_state_of_eq:

      Increasing[A](r, %s. f(state_of(s))) = Increasing[A](r, f)

lemmas Increasing_state_ofD1:

      c ∈ Increasing[A](r, %s. f(state_of(s))) ==> c ∈ Increasing[A](r, f)

lemmas Increasing_state_ofD1:

      c ∈ Increasing[A](r, %s. f(state_of(s))) ==> c ∈ Increasing[A](r, f)

lemmas Increasing_state_ofD2:

      c ∈ Increasing[A](r, f) ==> c ∈ Increasing[A](r, %s. f(state_of(s)))

lemmas Increasing_state_ofD2:

      c ∈ Increasing[A](r, f) ==> c ∈ Increasing[A](r, %s. f(state_of(s)))

lemma Follows_state_of_eq:

      (%s. f(state_of(s))) Fols %s. g(state_of(s)) Wrt r / A = f Fols g Wrt r / A

lemmas Follows_state_ofD1:

      c ∈ (%s. f(state_of(s))) Fols %s. g(state_of(s)) Wrt r / A
      ==> c ∈ f Fols g Wrt r / A

lemmas Follows_state_ofD1:

      c ∈ (%s. f(state_of(s))) Fols %s. g(state_of(s)) Wrt r / A
      ==> c ∈ f Fols g Wrt r / A

lemmas Follows_state_ofD2:

      c ∈ f Fols g Wrt r / A
      ==> c ∈ (%s. f(state_of(s))) Fols %s. g(state_of(s)) Wrt r / A

lemmas Follows_state_ofD2:

      c ∈ f Fols g Wrt r / A
      ==> c ∈ (%s. f(state_of(s))) Fols %s. g(state_of(s)) Wrt r / A

lemma nat_list_inj_type:

      n ∈ nat ==> nat_list_inj(n) ∈ list(nat)

lemma length_nat_list_inj:

      n ∈ nat ==> length(nat_list_inj(n)) = n

lemma var_infinite_lemma:

      (λx∈nat. nat_var_inj(x)) ∈ inj(nat, var)

lemma nat_lepoll_var:

      nat lepoll var

lemma var_not_Finite:

      ¬ Finite(var)

lemma not_Finite_imp_exist:

      ¬ Finite(A) ==> ∃x. x ∈ A

lemma Inter_Diff_var_iff:

      Finite(A) ==> b ∈ \<Inter>RepFun(var - A, B) <-> (∀x∈var - A. b ∈ B(x))

lemma Inter_var_DiffD:

      [| b ∈ \<Inter>RepFun(var - A, B); Finite(A); x ∈ var - A |] ==> b ∈ B(x)

lemmas Inter_var_DiffI:

      [| Finite(A); ∀x∈var - A. b ∈ B(x) |] ==> b ∈ \<Inter>RepFun(var - A, B)

lemmas Inter_var_DiffI:

      [| Finite(A); ∀x∈var - A. b ∈ B(x) |] ==> b ∈ \<Inter>RepFun(var - A, B)

lemma Acts_subset_Int_Pow_simp:

      Acts(F) ⊆ A ∩ Pow(state × state) <-> Acts(F) ⊆ A

lemma setsum_nsetsum_eq:

      [| Finite(A); ∀x∈A. g(x) ∈ nat |]
      ==> setsum(%x. $# g(x), A) = $# nsetsum(%x. g(x), A)

lemma nsetsum_cong:

      [| A = B; ∀x∈A. f(x) = g(x); ∀x∈A. g(x) ∈ nat; Finite(A) |]
      ==> nsetsum(f, A) = nsetsum(g, B)