49 "fold_random_permutation f x {} = return_pmf x" |
49 "fold_random_permutation f x {} = return_pmf x" |
50 | "\<not>finite A \<Longrightarrow> fold_random_permutation f x A = return_pmf x" |
50 | "\<not>finite A \<Longrightarrow> fold_random_permutation f x A = return_pmf x" |
51 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> |
51 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> |
52 fold_random_permutation f x A = |
52 fold_random_permutation f x A = |
53 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" |
53 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" |
54 by (force, simp_all) |
54 by simp_all fastforce |
55 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)") |
55 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)") |
56 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a |
56 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a |
57 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
57 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
58 then have "card A > 0" by (simp add: card_gt_0_iff) |
58 then have "card A > 0" by (simp add: card_gt_0_iff) |
59 with A show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" |
59 with A show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" |
124 "fold_bind_random_permutation f g x {} = g x" |
124 "fold_bind_random_permutation f g x {} = g x" |
125 | "\<not>finite A \<Longrightarrow> fold_bind_random_permutation f g x A = g x" |
125 | "\<not>finite A \<Longrightarrow> fold_bind_random_permutation f g x A = g x" |
126 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> |
126 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> |
127 fold_bind_random_permutation f g x A = |
127 fold_bind_random_permutation f g x A = |
128 pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))" |
128 pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))" |
129 by (force, simp_all) |
129 by simp_all fastforce |
130 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") |
130 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") |
131 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b |
131 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b |
132 and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" |
132 and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" |
133 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
133 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
134 then have "card A > 0" by (simp add: card_gt_0_iff) |
134 then have "card A > 0" by (simp add: card_gt_0_iff) |