# HG changeset patch # User haftmann # Date 1305887744 -7200 # Node ID d1aad0957eb2360ab16c30f617f6d7cc6b9715a7 # Parent f115492c7c8ddddb260da6e468fa2c3062ab40dc tuned proofs diff -r f115492c7c8d -r d1aad0957eb2 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri May 20 12:09:54 2011 +0200 +++ b/src/HOL/Finite_Set.thy Fri May 20 12:35:44 2011 +0200 @@ -578,12 +578,12 @@ assume "x \ a" then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'" using insertI by auto - have 1: "f x y = f a (f x y')" + have "f x y = f a (f x y')" unfolding y by (rule fun_left_comm) - have 2: "fold_graph f z (insert x A - {a}) (f x y')" + moreover have "fold_graph f z (insert x A - {a}) (f x y')" using y' and `x \ a` and `x \ A` by (simp add: insert_Diff_if fold_graph.insertI) - from 1 2 show ?case by fast + ultimately show ?case by fast qed qed simp @@ -626,11 +626,12 @@ text{* The various recursion equations for @{const fold}: *} lemma fold_insert [simp]: - "finite A ==> x \ A ==> fold f z (insert x A) = f x (fold f z A)" -apply (rule fold_equality) -apply (erule fold_graph.insertI) -apply (erule fold_graph_fold) -done + assumes "finite A" and "x \ A" + shows "fold f z (insert x A) = f x (fold f z A)" +proof (rule fold_equality) + from `finite A` have "fold_graph f z A (fold f z A)" by (rule fold_graph_fold) + with `x \ A`show "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI) +qed lemma fold_fun_comm: "finite A \ f x (fold f z A) = fold f (f x z) A" @@ -646,8 +647,8 @@ by (simp add: fold_fun_comm) lemma fold_rec: -assumes "finite A" and "x \ A" -shows "fold f z A = f x (fold f z (A - {x}))" + assumes "finite A" and "x \ A" + shows "fold f z A = f x (fold f z (A - {x}))" proof - have A: "A = insert x (A - {x})" using `x \ A` by blast then have "fold f z A = fold f z (insert x (A - {x}))" by simp @@ -815,84 +816,49 @@ subsection {* The derived combinator @{text fold_image} *} definition fold_image :: "('b \ 'b \ 'b) \ ('a \ 'b) \ 'b \ 'a set \ 'b" -where "fold_image f g = fold (%x y. f (g x) y)" + where "fold_image f g = fold (\x y. f (g x) y)" lemma fold_image_empty[simp]: "fold_image f g z {} = z" -by(simp add:fold_image_def) + by (simp add:fold_image_def) context ab_semigroup_mult begin lemma fold_image_insert[simp]: -assumes "finite A" and "a \ A" -shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" + assumes "finite A" and "a \ A" + shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" proof - - interpret I: comp_fun_commute "%x y. (g x) * y" proof + interpret comp_fun_commute "%x y. (g x) * y" proof qed (simp add: fun_eq_iff mult_ac) show ?thesis using assms by (simp add: fold_image_def) qed -(* -lemma fold_commute: - "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)" - apply (induct set: finite) - apply simp - apply (simp add: mult_left_commute [of x]) - done - -lemma fold_nest_Un_Int: - "finite A ==> finite B - ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)" - apply (induct set: finite) - apply simp - apply (simp add: fold_commute Int_insert_left insert_absorb) - done - -lemma fold_nest_Un_disjoint: - "finite A ==> finite B ==> A Int B = {} - ==> fold times g z (A Un B) = fold times g (fold times g z B) A" - by (simp add: fold_nest_Un_Int) -*) - lemma fold_image_reindex: -assumes fin: "finite A" -shows "inj_on h A \ fold_image times g z (h`A) = fold_image times (g\h) z A" -using fin by induct auto - -(* -text{* - Fusion theorem, as described in Graham Hutton's paper, - A Tutorial on the Universality and Expressiveness of Fold, - JFP 9:4 (355-372), 1999. -*} - -lemma fold_fusion: - assumes "ab_semigroup_mult g" - assumes fin: "finite A" - and hyp: "\x y. h (g x y) = times x (h y)" - shows "h (fold g j w A) = fold times j (h w) A" -proof - - class_interpret ab_semigroup_mult [g] by fact - show ?thesis using fin hyp by (induct set: finite) simp_all -qed -*) + assumes "finite A" + shows "inj_on h A \ fold_image times g z (h ` A) = fold_image times (g \ h) z A" + using assms by induct auto lemma fold_image_cong: - "finite A \ - (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A" -apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C") - apply simp -apply (erule finite_induct, simp) -apply (simp add: subset_insert_iff, clarify) -apply (subgoal_tac "finite C") - prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) -apply (subgoal_tac "C = insert x (C - {x})") - prefer 2 apply blast -apply (erule ssubst) -apply (drule spec) -apply (erule (1) notE impE) -apply (simp add: Ball_def del: insert_Diff_single) -done + assumes "finite A" and g_h: "\x. x\A \ g x = h x" + shows "fold_image times g z A = fold_image times h z A" +proof - + from `finite A` + have "\C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C" + proof (induct arbitrary: C) + case empty then show ?case by simp + next + case (insert x F) then show ?case apply - + apply (simp add: subset_insert_iff, clarify) + apply (subgoal_tac "finite C") + prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) + apply (subgoal_tac "C = insert x (C - {x})") + prefer 2 apply blast + apply (erule ssubst) + apply (simp add: Ball_def del: insert_Diff_single) + done + qed + with g_h show ?thesis by simp +qed end