theory CNodeInv_AI

lemma fold_Int_sub:
  assumes "finite S" "finite T"
  shows "(\<Sum>x \<in> (S \<inter> T). (f x :: nat)) = (\<Sum>x \<in> T. f x) - (\<Sum>x \<in> (T - S). f x)" proof - from assms sum.union_disjoint[where A="S \<inter> T" and B="T - S" and g=f] show ?thesis apply simp apply (drule meta_mp) apply blast apply (subgoal_tac "S \<inter> T \<union> (T - S) = T") apply simp apply blast done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S) proof (state)
goal (1 subgoal):
 1. comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S) proof (chain)
picking this:
finite S
finite T
\<lbrakk>finite (S \<inter> T); finite (T - S); S \<inter> T \<inter> (T - S) = {}\<rbrakk> \<Longrightarrow> comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S) proof (prove)
using this:
finite S
finite T
\<lbrakk>finite (S \<inter> T); finite (T - S); S \<inter> T \<inter> (T - S) = {}\<rbrakk> \<Longrightarrow> comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S)

goal (1 subgoal):
 1. comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; finite T; S \<inter> T \<inter> (T - S) = {} \<Longrightarrow> comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S)\<rbrakk> \<Longrightarrow> comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite S; finite T\<rbrakk> \<Longrightarrow> S \<inter> T \<inter> (T - S) = {}
 2. \<lbrakk>finite S; finite T; comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S)\<rbrakk> \<Longrightarrow> comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; finite T; comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S)\<rbrakk> \<Longrightarrow> comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite S; finite T; comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S); S \<inter> T \<union> (T - S) = T\<rbrakk> \<Longrightarrow> comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S)
 2. \<lbrakk>finite S; finite T; comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S)\<rbrakk> \<Longrightarrow> S \<inter> T \<union> (T - S) = T proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; finite T; comm_monoid_add_class.sum f (S \<inter> T \<union> (T - S)) = comm_monoid_add_class.sum f (S \<inter> T) + comm_monoid_add_class.sum f (T - S)\<rbrakk> \<Longrightarrow> S \<inter> T \<union> (T - S) = T proof (prove)
goal:
No subgoals! proof (state)
this:
comm_monoid_add_class.sum f (S \<inter> T) = comm_monoid_add_class.sum f T - comm_monoid_add_class.sum f (T - S)

goal:
No subgoals!