| changeset 63539 | 70d4d9e5707b |
| parent 63194 | 0b7bdb75f451 |
| child 63965 | d510b816ea41 |
| 63533:42b6186fc0e4 | 63539:70d4d9e5707b |
|---|---|
50 fold_random_permutation f x A = |
50 fold_random_permutation f x A = |
51 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" |
51 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" |
52 by (force, simp_all) |
52 by (force, simp_all) |
53 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)") |
53 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)") |
54 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a |
54 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a |
55 assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
55 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
56 moreover from this have "card A > 0" by (simp add: card_gt_0_iff) |
56 then have "card A > 0" by (simp add: card_gt_0_iff) |
57 ultimately show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" |
57 with A show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" |
58 by simp |
58 by simp |
59 qed simp_all |
59 qed simp_all |
60 |
60 |
61 |
61 |
62 text \<open> |
62 text \<open> |
126 pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))" |
126 pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))" |
127 by (force, simp_all) |
127 by (force, simp_all) |
128 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") |
128 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") |
129 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b |
129 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b |
130 and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" |
130 and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" |
131 assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
131 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
132 moreover from this have "card A > 0" by (simp add: card_gt_0_iff) |
132 then have "card A > 0" by (simp add: card_gt_0_iff) |
133 ultimately show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)" |
133 with A show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)" |
134 by simp |
134 by simp |
135 qed simp_all |
135 qed simp_all |
136 |
136 |
137 text \<open> |
137 text \<open> |
138 We now show that the recursive definition is equivalent to |
138 We now show that the recursive definition is equivalent to |