diff --git a/thys/Buchi_Complementation/Ranking.thy b/thys/Buchi_Complementation/Ranking.thy --- a/thys/Buchi_Complementation/Ranking.thy +++ b/thys/Buchi_Complementation/Ranking.thy @@ -1,478 +1,478 @@ section \Rankings\ theory Ranking imports "Alternate" "Graph" begin subsection \Rankings\ type_synonym 'state ranking = "'state node \ nat" definition ranking :: "('label, 'state) nba \ 'label stream \ 'state ranking \ bool" where "ranking A w f \ (\ v \ gunodes A w. f v \ 2 * card (nodes A)) \ (\ v \ gunodes A w. \ u \ gusuccessors A w v. f u \ f v) \ (\ v \ gunodes A w. gaccepting A v \ even (f v)) \ (\ v \ gunodes A w. \ r k. gurun A w r v \ smap f (gtrace r v) = sconst k \ odd k)" subsection \Ranking Implies Word not in Language\ lemma ranking_stuck: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n k where "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" proof - have 0: "f u \ f v" if "v \ gunodes A w" "u \ gusuccessors A w v" for v u using assms(1) that unfolding ranking_def by auto have 1: "shd (v ## gtrace r v) \ gunodes A w" using assms(2) by auto have 2: "sdescending (smap f (v ## gtrace r v))" using 1 assms(3) proof (coinduction arbitrary: r v rule: sdescending.coinduct) case sdescending obtain u s where 1: "r = u ## s" using stream.exhaust by blast have 2: "v \ gunodes A w" using sdescending(1) by simp have 3: "gurun A w (u ## s) v" using sdescending(2) 1 by auto have 4: "u \ gusuccessors A w v" using 3 by auto have 5: "u \ gureachable A w v" using graph.reachable_successors 4 by blast show ?case unfolding 1 proof (intro exI conjI disjI1) show "f u \ f v" using 0 2 4 by this show "shd (u ## gtrace s u) \ gunodes A w" using 2 5 by auto show "gurun A w s u" using 3 by auto qed auto qed obtain s k where 3: "smap f (v ## gtrace r v) = s @- sconst k" using sdescending_stuck[OF 2] by metis have "gtrace (sdrop (Suc (length s)) r) (gtarget (stake (Suc (length s)) r) v) = sdrop (Suc (length s)) (gtrace r v)" using sscan_sdrop by rule also have "smap f \ = sdrop (length s) (smap f (v ## gtrace r v))" by (metis "3" id_apply sdrop_simps(2) sdrop_smap sdrop_stl shift_eq siterate.simps(2) stream.sel(2)) also have "\ = sconst k" unfolding 3 using shift_eq by metis finally show ?thesis using that by blast qed lemma ranking_stuck_odd: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n where "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd" proof - obtain n k where 1: "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" using ranking_stuck assms by this have 2: "gtarget (stake n r) v \ gunodes A w" using assms(2, 3) by (simp add: graph.nodes_target graph.run_stake) have 3: "gurun A w (sdrop n r) (gtarget (stake n r) v)" using assms(2, 3) by (simp add: graph.run_sdrop) have 4: "odd k" using 1 2 3 assms(1) unfolding ranking_def by meson have 5: "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd" unfolding 1 using 4 by simp show ?thesis using that 5 by this qed lemma ranking_language: assumes "ranking A w f" shows "w \ language A" proof assume 1: "w \ language A" obtain r p where 2: "run A (w ||| r) p" "p \ initial A" "infs (accepting A) (p ## r)" using 1 by rule let ?r = "fromN 1 ||| r" let ?v = "(0, p)" have 3: "?v \ gunodes A w" "gurun A w ?r ?v" using 2(1, 2) by (auto intro: run_grun) obtain n where 4: "Ball (sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v)))) odd" using ranking_stuck_odd assms 3 by this let ?s = "stake n ?r" let ?t = "sdrop n ?r" let ?u = "gtarget ?s ?v" have "sset (gtrace ?t ?u) \ gureachable A w ?v" proof (intro graph.reachable_trace graph.reachable_target graph.reachable.reflexive) show "gupath A w ?s ?v" using graph.run_stake 3(2) by this show "gurun A w ?t ?u" using graph.run_sdrop 3(2) by this qed also have "\ \ gunodes A w" using 3(1) by blast finally have 7: "sset (gtrace ?t ?u) \ gunodes A w" by this have 8: "\ p. p \ gunodes A w \ gaccepting A p \ even (f p)" using assms unfolding ranking_def by auto have 9: "\ p. p \ sset (gtrace ?t ?u) \ gaccepting A p \ even (f p)" using 7 8 by auto have 19: "infs (accepting A) (smap snd ?r)" using 2(3) by simp have 18: "infs (gaccepting A) ?r" using 19 by simp have 17: "infs (gaccepting A) (gtrace ?r ?v)" using 18 unfolding gtrace_alt_def by this have 16: "infs (gaccepting A) (gtrace (?s @- ?t) ?v)" using 17 unfolding stake_sdrop by this have 15: "infs (gaccepting A) (gtrace ?t ?u)" using 16 by simp have 13: "infs (even \ f) (gtrace ?t ?u)" using infs_mono[OF _ 15] 9 by simp have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by (simp add: comp_def) have 11: "Bex (sset (smap f (gtrace ?t ?u))) even" using 12 infs_any by metis show False using 4 11 by auto qed subsection \Word not in Language Implies Ranking\ subsubsection \Removal of Endangered Nodes\ definition clean :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "clean A w V \ {v \ V. infinite (greachable A w V v)}" lemma clean_decreasing: "clean A w V \ V" unfolding clean_def by auto lemma clean_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ clean A w V \ v \ clean A w V" proof - assume 1: "u \ clean A w V" have 2: "u \ V" "infinite (greachable A w V u)" using 1 unfolding clean_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast have 5: "infinite (greachable A w V v)" using 2(2) 4 by (simp add: infinite_super) show "v \ clean A w V" unfolding clean_def using assms(1) 5 by simp qed subsubsection \Removal of Safe Nodes\ definition prune :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "prune A w V \ {v \ V. \ u \ greachable A w V v. gaccepting A u}" lemma prune_decreasing: "prune A w V \ V" unfolding prune_def by auto lemma prune_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ prune A w V \ v \ prune A w V" proof - assume 1: "u \ prune A w V" have 2: "u \ V" "\ x \ greachable A w V u. gaccepting A x" using 1 unfolding prune_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast show "v \ prune A w V" unfolding prune_def using assms(1) 2(2) 4 by auto qed subsubsection \Run Graph Interation\ definition graph :: "('label, 'state) nba \ 'label stream \ nat \ 'state node set" where "graph A w k \ alternate (clean A w) (prune A w) k (gunodes A w)" abbreviation "level A w k l \ {v \ graph A w k. fst v = l}" lemma graph_0[simp]: "graph A w 0 = gunodes A w" unfolding graph_def by simp lemma graph_Suc[simp]: "graph A w (Suc k) = (if even k then clean A w else prune A w) (graph A w k)" unfolding graph_def by simp lemma graph_antimono: "antimono (graph A w)" using alternate_antimono clean_decreasing prune_decreasing - unfolding antimono_def le_fun_def graph_def + unfolding monotone_def le_fun_def graph_def by metis lemma graph_nodes: "graph A w k \ gunodes A w" using graph_0 graph_antimono le0 antimonoD by metis lemma graph_successors: assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "u \ graph A w k \ v \ graph A w k" using assms proof (induct k arbitrary: u v) case 0 show ?case using 0(2) by simp next case (Suc k) have 1: "v \ graph A w k" using Suc using antimono_iff_le_Suc graph_antimono rev_subsetD by blast show ?case using Suc(2) clean_successors[OF 1 Suc(4)] prune_successors[OF 1 Suc(4)] by auto qed lemma graph_level_finite: assumes "finite (nodes A)" shows "finite (level A w k l)" proof - have "level A w k l \ {v \ gunodes A w. fst v = l}" by (simp add: graph_nodes subset_CollectI) also have "{v \ gunodes A w. fst v = l} \ {l} \ nodes A" using gnodes_nodes by force also have "finite ({l} \ nodes A)" using assms(1) by simp finally show ?thesis by this qed lemma find_safe: assumes "w \ language A" assumes "V \ {}" "V \ gunodes A w" assumes "\ v. v \ V \ gsuccessors A w V v \ {}" obtains v where "v \ V" "\ u \ greachable A w V v. \ gaccepting A u" proof (rule ccontr) assume 1: "\ thesis" have 2: "\ v. v \ V \ \ u \ greachable A w V v. gaccepting A u" using that 1 by auto have 3: "\ r v. v \ initial A \ run A (w ||| r) v \ fins (accepting A) r" using assms(1) by auto obtain v where 4: "v \ V" using assms(2) by force obtain x where 5: "x \ greachable A w V v" "gaccepting A x" using 2 4 by blast obtain y where 50: "gpath A w V y v" "x = gtarget y v" using 5(1) by rule obtain r where 6: "grun A w V r x" "infs (\ x. x \ V \ gaccepting A x) r" proof (rule graph.recurring_condition) show "x \ V \ gaccepting A x" using greachable_subset 4 5 by blast next fix v assume 1: "v \ V \ gaccepting A v" obtain v' where 20: "v' \ gsuccessors A w V v" using assms(4) 1 by (meson IntE equals0I) have 21: "v' \ V" using 20 by auto have 22: "\ u \ greachable A w V v'. u \ V \ gaccepting A u" using greachable_subset 2 21 by blast obtain r where 30: "gpath A w V r v'" "gtarget r v' \ V \ gaccepting A (gtarget r v')" using 22 by blast show "\ r. r \ [] \ gpath A w V r v \ gtarget r v \ V \ gaccepting A (gtarget r v)" proof (intro exI conjI) show "v' # r \ []" by simp show "gpath A w V (v' # r) v" using 20 30 by auto show "gtarget (v' # r) v \ V" using 30 by simp show "gaccepting A (gtarget (v' # r) v)" using 30 by simp qed qed auto obtain u where 100: "u \ ginitial A" "v \ gureachable A w u" using 4 assms(3) by blast have 101: "gupath A w y v" using gpath_subset 50(1) subset_UNIV by this have 102: "gurun A w r x" using grun_subset 6(1) subset_UNIV by this obtain t where 103: "gupath A w t u" "v = gtarget t u" using 100(2) by rule have 104: "gurun A w (t @- y @- r) u" using 101 102 103 50(2) by auto obtain s q where 7: "t @- y @- r = fromN (Suc 0) ||| s" "u = (0, q)" using grun_elim[OF 104] 100(1) by blast have 8: "run A (w ||| s) q" using grun_run[OF 104[unfolded 7]] by simp have 9: "q \ initial A" using 100(1) 7(2) by auto have 91: "sset (trace (w ||| s) q) \ reachable A q" using nba.reachable_trace nba.reachable.reflexive 8 by this have 10: "fins (accepting A) s" using 3 9 8 by this have 12: "infs (gaccepting A) r" using infs_mono[OF _ 6(2)] by simp have "s = smap snd (t @- y @- r)" unfolding 7(1) by simp also have "infs (accepting A) \" using 12 by (simp add: comp_def) finally have 13: "infs (accepting A) s" by this show False using 10 13 by simp qed lemma remove_run: assumes "finite (nodes A)" "w \ language A" assumes "V \ gunodes A w" "clean A w V \ {}" obtains v r where "grun A w V r v" "sset (gtrace r v) \ clean A w V" "sset (gtrace r v) \ - prune A w (clean A w V)" proof - obtain u where 1: "u \ clean A w V" "\ x \ greachable A w (clean A w V) u. \ gaccepting A x" proof (rule find_safe) show "w \ language A" using assms(2) by this show "clean A w V \ {}" using assms(4) by this show "clean A w V \ gunodes A w" using assms(3) by (meson clean_decreasing subset_iff) next fix v assume 1: "v \ clean A w V" have 2: "v \ V" using 1 clean_decreasing by blast have 3: "infinite (greachable A w V v)" using 1 clean_def by auto have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 2 assms(1, 3) finite_nodes_gsuccessors by blast finally have 4: "finite (gsuccessors A w V v)" by this have 5: "infinite (insert v (\((greachable A w V) ` (gsuccessors A w V v))))" using graph.reachable_step 3 by metis obtain u where 6: "u \ gsuccessors A w V v" "infinite (greachable A w V u)" using 4 5 by auto have 7: "u \ clean A w V" using 6 unfolding clean_def by auto show "gsuccessors A w (clean A w V) v \ {}" using 6(1) 7 by auto qed auto have 2: "u \ V" using 1(1) unfolding clean_def by auto have 3: "infinite (greachable A w V u)" using 1(1) unfolding clean_def by simp have 4: "finite (gsuccessors A w V v)" if "v \ greachable A w V u" for v proof - have 1: "v \ V" using that greachable_subset 2 by blast have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 1 assms(1, 3) finite_nodes_gsuccessors by blast finally show ?thesis by this qed obtain r where 5: "grun A w V r u" using graph.koenig[OF 3 4] by this have 6: "greachable A w V u \ V" using 2 greachable_subset by blast have 7: "sset (gtrace r u) \ V" using graph.reachable_trace[OF graph.reachable.reflexive 5(1)] 6 by blast have 8: "sset (gtrace r u) \ clean A w V" unfolding clean_def using 7 infinite_greachable_gtrace[OF 5(1)] by auto have 9: "sset (gtrace r u) \ greachable A w (clean A w V) u" using 5 8 by (metis graph.reachable.reflexive graph.reachable_trace grun_subset) show ?thesis proof show "grun A w V r u" using 5(1) by this show "sset (gtrace r u) \ clean A w V" using 8 by this show "sset (gtrace r u) \ - prune A w (clean A w V)" proof (intro subsetI ComplI) fix p assume 10: "p \ sset (gtrace r u)" "p \ prune A w (clean A w V)" have 20: "\ x \ greachable A w (clean A w V) p. gaccepting A x" using 10(2) unfolding prune_def by auto have 30: "greachable A w (clean A w V) p \ greachable A w (clean A w V) u" using 10(1) 9 by blast show "False" using 1(2) 20 30 by force qed qed qed lemma level_bounded: assumes "finite (nodes A)" "w \ language A" obtains n where "\ l. l \ n \ card (level A w (2 * k) l) \ card (nodes A) - k" proof (induct k arbitrary: thesis) case (0) show ?case proof (rule 0) fix l :: nat have "finite ({l} \ nodes A)" using assms(1) by simp also have "level A w 0 l \ {l} \ nodes A" using gnodes_nodes by force also (card_mono) have "card \ = card (nodes A)" using assms(1) by simp finally show "card (level A w (2 * 0) l) \ card (nodes A) - 0" by simp qed next case (Suc k) show ?case proof (cases "graph A w (Suc (2 * k)) = {}") case True have 3: "graph A w (2 * Suc k) = {}" using True prune_decreasing by simp blast show ?thesis using Suc(2) 3 by simp next case False obtain v r where 1: "grun A w (graph A w (2 * k)) r v" "sset (gtrace r v) \ graph A w (Suc (2 * k))" "sset (gtrace r v) \ - graph A w (Suc (Suc (2 * k)))" proof (rule remove_run) show "finite (nodes A)" "w \ language A" using assms by this show "clean A w (graph A w (2 * k)) \ {}" using False by simp show "graph A w (2 * k) \ gunodes A w" using graph_nodes by this qed auto obtain l q where 2: "v = (l, q)" by force obtain n where 90: "\ l. n \ l \ card (level A w (2 * k) l) \ card (nodes A) - k" using Suc(1) by blast show ?thesis proof (rule Suc(2)) fix j assume 100: "n + Suc l \ j" have 6: "graph A w (Suc (Suc (2 * k))) \ graph A w (Suc (2 * k))" using graph_antimono antimono_iff_le_Suc by blast have 101: "gtrace r v !! (j - Suc l) \ graph A w (Suc (2 * k))" using 1(2) snth_sset by auto have 102: "gtrace r v !! (j - Suc l) \ graph A w (Suc (Suc (2 * k)))" using 1(3) snth_sset by blast have 103: "gtrace r v !! (j - Suc l) \ level A w (Suc (2 * k)) j" using 1(1) 100 101 2 by (auto elim: grun_elim) have 104: "gtrace r v !! (j - Suc l) \ level A w (Suc (Suc (2 * k))) j" using 100 102 by simp have "level A w (2 * Suc k) j = level A w (Suc (Suc (2 * k))) j" by simp also have "\ \ level A w (Suc (2 * k)) j" using 103 104 6 by blast also have "\ \ level A w (2 * k) j" by (simp add: Collect_mono clean_def) finally have 105: "level A w (2 * Suc k) j \ level A w (2 * k) j" by this have "card (level A w (2 * Suc k) j) < card (level A w (2 * k) j)" using assms(1) 105 by (simp add: graph_level_finite psubset_card_mono) also have "\ \ card (nodes A) - k" using 90 100 by simp finally show "card (level A w (2 * Suc k) j) \ card (nodes A) - Suc k" by simp qed qed qed lemma graph_empty: assumes "finite (nodes A)" "w \ language A" shows "graph A w (Suc (2 * card (nodes A))) = {}" proof - obtain n where 1: "\ l. l \ n \ card (level A w (2 * card (nodes A)) l) = 0" using level_bounded[OF assms(1, 2), of "card (nodes A)"] by auto have "graph A w (2 * card (nodes A)) = (\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ (\ l \ {n ..}. level A w (2 * card (nodes A)) l)" by auto also have "(\ l \ {n ..}. level A w (2 * card (nodes A)) l) = {}" using graph_level_finite assms(1) 1 by fastforce also have "finite ((\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ {})" using graph_level_finite assms(1) by auto finally have 100: "finite (graph A w (2 * card (nodes A)))" by this have 101: "finite (greachable A w (graph A w (2 * card (nodes A))) v)" for v using 100 greachable_subset[of A w "graph A w (2 * card (nodes A))" v] using finite_insert infinite_super by auto show ?thesis using 101 by (simp add: clean_def) qed lemma graph_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ graph A w k" shows "k \ 2 * card (nodes A)" using graph_empty graph_antimono assms - by (metis (no_types, lifting) Suc_leI antimono_def basic_trans_rules(30) empty_iff not_le_imp_less) + by (metis Suc_leI empty_iff monotone_def not_le_imp_less rev_subsetD) subsection \Node Ranks\ definition rank :: "('label, 'state) nba \ 'label stream \ 'state node \ nat" where "rank A w v \ GREATEST k. v \ graph A w k" lemma rank_member: assumes "finite (nodes A)" "w \ language A" "v \ gunodes A w" shows "v \ graph A w (rank A w v)" unfolding rank_def proof (rule GreatestI_nat) show "v \ graph A w 0" using assms(3) by simp show "k \ 2 * card (nodes A)" if "v \ graph A w k" for k using graph_le assms(1, 2) that by blast qed lemma rank_removed: assumes "finite (nodes A)" "w \ language A" shows "v \ graph A w (Suc (rank A w v))" proof assume "v \ graph A w (Suc (rank A w v))" then have 2: "Suc (rank A w v) \ rank A w v" unfolding rank_def using Greatest_le_nat graph_le assms by metis then show "False" by auto qed lemma rank_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "rank A w u \ rank A w v" unfolding rank_def proof (rule Greatest_le_nat) have 1: "u \ gureachable A w v" using graph.reachable_successors assms(4) by blast have 2: "u \ gunodes A w" using assms(3) 1 by auto show "v \ graph A w (GREATEST k. u \ graph A w k)" unfolding rank_def[symmetric] proof (rule graph_successors) show "v \ gunodes A w" using assms(3) by this show "u \ gusuccessors A w v" using assms(4) by this show "u \ graph A w (rank A w u)" using rank_member assms(1, 2) 2 by this qed show "k \ 2 * card (nodes A)" if "v \ graph A w k" for k using graph_le assms(1, 2) that by blast qed lemma language_ranking: assumes "finite (nodes A)" "w \ language A" shows "ranking A w (rank A w)" unfolding ranking_def proof (intro conjI ballI allI impI) fix v assume 1: "v \ gunodes A w" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1 by this show "rank A w v \ 2 * card (nodes A)" using graph_le assms 2 by this next fix v u assume 1: "v \ gunodes A w" "u \ gusuccessors A w v" show "rank A w u \ rank A w v" using rank_le assms 1 by this next fix v assume 1: "v \ gunodes A w" "gaccepting A v" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1(1) by this have 3: "v \ graph A w (Suc (rank A w v))" using rank_removed assms by this have 4: "v \ prune A w (graph A w (rank A w v))" using 2 1(2) unfolding prune_def by auto have 5: "graph A w (Suc (rank A w v)) \ prune A w (graph A w (rank A w v))" using 3 4 by blast show "even (rank A w v)" using 5 by auto next fix v r k assume 1: "v \ gunodes A w" "gurun A w r v" "smap (rank A w) (gtrace r v) = sconst k" have "sset (gtrace r v) \ gureachable A w v" using 1(2) by (metis graph.reachable.reflexive graph.reachable_trace) then have 6: "sset (gtrace r v) \ gunodes A w" using 1(1) by blast have 60: "rank A w ` sset (gtrace r v) \ {k}" using 1(3) by (metis equalityD1 sset_sconst stream.set_map) have 50: "sset (gtrace r v) \ graph A w k" using rank_member[OF assms] subsetD[OF 6] 60 unfolding image_subset_iff by auto have 70: "grun A w (graph A w k) r v" using grun_subset 1(2) 50 by this have 7: "sset (gtrace r v) \ clean A w (graph A w k)" unfolding clean_def using 50 infinite_greachable_gtrace[OF 70] by auto have 8: "sset (gtrace r v) \ graph A w (Suc k) = {}" using rank_removed[OF assms] 60 by blast have 9: "sset (gtrace r v) \ {}" using stream.set_sel(1) by auto have 10: "graph A w (Suc k) \ clean A w (graph A w k)" using 7 8 9 by blast show "odd k" using 10 unfolding graph_Suc by auto qed subsection \Correctness Theorem\ theorem language_ranking_iff: assumes "finite (nodes A)" shows "w \ language A \ (\ f. ranking A w f)" using ranking_language language_ranking assms by blast end diff --git a/thys/Markov_Models/Markov_Decision_Process.thy b/thys/Markov_Models/Markov_Decision_Process.thy --- a/thys/Markov_Models/Markov_Decision_Process.thy +++ b/thys/Markov_Models/Markov_Decision_Process.thy @@ -1,814 +1,816 @@ (* Author: Johannes Hölzl *) section \Markov Decision Processes\ theory Markov_Decision_Process imports Discrete_Time_Markov_Chain begin definition "some_elem s = (SOME x. x \ s)" lemma some_elem_ne: "s \ {} \ some_elem s \ s" unfolding some_elem_def by (auto intro: someI) subsection \Configurations\ text \ We want to construct a \emph{non-free} codatatype \'s cfg = Cfg (state: 's) (action: 's pmf) (cont: 's \ 's cfg)\. with the restriction @{term "state (cont cfg s) = s"} \ hide_const cont codatatype 's scheduler = Scheduler (action_sch: "'s pmf") (cont_sch: "'s \ 's scheduler") lemma equivp_rel_prod: "equivp R \ equivp Q \ equivp (rel_prod R Q)" by (auto intro!: equivpI prod.rel_symp prod.rel_transp prod.rel_reflp elim: equivpE) coinductive eq_scheduler :: "'s scheduler \ 's scheduler \ bool" where "\D. action_sch sc1 = D \ action_sch sc2 = D \ (\s\D. eq_scheduler (cont_sch sc1 s) (cont_sch sc2 s)) \ eq_scheduler sc1 sc2" lemma eq_scheduler_refl[intro]: "eq_scheduler sc sc" by (coinduction arbitrary: sc) auto quotient_type 's cfg = "'s \ 's scheduler" / "rel_prod (=) eq_scheduler" proof (intro equivp_rel_prod equivpI reflpI sympI transpI) show "eq_scheduler sc1 sc2 \ eq_scheduler sc2 sc1" for sc1 sc2 :: "'s scheduler" by (coinduction arbitrary: sc1 sc2) (auto elim: eq_scheduler.cases) show "eq_scheduler sc1 sc2 \ eq_scheduler sc2 sc3 \ eq_scheduler sc1 sc3" for sc1 sc2 sc3 :: "'s scheduler" by (coinduction arbitrary: sc1 sc2 sc3) (subst (asm) (1 2) eq_scheduler.simps, auto) qed auto lift_definition state :: "'s cfg \ 's" is "fst" by auto lift_definition action :: "'s cfg \ 's pmf" is "\(s, sc). action_sch sc" by (force elim: eq_scheduler.cases) lift_definition cont :: "'s cfg \ 's \ 's cfg" is "\(s, sc) t. if t \ action_sch sc then (t, cont_sch sc t) else (t, cont_sch sc (some_elem (action_sch sc)))" apply (simp add: rel_prod_conv split: prod.splits) apply (subst (asm) eq_scheduler.simps) apply (auto simp: Let_def set_pmf_not_empty[THEN some_elem_ne]) done lift_definition Cfg :: "'s \ 's pmf \ ('s \ 's cfg) \ 's cfg" is "\s D c. (s, Scheduler D (\t. snd (c t)))" by (auto simp: rel_prod_conv split_beta' eq_scheduler.simps[of "Scheduler _ _"]) lift_definition cfg_corec :: "'s \ ('a \ 's pmf) \ ('a \ 's \ 'a) \ 'a \ 's cfg" is "\s D C x. (s, corec_scheduler D (\x s. Inr (C x s)) x)" . lemma state_cont[simp]: "state (cont cfg s) = s" by transfer (simp split: prod.split) lemma state_Cfg[simp]: "state (Cfg s d' c') = s" by transfer simp lemma action_Cfg[simp]: "action (Cfg s d' c') = d'" by transfer simp lemma cont_Cfg[simp]: "t \ set_pmf d' \ state (c' t) = t \ cont (Cfg s d' c') t = c' t" by transfer (auto simp add: rel_prod_conv split: prod.split) lemma state_cfg_corec[simp]: "state (cfg_corec s d c x) = s" by transfer auto lemma action_cfg_corec[simp]: "action (cfg_corec s d c x) = d x" by transfer auto lemma cont_cfg_corec[simp]: "t \ set_pmf (d x) \ cont (cfg_corec s d c x) t = cfg_corec t d c (c x t)" by transfer auto lemma cfg_coinduct[consumes 1, case_names state action cont, coinduct pred]: "X c d \ (\c d. X c d \ state c = state d) \ (\c d. X c d \ action c = action d) \ (\c d t. X c d \ t \ set_pmf (action c) \ X (cont c t) (cont d t)) \ c = d" proof (transfer, clarsimp) fix X :: "('a \ 'a scheduler) \ ('a \ 'a scheduler) \ bool" and B s1 s2 sc1 sc2 assume X: "X (s1, sc1) (s2, sc2)" and "rel_fun cr_cfg (rel_fun cr_cfg (=)) X B" and 1: "\s1 sc1 s2 sc2. X (s1, sc1) (s2, sc2) \ s1 = s2" and 2: "\s1 sc1 s2 sc2. X (s1, sc1) (s2, sc2) \ action_sch sc1 = action_sch sc2" and 3: "\s1 sc1 s2 sc2 t. X (s1, sc1) (s2, sc2) \ t \ set_pmf (action_sch sc2) \ X (t, cont_sch sc1 t) (t, cont_sch sc2 t)" from X show "eq_scheduler sc1 sc2" by (coinduction arbitrary: s1 s2 sc1 sc2) (blast dest: 2 3) qed coinductive rel_cfg :: "('a \ 'b \ bool) \ 'a cfg \ 'b cfg \ bool" for P :: "'a \ 'b \ bool" where "P (state cfg1) (state cfg2) \ rel_pmf (\s t. rel_cfg P (cont cfg1 s) (cont cfg2 t)) (action cfg1) (action cfg2) \ rel_cfg P cfg1 cfg2" lemma rel_cfg_state: "rel_cfg P cfg1 cfg2 \ P (state cfg1) (state cfg2)" by (auto elim: rel_cfg.cases) lemma rel_cfg_cont: "rel_cfg P cfg1 cfg2 \ rel_pmf (\s t. rel_cfg P (cont cfg1 s) (cont cfg2 t)) (action cfg1) (action cfg2)" by (auto elim: rel_cfg.cases) lemma rel_cfg_action: assumes P: "rel_cfg P cfg1 cfg2" shows "rel_pmf P (action cfg1) (action cfg2)" proof (rule pmf.rel_mono_strong) show "rel_pmf (\s t. rel_cfg P (cont cfg1 s) (cont cfg2 t)) (action cfg1) (action cfg2)" using P by (rule rel_cfg_cont) qed (auto dest: rel_cfg_state) lemma rel_cfg_eq: "rel_cfg (=) cfg1 cfg2 \ cfg1 = cfg2" proof safe show "rel_cfg (=) cfg1 cfg2 \ cfg1 = cfg2" proof (coinduction arbitrary: cfg1 cfg2) case cont have "action cfg1 = action cfg2" using \rel_cfg (=) cfg1 cfg2\ by (auto dest: rel_cfg_action simp: pmf.rel_eq) then have "rel_pmf (\s t. rel_cfg (=) (cont cfg1 s) (cont cfg2 t)) (action cfg1) (action cfg1)" using cont by (auto dest: rel_cfg_cont) then have "rel_pmf (\s t. rel_cfg (=) (cont cfg1 s) (cont cfg2 t) \ s = t) (action cfg1) (action cfg1)" by (rule pmf.rel_mono_strong) (auto dest: rel_cfg_state) then have "pred_pmf (\s. rel_cfg (=) (cont cfg1 s) (cont cfg2 s)) (action cfg1)" unfolding pmf.pred_rel by (rule pmf.rel_mono_strong) (auto simp: eq_onp_def) with \t \ action cfg1\ show ?case by (auto simp: pmf.pred_set) qed (auto dest: rel_cfg_state rel_cfg_action simp: pmf.rel_eq) show "rel_cfg (=) cfg2 cfg2" by (coinduction arbitrary: cfg2) (auto intro!: rel_pmf_reflI) qed subsection \Configuration with Memoryless Scheduler\ definition "memoryless_on f s = cfg_corec s f (\_ t. t) s" lemma shows state_memoryless_on[simp]: "state (memoryless_on f s) = s" and action_memoryless_on[simp]: "action (memoryless_on f s) = f s" and cont_memoryless_on[simp]: "t \ (f s) \ cont (memoryless_on f s) t = memoryless_on f t" by (simp_all add: memoryless_on_def) definition K_cfg :: "'s cfg \ 's cfg pmf" where "K_cfg cfg = map_pmf (cont cfg) (action cfg)" lemma set_K_cfg: "set_pmf (K_cfg cfg) = cont cfg ` set_pmf (action cfg)" by (simp add: K_cfg_def) lemma nn_integral_K_cfg: "(\\<^sup>+cfg. f cfg \K_cfg cfg) = (\\<^sup>+s. f (cont cfg s) \action cfg)" by (simp add: K_cfg_def map_pmf_rep_eq nn_integral_distr) subsection \MDP Kernel and Induced Configurations\ locale Markov_Decision_Process = fixes K :: "'s \ 's pmf set" assumes K_wf: "\s. K s \ {}" begin definition "E = (SIGMA s:UNIV. \D\K s. set_pmf D)" coinductive cfg_onp :: "'s \ 's cfg \ bool" where "\s. state cfg = s \ action cfg \ K s \ (\t. t \ action cfg \ cfg_onp t (cont cfg t)) \ cfg_onp s cfg" definition "cfg_on s = {cfg. cfg_onp s cfg}" lemma shows cfg_onD_action[intro, simp]: "cfg \ cfg_on s \ action cfg \ K s" and cfg_onD_cont[intro, simp]: "cfg \ cfg_on s \ t \ action cfg \ cont cfg t \ cfg_on t" and cfg_onD_state[simp]: "cfg \ cfg_on s \ state cfg = s" and cfg_onI: "state cfg = s \ action cfg \ K s \ (\t. t \ action cfg \ cont cfg t \ cfg_on t) \ cfg \ cfg_on s" by (auto simp: cfg_on_def intro: cfg_onp.intros elim: cfg_onp.cases) lemma cfg_on_coinduct[coinduct set: cfg_on]: assumes "P s cfg" assumes "\cfg s. P s cfg \ state cfg = s" assumes "\cfg s. P s cfg \ action cfg \ K s" assumes "\cfg s t. P s cfg \ t \ action cfg \ P t (cont cfg t)" shows "cfg \ cfg_on s" using assms cfg_onp.coinduct[of P s cfg] by (simp add: cfg_on_def) lemma memoryless_on_cfg_onI: assumes "\s. f s \ K s" shows "memoryless_on f s \ cfg_on s" by (coinduction arbitrary: s) (auto intro: assms) lemma cfg_of_cfg_onI: "D \ K s \ (\t. t \ D \ c t \ cfg_on t) \ Cfg s D c \ cfg_on s" by (rule cfg_onI) auto definition "arb_act s = (SOME D. D \ K s)" lemma arb_actI[simp]: "arb_act s \ K s" by (simp add: arb_act_def some_in_eq K_wf) lemma cfg_on_not_empty[intro, simp]: "cfg_on s \ {}" by (auto intro: memoryless_on_cfg_onI arb_actI) sublocale MC: MC_syntax K_cfg . abbreviation St :: "'s stream measure" where "St \ stream_space (count_space UNIV)" subsection \Trace Space\ definition "T cfg = distr (MC.T cfg) St (smap state)" sublocale T: prob_space "T cfg" for cfg by (simp add: T_def MC.T.prob_space_distr) lemma space_T[simp]: "space (T cfg) = space St" by (simp add: T_def) lemma sets_T[simp]: "sets (T cfg) = sets St" by (simp add: T_def) lemma measurable_T1[simp]: "measurable (T cfg) N = measurable St N" by (simp add: T_def) lemma measurable_T2[simp]: "measurable N (T cfg) = measurable N St" by (simp add: T_def) lemma nn_integral_T: assumes [measurable]: "f \ borel_measurable St" shows "(\\<^sup>+X. f X \T cfg) = (\\<^sup>+cfg'. (\\<^sup>+x. f (state cfg' ## x) \T cfg') \K_cfg cfg)" by (simp add: T_def MC.nn_integral_T[of _ cfg] nn_integral_distr) lemma T_eq: "T cfg = (measure_pmf (K_cfg cfg) \ (\cfg'. distr (T cfg') St (\\. state cfg' ## \)))" proof (rule measure_eqI) fix A assume "A \ sets (T cfg)" then show "emeasure (T cfg) A = emeasure (measure_pmf (K_cfg cfg) \ (\cfg'. distr (T cfg') St (\\. state cfg' ## \))) A" by (subst emeasure_bind[where N=St]) (auto simp: space_subprob_algebra nn_integral_distr nn_integral_indicator[symmetric] nn_integral_T[of _ cfg] simp del: nn_integral_indicator intro!: prob_space_imp_subprob_space T.prob_space_distr) qed simp lemma T_memoryless_on: "T (memoryless_on ct s) = MC_syntax.T ct s" proof - interpret ct: MC_syntax ct . have "T \ (memoryless_on ct) = MC_syntax.T ct" proof (rule ct.T_bisim[symmetric]) fix s show "(T \ memoryless_on ct) s = measure_pmf (ct s) \ (\s. distr ((T \ memoryless_on ct) s) St ((##) s))" by (auto simp add: T_eq[of "memoryless_on ct s"] K_cfg_def map_pmf_rep_eq bind_distr[where K=St] space_subprob_algebra T.prob_space_distr prob_space_imp_subprob_space intro!: bind_measure_pmf_cong) qed (simp_all, intro_locales) then show ?thesis by (simp add: fun_eq_iff) qed lemma nn_integral_T_lfp: assumes [measurable]: "case_prod g \ borel_measurable (count_space UNIV \\<^sub>M borel)" assumes cont_g: "\s. sup_continuous (g s)" assumes int_g: "\f cfg. f \ borel_measurable (stream_space (count_space UNIV)) \ (\\<^sup>+\. g (state cfg) (f \) \T cfg) = g (state cfg) (\\<^sup>+\. f \ \T cfg)" shows "(\\<^sup>+\. lfp (\f \. g (shd \) (f (stl \))) \ \T cfg) = lfp (\f cfg. \\<^sup>+t. g (state t) (f t) \K_cfg cfg) cfg" proof (rule nn_integral_lfp) show "\s. sets (T s) = sets St" "\F. F \ borel_measurable St \ (\a. g (shd a) (F (stl a))) \ borel_measurable St" by auto next fix s and F :: "'s stream \ ennreal" assume "F \ borel_measurable St" then show "(\\<^sup>+ a. g (shd a) (F (stl a)) \T s) = (\\<^sup>+ cfg. g (state cfg) (integral\<^sup>N (T cfg) F) \K_cfg s)" by (rewrite nn_integral_T) (simp_all add: int_g) qed (auto intro!: order_continuous_intros cont_g[THEN sup_continuous_compose]) lemma emeasure_Collect_T: assumes [measurable]: "Measurable.pred St P" shows "emeasure (T cfg) {x\space St. P x} = (\\<^sup>+cfg'. emeasure (T cfg') {x\space St. P (state cfg' ## x)} \K_cfg cfg)" using MC.emeasure_Collect_T[of "\x. P (smap state x)" cfg] by (simp add: nn_integral_distr emeasure_Collect_distr T_def) definition E_sup :: "'s \ ('s stream \ ennreal) \ ennreal" where "E_sup s f = (\cfg\cfg_on s. \\<^sup>+x. f x \T cfg)" lemma E_sup_const: "0 \ c \ E_sup s (\_. c) = c" using T.emeasure_space_1 by (simp add: E_sup_def) lemma E_sup_mult_right: assumes [measurable]: "f \ borel_measurable St" and [simp]: "0 \ c" shows "E_sup s (\x. c * f x) = c * E_sup s f" by (simp add: nn_integral_cmult E_sup_def SUP_mult_left_ennreal) lemma E_sup_mono: "(\\. f \ \ g \) \ E_sup s f \ E_sup s g" unfolding E_sup_def by (intro SUP_subset_mono order_refl nn_integral_mono) lemma E_sup_add: assumes [measurable]: "f \ borel_measurable St" "g \ borel_measurable St" shows "E_sup s (\x. f x + g x) \ E_sup s f + E_sup s g" proof - have "E_sup s (\x. f x + g x) = (\cfg\cfg_on s. (\\<^sup>+x. f x \T cfg) + (\\<^sup>+x. g x \T cfg))" by (simp add: E_sup_def nn_integral_add) also have "\ \ (\cfg\cfg_on s. \\<^sup>+x. f x \T cfg) + (\cfg\cfg_on s. (\\<^sup>+x. g x \T cfg))" by (auto simp: SUP_le_iff intro!: add_mono SUP_upper) finally show ?thesis by (simp add: E_sup_def) qed lemma E_sup_add_left: assumes [measurable]: "f \ borel_measurable St" shows "E_sup s (\x. f x + c) = E_sup s f + c" by (simp add: nn_integral_add E_sup_def T.emeasure_space_1[simplified] ennreal_SUP_add_left) lemma E_sup_add_right: "f \ borel_measurable St \ E_sup s (\x. c + f x) = c + E_sup s f" using E_sup_add_left[of f s c] by (simp add: add.commute) lemma E_sup_SUP: assumes [measurable]: "\i. f i \ borel_measurable St" and [simp]: "incseq f" shows "E_sup s (\x. \i. f i x) = (\i. E_sup s (f i))" by (auto simp add: E_sup_def nn_integral_monotone_convergence_SUP intro: SUP_commute) lemma E_sup_iterate: assumes [measurable]: "f \ borel_measurable St" shows "E_sup s f = (\D\K s. \\<^sup>+ t. E_sup t (\\. f (t ## \)) \measure_pmf D)" proof - let ?v = "\t. \\<^sup>+x. f (state t ## x) \T t" let ?p = "\t. E_sup t (\\. f (t ## \))" have "E_sup s f = (\cfg\cfg_on s. \\<^sup>+t. ?v t \K_cfg cfg)" unfolding E_sup_def by (intro SUP_cong refl) (subst nn_integral_T, simp_all add: cfg_on_def) also have "\ = (\D\K s. \\<^sup>+t. ?p t \measure_pmf D)" proof (intro antisym SUP_least) fix cfg :: "'s cfg" assume cfg: "cfg \ cfg_on s" then show "(\\<^sup>+ t. ?v t \K_cfg cfg) \ (SUP D\K s. \\<^sup>+t. ?p t \measure_pmf D)" by (auto simp: E_sup_def nn_integral_K_cfg AE_measure_pmf_iff intro!: nn_integral_mono_AE SUP_upper2) next fix D assume D: "D \ K s" show "(\\<^sup>+t. ?p t \D) \ (SUP cfg \ cfg_on s. \\<^sup>+ t. ?v t \K_cfg cfg)" proof cases assume p_finite: "\t\D. ?p t < \" show ?thesis proof (rule ennreal_le_epsilon) fix e :: real assume "0 < e" have "\t\D. \cfg\cfg_on t. ?p t \ ?v cfg + e" proof fix t assume "t \ D" moreover have "(SUP cfg \ cfg_on t. ?v cfg) = ?p t" unfolding E_sup_def by (simp add: cfg_on_def) ultimately have "(SUP cfg \ cfg_on t. ?v cfg) \ \" using p_finite by auto from SUP_approx_ennreal[OF \0 _ refl this] show "\cfg\cfg_on t. ?p t \ ?v cfg + e" by (auto simp add: E_sup_def intro: less_imp_le) qed then obtain cfg' where v_cfg': "\t. t \ D \ ?p t \ ?v (cfg' t) + e" and cfg_on_cfg': "\t. t \ D \ cfg' t \ cfg_on t" unfolding Bex_def bchoice_iff by blast let ?cfg = "Cfg s D cfg'" have cfg: "K_cfg ?cfg = map_pmf cfg' D" by (auto simp add: K_cfg_def fun_eq_iff cfg_on_cfg' intro!: map_pmf_cong) have "(\\<^sup>+ t. ?p t \D) \ (\\<^sup>+t. ?v (cfg' t) + e \D)" by (intro nn_integral_mono_AE) (simp add: v_cfg' AE_measure_pmf_iff) also have "\ = (\\<^sup>+t. ?v (cfg' t) \D) + e" using \0 < e\ measure_pmf.emeasure_space_1[of D] by (subst nn_integral_add) (auto intro: cfg_on_cfg' ) also have "(\\<^sup>+t. ?v (cfg' t) \D) = (\\<^sup>+t. ?v t \K_cfg ?cfg)" by (simp add: cfg map_pmf_rep_eq nn_integral_distr) also have "\ \ (SUP cfg\cfg_on s. (\\<^sup>+t. ?v t \K_cfg cfg))" by (auto intro!: SUP_upper intro!: cfg_of_cfg_onI D cfg_on_cfg') finally show "(\\<^sup>+ t. ?p t \D) \ (SUP cfg \ cfg_on s. \\<^sup>+ t. ?v t \K_cfg cfg) + e" by (blast intro: add_mono) qed next assume "\ (\t\D. ?p t < \)" then obtain t where "t \ D" "?p t = \" by (auto simp: not_less top_unique) then have "\ = pmf (D) t * ?p t" by (auto simp: ennreal_mult_top set_pmf_iff) also have "\ = (SUP cfg \ cfg_on t. pmf (D) t * ?v cfg)" unfolding E_sup_def by (auto simp: SUP_mult_left_ennreal[symmetric]) also have "\ \ (SUP cfg \ cfg_on s. \\<^sup>+ t. ?v t \K_cfg cfg)" unfolding E_sup_def proof (intro SUP_least SUP_upper2) fix cfg :: "'s cfg" assume cfg: "cfg \ cfg_on t" let ?cfg = "Cfg s D ((memoryless_on arb_act) (t := cfg))" have C: "K_cfg ?cfg = map_pmf ((memoryless_on arb_act) (t := cfg)) D" by (auto simp add: K_cfg_def fun_eq_iff intro!: map_pmf_cong simp: cfg) show "?cfg \ cfg_on s" by (auto intro!: cfg_of_cfg_onI D cfg memoryless_on_cfg_onI) have "ennreal (pmf (D) t) * (\\<^sup>+ x. f (state cfg ## x) \T cfg) = (\\<^sup>+t'. (\\<^sup>+ x. f (state cfg ## x) \T cfg) * indicator {t} t' \D)" by (auto simp add: max_def emeasure_pmf_single intro: mult_ac) also have "\ = (\\<^sup>+cfg. ?v cfg * indicator {t} (state cfg) \K_cfg ?cfg)" unfolding C using cfg by (auto simp add: nn_integral_distr map_pmf_rep_eq split: split_indicator simp del: nn_integral_indicator_singleton intro!: nn_integral_cong) also have "\ \ (\\<^sup>+cfg. ?v cfg \K_cfg ?cfg)" by (auto intro!: nn_integral_mono split: split_indicator) finally show "ennreal (pmf (D) t) * (\\<^sup>+ x. f (state cfg ## x) \T cfg) \ (\\<^sup>+ t. \\<^sup>+ x. f (state t ## x) \T t \K_cfg ?cfg)" . qed finally show ?thesis by (simp add: top_unique del: Sup_eq_top_iff SUP_eq_top_iff) qed qed finally show ?thesis . qed lemma E_sup_bot: "E_sup s \ = 0" by (auto simp add: E_sup_def bot_ennreal) lemma E_sup_lfp: fixes g defines "l \ \f \. g (shd \) (f (stl \))" assumes measurable_g[measurable]: "case_prod g \ borel_measurable (count_space UNIV \\<^sub>M borel)" assumes cont_g: "\s. sup_continuous (g s)" assumes int_g: "\f cfg. f \ borel_measurable St \ (\\<^sup>+ \. g (state cfg) (f \) \T cfg) = g (state cfg) (integral\<^sup>N (T cfg) f)" shows "(\s. E_sup s (lfp l)) = lfp (\f s. \D\K s. \\<^sup>+t. g t (f t) \measure_pmf D)" proof (rule lfp_transfer_bounded[where \="\F s. E_sup s F" and f=l and P="\f. f \ borel_measurable St"]) show "sup_continuous (\f s. \x\K s. \\<^sup>+ t. g t (f t) \measure_pmf x)" using cont_g[THEN sup_continuous_compose] by (auto intro!: order_continuous_intros) show "sup_continuous l" using cont_g[THEN sup_continuous_compose] by (auto intro!: order_continuous_intros simp: l_def) show "\F. (\s. E_sup s \) \ (\s. \D\K s. \\<^sup>+ t. g t (F t) \measure_pmf D)" using K_wf by (auto simp: E_sup_bot le_fun_def intro: SUP_upper2 ) next fix f :: "'s stream \ ennreal" assume f: "f \ borel_measurable St" moreover have "E_sup s (\\. g s (f \)) = g s (E_sup s f)" for s unfolding E_sup_def using int_g[OF f] by (subst SUP_sup_continuous_ennreal[OF cont_g, symmetric]) (auto intro!: SUP_cong simp del: cfg_onD_state dest: cfg_onD_state[symmetric]) ultimately show "(\s. E_sup s (l f)) = (\s. \D\K s. \\<^sup>+ t. g t (E_sup t f) \measure_pmf D)" by (subst E_sup_iterate) (auto simp: l_def int_g fun_eq_iff intro!: SUP_cong nn_integral_cong) qed (auto simp: bot_fun_def l_def SUP_apply[abs_def] E_sup_SUP) definition "P_sup s P = (\cfg\cfg_on s. emeasure (T cfg) {x\space St. P x})" lemma P_sup_eq_E_sup: assumes [measurable]: "Measurable.pred St P" shows "P_sup s P = E_sup s (indicator {x\space St. P x})" by (auto simp add: P_sup_def E_sup_def intro!: SUP_cong nn_integral_cong) lemma P_sup_True[simp]: "P_sup t (\\. True) = 1" using T.emeasure_space_1 by (auto simp add: P_sup_def SUP_constant) lemma P_sup_False[simp]: "P_sup t (\\. False) = 0" by (auto simp add: P_sup_def SUP_constant) lemma P_sup_SUP: fixes P :: "nat \ 's stream \ bool" assumes "mono P" and P[measurable]: "\i. Measurable.pred St (P i)" shows "P_sup s (\x. \i. P i x) = (\i. P_sup s (P i))" proof - have "P_sup s (\x. \i. P i x) = (\cfg\cfg_on s. emeasure (T cfg) (\i. {x\space St. P i x}))" by (auto simp: P_sup_def intro!: SUP_cong arg_cong2[where f=emeasure]) also have "\ = (\cfg\cfg_on s. \i. emeasure (T cfg) {x\space St. P i x})" using \mono P\ by (auto intro!: SUP_cong SUP_emeasure_incseq[symmetric] simp: mono_def le_fun_def) also have "\ = (\i. P_sup s (P i))" by (subst SUP_commute) (simp add: P_sup_def) finally show ?thesis by simp qed lemma P_sup_lfp: assumes Q: "sup_continuous Q" assumes f: "f \ measurable St M" assumes Q_m: "\P. Measurable.pred M P \ Measurable.pred M (Q P)" shows "P_sup s (\x. lfp Q (f x)) = (\i. P_sup s (\x. (Q ^^ i) \ (f x)))" unfolding sup_continuous_lfp[OF Q] apply simp proof (rule P_sup_SUP) fix i show "Measurable.pred St (\x. (Q ^^ i) \ (f x))" apply (intro measurable_compose[OF f]) by (induct i) (auto intro!: Q_m) qed (intro mono_funpow sup_continuous_mono[OF Q] mono_compose[where f=f]) lemma P_sup_iterate: assumes [measurable]: "Measurable.pred St P" shows "P_sup s P = (\D\K s. \\<^sup>+ t. P_sup t (\\. P (t ## \)) \measure_pmf D)" proof - have [simp]: "\x s. indicator {x \ space St. P x} (x ## s) = indicator {s \ space St. P (x ## s)} s" by (auto simp: space_stream_space split: split_indicator) show ?thesis using E_sup_iterate[of "indicator {x\space St. P x}" s] by (auto simp: P_sup_eq_E_sup) qed definition "E_inf s f = (\cfg\cfg_on s. \\<^sup>+x. f x \T cfg)" lemma E_inf_const: "0 \ c \ E_inf s (\_. c) = c" using T.emeasure_space_1 by (simp add: E_inf_def) lemma E_inf_mono: "(\\. f \ \ g \) \ E_inf s f \ E_inf s g" unfolding E_inf_def by (intro INF_superset_mono order_refl nn_integral_mono) lemma E_inf_iterate: assumes [measurable]: "f \ borel_measurable St" shows "E_inf s f = (\D\K s. \\<^sup>+ t. E_inf t (\\. f (t ## \)) \measure_pmf D)" proof - let ?v = "\t. \\<^sup>+x. f (state t ## x) \T t" let ?p = "\t. E_inf t (\\. f (t ## \))" have "E_inf s f = (\cfg\cfg_on s. \\<^sup>+t. ?v t \K_cfg cfg)" unfolding E_inf_def by (intro INF_cong refl) (subst nn_integral_T, simp_all add: cfg_on_def) also have "\ = (\D\K s. \\<^sup>+t. ?p t \measure_pmf D)" proof (intro antisym INF_greatest) fix cfg :: "'s cfg" assume cfg: "cfg \ cfg_on s" then show "(INF D\K s. \\<^sup>+t. ?p t \measure_pmf D) \ (\\<^sup>+ t. ?v t \K_cfg cfg)" by (auto simp add: E_inf_def nn_integral_K_cfg AE_measure_pmf_iff intro!: nn_integral_mono_AE INF_lower2) next fix D assume D: "D \ K s" show "(INF cfg \ cfg_on s. \\<^sup>+ t. ?v t \K_cfg cfg) \ (\\<^sup>+t. ?p t \D)" proof (rule ennreal_le_epsilon) fix e :: real assume "0 < e" have "\t\D. \cfg\cfg_on t. ?v cfg \ ?p t + e" proof fix t assume "t \ D" show "\cfg\cfg_on t. ?v cfg \ ?p t + e" proof cases assume "?p t = \" with cfg_on_not_empty[of t] show ?thesis by (auto simp: top_add simp del: cfg_on_not_empty) next assume p_finite: "?p t \ \" note \t \ D\ moreover have "(INF cfg \ cfg_on t. ?v cfg) = ?p t" unfolding E_inf_def by (simp add: cfg_on_def) ultimately have "(INF cfg \ cfg_on t. ?v cfg) \ \" using p_finite by auto from INF_approx_ennreal[OF \0 < e\ refl this] show "\cfg\cfg_on t. ?v cfg \ ?p t + e" by (auto simp: E_inf_def intro: less_imp_le) qed qed then obtain cfg' where v_cfg': "\t. t \ D \ ?v (cfg' t) \ ?p t + e" and cfg_on_cfg': "\t. t \ D \ cfg' t \ cfg_on t" unfolding Bex_def bchoice_iff by blast let ?cfg = "Cfg s D cfg'" have cfg: "K_cfg ?cfg = map_pmf cfg' D" by (auto simp add: K_cfg_def cfg_on_cfg' intro!: map_pmf_cong) have "?cfg \ cfg_on s" by (auto intro: D cfg_on_cfg' cfg_of_cfg_onI) then have "(INF cfg \ cfg_on s. \\<^sup>+ t. ?v t \K_cfg cfg) \ (\\<^sup>+ t. ?p t + e \D)" by (rule INF_lower2) (auto simp: cfg map_pmf_rep_eq nn_integral_distr v_cfg' AE_measure_pmf_iff intro!: nn_integral_mono_AE) also have "\ = (\\<^sup>+ t. ?p t \D) + e" using \0 < e\ by (simp add: nn_integral_add measure_pmf.emeasure_space_1[simplified]) finally show "(INF cfg \ cfg_on s. \\<^sup>+ t. ?v t \K_cfg cfg) \ (\\<^sup>+ t. ?p t \D) + e" . qed qed finally show ?thesis . qed lemma emeasure_T_const[simp]: "emeasure (T s) (space St) = 1" using T.emeasure_space_1[of s] by simp lemma E_inf_greatest: "(\cfg. cfg \ cfg_on s \ x \ (\\<^sup>+x. f x \T cfg)) \ x \ E_inf s f" unfolding E_inf_def by (rule INF_greatest) lemma E_inf_lower2: "cfg \ cfg_on s \ (\\<^sup>+x. f x \T cfg) \ x \ E_inf s f \ x" unfolding E_inf_def by (rule INF_lower2) text \ Maybe the following statement can be generalized to infinite @{term "K s"}. \ lemma E_inf_lfp: fixes g defines "l \ \f \. g (shd \) (f (stl \))" assumes measurable_g[measurable]: "case_prod g \ borel_measurable (count_space UNIV \\<^sub>M borel)" assumes cont_g: "\s. sup_continuous (g s)" assumes int_g: "\f cfg. f \ borel_measurable St \ (\\<^sup>+ \. g (state cfg) (f \) \T cfg) = g (state cfg) (integral\<^sup>N (T cfg) f)" assumes K_finite: "\s. finite (K s)" shows "(\s. E_inf s (lfp l)) = lfp (\f s. \D\K s. \\<^sup>+t. g t (f t) \measure_pmf D)" proof (rule antisym) let ?F = "\F s. \D\K s. \\<^sup>+ t. g t (F t) \measure_pmf D" let ?I = "\D. (\\<^sup>+t. g t (lfp ?F t) \measure_pmf D)" have mono_F: "mono ?F" using sup_continuous_mono[OF cont_g] by (force intro!: INF_mono nn_integral_mono monoI simp: mono_def le_fun_def) define ct where "ct s = (SOME D. D \ K s \ (lfp ?F s = ?I D))" for s { fix s have "finite (?I ` K s)" by (auto intro: K_finite) then obtain D where "D \ K s" "?I D = Min (?I ` K s)" by (auto simp: K_wf dest!: Min_in) note this(2) also have "\ = (INF D \ K s. ?I D)" using K_wf by (subst Min_Inf) (auto intro: K_finite) also have "\ = lfp ?F s" by (rewrite in "_ = \" lfp_unfold[OF mono_F]) auto finally have "\D. D \ K s \ (lfp ?F s = ?I D)" using \D \ K s\ by auto then have "ct s \ K s \ (lfp ?F s = ?I (ct s))" unfolding ct_def by (rule someI_ex) then have "ct s \ K s" "lfp ?F s = ?I (ct s)" by auto } note ct = this then have ct_cfg_on[simp]: "\s. memoryless_on ct s \ cfg_on s" by (intro memoryless_on_cfg_onI) simp then show "(\s. E_inf s (lfp l)) \ lfp ?F" proof (intro le_funI, rule E_inf_lower2) fix s define P where "P f cfg = \\<^sup>+ t. g (state t) (f t) \K_cfg cfg" for f cfg have "integral\<^sup>N (T (memoryless_on ct s)) (lfp l) = lfp P (memoryless_on ct s)" unfolding P_def l_def using measurable_g cont_g int_g by (rule nn_integral_T_lfp) also have "\ = (SUP i. (P ^^ i) \) (memoryless_on ct s)" by (rewrite sup_continuous_lfp) (auto intro!: order_continuous_intros cont_g[THEN sup_continuous_compose] simp: P_def) also have "\ = (SUP i. (P ^^ i) \ (memoryless_on ct s))" by (simp add: image_comp) also have "\ \ lfp ?F s" proof (rule SUP_least) fix i show "(P ^^ i) \ (memoryless_on ct s) \ lfp ?F s" proof (induction i arbitrary: s) case 0 then show ?case by simp next case (Suc n) have "(P ^^ Suc n) \ (memoryless_on ct s) = (\\<^sup>+ t. g t ((P ^^ n) \ (memoryless_on ct t)) \ct s)" by (auto simp add: P_def K_cfg_def AE_measure_pmf_iff intro!: nn_integral_cong_AE) also have "\ \ (\\<^sup>+ t. g t (lfp ?F t) \ct s)" by (intro nn_integral_mono sup_continuous_mono[OF cont_g, THEN monoD] Suc) also have "\ = lfp ?F s" by (rule ct(2) [symmetric]) finally show ?case . qed qed finally show "integral\<^sup>N (T (memoryless_on ct s)) (lfp l) \ lfp ?F s" . qed have cont_l: "sup_continuous l" by (auto simp: l_def intro!: order_continuous_intros cont_g[THEN sup_continuous_compose]) show "lfp ?F \ (\s. E_inf s (lfp l))" proof (intro lfp_lowerbound le_funI) fix s show "(\x\K s. \\<^sup>+ t. g t (E_inf t (lfp l)) \measure_pmf x) \ E_inf s (lfp l)" proof (rewrite in "_ \ \" E_inf_iterate) show l: "lfp l \ borel_measurable St" using cont_l by (rule borel_measurable_lfp) (simp add: l_def) show "(\D\K s. \\<^sup>+ t. g t (E_inf t (lfp l)) \measure_pmf D) \ (\D\K s. \\<^sup>+ t. E_inf t (\\. lfp l (t ## \)) \measure_pmf D)" proof (rule INF_mono nn_integral_mono bexI)+ fix t D assume "D \ K s" { fix cfg assume "cfg \ cfg_on t" have "(\\<^sup>+ \. g (state cfg) (lfp l \) \T cfg) = g (state cfg) (\\<^sup>+ \. (lfp l \) \T cfg)" using l by (rule int_g) with \cfg \ cfg_on t\ have *: "(\\<^sup>+ \. g t (lfp l \) \T cfg) = g t (\\<^sup>+ \. (lfp l \) \T cfg)" by simp } then have *: "g t (\cfg\cfg_on t. integral\<^sup>N (T cfg) (lfp l)) \ (\cfg\cfg_on t. \\<^sup>+ \. g t (lfp l \) \T cfg)" apply simp apply (rule INF_greatest) apply (rule sup_continuous_mono[OF cont_g, THEN monoD]) apply (rule INF_lower) apply assumption done show "g t (E_inf t (lfp l)) \ E_inf t (\\. lfp l (t ## \))" apply (rewrite in "_ \ \" lfp_unfold[OF sup_continuous_mono[OF cont_l]]) apply (rewrite in "_ \ \" l_def) apply (simp add: E_inf_def *) done qed qed qed qed definition "P_inf s P = (\cfg\cfg_on s. emeasure (T cfg) {x\space St. P x})" lemma P_inf_eq_E_inf: assumes [measurable]: "Measurable.pred St P" shows "P_inf s P = E_inf s (indicator {x\space St. P x})" by (auto simp add: P_inf_def E_inf_def intro!: SUP_cong nn_integral_cong) lemma P_inf_True[simp]: "P_inf t (\\. True) = 1" using T.emeasure_space_1 by (auto simp add: P_inf_def SUP_constant) lemma P_inf_False[simp]: "P_inf t (\\. False) = 0" by (auto simp add: P_inf_def SUP_constant) lemma P_inf_INF: fixes P :: "nat \ 's stream \ bool" assumes "decseq P" and P[measurable]: "\i. Measurable.pred St (P i)" shows "P_inf s (\x. \i. P i x) = (\i. P_inf s (P i))" proof - have "P_inf s (\x. \i. P i x) = (\cfg\cfg_on s. emeasure (T cfg) (\i. {x\space St. P i x}))" by (auto simp: P_inf_def intro!: INF_cong arg_cong2[where f=emeasure]) also have "\ = (\cfg\cfg_on s. \i. emeasure (T cfg) {x\space St. P i x})" - using \decseq P\ by (auto intro!: INF_cong INF_emeasure_decseq[symmetric] simp: decseq_def le_fun_def) + using \decseq P\ + by (auto intro!: INF_cong INF_emeasure_decseq[symmetric] + simp: decseq_def monotone_def le_fun_def) also have "\ = (\i. P_inf s (P i))" by (subst INF_commute) (simp add: P_inf_def) finally show ?thesis by simp qed lemma P_inf_gfp: assumes Q: "inf_continuous Q" assumes f: "f \ measurable St M" assumes Q_m: "\P. Measurable.pred M P \ Measurable.pred M (Q P)" shows "P_inf s (\x. gfp Q (f x)) = (\i. P_inf s (\x. (Q ^^ i) \ (f x)))" unfolding inf_continuous_gfp[OF Q] apply simp proof (rule P_inf_INF) fix i show "Measurable.pred St (\x. (Q ^^ i) \ (f x))" apply (intro measurable_compose[OF f]) by (induct i) (auto intro!: Q_m) next show "decseq (\i x. (Q ^^ i) \ (f x))" using inf_continuous_mono[OF Q, THEN funpow_increasing[rotated]] - unfolding decseq_def le_fun_def by auto + unfolding decseq_def monotone_def le_fun_def by auto qed lemma P_inf_iterate: assumes [measurable]: "Measurable.pred St P" shows "P_inf s P = (\D\K s. \\<^sup>+ t. P_inf t (\\. P (t ## \)) \measure_pmf D)" proof - have [simp]: "\x s. indicator {x \ space St. P x} (x ## s) = indicator {s \ space St. P (x ## s)} s" by (auto simp: space_stream_space split: split_indicator) show ?thesis using E_inf_iterate[of "indicator {x\space St. P x}" s] by (auto simp: P_inf_eq_E_inf) qed end subsection \Finite MDPs\ locale Finite_Markov_Decision_Process = Markov_Decision_Process K for K :: "'s \ 's pmf set" + fixes S :: "'s set" assumes S_not_empty: "S \ {}" assumes S_finite: "finite S" assumes K_closed: "\s. s \ S \ (\D\K s. set_pmf D) \ S" assumes K_finite: "\s. s \ S \ finite (K s)" begin lemma action_closed: "s \ S \ cfg \ cfg_on s \ t \ action cfg \ t \ S" using cfg_onD_action[of cfg s] K_closed[of s] by auto lemma set_pmf_closed: "s \ S \ D \ K s \ t \ D \ t \ S" using K_closed by auto lemma Pi_closed: "ct \ Pi S K \ s \ S \ t \ ct s \ t \ S" using set_pmf_closed by auto lemma E_closed: "s \ S \ (s, t) \ E \ t \ S" using K_closed by (auto simp: E_def) lemma set_pmf_finite: "s \ S \ D \ K s \ finite D" using K_closed by (intro finite_subset[OF _ S_finite]) auto definition "valid_cfg = (\s\S. cfg_on s)" lemma valid_cfgI: "s \ S \ cfg \ cfg_on s \ cfg \ valid_cfg" by (auto simp: valid_cfg_def) lemma valid_cfgD: "cfg \ valid_cfg \ cfg \ cfg_on (state cfg)" by (auto simp: valid_cfg_def) lemma shows valid_cfg_state_in_S: "cfg \ valid_cfg \ state cfg \ S" and valid_cfg_action: "cfg \ valid_cfg \ s \ action cfg \ s \ S" and valid_cfg_cont: "cfg \ valid_cfg \ s \ action cfg \ cont cfg s \ valid_cfg" by (auto simp: valid_cfg_def intro!: bexI[of _ s] intro: action_closed) lemma valid_K_cfg[intro]: "cfg \ valid_cfg \ cfg' \ K_cfg cfg \ cfg' \ valid_cfg" by (auto simp add: K_cfg_def valid_cfg_cont) definition "simple ct = memoryless_on (\s. if s \ S then ct s else arb_act s)" lemma simple_cfg_on[simp]: "ct \ Pi S K \ simple ct s \ cfg_on s" by (auto simp: simple_def intro!: memoryless_on_cfg_onI) lemma simple_valid_cfg[simp]: "ct \ Pi S K \ s \ S \ simple ct s \ valid_cfg" by (auto intro: valid_cfgI) lemma cont_simple[simp]: "s \ S \ t \ set_pmf (ct s) \ cont (simple ct s) t = simple ct t" by (simp add: simple_def) lemma state_simple[simp]: "state (simple ct s) = s" by (simp add: simple_def) lemma action_simple[simp]: "s \ S \ action (simple ct s) = ct s" by (simp add: simple_def) lemma simple_valid_cfg_iff: "ct \ Pi S K \ simple ct s \ valid_cfg \ s \ S" using cfg_onD_state[of "simple ct s"] by (auto simp add: valid_cfg_def intro!: bexI[of _ s]) end end diff --git a/thys/Stable_Matching/Contracts.thy b/thys/Stable_Matching/Contracts.thy --- a/thys/Stable_Matching/Contracts.thy +++ b/thys/Stable_Matching/Contracts.thy @@ -1,2682 +1,2683 @@ (*<*) theory Contracts imports Choice_Functions "HOL-Library.Dual_Ordered_Lattice" "HOL-Library.Bourbaki_Witt_Fixpoint" "HOL-Library.While_Combinator" "HOL-Library.Product_Order" begin (*>*) section\ \citet{HatfieldMilgrom:2005}: Matching with contracts \label{sec:contracts} \ text\ We take the original paper on matching with contracts by \citet{HatfieldMilgrom:2005} as our roadmap, which follows a similar path to \citet[\S2.5]{RothSotomayor:1990}. We defer further motivation to these texts. Our first move is to capture the scenarios described in their {\S}I(A) (p916) in a locale. \ locale Contracts = fixes Xd :: "'x::finite \ 'd::finite" fixes Xh :: "'x \ 'h::finite" fixes Pd :: "'d \ 'x rel" fixes Ch :: "'h \ 'x cfun" assumes Pd_linear: "\d. Linear_order (Pd d)" assumes Pd_range: "\d. Field (Pd d) \ {x. Xd x = d}" assumes Ch_range: "\h. \X. Ch h X \ {x\X. Xh x = h}" assumes Ch_singular: "\h. \X. inj_on Xd (Ch h X)" begin text \ The set of contracts is modelled by the type @{typ "'x"}, a free type variable that will later be interpreted by some non-empty set. Similarly @{typ "'d"} and @{typ "'h"} track the names of doctors and hospitals respectively. All of these are finite by virtue of belonging to the \finite\ type class. We fix four constants: \begin{itemize} \item \Xd\ (\Xh\) projects the name of the relevant doctor (hospital) from a contract; \item \Pd\ maps doctors to their linear preferences over some subset of contracts that name them (assumptions @{thm [source] Pd_linear} and @{thm [source] Pd_range}); and \item \Ch\ maps hospitals to their choice functions (\S\ref{sec:cf}), which are similarly constrained to contracts that name them (assumption @{thm [source] Ch_range}). Moreover their choices must name each doctor at most once, i.e., \Xd\ must be injective on these (assumption @{thm [source] "Ch_singular"}). \end{itemize} The reader familiar with the literature will note that we do not have a null contract (also said to represent the @{emph \outside option\} of unemployment), and instead use partiality of the doctors' preferences. This provides two benefits: firstly, \Xh\ is a total function here, and secondly we achieve some economy of description when instantiating this locale as \Pd\ only has to rank the relevant contracts. We note in passing that neither the doctors' nor hospitals' choice functions are required to be decisive, unlike the standard literature on choice functions (\S\ref{sec:cf}). In addition to the above, the following constitute the definitions that must be trusted for the results we prove to be meaningful. \ definition Cd :: "'d \ 'x cfun" where "Cd d \ set_option \ MaxR.MaxR_opt (Pd d)" definition CD_on :: "'d set \ 'x cfun" where "CD_on ds X = (\d\ds. Cd d X)" abbreviation CD :: "'x set \ 'x set" where "CD \ CD_on UNIV" definition CH :: "'x cfun" where "CH X = (\h. Ch h X)" text\ The function @{const "Cd"} constructs a choice function from the doctor's linear preferences (see \S\ref{sec:cf-linear}). Both @{const "CD"} and @{const "CH"} simply aggregate opinions in the obvious way. The functions @{const "CD_on"} is parameterized with a set of doctors to support the proofs of \S\ref{sec:contracts-vacancy-chain}. We also define \RD\ (\Rh\, \RH\) to be the subsets of a given set of contracts that are rejected by the doctors (hospitals). (The abbreviation @{const "Rf"} is defined in \S\ref{sec:cf-rf}.) \ abbreviation (input) RD_on :: "'d set \ 'x cfun" where "RD_on ds \ Rf (CD_on ds)" abbreviation (input) RD :: "'x cfun" where "RD \ RD_on UNIV" abbreviation (input) Rh :: "'h \ 'x cfun" where "Rh h \ Rf (Ch h)" abbreviation (input) RH :: "'x cfun" where "RH \ Rf CH" text \ A @{emph \mechanism\} maps doctor and hospital preferences into a match (here a set of contracts). \ type_synonym (in -) ('d, 'h, 'x) mechanism = "('d \ 'x rel) \ ('h \ 'x cfun) \ 'd set \ 'x set" (*<*) (* Pd *) lemmas Pd_linear' = Pd_linear[rule_format] lemmas Pd_range' = subsetD[OF Pd_range[rule_format], simplified, of x d] for x d lemma Pd_refl: assumes "x \ Field (Pd d)" shows "(x, x) \ Pd d" using assms Pd_linear' by (meson subset_refl underS_incl_iff) lemma Pd_Xd: assumes "(x, y) \ Pd d" shows "Xd x = d \ Xd y = d" using assms Pd_range contra_subsetD unfolding Field_def by blast lemma Above_Pd_Xd: assumes "x \ Above (Pd d) X" shows "Xd x = d" using assms by (blast dest: Above_Field Pd_range') lemma AboveS_Pd_Xd: assumes "x \ AboveS (Pd d) X" shows "Xd x = d" using assms by (blast dest: AboveS_Field Pd_range') (* Cd *) interpretation Cd: linear_cf "Pd d" "Cd d" for d using Cd_def Pd_linear by unfold_locales simp_all lemmas Cd_domain = Cd.domain lemmas Cd_f_range = Cd.f_range lemmas Cd_range = Cd.range lemmas Cd_range' = Cd.range' lemmas Rf_Cd_mono = Cd.Rf_mono_on[of UNIV, unfolded mono_on_mono] lemmas Cd_Chernoff = Cd.Chernoff lemmas Cd_path_independent = Cd.path_independent lemmas Cd_iia = Cd.iia lemmas Cd_irc = Cd.irc lemmas Cd_lad = Cd.lad lemmas Cd_mono = Cd.mono lemmas Cd_greatest = Cd.greatest lemmas Cd_preferred = Cd.preferred lemmas Cd_singleton = Cd.singleton lemmas Cd_union = Cd.union lemmas Cd_idem = iia_f_idem[OF Cd.f_range[of UNIV d, folded Cd_def] Cd_iia[of UNIV], simplified] for d lemma Cd_Xd: shows "x \ Cd d X \ Xd x = d" using Pd_range Cd_range by fastforce lemma Cd_inj_on_Xd: shows "inj_on Xd (Cd d X)" by (rule inj_onI) (clarsimp simp: Cd_Xd Cd_singleton) lemma Cd_range_disjoint: assumes "d \ d'" shows "Cd d A \ Cd d' A = {}" using assms Cd_range Pd_range by blast lemma Cd_single: assumes "x \ X" assumes "inj_on Xd X" assumes "x \ Field (Pd d)" shows "x \ Cd d X" using assms Pd_linear unfolding Cd_greatest greatest_def by clarsimp (metis Pd_Xd inj_on_eq_iff subset_refl underS_incl_iff) lemma Cd_Above: shows "Cd d X = Above (Pd d) (X \ Field (Pd d)) \ X" unfolding Cd_greatest greatest_Above Above_def by blast (* Code generator setup. Repeats a lot of stuff. *) definition maxR :: "'d \ 'x \ 'x \ 'x" where "maxR d x y = (if (x, y) \ Pd d then y else x)" definition MaxR_f :: "'d \ 'x \ 'x option \ 'x option" where "MaxR_f d = (\x acc. if x \ Field (Pd d) then Some (case acc of None \ x | Some y \ maxR d x y) else acc)" lemma MaxR_maxR: shows "MaxR.maxR (Pd d) = maxR d" by (simp add: fun_eq_iff maxR_def Cd.maxR_code) lemma MaxR_MaxR_f: shows "MaxR.MaxR_f (Pd d) = MaxR_f d" by (simp add: fun_eq_iff Cd.MaxR_f_code MaxR_f_def MaxR_maxR cong: option.case_cong) lemmas Cd_code[code] = Cd.code[unfolded MaxR_MaxR_f] lemma Cd_simps[simp, nitpick_simp]: shows "Cd d {} = {}" "Cd d (insert x A) = (if x \ Field (Pd d) then if Cd d A = {} then {x} else {maxR d x y |y. y \ Cd d A} else Cd d A)" unfolding Cd.simps MaxR_maxR by simp_all (* CD *) lemma CD_on_def2: shows "CD_on ds A = (\d\ds. Cd d (A \ Field (Pd d)))" using Cd_domain unfolding CD_on_def by blast lemma CD_on_Xd: assumes "x \ CD_on ds A" shows "Xd x \ ds" using assms Cd_Xd unfolding CD_on_def by blast lemma mem_CD_on_Cd: shows "x \ CD_on ds X \ (x \ Cd (Xd x) X \ Xd x \ ds)" unfolding CD_on_def using Cd_range Cd_Xd by blast lemma CD_on_domain: assumes "d \ ds" shows "CD_on ds A \ Field (Pd d) = Cd d (A \ Field (Pd d))" unfolding CD_on_def2 using assms Cd_range by (force dest: Pd_range') lemma CD_on_range: shows "CD_on ds A \ A \ (\d\ds. Field (Pd d))" using Cd_range unfolding CD_on_def by blast lemmas CD_on_range' = subsetD[OF CD_on_range] lemma CD_on_f_range_on: shows "f_range_on A (CD_on ds)" by (rule f_range_onI) (meson CD_on_range Int_subset_iff) lemma RD_on_mono: shows "mono (RD_on ds)" unfolding CD_on_def by (rule monoI) (auto dest: monoD[OF Rf_Cd_mono]) lemma CD_on_Chernoff: shows "Chernoff (CD_on ds)" using mono_on_mono RD_on_mono[of ds] Rf_mono_on_iia_on[of UNIV] Chernoff_on_iia_on by (simp add: fun_eq_iff) blast lemma CD_on_irc: shows "irc (CD_on ds)" by (rule ircI) (fastforce simp: CD_on_def ircD[OF Cd_irc] simp del: Cd_simps cong: SUP_cong) lemmas CD_on_consistency = irc_on_consistency_on[OF CD_on_irc, simplified] lemma CD_on_path_independent: shows "path_independent (\X. CD_on ds X)" using CD_on_f_range_on CD_on_Chernoff CD_on_consistency by (blast intro: path_independent_onI2) lemma CD_on_simps: shows "CD_on ds {} = {}" using CD_on_range by blast lemmas CD_on_iia = RD_on_mono[unfolded Rf_mono_iia] lemmas CD_on_idem = iia_f_idem[OF CD_on_f_range_on CD_on_iia, simplified] lemma CD_on_inj_on_Xd: shows "inj_on Xd (CD_on ds X)" unfolding CD_on_def by (rule inj_onI) (clarsimp simp: Cd_Xd Cd_singleton) lemma CD_on_card: shows "card (CD_on ds X) = (\d\ds. card (Cd d X))" unfolding CD_on_def by (simp add: card_UN_disjoint Cd_range_disjoint) lemma CD_on_closed: assumes "inj_on Xd X" assumes "X \ (\d\ds. Field (Pd d))" shows "CD_on ds X = X" using assms Cd_domain Cd_single[OF _ assms(1)] unfolding CD_on_def2 by (force dest: Cd_range') (* Ch *) lemmas Ch_singular' = Ch_singular[rule_format] lemmas Ch_range' = subsetD[OF Ch_range[rule_format], simplified, of x h X] for x h X lemma Ch_simps: shows "Ch h {} = {}" using Ch_range by blast lemma Ch_range_disjoint: assumes "h \ h'" shows "Ch h A \ Ch h' A = {}" using assms Ch_range by blast lemma Ch_f_range: shows "f_range (Ch h)" using Ch_range unfolding f_range_on_def by blast (* CH *) lemma CH_card: shows "card (CH X) = (\h\UNIV. card (Ch h X))" unfolding CH_def by (simp add: card_UN_disjoint Ch_range_disjoint) lemma CH_simps: shows "CH {} = {}" unfolding CH_def by (simp add: Ch_simps) lemma CH_range: shows "CH A \ A" unfolding CH_def using Ch_range by blast lemmas CH_range' = subsetD[OF CH_range] lemmas CH_f_range_on = f_range_onI[OF CH_range] lemma mem_CH_Ch: shows "x \ CH X \ x \ Ch (Xh x) X" unfolding CH_def using Ch_range by blast lemma mem_Ch_CH: assumes "x \ Ch h X" shows "x \ CH X" unfolding CH_def using assms Ch_range by blast (*>*) text\ An @{emph \allocation\} is a set of contracts where each names a distinct doctor. (Hospitals can contract multiple doctors.) \ abbreviation (input) allocation :: "'x set \ bool" where "allocation \ inj_on Xd" text\ We often wish to extract a doctor's or a hospital's contract from an @{const "allocation"}. \ definition dX :: "'x set \ 'd \ 'x set" where "dX X d = {x \ X. Xd x = d}" definition hX :: "'x set \ 'h \ 'x set" where "hX X h = {x \ X. Xh x = h}" (*<*) lemma dX_union: shows "dX (X \ Y) d = dX X d \ dX Y d" unfolding dX_def by auto lemma dX_range: shows "\d. dX X d \ {x. Xd x = d}" unfolding dX_def by clarsimp lemma dX_range': assumes "x \ dX X d" shows "x \ X \ Xd x = d" using assms unfolding dX_def by simp lemma dX_empty_or_singleton: assumes "allocation X" shows "\d. dX X d = {} \ (\x. dX X d = {x})" unfolding dX_def using \allocation X\ by (fastforce dest: inj_onD) lemma dX_linear: assumes "allocation X" shows "Linear_order (dX X d \ dX X d)" using spec[OF dX_empty_or_singleton[OF \allocation X\], where x=d] by fastforce lemma dX_singular: assumes "allocation X" assumes "x \ X" assumes "d = Xd x" shows "dX X d = {x}" using assms unfolding dX_def by (fastforce dest: inj_onD) lemma dX_Int_Field_Pd: assumes "dX X d \ Field (Pd d)" shows "X \ Field (Pd d) = dX X d" using assms unfolding dX_def by (fastforce dest: Pd_range') lemma Cd_Above_dX: assumes "dX X d \ Field (Pd d)" shows "Cd d X = Above (Pd d) (dX X d) \ X" using assms unfolding Cd_greatest greatest_Above Above_def dX_def by (auto dest: Pd_range') (*>*) text\ @{emph \Stability\} is the key property we look for in a match (here a set of contracts), and consists of two parts. Firstly, we ask that it be @{emph \individually rational\}, i.e., the contracts in the match are actually acceptable to all participants. Note that this implies the match is an @{const "allocation"}. \ definition individually_rational_on :: "'d set \ 'x set \ bool" where "individually_rational_on ds X \ CD_on ds X = X \ CH X = X" abbreviation individually_rational :: "'x set \ bool" where "individually_rational \ individually_rational_on UNIV" text\ The second condition requires that there be no coalition of a hospital and one or more doctors who prefer another set of contracts involving them; the hospital strictly, the doctors weakly. Contrast this definition with the classical one for stable marriages given in \S\ref{sec:sotomayor}. \ definition blocking_on :: "'d set \ 'x set \ 'h \ 'x set \ bool" where "blocking_on ds X h X' \ X' \ Ch h X \ X' = Ch h (X \ X') \ X' \ CD_on ds (X \ X')" definition stable_no_blocking_on :: "'d set \ 'x set \ bool" where "stable_no_blocking_on ds X \ (\h X'. \blocking_on ds X h X')" abbreviation stable_no_blocking :: "'x set \ bool" where "stable_no_blocking \ stable_no_blocking_on UNIV" definition stable_on :: "'d set \ 'x set \ bool" where "stable_on ds X \ individually_rational_on ds X \ stable_no_blocking_on ds X" abbreviation stable :: "'x set \ bool" where "stable \ stable_on UNIV" (*<*) lemma stable_onI: assumes "individually_rational_on ds X" assumes "stable_no_blocking_on ds X" shows "stable_on ds X" unfolding stable_on_def using assms by blast lemma individually_rational_onI: assumes "CD_on ds X = X" assumes "CH X = X" shows "individually_rational_on ds X" unfolding individually_rational_on_def using assms by blast lemma individually_rational_on_CD_on: assumes "individually_rational_on ds X" shows "CD_on ds X = X" using assms unfolding individually_rational_on_def by blast lemma individually_rational_on_Cd: assumes "individually_rational_on ds X" shows "Cd d X = dX X d" using individually_rational_on_CD_on[OF assms] by (auto simp: dX_def mem_CD_on_Cd dest: Cd_range' Cd_Xd) lemma individually_rational_on_empty: shows "individually_rational_on ds {}" by (simp add: CD_on_simps CH_simps individually_rational_onI) lemma blocking_onI: assumes "X'' \ Ch h X" assumes "X'' = Ch h (X \ X'')" assumes "\x. x \ X'' \ x \ CD_on ds (X \ X'')" shows "blocking_on ds X h X''" unfolding blocking_on_def using assms by blast lemma blocking_on_imp_not_stable: assumes "blocking_on ds X h X''" shows "\stable_on ds X" unfolding stable_on_def stable_no_blocking_on_def using assms by blast lemma blocking_on_allocation: assumes "blocking_on ds X h X''" shows "allocation X''" using assms unfolding blocking_on_def by (metis Ch_singular') lemma blocking_on_Field: assumes "blocking_on ds X h X''" shows "dX X'' d \ Field (Pd d)" using assms blocking_on_allocation[OF assms] unfolding blocking_on_def dX_def by (force simp: Pd_range' dest: CD_on_range') lemma blocking_on_CD_on: assumes "blocking_on ds X h X''" shows "X'' \ CD_on ds (X \ X'')" using assms unfolding blocking_on_def by blast lemma blocking_on_CD_on': assumes "blocking_on ds X h X''" assumes "x \ X''" shows "x \ CD_on ds (X \ X'')" using assms unfolding blocking_on_def by blast lemma blocking_on_Cd: assumes "blocking_on ds X h X''" shows "dX X'' d \ Cd d (X \ X'')" using assms unfolding blocking_on_def by (force dest: dX_range' simp: mem_CD_on_Cd) lemma stable_no_blocking_onI: assumes "\h X''. \X'' = Ch h (X \ X''); X'' \ Ch h X; X'' \ CD_on ds (X \ X'')\ \ False" shows "stable_no_blocking_on ds X" unfolding stable_no_blocking_on_def blocking_on_def using assms by blast lemma stable_no_blocking_onI2: assumes "\h X''. blocking_on ds X h X'' \ False" shows "stable_no_blocking_on ds X" unfolding stable_no_blocking_on_def using assms by blast lemma "stable_no_blocking_on ds UNIV" using stable_no_blocking_onI by fastforce lemma assumes "stable_on ds X" shows stable_on_CD_on: "CD_on ds X = X" and stable_on_Xd: "x \ X \ Xd x \ ds" and stable_on_range': "x \ X \ x \ Field (Pd (Xd x))" and stable_on_CH: "CH X = X" and stable_on_no_blocking_on: "stable_no_blocking_on ds X" using assms mem_CD_on_Cd Cd_range' Pd_range' unfolding stable_on_def individually_rational_on_def by blast+ lemma stable_on_allocation: assumes "stable_on ds X" shows "allocation X" using assms unfolding stable_on_def individually_rational_on_def by (metis CD_on_inj_on_Xd) lemma stable_on_blocking_onD: assumes "stable_on ds X" shows "\X'' = Ch h (X \ X''); X'' \ CD_on ds (X \ X'')\ \ X'' = Ch h X" using \stable_on ds X\ unfolding stable_on_def individually_rational_on_def stable_no_blocking_on_def blocking_on_def by blast lemma not_stable_on_cases[consumes 1, case_names not_individually_rational not_no_blocking]: assumes "\ stable_on ds X" assumes "\ individually_rational_on ds X \ P" assumes "\ stable_no_blocking_on ds X \ P" shows "P" using assms unfolding stable_on_def by blast (*>*) text\\ end subsection\ Theorem~1: Existence of stable pairs \ text\ We proceed to define a function whose fixed points capture all stable matches. \citet[I(B), p917]{HatfieldMilgrom:2005} provide the following intuition: \begin{quote} The first theorem states that a set of contracts is stable if any alternative contract would be rejected by some doctor or some hospital from its suitably defined opportunity set. In the formulas below, think of the doctors' opportunity set as @{term "XD"} and the hospitals' opportunity set as @{term "XH"}. If @{term "X'"} is the corresponding stable set, then @{term "XD"} must include, in addition to @{term "X'"}, all contracts that would not be rejected by the hospitals, and @{term "XH"} must similarly include @{term "X'"} and all contracts that would not be rejected by the doctors. If @{term "X'"} is stable, then every alternative contract is rejected by somebody, so @{term "X = XH \ XD"} [where @{term "X"} is the set of all contracts]. This logic is summarized in the first theorem. \end{quote} See also \citet[p6,\S4]{Fleiner:2003} and \citet[\S2]{Fleiner:2002}, from whom we adopt the term @{emph \stable pair\}. \ context Contracts begin definition stable_pair_on :: "'d set \ 'x set \ 'x set \ bool" where "stable_pair_on ds = (\(XD, XH). XD = - RH XH \ XH = - RD_on ds XD)" abbreviation stable_pair :: "'x set \ 'x set \ bool" where "stable_pair \ stable_pair_on UNIV" abbreviation match :: "'x set \ 'x set \ 'x set" where "match X \ fst X \ snd X" text \ \citet[Theorem~1]{HatfieldMilgrom:2005} state that every solution @{term "(XD, XH)"} of @{const "stable_pair"} yields a stable match @{term "XD \ XH"}, and conversely, i.e., every stable match is the intersection of some stable pair. \citet{AygunSonmez:2012-WP2} show that neither is the case without further restrictions on the hospitals' choice functions @{term "Ch"}; we exhibit their counterexample below. Even so we can establish some properties in the present setting: \ lemma stable_pair_on_CD_on: assumes "stable_pair_on ds XD_XH" shows "match XD_XH = CD_on ds (fst XD_XH)" using %invisible assms CD_on_range unfolding stable_pair_on_def split_def fst_conv snd_conv by blast lemma stable_pair_on_CH: assumes "stable_pair_on ds XD_XH" shows "match XD_XH = CH (snd XD_XH)" using %invisible assms CH_range unfolding stable_pair_on_def split_def fst_conv snd_conv by blast lemma stable_pair_on_CD_on_CH: assumes "stable_pair_on ds XD_XH" shows "CD_on ds (fst XD_XH) = CH (snd XD_XH)" using %invisible assms stable_pair_on_CD_on stable_pair_on_CH by blast lemma stable_pair_on_allocation: assumes "stable_pair_on ds XD_XH" shows "allocation (match XD_XH)" unfolding %invisible stable_pair_on_CD_on[OF assms] by (rule CD_on_inj_on_Xd) (*<*) lemma stable_pair_onI: assumes "fst XD_XH = - RH (snd XD_XH)" assumes "snd XD_XH = - RD_on ds (fst XD_XH)" shows "stable_pair_on ds XD_XH" using assms unfolding stable_pair_on_def split_def by blast lemma stable_pair_onE: shows "\stable_pair_on ds XD_XH; \- RH (snd XD_XH) = fst XD_XH; - RD_on ds (fst XD_XH) = snd XD_XH\ \ P\ \ P" unfolding stable_pair_on_def split_def by blast lemma stable_pair_on_Cd: assumes "stable_pair_on ds XD_XH" assumes "d \ ds" shows "Cd d (fst XD_XH) = match XD_XH \ Field (Pd d)" using stable_pair_on_CD_on[OF \stable_pair_on ds XD_XH\] CD_on_domain Cd_domain \d \ ds\ by simp lemma stable_pair_on_Cd_match: assumes "stable_pair_on ds XD_XH" assumes "d \ ds" shows "Cd d (match XD_XH) = Cd d (fst XD_XH)" using assms by (metis Cd_domain Cd_idem stable_pair_on_Cd) lemma stable_pair_on_Xd: assumes "stable_pair_on ds XD_XH" assumes "x \ match XD_XH" shows "Xd x \ ds" using assms CD_on_Xd unfolding stable_pair_on_def split_def by blast lemma stable_pair_on_match_Cd: assumes "stable_pair_on ds XD_XH" assumes "x \ match XD_XH" shows "x \ Cd (Xd x) (match XD_XH)" using assms by (metis (full_types) CD_on_def Cd_Xd UN_iff stable_pair_on_CD_on stable_pair_on_Cd_match) (*>*) text\ We run out of steam on the following two lemmas, which are the remaining requirements for stability. \ lemma assumes "stable_pair_on ds XD_XH" shows "individually_rational_on ds (match XD_XH)" oops lemma assumes "stable_pair_on ds XD_XH" shows "stable_no_blocking (match XD_XH)" oops text\ \citet{HatfieldMilgrom:2005} also claim that the converse holds: \ lemma assumes "stable_on ds X" obtains XD_XH where "stable_pair_on ds XD_XH" and "X = match XD_XH" oops text\ Again, the following counterexample shows that the @{const substitutes} condition on @{term "Ch"} is too weak to guarantee this. We show it holds under stronger assumptions in \S\ref{sec:contracts-t1-converse}. \ end subsubsection\ Theorem~1 does not hold \citep{AygunSonmez:2012-WP2} \label{sec:contracts-t1-counterexample} \ text\ The following counterexample, due to \citet[\S3: Example~2]{AygunSonmez:2012-WP2}, comprehensively demonstrates that \citet[Theorem~1]{HatfieldMilgrom:2005} does not hold. We create three types: \D2\ consists of two elements, representing the doctors, and \H\ is the type of the single hospital. There are four contracts in the type \X4\. \ datatype D2 = D1 | D2 datatype H1 = H datatype X4 = Xd1 | Xd1' | Xd2 | Xd2' (*<*) lemma D2_UNIV: shows "UNIV = set [D1, D2]" using D2.exhaust by auto instantiation D2 :: enum begin definition "enum_class.enum = [D1, D2]" definition "enum_class.enum_all P = (P D1 \ P D2)" definition "enum_class.enum_ex P = (P D1 \ P D2)" instance by standard (simp_all add: enum_D2_def enum_all_D2_def enum_ex_D2_def D2_UNIV) end lemma D2_ALL: shows "(\d. P d) = (\d\{D1, D2}. P d)" using D2_UNIV by auto lemma D2_UNION: shows "(\d. P d) = (\d\{D1, D2}. P d)" using D2_UNIV by auto instance H1 :: finite by standard (metis (full_types) H1.exhaust ex_new_if_finite finite.intros(1) finite_insert insert_subset subset_insertI) lemma X4_UNIV: shows "UNIV = set [Xd1, Xd1', Xd2, Xd2']" using X4.exhaust by auto lemmas X4_pow = subset_subseqs[OF subset_trans[OF subset_UNIV Set.equalityD1[OF X4_UNIV]]] instance X4 :: finite by standard (simp add: X4_UNIV) lemma X4_ALL: shows "(\X''. P X'') \ (\X''\set ` set (subseqs [Xd1, Xd1', Xd2, Xd2']). P X'')" using X4_pow by blast (*>*) primrec X4d :: "X4 \ D2" where "X4d Xd1 = D1" | "X4d Xd1' = D1" | "X4d Xd2 = D2" | "X4d Xd2' = D2" abbreviation X4h :: "X4 \ H1" where "X4h _ \ H" primrec PX4d :: "D2 \ X4 rel" where "PX4d D1 = linord_of_list [Xd1', Xd1]" | "PX4d D2 = linord_of_list [Xd2, Xd2']" function CX4h :: "H1 \ X4 cfun" where "CX4h _ {Xd1} = {Xd1}" | "CX4h _ {Xd1'} = {Xd1'}" | "CX4h _ {Xd2} = {Xd2}" | "CX4h _ {Xd2'} = {Xd2'}" | "CX4h _ {Xd1, Xd1'} = {Xd1}" | "CX4h _ {Xd1, Xd2} = {Xd1, Xd2}" | "CX4h _ {Xd1, Xd2'} = {Xd2'}" | "CX4h _ {Xd1', Xd2} = {Xd1'}" | "CX4h _ {Xd1', Xd2'} = {Xd1', Xd2'}" | "CX4h _ {Xd2, Xd2'} = {Xd2}" | "CX4h _ {Xd1, Xd1', Xd2} = {}" | "CX4h _ {Xd1, Xd1', Xd2'} = {}" | "CX4h _ {Xd1, Xd2, Xd2'} = {}" | "CX4h _ {Xd1', Xd2, Xd2'} = {}" | "CX4h _ {Xd1, Xd1', Xd2, Xd2'} = {}" | "CX4h _ {} = {}" apply %invisible (case_tac x) apply (cut_tac X=b in X4_pow) apply simp apply force apply auto done (*<*) termination by %invisible lexicographic_order lemma PX4d_linear: shows "Linear_order (PX4d d)" by (cases d) (simp_all add: linord_of_list_Linear_order) lemma PX4d_range: shows "Field (PX4d d) \ {x. X4d x = d}" by (cases d) simp_all lemma CX4h_range: shows "CX4h h X \ {x \ X. H = h}" by (cases "(h, X)" rule: CX4h.cases) (auto simp: spec[OF H1.nchotomy, of h]) lemma CX4h_singular: shows "inj_on X4d (CX4h h X)" by (cases "(h, X)" rule: CX4h.cases) auto (*>*) text\\ interpretation StableNoDecomp: Contracts X4d X4h PX4d CX4h using %invisible PX4d_linear PX4d_range CX4h_range CX4h_singular by unfold_locales blast+ text\ There are two stable matches in this model. \ (*<*) lemma Xd1_Xd2_stable: shows "StableNoDecomp.stable {Xd1, Xd2}" proof(rule StableNoDecomp.stable_onI) show "StableNoDecomp.individually_rational {Xd1, Xd2}" by (simp add: StableNoDecomp.individually_rational_on_def StableNoDecomp.CD_on_def StableNoDecomp.CH_def insert_commute D2_UNION cong add: SUP_cong_simp) show "StableNoDecomp.stable_no_blocking {Xd1, Xd2}" apply (rule StableNoDecomp.stable_no_blocking_onI) apply (rule_tac x="(H, X'')" in CX4h.cases) apply (simp_all add: insert_commute) done qed lemma Xd1'_Xd2'_stable: shows "StableNoDecomp.stable {Xd1', Xd2'}" proof(rule StableNoDecomp.stable_onI) show "StableNoDecomp.individually_rational {Xd1', Xd2'}" by (simp add: StableNoDecomp.individually_rational_on_def StableNoDecomp.CD_on_def StableNoDecomp.CH_def insert_commute D2_UNION cong add: SUP_cong_simp) show "StableNoDecomp.stable_no_blocking {Xd1', Xd2'}" apply (rule StableNoDecomp.stable_no_blocking_onI) apply (rule_tac x="(H, X'')" in CX4h.cases) apply (simp_all add: insert_commute) done qed (*>*) text\\ lemma stable: shows "StableNoDecomp.stable X \ X = {Xd1, Xd2} \ X = {Xd1', Xd2'}" (*<*) (is "?lhs = ?rhs") proof(rule iffI) assume ?lhs then show ?rhs using X4_pow[where X=X] unfolding StableNoDecomp.stable_on_def StableNoDecomp.individually_rational_on_def StableNoDecomp.stable_no_blocking_on_def StableNoDecomp.blocking_on_def StableNoDecomp.CD_on_def StableNoDecomp.CH_def by simp (elim disjE, simp_all add: D2_UNION X4_ALL insert_commute StableNoDecomp.maxR_def cong add: SUP_cong_simp) next assume ?rhs then show ?lhs using Xd1_Xd2_stable Xd1'_Xd2'_stable by blast qed (*>*) text\ However neither arises from a pair \XD, XH\ that satisfy @{const "StableNoDecomp.stable_pair"}: \ lemma StableNoDecomp_XD_XH: shows "StableNoDecomp.stable_pair (XD, XH) \ (XD = {} \ XH = {Xd1, Xd1', Xd2, Xd2'})" (*<*) (is "?lhs = ?rhs") proof(rule iffI) note image_cong_simp [cong del] note INF_cong_simp [cong] note SUP_cong_simp [cong] assume ?lhs then show ?rhs (* Expand the Cartesian product and check. *) using X4_pow [of XD] X4_pow [of XH] apply simp apply (erule StableNoDecomp.stable_pair_onE) apply (elim disjE) apply (simp_all add: StableNoDecomp.CD_on_def StableNoDecomp.CH_def) unfolding X4_UNIV [simplified] apply (auto simp: D2_ALL D2_UNION X4_ALL insert_commute StableNoDecomp.maxR_def linord_of_list_linord_of_listP) done next assume ?rhs then show ?lhs unfolding StableNoDecomp.stable_pair_on_def using X4.exhaust by (auto simp: StableNoDecomp.CH_def) qed (*>*) text\\ proposition assumes "StableNoDecomp.stable_pair (XD, XH)" shows "\StableNoDecomp.stable (XD \ XH)" using %invisible assms apply (subst (asm) StableNoDecomp_XD_XH) apply (simp add: StableNoDecomp.stable_on_def StableNoDecomp.stable_no_blocking_on_def StableNoDecomp.blocking_on_def StableNoDecomp.individually_rational_on_empty) apply (auto simp: StableNoDecomp.mem_CD_on_Cd MaxR_def exI[where x=D1] exI[where x=H] exI[where x="{Xd1}"]) done text\ Moreover the converse of Theorem~1 does not hold either: the single decomposition that satisfies @{const "StableNoDecomp.stable_pair"} (@{thm [source] "StableNoDecomp_XD_XH"}) does not yield a stable match: \ proposition assumes "StableNoDecomp.stable X" shows "\(\XD XH. StableNoDecomp.stable_pair (XD, XH) \ X = XD \ XH)" using %invisible assms StableNoDecomp_XD_XH stable by fastforce text\ So there is not hope for \citet[Theorem~1]{HatfieldMilgrom:2005} as it stands. Note that the counterexample satisfies the @{const "substitutes"} condition (see \S\ref{sec:cf-substitutes}): \ lemma shows "substitutes (CX4h H)" proof %invisible (rule substitutes_onI) fix A a b assume "b \ CX4h H (insert b A)" then show "b \ CX4h H (insert a (insert b A))" apply (case_tac [!] a) apply (case_tac [!] b) apply ( (rule CX4h.cases[of "(H, A)"], auto simp: insert_commute)[1] )+ done qed text\ Therefore while @{const "substitutes"} supports the monotonicity argument that underpins their deferred-acceptance algorithm (see \S\ref{sec:contracts-algorithmics}), it is not enough to rescue Theorem~1. One way forward is to constrain the hospitals' choice functions, which we discuss in the next section. \ subsubsection\ Theorem 1 holds with @{emph \independence of rejected contracts\} \label{sec:contracts-irc} \ text\ \citet{AygunSonmez:2012-WP2} propose to rectify this issue by requiring hospitals' choices to satisfy @{const "irc"} (\S\ref{sec:cf-irc}). Reassuringly their counterexample fails to satisfy it: \ lemma shows "\irc (CX4h H)" by %invisible (fastforce simp: insert_commute dest: irc_onD[where a="Xd2" and B="{Xd1, Xd1'}"]) text\ We adopt this hypothesis by extending the @{const "Contracts"} locale: \ locale ContractsWithIRC = Contracts + assumes Ch_irc: "\h. irc (Ch h)" begin text\ This property requires that \Ch\ behave, for example, as follows: \ lemma Ch_domain: shows "Ch h (A \ {x. Xh x = h}) = Ch h A" using %invisible irc_on_discard[OF spec[OF Ch_irc, of h], where B="A \ {x. Xh x = h}" and C="A - {x. Xh x = h}"] by (fastforce simp: Un_Diff_Int ac_simps dest: Ch_range') lemma %invisible CH_domain: shows "CH A \ {x. Xh x = h} = Ch h (A \ {x. Xh x = h})" unfolding CH_def using Ch_range by (auto simp: Ch_domain) lemma %invisible stable_pair_on_Ch: assumes "stable_pair_on ds XD_XH" shows "Ch h (snd XD_XH) = match XD_XH \ {x. Xh x = h}" using stable_pair_on_CH[OF assms] CH_domain Ch_domain by simp lemmas %invisible Ch_consistency = irc_on_consistency_on[OF spec[OF Ch_irc], simplified, of h] for h lemmas Ch_irc_idem = consistency_on_f_idem[OF Ch_f_range Ch_consistency, simplified] lemma CH_irc_idem: shows "CH (CH A) = CH A" unfolding %invisible CH_def by (metis CH_def CH_domain Ch_domain Ch_irc_idem) lemma Ch_CH_irc_idem: shows "Ch h (CH A) = Ch h A" using %invisible CH_domain CH_irc_idem Ch_domain by blast text\ This suffices to show the left-to-right direction of Theorem~1. \ lemma stable_pair_on_individually_rational: assumes "stable_pair_on ds XD_XH" shows "individually_rational_on ds (match XD_XH)" by %invisible (metis CD_on_idem CH_irc_idem stable_pair_on_CD_on stable_pair_on_CD_on_CH assms individually_rational_onI) lemma stable_pair_on_stable_no_blocking_on: assumes "stable_pair_on ds XD_XH" shows "stable_no_blocking_on ds (match XD_XH)" proof(rule stable_no_blocking_onI) fix h X'' assume C: "X'' = Ch h (match XD_XH \ X'')" assume NE: "X'' \ Ch h (match XD_XH)" assume CD: "X'' \ CD_on ds (match XD_XH \ X'')" have "X'' \ snd XD_XH" proof - from CD have "X'' \ CD_on ds (CD_on ds (fst XD_XH) \ X'')" by (simp only: stable_pair_on_CD_on[OF assms]) then have "X'' \ CD_on ds (fst XD_XH \ X'')" using CD_on_path_independent unfolding path_independent_def by (simp add: Un_commute) moreover have "fst XD_XH \ CD_on ds (fst XD_XH \ X'') \ CD_on ds (fst XD_XH)" using CD_on_Chernoff unfolding Chernoff_on_def by (simp add: inf_commute) ultimately show ?thesis using assms unfolding stable_pair_on_def split_def by blast qed then have "Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \ X'')" by (force intro!: consistencyD[OF Ch_consistency] dest: Ch_range') moreover from NE have "X'' \ Ch h (snd XD_XH)" using stable_pair_on_CH[OF assms] CH_domain[of _ h] Ch_domain[of h] by (metis Ch_irc_idem) ultimately have "X'' \ Ch h (match XD_XH \ X'')" using stable_pair_on_CH[OF assms] CH_domain[of _ h] Ch_domain[of h] by (metis (no_types, lifting) inf.right_idem inf_sup_distrib2) with C show False by blast qed theorem stable_pair_on_stable_on: assumes "stable_pair_on ds XD_XH" shows "stable_on ds (match XD_XH)" using %invisible assms stable_pair_on_allocation stable_pair_on_individually_rational stable_pair_on_stable_no_blocking_on by (blast intro: stable_onI) end subsubsection\ The converse of Theorem~1 \label{sec:contracts-t1-converse} \ text (in Contracts) \ The forward direction of Theorem~1 gives us a way of finding stable matches by computing fixed points of a function closely related to @{const "stable_pair"} (see \S\ref{sec:contracts-algorithmics}). The converse says that every stable match can be decomposed in this way, which implies that the stable matches form a lattice (see also \S\ref{sec:contracts-algorithmics}). The following proofs assume that the hospitals' choice functions satisfy @{const "substitutes"} and @{const "irc"}. \ context ContractsWithIRC begin context fixes ds :: "'b set" fixes X :: "'a set" begin text\ Following \citet[Proof of Theorem~1]{HatfieldMilgrom:2005}, we partition the set of all contracts into @{term "[X, XD_smallest - X, XH_largest - X]"} with careful definitions of the two sets @{term "XD_smallest"} and @{term "XH_largest"}. Specifically @{term "XH_largest"} contains all contracts ranked at least as good as those in @{term "X"} by the doctors, considering unemployment and unacceptable contracts. Similarly @{term "XD_smallest"} contains those ranked at least as poorly. \ definition XH_largest :: "'a set" where "XH_largest = {y. Xd y \ ds \ y \ Field (Pd (Xd y)) \ (\x \ dX X (Xd y). (x, y) \ Pd (Xd y))}" definition XD_smallest :: "'a set" where "XD_smallest = - (XH_largest - X)" context assumes "stable_on ds X" begin lemma Ch_XH_largest_Field: assumes "x \ Ch h XH_largest" shows "x \ Field (Pd (Xd x))" using assms unfolding XH_largest_def by (blast dest: Ch_range') lemma Ch_XH_largest_Xd: assumes "x \ Ch h XH_largest" shows "Xd x \ ds" using assms unfolding XH_largest_def by (blast dest: Ch_range') lemma X_subseteq_XH_largest: shows "X \ XH_largest" proof(rule subsetI) fix x assume "x \ X" then obtain d where "d \ ds" "x \ Cd d X" using stable_on_CD_on[OF \stable_on ds X\] unfolding CD_on_def by blast with \stable_on ds X\ show "x \ XH_largest" using Pd_linear' Pd_range' Cd_range subset_Image1_Image1_iff[of "Pd d"] stable_on_allocation[of ds X] unfolding XH_largest_def linear_order_on_def partial_order_on_def stable_on_def inj_on_def dX_def by simp blast qed lemma X_subseteq_XD_smallest: shows "X \ XD_smallest" unfolding XD_smallest_def by blast lemma X_XD_smallest_XH_largest: shows "X = XD_smallest \ XH_largest" using X_subseteq_XH_largest unfolding XD_smallest_def by blast text\ The goal of the next few lemmas is to show the constituents of @{term "stable_pair_on ds (XD_smallest, XH_largest)"}. Intuitively, if a doctor has a contract @{term "x"} in @{term "X"}, then all of their contracts in @{const "XH_largest"} are at least as desirable as @{term "x"}, and so the @{const "stable_no_blocking"} hypothesis guarantees the hospitals choose @{term "x"} from @{const "XH_largest"}, and similarly the doctors @{term "x"} from @{const "XD_smallest"}. \ lemma XH_largestCdXXH_largest: assumes "x \ Ch h XH_largest" shows "x \ Cd (Xd x) (X \ Ch h XH_largest)" proof - from assms have "(y, x) \ Pd (Xd x)" if "Xd y = Xd x" and "y \ X" for y using that by (fastforce simp: XH_largest_def dX_def dest: Ch_range') with Ch_XH_largest_Field[OF assms] Pd_linear Pd_range show ?thesis using assms Ch_XH_largest_Field[OF assms] by (clarsimp simp: Cd_greatest greatest_def) (metis Ch_singular Pd_range' inj_onD subset_refl underS_incl_iff) qed lemma CH_XH_largest: shows "CH XH_largest = X" proof - have "Ch h XH_largest \ CD_on ds (X \ Ch h XH_largest)" for h using XH_largestCdXXH_largest Ch_XH_largest_Xd Ch_XH_largest_Field unfolding CD_on_def by blast from \stable_on ds X\ have "Ch h XH_largest = Ch h X" for h using \Ch h XH_largest \ CD_on ds (X \ Ch h XH_largest)\ X_subseteq_XH_largest by - (erule stable_on_blocking_onD[where h=h and X''="Ch h XH_largest"]; force intro!: consistencyD[OF Ch_consistency] dest: Ch_range') with stable_on_CH[OF \stable_on ds X\] show ?thesis unfolding CH_def by simp qed lemma Cd_XD_smallest: assumes "d \ ds" shows "Cd d (XD_smallest \ Field (Pd d)) = Cd d (X \ Field (Pd d))" proof(cases "X \ Field (Pd d) = {}") case True with Pd_range' Cd_range'[where X=X] stable_on_CD_on[OF \stable_on ds X\] mem_CD_on_Cd assms have "- XH_largest \ Field (Pd d) = {}" unfolding XH_largest_def dX_def by auto blast then show ?thesis unfolding XD_smallest_def by (simp add: Int_Un_distrib2) next case False with Pd_linear'[of d] \stable_on ds X\ stable_on_CD_on stable_on_allocation assms show ?thesis unfolding XD_smallest_def order_on_defs total_on_def by (auto 0 0 simp: Int_Un_distrib2 Cd_greatest greatest_def XH_largest_def dX_def) (metis (mono_tags, lifting) IntI Pd_range' UnCI inj_onD)+ qed lemma CD_on_XD_smallest: shows "CD_on ds XD_smallest = X" using stable_on_CD_on[OF \stable_on ds X\] unfolding CD_on_def2 by (simp add: Cd_XD_smallest) theorem stable_on_stable_pair_on: shows "stable_pair_on ds (XD_smallest, XH_largest)" proof(rule stable_pair_onI, simp_all only: prod.sel) from CH_XH_largest have "- RH XH_largest = - (XH_largest - X)" by blast also from X_XD_smallest_XH_largest have "\ = XD_smallest" unfolding XD_smallest_def by blast finally show "XD_smallest = -RH XH_largest" by blast next from CD_on_XD_smallest have "-RD_on ds XD_smallest = -(XD_smallest - X)" by simp also have "\ = XH_largest" unfolding XD_smallest_def using X_subseteq_XH_largest by blast finally show "XH_largest = -RD_on ds XD_smallest" by blast qed end end text\ Our ultimate statement of Theorem~1 of \cite{HatfieldMilgrom:2005} ala \citet{AygunSonmez:2012-WP2} goes as follows, bearing in mind that we are working in the @{const "ContractsWithIRC"} locale: \ theorem T1: shows "stable_on ds X \ (\XD_XH. stable_pair_on ds XD_XH \ X = match XD_XH)" using stable_pair_on_stable_on stable_on_stable_pair_on X_XD_smallest_XH_largest by fastforce end subsection\ Theorem~3: Algorithmics \label{sec:contracts-algorithmics} \ text (in Contracts) \ Having revived Theorem~1, we reformulate @{const "stable_pair"} as a monotone (aka @{emph \isotone\}) function and exploit the lattice structure of its fixed points, following \citet[{\S}II, Theorem~3]{HatfieldMilgrom:2005}. This underpins all of their results that we formulate here. \citet[\S2]{Fleiner:2002} provides an intuitive gloss of these definitions. \ context Contracts begin definition F1 :: "'x cfun" where "F1 X' = - RH X'" definition F2 :: "'d set \ 'x cfun" where "F2 ds X' = - RD_on ds X'" definition F :: "'d set \ 'x set \ 'x set dual \ 'x set \ 'x set dual" where "F ds = (\(XD, XH). (F1 (undual XH), dual (F2 ds (F1 (undual XH)))))" text\ We exploit Isabelle/HOL's ordering type classes (over the type constructors @{typ "'a set"} and @{typ "'a \ 'b"}) to define @{const "F"}. As @{const "F"} is @{const "antimono"} (where @{thm "antimono_def"} for a lattice order \\\) on its second argument \XH\, we adopt the dual lattice order using the type constructor @{typ "'a dual"}, where @{const "dual"} and @{const "undual"} mediate the isomorphism on values, to satisfy Isabelle/HOL's @{const "mono"} predicate. Note we work under the @{const "substitutes"} hypothesis here. Relating this function to @{const "stable_pair"} is syntactically awkward but straightforward: \ lemma fix_F_stable_pair_on: assumes "X = F ds X" shows "stable_pair_on ds (map_prod id undual X)" using %invisible assms by (cases X) (simp add: F_def F1_def F2_def stable_pair_on_def dual_eq_iff) lemma stable_pair_on_fix_F: assumes "stable_pair_on ds X" shows "map_prod id dual X = F ds (map_prod id dual X)" using %invisible assms unfolding F_def F1_def F2_def stable_pair_on_def split_def by (metis fst_map_prod id_apply prod.collapse snd_map_prod undual_dual) end text (in Contracts) \ The function @{const F} is monotonic under @{const substitutes}. \ locale ContractsWithSubstitutes = Contracts + assumes Ch_substitutes: "\h. substitutes (Ch h)" begin (*<*) lemma Rh_mono: shows "mono (Rh h)" using %invisible substitutes_on_Rf_mono_on[OF spec[OF Ch_substitutes]] mono_on_mono by (simp add: fun_eq_iff) blast lemmas Ch_iia = Rh_mono[unfolded Rf_mono_iia] lemmas Ch_Chernoff = Ch_iia[unfolded Chernoff_on_iia_on[symmetric]] lemmas Ch_subsitutes_idem = iia_f_idem[OF Ch_f_range Ch_iia, simplified] lemma RH_mono: shows "mono RH" unfolding %invisible CH_def by (rule monoI) (auto dest: monoD[OF Rh_mono]) lemmas CH_iia = RH_mono[unfolded Rf_mono_iia] lemmas CH_Chernoff = CH_iia[unfolded Chernoff_on_iia_on[symmetric]] lemmas CH_substitutes_idem = iia_f_idem[OF CH_f_range_on CH_iia, simplified] (*>*) text\\ lemma F1_antimono: shows "antimono F1" by %invisible (rule antimonoI) (auto simp: F1_def dest: Diff_mono[OF _ monoD[OF RH_mono]]) lemma F2_antimono: shows "antimono (F2 ds)" by %invisible (rule antimonoI) (auto simp: F2_def dest: Diff_mono[OF _ monoD[OF RD_on_mono]]) lemma F_mono: shows "mono (F ds)" unfolding %invisible F_def using antimonoD[OF F1_antimono] antimonoD[OF F2_antimono] by (auto intro: monoI simp: less_eq_dual_def) text\ We define the extremal fixed points using Isabelle/HOL's least and greatest fixed point operators: \ definition gfp_F :: "'b set \ 'a set \ 'a set" where "gfp_F ds = map_prod id undual (gfp (F ds))" definition lfp_F :: "'b set \ 'a set \ 'a set" where "lfp_F ds = map_prod id undual (lfp (F ds))" lemmas gfp_F_stable_pair_on = fix_F_stable_pair_on[OF gfp_unfold[OF F_mono], folded gfp_F_def] lemmas lfp_F_stable_pair_on = fix_F_stable_pair_on[OF lfp_unfold[OF F_mono], folded lfp_F_def] text\ These last two lemmas show that the least and greatest fixed points do satisfy @{const "stable_pair"}. Using standard fixed-point properties, we can establish: \ lemma F2_o_F1_mono: shows "mono (F2 ds \ F1)" by %invisible (metis F2_antimono F1_antimono antimono_def comp_apply monoI) lemmas F2_F1_mono = F2_o_F1_mono[unfolded o_def] lemma gfp_F_lfp_F: shows "gfp_F ds = (F1 (lfp (F2 ds \ F1)), lfp (F2 ds \ F1))" proof %invisible - let ?F' = "dual \ F2 ds \ F1 \ undual" have "gfp (F ds) = (F1 (undual (gfp ?F')), gfp ?F')" by (subst gfp_prod[OF F_mono]) (simp add: F_def o_def gfp_const) also have "gfp ?F' = dual (lfp (F2 ds \ F1))" by (simp add: lfp_dual_gfp[OF F2_o_F1_mono, simplified o_assoc]) finally show ?thesis unfolding gfp_F_def by simp qed end text\ We need hospital CFs to satisfy both @{const substitutes} and @{const irc} to relate these fixed points to stable matches. \ locale ContractsWithSubstitutesAndIRC = ContractsWithSubstitutes + ContractsWithIRC begin lemmas gfp_F_stable_on = stable_pair_on_stable_on[OF gfp_F_stable_pair_on] lemmas lfp_F_stable_on = stable_pair_on_stable_on[OF lfp_F_stable_pair_on] end text\ \label{sec:contracts-codegen-gfp_F} We demonstrate the effectiveness of our definitions by executing an example due to \citet[p920]{HatfieldMilgrom:2005} using Isabelle/HOL's code generator \citep{Haftmann-Nipkow:2010:code}. Note that, while adequate for this toy instance, the representations used here are hopelessly n{\"a}ive: sets are represented by lists and operations typically traverse the entire contract space. It is feasible, with more effort, to derive efficient algorithms; see, for instance, \citet{Bijlsma:1991,Bulwahn-et-al:2008:imp_HOL}. \ context ContractsWithSubstitutes begin lemma gfp_F_code[code]: shows "gfp_F ds = map_prod id undual (while (\A. F ds A \ A) (F ds) top)" using %invisible gfp_F_def gfp_while_lattice[OF F_mono] by simp lemma lfp_F_code[code]: shows "lfp_F ds = map_prod id undual (while (\A. F ds A \ A) (F ds) bot)" using %invisible lfp_F_def lfp_while_lattice[OF F_mono] by simp end text\ There are two hospitals and two doctors. \ datatype H2 = H1 | H2 text\ The contract space is simply the Cartesian product @{typ "D2 \ H2"}. \ type_synonym X_D2_H2 = "D2 \ H2" text\ Doctor @{const "D1"} prefers \H1 \ H2\, doctor @{const "D2"} the same \H1 \ H2\ (but over different contracts). \ primrec P_D2_H2_d :: "D2 \ X_D2_H2 rel" where "P_D2_H2_d D1 = linord_of_list [(D1, H1), (D1, H2)]" | "P_D2_H2_d D2 = linord_of_list [(D2, H1), (D2, H2)]" text\ Hospital @{const "H1"} prefers \{D1} \ {D2} \ \\, and hospital @{const "H2"} \{D1, D2} \ {D1} \ {D2} \ \\. We interpret these constraints as follows: \ definition P_D2_H2_H1 :: "X_D2_H2 cfun" where "P_D2_H2_H1 A = (if (D1, H1) \ A then {(D1, H1)} else if (D2, H1) \ A then {(D2, H1)} else {})" definition P_D2_H2_H2 :: "X_D2_H2 cfun" where "P_D2_H2_H2 A = (if {(D1, H2), (D2, H2)} \ A then {(D1, H2), (D2, H2)} else if (D1, H2) \ A then {(D1, H2)} else if (D2, H2) \ A then {(D2, H2)} else {})" primrec P_D2_H2_h :: "H2 \ X_D2_H2 cfun" where "P_D2_H2_h H1 = P_D2_H2_H1" | "P_D2_H2_h H2 = P_D2_H2_H2" (*<*) lemma H2_UNIV: shows "UNIV = set [H1, H2]" using H2.exhaust by auto instantiation H2 :: enum begin definition "enum_class.enum = [H1, H2]" definition "enum_class.enum_all P = (P H1 \ P H2)" definition "enum_class.enum_ex P = (P H1 \ P H2)" instance by standard (simp_all add: enum_H2_def enum_all_H2_def enum_ex_H2_def H2_UNIV) end lemma H2_ALL [simp]: shows "(\h. P h) = (\h\{H1, H2}. P h)" using H2_UNIV by auto lemma H2_UNION: shows "(\h. P h) = (\h\{H1, H2}. P h)" using H2_UNIV by auto lemma P_D2_H2_d_linear: shows "Linear_order (P_D2_H2_d d)" by (cases d) (simp_all add: linord_of_list_Linear_order) lemma P_D2_H2_d_range: shows "Field (P_D2_H2_d d) \ {x. fst x = d}" by (cases d) simp_all lemma P_D2_H2_h_substitutes: shows "substitutes (P_D2_H2_h h)" by %invisible (cases h) (auto intro!: substitutes_onI simp: P_D2_H2_H1_def P_D2_H2_H2_def split: if_splits) (*>*) text\ Isabelle's code generator requires us to hoist the relevant definitions from the locale to the top-level (see the \verb!codegen! documentation, \S7.3). \ global_interpretation P920_example: ContractsWithSubstitutes fst snd P_D2_H2_d P_D2_H2_h defines P920_example_gfp_F = P920_example.gfp_F and P920_example_lfp_F = P920_example.lfp_F and P920_example_F = P920_example.F and P920_example_F1 = P920_example.F1 and P920_example_F2 = P920_example.F2 and P920_example_maxR = P920_example.maxR and P920_example_MaxR_f = P920_example.MaxR_f and P920_example_Cd = P920_example.Cd and P920_example_CD_on = P920_example.CD_on and P920_example_CH = P920_example.CH using %invisible P_D2_H2_d_linear P_D2_H2_h_substitutes by %invisible unfold_locales (simp_all, simp_all add: D2_ALL P_D2_H2_H1_def P_D2_H2_H2_def) (*<*) (* Codegen hackery: avoid the CoSet constructor as some operations do not handle it. *) declare UNIV_coset[code del] declare UNIV_enum[code] declare compl_set[code del] compl_coset[code del] declare Compl_eq_Diff_UNIV[code] (* code_thms P920_example_gfp_F export_code P920_example_gfp_F in SML module_name F file "F.sml" value "P920_example_gfp_F UNIV" *) lemma P920_example_gfp_F_value: shows "P920_example_gfp_F UNIV = ({(D1, H1), (D1, H2), (D2, H2)}, {(D1, H1), (D2, H1), (D2, H2)})" by eval lemma P920_example_gfp_F_match_value: shows "P920_example.match (P920_example_gfp_F UNIV) = {(D1, H1), (D2, H2)}" unfolding P920_example_gfp_F_value by simp lemma P920_example_lfp_F_value: shows "P920_example_lfp_F UNIV = ({(D1, H1), (D1, H2), (D2, H2)}, {(D1, H1), (D2, H1), (D2, H2)})" by eval (*>*) text\ We can now evaluate the @{const "gfp"} of @{const "P920_example.F"} (i.e., \F\ specialized to the above constants) using Isabelle's \verb!value! antiquotation or \verb!eval! method. This yields the \(XD, XH)\ pair: \begin{center} @{thm (rhs) "P920_example_gfp_F_value"} \end{center} The stable match is therefore @{thm (rhs) "P920_example_gfp_F_match_value"}. The @{const "lfp"} of @{const "P920_example.F"} is identical to the @{const "gfp"}: \begin{center} @{thm (rhs) "P920_example_lfp_F_value"} \end{center} This implies that there is only one stable match in this scenario. \ subsection\ Theorem~4: Optimality \label{sec:contracts-optimality} \ text (in ContractsWithSubstitutes) \ \citet[Theorem~4]{HatfieldMilgrom:2005} assert that the greatest fixed point @{const "gfp_F"} of @{const "F"} yields the stable match most preferred by the doctors in the following sense: \ context Contracts begin definition doctor_optimal_match :: "'d set \ 'x set \ bool" where "doctor_optimal_match ds Y \ (stable_on ds Y \ (\X. \x\X. stable_on ds X \ (\y \ Y. (x, y) \ Pd (Xd x))))" (*<*) lemmas doctor_optimal_matchI = iffD2[OF doctor_optimal_match_def, unfolded conj_imp_eq_imp_imp, rule_format] lemmas doctor_optimal_match_stable_on = iffD1[OF doctor_optimal_match_def, THEN conjunct1] lemmas doctor_optimal_match_optimal = iffD1[OF doctor_optimal_match_def, THEN conjunct2, rule_format] lemma doctor_optimal_match_unique: assumes "doctor_optimal_match ds X" assumes "doctor_optimal_match ds Y" shows "X = Y" proof(rule iffD2[OF set_eq_iff, rule_format]) fix x from Pd_linear'[where d="Xd x"] Pd_Xd[where d="Xd x"] stable_on_allocation[OF doctor_optimal_match_stable_on[OF assms(1)]] stable_on_allocation[OF doctor_optimal_match_stable_on[OF assms(2)]] assms show "x \ X \ x \ Y" unfolding doctor_optimal_match_def order_on_defs by - (rule iffI; metis antisymD inj_on_eq_iff) qed (*>*) end text (in ContractsWithSubstitutes) \ In a similar sense, @{const "lfp_F"} is the doctor-pessimal match. We state a basic doctor-optimality result in terms of @{const "stable_pair"} in the @{const "ContractsWithSubstitutes"} locale for generality; we can establish @{const "doctor_optimal_match"} only under additional constraints on hospital choice functions (see \S\ref{sec:contracts-irc}). \ context ContractsWithSubstitutes begin context fixes XD_XH :: "'a set \ 'a set" fixes ds :: "'b set" assumes "stable_pair_on ds XD_XH" begin lemma gfp_F_upperbound: shows "(fst XD_XH, dual (snd XD_XH)) \ gfp (F ds)" proof %invisible - have "(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))" using stable_pair_on_fix_F[OF \stable_pair_on ds XD_XH\] by (metis id_apply map_prod_simp prod.collapse) then show ?thesis by (fastforce intro: gfp_upperbound) qed lemma XD_XH_gfp_F: shows "fst XD_XH \ fst (gfp_F ds)" and "snd (gfp_F ds) \ snd XD_XH" using %invisible gfp_F_upperbound unfolding gfp_F_def by (simp_all add: less_eq_dual_def less_eq_prod_def) lemma lfp_F_upperbound: shows "lfp (F ds) \ (fst XD_XH, dual (snd XD_XH))" proof %invisible - have "(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))" using stable_pair_on_fix_F[OF \stable_pair_on ds XD_XH\] by (metis id_apply map_prod_simp prod.collapse) then show ?thesis by (fastforce intro: lfp_lowerbound) qed lemma XD_XH_lfp_F: shows "fst (lfp_F ds) \ fst XD_XH" and "snd XD_XH \ snd (lfp_F ds)" using %invisible lfp_F_upperbound unfolding lfp_F_def by (simp_all add: less_eq_dual_def less_eq_prod_def) text\ We appeal to the doctors' linear preferences to show the optimality (pessimality) of @{const "gfp_F"} (@{const "lfp_F"}) for doctors. \ theorem gfp_f_doctor_optimal: assumes "x \ match XD_XH" shows "\y \ match (gfp_F ds). (x, y) \ Pd (Xd x)" using %invisible assms gfp_F_stable_pair_on[where ds=ds] \stable_pair_on ds XD_XH\ stable_pair_on_CD_on stable_pair_on_Xd Cd_Xd mem_CD_on_Cd XD_XH_gfp_F(1) Cd_mono[where d="Xd x" and x=x and X="fst XD_XH" and Y="fst (gfp_F ds)"] by (metis sup.absorb_iff2) theorem lfp_f_doctor_pessimal: assumes "x \ match (lfp_F ds)" shows "\y \ match XD_XH. (x, y) \ Pd (Xd x)" using %invisible assms lfp_F_stable_pair_on[where ds=ds] \stable_pair_on ds XD_XH\ stable_pair_on_CD_on stable_pair_on_Xd Cd_Xd mem_CD_on_Cd XD_XH_lfp_F(1) Cd_mono[where d="Xd x" and x=x and X="fst (lfp_F ds)" and Y="fst XD_XH"] by (metis sup.absorb_iff2) end end theorem (in ContractsWithSubstitutesAndIRC) gfp_F_doctor_optimal_match: shows "doctor_optimal_match ds (match (gfp_F ds))" by %invisible (rule doctor_optimal_matchI[OF gfp_F_stable_on]) (auto simp: T1 elim: gfp_f_doctor_optimal) text (in ContractsWithSubstitutesAndIRC) \ Conversely @{const "lfp_F"} is most preferred by the hospitals in a revealed-preference sense, and @{const "gfp_F"} least preferred. These results depend on @{thm [source] Ch_domain} and hence the @{const "irc"} hypothesis on hospital choice functions. \ context ContractsWithSubstitutesAndIRC begin theorem lfp_f_hospital_optimal: assumes "stable_pair_on ds XD_XH" assumes "x \ Ch h (match (lfp_F ds))" shows "x \ Ch h (match (lfp_F ds) \ match XD_XH)" proof %invisible - from \stable_pair_on ds XD_XH\ have "match (lfp_F ds) \ match XD_XH \ snd (lfp_F ds)" by (simp add: XD_XH_lfp_F(2) le_infI2) with \x \ Ch h (match (lfp_F ds))\ lfp_F_stable_pair_on stable_pair_on_Ch Ch_range show ?thesis by - (rule iia_onD[OF Ch_iia[where h=h], where B="snd (lfp_F ds)", simplified]; blast) qed theorem gfp_f_hospital_pessimal: assumes "stable_pair_on ds XD_XH" assumes "x \ Ch h (match XD_XH)" shows "x \ Ch h (match (gfp_F ds) \ match XD_XH)" proof %invisible - from \stable_pair_on ds XD_XH\ have "match (gfp_F ds) \ match XD_XH \ snd XD_XH" by (simp add: XD_XH_gfp_F(2) le_infI2) with assms lfp_F_stable_pair_on stable_pair_on_Ch Ch_range show ?thesis by - (rule iia_onD[OF Ch_iia[where h=h], where B="snd XD_XH", simplified]; blast+) qed end text\ The general lattice-theoretic results of e.g. \citet{Fleiner:2002} depend on the full Tarski-Knaster fixed point theorem, which is difficult to state in the present type class-based setting. (The theorem itself is available in the Isabelle/HOL distribution but requires working with less convenient machinery.) \ subsection\ Theorem~5 does not hold \citep{HatfieldKojima:2008} \ text (in Contracts) \ \citet[Theorem~5]{HatfieldMilgrom:2005} claim that: \begin{quote} Suppose \H\ contains at least two hospitals, which we denote by \h\ and \h'\. Further suppose that @{term "Rh h"} is not isotone, that is, contracts are not @{const "substitutes"} for \h\. Then there exist preference orderings for the doctors in set \D\, a preference ordering for a hospital \h'\ with a single job opening such that, regardless of the preferences of the other hospitals, no stable set of contracts exists. \end{quote} \citet[Observation~1]{HatfieldKojima:2008} show this is not true: there can be stable matches even if hospital choice functions violate @{const "substitutes"}. This motivates looking for conditions weaker than @{const "substitutes"} that still guarantee stable matches, a project taken up by \citet{HatfieldKojima:2010}; see \S\ref{sec:cop}. We omit their counterexample to this incorrect claim. \ subsection\ Theorem~6: ``Vacancy chain'' dynamics \label{sec:contracts-vacancy-chain} \ text (in ContractsWithSubstitutesAndIRC) \ \citet[II(C), p923]{HatfieldMilgrom:2005} propose a model for updating a stable match @{term "X"} when a doctor @{term "d'"} retires. Intuitively the contracts mentioning @{term "d'"} are discarded and a modified algorithm run from the @{const "XH_largest"} and @{const "XD_smallest"} sets determined from @{term "X"}. The result is another stable match where the remaining doctors @{term "ds - {d'}"} are (weakly) better off and the hospitals (weakly) worse off than they were in the initial state. The proofs are essentially the same as for optimality (\S\ref{sec:contracts-optimality}). \ context ContractsWithSubstitutesAndIRC begin context fixes X :: "'a set" fixes d' :: "'b" fixes ds :: "'b set" begin text\ \citeauthor{HatfieldMilgrom:2005} do not motivate why the process uses this functional and not @{const "F"}. \ definition F' :: "'a set \ 'a set dual \ 'a set \ 'a set dual" where "F' = (\(XD, XH). (- RH (undual XH), dual (- RD_on (ds-{d'}) XD)))" lemma F'_apply: "F' (XD, XH) = (- RH (undual XH), dual (- RD_on (ds - {d'}) XD))" by (simp add: F'_def) lemma %invisible F1'_antimono: shows "antimono (\XH. - RH XH)" by %invisible (rule antimonoI) (auto simp: F1_def dest: Diff_mono[OF _ monoD[OF RH_mono]]) lemma %invisible F2'_antimono: shows "antimono (\XD. - RD_on (ds-{d'}) XD)" by %invisible (rule antimonoI) (auto simp: F2_def dest: Diff_mono[OF _ monoD[OF RD_on_mono]]) lemma F'_mono: shows "mono F'" unfolding %invisible F'_def using antimonoD[OF F1'_antimono] antimonoD[OF F2'_antimono] by (auto intro: monoI simp: less_eq_dual_def) lemma fix_F'_stable_pair_on: "stable_pair_on (ds - {d'}) (map_prod id undual A)" if "A = F' A" proof %invisible - obtain x y where "A = (x, y)" by (cases A) with that have "F' (x, y) = (x, y)" by simp then have "- Rf CH (undual y) = x" and "dual (- Rf (CD_on (ds - {d'})) x) = y" by (simp_all only: F'_apply prod_eq_iff fst_conv snd_conv) with \A = (x, y)\ show ?thesis by (simp add: stable_pair_on_def dual_eq_iff) qed text\ We model their update process using the @{const "while"} combinator, as we cannot connect it to the extremal fixed points as we did in \S\ref{sec:contracts-algorithmics} because we begin computing from the stable match @{term "X"}. \ definition F'_iter :: "'a set \ 'a set dual" where "F'_iter = (while (\A. F' A \ A) F' (XD_smallest ds X, dual (XH_largest ds X)))" abbreviation F'_iter_match :: "'a set" where "F'_iter_match \ match (map_prod id undual F'_iter)" context assumes "stable_on ds X" begin lemma F_start: shows "F ds (XD_smallest ds X, dual (XH_largest ds X)) = (XD_smallest ds X, dual (XH_largest ds X))" using %invisible CH_XH_largest[OF \stable_on ds X\] CD_on_XD_smallest[OF \stable_on ds X\] X_subseteq_XH_largest[OF \stable_on ds X\] unfolding F_def F1_def F2_def XD_smallest_def by (auto simp add: dual_eq_iff) lemma F'_start: shows "(XD_smallest ds X, dual (XH_largest ds X)) \ F' (XD_smallest ds X, dual (XH_largest ds X))" using %invisible F_start unfolding F_def F1_def F2_def F'_def unfolding CD_on_def XD_smallest_def by (auto simp add: dual_eq_iff dual_less_eq_iff) lemma shows F'_iter_stable_pair_on: "stable_pair_on (ds-{d'}) (map_prod id undual F'_iter)" (is "?thesis1") and F'_start_le_F'_iter: "(XD_smallest ds X, dual (XH_largest ds X)) \ F'_iter" (is "?thesis2") proof %invisible - obtain P where XXX: "while_option (\A. F' A \ A) F' ((XD_smallest ds X), dual (XH_largest ds X)) = Some P" using while_option_finite_increasing_Some[OF F'_mono _ F'_start, simplified] by blast with while_option_stop2[OF XXX] fix_F'_stable_pair_on[where A=P] show ?thesis1 and ?thesis2 using funpow_mono2[OF F'_mono _ order.refl F'_start, where i=0] unfolding F'_iter_def while_def by auto qed lemma F'_iter_match_stable_on: shows "stable_on (ds-{d'}) F'_iter_match" by %invisible (rule stable_pair_on_stable_on) (metis F'_iter_stable_pair_on) theorem F'_iter_match_doctors_weakly_better_off: assumes "x \ Cd d X" assumes "d \ d'" shows "\y \ Cd d F'_iter_match. (x, y) \ Pd d" proof %invisible - from \stable_on ds X\ assms have "d \ ds" by (blast dest: Cd_Xd Cd_range' stable_on_Xd) with assms \stable_on ds X\ stable_on_stable_pair_on[OF \stable_on ds X\] have "\y\Cd d (XD_smallest ds X \ fst F'_iter). (x, y) \ Pd d" by - (rule Cd_mono; fastforce dest: X_XD_smallest_XH_largest stable_pair_on_Cd_match) with F'_iter_stable_pair_on F'_start_le_F'_iter have "\y\Cd d (fst F'_iter). (x, y) \ Pd d" by (metis Pair_le Un_absorb1 prod.collapse) with \d \ d'\ \d \ ds\ show ?thesis using stable_pair_on_Cd[OF F'_iter_stable_pair_on, symmetric, of d] by (subst Cd_domain[symmetric]) (simp add: Cd_idem) qed theorem F'_iter_match_hospitals_weakly_worse_off: assumes "x \ Ch h X" shows "x \ Ch h (F'_iter_match \ X)" proof %invisible - from F'_iter_stable_pair_on F'_start_le_F'_iter stable_on_stable_pair_on[OF \stable_on ds X\] X_subseteq_XH_largest[OF \stable_on ds X\] have "F'_iter_match \ X \ XH_largest ds X" by (simp add: less_eq_prod_def le_infI2 less_eq_dual_def) with assms Ch_range \stable_on ds X\ show ?thesis by - (rule iia_onD[OF Ch_iia, where B="XH_largest ds X"], auto, metis Ch_CH_irc_idem CH_XH_largest) qed text\ \citeauthor{HatfieldMilgrom:2005} observe but do not prove that @{const "F'_iter_match"} is not necessarily doctor-optimal wrt the new set of doctors, even if @{term "X"} was. These results seem incomplete. One might expect that the process of reacting to a doctor's retirement would involve considering new entrants to the workforce and allowing the set of possible contracts to be refined. There are also the questions of hospitals opening and closing. \ end end end subsection\ Theorems~8~and~9: A ``rural hospitals'' theorem \label{sec:contracts-rh} \ text\ Given that some hospitals are less desirable than others, the question arises of whether there is a mechanism that can redistribute doctors to under-resourced hospitals while retaining the stability of the match. Roth's @{emph \rural hospitals theorem\} \citep[Theorem~5.12]{RothSotomayor:1990} resolves this in the negative by showing that each doctor and hospital signs the same number of contracts in every stable match. In the context of contracts the theorem relies on the further hypothesis that hospital choices satisfy the law of aggregate demand (\S\ref{sec:cf-lad}). \ locale ContractsWithLAD = Contracts + assumes Ch_lad: "\h. lad (Ch h)" locale ContractsWithSubstitutesAndLAD = ContractsWithSubstitutes + ContractsWithLAD text\ We can use results that hold under @{const "irc"} by discharging that hypothesis against @{const "lad"} using the @{thm [source] "lad_on_substitutes_on_irc_on"} lemma. This is the effect of the following \sublocale\ command: \ sublocale ContractsWithSubstitutesAndLAD < ContractsWithSubstitutesAndIRC using Ch_range Ch_substitutes Ch_lad by unfold_locales (blast intro: lad_on_substitutes_on_irc_on f_range_onI) context ContractsWithSubstitutesAndLAD begin text\ The following results lead to \citet[Theorem~8]{HatfieldMilgrom:2005}, and the proofs go as they say. Again we state these with respect to an arbitrary solution to @{const "stable_pair"}. \ context fixes XD_XH :: "'a set \ 'a set" fixes ds :: "'b set" assumes "stable_pair_on ds XD_XH" begin lemma Cd_XD_gfp_F_card: assumes "d \ ds" shows "card (Cd d (fst XD_XH)) \ card (Cd d (fst (gfp_F ds)))" using %invisible assms Cd_lad XD_XH_gfp_F(1)[OF \stable_pair_on ds XD_XH\] unfolding lad_on_def by blast lemma Ch_gfp_F_XH_card: shows "card (Ch h (snd (gfp_F ds))) \ card (Ch h (snd XD_XH))" using %invisible Ch_lad XD_XH_gfp_F(2)[OF \stable_pair_on ds XD_XH\] unfolding lad_on_def by blast theorem Theorem_8: shows "d \ ds \ card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))" and "card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))" proof %invisible - let ?Sum_Cd_gfp = "\d\ds. card (Cd d (fst (gfp_F ds)))" let ?Sum_Ch_gfp = "\h\UNIV. card (Ch h (snd (gfp_F ds)))" let ?Sum_Cd_XD = "\d\ds. card (Cd d (fst XD_XH))" let ?Sum_Ch_XH = "\h\UNIV. card (Ch h (snd XD_XH))" have "?Sum_Cd_gfp = ?Sum_Ch_gfp" using stable_pair_on_CD_on_CH[OF gfp_F_stable_pair_on] CD_on_card[symmetric] CH_card[symmetric] by simp also have "\ \ ?Sum_Ch_XH" using Ch_gfp_F_XH_card by (simp add: sum_mono) also have "\ = ?Sum_Cd_XD" using stable_pair_on_CD_on_CH[OF \stable_pair_on ds XD_XH\] CD_on_card[symmetric] CH_card[symmetric] by simp finally have "?Sum_Cd_XD = ?Sum_Cd_gfp" using Cd_XD_gfp_F_card by (simp add: eq_iff sum_mono) with Cd_XD_gfp_F_card show "d \ ds \ card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))" by (fastforce elim: sum_mono_inv) have "?Sum_Ch_XH = ?Sum_Cd_XD" using stable_pair_on_CD_on_CH[OF \stable_pair_on ds XD_XH\] CD_on_card[symmetric] CH_card[symmetric] by simp also have "\ \ ?Sum_Cd_gfp" using Cd_XD_gfp_F_card by (simp add: sum_mono) also have "\ = ?Sum_Ch_gfp" using stable_pair_on_CD_on_CH[OF gfp_F_stable_pair_on] CD_on_card[symmetric] CH_card[symmetric] by simp finally have "?Sum_Ch_gfp = ?Sum_Ch_XH" using Ch_gfp_F_XH_card by (simp add: eq_iff sum_mono) with Ch_gfp_F_XH_card show "card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))" by (fastforce elim: sym[OF sum_mono_inv]) qed end text\ Their result may be more easily understood when phrased in terms of arbitrary stable matches: \ corollary rural_hospitals_theorem: assumes "stable_on ds X" assumes "stable_on ds Y" shows "d \ ds \ card (Cd d X) = card (Cd d Y)" and "card (Ch h X) = card (Ch h Y)" using %invisible assms T1[of ds X] T1[of ds Y] Theorem_8 stable_pair_on_Cd_match Ch_CH_irc_idem stable_pair_on_CH by force+ end text\ \citet[Theorem~9]{HatfieldMilgrom:2005} show that without @{const "lad"}, the rural hospitals theorem does not hold. Their proof does not seem to justify the theorem as stated (for instance, the contracts \x'\, \y'\ and \z'\ need not exist), and so we instead simply provide a counterexample (discovered by \verb!nitpick!) to the same effect. \ lemma (in ContractsWithSubstitutesAndIRC) Theorem_9_counterexample: assumes "stable_on ds Y" assumes "stable_on ds Z" shows "card (Ch h Y) = card (Ch h Z)" oops datatype X3 = Xd1 | Xd1' | Xd2 (*<*) lemma X3_UNIV: shows "UNIV = set [Xd1, Xd1', Xd2]" using X3.exhaust by auto lemmas X3_pow = subset_subseqs[OF subset_trans[OF subset_UNIV Set.equalityD1[OF X3_UNIV]]] instance X3 :: finite by standard (simp add: X3_UNIV) lemma X3_all_pow: shows "(\X''. P X'') \ (\X''\set ` set (subseqs [Xd1, Xd1', Xd2]). P X'')" using X3_pow by blast (*>*) primrec X3d :: "X3 \ D2" where "X3d Xd1 = D1" | "X3d Xd1' = D1" | "X3d Xd2 = D2" abbreviation X3h :: "X3 \ H1" where "X3h _ \ H" primrec PX3d :: "D2 \ X3 rel" where "PX3d D1 = linord_of_list [Xd1, Xd1']" | "PX3d D2 = linord_of_list [Xd2]" function CX3h :: "H1 \ X3 set \ X3 set" where "CX3h _ {Xd1} = {Xd1}" | "CX3h _ {Xd1'} = {Xd1'}" | "CX3h _ {Xd2} = {Xd2}" | "CX3h _ {Xd1, Xd1'} = {Xd1'}" | "CX3h _ {Xd1, Xd2} = {Xd1, Xd2}" | "CX3h _ {Xd1', Xd2} = {Xd1'}" | "CX3h _ {Xd1, Xd1', Xd2} = {Xd1'}" | "CX3h _ {} = {}" apply %invisible (case_tac x) apply (cut_tac X=b in X3_pow) apply auto done (*<*) termination by lexicographic_order lemma PX3d_linear: shows "Linear_order (PX3d d)" by (cases d) (simp_all add: linord_of_list_Linear_order) lemma PX3d_range: shows "Field (PX3d d) \ {x. X3d x = d}" by (cases d) simp_all lemma CX3h_range: shows "CX3h h X \ {x\X. X3h x = h}" by (cases "(h, X)" rule: CX3h.cases; simp; metis (mono_tags) H1.exhaust) lemma CX3h_singular: shows "inj_on X3d (CX3h h X)" by (cases "(h, X)" rule: CX3h.cases) auto lemma CX3h_substitutes: shows "substitutes (CX3h h)" apply (rule substitutes_onI) apply (cases h) apply (cut_tac X=B in X3_pow) apply (case_tac b) apply (case_tac [!] a) apply (auto simp: insert_commute) done lemma CX3h_irc: shows "irc (CX3h h)" apply (rule ircI) apply (cases h) apply (cut_tac X=B in X3_pow) apply (case_tac a) apply (auto simp: insert_commute) done (*>*) interpretation Theorem_9: ContractsWithSubstitutesAndIRC X3d X3h PX3d CX3h using %invisible PX3d_linear PX3d_range CX3h_range CX3h_singular CX3h_substitutes CX3h_irc by unfold_locales blast+ lemma Theorem_9_stable_Xd1': shows "Theorem_9.stable_on UNIV {Xd1'}" proof %invisible (rule Theorem_9.stable_onI) note image_cong_simp [cong del] note INF_cong_simp [cong] note SUP_cong_simp [cong] show "Theorem_9.individually_rational_on UNIV {Xd1'}" by (rule Theorem_9.individually_rational_onI) (simp_all add: D2_UNION Theorem_9.CD_on_def Theorem_9.CH_def) show "Theorem_9.stable_no_blocking_on UNIV {Xd1'}" apply (rule Theorem_9.stable_no_blocking_onI) apply (case_tac h) apply (cut_tac X=X'' in X3_pow) apply simp apply safe apply (simp_all add: insert_commute) done qed lemma Theorem_9_stable_Xd1_Xd2: shows "Theorem_9.stable_on UNIV {Xd1, Xd2}" proof %invisible (rule Theorem_9.stable_onI) note image_cong_simp [cong del] note INF_cong_simp [cong] note SUP_cong_simp [cong] show "Theorem_9.individually_rational_on UNIV {Xd1, Xd2}" by (rule Theorem_9.individually_rational_onI) (simp_all add: D2_UNION Theorem_9.CD_on_def Theorem_9.CH_def insert_commute) show "Theorem_9.stable_no_blocking_on UNIV {Xd1, Xd2}" apply (rule Theorem_9.stable_no_blocking_onI) apply (case_tac h) apply (cut_tac X=X'' in X3_pow) apply simp apply safe apply (simp_all add: D2_UNION Theorem_9.CD_on_def Theorem_9.maxR_def linord_of_list_linord_of_listP insert_commute) done qed text \ This violates the rural hospitals theorem: \ theorem shows "card (Theorem_9.CH {Xd1'}) \ card (Theorem_9.CH {Xd1, Xd2})" using %invisible Theorem_9_stable_Xd1' Theorem_9_stable_Xd1_Xd2 Theorem_9.stable_on_CH by simp text\ {\ldots}which is attributed to the failure of the hospitals' choice functions to satisfy @{const "lad"}: \ lemma CX3h_not_lad: shows "\lad (CX3h h)" unfolding %invisible lad_on_def apply (cases h) apply clarsimp apply (rule exI[where x="{Xd1, Xd1', Xd2}"]) apply (rule exI[where x="{Xd1, Xd2}"]) apply simp done text\ \citet{CiupanHatfieldKominers:2016} discuss an alternative approach to this result in a marriage market. \ subsection\ Theorems~15 and 16: Cumulative Offer Processes \label{sec:contracts-cop} \ text\ The goal of \citet[{\S}V]{HatfieldMilgrom:2005} is to connect this theory of contracts with matching to earlier work on auctions by the first of the authors, in particular by eliminating the @{const "substitutes"} hypothesis. They do so by defining a @{emph \cumulative offer process\} (COP): \ context Contracts begin definition cop_F_HM :: "'d set \ 'x set \ 'x set \ 'x set \ 'x set" where "cop_F_HM ds = (\(XD, XH). (- RH XH, XH \ CD_on ds (- RH XH)))" text\ Intuitively all of the doctors simultaneously offer their most preferred contracts that have yet to be rejected by the hospitals, and the hospitals choose amongst these and all that have been offered previously. Asking hospital choice functions to satisfy the @{const "substitutes"} condition effectively forces hospitals to consider only the contracts they have previously not rejected. This definition is neither monotonic nor increasing (i.e., it is not the case that @{term "\x. x \ cop_F_HM ds x"}). We rectify this by focusing on the second part of the definition. \ definition cop_F :: "'d set \ 'x set \ 'x set" where "cop_F ds XH = XH \ CD_on ds (- RH XH)" lemma cop_F_HM_cop_F: shows "cop_F_HM ds XD_XH = (- RH (snd XD_XH), cop_F ds (snd XD_XH))" unfolding cop_F_HM_def cop_F_def split_def by simp lemma cop_F_increasing: shows "x \ cop_F ds x" unfolding %invisible cop_F_def by simp text\ We have the following straightforward case distinction principles: \ lemma cop_F_cases: assumes "x \ cop_F ds fp" obtains (fp) "x \ fp" | (CD_on) "x \ CD_on ds (-RH fp) - fp" using assms unfolding cop_F_def by blast lemma CH_cop_F_cases: assumes "x \ CH (cop_F ds fp)" obtains (CH) "x \ CH fp" | (RH_fp) "x \ RH fp" | (CD_on) "x \ CD_on ds (-RH fp) - fp" using assms CH_range cop_F_def by auto text\ The existence of fixed points for our earlier definitions (\S\ref{sec:contracts-algorithmics}) was guaranteed by the Tarski-Knaster theorem, which relies on the monotonicity of the defining functional. As @{const "cop_F"} lacks this property, we appeal instead to the Bourbaki-Witt theorem for increasing functions. \ interpretation COP: bourbaki_witt_fixpoint Sup "{(x, y). x \ y}" "cop_F ds" for ds by %invisible (rule bourbaki_witt_fixpoint_complete_latticeI[OF cop_F_increasing]) definition fp_cop_F :: "'d set \ 'x set" where "fp_cop_F ds = COP.fixp_above ds {}" abbreviation "cop ds \ CH (fp_cop_F ds)" (*<*) lemmas fp_cop_F_unfold = COP.fixp_above_unfold[where a="{}", folded fp_cop_F_def, simplified Field_def, simplified] lemmas fp_cop_F_code = COP.fixp_above_conv_while[where a="{}", folded fp_cop_F_def, simplified Field_def, simplified] (*>*) text\ Given that the set of contracts is finite, we avoid continuity and admissibility issues; we have the following straightforward induction principle: \ lemma fp_cop_F_induct[case_names base step]: assumes "P {}" assumes "\fp. P fp \ P (cop_F ds fp)" shows "P (fp_cop_F ds)" using %invisible assms by (induct rule: COP.fixp_above_induct[where a="{}", folded fp_cop_F_def]) (fastforce intro: admissible_chfin)+ text\ An alternative is to use the @{const "while"} combinator, which is equivalent to the above by @{thm [source] COP.fixp_above_conv_while}. In any case, invariant reasoning is essential to verifying the properties of the COP, no matter how we phrase it. We develop a small program logic to ease the reuse of the invariants we prove. \ definition valid :: "'d set \ ('d set \ 'x set \ bool) \ ('d set \ 'x set \ bool) \ bool" where "valid ds P Q = (Q ds {} \ (\fp. P ds fp \ Q ds fp \ Q ds (cop_F ds fp)))" abbreviation invariant :: "'d set \ ('d set \ 'x set \ bool) \ bool" where "invariant ds P \ valid ds (\_ _. True) P" text\ Intuitively @{term "valid ds P Q"} asserts that the COP satisfies @{term "Q"} assuming that it satisfies @{term "P"}. This allows us to decompose our invariant proofs. By setting the precondition to @{term "True"}, @{term "invariant ds P"} captures the proof obligations of @{term "fp_cop_F_induct"} exactly. The following lemmas ease the syntactic manipulation of these facts. \ lemma validI[case_names base step]: assumes "Q ds {}" assumes "\fp. \P ds fp; Q ds fp\ \ Q ds (cop_F ds fp)" shows "valid ds P Q" using %invisible assms unfolding valid_def by blast lemma invariant_cop_FD: assumes "invariant ds P" assumes "P ds fp" shows "P ds (cop_F ds fp)" using %invisible assms unfolding valid_def by blast lemma invariantD: assumes "invariant ds P" shows "P ds (fp_cop_F ds)" using %invisible assms fp_cop_F_induct unfolding valid_def by blast lemma valid_pre: assumes "valid ds P' Q" assumes "\fp. P ds fp \ P' ds fp" shows "valid ds P Q" using %invisible assms unfolding valid_def by blast lemma valid_invariant: assumes "valid ds P Q" assumes "invariant ds P" shows "invariant ds (\ ds fp. P ds fp \ Q ds fp)" using %invisible assms unfolding valid_def by blast lemma valid_conj: assumes "valid ds (\ds fp. R ds fp \ P ds fp \ Q ds fp) P" assumes "valid ds (\ds fp. R ds fp \ P ds fp \ Q ds fp) Q" shows "valid ds R (\ ds fp. P ds fp \ Q ds fp)" using %invisible assms unfolding valid_def by blast end text (in ContractsWithSubstitutes) \ \citet[Theorem~15]{HatfieldMilgrom:2005} assert that @{const "fp_cop_F"} is equivalent to the doctor-offering algorithm @{const "gfp_F"}, assuming @{const "substitutes"}. (Note that the fixed points generated by increasing functions do not necessarily form a lattice, so there is not necessarily a hospital-optimal match, and indeed in general these do not exist.) Our proof is eased by the decomposition lemma @{thm [source] gfp_F_lfp_F} and the standard properties of fixed points in a lattice. \ context ContractsWithSubstitutes begin lemma lfp_F2_o_F1_fp_cop_F: shows "lfp (F2 ds \ F1) = fp_cop_F ds" proof(rule antisym) have "(F2 ds \ F1) (fp_cop_F ds) \ cop_F ds (fp_cop_F ds)" by (clarsimp simp: F2_def F1_def cop_F_def) then show "lfp (F2 ds \ F1) \ fp_cop_F ds" by (simp add: lfp_lowerbound fp_cop_F_unfold[symmetric]) next show "fp_cop_F ds \ lfp (F2 ds \ F1)" proof(induct rule: fp_cop_F_induct) case base then show ?case by simp next case (step fp) note IH = \fp \ lfp (F2 ds \ F1)\ then have "CD_on ds (- RH fp) \ lfp (F2 ds \ F1)" - by (subst lfp_unfold[OF F2_o_F1_mono]) - (metis (no_types, lifting) Compl_Diff_eq F1_antimono F2_antimono F1_def F2_def Un_subset_iff antimonoD comp_apply) + apply (subst lfp_unfold[OF F2_o_F1_mono]) + by (smt (verit, ccfv_SIG) Compl_iff Contracts.F1_def Contracts.F2_def Contracts_axioms DiffD2 + F2_o_F1_mono comp_eq_dest_lhs in_mono monoD subsetI) with IH show ?case unfolding cop_F_def by blast qed qed theorem Theorem_15: shows "gfp_F ds = (- RH (fp_cop_F ds), fp_cop_F ds)" using lfp_F2_o_F1_fp_cop_F unfolding gfp_F_lfp_F F1_def by simp theorem Theorem_15_match: shows "match (gfp_F ds) = CH (fp_cop_F ds)" using Theorem_15 by (fastforce dest: subsetD[OF CH_range]) end text\ \label{sec:contracts-codegen-fp_cop_F} With some auxiliary definitions, we can evaluate the COP on the example from \S\ref{sec:contracts-codegen-gfp_F}. \ (*<*) definition "P920_example_cop_F = P920_example.cop_F" definition "P920_example_fp_cop_F = P920_example.fp_cop_F" lemmas P920_example_cop_F_code[code] = P920_example.cop_F_def[folded P920_example_cop_F_def] lemmas P920_example_fp_cop_F_code[code] = P920_example.fp_cop_F_code[folded P920_example_fp_cop_F_def P920_example_cop_F_def] (*>*) lemma P920_example_fp_cop_F_value: shows "P920_example_CH (P920_example_fp_cop_F UNIV) = {(D1, H1), (D2, H2)}" by eval text\ \citet[Theorem~16]{HatfieldMilgrom:2005} assert that this process yields a stable match when we have a single hospital (now called an auctioneer) with unrestricted preferences. As before, this holds provided the auctioneer's preferences satisfy @{const "irc"}. We begin by establishing two obvious invariants of the COP that hold in general. \ context Contracts begin lemma %invisible CH_Ch_singular: assumes "(UNIV::'h set) = {h}" shows "CH A = Ch h A" unfolding CH_def using assms by auto definition cop_F_range_inv :: "'d set \ 'x set \ bool" where "cop_F_range_inv ds fp \ (\x\fp. x \ Field (Pd (Xd x)) \ Xd x \ ds)" definition cop_F_closed_inv :: "'d set \ 'x set \ bool" where "cop_F_closed_inv ds fp \ (\x\fp. above (Pd (Xd x)) x \ fp)" text\ The first, @{const "cop_F_range_inv"}, simply states that the result of the COP respects the structural conditions for doctors. The second @{const "cop_F_closed_inv"} states that the COP is upwards-closed with respect to the doctors' preferences. \ lemma cop_F_range_inv: shows "invariant ds cop_F_range_inv" unfolding valid_def cop_F_range_inv_def cop_F_def by (fastforce simp: mem_CD_on_Cd dest: Cd_range') lemma cop_F_closed_inv: shows "invariant ds cop_F_closed_inv" unfolding valid_def cop_F_closed_inv_def cop_F_def above_def by (clarsimp simp: subset_iff) (metis Cd_preferred ComplI Un_upper1 mem_CD_on_Cd subsetCE) lemmas fp_cop_F_range_inv = invariantD[OF cop_F_range_inv] lemmas fp_cop_F_range_inv' = fp_cop_F_range_inv[unfolded cop_F_range_inv_def, rule_format] lemmas fp_cop_F_closed_inv = invariantD[OF cop_F_closed_inv] lemmas fp_cop_F_closed_inv' = subsetD[OF bspec[OF invariantD[OF cop_F_closed_inv, unfolded cop_F_closed_inv_def, simplified]]] text\ The only challenge in showing that the COP yields a stable match is in establishing @{const "stable_no_blocking_on"}. Our key lemma states that that if @{const "CH"} rejects all contracts for doctor \d\ in @{const "fp_cop_F"}, then all contracts for \d\ are in @{const "fp_cop_F"}. \ lemma cop_F_RH: assumes "d \ ds" assumes "x \ Field (Pd d)" assumes "aboveS (Pd d) x \ RH fp" shows "x \ cop_F ds fp" using %invisible assms Pd_linear unfolding cop_F_def by (clarsimp simp: mem_CD_on_Cd Cd_greatest greatest_def aboveS_def order_on_defs total_on_def subset_iff) (metis Compl_Diff_eq Compl_iff Diff_iff IntE Pd_Xd refl_onD) lemma fp_cop_F_all: assumes "d \ ds" assumes "d \ Xd ` CH (fp_cop_F ds)" shows "Field (Pd d) \ fp_cop_F ds" proof %invisible (rule subsetI) fix x assume "x \ Field (Pd d)" from spec[OF Pd_linear] this finite[of "Pd d"] show "x \ fp_cop_F ds" proof(induct rule: finite_Linear_order_induct) case (step x) with assms Pd_range Pd_Xd cop_F_RH[of d ds _ "fp_cop_F ds", unfolded fp_cop_F_unfold[symmetric]] show ?case unfolding aboveS_def by (fastforce iff: image_iff) qed qed text\ \citet{AygunSonmez:2012-WP2} observe that any blocking contract must be weakly preferred by its doctor to anything in the outcome of the @{const "fp_cop_F"}: \ lemma fp_cop_F_preferred: assumes "y \ CD_on ds (CH (fp_cop_F ds) \ X'')" assumes "x \ CH (fp_cop_F ds)" assumes "Xd x = Xd y" shows "(x, y) \ Pd (Xd x)" using %invisible assms fp_cop_F_range_inv'[OF CH_range'[OF assms(2)]] Pd_Xd Pd_linear by (clarsimp simp: CD_on_def Cd_greatest greatest_def) (metis Int_iff Un_iff subset_refl underS_incl_iff) text\ The headline lemma cobbles these results together. \ lemma X''_closed: assumes "X'' \ CD_on ds (CH (fp_cop_F ds) \ X'')" shows "X'' \ fp_cop_F ds" proof(rule subsetI) fix x assume "x \ X''" show "x \ fp_cop_F ds" proof(cases "Xd x \ Xd ` CH (fp_cop_F ds)") case True then obtain y where "Xd y = Xd x" and "y \ CH (fp_cop_F ds)" by clarsimp with assms \x \ X''\ show ?thesis using CH_range fp_cop_F_closed_inv' fp_cop_F_preferred unfolding above_def by blast next case False with assms \x \ X''\ show ?thesis by (meson Cd_range' IntD2 fp_cop_F_all mem_CD_on_Cd rev_subsetD) qed qed text (in Contracts) \ The @{const "irc"} constraint on the auctioneer's preferences is needed for @{const "stable_no_blocking"} and their part of @{const "individually_rational"}. \ end context ContractsWithIRC begin lemma cop_stable_no_blocking_on: shows "stable_no_blocking_on ds (cop ds)" proof(rule stable_no_blocking_onI) fix h X'' assume C: "X'' = Ch h (CH (fp_cop_F ds) \ X'')" assume NE: "X'' \ Ch h (CH (fp_cop_F ds))" assume CD: "X'' \ CD_on ds (CH (fp_cop_F ds) \ X'')" from CD have "X'' \ fp_cop_F ds" by (rule X''_closed) then have X: "CH (fp_cop_F ds) \ X'' \ fp_cop_F ds" using CH_range by simp from C NE Ch_CH_irc_idem[of h] show False using consistency_onD[OF Ch_consistency _ X] CH_domain Ch_domain by blast qed theorem Theorem_16: assumes h: "(UNIV::'c set) = {h}" shows "stable_on ds (cop ds)" (is "stable_on ds ?fp") proof(rule stable_onI) show "individually_rational_on ds ?fp" proof(rule individually_rational_onI) from h have "allocation ?fp" by (simp add: Ch_singular CH_Ch_singular) then show "CD_on ds ?fp = ?fp" by (rule CD_on_closed) (blast dest: CH_range' fp_cop_F_range_inv') show "CH (CH (fp_cop_F ds)) = CH (fp_cop_F ds)" by (simp add: CH_irc_idem) qed show "stable_no_blocking_on ds ?fp" by (rule cop_stable_no_blocking_on) qed end subsection\ Concluding remarks \ text\ From \citet{HatfieldMilgrom:2005}, we have not shown Theorems~2, 7, 13 and~14, all of which are intended to position their results against prior work in this space. We delay establishing their strategic results (Theorems~10, 11 and~12) to \S\ref{sec:strategic}, after we have developed more useful invariants for the COP. By assuming \isa{irc}, \citet{AygunSonmez:2012-WP2} are essentially trading on Plott's path independence condition (\S\ref{sec:cf-path-independence}), as observed by \citet{ChambersYenmez:2013}. The latter show that these results generalize naturally to many-to-many matches, where doctors also use path-independent choice functions; see also \citet{Fleiner:2003}. For many applications, however, @{const "substitutes"} proves to be too strong a condition. The COP of \S\ref{sec:contracts-cop} provides a way forward, as we discuss in the next section. \ (*<*) end (*>*) diff --git a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy --- a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy +++ b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy @@ -1,1821 +1,1708 @@ (* Title: Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section\Relativization of the results about orders\ theory SML_Simple_Orders imports "../../Introduction" "../Foundations/SML_Relations" Complex_Main begin subsection\Class \<^class>\ord\\ subsubsection\Definitions and common properties\ locale ord_ow = fixes U :: "'ao set" and le :: "['ao, 'ao] \ bool" (infix \\\<^sub>o\<^sub>w\ 50) and ls :: "['ao, 'ao] \ bool" (infix \<\<^sub>o\<^sub>w\ 50) begin notation le (\'(\\<^sub>o\<^sub>w')\) and le (infix \\\<^sub>o\<^sub>w\ 50) and ls (\'(<\<^sub>o\<^sub>w')\) and ls (infix \<\<^sub>o\<^sub>w\ 50) abbreviation (input) ge (infix \\\<^sub>o\<^sub>w\ 50) where "x \\<^sub>o\<^sub>w y \ y \\<^sub>o\<^sub>w x" abbreviation (input) gt (infix \>\<^sub>o\<^sub>w\ 50) where "x >\<^sub>o\<^sub>w y \ y <\<^sub>o\<^sub>w x" notation ge (\'(\\<^sub>o\<^sub>w')\) and ge (infix \\\<^sub>o\<^sub>w\ 50) and gt (\'(>\<^sub>o\<^sub>w')\) and gt (infix \>\<^sub>o\<^sub>w\ 50) tts_register_sbts \(\\<^sub>o\<^sub>w)\ | U proof- assume "Domainp AOA = (\x. x \ U)" "bi_unique AOA" "right_total AOA" from tts_AA_eq_transfer[OF this] show ?thesis by auto qed tts_register_sbts \(<\<^sub>o\<^sub>w)\ | U proof- assume "Domainp AOA = (\x. x \ U)" "bi_unique AOA" "right_total AOA" from tts_AA_eq_transfer[OF this] show ?thesis by auto qed end locale ord_pair_ow = ord\<^sub>1: ord_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: ord_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 begin notation le\<^sub>1 (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and le\<^sub>1 (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and ls\<^sub>1 (\'(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and ls\<^sub>1 (infix \<\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and le\<^sub>2 (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and le\<^sub>2 (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) and ls\<^sub>2 (\'(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and ls\<^sub>2 (infix \<\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) notation ord\<^sub>1.ge (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and ord\<^sub>1.ge (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and ord\<^sub>1.gt (\'(>\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and ord\<^sub>1.gt (infix \>\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and ord\<^sub>2.ge (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and ord\<^sub>2.ge (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) and ord\<^sub>2.gt (\'(>\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and ord\<^sub>2.gt (infix \>\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) end ud \ord.lessThan\ (\(with _ : ({..<_}))\ [1000] 10) ud lessThan' \lessThan\ ud \ord.atMost\ (\(with _ : ({.._}))\ [1000] 10) ud atMost' \atMost\ ud \ord.greaterThan\ (\(with _ : ({_<..}))\ [1000] 10) ud greaterThan' \greaterThan\ ud \ord.atLeast\ (\(with _ : ({_..}))\ [1000] 10) ud atLeast' \atLeast\ ud \ord.greaterThanLessThan\ (\(with _ : ({_<..<_}))\ [1000, 999, 1000] 10) ud greaterThanLessThan' \greaterThanLessThan\ ud \ord.atLeastLessThan\ (\(with _ _ : ({_..<_}))\ [1000, 999, 1000, 1000] 10) ud atLeastLessThan' \atLeastLessThan\ ud \ord.greaterThanAtMost\ (\(with _ _ : ({_<.._}))\ [1000, 999, 1000, 999] 10) ud greaterThanAtMost' \greaterThanAtMost\ ud \ord.atLeastAtMost\ (\(with _ : ({_.._}))\ [1000, 1000, 1000] 10) ud atLeastAtMost' \atLeastAtMost\ ud \ord.min\ (\(with _ : \min\ _ _)\ [1000, 1000, 999] 10) ud min' \min\ ud \ord.max\ (\(with _ : \max\ _ _)\ [1000, 1000, 999] 10) ud max' \max\ ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (\x. x \ U)" and [transfer_rule]: "right_total A" trp (?'a A) in lessThan_ow: lessThan.with_def (\(on _ with _ : ({..<_}))\ [1000, 1000, 1000] 10) and atMost_ow: atMost.with_def (\(on _ with _ : ({.._}))\ [1000, 1000, 1000] 10) and greaterThan_ow: greaterThan.with_def (\(on _ with _: ({_<..}))\ [1000, 1000, 1000] 10) and atLeast_ow: atLeast.with_def (\(on _ with _ : ({_..}))\ [1000, 1000, 1000] 10) ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (\x. x \ U)" and [transfer_rule]: "bi_unique A" "right_total A" trp (?'a A) in greaterThanLessThan_ow: greaterThanLessThan.with_def (\(on _ with _ : ({_<..<_}))\ [1000, 1000, 1000, 1000] 10) and atLeastLessThan_ow: atLeastLessThan.with_def (\(on _ with _ _ : ({_..<_}))\ [1000, 1000, 999, 1000, 1000] 10) and greaterThanAtMost_ow: greaterThanAtMost.with_def (\(on _ with _ _ : ({_<.._}))\ [1000, 1000, 999, 1000, 1000] 10) and atLeastAtMost_ow: atLeastAtMost.with_def (\(on _ with _ : ({_.._}))\ [1000, 1000, 1000, 1000] 10) ctr parametricity in min_ow: min.with_def and max_ow: max.with_def context ord_ow begin abbreviation lessThan :: "'ao \ 'ao set" ("(1{..<\<^sub>o\<^sub>w_})") where "{..<\<^sub>o\<^sub>w u} \ on U with (<\<^sub>o\<^sub>w) : {.. 'ao set" ("(1{..\<^sub>o\<^sub>w_})") where "{..\<^sub>o\<^sub>w u} \ on U with (\\<^sub>o\<^sub>w) : {..u}" abbreviation greaterThan :: "'ao \ 'ao set" ("(1{_<\<^sub>o\<^sub>w..})") where "{l<\<^sub>o\<^sub>w..} \ on U with (<\<^sub>o\<^sub>w) : {l<..}" abbreviation atLeast :: "'ao \ 'ao set" ("(1{_..\<^sub>o\<^sub>w})") where "atLeast l \ on U with (\\<^sub>o\<^sub>w) : {l..}" abbreviation greaterThanLessThan :: "'ao \ 'ao \ 'ao set" ("(1{_<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>w_})") where "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} \ on U with (<\<^sub>o\<^sub>w) : {l<.. 'ao \ 'ao set" ("(1{_..<\<^sub>o\<^sub>w_})") where "{l..<\<^sub>o\<^sub>w u} \ on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l<..u}" abbreviation greaterThanAtMost :: "'ao \ 'ao \ 'ao set" ("(1{_<\<^sub>o\<^sub>w.._})") where "{l<\<^sub>o\<^sub>w..u} \ on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l<..u}" abbreviation atLeastAtMost :: "'ao \ 'ao \ 'ao set" ("(1{_..\<^sub>o\<^sub>w_})") where "{l..\<^sub>o\<^sub>wu} \ on U with (\\<^sub>o\<^sub>w) : {l..u}" abbreviation min :: "'ao \ 'ao \ 'ao" where "min \ min.with (\\<^sub>o\<^sub>w)" abbreviation max :: "'ao \ 'ao \ 'ao" where "max \ max.with (\\<^sub>o\<^sub>w)" end context ord_pair_ow begin notation ord\<^sub>1.lessThan ("(1{..<\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.atMost ("(1{..\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.greaterThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>1..})") notation ord\<^sub>1.atLeast ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>1})") notation ord\<^sub>1.greaterThanLessThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>1..<\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.atLeastLessThan ("(1{_..<\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.greaterThanAtMost ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>1.._})") notation ord\<^sub>1.atLeastAtMost ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>2.lessThan ("(1{..<\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.atMost ("(1{..\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.greaterThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>2..})") notation ord\<^sub>2.atLeast ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>2})") notation ord\<^sub>2.greaterThanLessThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>2..<\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.atLeastLessThan ("(1{_..<\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.greaterThanAtMost ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>2.._})") notation ord\<^sub>2.atLeastAtMost ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") end subsection\Preorders\ subsubsection\Definitions and common properties\ locale partial_preordering_ow = fixes U :: "'ao set" and le :: "'ao \ 'ao \ bool" (infix "\<^bold>\\<^sub>o\<^sub>w" 50) assumes refl: "a \ U \ a \<^bold>\\<^sub>o\<^sub>w a" and trans: "\ a \ U; b \ U; c \ U; a \<^bold>\\<^sub>o\<^sub>w b; b \<^bold>\\<^sub>o\<^sub>w c \ \ a \<^bold>\\<^sub>o\<^sub>w c" begin notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) end locale preordering_ow = partial_preordering_ow U le for U :: "'ao set" and le :: "'ao \ 'ao \ bool" (infix "\<^bold>\\<^sub>o\<^sub>w" 50) + fixes ls :: \'ao \ 'ao \ bool\ (infix "\<^bold><\<^sub>o\<^sub>w" 50) assumes strict_iff_not: "\ a \ U; b \ U \ \ a \<^bold><\<^sub>o\<^sub>w b \ a \<^bold>\\<^sub>o\<^sub>w b \ \ b \<^bold>\\<^sub>o\<^sub>w a" locale preorder_ow = ord_ow U le ls for U :: "'ao set" and le ls + assumes less_le_not_le: "\ x \ U; y \ U \ \ x <\<^sub>o\<^sub>w y \ x \\<^sub>o\<^sub>w y \ \ (y \\<^sub>o\<^sub>w x)" and order_refl[iff]: "x \ U \ x \\<^sub>o\<^sub>w x" and order_trans: "\ x \ U; y \ U; z \ U; x \\<^sub>o\<^sub>w y; y \\<^sub>o\<^sub>w z \ \ x \\<^sub>o\<^sub>w z" begin sublocale order: preordering_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ + dual_order: preordering_ow U \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ apply unfold_locales subgoal by auto subgoal by (meson order_trans) subgoal using less_le_not_le by simp subgoal by (meson order_trans) subgoal by (metis less_le_not_le) done end locale ord_preorder_ow = ord\<^sub>1: ord_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: preorder_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 begin sublocale ord_pair_ow . end locale preorder_pair_ow = ord\<^sub>1: preorder_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: preorder_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 and ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 and ls\<^sub>2 begin sublocale ord_preorder_ow .. end ud \preordering_bdd.bdd\ ud \preorder.bdd_above\ ud bdd_above' \bdd_above\ ud \preorder.bdd_below\ ud bdd_below' \bdd_below\ ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (\x. x \ U)" and [transfer_rule]: "right_total A" trp (?'a A) in bdd_ow: bdd.with_def (\(on _ with _ : \bdd\ _)\ [1000, 1000, 1000] 10) and bdd_above_ow: bdd_above.with_def (\(on _ with _ : \bdd'_above\ _)\ [1000, 1000, 1000] 10) and bdd_below_ow: bdd_below.with_def (\(on _ with _ : \bdd'_below\ _)\ [1000, 1000, 1000] 10) declare bdd.with[ud_with del] context preorder_ow begin abbreviation bdd_above :: "'ao set \ bool" where "bdd_above \ bdd_above_ow U (\\<^sub>o\<^sub>w)" abbreviation bdd_below :: "'ao set \ bool" where "bdd_below \ bdd_below_ow U (\\<^sub>o\<^sub>w)" end subsubsection\Transfer rules\ context includes lifting_syntax begin lemma partial_preordering_transfer[transfer_rule]: assumes [transfer_rule]: "right_total A" shows "((A ===> A ===> (=)) ===> (=)) (partial_preordering_ow (Collect (Domainp A))) partial_preordering" unfolding partial_preordering_ow_def partial_preordering_def apply transfer_prover_start apply transfer_step+ by blast lemma preordering_transfer[transfer_rule]: assumes [transfer_rule]: "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (preordering_ow (Collect (Domainp A))) preordering" unfolding preordering_ow_def preordering_ow_axioms_def preordering_def preordering_axioms_def apply transfer_prover_start apply transfer_step+ by blast lemma preorder_transfer[transfer_rule]: assumes [transfer_rule]: "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (preorder_ow (Collect (Domainp A))) class.preorder" unfolding preorder_ow_def class.preorder_def apply transfer_prover_start apply transfer_step+ by blast end subsubsection\Relativization\ context preordering_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting preordering_ow_axioms eliminating through auto begin tts_lemma strict_implies_order: assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" shows "a \<^bold>\\<^sub>o\<^sub>w b" is preordering.strict_implies_order. tts_lemma irrefl: assumes "a \ U" shows "\a \<^bold><\<^sub>o\<^sub>w a" is preordering.irrefl. tts_lemma asym: assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w a" shows False is preordering.asym. tts_lemma strict_trans1: assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold>\\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w c" shows "a \<^bold><\<^sub>o\<^sub>w c" is preordering.strict_trans1. tts_lemma strict_trans2: assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold>\\<^sub>o\<^sub>w c" shows "a \<^bold><\<^sub>o\<^sub>w c" is preordering.strict_trans2. tts_lemma strict_trans: assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w c" shows "a \<^bold><\<^sub>o\<^sub>w c" is preordering.strict_trans. end end context preorder_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting preorder_ow_axioms eliminating through auto begin tts_lemma less_irrefl: assumes "x \ U" shows "\ x <\<^sub>o\<^sub>w x" is preorder_class.less_irrefl. tts_lemma bdd_below_Ioc: assumes "a \ U" and "b \ U" shows "bdd_below {a<\<^sub>o\<^sub>w..b}" is preorder_class.bdd_below_Ioc. tts_lemma bdd_above_Ioc: assumes "a \ U" and "b \ U" shows "bdd_above {a<\<^sub>o\<^sub>w..b}" is preorder_class.bdd_above_Ioc. tts_lemma bdd_above_Iic: assumes "b \ U" shows "bdd_above {..\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Iic. tts_lemma bdd_above_Iio: assumes "b \ U" shows "bdd_above {..<\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Iio. tts_lemma bdd_below_Ici: assumes "a \ U" shows "bdd_below {a..\<^sub>o\<^sub>w}" is preorder_class.bdd_below_Ici. tts_lemma bdd_below_Ioi: assumes "a \ U" shows "bdd_below {a<\<^sub>o\<^sub>w..}" is preorder_class.bdd_below_Ioi. tts_lemma bdd_above_Icc: assumes "a \ U" and "b \ U" shows "bdd_above {a..\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Icc. tts_lemma bdd_above_Ioo: assumes "a \ U" and "b \ U" shows "bdd_above {a<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Ioo. tts_lemma bdd_below_Icc: assumes "a \ U" and "b \ U" shows "bdd_below {a..\<^sub>o\<^sub>wb}" is preorder_class.bdd_below_Icc. tts_lemma bdd_below_Ioo: assumes "a \ U" and "b \ U" shows "bdd_below {a<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wb}" is preorder_class.bdd_below_Ioo. tts_lemma bdd_above_Ico: assumes "a \ U" and "b \ U" shows "bdd_above (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. U" and "b \ U" shows "bdd_below (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. U" shows "{a<\<^sub>o\<^sub>w..} \ {a..\<^sub>o\<^sub>w}" is preorder_class.Ioi_le_Ico. tts_lemma eq_refl: assumes "y \ U" and "x = y" shows "x \\<^sub>o\<^sub>w y" is preorder_class.eq_refl. tts_lemma less_imp_le: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "x \\<^sub>o\<^sub>w y" is preorder_class.less_imp_le. tts_lemma less_not_sym: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "\ y <\<^sub>o\<^sub>w x" is preorder_class.less_not_sym. tts_lemma less_imp_not_less: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(\ y <\<^sub>o\<^sub>w x) = True" is preorder_class.less_imp_not_less. tts_lemma less_asym': assumes "a \ U" and "b \ U" and "a <\<^sub>o\<^sub>w b" and "b <\<^sub>o\<^sub>w a" shows P is preorder_class.less_asym'. tts_lemma less_imp_triv: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(y <\<^sub>o\<^sub>w x \ P) = True" is preorder_class.less_imp_triv. tts_lemma less_trans: assumes "x \ U" and "y \ U" and "z \ U" and "x <\<^sub>o\<^sub>w y" and "y <\<^sub>o\<^sub>w z" shows "x <\<^sub>o\<^sub>w z" is preorder_class.less_trans. tts_lemma less_le_trans: assumes "x \ U" and "y \ U" and "z \ U" and "x <\<^sub>o\<^sub>w y" and "y \\<^sub>o\<^sub>w z" shows "x <\<^sub>o\<^sub>w z" is preorder_class.less_le_trans. tts_lemma le_less_trans: assumes "x \ U" and "y \ U" and "z \ U" and "x \\<^sub>o\<^sub>w y" and "y <\<^sub>o\<^sub>w z" shows "x <\<^sub>o\<^sub>w z" is preorder_class.le_less_trans. tts_lemma bdd_aboveI: assumes "A \ U" and "M \ U" and "\x. \x \ U; x \ A\ \ x \\<^sub>o\<^sub>w M" shows "bdd_above A" is preorder_class.bdd_aboveI. tts_lemma bdd_belowI: assumes "A \ U" and "m \ U" and "\x. \x \ U; x \ A\ \ m \\<^sub>o\<^sub>w x" shows "bdd_below A" is preorder_class.bdd_belowI. tts_lemma less_asym: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" and "\ P \ y <\<^sub>o\<^sub>w x" shows P is preorder_class.less_asym. tts_lemma transp_less: "transp_on U (<\<^sub>o\<^sub>w)" is preorder_class.transp_less. tts_lemma transp_le: "transp_on U (\\<^sub>o\<^sub>w)" is preorder_class.transp_le. tts_lemma transp_gr: "transp_on U (\x y. y <\<^sub>o\<^sub>w x)" is preorder_class.transp_gr. tts_lemma transp_ge: "transp_on U (\x y. y \\<^sub>o\<^sub>w x)" is preorder_class.transp_ge. tts_lemma bdd_above_Int1: assumes "A \ U" and "B \ U" and "bdd_above A" shows "bdd_above (A \ B)" is preorder_class.bdd_above_Int1. tts_lemma bdd_above_Int2: assumes "B \ U" and "A \ U" and "bdd_above B" shows "bdd_above (A \ B)" is preorder_class.bdd_above_Int2. tts_lemma bdd_below_Int1: assumes "A \ U" and "B \ U" and "bdd_below A" shows "bdd_below (A \ B)" is preorder_class.bdd_below_Int1. tts_lemma bdd_below_Int2: assumes "B \ U" and "A \ U" and "bdd_below B" shows "bdd_below (A \ B)" is preorder_class.bdd_below_Int2. tts_lemma bdd_above_mono: assumes "B \ U" and "bdd_above B" and "A \ B" shows "bdd_above A" is preorder_class.bdd_above_mono. tts_lemma bdd_below_mono: assumes "B \ U" and "bdd_below B" and "A \ B" shows "bdd_below A" is preorder_class.bdd_below_mono. tts_lemma atLeastAtMost_subseteq_atLeastLessThan_iff: assumes "a \ U" and "b \ U" and "c \ U" and "d \ U" shows "({a..\<^sub>o\<^sub>wb} \ (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {c..\<^sub>o\<^sub>w b \ b <\<^sub>o\<^sub>w d \ c \\<^sub>o\<^sub>w a)" is preorder_class.atLeastAtMost_subseteq_atLeastLessThan_iff. tts_lemma atMost_subset_iff: assumes "x \ U" and "y \ U" shows "({..\<^sub>o\<^sub>wx} \ {..\<^sub>o\<^sub>wy}) = (x \\<^sub>o\<^sub>w y)" is Set_Interval.atMost_subset_iff. tts_lemma single_Diff_lessThan: assumes "k \ U" shows "{k} - {..<\<^sub>o\<^sub>wk} = {k}" is Set_Interval.single_Diff_lessThan. tts_lemma atLeast_subset_iff: assumes "x \ U" and "y \ U" shows "({x..\<^sub>o\<^sub>w} \ {y..\<^sub>o\<^sub>w}) = (y \\<^sub>o\<^sub>w x)" is Set_Interval.atLeast_subset_iff. tts_lemma atLeastatMost_psubset_iff: assumes "a \ U" and "b \ U" and "c \ U" and "d \ U" shows "({a..\<^sub>o\<^sub>wb} \ {c..\<^sub>o\<^sub>wd}) = (c \\<^sub>o\<^sub>w d \ (\ a \\<^sub>o\<^sub>w b \ c \\<^sub>o\<^sub>w a \ b \\<^sub>o\<^sub>w d \ (c <\<^sub>o\<^sub>w a \ b <\<^sub>o\<^sub>w d)))" is preorder_class.atLeastatMost_psubset_iff. tts_lemma not_empty_eq_Iic_eq_empty: assumes "h \ U" shows "{} \ {..\<^sub>o\<^sub>wh}" is preorder_class.not_empty_eq_Iic_eq_empty. tts_lemma atLeastatMost_subset_iff: assumes "a \ U" and "b \ U" and "c \ U" and "d \ U" shows "({a..\<^sub>o\<^sub>wb} \ {c..\<^sub>o\<^sub>wd}) = (\ a \\<^sub>o\<^sub>w b \ b \\<^sub>o\<^sub>w d \ c \\<^sub>o\<^sub>w a)" is preorder_class.atLeastatMost_subset_iff. tts_lemma Icc_subset_Ici_iff: assumes "l \ U" and "h \ U" and "l' \ U" shows "({l..\<^sub>o\<^sub>wh} \ {l'..\<^sub>o\<^sub>w}) = (\ l \\<^sub>o\<^sub>w h \ l' \\<^sub>o\<^sub>w l)" is preorder_class.Icc_subset_Ici_iff. tts_lemma Icc_subset_Iic_iff: assumes "l \ U" and "h \ U" and "h' \ U" shows "({l..\<^sub>o\<^sub>wh} \ {..\<^sub>o\<^sub>wh'}) = (\ l \\<^sub>o\<^sub>w h \ h \\<^sub>o\<^sub>w h')" is preorder_class.Icc_subset_Iic_iff. tts_lemma not_empty_eq_Ici_eq_empty: assumes "l \ U" shows "{} \ {l..\<^sub>o\<^sub>w}" is preorder_class.not_empty_eq_Ici_eq_empty. tts_lemma not_Ici_eq_empty: assumes "l \ U" shows "{l..\<^sub>o\<^sub>w} \ {}" is preorder_class.not_Ici_eq_empty. tts_lemma not_Iic_eq_empty: assumes "h \ U" shows "{..\<^sub>o\<^sub>wh} \ {}" is preorder_class.not_Iic_eq_empty. tts_lemma atLeastatMost_empty_iff2: assumes "a \ U" and "b \ U" shows "({} = {a..\<^sub>o\<^sub>wb}) = (\ a \\<^sub>o\<^sub>w b)" is preorder_class.atLeastatMost_empty_iff2. tts_lemma atLeastLessThan_empty_iff2: assumes "a \ U" and "b \ U" shows "({} = (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. a <\<^sub>o\<^sub>w b)" is preorder_class.atLeastLessThan_empty_iff2. tts_lemma greaterThanAtMost_empty_iff2: assumes "k \ U" and "l \ U" shows "({} = {k<\<^sub>o\<^sub>w..l}) = (\ k <\<^sub>o\<^sub>w l)" is preorder_class.greaterThanAtMost_empty_iff2. tts_lemma atLeastatMost_empty_iff: assumes "a \ U" and "b \ U" shows "({a..\<^sub>o\<^sub>wb} = {}) = (\ a \\<^sub>o\<^sub>w b)" is preorder_class.atLeastatMost_empty_iff. tts_lemma atLeastLessThan_empty_iff: assumes "a \ U" and "b \ U" shows "((on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. a <\<^sub>o\<^sub>w b)" is preorder_class.atLeastLessThan_empty_iff. tts_lemma greaterThanAtMost_empty_iff: assumes "k \ U" and "l \ U" shows "({k<\<^sub>o\<^sub>w..l} = {}) = (\ k <\<^sub>o\<^sub>w l)" is preorder_class.greaterThanAtMost_empty_iff. end tts_context tts: (?'a to U) substituting preorder_ow_axioms begin tts_lemma bdd_above_empty: assumes "U \ {}" shows "bdd_above {}" is preorder_class.bdd_above_empty. tts_lemma bdd_below_empty: assumes "U \ {}" shows "bdd_below {}" is preorder_class.bdd_below_empty. end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'a set\) rewriting ctr_simps substituting preorder_ow_axioms eliminating through (auto intro: bdd_above_empty bdd_below_empty) begin tts_lemma bdd_belowI2: assumes "A \ U\<^sub>2" and "m \ U" and "\x\U\<^sub>2. f x \ U" and "\x. x \ A \ m \\<^sub>o\<^sub>w f x" shows "bdd_below (f ` A)" given preorder_class.bdd_belowI2 by blast tts_lemma bdd_aboveI2: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "M \ U" and "\x. x \ A \ f x \\<^sub>o\<^sub>w M" shows "bdd_above (f ` A)" given preorder_class.bdd_aboveI2 by blast end end subsection\Partial orders\ subsubsection\Definitions and common properties\ locale ordering_ow = partial_preordering_ow U le for U :: "'ao set" and le :: "'ao \ 'ao \ bool" (infix "\<^bold>\\<^sub>o\<^sub>w" 50) + fixes ls :: "'ao \ 'ao \ bool" (infix "\<^bold><\<^sub>o\<^sub>w" 50) assumes strict_iff_order: "\ a \ U; b \ U \ \ a \<^bold><\<^sub>o\<^sub>w b \ a \<^bold>\\<^sub>o\<^sub>w b \ a \ b" and antisym: "\ a \ U; b \ U; a \<^bold>\\<^sub>o\<^sub>w b; b \<^bold>\\<^sub>o\<^sub>w a \ \ a = b" begin notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) sublocale preordering_ow U \(\<^bold>\\<^sub>o\<^sub>w)\ \(\<^bold><\<^sub>o\<^sub>w)\ using local.antisym strict_iff_order by unfold_locales blast end locale order_ow = preorder_ow U le ls for U :: "'ao set" and le ls + assumes antisym: "\ x \ U; y \ U; x \\<^sub>o\<^sub>w y; y \\<^sub>o\<^sub>w x \ \ x = y" begin sublocale order: ordering_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ + dual_order: ordering_ow U \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ apply unfold_locales subgoal by (force simp: less_le_not_le antisym) subgoal by (simp add: antisym) subgoal by (force simp: less_le_not_le antisym) subgoal by (simp add: antisym) done no_notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) end locale ord_order_ow = ord\<^sub>1: ord_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 sublocale ord_order_ow \ ord_preorder_ow .. locale preorder_order_ow = ord\<^sub>1: preorder_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 sublocale preorder_order_ow \ preorder_pair_ow .. locale order_pair_ow = ord\<^sub>1: order_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 sublocale order_pair_ow \ preorder_order_ow .. -definition mono where - "mono f \ (\x y. x \ y \ f x \ f y)" - -definition strict_mono where - "strict_mono f \ (\x y. x < y \ f x < f y)" - -lemma mono_iff_mono: "mono f \ Fun.mono f" - by (simp add: mono_def Fun.mono_def) - -ud \mono\ (\(with _ _ : \mono\ _)\ [1000, 999, 1000] 10) -ud \strict_mono\ (\(with _ _ : \strict'_mono\ _)\ [1000, 999, 1000] 10) -ud \order.antimono\ (\(with _ _ : \strict'_mono\ _)\ [1000, 999, 1000] 10) -ud antimono' \antimono\ ud \monoseq\ (\(with _ : \monoseq\ _)\ [1000, 1000] 10) ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp (B::'c\'d\bool) = (\x. x \ U\<^sub>2)" and [transfer_rule]: "right_total B" trp (?'b \A::'a\'b\bool\) and (?'a B) - in mono_ow: mono.with_def - (\(on _ with _ _ : \mono\ _)\ [1000, 1000, 999, 1000] 10) - and strict_mono_ow: strict_mono.with_def - (\(on _ with _ _ : \strict'_mono\ _)\ [1000, 1000, 999, 1000] 10) - and antimono_ow: antimono.with_def - (\(on _ with _ _ : \antimono\ _)\ [1000, 1000, 999, 1000] 10) - and monoseq_ow: monoseq.with_def + in monoseq_ow: monoseq.with_def subsubsection\Transfer rules\ context includes lifting_syntax begin lemma ordering_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (ordering_ow (Collect (Domainp A))) ordering" unfolding ordering_ow_def ordering_ow_axioms_def ordering_def ordering_axioms_def apply transfer_prover_start apply transfer_step+ unfolding Ball_Collect[symmetric] by (intro ext HOL.arg_cong2[where f="(\)"]) auto lemma order_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (order_ow (Collect (Domainp A))) class.order" unfolding order_ow_def class.order_def order_ow_axioms_def class.order_axioms_def apply transfer_prover_start apply transfer_step+ by simp end subsubsection\Relativization\ context ordering_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting ordering_ow_axioms eliminating through simp begin tts_lemma strict_implies_not_eq: assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" shows "a \ b" is ordering.strict_implies_not_eq. tts_lemma order_iff_strict: assumes "a \ U" and "b \ U" shows "(a \<^bold>\\<^sub>o\<^sub>w b) = (a \<^bold><\<^sub>o\<^sub>w b \ a = b)" is ordering.order_iff_strict. tts_lemma not_eq_order_implies_strict: assumes "a \ U" and "b \ U" and "a \ b" and "a \<^bold>\\<^sub>o\<^sub>w b" shows "a \<^bold><\<^sub>o\<^sub>w b" is ordering.not_eq_order_implies_strict. tts_lemma eq_iff: assumes "a \ U" and "b \ U" shows "(a = b) = (a \<^bold>\\<^sub>o\<^sub>w b \ b \<^bold>\\<^sub>o\<^sub>w a)" is ordering.eq_iff. end end context order_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting order_ow_axioms eliminating through clarsimp begin tts_lemma atLeastAtMost_singleton: assumes "a \ U" shows "{a..\<^sub>o\<^sub>wa} = {a}" is order_class.atLeastAtMost_singleton. tts_lemma less_imp_neq: assumes "y \ U" and "x <\<^sub>o\<^sub>w y" shows "x \ y" is order_class.less_imp_neq. tts_lemma atLeastatMost_empty: assumes "b \ U" and "a \ U" and "b <\<^sub>o\<^sub>w a" shows "{a..\<^sub>o\<^sub>wb} = {}" is order_class.atLeastatMost_empty. tts_lemma less_imp_not_eq: assumes "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(x = y) = False" is order_class.less_imp_not_eq. tts_lemma less_imp_not_eq2: assumes "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(y = x) = False" is order_class.less_imp_not_eq2. tts_lemma atLeastLessThan_empty: assumes "b \ U" and "a \ U" and "b \\<^sub>o\<^sub>w a" shows "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. U" and "k \ U" and "l \\<^sub>o\<^sub>w k" shows "{k<\<^sub>o\<^sub>w..l} = {}" is order_class.greaterThanAtMost_empty. tts_lemma antisym_conv1: assumes "x \ U" and "y \ U" and "\ x <\<^sub>o\<^sub>w y" shows "(x \\<^sub>o\<^sub>w y) = (x = y)" is order_class.antisym_conv1. tts_lemma antisym_conv2: assumes "x \ U" and "y \ U" and "x \\<^sub>o\<^sub>w y" shows "(\ x <\<^sub>o\<^sub>w y) = (x = y)" is order_class.antisym_conv2. tts_lemma greaterThanLessThan_empty: assumes "l \ U" and "k \ U" and "l \\<^sub>o\<^sub>w k" shows "{k<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wl} = {}" is order_class.greaterThanLessThan_empty. tts_lemma atLeastLessThan_eq_atLeastAtMost_diff: assumes "a \ U" and "b \ U" shows "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a..o\<^sub>wb} - {b}" is order_class.atLeastLessThan_eq_atLeastAtMost_diff. tts_lemma greaterThanAtMost_eq_atLeastAtMost_diff: assumes "a \ U" and "b \ U" shows "{a<\<^sub>o\<^sub>w..b} = {a..\<^sub>o\<^sub>wb} - {a}" is order_class.greaterThanAtMost_eq_atLeastAtMost_diff. tts_lemma less_separate: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "\x'\U. \y'\U. x \ {..<\<^sub>o\<^sub>wx'} \ y \ {y'<\<^sub>o\<^sub>w..} \ {..<\<^sub>o\<^sub>wx'} \ {y'<\<^sub>o\<^sub>w..} = {}" is order_class.less_separate. tts_lemma order_iff_strict: assumes "a \ U" and "b \ U" shows "(a \\<^sub>o\<^sub>w b) = (a <\<^sub>o\<^sub>w b \ a = b)" is order_class.order.order_iff_strict. tts_lemma le_less: assumes "x \ U" and "y \ U" shows "(x \\<^sub>o\<^sub>w y) = (x <\<^sub>o\<^sub>w y \ x = y)" is order_class.le_less. tts_lemma strict_iff_order: assumes "a \ U" and "b \ U" shows "(a <\<^sub>o\<^sub>w b) = (a \\<^sub>o\<^sub>w b \ a \ b)" is order_class.order.strict_iff_order. tts_lemma less_le: assumes "x \ U" and "y \ U" shows "(x <\<^sub>o\<^sub>w y) = (x \\<^sub>o\<^sub>w y \ x \ y)" is order_class.less_le. tts_lemma atLeastAtMost_singleton': assumes "b \ U" and "a = b" shows "{a..\<^sub>o\<^sub>wb} = {a}" is order_class.atLeastAtMost_singleton'. tts_lemma le_imp_less_or_eq: assumes "x \ U" and "y \ U" and "x \\<^sub>o\<^sub>w y" shows "x <\<^sub>o\<^sub>w y \ x = y" is order_class.le_imp_less_or_eq. tts_lemma antisym_conv: assumes "y \ U" and "x \ U" and "y \\<^sub>o\<^sub>w x" shows "(x \\<^sub>o\<^sub>w y) = (x = y)" is order_class.antisym_conv. tts_lemma le_neq_trans: assumes "a \ U" and "b \ U" and "a \\<^sub>o\<^sub>w b" and "a \ b" shows "a <\<^sub>o\<^sub>w b" is order_class.le_neq_trans. tts_lemma neq_le_trans: assumes "a \ U" and "b \ U" and "a \ b" and "a \\<^sub>o\<^sub>w b" shows "a <\<^sub>o\<^sub>w b" is order_class.neq_le_trans. tts_lemma Iio_Int_singleton: assumes "k \ U" and "x \ U" shows "{..<\<^sub>o\<^sub>wk} \ {x} = (if x <\<^sub>o\<^sub>w k then {x} else {})" is order_class.Iio_Int_singleton. tts_lemma atLeastAtMost_singleton_iff: assumes "a \ U" and "b \ U" and "c \ U" shows "({a..\<^sub>o\<^sub>wb} = {c}) = (a = b \ b = c)" is order_class.atLeastAtMost_singleton_iff. tts_lemma Icc_eq_Icc: assumes "l \ U" and "h \ U" and "l' \ U" and "h' \ U" shows "({l..\<^sub>o\<^sub>wh} = {l'..\<^sub>o\<^sub>wh'}) = (h = h' \ l = l' \ \ l' \\<^sub>o\<^sub>w h' \ \ l \\<^sub>o\<^sub>w h)" is order_class.Icc_eq_Icc. tts_lemma lift_Suc_mono_less_iff: assumes "range f \ U" and "\n. f n <\<^sub>o\<^sub>w f (Suc n)" shows "(f n <\<^sub>o\<^sub>w f m) = (n < m)" is order_class.lift_Suc_mono_less_iff. tts_lemma lift_Suc_mono_less: assumes "range f \ U" and "\n. f n <\<^sub>o\<^sub>w f (Suc n)" and "n < n'" shows "f n <\<^sub>o\<^sub>w f n'" is order_class.lift_Suc_mono_less. tts_lemma lift_Suc_mono_le: assumes "range f \ U" and "\n. f n \\<^sub>o\<^sub>w f (Suc n)" and "n \ n'" shows "f n \\<^sub>o\<^sub>w f n'" is order_class.lift_Suc_mono_le. tts_lemma lift_Suc_antimono_le: assumes "range f \ U" and "\n. f (Suc n) \\<^sub>o\<^sub>w f n" and "n \ n'" shows "f n' \\<^sub>o\<^sub>w f n" is order_class.lift_Suc_antimono_le. tts_lemma ivl_disj_int_two: assumes "l \ U" and "m \ U" and "u \ U" shows "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wm} \ (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {m..o\<^sub>w..m} \ {m<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} = {}" "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l.. (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {m..o\<^sub>wm} \ {m<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} = {}" "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wm} \ {m..\<^sub>o\<^sub>wu} = {}" "{l<\<^sub>o\<^sub>w..m} \ {m<\<^sub>o\<^sub>w..u} = {}" "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l.. {m..\<^sub>o\<^sub>wu} = {}" "{l..\<^sub>o\<^sub>wm} \ {m<\<^sub>o\<^sub>w..u} = {}" is Set_Interval.ivl_disj_int_two. tts_lemma ivl_disj_int_one: assumes "l \ U" and "u \ U" shows "{..\<^sub>o\<^sub>wl} \ {l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} = {}" "{..<\<^sub>o\<^sub>wl} \ (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l..o\<^sub>wl} \ {l<\<^sub>o\<^sub>w..u} = {}" "{..<\<^sub>o\<^sub>wl} \ {l..\<^sub>o\<^sub>wu} = {}" "{l<\<^sub>o\<^sub>w..u} \ {u<\<^sub>o\<^sub>w..} = {}" "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} \ {u..\<^sub>o\<^sub>w} = {}" "{l..\<^sub>o\<^sub>wu} \ {u<\<^sub>o\<^sub>w..} = {}" "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l.. {u..\<^sub>o\<^sub>w} = {}" is Set_Interval.ivl_disj_int_one. tts_lemma min_absorb2: assumes "y \ U" and "x \ U" and "y \\<^sub>o\<^sub>w x" shows "local.min x y = y" is Orderings.min_absorb2. tts_lemma max_absorb1: assumes "y \ U" and "x \ U" and "y \\<^sub>o\<^sub>w x" shows "local.max x y = x" is Orderings.max_absorb1. - -tts_lemma decseq_imp_monoseq: - assumes "range X \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ X" - shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" - is Topological_Spaces.decseq_imp_monoseq. - -tts_lemma decseq_Suc_iff: - assumes "range f \ U" - shows "(on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ f) = (\x. f (Suc x) \\<^sub>o\<^sub>w f x)" - is Topological_Spaces.decseq_Suc_iff. - -tts_lemma decseq_const: - assumes "k \ U" - shows "on (UNIV::nat set) with (\\<^sub>o\<^sub>w) (\) : \antimono\ (\x. k)" - is Topological_Spaces.decseq_const. tts_lemma atMost_Int_atLeast: assumes "n \ U" shows "{..\<^sub>o\<^sub>wn} \ {n..\<^sub>o\<^sub>w} = {n}" is Set_Interval.atMost_Int_atLeast. tts_lemma monoseq_Suc: assumes "range X \ U" shows "(with (\\<^sub>o\<^sub>w) : \monoseq\ X) = ((\x. X x \\<^sub>o\<^sub>w X (Suc x)) \ (\x. X (Suc x) \\<^sub>o\<^sub>w X x))" is Topological_Spaces.monoseq_Suc. -tts_lemma decseq_SucI: - assumes "range X \ U" and "\n. X (Suc n) \\<^sub>o\<^sub>w X n" - shows "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ X" - is Topological_Spaces.decseq_SucI. - -tts_lemma decseq_SucD: - assumes "range A \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ A" - shows "A (Suc i) \\<^sub>o\<^sub>w A i" - is Topological_Spaces.decseq_SucD. - tts_lemma mono_SucI2: assumes "range X \ U" and "\x. X (Suc x) \\<^sub>o\<^sub>w X x" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.mono_SucI2. tts_lemma mono_SucI1: assumes "range X \ U" and "\x. X x \\<^sub>o\<^sub>w X (Suc x)" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.mono_SucI1. -tts_lemma decseqD: - assumes "range f \ U" - and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ f" - and "(i::nat) \ j" - shows "f j \\<^sub>o\<^sub>w f i" - is Topological_Spaces.decseqD. - tts_lemma monoI2: assumes "range X \ U" and "\x y. x \ y \ X y \\<^sub>o\<^sub>w X x" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.monoI2. tts_lemma monoI1: assumes "range X \ U" and "\x y. x \ y \ X x \\<^sub>o\<^sub>w X y" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.monoI1. -tts_lemma antimono_iff_le_Suc: - assumes "range f \ U" - shows "(on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ f) = (\x. f (Suc x) \\<^sub>o\<^sub>w f x)" - is Nat.antimono_iff_le_Suc. - end tts_context tts: (?'a to U) rewriting ctr_simps substituting order_ow_axioms eliminating through clarsimp begin tts_lemma ex_min_if_finite: assumes "S \ U" and "finite S" and "S \ {}" shows "\x\S. \ (\y\S. y <\<^sub>o\<^sub>w x)" is Lattices_Big.ex_min_if_finite. end tts_context tts: (?'a to U) sbterms: (\(\)::['a::order, 'a::order] \ bool\ to \(\\<^sub>o\<^sub>w)\) and (\(<)::['a::order, 'a::order] \ bool\ to \(<\<^sub>o\<^sub>w)\) substituting order_ow_axioms eliminating through clarsimp begin tts_lemma xt1: shows "\a = b; c <\<^sub>o\<^sub>w b\ \ c <\<^sub>o\<^sub>w a" "\b <\<^sub>o\<^sub>w a; b = c\ \ c <\<^sub>o\<^sub>w a" "\a = b; c \\<^sub>o\<^sub>w b\ \ c \\<^sub>o\<^sub>w a" "\b \\<^sub>o\<^sub>w a; b = c\ \ c \\<^sub>o\<^sub>w a" "\y \ U; x \ U; y \\<^sub>o\<^sub>w x; x \\<^sub>o\<^sub>w y\ \ x = y" "\y \ U; x \ U; z \ U; y \\<^sub>o\<^sub>w x; z \\<^sub>o\<^sub>w y\ \ z \\<^sub>o\<^sub>w x" "\y \ U; x \ U; z \ U; y <\<^sub>o\<^sub>w x; z \\<^sub>o\<^sub>w y\ \ z <\<^sub>o\<^sub>w x" "\y \ U; x \ U; z \ U; y \\<^sub>o\<^sub>w x; z <\<^sub>o\<^sub>w y\ \ z <\<^sub>o\<^sub>w x" "\b \ U; a \ U; b <\<^sub>o\<^sub>w a; a <\<^sub>o\<^sub>w b\ \ P" "\y \ U; x \ U; z \ U; y <\<^sub>o\<^sub>w x; z <\<^sub>o\<^sub>w y\ \ z <\<^sub>o\<^sub>w x" "\b \ U; a \ U; b \\<^sub>o\<^sub>w a; a \ b\ \ b <\<^sub>o\<^sub>w a" "\a \ U; b \ U; a \ b; b \\<^sub>o\<^sub>w a\ \ b <\<^sub>o\<^sub>w a" "\ b \ U; c \ U; a = f b; c <\<^sub>o\<^sub>w b; \x y. \x \ U; y \ U; y <\<^sub>o\<^sub>w x\ \ f y <\<^sub>o\<^sub>w f x \ \ f c <\<^sub>o\<^sub>w a" "\ b \ U; a \ U; b <\<^sub>o\<^sub>w a; f b = c; \x y. \x \ U; y \ U; y <\<^sub>o\<^sub>w x\ \ f y <\<^sub>o\<^sub>w f x \ \ c <\<^sub>o\<^sub>w f a" "\ b \ U; c \ U; a = f b; c \\<^sub>o\<^sub>w b; \x y. \x \ U; y \ U; y \\<^sub>o\<^sub>w x\ \ f y \\<^sub>o\<^sub>w f x \ \ f c \\<^sub>o\<^sub>w a" "\ b \ U; a \ U; b \\<^sub>o\<^sub>w a; f b = c; \x y. \x \ U; y \ U; y \\<^sub>o\<^sub>w x\ \ f y \\<^sub>o\<^sub>w f x \ \ c \\<^sub>o\<^sub>w f a" is Orderings.xt1. end end context ord_order_ow begin tts_context tts: (?'a to U\<^sub>2) and (?'b to U\<^sub>1) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(\)::[?'b::ord, ?'b::ord] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'b::ord, ?'b::ord] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) rewriting ctr_simps substituting ord\<^sub>2.order_ow_axioms eliminating through clarsimp begin tts_lemma xt2: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \ U\<^sub>1" and "a \ U\<^sub>2" and "c \ U\<^sub>1" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "f c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" is Orderings.xt2. tts_lemma xt6: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \ U\<^sub>1" and "a \ U\<^sub>2" and "c \ U\<^sub>1" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "f c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" is Orderings.xt6. end end context order_pair_ow begin tts_context tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) - rewriting ctr_simps - substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms - eliminating through - ( - unfold - strict_mono_ow_def - mono_ow_def - antimono_ow_def - bdd_above_ow_def - bdd_below_ow_def - bdd_ow_def, - clarsimp - ) -begin - -tts_lemma antimonoD: - assumes "x \ U\<^sub>1" - and "y \ U\<^sub>1" - and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" - and "x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y" - shows "f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" - is Orderings.antimonoD. - -tts_lemma antimonoI: - assumes "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" - shows "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" - is Orderings.antimonoI. - -tts_lemma antimonoE: - assumes "x \ U\<^sub>1" - and "y \ U\<^sub>1" - and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" - and "x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y" - and "f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x \ thesis" - shows thesis - is Orderings.antimonoE. - -tts_lemma bdd_below_image_antimono: - assumes "\x\U\<^sub>1. f x \ U\<^sub>2" - and "A \ U\<^sub>1" - and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" - and "ord\<^sub>1.bdd_above A" - shows "ord\<^sub>2.bdd_below (f ` A)" - is Conditionally_Complete_Lattices.bdd_below_image_antimono. - -tts_lemma bdd_above_image_antimono: - assumes "\x\U\<^sub>1. f x \ U\<^sub>2" - and "A \ U\<^sub>1" - and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" - and "ord\<^sub>1.bdd_below A" - shows "ord\<^sub>2.bdd_above (f ` A)" - is Conditionally_Complete_Lattices.bdd_above_image_antimono. - -end - -tts_context - tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(\)::[?'b::order, ?'b::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'b::order, ?'b::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) rewriting ctr_simps substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms eliminating through clarsimp begin tts_lemma xt3: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt3. tts_lemma xt4: assumes "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 b" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f x" shows "f c <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" is Orderings.xt4. tts_lemma xt5: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt5. tts_lemma xt7: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt7. tts_lemma xt8: assumes "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 b" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f x" shows "f c <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" is Orderings.xt8. tts_lemma xt9: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt9. end tts_context tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(\)::[?'b::order, ?'b::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'b::order, ?'b::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) rewriting ctr_simps substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms eliminating through simp begin tts_lemma order_less_subst1: assumes "a \ U\<^sub>1" and "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "c \ U\<^sub>2" and "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f b" and "b <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 y\ \ f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f y" shows "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f c" is Orderings.order_less_subst1. tts_lemma order_subst1: assumes "a \ U\<^sub>1" and "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "c \ U\<^sub>2" and "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f b" and "b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 y\ \ f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f y" shows "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f c" is Orderings.order_subst1. end tts_context tts: (?'a to U\<^sub>1) and (?'c to U\<^sub>2) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(\)::[?'c::order, ?'c::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'c::order, ?'c::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) rewriting ctr_simps substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms eliminating through simp begin tts_lemma order_less_le_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_less_le_subst2. tts_lemma order_le_less_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_le_less_subst2. tts_lemma order_less_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_less_subst2. tts_lemma order_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_subst2. end end subsection\Dense orders\ subsubsection\Definitions and common properties\ locale dense_order_ow = order_ow U le ls for U :: "'ao set" and le ls + assumes dense: "\ x \ U; y \ U; x <\<^sub>o\<^sub>w y \ \ (\z\U. x <\<^sub>o\<^sub>w z \ z <\<^sub>o\<^sub>w y)" subsubsection\Transfer rules\ context includes lifting_syntax begin lemma dense_order_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (dense_order_ow (Collect (Domainp A))) class.dense_order" unfolding dense_order_ow_def class.dense_order_def dense_order_ow_axioms_def class.dense_order_axioms_def apply transfer_prover_start apply transfer_step+ by simp end subsection\ Partial orders with the greatest element and partial orders with the least elements \ subsubsection\Definitions and common properties\ locale ordering_top_ow = ordering_ow U le ls for U :: "'ao set" and le ls + fixes top :: "'ao" ("\<^bold>\\<^sub>o\<^sub>w") assumes top_closed[simp]: "\<^bold>\\<^sub>o\<^sub>w \ U" assumes extremum[simp]: "a \ U \ a \<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w" begin notation top ("\<^bold>\\<^sub>o\<^sub>w") end locale bot_ow = fixes U :: "'ao set" and bot (\\\<^sub>o\<^sub>w\) assumes bot_closed[simp]: "\\<^sub>o\<^sub>w \ U" begin notation bot (\\\<^sub>o\<^sub>w\) end locale bot_pair_ow = ord\<^sub>1: bot_ow U\<^sub>1 bot\<^sub>1 + ord\<^sub>2: bot_ow U\<^sub>2 bot\<^sub>2 for U\<^sub>1 :: "'ao set" and bot\<^sub>1 and U\<^sub>2 :: "'bo set" and bot\<^sub>2 begin notation bot\<^sub>1 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\) notation bot\<^sub>2 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\) end locale order_bot_ow = order_ow U le ls + bot_ow U bot for U :: "'ao set" and bot le ls + assumes bot_least: "a \ U \ \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w a" begin sublocale bot: ordering_top_ow U \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ \\\<^sub>o\<^sub>w\ apply unfold_locales subgoal by simp subgoal by (simp add: bot_least) done no_notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) and top ("\<^bold>\\<^sub>o\<^sub>w") end locale order_bot_pair_ow = ord\<^sub>1: order_bot_ow U\<^sub>1 bot\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_bot_ow U\<^sub>2 bot\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and bot\<^sub>1 le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and bot\<^sub>2 le\<^sub>2 ls\<^sub>2 begin sublocale bot_pair_ow .. sublocale order_pair_ow .. end locale top_ow = fixes U :: "'ao set" and top (\\\<^sub>o\<^sub>w\) assumes top_closed[simp]: "\\<^sub>o\<^sub>w \ U" begin notation top (\\\<^sub>o\<^sub>w\) end locale top_pair_ow = ord\<^sub>1: top_ow U\<^sub>1 top\<^sub>1 + ord\<^sub>2: top_ow U\<^sub>2 top\<^sub>2 for U\<^sub>1 :: "'ao set" and top\<^sub>1 and U\<^sub>2 :: "'bo set" and top\<^sub>2 begin notation top\<^sub>1 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\) notation top\<^sub>2 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\) end locale order_top_ow = order_ow U le ls + top_ow U top for U :: "'ao set" and le ls top + assumes top_greatest: "a \ U \ a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w" begin sublocale top: ordering_top_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ \\\<^sub>o\<^sub>w\ apply unfold_locales subgoal by simp subgoal by (simp add: top_greatest) done no_notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) and top ("\<^bold>\\<^sub>o\<^sub>w") end locale order_top_pair_ow = ord\<^sub>1: order_top_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 top\<^sub>1 + ord\<^sub>2: order_top_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 top\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 top\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 top\<^sub>2 begin sublocale top_pair_ow .. sublocale order_pair_ow .. end subsubsection\Transfer rules\ context includes lifting_syntax begin lemma ordering_top_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (ordering_top_ow (Collect (Domainp A))) ordering_top" proof- let ?P = "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=))" let ?ordering_top_ow = "ordering_top_ow (Collect (Domainp A))" have "?P ?ordering_top_ow (\le ls ext. ext \ UNIV \ ordering_top le ls ext)" unfolding ordering_top_ow_def ordering_top_def ordering_top_ow_axioms_def ordering_top_axioms_def apply transfer_prover_start apply transfer_step+ by blast thus ?thesis by simp qed lemma order_bot_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "(A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (order_bot_ow (Collect (Domainp A))) class.order_bot" proof- let ?P = "(A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))" let ?order_bot_ow = "order_bot_ow (Collect (Domainp A))" have "?P ?order_bot_ow (\bot le ls. bot \ UNIV \ class.order_bot bot le ls)" unfolding class.order_bot_def order_bot_ow_def class.order_bot_axioms_def order_bot_ow_axioms_def bot_ow_def apply transfer_prover_start apply transfer_step+ by blast thus ?thesis by simp qed lemma order_top_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (order_top_ow (Collect (Domainp A))) class.order_top" proof- let ?P = "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=))" let ?order_top_ow = "order_top_ow (Collect (Domainp A))" have "?P ?order_top_ow (\le ls top. top \ UNIV \ class.order_top le ls top)" unfolding class.order_top_def order_top_ow_def class.order_top_axioms_def order_top_ow_axioms_def top_ow_def apply transfer_prover_start apply transfer_step+ by blast thus ?thesis by simp qed end subsubsection\Relativization\ context ordering_top_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting ordering_top_ow_axioms eliminating through simp applying [OF top_closed] begin tts_lemma extremum_uniqueI: assumes "\<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w" shows "\<^bold>\\<^sub>o\<^sub>w = \<^bold>\\<^sub>o\<^sub>w" is ordering_top.extremum_uniqueI. tts_lemma extremum_unique: shows "(\<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w) = (\<^bold>\\<^sub>o\<^sub>w = \<^bold>\\<^sub>o\<^sub>w)" is ordering_top.extremum_unique. tts_lemma extremum_strict: shows "\ \<^bold>\\<^sub>o\<^sub>w \<^bold><\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w" is ordering_top.extremum_strict. tts_lemma not_eq_extremum: shows "(\<^bold>\\<^sub>o\<^sub>w \ \<^bold>\\<^sub>o\<^sub>w) = (\<^bold>\\<^sub>o\<^sub>w \<^bold><\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w)" is ordering_top.not_eq_extremum. end end context order_bot_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting order_bot_ow_axioms eliminating through simp begin tts_lemma bdd_above_bot: assumes "A \ U" shows "bdd_below A" is order_bot_class.bdd_below_bot. tts_lemma not_less_bot: assumes "a \ U" shows "\ a <\<^sub>o\<^sub>w \\<^sub>o\<^sub>w" is order_bot_class.not_less_bot. tts_lemma max_bot: assumes "x \ U" shows "max \\<^sub>o\<^sub>w x = x" is order_bot_class.max_bot. tts_lemma max_bot2: assumes "x \ U" shows "max x \\<^sub>o\<^sub>w = x" is order_bot_class.max_bot2. tts_lemma min_bot: assumes "x \ U" shows "min \\<^sub>o\<^sub>w x = \\<^sub>o\<^sub>w" is order_bot_class.min_bot. tts_lemma min_bot2: assumes "x \ U" shows "min x \\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w" is order_bot_class.min_bot2. tts_lemma bot_unique: assumes "a \ U" shows "(a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w) = (a = \\<^sub>o\<^sub>w)" is order_bot_class.bot_unique. tts_lemma bot_less: assumes "a \ U" shows "(a \ \\<^sub>o\<^sub>w) = (\\<^sub>o\<^sub>w <\<^sub>o\<^sub>w a)" is order_bot_class.bot_less. tts_lemma atLeast_eq_UNIV_iff: assumes "x \ U" shows "({x..\<^sub>o\<^sub>w} = U) = (x = \\<^sub>o\<^sub>w)" is order_bot_class.atLeast_eq_UNIV_iff. tts_lemma le_bot: assumes "a \ U" and "a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w" shows "a = \\<^sub>o\<^sub>w" is order_bot_class.le_bot. end end context order_top_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting order_top_ow_axioms eliminating through simp begin tts_lemma bdd_above_top: assumes "A \ U" shows "bdd_above A" is order_top_class.bdd_above_top. tts_lemma not_top_less: assumes "a \ U" shows "\ \\<^sub>o\<^sub>w <\<^sub>o\<^sub>w a" is order_top_class.not_top_less. tts_lemma max_top: assumes "x \ U" shows "max \\<^sub>o\<^sub>w x = \\<^sub>o\<^sub>w" is order_top_class.max_top. tts_lemma max_top2: assumes "x \ U" shows "max x \\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w" is order_top_class.max_top2. tts_lemma min_top: assumes "x \ U" shows "min \\<^sub>o\<^sub>w x = x" is order_top_class.min_top. tts_lemma min_top2: assumes "x \ U" shows "min x \\<^sub>o\<^sub>w = x" is order_top_class.min_top2. tts_lemma top_unique: assumes "a \ U" shows "(\\<^sub>o\<^sub>w \\<^sub>o\<^sub>w a) = (a = \\<^sub>o\<^sub>w)" is order_top_class.top_unique. tts_lemma less_top: assumes "a \ U" shows "(a \ \\<^sub>o\<^sub>w) = (a <\<^sub>o\<^sub>w \\<^sub>o\<^sub>w)" is order_top_class.less_top. tts_lemma atMost_eq_UNIV_iff: assumes "x \ U" shows "({..\<^sub>o\<^sub>wx} = U) = (x = \\<^sub>o\<^sub>w)" is order_top_class.atMost_eq_UNIV_iff. tts_lemma top_le: assumes "a \ U" and "\\<^sub>o\<^sub>w \\<^sub>o\<^sub>w a" shows "a = \\<^sub>o\<^sub>w" is order_top_class.top_le. end end text\\newpage\ end \ No newline at end of file