diff --git a/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy b/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy --- a/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy +++ b/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy @@ -1,271 +1,271 @@ (* Title: Decreasing Diagrams II Author: Bertram Felgenhauer (2015) Maintainer: Bertram Felgenhauer License: LGPL or BSD License clarification: This file is also licensed under the BSD license to facilitate reuse and moving snippets from here to more suitable places. *) section \Preliminaries\ theory Decreasing_Diagrams_II_Aux imports Well_Quasi_Orders.Multiset_Extension Well_Quasi_Orders.Well_Quasi_Orders begin subsection \Trivialities\ (* move to Relation.thy? *) lemma asymI2: "(\a b. (a,b) \ R \ (b,a) \ R) \ asym R" by (metis asymI irrefl_def) (* move to Relation.thy? *) abbreviation "strict_order R \ irrefl R \ trans R" (* move to Relation.thy? *) lemma order_asym: "trans R \ asym R = irrefl R" -unfolding asym.simps irrefl_def trans_def by meson + by (metis asymD asym_if_irrefl_and_trans irreflI) (* move to Relation.thy? *) lemma strict_order_strict: "strict_order q \ strict (\a b. (a, b) \ q\<^sup>=) = (\a b. (a, b) \ q)" unfolding trans_def irrefl_def by fast (* move to Wellfounded.thy? *) lemma mono_lex1: "mono (\r. lex_prod r s)" by (auto simp add: mono_def) (* move to Wellfounded.thy? *) lemma mono_lex2: "mono (lex_prod r)" by (auto simp add: mono_def) (* move to Wellfounded.thy? *) lemma irrefl_lex_prod: "irrefl R \ irrefl S \ irrefl (R <*lex*> S)" by (auto simp add: lex_prod_def irrefl_def) lemmas converse_inward = rtrancl_converse[symmetric] converse_Un converse_UNION converse_relcomp converse_converse converse_Id subsection \Complete lattices and least fixed points\ context complete_lattice begin subsubsection \A chain-based induction principle\ abbreviation set_chain :: "'a set \ bool" where "set_chain C \ \x \ C. \y \ C. x \ y \ y \ x" lemma lfp_chain_induct: assumes mono: "mono f" and step: "\x. P x \ P (f x)" and chain: "\C. set_chain C \ \ x \ C. P x \ P (Sup C)" shows "P (lfp f)" unfolding lfp_eq_fixp[OF mono] proof (rule fixp_induct) show "monotone (\) (\) f" using mono unfolding order_class.mono_def monotone_def . next show "P (Sup {})" using chain[of "{}"] by simp next show "ccpo.admissible Sup (\) P" by (auto simp add: chain ccpo.admissible_def Complete_Partial_Order.chain_def) qed fact subsubsection \Preservation of transitivity, asymmetry, irreflexivity by suprema\ lemma trans_Sup_of_chain: assumes "set_chain C" and trans: "\R. R \ C \ trans R" shows "trans (Sup C)" proof (intro transI) fix x y z assume "(x,y) \ Sup C" and "(y,z) \ Sup C" from \(x,y) \ Sup C\ obtain R where "R \ C" and "(x,y) \ R" by blast from \(y,z) \ Sup C\ obtain S where "S \ C" and "(y,z) \ S" by blast from \R \ C\ and \S \ C\ and \set_chain C\ have "R \ S = R \ R \ S = S" by blast with \R \ C\ and \S \ C\ have "R \ S \ C" by fastforce with \(x,y) \ R\ and \(y,z) \ S\ and trans[of "R \ S"] have "(x,z) \ R \ S" unfolding trans_def by blast with \R \ S \ C\ show "(x,z) \ \C" by blast qed lemma asym_Sup_of_chain: assumes "set_chain C" and asym: "\ R. R \ C \ asym R" shows "asym (Sup C)" proof (intro asymI2 notI) fix a b assume "(a,b) \ Sup C" then obtain "R" where "R \ C" and "(a,b) \ R" by blast assume "(b,a) \ Sup C" then obtain "S" where "S \ C" and "(b,a) \ S" by blast from \R \ C\ and \S \ C\ and \set_chain C\ have "R \ S = R \ R \ S = S" by blast with \R \ C\ and \S \ C\ have "R \ S \ C" by fastforce - with \(a,b) \ R\ and \(b,a) \ S\ and asym show "False" unfolding asym.simps by blast + with \(a,b) \ R\ and \(b,a) \ S\ and asym[THEN asymD] show "False" by blast qed lemma strict_order_lfp: assumes "mono f" and "\R. strict_order R \ strict_order (f R)" shows "strict_order (lfp f)" proof (intro lfp_chain_induct[of f strict_order]) fix C :: "('b \ 'b) set set" assume "set_chain C" and "\R \ C. strict_order R" from this show "strict_order (Sup C)" by (metis asym_Sup_of_chain trans_Sup_of_chain order_asym) qed fact+ lemma trans_lfp: assumes "mono f" and "\R. trans R \ trans (f R)" shows "trans (lfp f)" by (metis lfp_chain_induct[of f trans] assms trans_Sup_of_chain) end (* complete_lattice *) subsection \Multiset extension\ lemma mulex_iff_mult: "mulex r M N \ (M,N) \ mult {(M,N) . r M N}" by (auto simp add: mulex_on_def restrict_to_def mult_def mulex1_def tranclp_unfold) lemma multI: assumes "trans r" "M = I + K" "N = I + J" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k,j) \ r" shows "(M,N) \ mult r" using assms one_step_implies_mult by blast lemma multE: assumes "trans r" and "(M,N) \ mult r" obtains I J K where "M = I + K" "N = I + J" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k,j) \ r" using mult_implies_one_step[OF assms] by blast lemma mult_on_union: "(M,N) \ mult r \ (K + M, K + N) \ mult r" using mulex_on_union[of "\x y. (x,y) \ r" UNIV] by (auto simp: mulex_iff_mult) lemma mult_on_union': "(M,N) \ mult r \ (M + K, N + K) \ mult r" using mulex_on_union'[of "\x y. (x,y) \ r" UNIV] by (auto simp: mulex_iff_mult) lemma mult_on_add_mset: "(M,N) \ mult r \ (add_mset k M, add_mset k N) \ mult r" unfolding add_mset_add_single[of k M] add_mset_add_single[of k N] by (rule mult_on_union') lemma mult_empty[simp]: "(M,{#}) \ mult R" by (metis mult_def not_less_empty trancl.cases) lemma mult_singleton[simp]: "(x, y) \ r \ (add_mset x M, add_mset y M) \ mult r" unfolding add_mset_add_single[of x M] add_mset_add_single[of y M] apply (rule mult_on_union) using mult1_singleton[of x y r] by (auto simp add: mult_def mult_on_union) lemma empty_mult[simp]: "({#},N) \ mult R \ N \ {#}" using empty_mulex_on[of N UNIV "\M N. (M,N) \ R"] by (auto simp add: mulex_iff_mult) lemma trans_mult: "trans (mult R)" unfolding mult_def by simp lemma strict_order_mult: assumes "irrefl R" and "trans R" shows "irrefl (mult R)" and "trans (mult R)" proof - show "irrefl (mult R)" unfolding irrefl_def proof (intro allI notI, elim multE[OF \trans R\]) fix M I J K assume "M = I + J" "M = I + K" "J \ {#}" and *: "\k \ set_mset K. \j \ set_mset J. (k, j) \ R" from \M = I + J\ and \M = I + K\ have "J = K" by simp have "finite (set_mset J)" by simp then have "set_mset J = {}" using * unfolding \J = K\ by (induct rule: finite_induct) (simp, metis assms insert_absorb insert_iff insert_not_empty irrefl_def transD) then show "False" using \J \ {#}\ by simp qed qed (simp add: trans_mult) lemma mult_of_image_mset: assumes "trans R" and "trans R'" and "\x y. x \ set_mset N \ y \ set_mset M \ (x,y) \ R \ (f x, f y) \ R'" and "(N, M) \ mult R" shows "(image_mset f N, image_mset f M) \ mult R'" proof (insert assms(4), elim multE[OF assms(1)]) fix I J K assume "N = I + K" "M = I + J" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k, j) \ R" thus "(image_mset f N, image_mset f M) \ mult R'" using assms(2,3) by (intro multI) (auto, blast) qed subsection \Incrementality of @{term mult1} and @{term mult}\ lemma mono_mult1: "mono mult1" unfolding mono_def mult1_def by blast lemma mono_mult: "mono mult" unfolding mono_def mult_def proof (intro allI impI subsetI) fix R S :: "'a rel" and x assume "R \ S" and "x \ (mult1 R)\<^sup>+" then show "x \ (mult1 S)\<^sup>+" using mono_mult1[unfolded mono_def] trancl_mono[of x "mult1 R" "mult1 S"] by auto qed subsection \Well-orders and well-quasi-orders\ lemma wf_iff_wfp_on: "wf p \ wfp_on (\a b. (a, b) \ p) UNIV" unfolding wfp_on_iff_inductive_on wf_def inductive_on_def by force lemma well_order_implies_wqo: assumes "well_order r" shows "wqo_on (\a b. (a, b) \ r) UNIV" proof (intro wqo_onI almost_full_onI) show "transp_on (\a b. (a, b) \ r) UNIV" using assms by (auto simp only: well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def trans_def transp_on_def) next fix f :: "nat \ 'a" show "good (\a b. (a, b) \ r) f" using assms unfolding well_order_on_def wf_iff_wfp_on wfp_on_def not_ex not_all de_Morgan_conj proof (elim conjE allE exE) fix x assume "linear_order r" and "f x \ UNIV \ (f (Suc x), f x) \ r - Id" then have "(f x, f (Suc x)) \ r" using \linear_order r\ by (force simp: linear_order_on_def Relation.total_on_def partial_order_on_def preorder_on_def refl_on_def) then show "good (\a b. (a, b) \ r) f" by (auto simp: good_def) qed qed subsection \Splitting lists into prefix, element, and suffix\ fun list_splits :: "'a list \ ('a list \ 'a \ 'a list) list" where "list_splits [] = []" | "list_splits (x # xs) = ([], x, xs) # map (\(xs, x', xs'). (x # xs, x', xs')) (list_splits xs)" lemma list_splits_empty[simp]: "list_splits xs = [] \ xs = []" by (cases xs) simp_all lemma elem_list_splits_append: assumes "(ys, y, zs) \ set (list_splits xs)" shows "ys @ [y] @ zs = xs" using assms by (induct xs arbitrary: ys) auto lemma elem_list_splits_length: assumes "(ys, y, zs) \ set (list_splits xs)" shows "length ys < length xs" and "length zs < length xs" using elem_list_splits_append[OF assms] by auto lemma elem_list_splits_elem: assumes "(xs, y, ys) \ set (list_splits zs)" shows "y \ set zs" using elem_list_splits_append[OF assms] by force lemma list_splits_append: "list_splits (xs @ ys) = map (\(xs', x', ys'). (xs', x', ys' @ ys)) (list_splits xs) @ map (\(xs', x', ys'). (xs @ xs', x', ys')) (list_splits ys)" by (induct xs) auto lemma list_splits_rev: "list_splits (rev xs) = map (\(xs, x, ys). (rev ys, x, rev xs)) (rev (list_splits xs))" by (induct xs) (auto simp add: list_splits_append comp_def prod.case_distrib rev_map) lemma list_splits_map: "list_splits (map f xs) = map (\(xs, x, ys). (map f xs, f x, map f ys)) (list_splits xs)" by (induct xs) auto end (* Decreasing_Diagrams_II_Aux *) diff --git a/thys/Functional_Ordered_Resolution_Prover/Executable_FO_Ordered_Resolution_Prover.thy b/thys/Functional_Ordered_Resolution_Prover/Executable_FO_Ordered_Resolution_Prover.thy --- a/thys/Functional_Ordered_Resolution_Prover/Executable_FO_Ordered_Resolution_Prover.thy +++ b/thys/Functional_Ordered_Resolution_Prover/Executable_FO_Ordered_Resolution_Prover.thy @@ -1,263 +1,263 @@ (* Title: An Executable Simple Ordered Resolution Prover for First-Order Clauses Author: Dmitriy Traytel , 2017, 2018 Author: Anders Schlichtkrull , 2018 Maintainer: Anders Schlichtkrull *) section \An Executable Simple Ordered Resolution Prover for First-Order Clauses\ text \ This theory provides an executable functional implementation of the \deterministic_RP\ prover, building on the \textsf{IsaFoR} library for the notion of terms and on the Knuth--Bendix order. \ theory Executable_FO_Ordered_Resolution_Prover imports Deterministic_FO_Ordered_Resolution_Prover Executable_Subsumption "HOL-Library.Code_Target_Nat" Show.Show_Instances IsaFoR_Term begin global_interpretation RP: deterministic_FO_resolution_prover where S = "\_. {#}" and subst_atm = "(\)" and id_subst = "Var :: _ \ ('f :: {weighted, compare_order}, nat) term" and comp_subst = "(\\<^sub>s)" and renamings_apart = renamings_apart and atm_of_atms = "Fun undefined" and mgu = mgu_sets and less_atm = less_kbo and size_atm = size and timestamp_factor = 1 and size_factor = 1 defines deterministic_RP = RP.deterministic_RP and deterministic_RP_step = RP.deterministic_RP_step and is_final_dstate = RP.is_final_dstate and is_reducible_lit = RP.is_reducible_lit and is_tautology = RP.is_tautology and maximal_wrt = RP.maximal_wrt and reduce = RP.reduce and reduce_all = RP.reduce_all and reduce_all2 = RP.reduce_all2 and remdups_clss = RP.remdups_clss and resolve = RP.resolve and resolve_on = RP.resolve_on and resolvable = RP.resolvable and resolvent = RP.resolvent and resolve_rename = RP.resolve_rename and resolve_rename_either_way = RP.resolve_rename_either_way and select_min_weight_clause = RP.select_min_weight_clause and strictly_maximal_wrt = RP.strictly_maximal_wrt and strictly_subsume = RP.strictly_subsume and subsume = RP.subsume and weight = RP.weight and St0 = RP.St0 and sorted_list_of_set = "linorder.sorted_list_of_set (le_of_comp compare)" and sort_key = "linorder.sort_key (le_of_comp compare)" and insort_key = "linorder.insort_key (le_of_comp compare)" by (unfold_locales) (auto simp: less_kbo_subst is_ground_atm_ground less_kbo_less intro: ground_less_less_kbo) declare RP.deterministic_RP.simps[code] RP.deterministic_RP_step.simps[code] RP.is_final_dstate.simps[code] RP.is_tautology_def[code] RP.reduce.simps[code] RP.reduce_all_def[code] RP.reduce_all2.simps[code] RP.resolve_rename_def[code] RP.resolve_rename_either_way_def[code] RP.select_min_weight_clause.simps[code] RP.weight.simps[code] St0_def[code] substitution_ops.strictly_subsumes_def[code] substitution_ops.subst_cls_lists_def[code] substitution_ops.subst_lit_def[code] substitution_ops.subst_cls_def[code] lemma remove1_mset_subset_eq: "remove1_mset a A \# B \ A \# add_mset a B" by (metis add_mset_add_single subset_eq_diff_conv) lemma Bex_cong: "(\b. b \ B \ P b = Q b) \ Bex B P = Bex B Q" by auto lemma is_reducible_lit_code[code]: "RP.is_reducible_lit Ds C L = (\D \ set Ds. (\L' \ set D. if is_pos L' = is_neg L then (case match_term_list [(atm_of L', atm_of L)] Map.empty of None \ False | Some \ \ subsumes_list (remove1 L' D) C \) else False))" unfolding RP.is_reducible_lit_def subsumes_list_alt subsumes_modulo_def apply (rule Bex_cong)+ subgoal for D L' apply (split if_splits option.splits)+ apply safe subgoal for \ using term_subst_eq[of _ "subst_of_map Var (\x. if x \ vars_lit L' then Some (\ x) else None)" \] by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def dest!: match_term_list_complete[of _ _ "\x. if x \ vars_lit L' then Some (\ x) else None"]) subgoal for \ using term_subst_eq[of _ "subst_of_map Var (\x. if x \ vars_lit L' then Some (\ x) else None)" \] by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def dest!: match_term_list_complete[of _ _ "\x. if x \ vars_lit L' then Some (\ x) else None"]) subgoal for \ by (cases L; cases L'; simp add: subst_lit_def) subgoal for \ by (cases L; cases L'; simp add: subst_lit_def) subgoal for \ \ using same_on_vars_clause[of "mset (remove1 L' D)" "subst_of_map Var (\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None)" \] apply (cases L; cases L'; auto simp add: subst_lit_def dom_def subst_of_map_def dest!: match_term_list_sound split: option.splits if_splits intro!: exI[of _ "\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None"]) by (auto 0 4 simp: extends_subst_def subst_of_map_def split: option.splits dest!: term_subst_eq_rev) subgoal for \ \ by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def extends_subst_def dest!: match_term_list_sound intro!: exI[of _ "subst_of_map Var \"] term_subst_eq) subgoal for \ \ using same_on_vars_clause[of "mset (remove1 L' D)" "subst_of_map Var (\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None)" \] apply (cases L; cases L'; auto simp add: subst_lit_def dom_def subst_of_map_def dest!: match_term_list_sound split: option.splits if_splits intro!: exI[of _ "\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None"]) by (auto 0 4 simp: extends_subst_def subst_of_map_def split: option.splits dest!: term_subst_eq_rev) subgoal for \ \ by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def extends_subst_def dest!: match_term_list_sound intro!: exI[of _ "subst_of_map Var \"] term_subst_eq) subgoal for \ \ by (cases L; cases L'; simp add: subst_lit_def) subgoal for \ \ by (cases L; cases L'; simp add: subst_lit_def) done done declare Pairs_def[folded sorted_list_of_set_def, code] linorder.sorted_list_of_set_sort_remdups[OF class_linorder_compare, folded sorted_list_of_set_def sort_key_def, code] linorder.sort_key_def[OF class_linorder_compare, folded sort_key_def insort_key_def, code] linorder.insort_key.simps[OF class_linorder_compare, folded insort_key_def, code] export_code St0 in SML export_code deterministic_RP in SML module_name RP (*arbitrary*) instantiation nat :: weighted begin definition weights_nat :: "nat weights" where "weights_nat = \w = Suc \ prod_encode, w0 = 1, pr_strict = \(f, n) (g, m). f > g \ f = g \ n > m, least = \n. n = 0, scf = \_ _. 1\" instance by (intro_classes, unfold_locales) - (auto simp: weights_nat_def SN_iff_wf asymp.simps irreflp_def prod_encode_def - intro!: wf_subset[OF wf_lex_prod]) + (auto simp: weights_nat_def SN_iff_wf irreflp_def prod_encode_def + intro: asympI intro!: wf_subset[OF wf_lex_prod]) end definition prover :: "((nat, nat) Term.term literal list \ nat) list \ bool" where "prover N = (case deterministic_RP (St0 N 0) of None \ True | Some R \ [] \ set R)" theorem prover_complete_refutation: "prover N \ satisfiable (RP.grounded_N0 N)" unfolding prover_def St0_def using RP.deterministic_RP_complete[of N 0] RP.deterministic_RP_refutation[of N 0] by (force simp: grounding_of_clss_def grounding_of_cls_def ex_ground_subst split: option.splits if_splits) definition string_literal_of_nat :: "nat \ String.literal" where "string_literal_of_nat n = String.implode (show n)" export_code prover Fun Var Pos Neg string_literal_of_nat "0::nat" "Suc" in SML module_name RPx abbreviation "\ \ Fun 42" abbreviation "\ \ Fun 0 []" abbreviation "\ \ Fun 1 []" abbreviation "\ \ Fun 2 []" abbreviation "X \ Var 0" abbreviation "Y \ Var 1" abbreviation "Z \ Var 2" value "prover ([([Neg (\[X,Y,Z]), Pos (\[Y,Z,X])], 1), ([Pos (\[\,\,\])], 1), ([Neg (\[\,\,\])], 1)] :: ((nat, nat) Term.term literal list \ nat) list)" value "prover ([([Pos (\[X,Y])], 1), ([Neg (\[X,X])], 1)] :: ((nat, nat) Term.term literal list \ nat) list)" value "prover ([([Neg (\[X,Y,Z]), Pos (\[Y,Z,X])], 1)] :: ((nat, nat) Term.term literal list \ nat) list)" definition mk_MSC015_1 :: "nat \ ((nat, nat) Term.term literal list \ nat) list" where "mk_MSC015_1 n = (let init = ([Pos (\ (replicate n \))], 1); rules = map (\i. ([Neg (\ (map Var [0 ..< n - i - 1] @ \ # replicate i \)), Pos (\ (map Var [0 ..< n - i - 1] @ \ # replicate i \))], 1)) [0 ..< n]; goal = ([Neg (\ (replicate n \))], 1) in init # rules @ [goal])" value "prover (mk_MSC015_1 1)" value "prover (mk_MSC015_1 2)" value "prover (mk_MSC015_1 3)" value "prover (mk_MSC015_1 4)" value "prover (mk_MSC015_1 5)" value "prover (mk_MSC015_1 10)" lemma assumes "p a a a a a a a a a a a a a a" "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13. \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 a \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 b)" "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12. \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 a b \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 b a)" "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11. \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 a b b \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 b a a)" "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10. \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 a b b b \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 b a a a)" "(\x1 x2 x3 x4 x5 x6 x7 x8 x9. \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 a b b b b \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 b a a a a)" "(\x1 x2 x3 x4 x5 x6 x7 x8. \ p x1 x2 x3 x4 x5 x6 x7 x8 a b b b b b \ p x1 x2 x3 x4 x5 x6 x7 x8 b a a a a a)" "(\x1 x2 x3 x4 x5 x6 x7. \ p x1 x2 x3 x4 x5 x6 x7 a b b b b b b \ p x1 x2 x3 x4 x5 x6 x7 b a a a a a a)" "(\x1 x2 x3 x4 x5 x6. \ p x1 x2 x3 x4 x5 x6 a b b b b b b b \ p x1 x2 x3 x4 x5 x6 b a a a a a a a)" "(\x1 x2 x3 x4 x5. \ p x1 x2 x3 x4 x5 a b b b b b b b b \ p x1 x2 x3 x4 x5 b a a a a a a a a)" "(\x1 x2 x3 x4. \ p x1 x2 x3 x4 a b b b b b b b b b \ p x1 x2 x3 x4 b a a a a a a a a a)" "(\x1 x2 x3. \ p x1 x2 x3 a b b b b b b b b b b \ p x1 x2 x3 b a a a a a a a a a a)" "(\x1 x2. \ p x1 x2 a b b b b b b b b b b b \ p x1 x2 b a a a a a a a a a a a)" "(\x1. \ p x1 a b b b b b b b b b b b b \ p x1 b a a a a a a a a a a a a)" "(\ p a b b b b b b b b b b b b b \ p b a a a a a a a a a a a a a)" "\ p b b b b b b b b b b b b b b" shows False using assms by metis end diff --git a/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy --- a/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy +++ b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy @@ -1,803 +1,803 @@ (* Title: Integration of IsaFoR Terms and the Knuth-Bendix Order Author: Dmitriy Traytel , 2014 Author: Anders Schlichtkrull , 2017 Maintainer: Anders Schlichtkrull *) section \Integration of \textsf{IsaFoR} Terms and the Knuth--Bendix Order\ text \ This theory implements the abstract interface for atoms and substitutions using the \textsf{IsaFoR} library. \ theory IsaFoR_Term imports Deriving.Derive Ordered_Resolution_Prover.Abstract_Substitution First_Order_Terms.Unification First_Order_Terms.Subsumption "HOL-Cardinals.Wellorder_Extension" Open_Induction.Restricted_Predicates Knuth_Bendix_Order.KBO begin hide_const (open) mgu abbreviation subst_apply_literal :: "('f, 'v) term literal \ ('f, 'v, 'w) gsubst \ ('f, 'w) term literal" (infixl "\lit" 60) where "L \lit \ \ map_literal (\A. A \ \) L" definition subst_apply_clause :: "('f, 'v) term clause \ ('f, 'v, 'w) gsubst \ ('f, 'w) term clause" (infixl "\cls" 60) where "C \cls \ = image_mset (\L. L \lit \) C" abbreviation vars_lit :: "('f, 'v) term literal \ 'v set" where "vars_lit L \ vars_term (atm_of L)" definition vars_clause :: "('f, 'v) term clause \ 'v set" where "vars_clause C = Union (set_mset (image_mset vars_lit C))" definition vars_clause_list :: "('f, 'v) term clause list \ 'v set" where "vars_clause_list Cs = Union (vars_clause ` set Cs) " definition vars_partitioned :: "('f,'v) term clause list \ bool" where "vars_partitioned Cs \ (\i < length Cs. \j < length Cs. i \ j \ (vars_clause (Cs ! i) \ vars_clause (Cs ! j)) = {})" lemma vars_clause_mono: "S \# C \ vars_clause S \ vars_clause C" unfolding vars_clause_def by auto interpretation substitution_ops "(\)" Var "(\\<^sub>s)" . lemma is_ground_atm_is_ground_on_var: assumes "is_ground_atm (A \ \)" and "v \ vars_term A" shows "is_ground_atm (\ v)" using assms proof (induction A) case (Var x) then show ?case by auto next case (Fun f ts) then show ?case unfolding is_ground_atm_def by auto qed lemma is_ground_lit_is_ground_on_var: assumes ground_lit: "is_ground_lit (subst_lit L \)" and v_in_L: "v \ vars_lit L" shows "is_ground_atm (\ v)" proof - let ?A = "atm_of L" from v_in_L have A_p: "v \ vars_term ?A" by auto then have "is_ground_atm (?A \ \)" using ground_lit unfolding is_ground_lit_def by auto then show ?thesis using A_p is_ground_atm_is_ground_on_var by metis qed lemma is_ground_cls_is_ground_on_var: assumes ground_clause: "is_ground_cls (subst_cls C \)" and v_in_C: "v \ vars_clause C" shows "is_ground_atm (\ v)" proof - from v_in_C obtain L where L_p: "L \# C" "v \ vars_lit L" unfolding vars_clause_def by auto then have "is_ground_lit (subst_lit L \)" using ground_clause unfolding is_ground_cls_def subst_cls_def by auto then show ?thesis using L_p is_ground_lit_is_ground_on_var by metis qed lemma is_ground_cls_list_is_ground_on_var: assumes ground_list: "is_ground_cls_list (subst_cls_list Cs \)" and v_in_Cs: "v \ vars_clause_list Cs" shows "is_ground_atm (\ v)" proof - from v_in_Cs obtain C where C_p: "C \ set Cs" "v \ vars_clause C" unfolding vars_clause_list_def by auto then have "is_ground_cls (subst_cls C \)" using ground_list unfolding is_ground_cls_list_def subst_cls_list_def by auto then show ?thesis using C_p is_ground_cls_is_ground_on_var by metis qed lemma same_on_vars_lit: assumes "\v \ vars_lit L. \ v = \ v" shows "subst_lit L \ = subst_lit L \" using assms proof (induction L) case (Pos x) then have "\v \ vars_term x. \ v = \ v \ subst_atm_abbrev x \ = subst_atm_abbrev x \" using term_subst_eq by metis+ then show ?case unfolding subst_lit_def using Pos by auto next case (Neg x) then have "\v \ vars_term x. \ v = \ v \ subst_atm_abbrev x \ = subst_atm_abbrev x \" using term_subst_eq by metis+ then show ?case unfolding subst_lit_def using Neg by auto qed lemma in_list_of_mset_in_S: assumes "i < length (list_of_mset S)" shows "list_of_mset S ! i \# S" proof - from assms have "list_of_mset S ! i \ set (list_of_mset S)" by auto then have "list_of_mset S ! i \# mset (list_of_mset S)" by (meson in_multiset_in_set) then show ?thesis by auto qed lemma same_on_vars_clause: assumes "\v \ vars_clause S. \ v = \ v" shows "subst_cls S \ = subst_cls S \" by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset subst_cls_def vars_clause_def) interpretation substitution "(\)" "Var :: _ \ ('f, nat) term" "(\\<^sub>s)" proof unfold_locales show "\A. A \ Var = A" by auto next show "\A \ \. A \ \ \\<^sub>s \ = A \ \ \ \" by auto next show "\\ \. (\A. A \ \ = A \ \) \ \ = \" by (simp add: subst_term_eqI) next fix C :: "('f, nat) term clause" fix \ assume "is_ground_cls (subst_cls C \)" then have ground_atms_\: "\v. v \ vars_clause C \ is_ground_atm (\ v)" by (meson is_ground_cls_is_ground_on_var) define some_ground_trm :: "('f, nat) term" where "some_ground_trm = (Fun undefined [])" have ground_trm: "is_ground_atm some_ground_trm" unfolding is_ground_atm_def some_ground_trm_def by auto define \ where "\ = (\v. if v \ vars_clause C then \ v else some_ground_trm)" then have \_\: "\v \ vars_clause C. \ v = \ v" unfolding \_def by auto have all_ground_\: "is_ground_atm (\ v)" for v proof (cases "v \ vars_clause C") case True then show ?thesis using ground_atms_\ \_\ by auto next case False then show ?thesis unfolding \_def using ground_trm by auto qed have "is_ground_subst \" unfolding is_ground_subst_def proof fix A show "is_ground_atm (subst_atm_abbrev A \)" proof (induction A) case (Var v) then show ?case using all_ground_\ by auto next case (Fun f As) then show ?case using all_ground_\ by (simp add: is_ground_atm_def) qed qed moreover have "\v \ vars_clause C. \ v = \ v" using \_\ unfolding vars_clause_list_def by blast then have "subst_cls C \ = subst_cls C \" using same_on_vars_clause by auto ultimately show "\\. is_ground_subst \ \ subst_cls C \ = subst_cls C \" by auto next show "wfP (strictly_generalizes_atm :: ('f, 'v) term \ _ \ _)" unfolding wfP_def by (rule wf_subset[OF wf_subsumes]) (auto simp: strictly_generalizes_atm_def generalizes_atm_def term_subsumable.subsumes_def subsumeseq_term.simps) qed lemma vars_partitioned_var_disjoint: assumes "vars_partitioned Cs" shows "var_disjoint Cs" unfolding var_disjoint_def proof (intro allI impI) fix \s :: \('b \ ('a, 'b) term) list\ assume "length \s = length Cs" with assms[unfolded vars_partitioned_def] Fun_More.fun_merge[of "map vars_clause Cs" "nth \s"] obtain \ where \_p: "\i < length (map vars_clause Cs). \x \ map vars_clause Cs ! i. \ x = (\s ! i) x" by auto have "\i < length Cs. \S. S \# Cs ! i \ subst_cls S (\s ! i) = subst_cls S \" proof (rule, rule, rule, rule) fix i :: nat and S :: "('a, 'b) term literal multiset" assume "i < length Cs" and "S \# Cs ! i" then have "\v \ vars_clause S. (\s ! i) v = \ v" using vars_clause_mono[of S "Cs ! i"] \_p by auto then show "subst_cls S (\s ! i) = subst_cls S \" using same_on_vars_clause by auto qed then show "\\. \iS. S \# Cs ! i \ subst_cls S (\s ! i) = subst_cls S \" by auto qed lemma vars_in_instance_in_range_term: "vars_term (subst_atm_abbrev A \) \ Union (image vars_term (range \))" by (induction A) auto lemma vars_in_instance_in_range_lit: "vars_lit (subst_lit L \) \ Union (image vars_term (range \))" proof (induction L) case (Pos A) have "vars_term (A \ \) \ Union (image vars_term (range \))" using vars_in_instance_in_range_term[of A \] by blast then show ?case by auto next case (Neg A) have "vars_term (A \ \) \ Union (image vars_term (range \))" using vars_in_instance_in_range_term[of A \] by blast then show ?case by auto qed lemma vars_in_instance_in_range_cls: "vars_clause (subst_cls C \) \ Union (image vars_term (range \))" unfolding vars_clause_def subst_cls_def using vars_in_instance_in_range_lit[of _ \] by auto primrec renamings_apart :: "('f, nat) term clause list \ (('f, nat) subst) list" where "renamings_apart [] = []" | "renamings_apart (C # Cs) = (let \s = renamings_apart Cs in (\v. Var (v + Max (vars_clause_list (subst_cls_lists Cs \s) \ {0}) + 1)) # \s)" definition var_map_of_subst :: "('f, nat) subst \ nat \ nat" where "var_map_of_subst \ v = the_Var (\ v)" lemma len_renamings_apart: "length (renamings_apart Cs) = length Cs" by (induction Cs) (auto simp: Let_def) lemma renamings_apart_is_Var: "\\ \ set (renamings_apart Cs). \x. is_Var (\ x)" by (induction Cs) (auto simp: Let_def) lemma renamings_apart_inj: "\\ \ set (renamings_apart Cs). inj \" proof (induction Cs) case (Cons a Cs) then have "inj (\v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \ {0}))))" by (meson add_right_imp_eq injI nat.inject term.inject(1)) then show ?case using Cons by (auto simp: Let_def) qed auto lemma finite_vars_clause[simp]: "finite (vars_clause x)" unfolding vars_clause_def by auto lemma finite_vars_clause_list[simp]: "finite (vars_clause_list Cs)" unfolding vars_clause_list_def by (induction Cs) auto lemma Suc_Max_notin_set: "finite X \ Suc (v + Max (insert 0 X)) \ X" by (metis Max.boundedE Suc_n_not_le_n empty_iff finite.insertI le_add2 vimageE vimageI vimage_Suc_insert_0) lemma vars_partitioned_Nil[simp]: "vars_partitioned []" unfolding vars_partitioned_def by auto lemma subst_cls_lists_Nil[simp]: "subst_cls_lists Cs [] = []" unfolding subst_cls_lists_def by auto lemma vars_clause_hd_partitioned_from_tl: assumes "Cs \[]" shows "vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \ vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}" using assms proof (induction Cs) case (Cons C Cs) define \' :: "nat \ nat" where "\' = (\v. (Suc (v + Max ((vars_clause_list (subst_cls_lists Cs (renamings_apart Cs))) \ {0}))))" define \ :: "nat \ ('a, nat) term" where "\ = (\v. Var (\' v))" have "vars_clause (subst_cls C \) \ \ (vars_term ` range \)" using vars_in_instance_in_range_cls[of C "hd (renamings_apart (C # Cs))"] \_def \'_def by (auto simp: Let_def) moreover have "\ (vars_term ` range \) \ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}" proof - have "range \' \ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}" unfolding \'_def using Suc_Max_notin_set by auto then show ?thesis unfolding \_def \'_def by auto qed ultimately have "vars_clause (subst_cls C \) \ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}" by auto then show ?case unfolding \_def \'_def unfolding subst_cls_lists_def by (simp add: Let_def subst_cls_lists_def) qed auto lemma vars_partitioned_renamings_apart: "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))" proof (induction Cs) case (Cons C Cs) { fix i :: nat and j :: nat assume ij: "i < Suc (length Cs)" "j < i" have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" proof (cases i; cases j) fix j' :: nat assume i'j': "i = 0" "j = Suc j'" then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" using ij by auto next fix i' :: nat assume i'j': "i = Suc i'" "j = 0" have disjoin_C_Cs: "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \ vars_clause_list ((subst_cls_lists Cs (renamings_apart Cs))) = {}" using vars_clause_hd_partitioned_from_tl[of "C # Cs"] by (simp add: Let_def subst_cls_lists_def) { fix x assume asm: "x \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')" then have "(subst_cls_lists Cs (renamings_apart Cs) ! i') \ set (subst_cls_lists Cs (renamings_apart Cs))" using i'j' ij unfolding subst_cls_lists_def by (metis Suc_less_SucD length_map len_renamings_apart length_zip min_less_iff_conj nth_mem) moreover from asm have "x \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')" using i'j' ij unfolding subst_cls_lists_def by simp ultimately have "\D \ set (subst_cls_lists Cs (renamings_apart Cs)). x \ vars_clause D" by auto } then have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \ Union (set (map vars_clause ((subst_cls_lists Cs (renamings_apart Cs)))))" by auto then have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}" using disjoin_C_Cs unfolding vars_clause_list_def by auto moreover have "subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i" using i'j' ij unfolding subst_cls_lists_def by (simp add: Let_def) ultimately show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" using i'j' by (simp add: Int_commute) next fix i' :: nat and j' :: nat assume i'j': "i = Suc i'" "j = Suc j'" have "i' j'" using \i = Suc i'\ \j = Suc j'\ ij by blast ultimately have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}" using Cons unfolding vars_partitioned_def by auto then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" unfolding i'j' by (simp add: subst_cls_lists_def Let_def) next assume \i = 0\ and \j = 0\ then show \vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}\ using ij by auto qed } then show ?case unfolding vars_partitioned_def by (metis (no_types, lifting) Int_commute Suc_lessI len_renamings_apart length_map length_nth_simps(2) length_zip min.idem nat.inject not_less_eq subst_cls_lists_def) qed auto interpretation substitution_renamings "(\)" "Var :: _ \ ('f, nat) term" "(\\<^sub>s)" renamings_apart "Fun undefined" proof unfold_locales fix Cs :: "('f, nat) term clause list" show "length (renamings_apart Cs) = length Cs" using len_renamings_apart by auto next fix Cs :: "('f, nat) term clause list" fix \ :: "nat \ ('f, nat) Term.term" assume \_renaming: "\ \ set (renamings_apart Cs)" { have inj_is_renaming: "\\ :: ('f, nat) subst. (\x. is_Var (\ x)) \ inj \ \ is_renaming \" proof - fix \ :: "('f, nat) subst" fix x assume is_var_\: "\x. is_Var (\ x)" assume inj_\: "inj \" define \' where "\' = var_map_of_subst \" have \: "\ = Var \ \'" unfolding \'_def var_map_of_subst_def using is_var_\ by auto from is_var_\ inj_\ have "inj \'" unfolding is_renaming_def unfolding subst_domain_def inj_on_def \'_def var_map_of_subst_def by (metis term.collapse(1)) then have "inv \' \ \' = id" using inv_o_cancel[of \'] by simp then have "Var \ (inv \' \ \') = Var" by simp then have "\x. (Var \ (inv \' \ \')) x = Var x" by metis then have "\x. ((Var \ \') \\<^sub>s (Var \ (inv \'))) x = Var x" unfolding subst_compose_def by auto then have "\ \\<^sub>s (Var \ (inv \')) = Var" using \ by auto then show "is_renaming \" unfolding is_renaming_def by blast qed then have "\\ \ (set (renamings_apart Cs)). is_renaming \" using renamings_apart_is_Var renamings_apart_inj by blast } then show "is_renaming \" using \_renaming by auto next fix Cs :: "('f, nat) term clause list" have "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))" using vars_partitioned_renamings_apart by auto then show "var_disjoint (subst_cls_lists Cs (renamings_apart Cs))" using vars_partitioned_var_disjoint by auto next show "\\ As Bs. Fun undefined As \ \ = Fun undefined Bs \ map (\A. A \ \) As = Bs" by simp qed fun pairs :: "'a list \ ('a \ 'a) list" where "pairs (x # y # xs) = (x, y) # pairs (y # xs)" | "pairs _ = []" derive compare "term" derive compare "literal" lemma class_linorder_compare: "class.linorder (le_of_comp compare) (lt_of_comp compare)" apply standard apply (simp_all add: lt_of_comp_def le_of_comp_def split: order.splits) apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5)) apply (metis comparator_compare comparator_def order.distinct(5)) apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5)) by (metis comparator.sym comparator_compare invert_order.simps(2) order.distinct(5)) context begin interpretation compare_linorder: linorder "le_of_comp compare" "lt_of_comp compare" by (rule class_linorder_compare) definition Pairs where "Pairs AAA = concat (compare_linorder.sorted_list_of_set ((pairs \ compare_linorder.sorted_list_of_set) ` AAA))" lemma unifies_all_pairs_iff: "(\p \ set (pairs xs). fst p \ \ = snd p \ \) \ (\a \ set xs. \b \ set xs. a \ \ = b \ \)" proof (induct xs rule: pairs.induct) case (1 x y xs) then show ?case unfolding pairs.simps list.set ball_Un ball_simps simp_thms fst_conv snd_conv by metis qed simp_all lemma in_pair_in_set: assumes "(A,B) \ set ((pairs As))" shows "A \ set As \ B \ set As" using assms proof (induction As) case (Cons A As) note Cons_outer = this show ?case proof (cases As) case Nil then show ?thesis using Cons_outer by auto next case (Cons B As') then show ?thesis using Cons_outer by auto qed qed auto lemma in_pairs_sorted_list_of_set_in_set: assumes "finite AAA" "\AA \ AAA. finite AA" "AB_pairs \ (pairs \ compare_linorder.sorted_list_of_set) ` AAA" and "(A :: _ :: compare, B) \ set AB_pairs" shows "\AA. AA \ AAA \ A \ AA \ B \ AA" proof - from assms have "AB_pairs \ (pairs \ compare_linorder.sorted_list_of_set) ` AAA" by auto then obtain AA where AA_p: "AA \ AAA \ (pairs \ compare_linorder.sorted_list_of_set) AA = AB_pairs" by auto have "(A, B) \ set (pairs (compare_linorder.sorted_list_of_set AA))" using AA_p[] assms(4) by auto then have "A \ set (compare_linorder.sorted_list_of_set AA)" and "B \ set (compare_linorder.sorted_list_of_set AA)" using in_pair_in_set[of A] by auto then show ?thesis using assms(2) AA_p by auto qed lemma unifiers_Pairs: assumes "finite AAA" and "\AA \ AAA. finite AA" shows "unifiers (set (Pairs AAA)) = {\. is_unifiers \ AAA}" proof (rule; rule) fix \ :: "('a, 'b) subst" assume asm: "\ \ unifiers (set (Pairs AAA))" have "\AA. AA \ AAA \ card (AA \\<^sub>s\<^sub>e\<^sub>t \) \ Suc 0" proof - fix AA :: "('a, 'b) term set" assume asm': "AA \ AAA" then have "\p \ set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \ = subst_atm_abbrev (snd p) \" using assms asm unfolding Pairs_def by auto then have "\A \ AA. \B \ AA. subst_atm_abbrev A \ = subst_atm_abbrev B \" using assms asm' unfolding unifies_all_pairs_iff using compare_linorder.sorted_list_of_set by blast then show "card (AA \\<^sub>s\<^sub>e\<^sub>t \) \ Suc 0" by (smt imageE card.empty card_Suc_eq card_mono finite.intros(1) finite_insert le_SucI singletonI subsetI) qed then show "\ \ {\. is_unifiers \ AAA}" using assms by (auto simp: is_unifiers_def is_unifier_def subst_atms_def) next fix \ :: "('a, 'b) subst" assume asm: "\ \ {\. is_unifiers \ AAA}" { fix AB_pairs A B assume "AB_pairs \ set (compare_linorder.sorted_list_of_set ((pairs \ compare_linorder.sorted_list_of_set) ` AAA))" and "(A, B) \ set AB_pairs" then have "\AA. AA \ AAA \ A \ AA \ B \ AA" using assms by (simp add: in_pairs_sorted_list_of_set_in_set) then obtain AA where a: "AA \ AAA" "A \ AA" "B \ AA" by blast from a assms asm have card_AA_\: "card (AA \\<^sub>s\<^sub>e\<^sub>t \) \ Suc 0" unfolding is_unifiers_def is_unifier_def subst_atms_def by auto have "subst_atm_abbrev A \ = subst_atm_abbrev B \" proof (cases "card (AA \\<^sub>s\<^sub>e\<^sub>t \) = Suc 0") case True moreover have "subst_atm_abbrev A \ \ AA \\<^sub>s\<^sub>e\<^sub>t \" using a assms asm card_AA_\ by auto moreover have "subst_atm_abbrev B \ \ AA \\<^sub>s\<^sub>e\<^sub>t \" using a assms asm card_AA_\ by auto ultimately show ?thesis using a assms asm card_AA_\ by (metis (no_types, lifting) card_Suc_eq singletonD) next case False then have "card (AA \\<^sub>s\<^sub>e\<^sub>t \) = 0" using a assms asm card_AA_\ by arith then show ?thesis using a assms asm card_AA_\ by auto qed } then show "\ \ unifiers (set (Pairs AAA))" unfolding Pairs_def unifiers_def by auto qed end definition "mgu_sets AAA = map_option subst_of (unify (Pairs AAA) [])" lemma mgu_sets_is_imgu: fixes AAA :: "('a :: compare, nat) term set set" and \ :: "('a, nat) subst" assumes fin: "finite AAA" "\AA \ AAA. finite AA" and "mgu_sets AAA = Some \" shows "is_imgu \ AAA" proof - have "Unifiers.is_imgu \ (set (Pairs AAA))" using assms unify_sound unfolding mgu_sets_def by blast thus ?thesis unfolding Unifiers.is_imgu_def is_imgu_def unifiers_Pairs[OF fin] by simp qed interpretation mgu "(\)" "Var :: _ \ ('f :: compare, nat) term" "(\\<^sub>s)" renamings_apart "Fun undefined" mgu_sets proof unfold_locales fix AAA :: "('a :: compare, nat) term set set" and \ :: "('a, nat) subst" assume fin: "finite AAA" "\AA \ AAA. finite AA" and "mgu_sets AAA = Some \" thus "is_mgu \ AAA" using mgu_sets_is_imgu by auto next fix AAA :: "('a :: compare, nat) term set set" and \ :: "('a, nat) subst" assume fin: "finite AAA" "\AA \ AAA. finite AA" and "is_unifiers \ AAA" then have "\ \ unifiers (set (Pairs AAA))" unfolding is_mgu_def unifiers_Pairs[OF fin] by auto then show "\\. mgu_sets AAA = Some \" using unify_complete unfolding mgu_sets_def by blast qed interpretation imgu "(\)" "Var :: _ \ ('f :: compare, nat) term" "(\\<^sub>s)" renamings_apart "Fun undefined" mgu_sets proof unfold_locales fix AAA :: "('a :: compare, nat) term set set" and \ :: "('a, nat) subst" assume fin: "finite AAA" "\AA \ AAA. finite AA" and "mgu_sets AAA = Some \" thus "is_imgu \ AAA" by (rule mgu_sets_is_imgu) qed derive linorder prod derive linorder list text \ This part extends and integrates and the Knuth--Bendix order defined in \textsf{IsaFoR}. \ record 'f weights = w :: "'f \ nat \ nat" w0 :: nat pr_strict :: "'f \ nat \ 'f \ nat \ bool" least :: "'f \ bool" scf :: "'f \ nat \ nat \ nat" class weighted = fixes weights :: "'a weights" assumes weights_adm: "admissible_kbo (w weights) (w0 weights) (pr_strict weights) ((pr_strict weights)\<^sup>=\<^sup>=) (least weights) (scf weights)" and pr_strict_total: "fi = gj \ pr_strict weights fi gj \ pr_strict weights gj fi" and pr_strict_asymp: "asymp (pr_strict weights)" and scf_ok: "i < n \ scf weights (f, n) i \ 1" instantiation unit :: weighted begin definition weights_unit :: "unit weights" where "weights_unit = \w = Suc \ snd, w0 = 1, pr_strict = \(_, n) (_, m). n > m, least = \_. True, scf = \_ _. 1\" instance - by (intro_classes, unfold_locales) (auto simp: weights_unit_def SN_iff_wf asymp.simps irreflp_def - intro!: wf_subset[OF wf_inv_image[OF wf], of _ snd]) + by (intro_classes, unfold_locales) (auto simp: weights_unit_def SN_iff_wf irreflp_def + intro: asympI intro!: wf_subset[OF wf_inv_image[OF wf], of _ snd]) end global_interpretation KBO: admissible_kbo "w (weights :: 'f :: weighted weights)" "w0 (weights :: 'f :: weighted weights)" "pr_strict weights" "((pr_strict weights)\<^sup>=\<^sup>=)" "least weights" "scf weights" defines weight = KBO.weight and kbo = KBO.kbo by (simp add: weights_adm) lemma kbo_code[code]: "kbo s t = (let wt = weight t; ws = weight s in if vars_term_ms (KBO.SCF t) \# vars_term_ms (KBO.SCF s) \ wt \ ws then (if wt < ws then (True, True) else (case s of Var y \ (False, case t of Var x \ True | Fun g ts \ ts = [] \ least weights g) | Fun f ss \ (case t of Var x \ (True, True) | Fun g ts \ if pr_strict weights (f, length ss) (g, length ts) then (True, True) else if (f, length ss) = (g, length ts) then lex_ext_unbounded kbo ss ts else (False, False)))) else (False, False))" by (subst KBO.kbo.simps) (auto simp: Let_def split: term.splits) definition "less_kbo s t = fst (kbo t s)" lemma less_kbo_gtotal: "ground s \ ground t \ s = t \ less_kbo s t \ less_kbo t s" unfolding less_kbo_def using KBO.S_ground_total by (metis pr_strict_total subset_UNIV) lemma less_kbo_subst: fixes \ :: "('f :: weighted, 'v) subst" shows "less_kbo s t \ less_kbo (s \ \) (t \ \)" unfolding less_kbo_def by (rule KBO.S_subst) lemma wfP_less_kbo: "wfP less_kbo" proof - have "SN {(x, y). fst (kbo x y)}" - using pr_strict_asymp by (fastforce simp: asymp.simps irreflp_def intro!: KBO.S_SN scf_ok) + using pr_strict_asymp by (fastforce simp: asympI irreflp_def intro!: KBO.S_SN scf_ok) then show ?thesis unfolding SN_iff_wf wfP_def by (rule wf_subset) (auto simp: less_kbo_def) qed instantiation "term" :: (weighted, type) linorder begin definition "leq_term = (SOME leq. {(s,t). less_kbo s t} \ leq \ Well_order leq \ Field leq = UNIV)" lemma less_trm_extension: "{(s,t). less_kbo s t} \ leq_term" unfolding leq_term_def by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto lemma less_trm_well_order: "well_order leq_term" unfolding leq_term_def by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto definition less_eq_term :: "('a :: weighted, 'b) term \ _ \ bool" where "less_eq_term = in_rel leq_term" definition less_term :: "('a :: weighted, 'b) term \ _ \ bool" where "less_term s t = strict (\) s t" lemma leq_term_minus_Id: "leq_term - Id = {(x,y). x < y}" using less_trm_well_order unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def less_term_def less_eq_term_def by auto lemma less_term_alt: "(<) = in_rel (leq_term - Id)" by (simp add: in_rel_Collect_case_prod_eq leq_term_minus_Id) instance proof (standard, goal_cases less_less_eq refl trans antisym total) case (less_less_eq x y) then show ?case unfolding less_term_def .. next case (refl x) then show ?case using less_trm_well_order unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def less_eq_term_def by auto next case (trans x y z) then show ?case using less_trm_well_order unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def trans_def less_eq_term_def by auto next case (antisym x y) then show ?case using less_trm_well_order unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def less_eq_term_def by auto next case (total x y) then show ?case using less_trm_well_order unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def Relation.total_on_def less_eq_term_def by (cases "x = y") auto qed end instantiation "term" :: (weighted, type) wellorder begin instance using less_trm_well_order[unfolded well_order_on_def wf_def leq_term_minus_Id, THEN conjunct2] by intro_classes (atomize, auto) end lemma ground_less_less_kbo: "ground s \ ground t \ s < t \ less_kbo s t" using less_kbo_gtotal[of s t] less_trm_extension by (auto simp: less_term_def less_eq_term_def) lemma less_kbo_less: "less_kbo s t \ s < t" using less_trm_extension by (auto simp: less_term_alt less_kbo_def KBO.S_irrefl) lemma is_ground_atm_ground: "is_ground_atm t \ ground t" unfolding is_ground_atm_def by (induct t) (fastforce simp: in_set_conv_nth list_eq_iff_nth_eq)+ end diff --git a/thys/Prpu_Maxflow/Graph_Topological_Ordering.thy b/thys/Prpu_Maxflow/Graph_Topological_Ordering.thy --- a/thys/Prpu_Maxflow/Graph_Topological_Ordering.thy +++ b/thys/Prpu_Maxflow/Graph_Topological_Ordering.thy @@ -1,167 +1,167 @@ section "Topological Ordering of Graphs" theory Graph_Topological_Ordering imports Refine_Imperative_HOL.Sepref_Misc "List-Index.List_Index" begin subsection \List-Before Relation\ text \ Two elements of a list are in relation if the first element comes (strictly) before the second element. \ definition "list_before_rel l \ { (a,b). \l1 l2 l3. l=l1@a#l2@b#l3 }" text \list-before only relates elements of the list\ lemma list_before_rel_on_elems: "list_before_rel l \ set l \ set l" unfolding list_before_rel_def by auto text \Irreflexivity of list-before is equivalent to the elements of the list being disjoint.\ lemma list_before_irrefl_eq_distinct: "irrefl (list_before_rel l) \ distinct l" using not_distinct_decomp[of l] by (auto simp: irrefl_def list_before_rel_def) text \Alternative characterization via indexes\ lemma list_before_rel_alt: "list_before_rel l = { (l!i, l!j) | i j. i jlist-before is a strict ordering, i.e., it is transitive and asymmetric.\ lemma list_before_trans[trans]: "distinct l \ trans (list_before_rel l)" by (clarsimp simp: trans_def list_before_rel_alt) (metis index_nth_id less_trans) lemma list_before_asym: "distinct l \ asym (list_before_rel l)" - by (meson asym.intros irrefl_def list_before_irrefl_eq_distinct list_before_trans transE) + by (meson asymI irrefl_def list_before_irrefl_eq_distinct list_before_trans transE) text \Structural properties on the list\ lemma list_before_rel_empty[simp]: "list_before_rel [] = {}" unfolding list_before_rel_def by auto lemma list_before_rel_cons: "list_before_rel (x#l) = ({x}\set l) \ list_before_rel l" apply (intro equalityI subsetI; simp add: split_paired_all) subgoal for a b proof - assume "(a,b) \ list_before_rel (x # l)" then obtain i j where IDX_BOUND: "iset l" using IDX_BOUND by (auto simp: nth_Cons split: nat.splits) } moreover { assume "i\0" with IDX_BOUND have "a=l!(i-1)" "b=l!(j-1)" "i-1 < j-1" "j-1 < length l" by auto hence "(a, b) \ list_before_rel l" unfolding list_before_rel_alt by blast } ultimately show ?thesis by blast qed subgoal premises prems for a b proof - { assume [simp]: "a=x" and "b\set l" then obtain j where "b = l!j" "j list_before_rel l" hence ?thesis unfolding list_before_rel_alt by clarsimp (metis Suc_mono nth_Cons_Suc) } ultimately show ?thesis using prems by blast qed done subsection \Topological Ordering\ text \ A topological ordering of a graph (binary relation) is an enumeration of its nodes, such that for any two nodes \x\,\y\ with \x\ being enumerated earlier than \y\, there is no path from \y\ to \x\ in the graph. We define the predicate \is_top_sorted\ to capture the sortedness criterion, but not the completeness criterion, i.e., the list needs not contain all nodes of the graph. \ definition "is_top_sorted R l \ list_before_rel l \ (R\<^sup>*)\ = {}" lemma is_top_sorted_alt: "is_top_sorted R l \ (\x y. (x,y)\list_before_rel l \ (y,x)\R\<^sup>*)" unfolding is_top_sorted_def by auto lemma is_top_sorted_empty_rel[simp]: "is_top_sorted {} l \ distinct l" by (auto simp: is_top_sorted_def list_before_irrefl_eq_distinct[symmetric] irrefl_def) lemma is_top_sorted_empty_list[simp]: "is_top_sorted R []" by (auto simp: is_top_sorted_def) text \A topological sorted list must be distinct\ lemma is_top_sorted_distinct: assumes "is_top_sorted R l" shows "distinct l" proof (rule ccontr) assume "\distinct l" with list_before_irrefl_eq_distinct[of l] obtain x where "(x,x)\(list_before_rel l)" by (auto simp: irrefl_def) with assms show False unfolding is_top_sorted_def by auto qed lemma is_top_sorted_cons: "is_top_sorted R (x#l) \ ({x}\set l \ (R\<^sup>*)\ = {}) \ is_top_sorted R l" unfolding is_top_sorted_def by (auto simp: list_before_rel_cons) lemma is_top_sorted_append: "is_top_sorted R (l1@l2) \ (set l1\set l2 \ (R\<^sup>*)\ = {}) \ is_top_sorted R l1 \ is_top_sorted R l2" by (induction l1) (auto simp: is_top_sorted_cons) lemma is_top_sorted_remove_elem: "is_top_sorted R (l1@x#l2) \ is_top_sorted R (l1@l2)" by (auto simp: is_top_sorted_cons is_top_sorted_append) text \Removing edges from the graph preserves topological sorting\ lemma is_top_sorted_antimono: assumes "R\R'" assumes "is_top_sorted R' l" shows "is_top_sorted R l" using assms unfolding is_top_sorted_alt by (auto dest: rtrancl_mono_mp) text \ Adding a node to the graph, which has no incoming edges preserves topological ordering. \ lemma is_top_sorted_isolated_constraint: assumes "R' \ R \ {x}\X" "R'\UNIV\{x} = {}" assumes "x\set l" assumes "is_top_sorted R l" shows "is_top_sorted R' l" proof - { fix a b assume "(a,b)\R'\<^sup>*" "a\x" "b\x" hence "(a,b)\R\<^sup>*" proof (induction rule: converse_rtrancl_induct) case base then show ?case by simp next case (step y z) with assms(1,2) have "z\x" "(y,z)\R" by auto with step show ?case by auto qed } note AUX=this show ?thesis using assms(3,4) AUX list_before_rel_on_elems unfolding is_top_sorted_def by fastforce qed end diff --git a/thys/Szpilrajn/Szpilrajn.thy b/thys/Szpilrajn/Szpilrajn.thy --- a/thys/Szpilrajn/Szpilrajn.thy +++ b/thys/Szpilrajn/Szpilrajn.thy @@ -1,981 +1,981 @@ (*<*) theory Szpilrajn imports Main begin (*>*) text \ We formalize a more general version of Szpilrajn's extension theorem~@{cite "Szpilrajn:1930"}, employing the terminology of Bossert and Suzumura~@{cite "Bossert:2010"}. We also formalize Theorem 2.7 of their book. Our extension theorem states that any preorder can be extended to a total preorder while maintaining its structure. The proof of the extension theorem follows the proof presented in the Wikipedia article~@{cite Wiki}. \ section \Definitions\ subsection \Symmetric and asymmetric factor of a relation\ text \ According to Bossert and Suzumura, every relation can be partitioned into its symmetric and asymmetric factor. The symmetric factor of a relation \<^term>\r\ contains all pairs \<^term>\(x, y) \ r\ where \<^term>\(y, x) \ r\. Conversely, the asymmetric factor contains all pairs where this is not the case. In terms of an order \<^term>\(\)\, the asymmetric factor contains all \<^term>\(x, y) \ {(x, y) |x y. x \ y}\ where \<^term>\x < y\. \ definition sym_factor :: "'a rel \ 'a rel" where "sym_factor r \ {(x, y) \ r. (y, x) \ r}" lemma sym_factor_def': "sym_factor r = r \ r\" unfolding sym_factor_def by fast definition asym_factor :: "'a rel \ 'a rel" where "asym_factor r = {(x, y) \ r. (y, x) \ r}" subsubsection \Properties of the symmetric factor\ lemma sym_factorI[intro]: "(x, y) \ r \ (y, x) \ r \ (x, y) \ sym_factor r" unfolding sym_factor_def by blast lemma sym_factorE[elim?]: assumes "(x, y) \ sym_factor r" obtains "(x, y) \ r" "(y, x) \ r" using assms[unfolded sym_factor_def] by blast lemma sym_sym_factor[simp]: "sym (sym_factor r)" unfolding sym_factor_def by (auto intro!: symI) lemma trans_sym_factor[simp]: "trans r \ trans (sym_factor r)" unfolding sym_factor_def' using trans_Int by force lemma refl_on_sym_factor[simp]: "refl_on A r \ refl_on A (sym_factor r)" unfolding sym_factor_def by (auto intro!: refl_onI dest: refl_onD refl_onD1) lemma sym_factor_absorb_if_sym[simp]: "sym r \ sym_factor r = r" unfolding sym_factor_def' by (simp add: sym_conv_converse_eq) lemma sym_factor_idem[simp]: "sym_factor (sym_factor r) = sym_factor r" using sym_factor_absorb_if_sym[OF sym_sym_factor] . lemma sym_factor_reflc[simp]: "sym_factor (r\<^sup>=) = (sym_factor r)\<^sup>=" unfolding sym_factor_def by auto lemma sym_factor_Restr[simp]: "sym_factor (Restr r A) = Restr (sym_factor r) A" unfolding sym_factor_def by blast text \ In contrast to \<^term>\asym_factor\, the \<^term>\sym_factor\ is monotone. \ lemma sym_factor_mono: "r \ s \ sym_factor r \ sym_factor s" unfolding sym_factor_def by auto subsubsection \Properties of the asymmetric factor\ lemma asym_factorI[intro]: "(x, y) \ r \ (y, x) \ r \ (x, y) \ asym_factor r" unfolding asym_factor_def by blast lemma asym_factorE[elim?]: assumes "(x, y) \ asym_factor r" obtains "(x, y) \ r" using assms unfolding asym_factor_def by blast lemma refl_not_in_asym_factor[simp]: "(x, x) \ asym_factor r" unfolding asym_factor_def by blast lemma irrefl_asym_factor[simp]: "irrefl (asym_factor r)" unfolding asym_factor_def irrefl_def by fast lemma asym_asym_factor[simp]: "asym (asym_factor r)" using irrefl_asym_factor by (auto intro!: asymI simp: asym_factor_def) lemma trans_asym_factor[simp]: "trans r \ trans (asym_factor r)" unfolding asym_factor_def trans_def by fast lemma asym_if_irrefl_trans: "irrefl r \ trans r \ asym r" by (intro asymI) (auto simp: irrefl_def trans_def) lemma antisym_if_irrefl_trans: "irrefl r \ trans r \ antisym r" - using antisym_def asym.cases asym_if_irrefl_trans by auto + using antisym_def asym_if_irrefl_trans by (auto dest: asymD) lemma asym_factor_asym_rel[simp]: "asym r \ asym_factor r = r" unfolding asym_factor_def - by (cases r rule: asym.cases) auto + by (auto dest: asymD) lemma irrefl_trans_asym_factor_id[simp]: "irrefl r \ trans r \ asym_factor r = r" using asym_factor_asym_rel[OF asym_if_irrefl_trans] . lemma asym_factor_id[simp]: "asym_factor (asym_factor r) = asym_factor r" using asym_factor_asym_rel[OF asym_asym_factor] . lemma asym_factor_rtrancl: "asym_factor (r\<^sup>*) = asym_factor (r\<^sup>+)" unfolding asym_factor_def by (auto simp add: rtrancl_eq_or_trancl) lemma asym_factor_Restr[simp]: "asym_factor (Restr r A) = Restr (asym_factor r) A" unfolding asym_factor_def by blast lemma acyclic_asym_factor[simp]: "acyclic r \ acyclic (asym_factor r)" unfolding asym_factor_def by (auto intro: acyclic_subset) subsubsection \Relations between symmetric and asymmetric factor\ text \ We prove that \<^term>\sym_factor\ and \<^term>\asym_factor\ partition the input relation. \ lemma sym_asym_factor_Un: "sym_factor r \ asym_factor r = r" unfolding sym_factor_def asym_factor_def by blast lemma disjnt_sym_asym_factor[simp]: "disjnt (sym_factor r) (asym_factor r)" unfolding disjnt_def unfolding sym_factor_def asym_factor_def by blast lemma Field_sym_asym_factor_Un: "Field (sym_factor r) \ Field (asym_factor r) = Field r" using sym_asym_factor_Un Field_Un by metis lemma asym_factor_tranclE: assumes "(a, b) \ (asym_factor r)\<^sup>+" shows "(a, b) \ r\<^sup>+" using assms sym_asym_factor_Un by (metis UnCI subsetI trancl_mono) subsection \Extension of Orders\ text \ We use the definition of Bossert and Suzumura for \extends\. The requirement \<^term>\r \ R\ is obvious. The second requirement \<^term>\asym_factor r \ asym_factor R\ enforces that the extension \<^term>\R\ maintains all strict preferences of \<^term>\r\ (viewing \<^term>\r\ as a preference relation). \ definition extends :: "'a rel \ 'a rel \ bool" where "extends R r \ r \ R \ asym_factor r \ asym_factor R" text \ We define a stronger notion of \<^term>\extends\ where we also demand that \<^term>\sym_factor R \ (sym_factor r)\<^sup>=\. This enforces that the extension does not introduce preference cycles between previously unrelated pairs \<^term>\(x, y) \ R - r\. \ definition strict_extends :: "'a rel \ 'a rel \ bool" where "strict_extends R r \ extends R r \ sym_factor R \ (sym_factor r)\<^sup>=" lemma extendsI[intro]: "r \ R \ asym_factor r \ asym_factor R \ extends R r" unfolding extends_def by (intro conjI) lemma extendsE: assumes "extends R r" obtains "r \ R" "asym_factor r \ asym_factor R" using assms unfolding extends_def by blast lemma trancl_subs_extends_if_trans: "extends r_ext r \ trans r_ext \ r\<^sup>+ \ r_ext" unfolding extends_def asym_factor_def by (metis subrelI trancl_id trancl_mono) lemma extends_if_strict_extends: "strict_extends r_ext ext \ extends r_ext ext" unfolding strict_extends_def by blast lemma strict_extendsI[intro]: assumes "r \ R" "asym_factor r \ asym_factor R" "sym_factor R \ (sym_factor r)\<^sup>=" shows "strict_extends R r" unfolding strict_extends_def using assms by (intro conjI extendsI) lemma strict_extendsE: assumes "strict_extends R r" obtains "r \ R" "asym_factor r \ asym_factor R" "sym_factor R \ (sym_factor r)\<^sup>=" using assms extendsE unfolding strict_extends_def by blast lemma strict_extends_antisym_Restr: assumes "strict_extends R r" assumes "antisym (Restr r A)" shows "antisym ((R - r) \ Restr r A)" proof(rule antisymI, rule ccontr) fix x y assume "(x, y) \ (R - r) \ Restr r A" "(y, x) \ (R - r) \ Restr r A" "x \ y" with \strict_extends R r\ have "(x, y) \ sym_factor R" unfolding sym_factor_def by (auto elim!: strict_extendsE) with assms \x \ y\ have "(x, y) \ sym_factor r" by (auto elim!: strict_extendsE) then have "(x, y) \ r" "(y, x) \ r" unfolding sym_factor_def by simp_all with \antisym (Restr r A)\ \x \ y\ \(y, x) \ R - r \ Restr r A\ show False using antisymD by fastforce qed text \Here we prove that we have no preference cycles between previously unrelated pairs.\ lemma antisym_Diff_if_strict_extends: assumes "strict_extends R r" shows "antisym (R - r)" using strict_extends_antisym_Restr[OF assms, where ?A="{}"] by simp lemma strict_extends_antisym: assumes "strict_extends R r" assumes "antisym r" shows "antisym R" using assms strict_extends_antisym_Restr[OF assms(1), where ?A=UNIV] by (auto elim!: strict_extendsE simp: antisym_def) lemma strict_extends_if_strict_extends_reflc: assumes "strict_extends r_ext (r\<^sup>=)" shows "strict_extends r_ext r" proof(intro strict_extendsI) from assms show "r \ r_ext" by (auto elim: strict_extendsE) from assms \r \ r_ext\ show "asym_factor r \ asym_factor r_ext" unfolding strict_extends_def by (auto simp: asym_factor_def sym_factor_def) from assms show "sym_factor r_ext \ (sym_factor r)\<^sup>=" by (auto simp: sym_factor_def strict_extends_def) qed lemma strict_extends_diff_Id: assumes "irrefl r" "trans r" assumes "strict_extends r_ext (r\<^sup>=)" shows "strict_extends (r_ext - Id) r" proof(intro strict_extendsI) from assms show "r \ r_ext - Id" by (auto elim: strict_extendsE simp: irrefl_def) note antisym_r = antisym_if_irrefl_trans[OF assms(1,2)] with assms strict_extends_if_strict_extends_reflc show "asym_factor r \ asym_factor (r_ext - Id)" unfolding asym_factor_def by (auto intro: strict_extends_antisym[THEN antisymD] elim: strict_extendsE transE) from assms antisym_r show "sym_factor (r_ext - Id) \ (sym_factor r)\<^sup>=" unfolding sym_factor_def by (auto intro: strict_extends_antisym[THEN antisymD]) qed text \ Both \<^term>\extends\ and \<^term>\strict_extends\ form a partial order since they are reflexive, transitive, and antisymmetric. \ lemma shows reflp_extends: "reflp extends" and transp_extends: "transp extends" and antisymp_extends: "antisymp extends" unfolding extends_def reflp_def transp_def antisymp_def by auto lemma shows reflp_strict_extends: "reflp strict_extends" and transp_strict_extends: "transp strict_extends" and antisymp_strict_extends: "antisymp strict_extends" using reflp_extends transp_extends antisymp_extends unfolding strict_extends_def reflp_def transp_def antisymp_def by auto subsection \Missing order definitions\ lemma preorder_onD[dest?]: assumes "preorder_on A r" shows "refl_on A r" "trans r" using assms unfolding preorder_on_def by blast+ lemma preorder_onI[intro]: "refl_on A r \ trans r \ preorder_on A r" unfolding preorder_on_def by (intro conjI) abbreviation "preorder \ preorder_on UNIV" lemma preorder_rtrancl: "preorder (r\<^sup>*)" by (intro preorder_onI refl_rtrancl trans_rtrancl) definition "total_preorder_on A r \ preorder_on A r \ total_on A r" abbreviation "total_preorder r \ total_preorder_on UNIV r" lemma total_preorder_onI[intro]: "refl_on A r \ trans r \ total_on A r \ total_preorder_on A r" unfolding total_preorder_on_def by (intro conjI preorder_onI) lemma total_preorder_onD[dest?]: assumes "total_preorder_on A r" shows "refl_on A r" "trans r" "total_on A r" using assms unfolding total_preorder_on_def preorder_on_def by blast+ definition "strict_partial_order r \ trans r \ irrefl r" lemma strict_partial_orderI[intro]: "trans r \ irrefl r \ strict_partial_order r" unfolding strict_partial_order_def by blast lemma strict_partial_orderD[dest?]: assumes "strict_partial_order r" shows "trans r" "irrefl r" using assms unfolding strict_partial_order_def by blast+ lemma strict_partial_order_acyclic: assumes "strict_partial_order r" shows "acyclic r" by (metis acyclic_irrefl assms strict_partial_order_def trancl_id) abbreviation "partial_order \ partial_order_on UNIV" lemma partial_order_onI[intro]: "refl_on A r \ trans r \ antisym r \ partial_order_on A r" using partial_order_on_def by blast lemma linear_order_onI[intro]: "refl_on A r \ trans r \ antisym r \ total_on A r \ linear_order_on A r" using linear_order_on_def by blast lemma linear_order_onD[dest?]: assumes "linear_order_on A r" shows "refl_on A r" "trans r" "antisym r" "total_on A r" using assms[unfolded linear_order_on_def] partial_order_onD by blast+ text \A typical example is \<^term>\(\)\ on sets:\ lemma strict_partial_order_subset: "strict_partial_order {(x,y). x \ y}" proof show "trans {(x,y). x \ y}" by (auto simp add: trans_def) show "irrefl {(x, y). x \ y}" by (simp add: irrefl_def) qed text \We already have a definition of a strict linear order in \<^term>\strict_linear_order\.\ section \Extending preorders to total preorders\ text \ We start by proving that a preorder with two incomparable elements \<^term>\x\ and \<^term>\y\ can be strictly extended to a preorder where \<^term>\x < y\. \ lemma can_extend_preorder: assumes "preorder_on A r" and "y \ A" "x \ A" "(y, x) \ r" shows "preorder_on A ((insert (x, y) r)\<^sup>+)" "strict_extends ((insert (x, y) r)\<^sup>+) r" proof - note preorder_onD[OF \preorder_on A r\] then have "insert (x, y) r \ A \ A" using \y \ A\ \x \ A\ refl_on_domain by fast with \refl_on A r\ show "preorder_on A ((insert (x, y) r)\<^sup>+)" by (intro preorder_onI refl_onI trans_trancl) (auto simp: trancl_subset_Sigma intro!: r_into_trancl' dest: refl_onD) show "strict_extends ((insert (x, y) r)\<^sup>+) r" proof(intro strict_extendsI) from preorder_onD(2)[OF \preorder_on A r\] \(y, x) \ r\ show "asym_factor r \ asym_factor ((insert (x, y) r)\<^sup>+)" unfolding asym_factor_def trancl_insert using rtranclD rtrancl_into_trancl1 r_r_into_trancl by fastforce from assms have "(y, x) \ (insert (x, y) r)\<^sup>+" unfolding preorder_on_def trancl_insert using refl_onD rtranclD by fastforce with \trans r\ show "sym_factor ((insert (x, y) r)\<^sup>+) \ (sym_factor r)\<^sup>=" unfolding trancl_insert sym_factor_def by (fastforce intro: rtrancl_trans) qed auto qed text \ With this, we can start the proof of our main extension theorem. For this we will use a variant of Zorns Lemma, which only considers nonempty chains: \ lemma Zorns_po_lemma_nonempty: assumes po: "Partial_order r" and u: "\C. \C \ Chains r; C\{}\ \ \u\Field r. \a\C. (a, u) \ r" and "r \ {}" shows "\m\Field r. \a\Field r. (m, a) \ r \ a = m" proof - from \r \ {}\ obtain x where "x \ Field r" using FieldI2 by fastforce with assms show ?thesis using Zorns_po_lemma by (metis empty_iff) qed theorem strict_extends_preorder_on: assumes "preorder_on A base_r" shows "\r. total_preorder_on A r \ strict_extends r base_r" proof - text \ We define an order on the set of strict extensions of the base relation \<^term>\base_r\, where \<^term>\r \ s\ iff \<^term>\strict_extends r base_r\ and \<^term>\strict_extends s r\: \ define order_of_orders :: "('a rel) rel" where "order_of_orders = Restr {(r, s). strict_extends r base_r \ strict_extends s r} {r. preorder_on A r}" text \ We show that this order consists of those relations that are preorders and that strictly extend the base relation \<^term>\base_r\ \ have Field_order_of_orders: "Field order_of_orders = {r. preorder_on A r \ strict_extends r base_r}" using transp_strict_extends proof(safe) fix r assume "preorder_on A r" "strict_extends r base_r" with reflp_strict_extends have "(r, r) \ {(r, s). strict_extends r base_r \ strict_extends s r}" by (auto elim!: reflpE) with \preorder_on A r\ show "r \ Field order_of_orders" unfolding order_of_orders_def by (auto simp: Field_def) qed (auto simp: order_of_orders_def Field_def elim: transpE) text \ We now show that this set has a maximum and that any maximum of this set is a total preorder and as thus is one of the extensions we are looking for. We begin by showing the existence of a maximal element using Zorn's lemma. \ have "\m \ Field order_of_orders. \a \ Field order_of_orders. (m, a) \ order_of_orders \ a = m" proof (rule Zorns_po_lemma_nonempty) text \ Zorn's Lemma requires us to prove that our \<^term>\order_of_orders\ is a nonempty partial order and that every nonempty chain has an upper bound. The partial order property is trivial, since we used \<^term>\strict_extends\ for the relation, which is a partial order as shown above. \ from reflp_strict_extends transp_strict_extends have "Refl {(r, s). strict_extends r base_r \ strict_extends s r}" unfolding refl_on_def Field_def by (auto elim: transpE reflpE) moreover have "trans {(r, s). strict_extends r base_r \ strict_extends s r}" using transp_strict_extends by (auto elim: transpE intro: transI) moreover have "antisym {(r, s). strict_extends r base_r \ strict_extends s r}" using antisymp_strict_extends by (fastforce dest: antisympD intro: antisymI) ultimately show "Partial_order order_of_orders" unfolding order_of_orders_def order_on_defs using Field_order_of_orders Refl_Restr trans_Restr antisym_Restr by blast text \Also, our order is obviously not empty since it contains \<^term>\(base_r, base_r)\:\ have "(base_r, base_r) \ order_of_orders" unfolding order_of_orders_def using assms reflp_strict_extends by (auto dest: reflpD) thus "order_of_orders \ {}" by force text \ Next we show that each chain has an upper bound. For the upper bound we take the union of all relations in the chain. \ show "\u \ Field order_of_orders. \a \ C. (a, u) \ order_of_orders" if C_def: "C \ Chains order_of_orders" and C_nonempty: "C \ {}" for C proof (rule bexI[where x="\C"]) text \ Obviously each element in the chain is a strict extension of \<^term>\base_r\ by definition and as such it is also a preorder. \ have preorder_r: "preorder_on A r" and extends_r: "strict_extends r base_r" if "r \ C" for r using that C_def[unfolded order_of_orders_def Chains_def] by blast+ text \ Because a chain is partially ordered, the union of the chain is reflexive and transitive. \ have total_subs_C: "r \ s \ s \ r" if "r \ C" and "s \ C" for r s using C_def that unfolding Chains_def order_of_orders_def strict_extends_def extends_def by blast have preorder_UnC: "preorder_on A (\C)" proof(intro preorder_onI) show "refl_on A (\C)" using preorder_onD(1)[OF preorder_r] C_nonempty unfolding refl_on_def by auto from total_subs_C show "trans (\C)" using chain_subset_trans_Union[unfolded chain_subset_def] by (metis preorder_onD(2)[OF preorder_r]) qed text \We show that \<^term>\\C\ strictly extends the base relation.\ have strict_extends_UnC: "strict_extends (\C) base_r" proof(intro strict_extendsI) note extends_r_unfolded = extends_r[unfolded extends_def strict_extends_def] show "base_r \ (\C)" using C_nonempty extends_r_unfolded by blast then show "asym_factor base_r \ asym_factor (\C)" using extends_r_unfolded unfolding asym_factor_def by auto show "sym_factor (\C) \ (sym_factor base_r)\<^sup>=" proof(safe) fix x y assume "(x, y) \ sym_factor (\C)" "(x, y) \ sym_factor base_r" then have "(x, y) \ \C" "(y, x) \ \C" unfolding sym_factor_def by blast+ with extends_r obtain c where "c \ C" "(x, y) \ c" "(y, x) \ c" "strict_extends c base_r" using total_subs_C by blast then have "(x, y) \ sym_factor c" unfolding sym_factor_def by blast with \strict_extends c base_r\ \(x, y) \ sym_factor base_r\ show "x = y" unfolding strict_extends_def by blast qed qed from preorder_UnC strict_extends_UnC show "(\C) \ Field order_of_orders" unfolding Field_order_of_orders by simp text \ Lastly, we prove by contradiction that \<^term>\\C\ is an upper bound for the chain. \ show "\a \ C. (a, \C) \ order_of_orders" proof(rule ccontr) presume "\a \ C. (a, \C) \ order_of_orders" then obtain m where m: "m \ C" "(m, \C) \ order_of_orders" by blast hence strict_extends_m: "strict_extends m base_r" "preorder_on A m" using extends_r preorder_r by blast+ with m have "\ strict_extends (\C) m" using preorder_UnC unfolding order_of_orders_def by blast from m have "m \ \C" by blast moreover have "sym_factor (\C) \ (sym_factor m)\<^sup>=" proof(safe) fix a b assume "(a, b) \ sym_factor (\ C)" "(a, b) \ sym_factor m" then have "(a, b) \ sym_factor base_r \ (a, b) \ Id" using strict_extends_UnC[unfolded strict_extends_def] by blast with \(a, b) \ sym_factor m\ strict_extends_m(1) show "a = b" by (auto elim: strict_extendsE simp: sym_factor_mono[THEN in_mono]) qed ultimately have "\ asym_factor m \ asym_factor (\C)" using \\ strict_extends (\C) m\ unfolding strict_extends_def extends_def by blast then obtain x y where "(x, y) \ m" "(y, x) \ m" "(x, y) \ asym_factor m" "(x, y) \ asym_factor (\C)" unfolding asym_factor_def by blast then obtain w where "w \ C" "(y, x) \ w" unfolding asym_factor_def using \m \ C\ by auto with \(y, x) \ m\ have "\ extends m w" unfolding extends_def by auto moreover from \(x, y) \ m\ have "\ extends w m" proof(cases "(x, y) \ w") case True with \(y, x) \ w\ have "(x, y) \ asym_factor w" unfolding asym_factor_def by simp with \(x, y) \ asym_factor m\ show "\ extends w m" unfolding extends_def by auto qed (auto simp: extends_def) ultimately show False using \m \ C\ \w \ C\ using C_def[unfolded Chains_def order_of_orders_def strict_extends_def] by auto qed blast qed qed text \Let our maximal element be named \<^term>\max\:\ from this obtain max where max_field: "max \ Field order_of_orders" and is_max: "\a\Field order_of_orders. (max, a) \ order_of_orders \ a = max" by auto from max_field have max_extends_base: "preorder_on A max" "strict_extends max base_r" using Field_order_of_orders by blast+ text \ We still have to show, that \<^term>\max\ is a strict linear order, meaning that it is also a total order: \ have "total_on A max" proof fix x y :: 'a assume "x \ y" "x \ A" "y \ A" show "(x, y) \ max \ (y, x) \ max" proof (rule ccontr) text \ Assume that \<^term>\max\ is not total, and \<^term>\x\ and \<^term>\y\ are incomparable. Then we can extend \<^term>\max\ by setting $x < y$: \ presume "(x, y) \ max" and "(y, x) \ max" let ?max' = "(insert (x, y) max)\<^sup>+" note max'_extends_max = can_extend_preorder[OF \preorder_on A max\ \y \ A\ \x \ A\ \(y, x) \ max\] hence max'_extends_base: "strict_extends ?max' base_r" using \strict_extends max base_r\ transp_strict_extends by (auto elim: transpE) text \The extended relation is greater than \<^term>\max\, which is a contradiction.\ have "(max, ?max') \ order_of_orders" using max'_extends_base max'_extends_max max_extends_base unfolding order_of_orders_def by simp thus False using FieldI2 \(x, y) \ max\ is_max by fastforce qed simp_all qed with \preorder_on A max\ have "total_preorder_on A max" unfolding total_preorder_on_def by simp with \strict_extends max base_r\ show "?thesis" by blast qed text \ With this extension theorem, we can easily prove Szpilrajn's theorem and its equivalent for partial orders. \ corollary partial_order_extension: assumes "partial_order_on A r" shows "\r_ext. linear_order_on A r_ext \ r \ r_ext" proof - from assms strict_extends_preorder_on obtain r_ext where r_ext: "total_preorder_on A r_ext" "strict_extends r_ext r" unfolding partial_order_on_def by blast with assms have "antisym r_ext" unfolding partial_order_on_def using strict_extends_antisym by blast with assms r_ext have "linear_order_on A r_ext \ r \ r_ext" unfolding total_preorder_on_def order_on_defs strict_extends_def extends_def by blast then show ?thesis .. qed corollary Szpilrajn: assumes "strict_partial_order r" shows "\r_ext. strict_linear_order r_ext \ r \ r_ext" proof - from assms have "partial_order (r\<^sup>=)" by (auto simp: antisym_if_irrefl_trans strict_partial_order_def) from partial_order_extension[OF this] obtain r_ext where "linear_order r_ext" "(r\<^sup>=) \ r_ext" by blast with assms have "r \ r_ext - Id" "strict_linear_order (r_ext - Id)" by (auto simp: irrefl_def strict_linear_order_on_diff_Id dest: strict_partial_orderD(2)) then show ?thesis by blast qed corollary acyclic_order_extension: assumes "acyclic r" shows "\r_ext. strict_linear_order r_ext \ r \ r_ext" proof - from assms have "strict_partial_order (r\<^sup>+)" unfolding strict_partial_order_def using acyclic_irrefl trans_trancl by blast thus ?thesis by (meson Szpilrajn r_into_trancl' subset_iff) qed section \Consistency\ text \ As a weakening of transitivity, Suzumura introduces the notion of consistency which rules out all preference cycles that contain at least one strict preference. Consistency characterises those order relations which can be extended (in terms of \<^term>\extends\) to a total order relation. \ definition consistent :: "'a rel \ bool" where "consistent r = (\(x, y) \ r\<^sup>+. (y, x) \ asym_factor r)" lemma consistentI: "(\x y. (x, y) \ r\<^sup>+ \ (y, x) \ asym_factor r) \ consistent r" unfolding consistent_def by blast lemma consistent_if_preorder_on[simp]: "preorder_on A r \ consistent r" unfolding preorder_on_def consistent_def asym_factor_def by auto lemma consistent_asym_factor[simp]: "consistent r \ consistent (asym_factor r)" unfolding consistent_def using asym_factor_tranclE by fastforce lemma acyclic_asym_factor_if_consistent[simp]: "consistent r \ acyclic (asym_factor r)" unfolding consistent_def acyclic_def using asym_factor_tranclE by (metis case_prodD trancl.simps) lemma consistent_Restr[simp]: "consistent r \ consistent (Restr r A)" unfolding consistent_def asym_factor_def using trancl_mono by fastforce text \ This corresponds to Theorem 2.2~@{cite "Bossert:2010"}. \ theorem trans_if_refl_total_consistent: assumes "refl r" "total r" and "consistent r" shows "trans r" proof fix x y z assume "(x, y) \ r" "(y, z) \ r" from \(x, y) \ r\ \(y, z) \ r\ have "(x, z) \ r\<^sup>+" by simp hence "(z, x) \ asym_factor r" using \consistent r\ unfolding consistent_def by blast hence "x \ z \ (x, z) \ r" unfolding asym_factor_def using \total r\ by (auto simp: total_on_def) then show "(x, z) \ r" apply(cases "x = z") using refl_onD[OF \refl r\] by blast+ qed lemma order_extension_if_consistent: assumes "consistent r" obtains r_ext where "extends r_ext r" "total_preorder r_ext" proof - from assms have extends: "extends (r\<^sup>*) r" unfolding extends_def consistent_def asym_factor_def using rtranclD by (fastforce simp: Field_def) have preorder: "preorder (r\<^sup>*)" unfolding preorder_on_def using refl_on_def trans_def by fastforce from strict_extends_preorder_on[OF preorder] extends obtain r_ext where "total_preorder r_ext" "extends r_ext r" using transpE[OF transp_extends] unfolding strict_extends_def by blast then show thesis using that by blast qed lemma consistent_if_extends_trans: assumes "extends r_ext r" "trans r_ext" shows "consistent r" proof(rule consistentI, standard) fix x y assume *: "(x, y) \ r\<^sup>+" "(y, x) \ asym_factor r" with assms have "(x, y) \ r_ext" using trancl_subs_extends_if_trans[OF assms] by blast moreover from * assms have "(x, y) \ r_ext" unfolding extends_def asym_factor_def by auto ultimately show False by blast qed text \ With Theorem 2.6~@{cite "Bossert:2010"}, we show that \<^term>\consistent\ characterises the existence of order extensions. \ corollary order_extension_iff_consistent: "(\r_ext. extends r_ext r \ total_preorder r_ext) \ consistent r" using order_extension_if_consistent consistent_if_extends_trans by (metis total_preorder_onD(2)) text \ The following theorem corresponds to Theorem 2.7~@{cite "Bossert:2010"}. Bossert and Suzumura claim that this theorem generalises Szpilrajn's theorem; however, we cannot use the theorem to strictly extend a given order \<^term>\Q\. Therefore, it is not strong enough to extend a strict partial order to a strict linear order. It works for total preorders (called orderings by Bossert and Suzumura). Unfortunately, we were not able to generalise the theorem to allow for strict extensions. \ theorem general_order_extension_iff_consistent: assumes "\x y. \ x \ S; y \ S; x \ y \ \ (x, y) \ Q\<^sup>+" assumes "total_preorder_on S Ord" shows "(\Ext. extends Ext Q \ total_preorder Ext \ Restr Ext S = Ord) \ consistent Q" (is "?ExExt \ _") proof assume "?ExExt" then obtain Ext where "extends Ext Q" "refl Ext" "trans Ext" "total Ext" "Restr Ext S = Restr Ord S" using total_preorder_onD by fast show "consistent Q" proof(rule consistentI) fix x y assume "(x, y) \ Q\<^sup>+" with \extends Ext Q\ \trans Ext\ have "(x, y) \ Ext" unfolding extends_def by (metis trancl_id trancl_mono) then have "(y, x) \ asym_factor Ext" unfolding asym_factor_def by blast with \extends Ext Q\ show "(y, x) \ asym_factor Q" unfolding extends_def asym_factor_def by blast qed next assume "consistent Q" define Q' where "Q' \ Q\<^sup>* \ Ord \ Ord O Q\<^sup>* \ Q\<^sup>* O Ord \ (Q\<^sup>* O Ord) O Q\<^sup>*" have "refl (Q\<^sup>*)" "trans (Q\<^sup>*)" "refl_on S Ord" "trans Ord" "total_on S Ord" using refl_rtrancl trans_rtrancl total_preorder_onD[OF \total_preorder_on S Ord\] by - assumption have preorder_Q': "preorder Q'" proof show "refl Q'" unfolding Q'_def refl_on_def by auto from \trans (Q\<^sup>*)\ \refl_on S Ord\ \trans Ord\ show "trans Q'" unfolding Q'_def[simplified] apply(safe intro!: transI) unfolding relcomp.simps by (metis assms(1) refl_on_domain rtranclD transD)+ qed have "consistent Q'" using consistent_if_preorder_on preorder_Q' by blast have "extends Q' Q" proof(rule extendsI) have "Q \ Restr (Q\<^sup>*) (Field Q)" by (auto intro: FieldI1 FieldI2) then show "Q \ Q'" unfolding Q'_def by blast from \consistent Q\ have consistentD: "(x, y) \ Q\<^sup>+ \ (y, x) \ Q \ (x, y) \ Q" for x y unfolding consistent_def asym_factor_def using rtranclD by fastforce have refl_on_domainE: "\ (x, y) \ Ord; x \ S \ y \ S \ P \ \ P" for x y P using refl_on_domain[OF \refl_on S Ord\] by blast show "asym_factor Q \ asym_factor Q'" unfolding Q'_def asym_factor_def Field_def apply(safe) using assms(1) consistentD refl_on_domainE by (metis r_into_rtrancl rtranclD rtrancl_trancl_trancl)+ qed with strict_extends_preorder_on[OF \preorder Q'\] obtain Ext where Ext: "extends Ext Q'" "extends Ext Q" "total_preorder Ext" unfolding strict_extends_def by (metis transpE transp_extends) have not_in_Q': "x \ S \ y \ S \ (x, y) \ Ord \ (x, y) \ Q'" for x y using assms(1) unfolding Q'_def apply(safe) by (metis \refl_on S Ord\ refl_on_def refl_on_domain rtranclD)+ have "Restr Ext S = Ord" proof from \extends Ext Q'\ have "Ord \ Ext" unfolding Q'_def extends_def by auto with \refl_on S Ord\ show "Ord \ Restr Ext S" using refl_on_domain by fast next have "(x, y) \ Ord" if "x \ S" and "y \ S" and "(x, y) \ Ext" for x y proof(rule ccontr) assume "(x, y) \ Ord" with that not_in_Q' have "(x, y) \ Q'" by blast with \refl_on S Ord\ \total_on S Ord\ \x \ S\ \y \ S\ \(x, y) \ Ord\ have "(y, x) \ Ord" unfolding refl_on_def total_on_def by fast hence "(y, x) \ Q'" unfolding Q'_def by blast with \(x, y) \ Q'\ \(y, x) \ Q'\ \extends Ext Q'\ have "(x, y) \ Ext" unfolding extends_def asym_factor_def by auto with \(x, y) \ Ext\ show False by blast qed then show "Restr Ext S \ Ord" by blast qed with Ext show "?ExExt" by blast qed section \Strong consistency\ text \ We define a stronger version of \<^term>\consistent\ which requires that the relation does not contain hidden preference cycles, i.e. if there is a preference cycle then all the elements in the cycle should already be related (in both directions). In contrast to consistency which characterises relations that can be extended, strong consistency characterises relations that can be extended strictly (cf. \<^term>\strict_extends\). \ definition "strongly_consistent r \ sym_factor (r\<^sup>+) \ sym_factor (r\<^sup>=)" lemma consistent_if_strongly_consistent: "strongly_consistent r \ consistent r" unfolding strongly_consistent_def consistent_def by (auto simp: sym_factor_def asym_factor_def) lemma strongly_consistentI: "sym_factor (r\<^sup>+) \ sym_factor (r\<^sup>=) \ strongly_consistent r" unfolding strongly_consistent_def by blast lemma strongly_consistent_if_trans_strict_extension: assumes "strict_extends r_ext r" assumes "trans r_ext" shows "strongly_consistent r" proof(unfold strongly_consistent_def, standard) fix x assume "x \ sym_factor (r\<^sup>+)" then show "x \ sym_factor (r\<^sup>=)" using assms trancl_subs_extends_if_trans[OF extends_if_strict_extends] by (metis sym_factor_mono strict_extendsE subsetD sym_factor_reflc) qed lemma strict_order_extension_if_consistent: assumes "strongly_consistent r" obtains r_ext where "strict_extends r_ext r" "total_preorder r_ext" proof - from assms have "strict_extends (r\<^sup>+) r" unfolding strongly_consistent_def strict_extends_def extends_def asym_factor_def sym_factor_def by (auto simp: Field_def dest: tranclD) moreover have "strict_extends (r\<^sup>*) (r\<^sup>+)" unfolding strict_extends_def extends_def by (auto simp: asym_factor_rtrancl sym_factor_def dest: rtranclD) ultimately have extends: "strict_extends (r\<^sup>*) r" using transpE[OF transp_strict_extends] by blast have "preorder (r\<^sup>*)" unfolding preorder_on_def using refl_on_def trans_def by fastforce from strict_extends_preorder_on[OF this] extends obtain r_ext where "total_preorder r_ext" "strict_extends r_ext r" using transpE[OF transp_strict_extends] by blast then show thesis using that by blast qed experiment begin text \We can instantiate the above theorem to get Szpilrajn's theorem.\ lemma assumes "strict_partial_order r" shows "\r_ext. strict_linear_order r_ext \ r \ r_ext" proof - from assms[unfolded strict_partial_order_def] have "strongly_consistent r" "antisym r" unfolding strongly_consistent_def by (simp_all add: antisym_if_irrefl_trans) from strict_order_extension_if_consistent[OF this(1)] obtain r_ext where "strict_extends r_ext r" "total_preorder r_ext" by blast with assms[unfolded strict_partial_order_def] have "trans (r_ext - Id)" "irrefl (r_ext - Id)" "total (r_ext - Id)" "r \ (r_ext - Id)" using strict_extends_antisym[OF _ \antisym r\] by (auto simp: irrefl_def elim: strict_extendsE intro: trans_diff_Id dest: total_preorder_onD) then show ?thesis unfolding strict_linear_order_on_def by blast qed end (*<*) end (*>*) diff --git a/thys/UTP/toolkit/Sequence.thy b/thys/UTP/toolkit/Sequence.thy --- a/thys/UTP/toolkit/Sequence.thy +++ b/thys/UTP/toolkit/Sequence.thy @@ -1,287 +1,287 @@ (******************************************************************************) (* Project: Isabelle/UTP Toolkit *) (* File: Sequence.thy *) (* Authors: Simon Foster and Frank Zeyda *) (* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *) (******************************************************************************) section \ Infinite Sequences \ theory Sequence imports HOL.Real List_Extra "HOL-Library.Sublist" "HOL-Library.Nat_Bijection" begin typedef 'a seq = "UNIV :: (nat \ 'a) set" by (auto) setup_lifting type_definition_seq definition ssubstr :: "nat \ nat \ 'a seq \ 'a list" where "ssubstr i j xs = map (Rep_seq xs) [i ..< j]" lift_definition nth_seq :: "'a seq \ nat \ 'a" (infixl "!\<^sub>s" 100) is "\ f i. f i" . abbreviation sinit :: "nat \ 'a seq \ 'a list" where "sinit i xs \ ssubstr 0 i xs" lemma sinit_len [simp]: "length (sinit i xs) = i" by (simp add: ssubstr_def) lemma sinit_0 [simp]: "sinit 0 xs = []" by (simp add: ssubstr_def) lemma prefix_upt_0 [intro]: "i \ j \ prefix [0.. j \ prefix (sinit i xs) (sinit j xs)" by (simp add: map_mono_prefix prefix_upt_0 ssubstr_def) lemma sinit_strict_prefix: "i < j \ strict_prefix (sinit i xs) (sinit j xs)" by (metis sinit_len sinit_prefix le_less nat_neq_iff prefix_order.dual_order.strict_iff_order) lemma nth_sinit: "i < n \ sinit n xs ! i = xs !\<^sub>s i" apply (auto simp add: ssubstr_def) apply (transfer, auto) done lemma sinit_append_split: assumes "i < j" shows "sinit j xs = sinit i xs @ ssubstr i j xs" proof - have "[0.. lexord R" "(sinit j ys, sinit j xs) \ lexord R" shows False proof - have sinit_xs: "sinit j xs = sinit i xs @ ssubstr i j xs" by (metis assms(2) sinit_append_split) have sinit_ys: "sinit j ys = sinit i ys @ ssubstr i j ys" by (metis assms(2) sinit_append_split) from sinit_xs sinit_ys assms(4) have "(sinit i ys, sinit i xs) \ lexord R \ (sinit i ys = sinit i xs \ (ssubstr i j ys, ssubstr i j xs) \ lexord R)" by (auto dest: lexord_append) with assms lexord_asymmetric show False by (force) qed lemma sinit_linear_asym_lemma2: assumes "asym R" "(sinit i xs, sinit i ys) \ lexord R" "(sinit j ys, sinit j xs) \ lexord R" shows False proof (cases i j rule: linorder_cases) case less with assms show ?thesis by (auto dest: sinit_linear_asym_lemma1) next case equal with assms show ?thesis by (simp add: lexord_asymmetric) next case greater with assms show ?thesis by (auto dest: sinit_linear_asym_lemma1) qed lemma range_ext: assumes "\i :: nat. \x\{0.. x" by (metis lessI) with assms show "f(x) = g(x)" by (auto) qed lemma sinit_ext: "(\ i. sinit i xs = sinit i ys) \ xs = ys" by (simp add: ssubstr_def, transfer, auto intro: range_ext) definition seq_lexord :: "'a rel \ ('a seq) rel" where "seq_lexord R = {(xs, ys). (\ i. (sinit i xs, sinit i ys) \ lexord R)}" lemma seq_lexord_irreflexive: "\x. (x, x) \ R \ (xs, xs) \ seq_lexord R" by (auto dest: lexord_irreflexive simp add: irrefl_def seq_lexord_def) lemma seq_lexord_irrefl: "irrefl R \ irrefl (seq_lexord R)" by (simp add: irrefl_def seq_lexord_irreflexive) lemma seq_lexord_transitive: assumes "trans R" shows "trans (seq_lexord R)" unfolding seq_lexord_def proof (rule transI, clarify) fix xs ys zs :: "'a seq" and m n :: nat assume las: "(sinit m xs, sinit m ys) \ lexord R" "(sinit n ys, sinit n zs) \ lexord R" hence inz: "m > 0" using gr0I by force from las(1) obtain i where sinitm: "(sinit m xs!i, sinit m ys!i) \ R" "i < m" "\ j R" "j < n" "\ ki. (sinit i xs, sinit i zs) \ lexord R" proof (cases "i \ j") case True note lt = this with sinitm sinitn have "(sinit n xs!i, sinit n zs!i) \ R" by (metis assms le_eq_less_or_eq le_less_trans nth_sinit transD) moreover from lt sinitm sinitn have "\ j lexord R" using sinitm(2) sinitn(2) lt apply (rule_tac lexord_intro_elems) apply (auto) apply (metis less_le_trans less_trans nth_sinit) done thus ?thesis by auto next case False then have ge: "i > j" by auto with assms sinitm sinitn have "(sinit n xs!j, sinit n zs!j) \ R" by (metis less_trans nth_sinit) moreover from ge sinitm sinitn have "\ k lexord R" using sinitm(2) sinitn(2) ge apply (rule_tac lexord_intro_elems) apply (auto) apply (metis less_trans nth_sinit) done thus ?thesis by auto qed qed lemma seq_lexord_trans: "\ (xs, ys) \ seq_lexord R; (ys, zs) \ seq_lexord R; trans R \ \ (xs, zs) \ seq_lexord R" by (meson seq_lexord_transitive transE) lemma seq_lexord_antisym: "\ asym R; (a, b) \ seq_lexord R \ \ (b, a) \ seq_lexord R" by (auto dest: sinit_linear_asym_lemma2 simp add: seq_lexord_def) lemma seq_lexord_asym: assumes "asym R" shows "asym (seq_lexord R)" - by (meson assms asym.simps seq_lexord_antisym seq_lexord_irrefl) + by (meson assms asymD asymI seq_lexord_antisym seq_lexord_irrefl) lemma seq_lexord_total: assumes "total R" shows "total (seq_lexord R)" using assms by (auto simp add: total_on_def seq_lexord_def, meson lexord_linear sinit_ext) lemma seq_lexord_linear: assumes "(\ a b. (a,b)\ R \ a = b \ (b,a) \ R)" shows "(x,y) \ seq_lexord R \ x = y \ (y,x) \ seq_lexord R" proof - have "total R" using assms total_on_def by blast hence "total (seq_lexord R)" using seq_lexord_total by blast thus ?thesis by (auto simp add: total_on_def) qed instantiation seq :: (ord) ord begin definition less_seq :: "'a seq \ 'a seq \ bool" where "less_seq xs ys \ (xs, ys) \ seq_lexord {(xs, ys). xs < ys}" definition less_eq_seq :: "'a seq \ 'a seq \ bool" where "less_eq_seq xs ys = (xs = ys \ xs < ys)" instance .. end instance seq :: (order) order proof fix xs :: "'a seq" show "xs \ xs" by (simp add: less_eq_seq_def) next fix xs ys zs :: "'a seq" assume "xs \ ys" and "ys \ zs" then show "xs \ zs" by (force dest: seq_lexord_trans simp add: less_eq_seq_def less_seq_def trans_def) next fix xs ys :: "'a seq" assume "xs \ ys" and "ys \ xs" then show "xs = ys" apply (auto simp add: less_eq_seq_def less_seq_def) apply (rule seq_lexord_irreflexive [THEN notE]) defer apply (rule seq_lexord_trans) apply (auto intro: transI) done next fix xs ys :: "'a seq" show "xs < ys \ xs \ ys \ \ ys \ xs" apply (auto simp add: less_seq_def less_eq_seq_def) defer apply (rule seq_lexord_irreflexive [THEN notE]) apply auto apply (rule seq_lexord_irreflexive [THEN notE]) defer apply (rule seq_lexord_trans) apply (auto intro: transI) apply (simp add: seq_lexord_irreflexive) done qed instance seq :: (linorder) linorder proof fix xs ys :: "'a seq" have "(xs, ys) \ seq_lexord {(u, v). u < v} \ xs = ys \ (ys, xs) \ seq_lexord {(u, v). u < v}" by (rule seq_lexord_linear) auto then show "xs \ ys \ ys \ xs" by (auto simp add: less_eq_seq_def less_seq_def) qed lemma seq_lexord_mono [mono]: "(\ x y. f x y \ g x y) \ (xs, ys) \ seq_lexord {(x, y). f x y} \ (xs, ys) \ seq_lexord {(x, y). g x y}" apply (auto simp add: seq_lexord_def) apply (metis case_prodD case_prodI lexord_take_index_conv mem_Collect_eq) done fun insort_rel :: "'a rel \ 'a \ 'a list \ 'a list" where "insort_rel R x [] = [x]" | "insort_rel R x (y # ys) = (if (x = y \ (x,y) \ R) then x # y # ys else y # insort_rel R x ys)" inductive sorted_rel :: "'a rel \ 'a list \ bool" where Nil_rel [iff]: "sorted_rel R []" | Cons_rel: "\ y \ set xs. (x = y \ (x, y) \ R) \ sorted_rel R xs \ sorted_rel R (x # xs)" definition list_of_set :: "'a rel \ 'a set \ 'a list" where "list_of_set R = folding_on.F (insort_rel R) []" lift_definition seq_inj :: "'a seq seq \ 'a seq" is "\ f i. f (fst (prod_decode i)) (snd (prod_decode i))" . lift_definition seq_proj :: "'a seq \ 'a seq seq" is "\ f i j. f (prod_encode (i, j))" . lemma seq_inj_inverse: "seq_proj (seq_inj x) = x" by (transfer, simp) lemma seq_proj_inverse: "seq_inj (seq_proj x) = x" by (transfer, simp) lemma seq_inj: "inj seq_inj" by (metis injI seq_inj_inverse) lemma seq_inj_surj: "bij seq_inj" apply (rule bijI) apply (auto simp add: seq_inj) apply (metis rangeI seq_proj_inverse) done end \ No newline at end of file diff --git a/thys/ZFC_in_HOL/ZFC_Cardinals.thy b/thys/ZFC_in_HOL/ZFC_Cardinals.thy --- a/thys/ZFC_in_HOL/ZFC_Cardinals.thy +++ b/thys/ZFC_in_HOL/ZFC_Cardinals.thy @@ -1,2729 +1,2729 @@ section \Cartesian products, Disjoint Sums, Ranks, Cardinals\ theory ZFC_Cardinals imports ZFC_in_HOL begin declare [[coercion_enabled]] declare [[coercion "ord_of_nat :: nat \ V"]] subsection \Ordered Pairs\ lemma singleton_eq_iff [iff]: "set {a} = set {b} \ a=b" by simp lemma doubleton_eq_iff: "set {a,b} = set {c,d} \ (a=c \ b=d) \ (a=d \ b=c)" by (simp add: Set.doubleton_eq_iff) definition vpair :: "V \ V \ V" where "vpair a b = set {set {a},set {a,b}}" definition vfst :: "V \ V" where "vfst p \ THE x. \y. p = vpair x y" definition vsnd :: "V \ V" where "vsnd p \ THE y. \x. p = vpair x y" definition vsplit :: "[[V, V] \ 'a, V] \ 'a::{}" \ \for pattern-matching\ where "vsplit c \ \p. c (vfst p) (vsnd p)" nonterminal Vs syntax (ASCII) "_Tuple" :: "[V, Vs] \ V" ("<(_,/ _)>") "_hpattern" :: "[pttrn, patterns] \ pttrn" ("<_,/ _>") syntax "" :: "V \ Vs" ("_") "_Enum" :: "[V, Vs] \ Vs" ("_,/ _") "_Tuple" :: "[V, Vs] \ V" ("\(_,/ _)\") "_hpattern" :: "[pttrn, patterns] \ pttrn" ("\_,/ _\") translations "" \ ">" "" \ "CONST vpair x y" "" \ ">" "\. b" \ "CONST vsplit(\x . b)" "\. b" \ "CONST vsplit(\x y. b)" lemma vpair_def': "vpair a b = set {set {a,a},set {a,b}}" by (simp add: vpair_def) lemma vpair_iff [simp]: "vpair a b = vpair a' b' \ a=a' \ b=b'" unfolding vpair_def' doubleton_eq_iff by auto lemmas vpair_inject = vpair_iff [THEN iffD1, THEN conjE, elim!] lemma vfst_conv [simp]: "vfst \a,b\ = a" by (simp add: vfst_def) lemma vsnd_conv [simp]: "vsnd \a,b\ = b" by (simp add: vsnd_def) lemma vsplit [simp]: "vsplit c \a,b\ = c a b" by (simp add: vsplit_def) lemma vpair_neq_fst: "\a,b\ \ a" by (metis elts_of_set insertI1 mem_not_sym small_upair vpair_def') lemma vpair_neq_snd: "\a,b\ \ b" by (metis elts_of_set insertI1 mem_not_sym small_upair subsetD subset_insertI vpair_def') lemma vpair_nonzero [simp]: "\x,y\ \ 0" by (metis elts_0 elts_of_set empty_not_insert small_upair vpair_def) lemma zero_notin_vpair: "0 \ elts \x,y\" by (auto simp: vpair_def) lemma inj_on_vpair [simp]: "inj_on (\(x, y). \x, y\) A" by (auto simp: inj_on_def) subsection \Generalized Cartesian product\ definition VSigma :: "V \ (V \ V) \ V" where "VSigma A B \ set(\x \ elts A. \y \ elts (B x). {\x,y\})" abbreviation vtimes where "vtimes A B \ VSigma A (\x. B)" definition pairs :: "V \ (V * V)set" where "pairs r \ {(x,y). \x,y\ \ elts r} " lemma pairs_iff_elts: "(x,y) \ pairs z \ \x,y\ \ elts z" by (simp add: pairs_def) lemma VSigma_iff [simp]: "\a,b\ \ elts (VSigma A B) \ a \ elts A \ b \ elts (B a)" by (auto simp: VSigma_def UNION_singleton_eq_range) lemma VSigmaI [intro!]: "\ a \ elts A; b \ elts (B a)\ \ \a,b\ \ elts (VSigma A B)" by simp lemmas VSigmaD1 = VSigma_iff [THEN iffD1, THEN conjunct1] lemmas VSigmaD2 = VSigma_iff [THEN iffD1, THEN conjunct2] text \The general elimination rule\ lemma VSigmaE [elim!]: assumes "c \ elts (VSigma A B)" obtains x y where "x \ elts A" "y \ elts (B x)" "c=\x,y\" using assms by (auto simp: VSigma_def split: if_split_asm) lemma VSigmaE2 [elim!]: assumes "\a,b\ \ elts (VSigma A B)" obtains "a \ elts A" and "b \ elts (B a)" using assms by auto lemma VSigma_empty1 [simp]: "VSigma 0 B = 0" by auto lemma times_iff [simp]: "\a,b\ \ elts (vtimes A B) \ a \ elts A \ b \ elts B" by simp lemma timesI [intro!]: "\a \ elts A; b \ elts B\ \ \a,b\ \ elts (vtimes A B)" by simp lemma times_empty2 [simp]: "vtimes A 0 = 0" using elts_0 by blast lemma times_empty_iff: "VSigma A B = 0 \ A=0 \ (\x \ elts A. B x = 0)" by (metis VSigmaE VSigmaI elts_0 empty_iff trad_foundation) lemma elts_VSigma: "elts (VSigma A B) = (\(x,y). vpair x y) ` Sigma (elts A) (\x. elts (B x))" by auto lemma small_Sigma [simp]: assumes A: "small A" and B: "\x. x \ A \ small (B x)" shows "small (Sigma A B)" proof - obtain a where "elts a \ A" by (meson assms small_eqpoll) then obtain f where f: "bij_betw f (elts a) A" using eqpoll_def by blast have "\y. elts y \ B x" if "x \ A" for x using B small_eqpoll that by blast then obtain g where g: "\x. x \ A \ elts (g x) \ B x" by metis with f have "elts (VSigma a (g \ f)) \ Sigma A B" by (simp add: elts_VSigma Sigma_eqpoll_cong bij_betwE) then show ?thesis using small_eqpoll by blast qed lemma small_Times [simp]: assumes "small A" "small B" shows "small (A \ B)" by (simp add: assms) lemma small_Times_iff: "small (A \ B) \ small A \ small B \ A={} \ B={}" (is "_ = ?rhs") proof assume *: "small (A \ B)" { have "small A \ small B" if "x \ A" "y \ B" for x y proof - have "A \ fst ` (A \ B)" "B \ snd ` (A \ B)" using that by auto with that show ?thesis by (metis * replacement smaller_than_small) qed } then show ?rhs by (metis equals0I) next assume ?rhs then show "small (A \ B)" by auto qed subsection \Disjoint Sum\ definition vsum :: "V \ V \ V" (infixl "\" 65) where "A \ B \ (VSigma (set {0}) (\x. A)) \ (VSigma (set {1}) (\x. B))" definition Inl :: "V\V" where "Inl a \ \0,a\" definition Inr :: "V\V" where "Inr b \ \1,b\" lemmas sum_defs = vsum_def Inl_def Inr_def lemma Inl_nonzero [simp]:"Inl x \ 0" by (metis Inl_def vpair_nonzero) lemma Inr_nonzero [simp]:"Inr x \ 0" by (metis Inr_def vpair_nonzero) subsubsection\Equivalences for the injections and an elimination rule\ lemma Inl_in_sum_iff [iff]: "Inl a \ elts (A \ B) \ a \ elts A" by (auto simp: sum_defs) lemma Inr_in_sum_iff [iff]: "Inr b \ elts (A \ B) \ b \ elts B" by (auto simp: sum_defs) lemma sumE [elim!]: assumes u: "u \ elts (A \ B)" obtains x where "x \ elts A" "u=Inl x" | y where "y \ elts B" "u=Inr y" using u by (auto simp: sum_defs) subsubsection \Injection and freeness equivalences, for rewriting\ lemma Inl_iff [iff]: "Inl a=Inl b \ a=b" by (simp add: sum_defs) lemma Inr_iff [iff]: "Inr a=Inr b \ a=b" by (simp add: sum_defs) lemma inj_on_Inl [simp]: "inj_on Inl A" by (simp add: inj_on_def) lemma inj_on_Inr [simp]: "inj_on Inr A" by (simp add: inj_on_def) lemma Inl_Inr_iff [iff]: "Inl a=Inr b \ False" by (simp add: sum_defs) lemma Inr_Inl_iff [iff]: "Inr b=Inl a \ False" by (simp add: sum_defs) lemma sum_empty [simp]: "0 \ 0 = 0" by auto lemma elts_vsum: "elts (a \ b) = Inl ` (elts a) \ Inr ` (elts b)" by auto lemma sum_iff: "u \ elts (A \ B) \ (\x. x \ elts A \ u=Inl x) \ (\y. y \ elts B \ u=Inr y)" by blast lemma sum_subset_iff: "A\B \ C\D \ A\C \ B\D" by (auto simp: less_eq_V_def) lemma sum_equal_iff: fixes A :: V shows "A\B = C\D \ A=C \ B=D" by (simp add: eq_iff sum_subset_iff) definition is_sum :: "V \ bool" where "is_sum z = (\x. z = Inl x \ z = Inr x)" definition sum_case :: "(V \ 'a) \ (V \ 'a) \ V \ 'a" where "sum_case f g a \ THE z. (\x. a = Inl x \ z = f x) \ (\y. a = Inr y \ z = g y) \ (\ is_sum a \ z = undefined)" lemma sum_case_Inl [simp]: "sum_case f g (Inl x) = f x" by (simp add: sum_case_def is_sum_def) lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y" by (simp add: sum_case_def is_sum_def) lemma sum_case_non [simp]: "\ is_sum a \ sum_case f g a = undefined" by (simp add: sum_case_def is_sum_def) lemma is_sum_cases: "(\x. z = Inl x \ z = Inr x) \ \ is_sum z" by (auto simp: is_sum_def) lemma sum_case_split: "P (sum_case f g a) \ (\x. a = Inl x \ P(f x)) \ (\y. a = Inr y \ P(g y)) \ (\ is_sum a \ P undefined)" by (cases "is_sum a") (auto simp: is_sum_def) lemma sum_case_split_asm: "P (sum_case f g a) \ \ ((\x. a = Inl x \ \ P(f x)) \ (\y. a = Inr y \ \ P(g y)) \ (\ is_sum a \ \ P undefined))" by (auto simp: sum_case_split) subsubsection \Applications of disjoint sums and pairs: general union theorems for small sets\ lemma small_Un: assumes X: "small X" and Y: "small Y" shows "small (X \ Y)" proof - obtain x y where "elts x \ X" "elts y \ Y" by (meson assms small_eqpoll) then have "X \ Y \ Inl ` (elts x) \ Inr ` (elts y)" by (metis (mono_tags, lifting) Inr_Inl_iff Un_lepoll_mono disjnt_iff eqpoll_imp_lepoll eqpoll_sym f_inv_into_f inj_on_Inl inj_on_Inr inj_on_image_lepoll_2) then show ?thesis by (metis lepoll_iff replacement small_elts small_sup_iff smaller_than_small) qed lemma small_UN [simp,intro]: assumes A: "small A" and B: "\x. x \ A \ small (B x)" shows "small (\x\A. B x)" proof - obtain a where "elts a \ A" by (meson assms small_eqpoll) then obtain f where f: "bij_betw f (elts a) A" using eqpoll_def by blast have "\y. elts y \ B x" if "x \ A" for x using B small_eqpoll that by blast then obtain g where g: "\x. x \ A \ elts (g x) \ B x" by metis have sm: "small (Sigma (elts a) (elts \ g \ f))" by simp have "(\x\A. B x) \ Sigma A B" by (metis image_lepoll snd_image_Sigma) also have "... \ Sigma (elts a) (elts \ g \ f)" by (smt (verit) Sigma_eqpoll_cong bij_betw_iff_bijections comp_apply eqpoll_imp_lepoll eqpoll_sym f g) finally show ?thesis using lepoll_small sm by blast qed lemma small_Union [simp,intro]: assumes "\ \ Collect small" "small \" shows "small (\ \)" using small_UN [of \ "\x. x"] assms by (simp add: subset_iff) subsection\Generalised function space and lambda\ definition VLambda :: "V \ (V \ V) \ V" where "VLambda A b \ set ((\x. \x,b x\) ` elts A)" definition app :: "[V,V] \ V" where "app f x \ THE y. \x,y\ \ elts f" lemma beta [simp]: assumes "x \ elts A" shows "app (VLambda A b) x = b x" using assms by (auto simp: VLambda_def app_def) definition VPi :: "V \ (V \ V) \ V" where "VPi A B \ set {f \ elts (VPow(VSigma A B)). elts A \ Domain (pairs f) \ single_valued (pairs f)}" lemma VPi_I: assumes "\x. x \ elts A \ b x \ elts (B x)" shows "VLambda A b \ elts (VPi A B)" proof (clarsimp simp: VPi_def, intro conjI impI) show "VLambda A b \ VSigma A B" by (auto simp: assms VLambda_def split: if_split_asm) show "elts A \ Domain (pairs (VLambda A b))" by (force simp: VLambda_def pairs_iff_elts) show "single_valued (pairs (VLambda A b))" by (auto simp: VLambda_def single_valued_def pairs_iff_elts) show "small {f. f \ VSigma A B \ elts A \ Domain (pairs f) \ single_valued (pairs f)}" by (metis (mono_tags, lifting) down VPow_iff mem_Collect_eq subsetI) qed lemma apply_pair: assumes f: "f \ elts (VPi A B)" and x: "x \ elts A" shows "\x, app f x\ \ elts f" proof - have "x \ Domain (pairs f)" by (metis (no_types, lifting) VPi_def assms elts_of_set empty_iff mem_Collect_eq subsetD) then obtain y where y: "\x,y\ \ elts f" using pairs_iff_elts by auto show ?thesis unfolding app_def proof (rule theI) show "\x, y\ \ elts f" by (rule y) show "z = y" if "\x, z\ \ elts f" for z using f unfolding VPi_def by (metis (mono_tags, lifting) that elts_of_set empty_iff mem_Collect_eq pairs_iff_elts single_valued_def y) qed qed lemma VPi_D: assumes f: "f \ elts (VPi A B)" and x: "x \ elts A" shows "app f x \ elts (B x)" proof - have "f \ VSigma A B" by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq) then show ?thesis using apply_pair [OF assms] by blast qed lemma VPi_memberD: assumes f: "f \ elts (VPi A B)" and p: "p \ elts f" obtains x where "x \ elts A" "p = \x, app f x\" proof - have "f \ VSigma A B" by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq) then obtain x y where "p = \x,y\" "x \ elts A" using p by blast then have "y = app f x" by (metis (no_types, lifting) VPi_def apply_pair elts_of_set equals0D f mem_Collect_eq p pairs_iff_elts single_valuedD) then show thesis using \p = \x, y\\ \x \ elts A\ that by blast qed lemma fun_ext: assumes "f \ elts (VPi A B)" "g \ elts (VPi A B)" "\x. x \ elts A \ app f x = app g x" shows "f = g" by (metis VPi_memberD V_equalityI apply_pair assms) lemma eta[simp]: assumes "f \ elts (VPi A B)" shows "VLambda A ((app)f) = f" proof (rule fun_ext [OF _ assms]) show "VLambda A (app f) \ elts (VPi A B)" using VPi_D VPi_I assms by auto qed auto lemma fst_pairs_VLambda: "fst ` pairs (VLambda A f) = elts A" by (force simp: VLambda_def pairs_def) lemma snd_pairs_VLambda: "snd ` pairs (VLambda A f) = f ` elts A" by (force simp: VLambda_def pairs_def) lemma VLambda_eq_D1: "VLambda A f = VLambda B g \ A = B" by (metis ZFC_in_HOL.ext fst_pairs_VLambda) lemma VLambda_eq_D2: "\VLambda A f = VLambda A g; x \ elts A\ \ f x = g x" by (metis beta) subsection\Transitive closure of a set\ definition TC :: "V\V" where "TC \ transrec (\f x. x \ \ (f ` elts x))" lemma TC: "TC a = a \ \ (TC ` elts a)" by (metis (no_types, lifting) SUP_cong TC_def restrict_apply' transrec) lemma TC_0 [simp]: "TC 0 = 0" by (metis TC ZFC_in_HOL.Sup_empty elts_0 image_is_empty sup_V_0_left) lemma arg_subset_TC: "a \ TC a" by (metis (no_types) TC sup_ge1) lemma Transset_TC: "Transset(TC a)" proof (induction a rule: eps_induct) case (step x) have 1: "v \ elts (TC x)" if "v \ elts u" "u \ elts x" for u v using that unfolding TC [of x] using arg_subset_TC by fastforce have 2: "v \ elts (TC x)" if "v \ elts u" "\x\elts x. u \ elts (TC x)" for u v using that step unfolding TC [of x] Transset_def by auto show ?case unfolding Transset_def by (subst TC) (force intro: 1 2) qed lemma TC_least: "\Transset x; a\x\ \ TC a \ x" proof (induction a rule: eps_induct) case (step y) show ?case proof (cases "y=0") case True then show ?thesis by auto next case False have "\ (TC ` elts y) \ x" proof (rule cSup_least) show "TC ` elts y \ {}" using False by auto show "z \ x" if "z \ TC ` elts y" for z using that by (metis Transset_def image_iff step.IH step.prems vsubsetD) qed then show ?thesis by (simp add: step TC [of y]) qed qed definition less_TC (infix "\" 50) where "x \ y \ x \ elts (TC y)" definition le_TC (infix "\" 50) where "x \ y \ x \ y \ x=y" lemma less_TC_imp_not_le: "x \ a \ \ a \ x" proof (induction a arbitrary: x rule: eps_induct) case (step a) then show ?case unfolding TC[of a] less_TC_def using Transset_TC Transset_def by force qed lemma non_TC_less_0 [iff]: "\ (x \ 0)" using less_TC_imp_not_le by blast lemma less_TC_iff: "x \ y \ (\z \ elts y. x \ z)" by (auto simp: less_TC_def le_TC_def TC [of y]) lemma nonzero_less_TC: "x \ 0 \ 0 \ x" by (metis eps_induct le_TC_def less_TC_iff trad_foundation) lemma less_irrefl_TC [simp]: "\ x \ x" using less_TC_imp_not_le by blast lemma less_asym_TC: "\x \ y; y \ x\ \ False" by (metis TC_least Transset_TC Transset_def antisym_conv less_TC_def less_TC_imp_not_le order_refl) lemma le_antisym_TC: "\x \ y; y \ x\ \ x = y" using le_TC_def less_asym_TC by auto lemma less_le_TC: "x \ y \ x \ y \ x \ y" using le_TC_def less_asym_TC by blast lemma less_imp_le_TC [iff]: "x \ y \ x \ y" by (simp add: le_TC_def) lemma le_TC_refl [iff]: "x \ x" by (simp add: le_TC_def) lemma le_TC_trans [trans]: "\x \ y; y \ z\ \ x \ z" by (smt (verit, best) TC_least Transset_TC Transset_def le_TC_def less_TC_def vsubsetD) context order begin lemma nless_le_TC: "(\ a \ b) \ (\ a \ b) \ a = b" using le_TC_def less_asym_TC by blast lemma eq_refl_TC: "x = y \ x \ y" by simp local_setup \ HOL_Order_Tac.declare_order { ops = {eq = @{term \(=) :: V \ V \ bool\}, le = @{term \(\)\}, lt = @{term \(\)\}}, thms = {trans = @{thm le_TC_trans}, refl = @{thm le_TC_refl}, eqD1 = @{thm eq_refl_TC}, eqD2 = @{thm eq_refl_TC[OF sym]}, antisym = @{thm le_antisym_TC}, contr = @{thm notE}}, conv_thms = {less_le = @{thm eq_reflection[OF less_le_TC]}, nless_le = @{thm eq_reflection[OF nless_le_TC]}} } \ end lemma less_TC_trans [trans]: "\x \ y; y \ z\ \ x \ z" and less_le_TC_trans: "\x \ y; y \ z\ \ x \ z" and le_less_TC_trans [trans]: "\x \ y; y \ z\ \ x \ z" by simp_all lemma TC_sup_distrib: "TC (x \ y) = TC x \ TC y" by (simp add: Sup_Un_distrib TC [of "x \ y"] TC [of x] TC [of y] image_Un sup.assoc sup_left_commute) lemma TC_Sup_distrib: assumes "small X" shows "TC (\X) = \(TC ` X)" proof - have "\X \ \ (TC ` X)" using arg_subset_TC by fastforce moreover have "\ (\x\X. TC ` elts x) \ \ (TC ` X)" using assms by clarsimp (meson TC_least Transset_TC Transset_def arg_subset_TC replacement vsubsetD) ultimately have "\ X \ \ (\x\X. TC ` elts x) \ \ (TC ` X)" by simp moreover have "\ (TC ` X) \ \ X \ \ (\x\X. TC ` elts x)" proof (clarsimp simp add: Sup_le_iff assms) show "\x\X. y \ elts x" if "x \ X" "y \ elts (TC x)" "\x\X. \u\elts x. y \ elts (TC u)" for x y using that by (auto simp: TC [of x]) qed ultimately show ?thesis using Sup_Un_distrib TC [of "\X"] image_Union assms by (simp add: image_Union inf_sup_aci(5) sup.absorb_iff2) qed lemma TC': "TC x = x \ TC (\ (elts x))" by (simp add: TC [of x] TC_Sup_distrib) lemma TC_eq_0_iff [simp]: "TC x = 0 \ x=0" using arg_subset_TC by fastforce text\A distinctive induction principle\ lemma TC_induct_down_lemma: assumes ab: "a \ b" and base: "b \ d" and step: "\y z. \y \ b; y \ elts d; z \ elts y\ \ z \ elts d" shows "a \ elts d" proof - have "Transset (TC b \ d)" using Transset_TC unfolding Transset_def by (metis inf.bounded_iff less_TC_def less_eq_V_def local.step subsetI vsubsetD) moreover have "b \ TC b \ d" by (simp add: arg_subset_TC base) ultimately show ?thesis using TC_least [THEN vsubsetD] ab unfolding less_TC_def by (meson TC_least le_inf_iff vsubsetD) qed lemma TC_induct_down [consumes 1, case_names base step small]: assumes "a \ b" and "\y. y \ elts b \ P y" and "\y z. \y \ b; P y; z \ elts y\ \ P z" and "small (Collect P)" shows "P a" using TC_induct_down_lemma [of a b "set (Collect P)"] assms by (metis elts_of_set mem_Collect_eq vsubsetI) subsection\Rank of a set\ definition rank :: "V\V" where "rank a \ transrec (\f x. set (\y\elts x. elts (succ(f y)))) a" lemma rank: "rank a = set(\y \ elts a. elts (succ(rank y)))" by (subst rank_def [THEN def_transrec], simp) lemma rank_Sup: "rank a = \((\y. succ(rank y)) ` elts a)" by (metis elts_Sup image_image rank replacement set_of_elts small_elts) lemma Ord_rank [simp]: "Ord(rank a)" proof (induction a rule: eps_induct) case (step x) then show ?case unfolding rank_Sup [of x] by (metis (mono_tags, lifting) Ord_Sup Ord_succ imageE) qed lemma rank_of_Ord: "Ord i \ rank i = i" by (induction rule: Ord_induct) (metis (no_types, lifting) Ord_equality SUP_cong rank_Sup) lemma Ord_iff_rank: "Ord x \ rank x = x" using Ord_rank [of x] rank_of_Ord by fastforce lemma rank_lt: "a \ elts b \ rank a < rank b" by (metis Ord_linear2 Ord_rank ZFC_in_HOL.SUP_le_iff rank_Sup replacement small_elts succ_le_iff order.irrefl) lemma rank_0 [simp]: "rank 0 = 0" using transrec Ord_0 rank_def rank_of_Ord by presburger lemma rank_succ [simp]: "rank(succ x) = succ(rank x)" proof (rule order_antisym) show "rank (succ x) \ succ (rank x)" by (metis (no_types, lifting) Sup_insert elts_of_set elts_succ image_insert rank small_UN small_elts subset_insertI sup.orderE vsubsetI) show "succ (rank x) \ rank (succ x)" by (metis (mono_tags, lifting) ZFC_in_HOL.Sup_upper elts_succ image_insert insertI1 rank_Sup replacement small_elts) qed lemma rank_mono: "a \ b \ rank a \ rank b" using rank [of a] rank [of b] small_UN by force lemma VsetI: "rank b \ i \ b \ elts (Vset i)" proof (induction i arbitrary: b rule: eps_induct) case (step x) then consider "rank b \ elts x" | "(\y\elts x. rank b \ elts (TC y))" using le_TC_def less_TC_def less_TC_iff by fastforce then have "\y\elts x. b \ Vset y" proof cases case 1 then have "b \ Vset (rank b)" unfolding less_eq_V_def subset_iff by (meson Ord_mem_iff_lt Ord_rank le_TC_refl less_TC_iff rank_lt step.IH) then show ?thesis using "1" by blast next case 2 then show ?thesis using step.IH unfolding less_eq_V_def subset_iff less_TC_def by (meson Ord_mem_iff_lt Ord_rank Transset_TC Transset_def rank_lt vsubsetD) qed then show ?case by (simp add: Vset [of x]) qed lemma Ord_VsetI: "\Ord i; rank b < i\ \ b \ elts (Vset i)" by (meson Ord_mem_iff_lt Ord_rank VsetI arg_subset_TC less_TC_def vsubsetD) lemma arg_le_Vset_rank: "a \ Vset(rank a)" by (simp add: Ord_VsetI rank_lt vsubsetI) lemma two_in_Vset: obtains \ where "x \ elts (Vset \)" "y \ elts (Vset \)" by (metis Ord_rank Ord_VsetI elts_of_set insert_iff rank_lt small_elts small_insert_iff) lemma rank_eq_0_iff [simp]: "rank x = 0 \ x=0" using arg_le_Vset_rank by fastforce lemma small_ranks_imp_small: assumes "small (rank ` A)" shows "small A" proof - define i where "i \ set (\(elts ` (rank ` A)))" have "Ord i" unfolding i_def using Ord_Union Ord_rank assms imageE by blast have *: "Vset (rank x) \ (Vset i)" if "x \ A" for x unfolding i_def by (metis Ord_rank Sup_V_def ZFC_in_HOL.Sup_upper Vfrom_mono assms imageI le_less that) have "A \ elts (VPow (Vset i))" by (meson "*" VPow_iff arg_le_Vset_rank order.trans subsetI) then show ?thesis using down by blast qed lemma rank_Union: "rank(\ A) = \ (rank ` A)" proof (rule order_antisym) have "elts (\y\elts (\ A). succ (rank y)) \ elts (\ (rank ` A))" by clarsimp (meson Ord_mem_iff_lt Ord_rank less_V_def rank_lt vsubsetD) then show "rank (\ A) \ \ (rank ` A)" by (metis less_eq_V_def rank_Sup) show "\ (rank ` A) \ rank (\ A)" proof (cases "small A") case True then show ?thesis by (simp add: ZFC_in_HOL.SUP_le_iff ZFC_in_HOL.Sup_upper rank_mono) next case False then have "\ small (rank ` A)" using small_ranks_imp_small by blast then show ?thesis by blast qed qed lemma small_bounded_rank: "small {x. rank x \ elts a}" proof - have "{x. rank x \ elts a} \ {x. rank x \ a}" using less_TC_iff by auto also have "\ \ elts (Vset a)" using VsetI by blast finally show ?thesis using down by simp qed lemma small_bounded_rank_le: "small {x. rank x \ a}" using small_bounded_rank [of "VPow a"] VPow_iff [of _ a] by simp lemma TC_rank_lt: "a \ b \ rank a < rank b" proof (induction rule: TC_induct_down) case (base y) then show ?case by (simp add: rank_lt) next case (step y z) then show ?case using less_trans rank_lt by blast next case small show ?case using smaller_than_small [OF small_bounded_rank_le [of "rank b"]] by (simp add: Collect_mono less_V_def) qed lemma TC_rank_mem: "x \ y \ rank x \ elts (rank y)" by (simp add: Ord_mem_iff_lt TC_rank_lt) lemma wf_TC_less: "wf {(x,y). x \ y}" proof (rule wf_subset [OF wf_inv_image [OF foundation, of rank]]) show "{(x, y). x \ y} \ inv_image {(x, y). x \ elts y} rank" by (auto simp: TC_rank_mem inv_image_def) qed lemma less_TC_minimal: assumes "P a" obtains x where "P x" "x \ a" "\y. y \ x \ \ P y" using wfE_min' [OF wf_TC_less, of "{x. P x \ x \ a}"] by simp (metis le_TC_def less_le_TC_trans assms) lemma Vfrom_rank_eq: "Vfrom A (rank(x)) = Vfrom A x" proof (rule order_antisym) show "Vfrom A (rank x) \ Vfrom A x" proof (induction x rule: eps_induct) case (step x) have "(\j\elts (rank x). VPow (Vfrom A j)) \ (\j\elts x. VPow (Vfrom A j))" apply (rule Sup_least) apply (clarsimp simp add: rank [of x]) by (meson Ord_in_Ord Ord_rank OrdmemD Vfrom_mono order.trans less_imp_le order.refl step) then show ?case by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2) qed show "Vfrom A x \ Vfrom A (rank x)" proof (induction x rule: eps_induct) case (step x) have "(\j\elts x. VPow (Vfrom A j)) \ (\j\elts (rank x). VPow (Vfrom A j))" using step.IH TC_rank_mem less_TC_iff by force then show ?case by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2) qed qed lemma Vfrom_succ: "Vfrom A (succ(i)) = A \ VPow(Vfrom A i)" by (metis Ord_rank Vfrom_rank_eq Vfrom_succ_Ord rank_succ) lemma Vset_succ_TC: assumes "x \ elts (Vset (ZFC_in_HOL.succ k))" "u \ x" shows "u \ elts (Vset k)" using assms using TC_least Transset_Vfrom Vfrom_succ less_TC_def by auto subsection\Cardinal Numbers\ text\We extend the membership relation to a wellordering\ definition VWO :: "(V \ V) set" where "VWO \ @r. {(x,y). x \ elts y} \ r \ Well_order r \ Field r = UNIV" lemma VWO: "{(x,y). x \ elts y} \ VWO \ Well_order VWO \ Field VWO = UNIV" unfolding VWO_def by (metis (mono_tags, lifting) VWO_def foundation someI_ex total_well_order_extension) lemma wf_VWO: "wf(VWO - Id)" using VWO well_order_on_def by blast lemma wf_Ord_less: "wf {(x, y). Ord y \ x < y}" by (metis (no_types, lifting) Ord_mem_iff_lt eps_induct wfPUNIVI wfP_def) lemma refl_VWO: "refl VWO" using VWO order_on_defs by fastforce lemma trans_VWO: "trans VWO" using VWO by (simp add: VWO wo_rel.TRANS wo_rel_def) lemma antisym_VWO: "antisym VWO" using VWO by (simp add: VWO wo_rel.ANTISYM wo_rel_def) lemma total_VWO: "total VWO" using VWO by (metis wo_rel.TOTAL wo_rel.intro) lemma total_VWOId: "total (VWO-Id)" by (simp add: total_VWO) lemma Linear_order_VWO: "Linear_order VWO" using VWO well_order_on_def by blast lemma wo_rel_VWO: "wo_rel VWO" using VWO wo_rel_def by blast subsubsection \Transitive Closure and VWO\ lemma mem_imp_VWO: "x \ elts y \ (x,y) \ VWO" using VWO by blast lemma less_TC_imp_VWO: "x \ y \ (x,y) \ VWO" unfolding less_TC_def proof (induction y arbitrary: x rule: eps_induct) case (step y' u) then consider "u \ elts y'" | v where "v \ elts y'" "u \ elts (TC v)" by (auto simp: TC [of y']) then show ?case proof cases case 2 then show ?thesis by (meson mem_imp_VWO step.IH transD trans_VWO) qed (use mem_imp_VWO in blast) qed lemma le_TC_imp_VWO: "x \ y \ (x,y) \ VWO" by (metis Diff_iff Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO le_TC_def less_TC_imp_VWO) lemma le_TC_0_iff [simp]: "x \ 0 \ x = 0" by (simp add: le_TC_def) lemma less_TC_succ: " x \ succ \ \ x \ \ \ x = \" by (metis elts_succ insert_iff le_TC_def less_TC_iff) lemma le_TC_succ: "x \ succ \ \ x \ \ \ x = succ \" by (simp add: le_TC_def less_TC_succ) lemma Transset_TC_eq [simp]: "Transset x \ TC x = x" by (simp add: TC_least arg_subset_TC eq_iff) lemma Ord_TC_less_iff: "\Ord \; Ord \\ \ \ \ \ \ \ < \" by (metis Ord_def Ord_mem_iff_lt Transset_TC_eq less_TC_def) lemma Ord_mem_iff_less_TC: "Ord l \ k \ elts l \ k \ l" by (simp add: Ord_def less_TC_def) lemma le_TC_Ord: "\\ \ \; Ord \\ \ Ord \" by (metis Ord_def Ord_in_Ord Transset_TC_eq le_TC_def less_TC_def) lemma Ord_less_TC_mem: assumes "Ord \" "\ \ \" shows "\ \ elts \" using Ord_def assms less_TC_def by auto lemma VWO_TC_le: "\Ord \; Ord \; (\, \) \ VWO\ \ \ \ \" proof (induct \ arbitrary: \ rule: Ord_induct) case (step \) then show ?case by (metis DiffI IdD Linear_order_VWO Linear_order_in_diff_Id Ord_linear Ord_mem_iff_less_TC VWO iso_tuple_UNIV_I le_TC_def mem_imp_VWO) qed lemma VWO_iff_Ord_le [simp]: "\Ord \; Ord \\ \ (\, \) \ VWO \ \ \ \" by (metis VWO_TC_le Ord_TC_less_iff le_TC_def le_TC_imp_VWO le_less) lemma zero_TC_le [iff]: "0 \ y" using le_TC_def nonzero_less_TC by auto lemma succ_le_TC_iff: "Ord j \ succ i \ j \ i \ j" by (metis Ord_in_Ord Ord_linear Ord_mem_iff_less_TC Ord_succ le_TC_def less_TC_succ less_asym_TC) lemma VWO_0_iff [simp]: "(x,0) \ VWO \ x=0" proof show "x = 0" if "(x, 0) \ VWO" using zero_TC_le [of x] le_TC_imp_VWO that by (metis DiffI Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO pair_in_Id_conv) qed auto lemma VWO_antisym: assumes "(x,y) \ VWO" "(y,x) \ VWO" shows "x=y" by (metis Diff_iff IdD Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO assms) subsubsection \Relation VWF\ definition VWF where "VWF \ VWO - Id" lemma wf_VWF [iff]: "wf VWF" by (simp add: VWF_def wf_VWO) lemma trans_VWF [iff]: "trans VWF" by (simp add: VWF_def antisym_VWO trans_VWO trans_diff_Id) lemma asym_VWF [iff]: "asym VWF" - by (metis VWF_def asym.intros irrefl_diff_Id wf_VWF wf_not_sym) + by (metis wf_VWF wf_imp_asym) lemma total_VWF [iff]: "total VWF" using VWF_def total_VWOId by auto lemma total_on_VWF [iff]: "total_on A VWF" by (meson UNIV_I total_VWF total_on_def) lemma VWF_asym: assumes "(x,y) \ VWF" "(y,x) \ VWF" shows False using VWF_def assms wf_VWO wf_not_sym by fastforce lemma VWF_non_refl [iff]: "(x,x) \ VWF" by simp lemma VWF_iff_Ord_less [simp]: "\Ord \; Ord \\ \ (\,\) \ VWF \ \ < \" by (simp add: VWF_def less_V_def) lemma mem_imp_VWF: "x \ elts y \ (x,y) \ VWF" using VWF_def mem_imp_VWO by fastforce subsection\Order types\ definition ordermap :: "'a set \ ('a \ 'a) set \ 'a \ V" where "ordermap A r \ wfrec r (\f x. set (f ` {y \ A. (y,x) \ r}))" definition ordertype :: "'a set \ ('a \ 'a) set \ V" where "ordertype A r \ set (ordermap A r ` A)" lemma ordermap_type: "small A \ ordermap A r \ A \ elts (ordertype A r)" by (simp add: ordertype_def) lemma ordermap_in_ordertype [intro]: "\a \ A; small A\ \ ordermap A r a \ elts (ordertype A r)" by (simp add: ordertype_def) lemma ordermap: "wf r \ ordermap A r a = set (ordermap A r ` {y \ A. (y,a) \ r})" unfolding ordermap_def by (auto simp: wfrec_fixpoint adm_wf_def) lemma wf_Ord_ordermap [iff]: assumes "wf r" "trans r" shows "Ord (ordermap A r x)" using \wf r\ proof (induction x rule: wf_induct_rule) case (less u) have "Transset (set (ordermap A r ` {y \ A. (y, u) \ r}))" proof (clarsimp simp add: Transset_def) show "x \ ordermap A r ` {y \ A. (y, u) \ r}" if "small (ordermap A r ` {y \ A. (y, u) \ r})" and x: "x \ elts (ordermap A r y)" and "y \ A" "(y, u) \ r" for x y proof - have "ordermap A r y = ZFC_in_HOL.set (ordermap A r ` {a \ A. (a, y) \ r})" using ordermap assms(1) by force then have "x \ ordermap A r ` {z \ A. (z, y) \ r}" by (metis (no_types, lifting) elts_of_set empty_iff x) then have "\v. v \ A \ (v, u) \ r \ x = ordermap A r v" using that transD [OF \trans r\] by blast then show ?thesis by blast qed qed moreover have "Ord x" if "x \ elts (set (ordermap A r ` {y \ A. (y, u) \ r}))" for x using that less by (auto simp: split: if_split_asm) ultimately show ?case by (metis (full_types) Ord_def ordermap assms(1)) qed lemma wf_Ord_ordertype: assumes "wf r" "trans r" shows "Ord(ordertype A r)" proof - have "y \ set (ordermap A r ` A)" if "y = ordermap A r x" "x \ A" "small (ordermap A r ` A)" for x y using that by (auto simp: less_eq_V_def ordermap [OF \wf r\, of A x]) moreover have "z \ y" if "y \ ordermap A r ` A" "z \ elts y" for y z by (metis wf_Ord_ordermap OrdmemD assms imageE order.strict_implies_order that) ultimately show ?thesis unfolding ordertype_def Ord_def Transset_def by simp qed lemma Ord_ordertype [simp]: "Ord(ordertype A VWF)" using wf_Ord_ordertype by blast lemma Ord_ordermap [simp]: "Ord (ordermap A VWF x)" by blast lemma ordertype_singleton [simp]: assumes "wf r" shows "ordertype {x} r = 1" proof - have \: "{y. y = x \ (y, x) \ r} = {}" using assms by auto show ?thesis by (auto simp add: ordertype_def assms \ ordermap [where a=x]) qed subsubsection\@{term ordermap} preserves the orderings in both directions\ lemma ordermap_mono: assumes wx: "(w, x) \ r" and "wf r" "w \ A" "small A" shows "ordermap A r w \ elts (ordermap A r x)" proof - have "small {a \ A. (a, x) \ r} \ w \ A \ (w, x) \ r" by (simp add: assms) then show ?thesis using assms ordermap [of r A] by (metis (no_types, lifting) elts_of_set image_eqI mem_Collect_eq replacement) qed lemma converse_ordermap_mono: assumes "ordermap A r y \ elts (ordermap A r x)" "wf r" "total_on A r" "x \ A" "y \ A" "small A" shows "(y, x) \ r" proof (cases "x = y") case True then show ?thesis using assms(1) mem_not_refl by blast next case False then consider "(x,y) \ r" | "(y,x) \ r" using \total_on A r\ assms by (meson UNIV_I total_on_def) then show ?thesis by (meson ordermap_mono assms mem_not_sym) qed lemma converse_ordermap_mono_iff: assumes "wf r" "total_on A r" "x \ A" "y \ A" "small A" shows "ordermap A r y \ elts (ordermap A r x) \ (y, x) \ r" by (metis assms converse_ordermap_mono ordermap_mono) lemma ordermap_surj: "elts (ordertype A r) \ ordermap A r ` A" unfolding ordertype_def by simp lemma ordermap_bij: assumes "wf r" "total_on A r" "small A" shows "bij_betw (ordermap A r) A (elts (ordertype A r))" unfolding bij_betw_def proof (intro conjI) show "inj_on (ordermap A r) A" unfolding inj_on_def by (metis assms mem_not_refl ordermap_mono total_on_def) show "ordermap A r ` A = elts (ordertype A r)" by (metis ordertype_def \small A\ elts_of_set replacement) qed lemma ordermap_eq_iff [simp]: "\x \ A; y \ A; wf r; total_on A r; small A\ \ ordermap A r x = ordermap A r y \ x = y" by (metis bij_betw_iff_bijections ordermap_bij) lemma inv_into_ordermap: "\ \ elts (ordertype A r) \ inv_into A (ordermap A r) \ \ A" by (meson in_mono inv_into_into ordermap_surj) lemma ordertype_nat_imp_finite: assumes "ordertype A r = ord_of_nat m" "small A" "wf r" "total_on A r" shows "finite A" proof - have "A \ elts m" using eqpoll_def assms ordermap_bij by fastforce then show ?thesis using eqpoll_finite_iff finite_Ord_omega by blast qed lemma wf_ordertype_eqpoll: assumes "wf r" "total_on A r" "small A" shows "elts (ordertype A r) \ A" using assms eqpoll_def eqpoll_sym ordermap_bij by blast lemma ordertype_eqpoll: assumes "small A" shows "elts (ordertype A VWF) \ A" using assms wf_ordertype_eqpoll total_VWF wf_VWF by (simp add: wf_ordertype_eqpoll total_on_def) subsection \More advanced @{term ordertype} and @{term ordermap} results\ lemma ordermap_VWF_0 [simp]: "ordermap A VWF 0 = 0" by (simp add: ordermap wf_VWO VWF_def) lemma ordertype_empty [simp]: "ordertype {} r = 0" by (simp add: ordertype_def) lemma ordertype_eq_0_iff [simp]: "\small X; wf r\ \ ordertype X r = 0 \ X = {}" by (metis ordertype_def elts_of_set replacement image_is_empty zero_V_def) lemma ordermap_mono_less: assumes "(w, x) \ r" and "wf r" "trans r" and "w \ A" "x \ A" and "small A" shows "ordermap A r w < ordermap A r x" by (simp add: OrdmemD assms ordermap_mono) lemma ordermap_mono_le: assumes "(w, x) \ r \ w=x" and "wf r" "trans r" and "w \ A" "x \ A" and "small A" shows "ordermap A r w \ ordermap A r x" by (metis assms dual_order.strict_implies_order eq_refl ordermap_mono_less) lemma converse_ordermap_le_mono: assumes "ordermap A r y \ ordermap A r x" "wf r" "total r" "x \ A" "small A" shows "(y, x) \ r \ y=x" by (meson UNIV_I assms mem_not_refl ordermap_mono total_on_def vsubsetD) lemma ordertype_mono: assumes "X \ Y" and r: "wf r" "trans r" and "small Y" shows "ordertype X r \ ordertype Y r" proof - have "small X" using assms smaller_than_small by fastforce have *: "ordermap X r x \ ordermap Y r x" for x using \wf r\ proof (induction x rule: wf_induct_rule) case (less x) have "ordermap X r z < ordermap Y r x" if "z \ X" and zx: "(z,x) \ r" for z using less [OF zx] assms by (meson Ord_linear2 OrdmemD wf_Ord_ordermap ordermap_mono in_mono leD that(1) vsubsetD zx) then show ?case by (auto simp add: ordermap [of _ X x] \small X\ Ord_mem_iff_lt set_image_le_iff less_eq_V_def r) qed show ?thesis proof - have "ordermap Y r ` Y = elts (ordertype Y r)" by (metis ordertype_def \small Y\ elts_of_set replacement) then have "ordertype Y r \ ordermap X r ` X" using "*" \X \ Y\ by fastforce then show ?thesis by (metis Ord_linear2 Ord_mem_iff_lt ordertype_def wf_Ord_ordertype \small X\ elts_of_set replacement r) qed qed corollary ordertype_VWF_mono: assumes "X \ Y" "small Y" shows "ordertype X VWF \ ordertype Y VWF" using assms by (simp add: ordertype_mono) lemma ordertype_UNION_ge: assumes "A \ \" "wf r" "trans r" "\ \ Collect small" "small \" shows "ordertype A r \ ordertype (\\) r" by (rule ordertype_mono) (use assms in auto) lemma inv_ordermap_mono_less: assumes "(inv_into M (ordermap M r) \, inv_into M (ordermap M r) \) \ r" and "small M" and \: "\ \ elts (ordertype M r)" and \: "\ \ elts (ordertype M r)" and "wf r" "trans r" shows "\ < \" proof - have "\ = ordermap M r (inv_into M (ordermap M r) \)" by (metis \ f_inv_into_f ordermap_surj subset_eq) also have "\ < ordermap M r (inv_into M (ordermap M r) \)" by (meson \ \ assms in_mono inv_into_into ordermap_mono_less ordermap_surj) also have "\ = \" by (meson \ f_inv_into_f in_mono ordermap_surj) finally show ?thesis . qed lemma inv_ordermap_mono_eq: assumes "inv_into M (ordermap M r) \ = inv_into M (ordermap M r) \" and "\ \ elts (ordertype M r)" "\ \ elts (ordertype M r)" shows "\ = \" by (metis assms f_inv_into_f ordermap_surj subsetD) lemma inv_ordermap_VWF_mono_le: assumes "inv_into M (ordermap M VWF) \ \ inv_into M (ordermap M VWF) \" and "M \ ON" "small M" and \: "\ \ elts (ordertype M VWF)" and \: "\ \ elts (ordertype M VWF)" shows "\ \ \" proof - have "\ = ordermap M VWF (inv_into M (ordermap M VWF) \)" by (metis \ f_inv_into_f ordermap_surj subset_eq) also have "\ \ ordermap M VWF (inv_into M (ordermap M VWF) \)" by (metis ON_imp_Ord VWF_iff_Ord_less assms dual_order.strict_implies_order elts_of_set eq_refl inv_into_into order.not_eq_order_implies_strict ordermap_mono_less ordertype_def replacement trans_VWF wf_VWF) also have "\ = \" by (meson \ f_inv_into_f in_mono ordermap_surj) finally show ?thesis . qed lemma inv_ordermap_VWF_mono_iff: assumes "M \ ON" "small M" and "\ \ elts (ordertype M VWF)" and "\ \ elts (ordertype M VWF)" shows "inv_into M (ordermap M VWF) \ \ inv_into M (ordermap M VWF) \ \ \ \ \" by (metis ON_imp_Ord Ord_linear_le assms dual_order.eq_iff inv_into_ordermap inv_ordermap_VWF_mono_le) lemma inv_ordermap_VWF_strict_mono_iff: assumes "M \ ON" "small M" and "\ \ elts (ordertype M VWF)" and "\ \ elts (ordertype M VWF)" shows "inv_into M (ordermap M VWF) \ < inv_into M (ordermap M VWF) \ \ \ < \" by (simp add: assms inv_ordermap_VWF_mono_iff less_le_not_le) lemma strict_mono_on_ordertype: assumes "M \ ON" "small M" obtains f where "f \ elts (ordertype M VWF) \ M" "strict_mono_on (elts (ordertype M VWF)) f" proof show "inv_into M (ordermap M VWF) \ elts (ordertype M VWF) \ M" by (meson Pi_I' in_mono inv_into_into ordermap_surj) show "strict_mono_on (elts (ordertype M VWF)) (inv_into M (ordermap M VWF))" proof (clarsimp simp: strict_mono_on_def) fix x y assume "x \ elts (ordertype M VWF)" "y \ elts (ordertype M VWF)" "x < y" then show "inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y" using assms by (meson ON_imp_Ord Ord_linear2 inv_into_into inv_ordermap_VWF_mono_le leD ordermap_surj subsetD) qed qed lemma ordermap_inc_eq: assumes "x \ A" "small A" and \: "\x y. \x\A; y\A; (x,y) \ r\ \ (\ x, \ y) \ s" and r: "wf r" "total_on A r" and "wf s" shows "ordermap (\ ` A) s (\ x) = ordermap A r x" using \wf r\ \x \ A\ proof (induction x rule: wf_induct_rule) case (less x) then have 1: "{y \ A. (y, x) \ r} = A \ {y. (y, x) \ r}" using r by auto have 2: "{y \ \ ` A. (y, \ x) \ s} = \ ` A \ {y. (y, \ x) \ s}" by auto have inv\: "\x y. \x\A; y\A; (\ x, \ y) \ s\ \ (x, y) \ r" by (metis \ \wf s\ \total_on A r\ total_on_def wf_not_sym) have eq: "f ` (\ ` A \ {y. (y, \ x) \ s}) = (f \ \) ` (A \ {y. (y, x) \ r})" for f :: "'b \ V" using less by (auto simp: image_subset_iff inv\ \) show ?case using less by (simp add: ordermap [OF \wf r\, of _ x] ordermap [OF \wf s\, of _ "\ x"] 1 2 eq) qed lemma ordertype_inc_eq: assumes "small A" and \: "\x y. \x\A; y\A; (x,y) \ r\ \ (\ x, \ y) \ s" and r: "wf r" "total_on A r" and "wf s" shows "ordertype (\ ` A) s = ordertype A r" proof - have "ordermap (\ ` A) s (\ x) = ordermap A r x" if "x \ A" for x using assms that by (auto simp: ordermap_inc_eq) then show ?thesis unfolding ordertype_def by (metis (no_types, lifting) image_cong image_image) qed lemma ordertype_inc_le: assumes "small A" "small B" and \: "\x y. \x\A; y\A; (x,y) \ r\ \ (\ x, \ y) \ s" and r: "wf r" "total_on A r" and "wf s" "trans s" and "\ ` A \ B" shows "ordertype A r \ ordertype B s" by (metis assms ordertype_inc_eq ordertype_mono) corollary ordertype_VWF_inc_eq: assumes "A \ ON" "\ ` A \ ON" "small A" and "\x y. \x\A; y\A; x \ \ x < \ y" shows "ordertype (\ ` A) VWF = ordertype A VWF" proof (rule ordertype_inc_eq) show "(\ x, \ y) \ VWF" if "x \ A" "y \ A" "(x, y) \ VWF" for x y using that ON_imp_Ord assms by auto show "total_on A VWF" by (meson UNIV_I total_VWF total_on_def) qed (use assms in auto) lemma ordertype_image_ordermap: assumes "small A" "X \ A" "wf r" "trans r" "total_on X r" shows "ordertype (ordermap A r ` X) VWF = ordertype X r" proof (rule ordertype_inc_eq) show "small X" by (meson assms smaller_than_small) show "(ordermap A r x, ordermap A r y) \ VWF" if "x \ X" "y \ X" "(x, y) \ r" for x y by (meson that wf_Ord_ordermap VWF_iff_Ord_less assms ordermap_mono_less subsetD) qed (use assms in auto) lemma ordertype_map_image: assumes "B \ A" "small A" shows "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF" proof - have "ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)" using assms by auto then have "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (ordermap A VWF ` (A - B)) VWF" by simp also have "\ = ordertype (A - B) VWF" using \small A\ ordertype_image_ordermap by fastforce finally show ?thesis . qed proposition ordertype_le_ordertype: assumes r: "wf r" "total_on A r" and "small A" assumes s: "wf s" "total_on B s" "trans s" and "small B" shows "ordertype A r \ ordertype B s \ (\f \ A \ B. inj_on f A \ (\x \ A. \y \ A. ((x,y) \ r \ (f x, f y) \ s)))" (is "?lhs = ?rhs") proof assume L: ?lhs define f where "f \ inv_into B (ordermap B s) \ ordermap A r" show ?rhs proof (intro bexI conjI ballI impI) have AB: "elts (ordertype A r) \ ordermap B s ` B" by (metis L assms(7) ordertype_def replacement set_of_elts small_elts subset_iff_less_eq_V) have bijA: "bij_betw (ordermap A r) A (elts (ordertype A r))" using ordermap_bij \small A\ r by blast have "inv_into B (ordermap B s) (ordermap A r i) \ B" if "i \ A" for i by (meson L \small A\ inv_into_into ordermap_in_ordertype ordermap_surj subsetD that vsubsetD) then show "f \ A \ B" by (auto simp: Pi_iff f_def) show "inj_on f A" proof (clarsimp simp add: f_def inj_on_def) fix x y assume "x \ A" "y \ A" and "inv_into B (ordermap B s) (ordermap A r x) = inv_into B (ordermap B s) (ordermap A r y)" then have "ordermap A r x = ordermap A r y" by (meson AB \small A\ inv_into_injective ordermap_in_ordertype subsetD) then show "x = y" by (metis \x \ A\ \y \ A\ bijA bij_betw_inv_into_left) qed next fix x y assume "x \ A" "y \ A" and "(x, y) \ r" have \: "ordermap A r y \ ordermap B s ` B" by (meson L \y \ A\ \small A\ in_mono ordermap_in_ordertype ordermap_surj vsubsetD) moreover have \: "\x. inv_into B (ordermap B s) (ordermap A r x) = f x" by (simp add: f_def) then have *: "ordermap B s (f y) = ordermap A r y" using \ by (metis f_inv_into_f) moreover have "ordermap A r x \ ordermap B s ` B" by (meson L \x \ A\ \small A\ in_mono ordermap_in_ordertype ordermap_surj vsubsetD) moreover have "ordermap A r x < ordermap A r y" using * r s by (metis (no_types) wf_Ord_ordermap OrdmemD \(x, y) \ r\ \x \ A\ \small A\ ordermap_mono) ultimately show "(f x, f y) \ s" using \ s by (metis assms(7) f_inv_into_f inv_into_into less_asym ordermap_mono_less total_on_def) qed next assume R: ?rhs then obtain f where f: "f\A \ B" "inj_on f A" "\x\A. \y\A. (x, y) \ r \ (f x, f y) \ s" by blast show ?lhs by (rule ordertype_inc_le [where \=f]) (use f assms in auto) qed lemma iso_imp_ordertype_eq_ordertype: assumes iso: "iso r r' f" and "wf r" and "Total r" and sm: "small (Field r)" shows "ordertype (Field r) r = ordertype (Field r') r'" by (metis (no_types, lifting) iso_forward iso_wf assms iso_Field ordertype_inc_eq sm) lemma ordertype_infinite_ge_\: assumes "infinite A" "small A" shows "ordertype A VWF \ \" proof - have "inj_on (ordermap A VWF) A" by (meson ordermap_bij \small A\ bij_betw_def total_on_VWF wf_VWF) then have "infinite (ordermap A VWF ` A)" using \infinite A\ finite_image_iff by blast then show ?thesis using Ord_ordertype \small A\ infinite_Ord_omega by (auto simp: ordertype_def) qed lemma ordertype_eqI: assumes "wf r" "total_on A r" "small A" "wf s" "bij_betw f A B" "(\x \ A. \y \ A. (f x, f y) \ s \ (x,y) \ r)" shows "ordertype A r = ordertype B s" by (metis assms bij_betw_imp_surj_on ordertype_inc_eq) lemma ordermap_eq_self: assumes "Ord \" and x: "x \ elts \" shows "ordermap (elts \) VWF x = x" using Ord_in_Ord [OF assms] x proof (induction x rule: Ord_induct) case (step x) have 1: "{y \ elts \. (y, x) \ VWF} = elts x" (is "?A = _") proof show "?A \ elts x" using \Ord \\ by clarify (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less step.hyps) show "elts x \ ?A" using \Ord \\ by clarify (meson Ord_in_Ord Ord_trans OrdmemD VWF_iff_Ord_less step.prems) qed show ?case using step by (simp add: ordermap [OF wf_VWF, of _ x] 1 Ord_trans [of _ _ \] step.prems \Ord \\ cong: image_cong) qed lemma ordertype_eq_Ord [simp]: assumes "Ord \" shows "ordertype (elts \) VWF = \" using assms ordermap_eq_self [OF assms] by (simp add: ordertype_def) proposition ordertype_eq_iff: assumes \: "Ord \" and r: "wf r" and "small A" "total_on A r" "trans r" shows "ordertype A r = \ \ (\f. bij_betw f A (elts \) \ (\x \ A. \y \ A. f x < f y \ (x,y) \ r))" (is "?lhs = ?rhs") proof safe assume eq: "\ = ordertype A r" show "\f. bij_betw f A (elts (ordertype A r)) \ (\x\A. \y\A. f x < f y \ ((x, y) \ r))" proof (intro exI conjI ballI) show "bij_betw (ordermap A r) A (elts (ordertype A r))" by (simp add: assms ordermap_bij) then show "ordermap A r x < ordermap A r y \ (x, y) \ r" if "x \ A" "y \ A" for x y using that assms by (metis order.asym ordermap_mono_less total_on_def) qed next fix f assume f: "bij_betw f A (elts \)" "\x\A. \y\A. f x < f y \ (x, y) \ r" have "ordertype A r = ordertype (elts \) VWF" proof (rule ordertype_eqI) show "\x\A. \y\A. ((f x, f y) \ VWF) = ((x, y) \ r)" by (meson Ord_in_Ord VWF_iff_Ord_less \ bij_betwE f) qed (use assms f in auto) then show ?lhs by (simp add: \) qed corollary ordertype_VWF_eq_iff: assumes "Ord \" "small A" shows "ordertype A VWF = \ \ (\f. bij_betw f A (elts \) \ (\x \ A. \y \ A. f x < f y \ (x,y) \ VWF))" by (metis UNIV_I assms ordertype_eq_iff total_VWF total_on_def trans_VWF wf_VWF) lemma ordertype_le_Ord: assumes "Ord \" "X \ elts \" shows "ordertype X VWF \ \" by (metis assms ordertype_VWF_mono ordertype_eq_Ord small_elts) lemma ordertype_inc_le_Ord: assumes "small A" "Ord \" and \: "\x y. \x\A; y\A; (x,y) \ r\ \ \ x < \ y" and "wf r" "total_on A r" and sub: "\ ` A \ elts \" shows "ordertype A r \ \" proof - have "\x y. \x\A; y\A; (x,y) \ r\ \ (\ x, \ y) \ VWF" by (meson Ord_in_Ord VWF_iff_Ord_less \ \Ord \\ sub image_subset_iff) with assms show ?thesis by (metis ordertype_inc_eq ordertype_le_Ord wf_VWF) qed lemma le_ordertype_obtains_subset: assumes \: "\ \ \" "ordertype H VWF = \" and "small H" "Ord \" obtains G where "G \ H" "ordertype G VWF = \" proof (intro exI conjI that) let ?f = "ordermap H VWF" show \: "inv_into H ?f ` elts \ \ H" unfolding image_subset_iff by (metis \ inv_into_into ordermap_surj subsetD vsubsetD) have "\f. bij_betw f (inv_into H ?f ` elts \) (elts \) \ (\x\inv_into H ?f ` elts \. \y\inv_into H ?f ` elts \. (f x < f y) = ((x, y) \ VWF))" proof (intro exI conjI ballI iffI) show "bij_betw ?f (inv_into H ?f ` elts \) (elts \)" using ordermap_bij [OF wf_VWF total_on_VWF \small H\] \ by (metis bij_betw_inv_into_RIGHT bij_betw_subset less_eq_V_def \) next fix x y assume x: "x \ inv_into H ?f ` elts \" and y: "y \ inv_into H ?f ` elts \" show "?f x < ?f y" if "(x,y) \ VWF" using that \ \small H\ in_mono ordermap_mono_less x y by fastforce show "(x,y) \ VWF" if "?f x < ?f y" using that \ \small H\ in_mono ordermap_mono_less [OF _ wf_VWF trans_VWF] x y by (metis UNIV_I less_imp_not_less total_VWF total_on_def) qed then show "ordertype (inv_into H ?f ` elts \) VWF = \" by (subst ordertype_eq_iff) (use assms in auto) qed lemma ordertype_infinite_\: assumes "A \ elts \" "infinite A" shows "ordertype A VWF = \" proof (rule antisym) show "ordertype A VWF \ \" by (simp add: assms ordertype_le_Ord) show "\ \ ordertype A VWF" using assms down ordertype_infinite_ge_\ by auto qed text \For infinite sets of natural numbers\ lemma ordertype_nat_\: assumes "infinite N" shows "ordertype N less_than = \" proof - have "small N" by (meson inj_on_def ord_of_nat_inject small_def small_iff_range small_image_nat_V) have "ordertype (ord_of_nat ` N) VWF = \" by (force simp: assms finite_image_iff inj_on_def intro: ordertype_infinite_\) moreover have "ordertype (ord_of_nat ` N) VWF = ordertype N less_than" by (auto intro: ordertype_inc_eq \small N\) ultimately show ?thesis by simp qed proposition ordertype_eq_ordertype: assumes r: "wf r" "total_on A r" "trans r" and "small A" assumes s: "wf s" "total_on B s" "trans s" and "small B" shows "ordertype A r = ordertype B s \ (\f. bij_betw f A B \ (\x \ A. \y \ A. (f x, f y) \ s \ (x,y) \ r))" (is "?lhs = ?rhs") proof assume L: ?lhs define \ where "\ = ordertype A r" have A: "bij_betw (ordermap A r) A (ordermap A r ` A)" by (meson ordermap_bij assms(4) bij_betw_def r) have B: "bij_betw (ordermap B s) B (ordermap B s ` B)" by (meson ordermap_bij assms(8) bij_betw_def s) define f where "f \ inv_into B (ordermap B s) \ ordermap A r" show ?rhs proof (intro exI conjI) have bijA: "bij_betw (ordermap A r) A (elts \)" unfolding \_def using ordermap_bij \small A\ r by blast moreover have bijB: "bij_betw (ordermap B s) B (elts \)" by (simp add: L \_def ordermap_bij \small B\ s) ultimately show bij: "bij_betw f A B" unfolding f_def using bij_betw_comp_iff bij_betw_inv_into by blast have invB: "\\. \ \ elts \ \ ordermap B s (inv_into B (ordermap B s) \) = \" by (meson bijB bij_betw_inv_into_right) have ordermap_A_\: "\a. a \ A \ ordermap A r a \ elts \" using bijA bij_betwE by auto have f_in_B: "\a. a \ A \ f a \ B" using bij bij_betwE by fastforce show "\x\A. \y\A. (f x, f y) \ s \ (x, y) \ r" proof (intro iffI ballI) fix x y assume "x \ A" "y \ A" and ins: "(f x, f y) \ s" then have "ordermap A r x < ordermap A r y" unfolding o_def by (metis (mono_tags, lifting) f_def \small B\ comp_apply f_in_B invB ordermap_A_\ ordermap_mono_less s(1) s(3)) then show "(x, y) \ r" by (metis \x \ A\ \y \ A\ \small A\ order.asym ordermap_mono_less r total_on_def) next fix x y assume "x \ A" "y \ A" and "(x, y) \ r" then have "ordermap A r x < ordermap A r y" by (simp add: \small A\ ordermap_mono_less r) then have "(f y, f x) \ s" by (metis (mono_tags, lifting) \x \ A\ \y \ A\ \small B\ comp_apply f_def f_in_B invB order.asym ordermap_A_\ ordermap_mono_less s(1) s(3)) moreover have "f y \ f x" by (metis \(x, y) \ r\ \x \ A\ \y \ A\ bij bij_betw_inv_into_left r(1) wf_not_sym) ultimately show "(f x, f y) \ s" by (meson \x \ A\ \y \ A\ f_in_B s(2) total_on_def) qed qed next assume ?rhs then show ?lhs using assms ordertype_eqI by blast qed corollary ordertype_eq_ordertype_iso: assumes r: "wf r" "total_on A r" "trans r" and "small A" and FA: "Field r = A" assumes s: "wf s" "total_on B s" "trans s" and "small B" and FB: "Field s = B" shows "ordertype A r = ordertype B s \ (\f. iso r s f)" (is "?lhs = ?rhs") proof assume L: ?lhs then obtain f where "bij_betw f A B" "\x \ A. \y \ A. (f x, f y) \ s \ (x,y) \ r" using assms ordertype_eq_ordertype by blast then show ?rhs using FA FB iso_iff2 by blast next assume ?rhs then show ?lhs using FA FB \small A\ iso_imp_ordertype_eq_ordertype r by blast qed lemma Limit_ordertype_imp_Field_Restr: assumes Lim: "Limit (ordertype A r)" and r: "wf r" "total_on A r" and "small A" shows "Field (Restr r A) = A" proof - have "\y\A. (x,y) \ r" if "x \ A" for x proof - let ?oy = "succ (ordermap A r x)" have \
: "?oy \ elts (ordertype A r)" by (simp add: Lim \small A\ ordermap_in_ordertype succ_in_Limit_iff that) then have A: "inv_into A (ordermap A r) ?oy \ A" by (simp add: inv_into_ordermap) moreover have "(x, inv_into A (ordermap A r) ?oy) \ r" proof - have "ordermap A r x \ elts (ordermap A r (inv_into A (ordermap A r) ?oy))" by (metis "\
" elts_succ f_inv_into_f insert_iff ordermap_surj subsetD) then show ?thesis by (metis \small A\ A converse_ordermap_mono r that) qed ultimately show ?thesis .. qed then have "A \ Field (Restr r A)" by (auto simp: Field_def) then show ?thesis by (simp add: Field_Restr_subset subset_antisym) qed lemma ordertype_Field_Restr: assumes "wf r" "total_on A r" "trans r" "small A" "Field (Restr r A) = A" shows "ordertype (Field (Restr r A)) (Restr r A) = ordertype A r" using assms by (force simp: ordertype_eq_ordertype wf_Restr total_on_def trans_Restr) proposition ordertype_eq_ordertype_iso_Restr: assumes r: "wf r" "total_on A r" "trans r" and "small A" and FA: "Field (Restr r A) = A" assumes s: "wf s" "total_on B s" "trans s" and "small B" and FB: "Field (Restr s B) = B" shows "ordertype A r = ordertype B s \ (\f. iso (Restr r A) (Restr s B) f)" (is "?lhs = ?rhs") proof assume L: ?lhs then obtain f where "bij_betw f A B" "\x \ A. \y \ A. (f x, f y) \ s \ (x,y) \ r" using assms ordertype_eq_ordertype by blast then show ?rhs using FA FB bij_betwE unfolding iso_iff2 by fastforce next assume ?rhs moreover have "ordertype (Field (Restr r A)) (Restr r A) = ordertype A r" using FA \small A\ ordertype_Field_Restr r by blast moreover have "ordertype (Field (Restr s B)) (Restr s B) = ordertype B s" using FB \small B\ ordertype_Field_Restr s by blast ultimately show ?lhs using iso_imp_ordertype_eq_ordertype FA FB \small A\ r by (fastforce intro: total_on_imp_Total_Restr trans_Restr wf_Int1) qed lemma ordermap_insert: assumes "Ord \" and y: "Ord y" "y \ \" and U: "U \ elts \" shows "ordermap (insert \ U) VWF y = ordermap U VWF y" using y proof (induction rule: Ord_induct) case (step y) then have 1: "{u \ U. (u, y) \ VWF} = elts y \ U" apply (simp add: set_eq_iff) by (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less assms subsetD) have 2: "{u \ insert \ U. (u, y) \ VWF} = elts y \ U" apply (simp add: set_eq_iff) by (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less assms leD step.hyps step.prems subsetD) show ?case using step apply (simp only: ordermap [OF wf_VWF, of _ y] 1 2) by (meson Int_lower1 Ord_is_Transset Sup.SUP_cong Transset_def assms(1) in_mono vsubsetD) qed lemma ordertype_insert: assumes "Ord \" and U: "U \ elts \" shows "ordertype (insert \ U) VWF = succ (ordertype U VWF)" proof - have \: "{y \ insert \ U. (y, \) \ VWF} = U" "{y \ U. (y, \) \ VWF} = U" using Ord_in_Ord OrdmemD assms by auto have eq: "\x. x \ U \ ordermap (insert \ U) VWF x = ordermap U VWF x" by (meson Ord_in_Ord Ord_is_Transset Transset_def U assms(1) in_mono ordermap_insert) have "ordertype (insert \ U) VWF = ZFC_in_HOL.set (insert (ordermap U VWF \) (ordermap U VWF ` U))" by (simp add: ordertype_def ordermap_insert assms eq) also have "\ = succ (ZFC_in_HOL.set (ordermap U VWF ` U))" using "\" U by (simp add: ordermap [OF wf_VWF, of _ \] down succ_def vinsert_def) also have "\ = succ (ordertype U VWF)" by (simp add: ordertype_def) finally show ?thesis . qed lemma finite_ordertype_le_card: assumes "finite A" "wf r" "trans r" shows "ordertype A r \ ord_of_nat (card A)" proof - have "Ord (ordertype A r)" by (simp add: wf_Ord_ordertype assms) moreover have "ordermap A r ` A = elts (ordertype A r)" by (simp add: ordertype_def finite_imp_small \finite A\) moreover have "card (ordermap A r ` A) \ card A" using \finite A\ card_image_le by blast ultimately show ?thesis by (metis Ord_linear_le Ord_ord_of_nat \finite A\ card_ord_of_nat card_seteq finite_imageI less_eq_V_def) qed lemma ordertype_VWF_\: assumes "finite A" shows "ordertype A VWF \ elts \" proof - have "finite (ordermap A VWF ` A)" using assms by blast then have "ordertype A VWF < \" by (meson Ord_\ OrdmemD trans_VWF wf_VWF assms finite_ordertype_le_card le_less_trans ord_of_nat_\) then show ?thesis by (simp add: Ord_mem_iff_lt) qed lemma ordertype_VWF_finite_nat: assumes "finite A" shows "ordertype A VWF = ord_of_nat (card A)" by (metis finite_imp_small ordermap_bij total_on_VWF wf_VWF \_def assms bij_betw_same_card card_ord_of_nat elts_of_set f_inv_into_f inf ordertype_VWF_\) lemma finite_ordertype_eq_card: assumes "small A" "wf r" "trans r" "total_on A r" shows "ordertype A r = ord_of_nat m \ finite A \ card A = m" using ordermap_bij [OF \wf r\] proof - have *: "bij_betw (ordermap A r) A (elts (ordertype A r))" by (simp add: assms ordermap_bij) moreover have "card (ordermap A r ` A) = card A" by (meson bij_betw_def * card_image) ultimately show ?thesis using assms bij_betw_finite bij_betw_imp_surj_on finite_Ord_omega ordertype_VWF_finite_nat wf_Ord_ordertype by fastforce qed lemma ex_bij_betw_strict_mono_card: assumes "finite M" "M \ ON" obtains h where "bij_betw h {..finite M\ ordermap_bij ordertype_VWF_finite_nat by fastforce let ?h = "(inv_into M (ordermap M VWF)) \ ord_of_nat" show thesis proof show bijh: "bij_betw ?h {.. elts (ordertype M VWF)" "n \ elts (ordertype M VWF)" using \m < n\ \n < card M\ \finite M\ ordertype_VWF_finite_nat by auto have ord: "Ord (?h m)" "Ord (?h n)" using bijh assms(2) bij_betwE that by fastforce+ moreover assume "\ ?h m < ?h n" ultimately consider "?h m = ?h n" | "?h m > ?h n" using Ord_linear_lt by blast then show False proof cases case 1 then have "m = n" by (metis inv_ordermap_mono_eq mn comp_apply ord_of_nat_inject) with \m < n\ show False by blast next case 2 then have "ord_of_nat n \ ord_of_nat m" by (metis Finite_V mn assms comp_def inv_ordermap_VWF_mono_le less_imp_le) then show ?thesis using leD \m < n\ by blast qed qed with assms show ?thesis by (auto simp: strict_mono_on_def) qed qed qed lemma ordertype_finite_less_than [simp]: assumes "finite A" shows "ordertype A less_than = card A" proof - let ?M = "ord_of_nat ` A" obtain M: "finite ?M" "?M \ ON" using Ord_ord_of_nat assms by blast have "ordertype A less_than = ordertype ?M VWF" by (rule ordertype_inc_eq [symmetric]) (use assms finite_imp_small total_on_def in \force+\) also have "\ = card A" proof (subst ordertype_eq_iff) let ?M = "ord_of_nat ` A" obtain h where bijh: "bij_betw h {.. ord_of_nat \ inv_into {..f. bij_betw f ?M (elts (card A)) \ (\x\?M. \y\?M. f x < f y \ ((x, y) \ VWF))" proof (intro exI conjI ballI) have "bij_betw (ord_of_nat \ inv_into {.. ?M" "y \ ?M" then obtain m n where "x = ord_of_nat m" "y = ord_of_nat n" by auto have "(f x < f y) \ ((h \ inv_into {.. inv_into {.. = (x < y)" using bijh by (simp add: bij_betw_inv_into_right xy) also have "\ \ ((x, y) \ VWF)" using M(2) ON_imp_Ord xy by auto finally show "(f x < f y) \ ((x, y) \ VWF)" . qed qed auto finally show ?thesis . qed subsection \Cardinality of an arbitrary HOL set\ definition gcard :: "'a set \ V" where "gcard X \ if small X then (LEAST i. Ord i \ elts i \ X) else 0" subsection\Cardinality of a set\ definition vcard :: "V\V" where "vcard a \ (LEAST i. Ord i \ elts i \ elts a)" lemma gcard_eq_vcard [simp]: "gcard (elts x) = vcard x" by (simp add: vcard_def gcard_def) definition Card:: "V\bool" where "Card i \ i = vcard i" abbreviation CARD where "CARD \ Collect Card" lemma cardinal_cong: "elts x \ elts y \ vcard x = vcard y" unfolding vcard_def by (meson eqpoll_sym eqpoll_trans) lemma gcardinal_cong: assumes "X \ Y" shows "gcard X = gcard Y" proof - have "(LEAST i. Ord i \ elts i \ X) = (LEAST i. Ord i \ elts i \ Y)" by (meson eqpoll_sym eqpoll_trans assms) then show ?thesis unfolding gcard_def by (meson eqpoll_sym small_eqcong assms) qed lemma vcard_set_image: "inj_on f (elts x) \ vcard (set (f ` elts x)) = vcard x" by (simp add: cardinal_cong) lemma gcard_image: "inj_on f X \ gcard (f ` X) = gcard X" by (simp add: gcardinal_cong) lemma Card_cardinal_eq: "Card \ \ vcard \ = \" by (simp add: Card_def) lemma Card_is_Ord: assumes "Card \" shows "Ord \" proof - obtain \ where "Ord \" "elts \ \ elts \" using Ord_ordertype ordertype_eqpoll by blast then have "Ord (LEAST i. Ord i \ elts i \ elts \)" by (metis Ord_Least) then show ?thesis using Card_def vcard_def assms by auto qed lemma cardinal_eqpoll: "elts (vcard a) \ elts a" unfolding vcard_def using ordertype_eqpoll [of "elts a"] Ord_LeastI by (meson Ord_ordertype small_elts) lemma inj_into_vcard: obtains f where "f \ elts A \ elts (vcard A)" "inj_on f (elts A)" using cardinal_eqpoll [of A] inj_on_the_inv_into the_inv_into_onto by (fastforce simp: Pi_iff bij_betw_def eqpoll_def) lemma cardinal_idem [simp]: "vcard (vcard a) = vcard a" using cardinal_cong cardinal_eqpoll by blast lemma subset_smaller_vcard: assumes "\ \ vcard x" "Card \" obtains y where "y \ x" "vcard y = \" proof - obtain \ where \: "bij_betw \ (elts (vcard x)) (elts x)" using cardinal_eqpoll eqpoll_def by blast show thesis proof let ?y = "ZFC_in_HOL.set (\ ` elts \)" show "?y \ x" by (meson \ assms bij_betwE set_image_le_iff small_elts vsubsetD) show "vcard ?y = \" by (metis vcard_set_image Card_def assms bij_betw_def bij_betw_subset \ less_eq_V_def) qed qed text\every natural number is a (finite) cardinal\ lemma nat_into_Card: assumes "\ \ elts \" shows "Card(\)" proof (unfold Card_def vcard_def, rule sym) obtain n where n: "\ = ord_of_nat n" by (metis \_def assms elts_of_set imageE inf) have "Ord(\)" using assms by auto moreover { fix \ assume "\ < \" "Ord \" "elts \ \ elts \" with n have "elts \ \ {..Ord \\ \\ < \\ \Ord(\)\ by (metis \elts \ \ elts \\ card_seteq eqpoll_finite_iff eqpoll_iff_card finite_lessThan less_eq_V_def less_le_not_le order_refl) } ultimately show "(LEAST i. Ord i \ elts i \ elts \) = \" by (metis (no_types, lifting) Least_equality Ord_linear_le eqpoll_refl less_le_not_le) qed lemma Card_ord_of_nat [simp]: "Card (ord_of_nat n)" by (simp add: \_def nat_into_Card) lemma Card_0 [iff]: "Card 0" by (simp add: nat_into_Card) lemma CardI: "\Ord i; \j. \j < i; Ord j\ \ \ elts j \ elts i\ \ Card i" unfolding Card_def vcard_def by (metis Ord_Least Ord_linear_lt cardinal_eqpoll eqpoll_refl not_less_Ord_Least vcard_def) lemma vcard_0 [simp]: "vcard 0 = 0" using Card_0 Card_def by auto lemma Ord_cardinal [simp,intro!]: "Ord(vcard a)" unfolding vcard_def by (metis Card_def Card_is_Ord cardinal_cong cardinal_eqpoll vcard_def) lemma gcard_big_0: "\ small X \ gcard X = 0" by (simp add: gcard_def) lemma gcard_eq_card: assumes "finite X" shows "gcard X = ord_of_nat (card X)" proof - have "\y. Ord y \ elts y \ X \ ord_of_nat (card X) \ y" by (metis assms eqpoll_finite_iff eqpoll_iff_card order_le_less ordertype_VWF_finite_nat ordertype_eq_Ord) then have "(LEAST i. Ord i \ elts i \ X) = ord_of_nat (card X)" by (simp add: assms eqpoll_iff_card finite_Ord_omega Least_equality) with assms show ?thesis by (simp add: finite_imp_small gcard_def) qed lemma gcard_empty_0 [simp]: "gcard {} = 0" by (simp add: gcard_eq_card) lemma gcard_single_1 [simp]: "gcard {x} = 1" by (simp add: gcard_eq_card one_V_def) lemma Card_gcard [iff]: "Card (gcard X)" by (metis Card_0 Card_def cardinal_idem gcard_big_0 gcardinal_cong small_eqpoll gcard_eq_vcard) lemma gcard_eqpoll: "small X \ elts (gcard X) \ X" by (metis cardinal_eqpoll eqpoll_trans gcard_eq_vcard gcardinal_cong small_eqpoll) lemma lepoll_imp_gcard_le: assumes "A \ B" "small B" shows "gcard A \ gcard B" proof - have "elts (gcard A) \ A" "elts (gcard B) \ B" by (meson assms gcard_eqpoll lepoll_small)+ with \A \ B\ show ?thesis by (metis Ord_cardinal Ord_linear2 eqpoll_sym gcard_eq_vcard gcardinal_cong lepoll_antisym lepoll_trans2 less_V_def less_eq_V_def subset_imp_lepoll) qed lemma gcard_image_le: assumes "small A" shows "gcard (f ` A) \ gcard A" using assms image_lepoll lepoll_imp_gcard_le by blast lemma subset_imp_gcard_le: assumes "A \ B" "small B" shows "gcard A \ gcard B" by (simp add: assms lepoll_imp_gcard_le subset_imp_lepoll) lemma gcard_le_lepoll: "\gcard A \ \; small A\ \ A \ elts \" by (meson eqpoll_sym gcard_eqpoll lepoll_trans1 less_eq_V_def subset_imp_lepoll) subsection\Cardinality of a set\ text\The cardinals are the initial ordinals.\ lemma Card_iff_initial: "Card \ \ Ord \ \ (\\. Ord \ \ \ < \ \ ~ elts \ \ elts \)" by (metis CardI Card_def Card_is_Ord not_less_Ord_Least vcard_def) lemma Card_\ [iff]: "Card \" by (meson CardI Ord_\ eqpoll_finite_iff infinite_Ord_omega infinite_\ leD) lemma lt_Card_imp_lesspoll: "\i < a; Card a; Ord i\ \ elts i \ elts a" by (meson Card_iff_initial less_eq_V_def less_imp_le lesspoll_def subset_imp_lepoll) lemma lepoll_imp_Card_le: assumes "elts a \ elts b" shows "vcard a \ vcard b" using assms lepoll_imp_gcard_le by fastforce lemma lepoll_cardinal_le: "\elts A \ elts i; Ord i\ \ vcard A \ i" by (metis Ord_Least Ord_linear2 dual_order.trans eqpoll_refl lepoll_imp_Card_le not_less_Ord_Least vcard_def) lemma cardinal_le_lepoll: "vcard A \ \ \ elts A \ elts \" by (meson cardinal_eqpoll eqpoll_sym lepoll_trans1 less_eq_V_def subset_imp_lepoll) lemma lesspoll_imp_Card_less: assumes "elts a \ elts b" shows "vcard a < vcard b" by (metis assms cardinal_eqpoll eqpoll_sym eqpoll_trans lepoll_imp_Card_le less_V_def lesspoll_def) lemma Card_Union [simp,intro]: assumes A: "\x. x \ A \ Card(x)" shows "Card(\A)" proof (rule CardI) show "Ord(\A)" using A by (simp add: Card_is_Ord Ord_Sup) next fix j assume j: "j < \A" "Ord j" hence "\c\A. j < c \ Card(c)" using A by (meson Card_is_Ord Ord_linear2 ZFC_in_HOL.Sup_least leD) then obtain c where c: "c\A" "j < c" "Card(c)" by blast hence jls: "elts j \ elts c" using j(2) lt_Card_imp_lesspoll by blast { assume eqp: "elts j \ elts (\A)" have "elts c \ elts (\A)" using c by (metis Card_def Sup_V_def ZFC_in_HOL.Sup_upper cardinal_le_lepoll j(1) not_less_0) also have "... \ elts j" by (rule eqpoll_sym [OF eqp]) also have "... \ elts c" by (rule jls) finally have "elts c \ elts c" . hence False by auto } thus "\ elts j \ elts (\A)" by blast qed lemma Card_UN: "(\x. x \ A \ Card(K x)) ==> Card(Sup (K ` A))" by blast subsection\Transfinite recursion for definitions based on the three cases of ordinals\ definition transrec3 :: "[V, [V,V]\V, [V,V\V]\V, V] \ V" where "transrec3 a b c \ transrec (\r x. if x=0 then a else if Limit x then c x (\y \ elts x. r y) else b(pred x) (r (pred x)))" lemma transrec3_0 [simp]: "transrec3 a b c 0 = a" by (simp add: transrec transrec3_def) lemma transrec3_succ [simp]: "transrec3 a b c (succ i) = b i (transrec3 a b c i)" by (simp add: transrec transrec3_def) lemma transrec3_Limit [simp]: "Limit i \ transrec3 a b c i = c i (\j \ elts i. transrec3 a b c j)" unfolding transrec3_def by (subst transrec) auto subsection \Cardinal Addition\ definition cadd :: "[V,V]\V" (infixl \\\ 65) where "\ \ \ \ vcard (\ \ \)" subsubsection\Cardinal addition is commutative\ lemma vsum_commute_eqpoll: "elts (a\b) \ elts (b\a)" proof - have "bij_betw (\z \ elts (a\b). sum_case Inr Inl z) (elts (a\b)) (elts (b\a))" unfolding bij_betw_def proof (intro conjI inj_onI) show "restrict (sum_case Inr Inl) (elts (a \ b)) ` elts (a \ b) = elts (b \ a)" apply auto apply (metis (no_types) imageI sum_case_Inr sum_iff) by (metis Inl_in_sum_iff imageI sum_case_Inl) qed auto then show ?thesis using eqpoll_def by blast qed lemma cadd_commute: "i \ j = j \ i" by (simp add: cadd_def cardinal_cong vsum_commute_eqpoll) subsubsection\Cardinal addition is associative\ lemma sum_assoc_bij: "bij_betw (\z \ elts ((a\b)\c). sum_case(sum_case Inl (\y. Inr(Inl y))) (\y. Inr(Inr y)) z) (elts ((a\b)\c)) (elts (a\(b\c)))" by (rule_tac f' = "sum_case (\x. Inl (Inl x)) (sum_case (\x. Inl (Inr x)) Inr)" in bij_betw_byWitness) auto lemma sum_assoc_eqpoll: "elts ((a\b)\c) \ elts (a\(b\c))" unfolding eqpoll_def by (metis sum_assoc_bij) lemma elts_vcard_vsum_eqpoll: "elts (vcard (i \ j)) \ Inl ` elts i \ Inr ` elts j" proof - have "elts (i \ j) \ Inl ` elts i \ Inr ` elts j" by (simp add: elts_vsum) then show ?thesis using cardinal_eqpoll eqpoll_trans by blast qed lemma cadd_assoc: "(i \ j) \ k = i \ (j \ k)" proof (unfold cadd_def, rule cardinal_cong) have "elts (vcard(i \ j) \ k) \ elts ((i \ j) \ k)" by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll intro: Un_eqpoll_cong) also have "\ \ elts (i \ (j \ k))" by (rule sum_assoc_eqpoll) also have "\ \ elts (i \ vcard(j \ k))" by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll [THEN eqpoll_sym] intro: Un_eqpoll_cong) finally show "elts (vcard (i \ j) \ k) \ elts (i \ vcard (j \ k))" . qed lemma cadd_left_commute: "j \ (i \ k) = i \ (j \ k)" using cadd_assoc cadd_commute by force lemmas cadd_ac = cadd_assoc cadd_commute cadd_left_commute text\0 is the identity for addition\ lemma vsum_0_eqpoll: "elts (0\a) \ elts a" by (simp add: elts_vsum) lemma cadd_0 [simp]: "Card \ \ 0 \ \ = \" by (metis Card_def cadd_def cardinal_cong vsum_0_eqpoll) lemma cadd_0_right [simp]: "Card \ \ \ \ 0 = \" by (simp add: cadd_commute) lemma vsum_lepoll_self: "elts a \ elts (a\b)" unfolding elts_vsum by (meson Inl_iff Un_upper1 inj_onI lepoll_def) lemma cadd_le_self: assumes \: "Card \" shows "\ \ \ \ a" proof (unfold cadd_def) have "\ \ vcard \" using Card_def \ by auto also have "\ \ vcard (\ \ a)" by (simp add: lepoll_imp_Card_le vsum_lepoll_self) finally show "\ \ vcard (\ \ a)" . qed text\Monotonicity of addition\ lemma cadd_le_mono: "\\' \ \; \' \ \\ \ \' \ \' \ \ \ \" unfolding cadd_def by (metis (no_types) lepoll_imp_Card_le less_eq_V_def subset_imp_lepoll sum_subset_iff) subsection\Cardinal multiplication\ definition cmult :: "[V,V]\V" (infixl \\\ 70) where "\ \ \ \ vcard (VSigma \ (\z. \))" subsubsection\Cardinal multiplication is commutative\ lemma prod_bij: "\bij_betw f A C; bij_betw g B D\ \ bij_betw (\(x, y). (f x, g y)) (A \ B) (C \ D)" apply (rule bij_betw_byWitness [where f' = "\(x,y). (inv_into A f x, inv_into B g y)"]) apply (auto simp: bij_betw_inv_into_left bij_betw_inv_into_right bij_betwE) using bij_betwE bij_betw_inv_into apply blast+ done lemma cmult_commute: "i \ j = j \ i" proof - have "(\(x, y). \x, y\) ` (elts i \ elts j) \ (\(x, y). \x, y\) ` (elts j \ elts i)" by (simp add: times_commute_eqpoll) then show ?thesis unfolding cmult_def using cardinal_cong elts_VSigma by auto qed subsubsection\Cardinal multiplication is associative\ lemma elts_vcard_VSigma_eqpoll: "elts (vcard (vtimes i j)) \ elts i \ elts j" proof - have "elts (vtimes i j) \ elts i \ elts j" by (simp add: elts_VSigma) then show ?thesis using cardinal_eqpoll eqpoll_trans by blast qed lemma elts_cmult: "elts (\' \ \) \ elts \' \ elts \" by (simp add: cmult_def elts_vcard_VSigma_eqpoll) lemma cmult_assoc: "(i \ j) \ k = i \ (j \ k)" unfolding cmult_def proof (rule cardinal_cong) have "elts (vcard (vtimes i j)) \ elts k \ (elts i \ elts j) \ elts k" by (blast intro: times_eqpoll_cong elts_vcard_VSigma_eqpoll cardinal_eqpoll) also have "\ \ elts i \ (elts j \ elts k)" by (rule times_assoc_eqpoll) also have "\ \ elts i \ elts (vcard (vtimes j k))" by (blast intro: times_eqpoll_cong elts_vcard_VSigma_eqpoll cardinal_eqpoll eqpoll_sym) finally show "elts (VSigma (vcard (vtimes i j)) (\z. k)) \ elts (VSigma i (\z. vcard (vtimes j k)))" by (simp add: elts_VSigma) qed subsubsection\Cardinal multiplication distributes over addition\ lemma cadd_cmult_distrib: "(i \ j) \ k = (i \ k) \ (j \ k)" unfolding cadd_def cmult_def proof (rule cardinal_cong) have "elts (vtimes (vcard (i \ j)) k) \ elts (vcard (vsum i j)) \ elts k" using cardinal_eqpoll elts_vcard_VSigma_eqpoll eqpoll_sym eqpoll_trans by blast also have "\ \ (Inl ` elts i \ Inr ` elts j) \ elts k" using elts_vcard_vsum_eqpoll times_eqpoll_cong by blast also have "\ \ (Inl ` elts i) \ elts k \ (Inr ` elts j) \ elts k" by (simp add: Sigma_Un_distrib1) also have "\ \ elts (vtimes i k \ vtimes j k)" unfolding Plus_def by (auto simp: elts_vsum elts_VSigma disjnt_iff intro!: Un_eqpoll_cong times_eqpoll_cong) also have "\ \ elts (vcard (vtimes i k \ vtimes j k))" by (simp add: cardinal_eqpoll eqpoll_sym) also have "\ \ elts (vcard (vtimes i k) \ vcard (vtimes j k))" by (metis cadd_assoc cadd_def cardinal_cong cardinal_eqpoll vsum_0_eqpoll vsum_commute_eqpoll) finally show "elts (VSigma (vcard (i \ j)) (\z. k)) \ elts (vcard (vtimes i k) \ vcard (vtimes j k))" . qed text\Multiplication by 0 yields 0\ lemma cmult_0 [simp]: "0 \ i = 0" using Card_0 Card_def cmult_def by auto text\1 is the identity for multiplication\ lemma cmult_1 [simp]: assumes "Card \" shows "1 \ \ = \" proof - have "elts (vtimes (set {0}) \) \ elts \" by (auto simp: elts_VSigma intro!: times_singleton_eqpoll) then show ?thesis by (metis Card_def assms cardinal_cong cmult_def elts_1 set_of_elts) qed subsection\Some inequalities for multiplication\ lemma cmult_square_le: assumes "Card \" shows "\ \ \ \ \" proof - have "elts \ \ elts (\ \ \)" using times_square_lepoll [of "elts \"] cmult_def elts_vcard_VSigma_eqpoll eqpoll_sym lepoll_trans2 by fastforce then show ?thesis using Card_def assms cmult_def lepoll_cardinal_le by fastforce qed text\Multiplication by a non-empty set\ lemma cmult_le_self: assumes "Card \" "\ \ 0" shows "\ \ \ \ \" proof - have "\ = vcard \" using Card_def \Card \\ by blast also have "\ \ vcard (vtimes \ \)" apply (rule lepoll_imp_Card_le) apply (simp add: elts_VSigma) by (metis ZFC_in_HOL.ext \\ \ 0\ elts_0 lepoll_times1) also have "\ = \ \ \" by (simp add: cmult_def) finally show ?thesis . qed text\Monotonicity of multiplication\ lemma cmult_le_mono: "\\' \ \; \' \ \\ \ \' \ \' \ \ \ \" unfolding cmult_def by (auto simp: elts_VSigma intro!: lepoll_imp_Card_le times_lepoll_mono subset_imp_lepoll) lemma vcard_Sup_le_cmult: assumes "small U" and \: "\x. x \ U \ vcard x \ \" shows "vcard (\U) \ vcard (set U) \ \" proof - have "\f. f \ elts x \ elts \ \ inj_on f (elts x)" if "x \ U" for x using \ [OF that] by (metis cardinal_le_lepoll image_subset_iff_funcset lepoll_def) then obtain \ where \: "\x. x \ U \ (\ x) \ elts x \ elts \ \ inj_on (\ x) (elts x)" by metis define u where "u \ \y. @x. x \ U \ y \ elts x" have u: "u y \ U \ y \ elts (u y)" if "y \ \(elts ` U)" for y unfolding u_def by (metis (mono_tags, lifting)that someI2_ex UN_iff) define \ where "\ \ \y. (u y, \ (u y) y)" have U: "elts (vcard (set U)) \ U" by (metis \small U\ cardinal_eqpoll elts_of_set) have "elts (\U) = \(elts ` U)" using \small U\ by blast also have "\ \ U \ elts \" unfolding lepoll_def proof (intro exI conjI) show "inj_on \ (\ (elts ` U))" using \ u by (smt (verit) \_def inj_on_def prod.inject) show "\ ` \ (elts ` U) \ U \ elts \" using \ u by (auto simp: \_def) qed also have "\ \ elts (vcard (set U) \ \)" using U elts_cmult eqpoll_sym eqpoll_trans times_eqpoll_cong by blast finally have "elts (\ U) \ elts (vcard (set U) \ \)" . then show ?thesis by (simp add: cmult_def lepoll_cardinal_le) qed subsection\The finite cardinals\ lemma succ_lepoll_succD: "elts (succ(m)) \ elts (succ(n)) \ elts m \ elts n" by (simp add: insert_lepoll_insertD) text\Congruence law for @{text succ} under equipollence\ lemma succ_eqpoll_cong: "elts a \ elts b \ elts (succ(a)) \ elts (succ(b))" by (simp add: succ_def insert_eqpoll_cong) lemma sum_succ_eqpoll: "elts (succ a \ b) \ elts (succ(a\b))" unfolding eqpoll_def proof (rule exI) let ?f = "\z. if z=Inl a then a\b else z" let ?g = "\z. if z=a\b then Inl a else z" show "bij_betw ?f (elts (succ a \ b)) (elts (succ (a \ b)))" apply (rule bij_betw_byWitness [where f' = ?g], auto) apply (metis Inl_in_sum_iff mem_not_refl) by (metis Inr_in_sum_iff mem_not_refl) qed lemma cadd_succ: "succ m \ n = vcard (succ(m \ n))" proof (unfold cadd_def) have [intro]: "elts (m \ n) \ elts (vcard (m \ n))" using cardinal_eqpoll eqpoll_sym by blast have "vcard (succ m \ n) = vcard (succ(m \ n))" by (rule sum_succ_eqpoll [THEN cardinal_cong]) also have "\ = vcard (succ(vcard (m \ n)))" by (blast intro: succ_eqpoll_cong cardinal_cong) finally show "vcard (succ m \ n) = vcard (succ(vcard (m \ n)))" . qed lemma nat_cadd_eq_add: "ord_of_nat m \ ord_of_nat n = ord_of_nat (m + n)" proof (induct m) case (Suc m) thus ?case by (metis Card_def Card_ord_of_nat add_Suc cadd_succ ord_of_nat.simps(2)) qed auto lemma vcard_disjoint_sup: assumes "x \ y = 0" shows "vcard (x \ y) = vcard x \ vcard y" proof - have "elts (x \ y) \ elts (x \ y)" unfolding eqpoll_def proof (rule exI) let ?f = "\z. if z \ elts x then Inl z else Inr z" let ?g = "sum_case id id" show "bij_betw ?f (elts (x \ y)) (elts (x \ y))" by (rule bij_betw_byWitness [where f' = ?g]) (use assms V_disjoint_iff in auto) qed then show ?thesis by (metis cadd_commute cadd_def cardinal_cong cardinal_idem vsum_0_eqpoll cadd_assoc) qed lemma vcard_sup: "vcard (x \ y) \ vcard x \ vcard y" proof - have "elts (x \ y) \ elts (x \ y)" unfolding lepoll_def proof (intro exI conjI) let ?f = "\z. if z \ elts x then Inl z else Inr z" show "inj_on ?f (elts (x \ y))" by (simp add: inj_on_def) show "?f ` elts (x \ y) \ elts (x \ y)" by force qed then show ?thesis using cadd_ac by (metis cadd_def cardinal_cong cardinal_idem lepoll_imp_Card_le vsum_0_eqpoll) qed subsection\Infinite cardinals\ definition InfCard :: "V\bool" where "InfCard \ \ Card \ \ \ \ \" lemma InfCard_iff: "InfCard \ \ Card \ \ infinite (elts \)" proof (cases "\ \ \") case True then show ?thesis using inj_ord_of_nat lepoll_def less_eq_V_def by (auto simp: InfCard_def \_def infinite_le_lepoll) next case False then show ?thesis using Card_iff_initial InfCard_def infinite_Ord_omega by blast qed lemma InfCard_ge_ord_of_nat: assumes "InfCard \" shows "ord_of_nat n \ \" using InfCard_def assms ord_of_nat_le_omega by blast lemma InfCard_not_0[iff]: "\ InfCard 0" by (simp add: InfCard_iff) definition csucc :: "V\V" where "csucc \ \ LEAST \'. Ord \' \ (Card \' \ \ < \')" lemma less_vcard_VPow: "vcard A < vcard (VPow A)" proof (rule lesspoll_imp_Card_less) show "elts A \ elts (VPow A)" by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self) qed lemma greater_Card: assumes "Card \" shows "\ < vcard (VPow \)" proof - have "\ = vcard \" using Card_def assms by blast also have "\ < vcard (VPow \)" proof (rule lesspoll_imp_Card_less) show "elts \ \ elts (VPow \)" by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self) qed finally show ?thesis . qed lemma assumes "Card \" shows Card_csucc [simp]: "Card (csucc \)" and less_csucc [simp]: "\ < csucc \" proof - have "Card (csucc \) \ \ < csucc \" unfolding csucc_def proof (rule Ord_LeastI2) show "Card (vcard (VPow \)) \ \ < (vcard (VPow \))" using Card_def assms greater_Card by auto qed auto then show "Card (csucc \)" "\ < csucc \" by auto qed lemma le_csucc: assumes "Card \" shows "\ \ csucc \" by (simp add: assms less_csucc less_imp_le) lemma csucc_le: "\Card \; \ \ elts \\ \ csucc \ \ \" unfolding csucc_def by (simp add: Card_is_Ord Ord_Least_le OrdmemD) lemma finite_csucc: "a \ elts \ \ csucc a = succ a" unfolding csucc_def proof (rule Least_equality) show "Ord (ZFC_in_HOL.succ a) \ Card (ZFC_in_HOL.succ a) \ a < ZFC_in_HOL.succ a" if "a \ elts \" using that by (auto simp: less_V_def less_eq_V_def nat_into_Card) show "ZFC_in_HOL.succ a \ y" if "a \ elts \" and "Ord y \ Card y \ a < y" for y :: V using that using Ord_mem_iff_lt dual_order.strict_implies_order by fastforce qed lemma Finite_imp_cardinal_cons [simp]: assumes FA: "finite A" and a: "a \ A" shows "vcard (set (insert a A)) = csucc(vcard (set A))" proof - show ?thesis unfolding csucc_def proof (rule Least_equality [THEN sym]) have "small A" by (simp add: FA Finite_V) then have "\ elts (set A) \ elts (set (insert a A))" using FA a eqpoll_imp_lepoll eqpoll_sym finite_insert_lepoll by fastforce then show "Ord (vcard (set (insert a A))) \ Card (vcard (set (insert a A))) \ vcard (set A) < vcard (set (insert a A))" by (simp add: Card_def lesspoll_imp_Card_less lesspoll_def subset_imp_lepoll subset_insertI) show "vcard (set (insert a A)) \ i" if "Ord i \ Card i \ vcard (set A) < i" for i proof - have "elts (vcard (set A)) \ A" by (metis FA finite_imp_small cardinal_eqpoll elts_of_set) then have less: "A \ elts i" using eq_lesspoll_trans eqpoll_sym lt_Card_imp_lesspoll that by blast show ?thesis using that less by (auto simp: less_imp_insert_lepoll lepoll_cardinal_le) qed qed qed lemma vcard_finite_set: "finite A \ vcard (set A) = ord_of_nat (card A)" by (induction A rule: finite_induct) (auto simp: set_empty \_def finite_csucc) lemma lt_csucc_iff: assumes "Ord \" "Card \" shows "\ < csucc \ \ vcard \ \ \" proof show "vcard \ \ \" if "\ < csucc \" proof - have "vcard \ \ csucc \" by (meson \Ord \\ dual_order.trans lepoll_cardinal_le lepoll_refl less_le_not_le that) then show ?thesis by (metis (no_types) Card_def Card_iff_initial Ord_linear2 Ord_mem_iff_lt assms cardinal_eqpoll cardinal_idem csucc_le eq_iff eqpoll_sym that) qed show "\ < csucc \" if "vcard \ \ \" proof - have "\ csucc \ \ \" using that by (metis Card_csucc Card_def assms(2) le_less_trans lepoll_imp_Card_le less_csucc less_eq_V_def less_le_not_le subset_imp_lepoll) then show ?thesis by (meson Card_csucc Card_is_Ord Ord_linear2 assms) qed qed lemma Card_lt_csucc_iff: "\Card \'; Card \\ \ (\' < csucc \) = (\' \ \)" by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord) lemma csucc_lt_csucc_iff: "\Card \'; Card \\ \ (csucc \' < csucc \) = (\' < \)" by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_less) lemma csucc_le_csucc_iff: "\Card \'; Card \\ \ (csucc \' \ csucc \) = (\' \ \)" by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_less) lemma csucc_0 [simp]: "csucc 0 = 1" by (simp add: finite_csucc one_V_def) lemma Card_Un [simp,intro]: assumes "Card x" "Card y" shows "Card(x \ y)" by (metis Card_is_Ord Ord_linear_le assms sup.absorb2 sup.orderE) lemma InfCard_csucc: "InfCard \ \ InfCard (csucc \)" using InfCard_def le_csucc by auto text\Kunen's Lemma 10.11\ lemma InfCard_is_Limit: assumes "InfCard \" shows "Limit \" proof (rule non_succ_LimitI) show "\ \ 0" using InfCard_def assms mem_not_refl by blast show "Ord \" using Card_is_Ord InfCard_def assms by blast show "ZFC_in_HOL.succ y \ \" for y proof assume "succ y = \" then have "Card (succ y)" using InfCard_def assms by auto moreover have "\ \ y" by (metis InfCard_iff Ord_in_Ord \Ord \\ \ZFC_in_HOL.succ y = \\ assms elts_succ finite_insert infinite_Ord_omega insertI1) moreover have "elts y \ elts (succ y)" using InfCard_iff \ZFC_in_HOL.succ y = \\ assms eqpoll_sym infinite_insert_eqpoll by fastforce ultimately show False by (metis Card_iff_initial Ord_in_Ord OrdmemD elts_succ insertI1) qed qed subsection\Toward's Kunen's Corollary 10.13 (1)\ text\Kunen's Theorem 10.12\ lemma InfCard_csquare_eq: assumes "InfCard(\)" shows "\ \ \ = \" using infinite_times_eqpoll_self [of "elts \"] assms unfolding InfCard_iff Card_def by (metis cardinal_cong cardinal_eqpoll cmult_def elts_vcard_VSigma_eqpoll eqpoll_trans) lemma InfCard_le_cmult_eq: assumes "InfCard \" "\ \ \" "\ \ 0" shows "\ \ \ = \" proof (rule order_antisym) have "\ \ \ \ \ \ \" by (simp add: assms(2) cmult_le_mono) also have "\ \ \" by (simp add: InfCard_csquare_eq assms(1)) finally show "\ \ \ \ \" . show "\ \ \ \ \" using InfCard_def assms(1) assms(3) cmult_le_self by auto qed text\Kunen's Corollary 10.13 (1), for cardinal multiplication\ lemma InfCard_cmult_eq: "\InfCard \; InfCard \\ \ \ \ \ = \ \ \" by (metis Card_is_Ord InfCard_def InfCard_le_cmult_eq Ord_linear_le cmult_commute inf_sup_aci(5) mem_not_refl sup.orderE sup_V_0_right zero_in_omega) lemma cmult_succ: "succ(m) \ n = n \ (m \ n)" unfolding cmult_def cadd_def proof (rule cardinal_cong) have "elts (vtimes (ZFC_in_HOL.succ m) n) \ elts n <+> elts m \ elts n" by (simp add: elts_VSigma prod_insert_eqpoll) also have "\ \ elts (n \ vcard (vtimes m n))" unfolding elts_VSigma elts_vsum Plus_def proof (rule Un_eqpoll_cong) show "(Sum_Type.Inr ` (elts m \ elts n)::(V + V \ V) set) \ Inr ` elts (vcard (vtimes m n))" by (simp add: elts_vcard_VSigma_eqpoll eqpoll_sym) qed (auto simp: disjnt_def) finally show "elts (vtimes (ZFC_in_HOL.succ m) n) \ elts (n \ vcard (vtimes m n))" . qed lemma cmult_2: assumes "Card n" shows "ord_of_nat 2 \ n = n \ n" proof - have "ord_of_nat 2 = succ (succ 0)" by force then show ?thesis by (simp add: cmult_succ assms) qed lemma InfCard_cdouble_eq: assumes "InfCard \" shows "\ \ \ = \" proof - have "\ \ \ = \ \ ord_of_nat 2" using InfCard_def assms cmult_2 cmult_commute by auto also have "\ = \" by (simp add: InfCard_le_cmult_eq InfCard_ge_ord_of_nat assms) finally show ?thesis . qed text\Corollary 10.13 (1), for cardinal addition\ lemma InfCard_le_cadd_eq: "\InfCard \; \ \ \\ \ \ \ \ = \" by (metis InfCard_cdouble_eq InfCard_def antisym cadd_le_mono cadd_le_self) lemma InfCard_cadd_eq: "\InfCard \; InfCard \\ \ \ \ \ = \ \ \" by (metis Card_iff_initial InfCard_def InfCard_le_cadd_eq Ord_linear_le cadd_commute sup.absorb2 sup.orderE) lemma csucc_le_Card_iff: "\Card \'; Card \\ \ csucc \' \ \ \ \' < \" by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_le) lemma cadd_InfCard_le: assumes "\ \ \" "\ \ \" "InfCard \" shows "\ \ \ \ \" using assms by (metis InfCard_cdouble_eq cadd_le_mono) lemma cmult_InfCard_le: assumes "\ \ \" "\ \ \" "InfCard \" shows "\ \ \ \ \" using assms by (metis InfCard_csquare_eq cmult_le_mono) subsection \The Aleph-seqence\ text \This is the well-known transfinite enumeration of the cardinal numbers.\ definition Aleph :: "V \ V" (\\_\ [90] 90) where "Aleph \ transrec (\f x. \ \ \((\y. csucc(f y)) ` elts x))" lemma Aleph: "Aleph \ = \ \ (\y\elts \. csucc (Aleph y))" by (simp add: Aleph_def transrec[of _ \]) lemma InfCard_Aleph [simp, intro]: "InfCard(Aleph x)" proof (induction x rule: eps_induct) case (step x) then show ?case by (simp add: Aleph [of x] InfCard_def Card_UN step) qed lemma Card_Aleph [simp, intro]: "Card(Aleph x)" using InfCard_def by auto lemma Aleph_0 [simp]: "\0 = \" by (simp add: Aleph [of 0]) lemma mem_Aleph_succ: "\\ \ elts (Aleph (succ \))" apply (simp add: Aleph [of "succ \"]) by (meson InfCard_Aleph Card_csucc Card_is_Ord InfCard_def Ord_mem_iff_lt less_csucc) lemma Aleph_lt_succD [simp]: "\\ < Aleph (succ \)" by (simp add: InfCard_is_Limit Limit_is_Ord OrdmemD mem_Aleph_succ) lemma Aleph_succ [simp]: "Aleph (succ x) = csucc (Aleph x)" proof (rule antisym) show "Aleph (ZFC_in_HOL.succ x) \ csucc (Aleph x)" apply (simp add: Aleph [of "succ x"]) by (metis Aleph InfCard_Aleph InfCard_def Sup_V_insert le_csucc le_sup_iff order_refl replacement small_elts) show "csucc (Aleph x) \ Aleph (ZFC_in_HOL.succ x)" by (force simp add: Aleph [of "succ x"]) qed lemma csucc_Aleph_le_Aleph: "\ \ elts \ \ csucc (\\) \ \\" by (metis Aleph ZFC_in_HOL.SUP_le_iff replacement small_elts sup_ge2) lemma Aleph_in_Aleph: "\ \ elts \ \ \\ \ elts (\\)" using csucc_Aleph_le_Aleph mem_Aleph_succ by auto lemma Aleph_Limit: assumes "Limit \" shows "Aleph \ = \ (Aleph ` elts \)" proof - have [simp]: "\ \ 0" using assms by auto show ?thesis proof (rule antisym) show "Aleph \ \ \ (Aleph ` elts \)" apply (simp add: Aleph [of \]) by (metis (mono_tags, lifting) Aleph_0 Aleph_succ Limit_def ZFC_in_HOL.SUP_le_iff ZFC_in_HOL.Sup_upper assms imageI replacement small_elts) show "\ (Aleph ` elts \) \ Aleph \" apply (simp add: cSup_le_iff) by (meson InfCard_Aleph InfCard_def csucc_Aleph_le_Aleph le_csucc order_trans) qed qed lemma Aleph_increasing: assumes ab: "\ < \" "Ord \" "Ord \" shows "\\ < \\" by (meson Aleph_in_Aleph InfCard_Aleph Card_iff_initial InfCard_def Ord_mem_iff_lt assms) lemma countable_iff_le_Aleph0: "countable (elts A) \ vcard A \ \0" proof show "vcard A \ \0" if "countable (elts A)" proof (cases "finite (elts A)") case True then show ?thesis using vcard_finite_set by fastforce next case False then have "elts \ \ elts A" using countableE_infinite [OF that] by (simp add: eqpoll_def \_def) (meson bij_betw_def bij_betw_inv bij_betw_trans inj_ord_of_nat) then show ?thesis using Card_\ Card_def cardinal_cong vcard_def by auto qed show "countable (elts A)" if "vcard A \ Aleph 0" proof - have "elts A \ elts \" using cardinal_le_lepoll [OF that] by simp then show ?thesis by (simp add: countable_iff_lepoll \_def inj_ord_of_nat) qed qed lemma Aleph_csquare_eq [simp]: "\\ \ \\ = \\" using InfCard_csquare_eq by auto lemma vcard_Aleph [simp]: "vcard (\\) = \\" using Card_def InfCard_Aleph InfCard_def by auto lemma omega_le_Aleph [simp]: "\ \ \\" using InfCard_def by auto lemma finite_iff_less_Aleph0: "finite (elts x) \ vcard x < \" proof show "finite (elts x) \ vcard x < \" by (metis Card_\ Card_def finite_lesspoll_infinite infinite_\ lesspoll_imp_Card_less) show "vcard x < \ \ finite (elts x)" by (meson Ord_cardinal cardinal_eqpoll eqpoll_finite_iff infinite_Ord_omega less_le_not_le) qed lemma countable_iff_vcard_less1: "countable (elts x) \ vcard x < \1" by (simp add: countable_iff_le_Aleph0 lt_csucc_iff one_V_def) lemma countable_infinite_vcard: "countable (elts x) \ infinite (elts x) \ vcard x = \0" by (metis Aleph_0 countable_iff_le_Aleph0 dual_order.refl finite_iff_less_Aleph0 less_V_def) subsection \The ordinal @{term "\1"}\ abbreviation "\1 \ Aleph 1" lemma Ord_\1 [simp]: "Ord \1" by (metis Ord_cardinal vcard_Aleph) lemma omega_\1 [iff]: "\ \ elts \1" by (metis Aleph_0 mem_Aleph_succ one_V_def) lemma ord_of_nat_\1 [iff]: "ord_of_nat n \ elts \1" using Ord_\1 Ord_trans by blast lemma countable_iff_less_\1: assumes "Ord \" shows "countable (elts \) \ \ < \1" by (simp add: assms countable_iff_le_Aleph0 lt_csucc_iff one_V_def) lemma less_\1_imp_countable: assumes "\ \ elts \1" shows "countable (elts \)" using Ord_\1 Ord_in_Ord OrdmemD assms countable_iff_less_\1 by blast lemma \1_gt0 [simp]: "\1 > 0" using Ord_\1 Ord_trans OrdmemD by blast lemma \1_gt1 [simp]: "\1 > 1" using Ord_\1 OrdmemD \_gt1 less_trans by blast lemma Limit_\1 [simp]: "Limit \1" by (simp add: InfCard_def InfCard_is_Limit le_csucc one_V_def) end