1.1 --- a/src/HOL/Finite_Set.thy Fri May 20 12:09:54 2011 +0200
1.2 +++ b/src/HOL/Finite_Set.thy Fri May 20 12:35:44 2011 +0200
1.3 @@ -578,12 +578,12 @@
1.4 assume "x \<noteq> a"
1.5 then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
1.6 using insertI by auto
1.7 - have 1: "f x y = f a (f x y')"
1.8 + have "f x y = f a (f x y')"
1.9 unfolding y by (rule fun_left_comm)
1.10 - have 2: "fold_graph f z (insert x A - {a}) (f x y')"
1.11 + moreover have "fold_graph f z (insert x A - {a}) (f x y')"
1.12 using y' and `x \<noteq> a` and `x \<notin> A`
1.13 by (simp add: insert_Diff_if fold_graph.insertI)
1.14 - from 1 2 show ?case by fast
1.15 + ultimately show ?case by fast
1.16 qed
1.17 qed simp
1.18
1.19 @@ -626,11 +626,12 @@
1.20 text{* The various recursion equations for @{const fold}: *}
1.21
1.22 lemma fold_insert [simp]:
1.23 - "finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
1.24 -apply (rule fold_equality)
1.25 -apply (erule fold_graph.insertI)
1.26 -apply (erule fold_graph_fold)
1.27 -done
1.28 + assumes "finite A" and "x \<notin> A"
1.29 + shows "fold f z (insert x A) = f x (fold f z A)"
1.30 +proof (rule fold_equality)
1.31 + from `finite A` have "fold_graph f z A (fold f z A)" by (rule fold_graph_fold)
1.32 + with `x \<notin> A`show "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI)
1.33 +qed
1.34
1.35 lemma fold_fun_comm:
1.36 "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
1.37 @@ -646,8 +647,8 @@
1.38 by (simp add: fold_fun_comm)
1.39
1.40 lemma fold_rec:
1.41 -assumes "finite A" and "x \<in> A"
1.42 -shows "fold f z A = f x (fold f z (A - {x}))"
1.43 + assumes "finite A" and "x \<in> A"
1.44 + shows "fold f z A = f x (fold f z (A - {x}))"
1.45 proof -
1.46 have A: "A = insert x (A - {x})" using `x \<in> A` by blast
1.47 then have "fold f z A = fold f z (insert x (A - {x}))" by simp
1.48 @@ -815,84 +816,49 @@
1.49 subsection {* The derived combinator @{text fold_image} *}
1.50
1.51 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
1.52 -where "fold_image f g = fold (%x y. f (g x) y)"
1.53 + where "fold_image f g = fold (\<lambda>x y. f (g x) y)"
1.54
1.55 lemma fold_image_empty[simp]: "fold_image f g z {} = z"
1.56 -by(simp add:fold_image_def)
1.57 + by (simp add:fold_image_def)
1.58
1.59 context ab_semigroup_mult
1.60 begin
1.61
1.62 lemma fold_image_insert[simp]:
1.63 -assumes "finite A" and "a \<notin> A"
1.64 -shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
1.65 + assumes "finite A" and "a \<notin> A"
1.66 + shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
1.67 proof -
1.68 - interpret I: comp_fun_commute "%x y. (g x) * y" proof
1.69 + interpret comp_fun_commute "%x y. (g x) * y" proof
1.70 qed (simp add: fun_eq_iff mult_ac)
1.71 show ?thesis using assms by (simp add: fold_image_def)
1.72 qed
1.73
1.74 -(*
1.75 -lemma fold_commute:
1.76 - "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
1.77 - apply (induct set: finite)
1.78 - apply simp
1.79 - apply (simp add: mult_left_commute [of x])
1.80 - done
1.81 -
1.82 -lemma fold_nest_Un_Int:
1.83 - "finite A ==> finite B
1.84 - ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
1.85 - apply (induct set: finite)
1.86 - apply simp
1.87 - apply (simp add: fold_commute Int_insert_left insert_absorb)
1.88 - done
1.89 -
1.90 -lemma fold_nest_Un_disjoint:
1.91 - "finite A ==> finite B ==> A Int B = {}
1.92 - ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
1.93 - by (simp add: fold_nest_Un_Int)
1.94 -*)
1.95 -
1.96 lemma fold_image_reindex:
1.97 -assumes fin: "finite A"
1.98 -shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
1.99 -using fin by induct auto
1.100 -
1.101 -(*
1.102 -text{*
1.103 - Fusion theorem, as described in Graham Hutton's paper,
1.104 - A Tutorial on the Universality and Expressiveness of Fold,
1.105 - JFP 9:4 (355-372), 1999.
1.106 -*}
1.107 -
1.108 -lemma fold_fusion:
1.109 - assumes "ab_semigroup_mult g"
1.110 - assumes fin: "finite A"
1.111 - and hyp: "\<And>x y. h (g x y) = times x (h y)"
1.112 - shows "h (fold g j w A) = fold times j (h w) A"
1.113 -proof -
1.114 - class_interpret ab_semigroup_mult [g] by fact
1.115 - show ?thesis using fin hyp by (induct set: finite) simp_all
1.116 -qed
1.117 -*)
1.118 + assumes "finite A"
1.119 + shows "inj_on h A \<Longrightarrow> fold_image times g z (h ` A) = fold_image times (g \<circ> h) z A"
1.120 + using assms by induct auto
1.121
1.122 lemma fold_image_cong:
1.123 - "finite A \<Longrightarrow>
1.124 - (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A"
1.125 -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")
1.126 - apply simp
1.127 -apply (erule finite_induct, simp)
1.128 -apply (simp add: subset_insert_iff, clarify)
1.129 -apply (subgoal_tac "finite C")
1.130 - prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
1.131 -apply (subgoal_tac "C = insert x (C - {x})")
1.132 - prefer 2 apply blast
1.133 -apply (erule ssubst)
1.134 -apply (drule spec)
1.135 -apply (erule (1) notE impE)
1.136 -apply (simp add: Ball_def del: insert_Diff_single)
1.137 -done
1.138 + assumes "finite A" and g_h: "\<And>x. x\<in>A \<Longrightarrow> g x = h x"
1.139 + shows "fold_image times g z A = fold_image times h z A"
1.140 +proof -
1.141 + from `finite A`
1.142 + have "\<And>C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C"
1.143 + proof (induct arbitrary: C)
1.144 + case empty then show ?case by simp
1.145 + next
1.146 + case (insert x F) then show ?case apply -
1.147 + apply (simp add: subset_insert_iff, clarify)
1.148 + apply (subgoal_tac "finite C")
1.149 + prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
1.150 + apply (subgoal_tac "C = insert x (C - {x})")
1.151 + prefer 2 apply blast
1.152 + apply (erule ssubst)
1.153 + apply (simp add: Ball_def del: insert_Diff_single)
1.154 + done
1.155 + qed
1.156 + with g_h show ?thesis by simp
1.157 +qed
1.158
1.159 end
1.160