diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,502 +1,503 @@ AODV Auto2_HOL Auto2_Imperative_HOL AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amortized_Complexity AnselmGod Applicative_Lifting Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic ArrowImpossibilityGS AutoFocus-Stream Automatic_Refinement AxiomaticCategoryTheory BDD BNF_Operations Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BNF_CC Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chord_Segments Circus Clean ClockSynchInst CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Completeness Complete_Non_Orders Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series Discrete_Summation DiscretePricing DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Factored_Transition_System_Bounding Farkas FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Falling_Factorial_Sum FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover GPU_Kernel_PL Gabow_SCC Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan GenClock General-Triangle Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Iptables_Semantics Irrationality_J_Hancl Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_to_DRA LTL_to_GBA LTL_Master_Theorem Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_KBOs Lambda_Free_RPOs Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Lambda_Free_EPO Launchbury Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp MFMC_Countable MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger MFOTL_Monitor MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multirelations Multi_Party_Computation Myhill-Nerode Name_Carrying_Type_Inference Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions Open_Induction OpSets Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinals_and_Cardinals Ordinary_Differential_Equations PCF PLM Pell POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Perfect-Number-Thm Perron_Frobenius Pi_Calculus Pi_Transcendental Planarity_Certificates Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Projective_Geometry Program-Conflict-Analysis Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Randomised_BSTs Random_Graph_Subgraph_Threshold Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Root_Balanced_Tree Routing Roy_Floyd_Warshall Safe_OCL SATSolverVerification SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Slicing Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Universal_Turing_Machine UPF UPF_Firewall UpDown_Scheme UTP Valuation VectorSpace Verified-Prover VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML Zeta_Function +ZFC_in_HOL pGCL diff --git a/thys/ZFC_in_HOL/Kirby.thy b/thys/ZFC_in_HOL/Kirby.thy new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/Kirby.thy @@ -0,0 +1,1067 @@ +section \Addition and Multiplication of Sets\ + +theory Kirby + imports ZFC_Cardinals + +begin + +subsection \Generalised Addition\ + +text \Source: Laurence Kirby, Addition and multiplication of sets + Math. Log. Quart. 53, No. 1, 52-65 (2007) / DOI 10.1002/malq.200610026 + @{url "http://faculty.baruch.cuny.edu/lkirby/mlqarticlejan2007.pdf"}\ + +instantiation V :: plus +begin + +text\This definition is credited to Tarski\ +definition plus_V :: "V \ V \ V" + where "plus_V x \ transrec (\f z. x \ set (f ` elts z))" + +instance .. +end + +definition lift :: "V \ V \ V" + where "lift x y \ set (plus x ` elts y)" + +lemma plus: "x + y = x \ set ((+)x ` elts y)" + unfolding plus_V_def by (subst transrec) auto + +lemma plus_eq_lift: "x + y = x \ lift x y" + unfolding lift_def using plus by blast + +text\Lemma 3.2\ +lemma lift_sup_distrib: "lift x (a \ b) = lift x a \ lift x b" + by (simp add: image_Un lift_def sup_V_def) + +lemma lift_Sup_distrib: "small Y \ lift x (\ Y) = \ (lift x ` Y)" + by (auto simp: lift_def Sup_V_def image_Union) + +lemma add_Sup_distrib: + fixes x::V shows "y \ 0 \ x + (SUP z\elts y. f z) = (SUP z\elts y. x + f z)" + by (auto simp: plus_eq_lift SUP_sup_distrib lift_Sup_distrib image_image) + +text\Proposition 3.3(ii)\ +instantiation V :: monoid_add +begin +instance +proof + show "a + b + c = a + (b + c)" for a b c :: V + proof (induction c rule: eps_induct) + case (step c) + have "(a+b) + c = a + b \ set ((+) (a + b) ` elts c)" + by (metis plus) + also have "\ = a \ lift a b \ set ((\u. a + (b+u)) ` elts c)" + using plus_eq_lift step.IH by auto + also have "\ = a \ lift a (b + c)" + proof - + have "lift a b \ set ((\u. a + (b + u)) ` elts c) = lift a (b + c)" + unfolding lift_def + by (metis elts_of_set image_image lift_def lift_sup_distrib plus_eq_lift replacement small_elts) + then show ?thesis + by (simp add: sup_assoc) + qed + also have "\ = a + (b + c)" + using plus_eq_lift by auto + finally show ?case . + qed + show "0 + x = x" for x :: V + proof (induction rule: eps_induct) + case (step x) + then show ?case + by (subst plus) auto + qed + show "x + 0 = x" for x :: V + by (subst plus) auto +qed +end + +lemma lift_0 [simp]: "lift 0 x = x" + by (simp add: lift_def) + +lemma lift_by0 [simp]: "lift x 0 = 0" + by (simp add: lift_def set_empty) + +lemma lift_by1 [simp]: "lift x 1 = set{x}" + by (simp add: lift_def) + +lemma plus_vinsert: "x + vinsert z y = vinsert (x+z) (x + y)" +proof - + have f1: "elts (x + y) = elts x \ (+) x ` elts y" + by (metis elts_of_set lift_def plus_eq_lift replacement small_Un small_elts sup_V_def) + moreover have "lift x (vinsert z y) = set ((+) x ` elts (set (insert z (elts y))))" + using vinsert_def lift_def by presburger + ultimately show ?thesis + by (simp add: vinsert_def plus_eq_lift sup_V_def) +qed + +lemma plus_V_succ_right: "x + succ y = succ (x + y)" + by (metis plus_vinsert succ_def) + +lemma mem_plus_V_E: + assumes l: "l \ elts (x + y)" + obtains "l \ elts x" | z where "z \ elts y" "l = x + z" + using l by (auto simp: plus [of x y] split: if_split_asm) + +lemma not_add_less_right: assumes "Ord y" shows "\ (x + y < x)" + using assms +proof (induction rule: Ord_induct) + case (step i) + then show ?case + by (metis less_le_not_le plus sup_ge1) +qed + +lemma not_add_mem_right: "\ (x + y \ elts x)" + by (metis sup_ge1 mem_not_refl plus vsubsetD) + +text\Proposition 3.3(iii)\ +lemma add_not_less_TC_self: "\ x + y \ x" +proof (induction y arbitrary: x rule: eps_induct) + case (step y) + then show ?case + using less_TC_imp_not_le plus_eq_lift by fastforce +qed + +lemma TC_sup_lift: "TC x \ lift x y = 0" +proof - + have "elts (TC x) \ elts (set ((+) x ` elts y)) = {}" + using add_not_less_TC_self by (auto simp: less_TC_def) + then have "TC x \ set ((+) x ` elts y) = set {}" + by (metis inf_V_def) + then show ?thesis + by (simp add: lift_def zero_V_def) +qed + +lemma lift_lift: "lift x (lift y z) = lift (x+y) z" + using add.assoc by (auto simp: lift_def) + +lemma lift_self_disjoint: "x \ lift x u = 0" + by (metis TC_sup_lift arg_subset_TC inf.absorb_iff2 inf_assoc inf_sup_aci(3) lift_0) + +lemma sup_lift_eq_lift: + assumes "x \ lift x u = x \ lift x v" + shows "lift x u = lift x v" + by (metis (no_types) assms inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup_commute sup_inf_absorb) + +text\Proposition 3.4(i)\ +proposition lift_eq_lift: "lift x y = lift x z \ y = z" +proof (induction y arbitrary: z rule: eps_induct) + case (step y) + show ?case + proof (intro vsubsetI order_antisym) + show "u \ elts z" if "u \ elts y" for u + proof - + have "x+u \ elts (lift x z)" + using lift_def step.prems that by fastforce + then obtain v where "v \ elts z" "x+u = x+v" + using lift_def by auto + then have "lift x u = lift x v" + using sup_lift_eq_lift by (simp add: plus_eq_lift) + then have "u=v" + using step.IH that by blast + then show ?thesis + using \v \ elts z\ by blast + qed + show "u \ elts y" if "u \ elts z" for u + proof - + have "x+u \ elts (lift x y)" + using lift_def step.prems that by fastforce + then obtain v where "v \ elts y" "x+u = x+v" + using lift_def by auto + then have "lift x u = lift x v" + using sup_lift_eq_lift by (simp add: plus_eq_lift) + then have "u=v" + using step.IH by (metis \v \ elts y\) + then show ?thesis + using \v \ elts y\ by auto + qed + qed +qed + +corollary inj_lift: "inj_on (lift x) A" + by (auto simp: inj_on_def dest: lift_eq_lift) + +corollary add_right_cancel [iff]: + fixes x y z::V shows "x+y = x+z \ y=z" + by (metis lift_eq_lift plus_eq_lift sup_lift_eq_lift) + +corollary add_mem_right_cancel [iff]: + fixes x y z::V shows "x+y \ elts (x+z) \ y \ elts z" + apply safe + apply (metis mem_plus_V_E not_add_mem_right add_right_cancel) + by (metis ZFC_in_HOL.ext dual_order.antisym elts_vinsert insert_subset order_refl plus_vinsert) + +corollary add_le_cancel_left [iff]: + fixes x y z::V shows "x+y \ x+z \ y\z" + by auto (metis add_mem_right_cancel mem_plus_V_E plus sup_ge1 vsubsetD) + +corollary add_less_cancel_left [iff]: + fixes x y z::V shows "x+y < x+z \ y x \ y = 0" + by (auto simp: inf.absorb_iff2 lift_eq_lift lift_self_disjoint) + + +text\Proposition 3.5\ +lemma card_lift: "vcard (lift x y) = vcard y" +proof (rule cardinal_cong) + have "bij_betw ((+)x) (elts y) (elts (lift x y))" + unfolding bij_betw_def + by (simp add: inj_on_def lift_def) + then show "elts (lift x y) \ elts y" + using eqpoll_def eqpoll_sym by blast +qed + +lemma eqpoll_lift: "elts (lift x y) \ elts y" + by (metis card_lift cardinal_eqpoll eqpoll_sym eqpoll_trans) + +lemma card_add: "vcard (x + y) = vcard x \ vcard y" + using card_lift [of x y] lift_self_disjoint [of x] + by (simp add: plus_eq_lift vcard_disjoint_sup) + +text\Proposition 3.6\ +proposition TC_add: "TC (x + y) = TC x \ lift x (TC y)" +proof (induction y rule: eps_induct) + case (step y) + have *: "\ (TC ` (+) x ` elts y) = TC x \ (SUP u\elts y. TC (set ((+) x ` elts u)))" + if "elts y \ {}" + proof - + obtain w where "w \ elts y" + using \elts y \ {}\ by blast + then have "TC x \ TC (x + w)" + by (simp add: step.IH) + then have \: "TC x \ (SUP w\elts y. TC (x + w))" + using \w \ elts y\ by blast + show ?thesis + using that + apply (intro conjI ballI impI order_antisym; clarsimp simp add: image_comp \) + apply(metis TC_sup_distrib Un_iff elts_sup_iff plus) + by (metis TC_least Transset_TC arg_subset_TC le_sup_iff plus vsubsetD) + qed + have "TC (x + y) = (x + y) \ \ (TC ` elts (x + y))" + using TC by blast + also have "\ = x \ lift x y \ \ (TC ` elts x) \ \ ((\u. TC (x+u)) ` elts y)" + apply (simp add: plus_eq_lift image_Un Sup_Un_distrib sup.left_commute sup_assoc TC_sup_distrib SUP_sup_distrib) + apply (simp add: lift_def sup.commute sup_aci *) + done + also have "\ = x \ \ (TC ` elts x) \ lift x y \ \ ((\u. TC x \ lift x (TC u)) ` elts y)" + by (simp add: sup_aci step.IH) + also have "\ = TC x \ lift x y \ \ ((\u. lift x (TC u)) ` elts y)" + by (simp add: sup_aci SUP_sup_distrib flip: TC [of x]) + also have "\ = TC x \ lift x (y \ \ (TC ` elts y))" + by (metis (no_types) elts_of_set lift_Sup_distrib image_image lift_sup_distrib replacement small_elts sup_assoc) + also have "\ = TC x \ lift x (TC y)" + by (simp add: TC [of y]) + finally show ?case . +qed + +corollary TC_add': "z \ x + y \ z \ x \ (\v. v \ y \ z = x + v)" + using TC_add by (force simp: less_TC_def lift_def) + +text\Corollary 3.7\ +corollary vcard_TC_add: "vcard (TC (x+y)) = vcard (TC x) \ vcard (TC y)" + by (simp add: TC_add TC_sup_lift card_lift vcard_disjoint_sup) + +text\Corollary 3.8\ +corollary TC_lift: + assumes "y \ 0" + shows "TC (lift x y) = TC x \ lift x (TC y)" +proof - + have "TC (lift x y) = lift x y \ \ ((\u. TC(x+u)) ` elts y)" + unfolding TC [of "lift x y"] by (simp add: lift_def image_image) + also have "\ = lift x y \ (SUP u\elts y. TC x \ lift x (TC u))" + by (simp add: TC_add) + also have "\ = lift x y \ TC x \ (SUP u\elts y. lift x (TC u))" + using assms by (auto simp: SUP_sup_distrib) + also have "\ = TC x \ lift x (TC y)" + by (simp add: TC [of y] sup_aci image_image lift_sup_distrib lift_Sup_distrib) + finally show ?thesis . +qed + +proposition rank_add_distrib: "rank (x+y) = rank x + rank y" +proof (induction y rule: eps_induct) + case (step y) + show ?case + proof (cases "y=0") + case False + then obtain e where e: "e \ elts y" + by fastforce + have "rank (x+y) = (SUP u\elts (x \ ZFC_in_HOL.set ((+) x ` elts y)). succ (rank u))" + by (metis plus rank_Sup) + also have "\ = (SUP x\elts x. succ (rank x)) \ (SUP z\elts y. succ (rank x + rank z))" + apply (simp add: Sup_Un_distrib image_Un image_image) + apply (simp add: step cong: SUP_cong_simp) + done + also have "\ = (SUP z \ elts y. rank x + succ (rank z))" + proof - + have "rank x \ (SUP z\elts y. ZFC_in_HOL.succ (rank x + rank z))" + using \y \ 0\ + by (auto simp: plus_eq_lift intro: order_trans [OF _ cSUP_upper [OF e]]) + then show ?thesis + by (force simp: plus_V_succ_right simp flip: rank_Sup [of x] intro!: order_antisym) + qed + also have "\ = rank x + (SUP z \ elts y. succ (rank z))" + by (simp add: add_Sup_distrib False) + also have "\ = rank x + rank y" + by (simp add: rank_Sup [of y]) + finally show ?thesis . + qed auto +qed + +lemma Ord_add [simp]: "\Ord x; Ord y\ \ Ord (x+y)" +proof (induction y rule: eps_induct) + case (step y) + then show ?case + by (metis Ord_rank rank_add_distrib rank_of_Ord) +qed + + +definition vle :: "V \ V \ bool" (infix "\" 50) + where "x \ y \ \z::V. x+z = y" + +lemma vle_refl [iff]: "x \ x" + by (metis (no_types) add.right_neutral vle_def) + +lemma vle_antisym: "\x \ y; y \ x\ \ x = y" + by (metis V_equalityI plus_eq_lift sup_ge1 vle_def vsubsetD) + +lemma vle_trans [trans]: "\x \ y; y \ z\ \ x \ z" + by (metis add.assoc vle_def) + +definition vle_comparable :: "V \ V \ bool" + where "vle_comparable x y \ x \ y \ y \ x" + +text\Lemma 3.13\ +lemma comparable: + assumes "a+b = c+d" + shows "vle_comparable a c" +unfolding vle_comparable_def +proof (rule ccontr) + assume non: "\ (a \ c \ c \ a)" + let ?\ = "\x. \z. a+x \ c+z" + have "?\ x" for x + proof (induction x rule: eps_induct) + case (step x) + show ?case + proof (cases "x=0") + case True + with non nonzero_less_TC show ?thesis + using vle_def by auto + next + case False + then obtain v where "v \ elts x" + using trad_foundation by blast + show ?thesis + proof clarsimp + fix z + assume eq: "a + x = c + z" + then have "z \ 0" + using vle_def non by auto + have av: "a+v \ elts (a+x)" + by (simp add: \v \ elts x\) + moreover have "a+x = c \ lift c z" + using eq plus_eq_lift by fastforce + ultimately have "a+v \ elts (c \ lift c z)" + by simp + moreover + define u where "u \ set (elts x - {v})" + have u: "v \ elts u" and xeq: "x = vinsert v u" + using \v \ elts x\ by (auto simp: u_def intro: order_antisym) + have case1: "a+v \ elts c" + proof + assume avc: "a + v \ elts c" + then have "a \ c" + by clarify (metis Un_iff elts_sup_iff eq mem_not_sym mem_plus_V_E plus_eq_lift) + moreover have "a \ lift a x = c \ lift c z" + using eq by (simp add: plus_eq_lift) + ultimately have "lift c z \ lift a x" + by (metis inf.absorb_iff2 inf_commute inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup.commute) + also have "\ = vinsert (a+v) (lift a u)" + by (simp add: lift_def vinsert_def xeq) + finally have *: "lift c z \ vinsert (a + v) (lift a u)" . + have "lift c z \ lift a u" + proof - + have "a + v \ elts (lift c z)" + using lift_self_disjoint [of c z] avc V_disjoint_iff by auto + then show ?thesis + using * less_eq_V_def by auto + qed + { fix e + assume "e \ elts z" + then have "c+e \ elts (lift c z)" + by (simp add: lift_def) + then have "c+e \ elts (lift a u)" + using \lift c z \ lift a u\ by blast + then obtain y where "y \ elts u" "c+e = a+y" + using lift_def by auto + then have False + by (metis elts_vinsert insert_iff step.IH xeq) + } + then show False + using \z \ 0\ by fastforce + qed + ultimately show False + by (metis (no_types) \v \ elts x\ av case1 eq mem_plus_V_E step.IH) + qed + qed + qed + then show False + using assms by blast +qed + +lemma vle1: "x \ y \ x \ y" + using vle_def plus_eq_lift by auto + +lemma vle2: "x \ y \ x \ y" + by (metis (full_types) TC_add' add.right_neutral le_TC_def vle_def nonzero_less_TC) + + +subsection \Generalised Multiplication\ + +text \Credited to Dana Scott\ + +instantiation V :: times +begin + +text\This definition is credited to Tarski\ +definition times_V :: "V \ V \ V" + where "times_V x \ transrec (\f y. \ ((\u. lift (f u) x) ` elts y))" + +instance .. +end + +lemma mult: "x * y = (SUP u\elts y. lift (x * u) x)" + unfolding times_V_def by (subst transrec) (force simp:) + +text \Lemma 4.2\ + +lemma mult_zero_right [simp]: + fixes x::V shows "x * 0 = 0" + by (metis ZFC_in_HOL.Sup_empty elts_0 image_empty mult) + +lemma mult_insert: "x * (vinsert y z) = x*z \ lift (x*y) x" + by (metis (no_types, lifting) elts_vinsert image_insert replacement small_elts sup_commute mult Sup_V_insert) + +lemma mult_succ: "x * succ y = x*y + x" + by (simp add: mult_insert plus_eq_lift succ_def) + +subsubsection\Proposition 4.3\ + +lemma mult_zero_left [simp]: + fixes x::V shows "0 * x = 0" +proof (induction x rule: eps_induct) + case (step x) + then show ?case + by (subst mult) auto +qed + +lemma mult_sup_distrib: + fixes x::V shows "x * (y \ z) = x*y \ x*z" + unfolding mult [of x "y \ z"] mult [of x y] mult [of x z] + by (simp add: Sup_Un_distrib image_Un) + +lemma mult_Sup_distrib: "small Y \ x * (\Y) = \ ((*) x ` Y)" + unfolding mult [of x "\Y"] + by (simp add: cSUP_UNION) (metis mult) + +lemma mult_lift_imp_distrib: "x * (lift y z) = lift (x*y) (x*z) \ x * (y+z) = x*y + x*z" + by (simp add: mult_sup_distrib plus_eq_lift) + +lemma mult_lift: "x * (lift y z) = lift (x*y) (x*z)" +proof (induction z rule: eps_induct) + case (step z) + have "x * lift y z = (SUP u\elts (lift y z). lift (x * u) x)" + using mult by blast + also have "\ = (SUP v\elts z. lift (x * (y + v)) x)" + using lift_def by auto + also have "\ = (SUP v\elts z. lift (x * y + x * v) x)" + using mult_lift_imp_distrib step.IH by auto + also have "\ = (SUP v\elts z. lift (x * y) (lift (x * v) x))" + by (simp add: lift_lift) + also have "\ = lift (x * y) (SUP v\elts z. lift (x * v) x)" + by (simp add: image_image lift_Sup_distrib) + also have "\ = lift (x*y) (x*z)" + by (metis mult) + finally show ?case . +qed + +lemma add_mult_distrib: "x * (y+z) = x*y + x*z" for x::V + by (simp add: mult_lift mult_lift_imp_distrib) + +instantiation V :: monoid_mult +begin +instance +proof + show "1 * x = x" for x :: V + proof (induction x rule: eps_induct) + case (step x) + then show ?case + by (subst mult) auto + qed + show "x * 1 = x" for x :: V + by (subst mult) auto + show "(x * y) * z = x * (y * z)" for x y z::V + proof (induction z rule: eps_induct) + case (step z) + have "(x * y) * z = (SUP u\elts z. lift (x * y * u) (x * y))" + using mult by blast + also have "\ = (SUP u\elts z. lift (x * (y * u)) (x * y))" + using step.IH by auto + also have "\ = (SUP u\elts z. x * lift (y * u) y)" + using mult_lift by auto + also have "\ = x * (SUP u\elts z. lift (y * u) y)" + by (simp add: image_image mult_Sup_distrib) + also have "\ = x * (y * z)" + by (metis mult) + finally show ?case . + qed +qed + +end + +lemma mult_sing_1 [simp]: + fixes x::V shows "x * set{1} = lift x x" + by (subst mult) auto + +lemma mult_2_right [simp]: + fixes x::V shows "x * set{0,1} = x+x" + by (subst mult) (auto simp: Sup_V_insert plus_eq_lift) + +lemma Ord_mult [simp]: "\Ord y; Ord x\ \ Ord (x*y)" +proof (induction y rule: Ord_induct3) + case 0 + then show ?case + by auto +next + case (succ k) + then show ?case + by (simp add: mult_succ) +next + case (Limit k) + then have "Ord (x * \ (elts k))" + by (force simp: mult_Sup_distrib intro: Ord_Sup) + then show ?case + using Limit.hyps Limit_eq_Sup_self by auto +qed + +subsubsection \Proposition 4.4-5\ +proposition rank_mult_distrib: "rank (x*y) = rank x * rank y" +proof (induction y rule: eps_induct) + case (step y) + have "rank (x*y) = (SUP y\elts (SUP u\elts y. lift (x * u) x). succ (rank y))" + by (metis rank_Sup mult) + also have "\ = (SUP u\elts y. SUP r\elts x. succ (rank (x * u + r)))" + apply (simp add: lift_def image_image image_UN) + apply (simp add: Sup_V_def) + done + also have "\ = (SUP u\elts y. SUP r\elts x. succ (rank (x * u) + rank r))" + using rank_add_distrib by auto + also have "\ = (SUP u\elts y. SUP r\elts x. succ (rank x * rank u + rank r))" + using step arg_cong [where f = Sup] by auto + also have "\ = (SUP u\elts y. rank x * rank u + rank x)" + proof (rule SUP_cong) + show "(SUP r\elts x. succ (rank x * rank u + rank r)) = rank x * rank u + rank x" + if "u \ elts y" for u + proof (cases "x=0") + case False + have "(SUP r\elts x. succ (rank x * rank u + rank r)) = rank x * rank u + (SUP y\elts x. succ (rank y))" + proof (rule order_antisym) + show "(SUP r\elts x. succ (rank x * rank u + rank r)) \ rank x * rank u + (SUP y\elts x. succ (rank y))" + by (auto simp: Sup_le_iff simp flip: plus_V_succ_right) + have "rank x * rank u + (SUP y\elts x. succ (rank y)) = (SUP y\elts x. rank x * rank u + succ (rank y))" + by (simp add: add_Sup_distrib False) + also have "\ \ (SUP r\elts x. succ (rank x * rank u + rank r))" + using plus_V_succ_right by auto + finally show "rank x * rank u + (SUP y\elts x. succ (rank y)) \ (SUP r\elts x. succ (rank x * rank u + rank r))" . + qed + also have "\ = rank x * rank u + rank x" + by (metis rank_Sup) + finally show ?thesis . + qed auto + qed auto + also have "\ = rank x * rank y" + by (simp add: rank_Sup [of y] mult_Sup_distrib mult_succ image_image) + finally show ?case . +qed + +lemma mult_le1: + fixes y::V assumes "y \ 0" shows "x \ x * y" +proof (cases "x = 0") + case False + then obtain r where r: "r \ elts x" + by fastforce + from \y \ 0\ show ?thesis + proof (induction y rule: eps_induct) + case (step y) + show ?case + proof (cases "y = 1") + case False + with \y \ 0\ obtain p where p: "p \ elts y" "p \ 0" + by (metis V_equalityI elts_1 insertI1 singletonD trad_foundation) + then have "x*p + r \ elts (lift (x*p) x)" + by (simp add: lift_def r) + moreover have "lift (x*p) x \ x*y" + by (metis bdd_above_iff_small cSUP_upper2 order_refl \p \ elts y\ replacement small_elts mult) + ultimately have "x*p + r \ elts (x*y)" + by blast + moreover have "x*p \ x*p + r" + by (metis TC_add' V_equalityI add.right_neutral eps_induct le_TC_refl less_TC_iff less_imp_le_TC) + ultimately show ?thesis + using step.IH [OF p] le_TC_trans less_TC_iff by blast + qed auto + qed +qed auto + +lemma mult_eq_0_iff [simp]: + fixes y::V shows "x * y = 0 \ x=0 \ y=0" +proof + show "x = 0 \ y = 0" if "x * y = 0" + by (metis le_0 le_TC_def less_TC_imp_not_le mult_le1 that) +qed auto + +lemma lift_lemma: + assumes "x \ 0" "y \ 0" shows "\ lift (x * y) x \ x" + using assms mult_le1 [of concl: x y] + by (auto simp: le_TC_def TC_lift less_TC_def less_TC_imp_not_le) + +lemma mult_le2: + fixes y::V assumes "x \ 0" "y \ 0" "y \ 1" shows "x \ x * y" +proof - + obtain v where v: "v \ elts y" "v \ 0" + using assms by fastforce + have "x \ x * y" + using lift_lemma [of x v] + by (metis \x \ 0\ bdd_above_iff_small cSUP_upper2 order_refl replacement small_elts mult v) + then show ?thesis + using assms mult_le1 [of y x] + by (auto simp: le_TC_def) +qed + + + +subsubsection\Theorem 4.6\ + +theorem mult_eq_imp_0: + assumes "a*x = a*y + b" "b \ a" + shows "b=0" +proof (cases "a=0 \ x=0") + case True + with assms show ?thesis + by (metis add_le_cancel_left mult_eq_0_iff eq_iff le_0) +next + case False + then have "a\0" "x\0" + by auto + then show ?thesis + proof (cases "y=0") + case True + then show ?thesis + using assms less_asym_TC mult_le2 by force + next + case False + have "b=0" if "Ord \" "x \ elts (Vset \)" "y \ elts (Vset \)" for \ + using that assms + proof (induction \ arbitrary: x y b rule: Ord_induct3) + case 0 + then show ?case by auto + next + case (succ k) + define \ where "\ \ \x y. \r. 0 \ r \ r \ a \ a*x = a*y + r" + show ?case + proof (rule ccontr) + assume "b \ 0" + then have "0 \ b" + by (metis nonzero_less_TC) + then have "\ x y" + unfolding \_def using succ.prems by blast + then obtain x' where "\ x' y" "x' \ x" and min: "\x''. x'' \ x' \ \ \ x'' y" + using less_TC_minimal [of "\x. \ x y" x] by blast + then obtain b' where "0 \ b'" "b' \ a" and eq: "a*x' = a*y + b'" + using \_def by blast + have "a*y \ a*x'" + using TC_add' \0 \ b'\ eq by auto + then obtain p where "p \ elts (a * x')" "a * y \ p" + using less_TC_iff by blast + then have "p \ elts (a * y)" + using less_TC_iff less_irrefl_TC by blast + then have "p \ \ (elts ` (\v. lift (a * v) a) ` elts x')" + by (metis \p \ elts (a * x')\ elts_Sup replacement small_elts mult) + then obtain u c where "u \ elts x'" "c \ elts a" "p = a*u + c" + using lift_def by auto + then have "p \ elts (lift (a*y) b')" + using \p \ elts (a * x')\ \p \ elts (a * y)\ eq plus_eq_lift by auto + then obtain d where d: "d \ elts b'" "p = a*y + d" "p = a*u + c" + by (metis \p = a * u + c\ \p \ elts (a * x')\ \p \ elts (a * y)\ eq mem_plus_V_E) + have noteq: "a*y \ a*u" + proof + assume "a*y = a*u" + then have "lift (a*y) a = lift (a*u) a" + by metis + also have "\ \ a*x'" + unfolding mult [of _ x'] using \u \ elts x'\ by (auto intro: cSUP_upper) + also have "\ = a*y \ lift (a*y) b'" + by (simp add: eq plus_eq_lift) + finally have "lift (a*y) a \ a*y \ lift (a*y) b'" . + then have "lift (a*y) a \ lift (a*y) b'" + using add_le_cancel_left less_TC_imp_not_le plus_eq_lift \b' \ a\ by auto + then have "a \ b'" + by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib) + then show False + using \b' \ a\ less_TC_imp_not_le by auto + qed + consider "a*y \ a*u" | "a*u \ a*y" + using d comparable vle_comparable_def by auto + then show False + proof cases + case 1 + then obtain e where e: "a*u = a*y + e" "e \ 0" + by (metis add.right_neutral noteq vle_def) + moreover have "e + c = d" + by (metis e add_right_cancel \p = a * u + c\ \p = a * y + d\ add.assoc) + with \d \ elts b'\ \b' \ a\ have "e \ a" + by (meson less_TC_iff less_TC_trans vle2 vle_def) + ultimately show False + \\contradicts minimality of @{term x'}\ + using min unfolding \_def by (meson \u \ elts x'\ le_TC_def less_TC_iff nonzero_less_TC) + next + case 2 + then obtain e where e: "a*y = a*u + e" "e \ 0" + by (metis add.right_neutral noteq vle_def) + moreover have "e + d = c" + by (metis e add_right_cancel \p = a * u + c\ \p = a * y + d\ add.assoc) + with \d \ elts b'\ \b' \ a\ have "e \ a" + by (metis \c \ elts a\ less_TC_iff vle2 vle_def) + ultimately have "\ y u" + unfolding \_def using nonzero_less_TC by blast + then obtain y' where "\ y' u" "y' \ y" and min: "\x''. x'' \ y' \ \ \ x'' u" + using less_TC_minimal [of "\x. \ x u" y] by blast + then obtain b' where "0 \ b'" "b' \ a" and eq: "a*y' = a*u + b'" + using \_def by blast + have u_k: "u \ elts (Vset k)" + using \u \ elts x'\ \x' \ x\ succ Vset_succ_TC less_TC_iff less_le_TC_trans by blast + have "a*u \ a*y'" + using TC_add' \0 \ b'\ eq by auto + then obtain p where "p \ elts (a * y')" "a * u \ p" + using less_TC_iff by blast + then have "p \ elts (a * u)" + using less_TC_iff less_irrefl_TC by blast + then have "p \ \ (elts ` (\v. lift (a * v) a) ` elts y')" + by (metis \p \ elts (a * y')\ elts_Sup replacement small_elts mult) + then obtain v c where "v \ elts y'" "c \ elts a" "p = a*v + c" + using lift_def by auto + then have "p \ elts (lift (a*u) b')" + using \p \ elts (a * y')\ \p \ elts (a * u)\ eq plus_eq_lift by auto + then obtain d where d: "d \ elts b'" "p = a*u + d" "p = a*v + c" + by (metis \p = a * v + c\ \p \ elts (a * y')\ \p \ elts (a * u)\ eq mem_plus_V_E) + have v_k: "v \ elts (Vset k)" + using Vset_succ_TC \v \ elts y'\ \y' \ y\ less_TC_iff less_le_TC_trans succ.hyps succ.prems(2) by blast + have noteq: "a*u \ a*v" + proof + assume "a*u = a*v" + then have "lift (a*v) a \ a*y'" + unfolding mult [of _ y'] using \v \ elts y'\ by (auto intro: cSUP_upper) + also have "\ = a*u \ lift (a*u) b'" + by (simp add: eq plus_eq_lift) + finally have "lift (a*v) a \ a*u \ lift (a*u) b'" . + then have "lift (a*u) a \ lift (a*u) b'" + by (metis \a * u = a * v\ le_iff_sup lift_sup_distrib sup_left_commute sup_lift_eq_lift) + then have "a \ b'" + by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib) + then show False + using \b' \ a\ less_TC_imp_not_le by auto + qed + consider "a*u \ a*v" | "a*v \ a*u" + using d comparable vle_comparable_def by auto + then show False + proof cases + case 1 + then obtain e where e: "a*v = a*u + e" "e \ 0" + by (metis add.right_neutral noteq vle_def) + moreover have "e + c = d" + by (metis add_right_cancel \p = a * u + d\ \p = a * v + c\ add.assoc e) + with \d \ elts b'\ \b' \ a\ have "e \ a" + by (meson less_TC_iff less_TC_trans vle2 vle_def) + ultimately show False + using succ.IH u_k v_k by blast + next + case 2 + then obtain e where e: "a*u = a*v + e" "e \ 0" + by (metis add.right_neutral noteq vle_def) + moreover have "e + d = c" + by (metis add_right_cancel add.assoc d e) + with \d \ elts b'\ \b' \ a\ have "e \ a" + by (metis \c \ elts a\ less_TC_iff vle2 vle_def) + ultimately show False + using succ.IH u_k v_k by blast + qed + qed + qed + next + case (Limit k) + obtain i j where k: "i \ elts k" "j \ elts k" + and x: "x \ elts (Vset i)" + and y: "y \ elts (Vset j)" + using that Limit by (auto simp: Limit_Vfrom_eq) + show ?case + proof (rule Limit.IH [of "i \ j"]) + show "i \ j \ elts k" + by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff) + show "x \ elts (Vset (i \ j))" "y \ elts (Vset (i \ j))" + using x y by (auto simp: Vfrom_sup) + qed (use Limit.prems in auto) + qed + then show ?thesis + by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt) + qed +qed + +subsubsection\Theorem 4.7\ + +lemma mult_cancellation_half: + assumes "a*x + r = a*y + s" "r \ a" "s \ a" + shows "x \ y" +proof - + have "x \ y" if "Ord \" "x \ elts (Vset \)" "y \ elts (Vset \)" for \ + using that assms + proof (induction \ arbitrary: x y r s rule: Ord_induct3) + case 0 + then show ?case + by auto + next + case (succ k) + show ?case + proof + fix u + assume u: "u \ elts x" + have u_k: "u \ elts (Vset k)" + using Vset_succ succ.hyps succ.prems(1) u by auto + obtain r' where "r' \ elts a" "r \ r'" + using less_TC_iff succ.prems(4) by blast + have "a*u + r' \ elts (lift (a*u) a)" + by (simp add: \r' \ elts a\ lift_def) + also have "\ \ elts (a*x)" + using u by (force simp: mult [of _ x]) + also have "\ \ elts (a*y + s)" + by (metis less_eq_V_def plus_eq_lift succ.prems(3) sup_ge1) + also have "\ = elts (a*y) \ elts (lift (a*y) s)" + by (simp add: plus_eq_lift) + finally have "a * u + r' \ elts (a * y) \ elts (lift (a * y) s)" . + then show "u \ elts y" + proof + assume *: "a * u + r' \ elts (a * y)" + show "u \ elts y" + proof - + obtain v e where v: "v \ elts y" "e \ elts a" "a * u + r' = a * v + e" + using * by (auto simp: mult [of _ y] lift_def) + then have v_k: "v \ elts (Vset k)" + using Vset_succ_TC less_TC_iff succ.prems(2) by blast + then have "u = v" + by (metis succ.IH u_k V_equalityI \r' \ elts a\ le_TC_refl less_TC_iff v(2) v(3) vsubsetD) + then show ?thesis + using \v \ elts y\ by blast + qed + next + assume "a * u + r' \ elts (lift (a * y) s)" + then obtain t where "t \ elts s" and t: "a * u + r' = a * y + t" + using lift_def by auto + have noteq: "a*y \ a*u" + proof + assume "a*y = a*u" + then have "lift (a*y) a = lift (a*u) a" + by metis + also have "\ \ a*x" + unfolding mult [of _ x] using \u \ elts x\ by (auto intro: cSUP_upper) + also have "\ \ a*y \ lift (a*y) s" + using \elts (a * x) \ elts (a * y + s)\ plus_eq_lift by auto + finally have "lift (a*y) a \ a*y \ lift (a*y) s" . + then have "lift (a*y) a \ lift (a*y) s" + using add_le_cancel_left less_TC_imp_not_le plus_eq_lift \s \ a\ by auto + then have "a \ s" + by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib) + then show False + using \s \ a\ less_TC_imp_not_le by auto + qed + consider "a * u \ a * y" | "a * y \ a * u" + using t comparable vle_comparable_def by blast + then have "False" + proof cases + case 1 + then obtain c where "a*y = a*u + c" + by (metis vle_def) + then have "c+t = r'" + by (metis add_right_cancel add.assoc t) + then have "c \ a" + using \r' \ elts a\ less_TC_iff vle2 vle_def by force + moreover have "c \ 0" + using \a * y = a * u + c\ noteq by auto + ultimately show ?thesis + using \a * y = a * u + c\ mult_eq_imp_0 by blast + next + case 2 + then obtain c where "a*u = a*y + c" + by (metis vle_def) + then have "c+r' = t" + by (metis add_right_cancel add.assoc t) + then have "c \ a" + by (metis \t \ elts s\ less_TC_iff less_TC_trans \s \ a\ vle2 vle_def) + moreover have "c \ 0" + using \a * u = a * y + c\ noteq by auto + ultimately show ?thesis + using \a * u = a * y + c\ mult_eq_imp_0 by blast + qed + then show "u \ elts y" .. + qed + qed + next + case (Limit k) + obtain i j where k: "i \ elts k" "j \ elts k" + and x: "x \ elts (Vset i)" and y: "y \ elts (Vset j)" + using that Limit by (auto simp: Limit_Vfrom_eq) + show ?case + proof (rule Limit.IH [of "i \ j"]) + show "i \ j \ elts k" + by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff) + show "x \ elts (Vset (i \ j))" "y \ elts (Vset (i \ j))" + using x y by (auto simp: Vfrom_sup) + thm Limit.prems + qed (auto intro: Limit.prems) + qed + then show ?thesis + by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt) +qed + + +theorem mult_cancellation_lemma: + assumes "a*x + r = a*y + s" "r \ a" "s \ a" + shows "x=y \ r=s" + by (metis add_right_cancel mult_cancellation_half antisym assms) + +corollary mult_cancellation [simp]: + fixes a::V + assumes "a \ 0" + shows "a*x = a*y \ x=y" + by (metis assms nonzero_less_TC mult_cancellation_lemma) + +corollary lift_mult_TC_disjoint: + fixes x::V + assumes "x \ y" + shows "lift (a*x) (TC a) \ lift (a*y) (TC a) = 0" + apply (rule V_equalityI) + using assms + by (force simp: less_TC_def inf_V_def zero_V_def lift_def image_iff dest: mult_cancellation_lemma) + +corollary lift_mult_disjoint: + fixes x::V + assumes "x \ y" + shows "lift (a*x) a \ lift (a*y) a = 0" +proof - + have "lift (a*x) a \ lift (a*y) a \ lift (a*x) (TC a) \ lift (a*y) (TC a)" + by (metis TC' inf_mono lift_sup_distrib sup_ge1) + then show ?thesis + using assms lift_mult_TC_disjoint by auto +qed + +lemma mult_add_mem: + assumes "a*x + r \ elts (a*y)" "r \ a" + shows "x \ elts y" "r \ elts a" +proof - + obtain v s where v: "a * x + r = a * v + s" "v \ elts y" "s \ elts a" + using assms unfolding mult [of a y] lift_def by auto + then show "x \ elts y" + by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma vsubsetD) + show "r \ elts a" + by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma v(1) v(3) vsubsetD) +qed + +lemma mult_add_mem_0: "a*x \ elts (a*y) \ x \ elts y \ 0 \ elts a" + proof - + have "x \ elts y" + if "a * x \ elts (a * y) \ 0 \ elts a" + using that using mult_add_mem [of a x 0] + using nonzero_less_TC by force + moreover have "a * x \ elts (a * y)" + if "x \ elts y" "0 \ elts a" + using that by (force simp: image_iff mult [of a y] lift_def) + ultimately show ?thesis + by (metis mult_eq_0_iff add.right_neutral mult_add_mem(2) nonzero_less_TC) +qed + + +lemma vcard_mult: "vcard (x * y) = vcard x \ vcard y" +proof - + have 1: "elts (lift (x * u) x) \ elts x" if "u \ elts y" for u + by (metis cardinal_eqpoll eqpoll_sym eqpoll_trans card_lift) + have 2: "pairwise (\u u'. disjnt (elts (lift (x * u) x)) (elts (lift (x * u') x))) (elts y)" + by (simp add: pairwise_def disjnt_def) (metis V_disjoint_iff lift_mult_disjoint) + have "x * y = (SUP u\elts y. lift (x * u) x)" + using mult by blast + then have "elts (x * y) \ (\u\elts y. elts (lift (x * u) x))" + by simp + also have "\ \ elts y \ elts x" + using Union_eqpoll_Times [OF 1 2] . + also have "\ \ elts x \ elts y" + by (simp add: times_commute_eqpoll) + also have "\ \ elts (vcard x) \ elts (vcard y)" + using cardinal_eqpoll eqpoll_sym times_eqpoll_cong by blast + also have "\ \ elts (vcard x \ vcard y)" + by (simp add: cmult_def elts_vcard_VSigma_eqpoll eqpoll_sym) + finally have "elts (x * y) \ elts (vcard x \ vcard y)" . + then show ?thesis + by (metis cadd_cmult_distrib cadd_def cardinal_cong cardinal_idem vsum_0_eqpoll) +qed + +proposition TC_mult: "TC(x * y) = (SUP r \ elts (TC x). SUP u \ elts (TC y). set{x * u + r})" +proof (cases "x = 0") + case False + have *: "TC(x * y) = (SUP u \ elts (TC y). lift (x * u) (TC x))" for y + proof (induction y rule: eps_induct) + case (step y) + have "TC(x * y) = (SUP u \ elts y. TC (lift (x * u) x))" + by (simp add: mult [of x y] TC_Sup_distrib image_image) + also have "\ = (SUP u \ elts y. TC(x * u) \ lift (x * u) (TC x))" + by (simp add: TC_lift False) + also have "\ = (SUP u \ elts y. (SUP z \ elts (TC u). lift (x * z) (TC x)) \ lift (x * u) (TC x))" + by (simp add: step) + also have "\ = (SUP u \ elts (TC y). lift (x * u) (TC x))" + by (auto simp: TC' [of y] image_Un Sup_Un_distrib TC_Sup_distrib cSUP_UNION SUP_sup_distrib) + finally show ?case . + qed + show ?thesis + by (force simp: * lift_def) +qed auto + + +corollary vcard_TC_mult: "vcard (TC(x * y)) = vcard (TC x) \ vcard (TC y)" +proof - + have "(\u\elts (TC x). \v\elts (TC y). {x * v + u}) = (\u\elts (TC x). (\v. x * v + u) ` elts (TC y))" + by (simp add: UNION_singleton_eq_range) + also have "\ \ (\x\elts (TC x). elts (lift (TC y * x) (TC y)))" + proof (rule UN_eqpoll_UN) + show "(\v. x * v + u) ` elts (TC y) \ elts (lift (TC y * u) (TC y))" + if "u \ elts (TC x)" for u + proof - + have "inj_on (\v. x * v + u) (elts (TC y))" + by (meson inj_onI less_TC_def mult_cancellation_lemma that) + then have "(\v. x * v + u) ` elts (TC y) \ elts (TC y)" + by (rule inj_on_image_eqpoll_self) + also have "\ \ elts (lift (TC y * u) (TC y))" + by (simp add: eqpoll_lift eqpoll_sym) + finally show ?thesis . + qed + show "pairwise (\u ya. disjnt ((\v. x * v + u) ` elts (TC y)) ((\v. x * v + ya) ` elts (TC y))) (elts (TC x))" + apply (auto simp: pairwise_def disjnt_def) + using less_TC_def mult_cancellation_lemma by blast + show "pairwise (\u ya. disjnt (elts (lift (TC y * u) (TC y))) (elts (lift (TC y * ya) (TC y)))) (elts (TC x))" + apply (auto simp: pairwise_def disjnt_def) + by (metis Int_iff V_disjoint_iff empty_iff lift_mult_disjoint) + qed + also have "\ = elts (TC y * TC x)" + by (metis elts_Sup image_image mult replacement small_elts) + finally have "(\u\elts (TC x). \v\elts (TC y). {x * v + u}) \ elts (TC y * TC x)" . + then show ?thesis + apply (subst cmult_commute) + by (simp add: TC_mult cardinal_cong flip: vcard_mult) +qed + +end diff --git a/thys/ZFC_in_HOL/ROOT b/thys/ZFC_in_HOL/ROOT new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/ROOT @@ -0,0 +1,13 @@ +chapter AFP + +session ZFC_in_HOL (AFP) = HOL + + options [timeout = 600] + sessions + "HOL-Library" + "HOL-Cardinals" + theories + Kirby + ZFC_Typeclasses + document_files + "root.tex" + "root.bib" diff --git a/thys/ZFC_in_HOL/ZFC_Cardinals.thy b/thys/ZFC_in_HOL/ZFC_Cardinals.thy new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/ZFC_Cardinals.thy @@ -0,0 +1,1433 @@ +section \Cartesian products, Disjoint Sums, Ranks, Cardinals\ + +theory ZFC_Cardinals + imports ZFC_in_HOL + +begin + +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 UN 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 + + +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) + +text\Introduction rules for the injections (as equivalences)\ + +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) + +text \Elimination rule\ + +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) + +text \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) + + +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 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 less_TC_trans [trans]: "\x \ y; y \ z\ \ x \ z" + by (meson TC_least Transset_TC Transset_def less_TC_def less_eq_V_def subsetD) + +lemma less_le_TC_trans [trans]: "\x \ y; y \ z\ \ x \ z" + using le_TC_def less_TC_trans by blast + +lemma le_less_TC_trans [trans]: "\x \ y; y \ z\ \ x \ z" + using le_TC_def less_TC_trans by blast + +lemma le_TC_trans [trans]: "\x \ y; y \ z\ \ x \ z" + using le_TC_def le_less_TC_trans by blast + +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 \ \ (\x\X. TC ` elts x) \ \ (TC ` X)" + using assms + apply (auto simp: Sup_le_iff) + using arg_subset_TC apply blast + by (metis TC_least Transset_TC Transset_def arg_subset_TC vsubsetD) + 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)" + by (smt Transset_TC Transset_def less_TC_def inf.bounded_iff inf.cobounded1 inf.commute inf_idem local.step vsubsetD vsubsetI) + 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" + apply (induction rule: Ord_induct) + by (metis (no_types, lifting) Ord_equality SUP_cong rank_Sup) + +lemma rank_lt: "a \ elts b \ rank a < rank b" + apply (subst rank [of b]) + by (metis (no_types, lifting) Ord_mem_iff_lt Ord_rank UN UN_iff elts_of_set elts_succ insert_iff rank small_elts) + +lemma rank_0 [simp]: "rank 0 = 0" + unfolding rank_def + using transrec by fastforce + +lemma rank_succ [simp]: "rank(succ x) = succ(rank x)" +proof (rule order_antisym) + show "rank (succ x) \ succ (rank x)" + apply (subst rank [of "succ x"]) + apply (metis (no_types, lifting) Sup_insert elts_of_set elts_succ equals0D image_insert rank small_sup_iff subset_insertI sup.orderE vsubsetI) + done + 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" + apply (rule vsubsetI) + using rank [of a] rank [of b] UN by auto + +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 (SUP y\elts (\ A). succ (rank y)) \ elts (\ (rank ` A))" + apply auto(*SLOW*) + using Ord_mem_iff_lt Ord_rank rank_lt apply blast + by (meson less_le_not_le 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 (metis (mono_tags, lifting) ZFC_in_HOL.Sup_least ZFC_in_HOL.Sup_upper image_iff 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 + apply (rule 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 "(SUP j\elts (rank x). VPow (Vfrom A j)) \ (SUP j\elts x. VPow (Vfrom A j))" + apply (rule Sup_least, clarify) + apply (simp add: rank [of x]) + using step.IH + by (metis Ord_rank OrdmemD Vfrom_mono2 dual_order.trans inf_sup_aci(5) less_V_def sup.orderE) + 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 "(SUP j\elts x. VPow (Vfrom A j)) \ (SUP 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 + apply (simp add: Vfrom_succ) + using TC_least Transset_Vfrom 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\Order types\ + +definition ordermap :: "[V set, (V \ V) set, V] \ V" + where "ordermap A r \ wfrec r (\f x. set (f ` {y \ A. (y,x) \ r}))" + +definition ordertype :: "[V set, (V \ V) 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: "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 Ord_ordermap [iff]: assumes "wf r" "trans r" "x \ A" 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 "x \ ordermap A r ` {z \ A. (z, y) \ r}" + by (metis (no_types, lifting) elts_of_set empty_iff \wf r\ ordermap 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 (no_types, lifting) OrdI Ord_is_Transset \wf r\ ordermap) +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 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: "Ord(ordertype A (VWO - Id))" + using antisym_VWO trans_VWO trans_diff_Id wf_Ord_ordertype wf_VWO by blast + +subsubsection\@{term ordermap} preserves the orderings in both directions\ + +lemma ordermap_mono: + "\(w, x) \ r; wf r; w \ A; small A\ \ ordermap A r w \ elts (ordermap A r x)" + by (simp add: ordermap [of r A]) + +lemma converse_ordermap_mono: + assumes "ordermap A r y \ elts (ordermap A r x)" "wf r" "total r" "y \ A" "x \ 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 r\ by (meson UNIV_I total_on_def) + then show ?thesis + using ordermap_mono + by (meson assms(1) assms(2) assms(5) assms(6) mem_not_sym) +qed + +lemma ordermap_surj: "elts (ordertype A r) \ ordermap A r ` A" + unfolding ordertype_def by simp + +lemma ordermap_bij: + assumes "wf r" "total 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" + apply (rule inj_onI) + by (metis UNIV_I assms mem_not_refl ordermap_mono total_on_def) + show "ordermap A r ` A = elts (ordertype A r)" + by (simp add: assms(3) ordertype_def) +qed + +lemma wf_ordertype_eqpoll: + assumes "wf r" "total 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 (VWO - Id)) \ A" + using assms total_VWOId wf_VWO wf_ordertype_eqpoll by auto + +subsection\Cardinality of a set\ + +definition + vcard :: "V\V" + where "vcard a \ (LEAST i. Ord i \ elts i \ elts a)" + +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 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 force + 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 cardinal_idem [simp]: "vcard (vcard a) = vcard a" + using cardinal_cong cardinal_eqpoll by blast + +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) + +text\The cardinals are the initial ordinals.\ +lemma Card_iff_initial: "Card \ \ Ord \ \ (\\. Ord \ \ \ < \ \ ~ elts \ \ elts \)" +proof - + { fix j + assume \: "Card \" "elts j \ elts \" "Ord j" + assume "j < \" + also have "\ = (LEAST i. Ord i \ elts i \ elts \)" using \ + by (simp add: Card_def vcard_def) + finally have "j < (LEAST i. Ord i \ elts i \ elts \)" . + hence "False" using \ + using not_less_Ord_Least by fastforce + } + then show ?thesis + by (blast intro: CardI Card_is_Ord) +qed + +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 Ord_cardinal [of a] Ord_cardinal [of b] +proof (cases rule: Ord_linear_le) + case le thus ?thesis . +next + case ge + have "elts b \ elts (vcard b)" + by (simp add: cardinal_eqpoll eqpoll_sym) + also have "\ \ elts (vcard a)" + by (meson ge less_eq_V_def subset_imp_lepoll) + also have "\ \ elts a" + by (simp add: cardinal_eqpoll) + finally have "elts b \ elts a" . + hence "elts a \ elts b" + using assms lepoll_antisym by blast + hence "vcard a = vcard b" + by (rule cardinal_cong) + thus ?thesis by simp +qed + +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 lesspoll_imp_Card_less: + assumes "elts a \ elts b" shows "vcard a < vcard b" + by (metis assms cardinal_eqpoll eqpoll_sym eqpoll_trans le_neq_trans lepoll_imp_Card_le lesspoll_def) + +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 + + +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: inj_on_vpair 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 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 + unfolding one_V_def cmult_def + using Card_def assms cardinal_cong by auto +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) + + +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 + + +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 "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 csucc_works: + assumes "Card \" shows "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 + +lemma + assumes "Card \" + shows Card_csucc [simp]: "Card (csucc \)" and less_csucc: "\ < csucc \" + using csucc_works [OF assms] by auto + +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]) + show "Ord (vcard (set (insert a A))) \ Card (vcard (set (insert a A))) \ vcard (set A) < vcard (set (insert a A))" + apply (auto simp: Card_def) + by (metis FA Finite finite_insert_lepoll FA a elts_of_set eqpoll_imp_lepoll eqpoll_sym lesspoll_def lesspoll_imp_Card_less small_insert 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 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 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) + +end diff --git a/thys/ZFC_in_HOL/ZFC_Library.thy b/thys/ZFC_in_HOL/ZFC_Library.thy new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/ZFC_Library.thy @@ -0,0 +1,431 @@ +theory ZFC_Library + imports "HOL-Library.Countable_Set" "HOL-Library.Equipollence" "HOL-Cardinals.Cardinals" + +begin + +text\These are a mixture of results that mostly deserve to be installed in the main Isabelle/HOL libraries.\ + +(*REPLACE*) +notation Sup ("\") +context conditionally_complete_lattice +begin +lemma cSUP_subset_mono: "A \ {} \ bdd_above (g ` B) \ A \ B \ (\x. x \ A \ f x \ g x) \ \(f ` A) \ \(g ` B)" + by (rule cSUP_mono) auto +end + +lemma lepoll_refl [iff]: "A \ A" + by (simp add: subset_imp_lepoll) + +lemma empty_lepoll [iff]: "{} \ A" + by (simp add: lepoll_iff) + +lemma lepoll_Pow_self: "A \ Pow A" + unfolding lepoll_def inj_def + proof (intro exI conjI) + show "inj_on (\x. {x}) A" + by (auto simp: inj_on_def) +qed auto + +lemma lesspoll_Pow_self: "A \ Pow A" + unfolding lesspoll_def + by (meson lepoll_Pow_self Cantors_paradox bij_betw_def eqpoll_def) + +lemma eqpoll_refl [iff]: "A \ A" + by (simp add: lepoll_antisym subset_imp_lepoll) + +lemma inj_on_image_eqpoll_self: "inj_on f A \ f ` A \ A" + by (meson bij_betw_def eqpoll_def eqpoll_sym) + +lemma inj_on_image_lepoll_1 [simp]: + assumes "inj_on f A" shows "f ` A \ B \ A \ B" + by (meson assms image_lepoll lepoll_def lepoll_trans order_refl) + +lemma inj_on_image_lepoll_2 [simp]: + assumes "inj_on f B" shows "A \ f ` B \ A \ B" + by (meson assms eq_iff image_lepoll lepoll_def lepoll_trans) + +lemma inj_on_image_lesspoll_1 [simp]: + assumes "inj_on f A" shows "f ` A \ B \ A \ B" + by (meson assms image_lepoll le_less lepoll_def lesspoll_trans1) + +lemma inj_on_image_lesspoll_2 [simp]: + assumes "inj_on f B" shows "A \ f ` B \ A \ B" + by (meson assms eqpoll_sym inj_on_image_eqpoll_self lesspoll_eq_trans) + +lemma inj_on_image_eqpoll_1 [simp]: + assumes "inj_on f A" shows "f ` A \ B \ A \ B" + by (metis assms eqpoll_trans inj_on_image_eqpoll_self eqpoll_sym) + +lemma inj_on_image_eqpoll_2 [simp]: + assumes "inj_on f B" shows "A \ f ` B \ A \ B" + by (metis assms inj_on_image_eqpoll_1 eqpoll_sym) + +lemma times_square_lepoll: "A \ A \ A" + unfolding lepoll_def inj_def +proof (intro exI conjI) + show "inj_on (\x. (x,x)) A" + by (auto simp: inj_on_def) +qed auto + +lemma times_commute_eqpoll: "A \ B \ B \ A" + unfolding eqpoll_def + by (force intro: bij_betw_byWitness [where f = "\(x,y). (y,x)" and f' = "\(x,y). (y,x)"]) + +lemma times_assoc_eqpoll: "(A \ B) \ C \ A \ (B \ C)" + unfolding eqpoll_def + by (force intro: bij_betw_byWitness [where f = "\((x,y),z). (x,(y,z))" and f' = "\(x,(y,z)). ((x,y),z)"]) + +lemma times_singleton_eqpoll: "{a} \ A \ A" +proof - + have "{a} \ A = (\x. (a,x)) ` A" + by auto + also have "\ \ A" + proof (rule inj_on_image_eqpoll_self) + show "inj_on (Pair a) A" + by (auto simp: inj_on_def) + qed + finally show ?thesis . +qed + + +lemma Union_eqpoll_Times: + assumes B: "\x. x \ A \ F x \ B" and disj: "pairwise (\x y. disjnt (F x) (F y)) A" + shows "(\x\A. F x) \ A \ B" +proof (rule lepoll_antisym) + obtain b where b: "\x. x \ A \ bij_betw (b x) (F x) B" + using B unfolding eqpoll_def by metis + show "\(F ` A) \ A \ B" + unfolding lepoll_def + proof (intro exI conjI) + define \ where "\ \ \z. THE x. x \ A \ z \ F x" + have \: "\ z = x" if "x \ A" "z \ F x" for x z + unfolding \_def + apply (rule the_equality) + apply (simp add: that) + by (metis disj disjnt_iff pairwiseD that) + let ?f = "\z. (\ z, b (\ z) z)" + show "inj_on ?f (\(F ` A))" + unfolding inj_on_def + by clarify (metis \ b bij_betw_inv_into_left) + show "?f ` \(F ` A) \ A \ B" + using \ b bij_betwE by blast + qed + show "A \ B \ \(F ` A)" + unfolding lepoll_def + proof (intro exI conjI) + let ?f = "\(x,y). inv_into (F x) (b x) y" + have *: "inv_into (F x) (b x) y \ F x" if "x \ A" "y \ B" for x y + by (metis b bij_betw_imp_surj_on inv_into_into that) + then show "inj_on ?f (A \ B)" + unfolding inj_on_def + by clarsimp (metis (mono_tags, lifting) b bij_betw_inv_into_right disj disjnt_iff pairwiseD) + show "?f ` (A \ B) \ \ (F ` A)" + by clarsimp (metis b bij_betw_imp_surj_on inv_into_into) + qed +qed + + +lemma countable_iff_lepoll: "countable A \ A \ (UNIV :: nat set)" + by (auto simp: countable_def lepoll_def) + +lemma infinite_times_eqpoll_self: + assumes "infinite A" shows "A \ A \ A" + by (simp add: Times_same_infinite_bij_betw assms eqpoll_def) + +lemma finite_lepoll_infinite: + assumes "infinite A" "finite B" shows "B \ A" +proof - + have "B \ (UNIV::nat set)" + unfolding lepoll_def + using finite_imp_inj_to_nat_seg [OF \finite B\] by blast + then show ?thesis + using \infinite A\ infinite_le_lepoll lepoll_trans by auto +qed + +lemma finite_lesspoll_infinite: + assumes "infinite A" "finite B" shows "B \ A" + by (meson assms eqpoll_finite_iff finite_lepoll_infinite lesspoll_def) + + +lemma infinite_insert_lepoll: + assumes "infinite A" shows "insert a A \ A" +proof - + obtain f :: "nat \ 'a" where "inj f" and f: "range f \ A" + using assms infinite_countable_subset by blast + let ?g = "(\z. if z=a then f 0 else if z \ range f then f (Suc (inv f z)) else z)" + show ?thesis + unfolding lepoll_def + proof (intro exI conjI) + show "inj_on ?g (insert a A)" + using inj_on_eq_iff [OF \inj f\] + by (auto simp: inj_on_def) + show "?g ` insert a A \ A" + using f by auto + qed +qed + +lemma infinite_insert_eqpoll: "infinite A \ insert a A \ A" + by (simp add: lepoll_antisym infinite_insert_lepoll subset_imp_lepoll subset_insertI) + + +lemma Un_lepoll_mono: + assumes "A \ C" "B \ D" "disjnt C D" shows "A \ B \ C \ D" +proof - + obtain f g where inj: "inj_on f A" "inj_on g B" and fg: "f ` A \ C" "g ` B \ D" + by (meson assms lepoll_def) + have "inj_on (\x. if x \ A then f x else g x) (A \ B)" + using inj \disjnt C D\ fg unfolding disjnt_iff + by (fastforce intro: inj_onI dest: inj_on_contraD split: if_split_asm) + with fg show ?thesis + unfolding lepoll_def + by (rule_tac x="\x. if x \ A then f x else g x" in exI) auto +qed + +lemma Un_eqpoll_cong: "\A \ C; B \ D; disjnt A B; disjnt C D\ \ A \ B \ C \ D" + by (meson Un_lepoll_mono eqpoll_imp_lepoll eqpoll_sym lepoll_antisym) + +lemma sum_lepoll_mono: + assumes "A \ C" "B \ D" shows "A <+> B \ C <+> D" +proof - + obtain f g where "inj_on f A" "f ` A \ C" "inj_on g B" "g ` B \ D" + by (meson assms lepoll_def) + then show ?thesis + unfolding lepoll_def + by (rule_tac x="case_sum (Inl \ f) (Inr \ g)" in exI) (force simp: inj_on_def) +qed + +lemma sum_eqpoll_cong: "\A \ C; B \ D\ \ A <+> B \ C <+> D" + by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym sum_lepoll_mono) + +lemma Sigma_lepoll_mono: + assumes "A \ C" "\x. x \ A \ B x \ D x" shows "Sigma A B \ Sigma C D" +proof - + have "\x. x \ A \ \f. inj_on f (B x) \ f ` (B x) \ D x" + by (meson assms lepoll_def) + then obtain f where "\x. x \ A \ inj_on (f x) (B x) \ f x ` B x \ D x" + by metis + with \A \ C\ show ?thesis + unfolding lepoll_def inj_on_def + by (rule_tac x="\(x,y). (x, f x y)" in exI) force +qed + +lemma times_lepoll_mono: + assumes "A \ C" "B \ D" shows "A \ B \ C \ D" +proof - + obtain f g where "inj_on f A" "f ` A \ C" "inj_on g B" "g ` B \ D" + by (meson assms lepoll_def) + then show ?thesis + unfolding lepoll_def + by (rule_tac x="\(x,y). (f x, g y)" in exI) (auto simp: inj_on_def) +qed + +lemma times_eqpoll_cong: "\A \ C; B \ D\ \ A \ B \ C \ D" + by (metis eqpoll_imp_lepoll eqpoll_sym lepoll_antisym times_lepoll_mono) + +lemma + assumes "B \ {}" shows lepoll_times1: "A \ A \ B" and lepoll_times2: "A \ B \ A" + using assms lepoll_iff by fastforce+ + + +lemma times_0_eqpoll: "{} \ A \ {}" + by (simp add: eqpoll_iff_bijections) + +lemma sum_times_distrib_eqpoll: "(A <+> B) \ C \ (A \ C) <+> (B \ C)" + unfolding eqpoll_def +proof + show "bij_betw (\(x,z). case_sum(\y. Inl(y,z)) (\y. Inr(y,z)) x) ((A <+> B) \ C) (A \ C <+> B \ C)" + by (rule bij_betw_byWitness [where f' = "case_sum (\(x,z). (Inl x, z)) (\(y,z). (Inr y, z))"]) auto +qed + +lemma prod_insert_eqpoll: + assumes "a \ A" shows "insert a A \ B \ B <+> A \ B" + unfolding eqpoll_def + proof + show "bij_betw (\(x,y). if x=a then Inl y else Inr (x,y)) (insert a A \ B) (B <+> A \ B)" + by (rule bij_betw_byWitness [where f' = "case_sum (\y. (a,y)) id"]) (auto simp: assms) +qed + +lemma insert_lepoll_insertD: + assumes "insert u A \ insert v B" "u \ A" "v \ B" shows "A \ B" +proof - + obtain f where inj: "inj_on f (insert u A)" and fim: "f ` (insert u A) \ insert v B" + by (meson assms lepoll_def) + show ?thesis + unfolding lepoll_def + proof (intro exI conjI) + let ?g = "\x\A. if f x = v then f u else f x" + show "inj_on ?g A" + using inj \u \ A\ by (auto simp: inj_on_def) + show "?g ` A \ B" + using fim \u \ A\ image_subset_iff inj inj_on_image_mem_iff by fastforce + qed +qed + +lemma insert_eqpoll_insertD: "\insert u A \ insert v B; u \ A; v \ B\ \ A \ B" + by (meson insert_lepoll_insertD eqpoll_imp_lepoll eqpoll_sym lepoll_antisym) + +lemma insert_lepoll_cong: + assumes "A \ B" "b \ B" shows "insert a A \ insert b B" +proof - + obtain f where f: "inj_on f A" "f ` A \ B" + by (meson assms lepoll_def) + let ?f = "\u \ insert a A. if u=a then b else f u" + show ?thesis + unfolding lepoll_def + proof (intro exI conjI) + show "inj_on ?f (insert a A)" + using f \b \ B\ by (auto simp: inj_on_def) + show "?f ` insert a A \ insert b B" + using f \b \ B\ by auto + qed +qed + +lemma insert_eqpoll_cong: + "\A \ B; a \ A; b \ B\ \ insert a A \ insert b B" + apply (rule lepoll_antisym) + apply (simp add: eqpoll_imp_lepoll insert_lepoll_cong)+ + by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong) + +lemma insert_eqpoll_insert_iff: + "\a \ A; b \ B\ \ insert a A \ insert b B \ A \ B" + by (meson insert_eqpoll_insertD insert_eqpoll_cong) + +lemma insert_lepoll_insert_iff: + " \a \ A; b \ B\ \ (insert a A \ insert b B) \ (A \ B)" + by (meson insert_lepoll_insertD insert_lepoll_cong) + +lemma less_imp_insert_lepoll: + assumes "A \ B" shows "insert a A \ B" +proof - + obtain f where "inj_on f A" "f ` A \ B" + using assms by (metis bij_betw_def eqpoll_def lepoll_def lesspoll_def psubset_eq) + then obtain b where b: "b \ B" "b \ f ` A" + by auto + show ?thesis + unfolding lepoll_def + proof (intro exI conjI) + show "inj_on (f(a:=b)) (insert a A)" + using b \inj_on f A\ by (auto simp: inj_on_def) + show "(f(a:=b)) ` insert a A \ B" + using \f ` A \ B\ by (auto simp: b) + qed +qed + +lemma finite_insert_lepoll: "finite A \ (insert a A \ A) \ (a \ A)" +proof (induction A rule: finite_induct) + case (insert x A) + then show ?case + apply (auto simp: insert_absorb) + by (metis insert_commute insert_iff insert_lepoll_insertD) +qed auto + + +lemma lists_lepoll_mono: + assumes "A \ B" shows "lists A \ lists B" +proof - + obtain f where "inj_on f A" "f ` A \ B" + by (meson assms lepoll_def) + then show ?thesis + unfolding lepoll_def + by (rule_tac x="map f" in exI) (simp add: inj_on_map_lists map_lists_mono) +qed + +lemma infinite_finite_times_lepoll_self: + assumes "infinite A" "finite B" shows "A \ B \ A" +proof - + have "B \ A" + by (simp add: assms finite_lepoll_infinite) + then have "A \ B \ A \ A" + by (simp add: subset_imp_lepoll times_lepoll_mono) + also have "\ \ A" + by (simp add: \infinite A\ infinite_times_eqpoll_self) + finally show ?thesis . +qed + + +lemma lists_n_lepoll_self: + assumes "infinite A" shows "{l \ lists A. length l = n} \ A" +proof (induction n) + case 0 + have "{l \ lists A. length l = 0} = {[]}" + by auto + then show ?case + by (metis Set.set_insert assms ex_in_conv finite.emptyI singleton_lepoll) +next + case (Suc n) + have "{l \ lists A. length l = Suc n} = (\x\A. \l \ {l \ lists A. length l = n}. {x#l})" + by (auto simp: length_Suc_conv) + also have "\ \ A \ {l \ lists A. length l = n}" + unfolding lepoll_iff + by (rule_tac x="\(x,l). Cons x l" in exI) auto + also have "\ \ A" + proof (cases "finite {l \ lists A. length l = n}") + case True + then show ?thesis + using assms infinite_finite_times_lepoll_self by blast + next + case False + have "A \ {l \ lists A. length l = n} \ A \ A" + by (simp add: Suc.IH subset_imp_lepoll times_lepoll_mono) + also have "\ \ A" + by (simp add: assms infinite_times_eqpoll_self) + finally show ?thesis . + qed + finally show ?case . +qed + +lemma lepoll_lists: "A \ lists A" + unfolding lepoll_def inj_on_def by(rule_tac x="\x. [x]" in exI) auto + +lemma infinite_eqpoll_lists: + assumes "infinite A" shows "lists A \ A" +proof - + have "lists A \ Sigma UNIV (\n. {l \ lists A. length l = n})" + unfolding lepoll_iff + by (rule_tac x=snd in exI) (auto simp: in_listsI snd_image_Sigma) + also have "\ \ (UNIV::nat set) \ A" + by (rule Sigma_lepoll_mono) (auto simp: lists_n_lepoll_self assms) + also have "\ \ A \ A" + by (metis assms infinite_le_lepoll order_refl subset_imp_lepoll times_lepoll_mono) + also have "\ \ A" + by (simp add: assms infinite_times_eqpoll_self) + finally show ?thesis + by (simp add: lepoll_antisym lepoll_lists) +qed + + +lemma UN_lepoll_UN: + assumes A: "\x. x \ A \ B x \ C x" + and disj: "pairwise (\x y. disjnt (C x) (C y)) A" + shows "\ (B`A) \ \ (C`A)" +proof - + obtain f where f: "\x. x \ A \ inj_on (f x) (B x) \ f x ` (B x) \ (C x)" + using A unfolding lepoll_def by metis + show ?thesis + unfolding lepoll_def + proof (intro exI conjI) + define \ where "\ \ \z. @x. x \ A \ z \ B x" + have \: "\ z \ A \ z \ B (\ z)" if "x \ A" "z \ B x" for x z + unfolding \_def by (metis (mono_tags, lifting) someI_ex that) + let ?f = "\z. (f (\ z) z)" + show "inj_on ?f (\(B ` A))" + using disj f unfolding inj_on_def disjnt_iff pairwise_def image_subset_iff + by (metis UN_iff \) + show "?f ` \ (B ` A) \ \ (C ` A)" + using \ f unfolding image_subset_iff by blast + qed +qed + +lemma UN_eqpoll_UN: + assumes A: "\x. x \ A \ B x \ C x" + and B: "pairwise (\x y. disjnt (B x) (B y)) A" + and C: "pairwise (\x y. disjnt (C x) (C y)) A" + shows "(\x\A. B x) \ (\x\A. C x)" +proof (rule lepoll_antisym) + show "\ (B ` A) \ \ (C ` A)" + by (meson A C UN_lepoll_UN eqpoll_imp_lepoll) + show "\ (C ` A) \ \ (B ` A)" + by (simp add: A B UN_lepoll_UN eqpoll_imp_lepoll eqpoll_sym) +qed + +end diff --git a/thys/ZFC_in_HOL/ZFC_Typeclasses.thy b/thys/ZFC_in_HOL/ZFC_Typeclasses.thy new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/ZFC_Typeclasses.thy @@ -0,0 +1,274 @@ +section \Type Classes for ZFC\ + +theory ZFC_Typeclasses + imports ZFC_Cardinals + +begin + + + +subsection\The class of embeddable types\ + +class embeddable = + assumes ex_inj: "\V_of :: 'a \ V. inj V_of" + +context countable +begin + +subclass embeddable +proof - + have "inj (ord_of_nat \ to_nat)" if "inj to_nat" + for to_nat :: "'a \ nat" + using that by (simp add: inj_compose inj_ord_of_nat) + then show "class.embeddable TYPE('a)" + by intro_classes (meson local.ex_inj) +qed + +end + +instance unit :: embeddable .. +instance bool :: embeddable .. +instance nat :: embeddable .. +instance int :: embeddable .. +instance rat :: embeddable .. +instance char :: embeddable .. +instance String.literal :: embeddable .. +instance typerep :: embeddable .. + + +lemma embeddable_classI: + fixes f :: "'a \ V" + assumes "\x y. f x = f y \ x = y" + shows "OFCLASS('a, embeddable_class)" +proof (intro_classes, rule exI) + show "inj f" + by (rule injI [OF assms]) assumption +qed + +instance V :: embeddable + by (rule embeddable_classI [where f=id]) auto + +instance prod :: (embeddable,embeddable) embeddable +proof - + have "inj (\(x,y). \V_of1 x, V_of2 y\)" if "inj V_of1" "inj V_of2" + for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" + using that by (auto simp: inj_on_def) + then show "OFCLASS('a \ 'b, embeddable_class)" + by intro_classes (meson embeddable_class.ex_inj) +qed + +instance sum :: (embeddable,embeddable) embeddable +proof - + have "inj (case_sum (Inl \ V_of1) (Inr \ V_of2))" if "inj V_of1" "inj V_of2" + for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" + using that by (auto simp: inj_on_def split: sum.split_asm) + then show "OFCLASS('a + 'b, embeddable_class)" + by intro_classes (meson embeddable_class.ex_inj) +qed + +instance option :: (embeddable) embeddable +proof - + have "inj (case_option 0 (\x. set{V_of x}))" if "inj V_of" + for V_of :: "'a \ V" + using that by (auto simp: inj_on_def split: option.split_asm) + then show "OFCLASS('a option, embeddable_class)" + by intro_classes (meson embeddable_class.ex_inj) +qed + +primrec V_of_list where + "V_of_list V_of Nil = 0" +| "V_of_list V_of (x#xs) = \V_of x, V_of_list V_of xs\" + +lemma inj_V_of_list: + assumes "inj V_of" + shows "inj (V_of_list V_of)" +proof - + note inj_eq [OF assms, simp] + have "x = y" if "V_of_list V_of x = V_of_list V_of y" for x y + using that + proof (induction x arbitrary: y) + case Nil + then show ?case + by (cases y) auto + next + case (Cons a x) + then show ?case + by (cases y) auto + qed + then show ?thesis + by (auto simp: inj_on_def) +qed + +instance list :: (embeddable) embeddable +proof - + have "inj (rec_list 0 (\x xs r. \V_of x, r\))" (is "inj ?f") + if V_of: "inj V_of" for V_of :: "'a \ V" + proof - + note inj_eq [OF V_of, simp] + have "x = y" if "?f x = ?f y" for x y + using that + proof (induction x arbitrary: y) + case Nil + then show ?case + by (cases y) auto + next + case (Cons a x) + then show ?case + by (cases y) auto + qed + then show ?thesis + by (auto simp: inj_on_def) + qed + then show "OFCLASS('a list, embeddable_class)" + by intro_classes (meson embeddable_class.ex_inj) +qed + + +subsection\The class of small types\ + +class small = + assumes small: "\V_of :: 'a \ V. \A. inj V_of \ range V_of \ (elts A)" +begin + + subclass embeddable + by intro_classes (use small in metis) + +end + +context countable +begin + +subclass small +proof - + have *: "inj (ord_of_nat \ to_nat)" if "inj to_nat" + for to_nat :: "'a \ nat" + using that by (simp add: inj_compose inj_ord_of_nat) + then show "class.small TYPE('a)" + apply intro_classes + by (metis VPow_iff * fun.set_map image_subset_iff local.ex_inj ord_of_nat_le_omega) +qed + +end + + +lemma lepoll_UNIV_imp_small: "X \ (UNIV::'a::small set) \ small X" + by (metis down inj_on_image_eqpoll_self lepoll_def lepoll_trans order_refl small small_eqcong small_iff) + +lemma lepoll_imp_small: + fixes A :: "'a::small set" + assumes "X \ A" + shows "small X" + by (metis lepoll_UNIV_imp_small UNIV_I assms lepoll_def subsetI) + +instance unit :: small .. +instance bool :: small .. +instance nat :: small .. +instance int :: small .. +instance rat :: small .. +instance char :: small .. +instance String.literal :: small .. +instance typerep :: small .. + +instance prod :: (small,small) small +proof - + have "inj (\(x,y). \V_of1 x, V_of2 y\)" + "range (\(x,y). \V_of1 x, V_of2 y\) \ elts (VSigma A (\x. B))" + if "inj V_of1" "inj V_of2" "range V_of1 \ elts A" "range V_of2 \ elts B" + for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A B + using that by (auto simp: inj_on_def) + then show "OFCLASS('a \ 'b, small_class)" + by intro_classes (meson small) +qed + +instance sum :: (small,small) small +proof - + have "inj (case_sum (Inl \ V_of1) (Inr \ V_of2))" + "range (case_sum (Inl \ V_of1) (Inr \ V_of2)) \ elts (A \ B)" + if "inj V_of1" "inj V_of2" "range V_of1 \ elts A" "range V_of2 \ elts B" + for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A B + using that by (force simp: inj_on_def split: sum.split)+ + then show "OFCLASS('a + 'b, small_class)" + by intro_classes (meson small) +qed + +instance option :: (small) small +proof - + have "inj (\x. case x of None \ 0 | Some x \ set {V_of x})" + "range (\x. case x of None \ 0 | Some x \ set {V_of x}) \ insert 0 (elts (VPow A))" + if "inj V_of" "range V_of \ elts A" + for V_of :: "'a \ V" and A + using that by (auto simp: inj_on_def split: option.split_asm) + then show "OFCLASS('a option, small_class)" + by intro_classes (metis elts_vinsert small) +qed + +instance list :: (small) small +proof - + have "small (range (V_of_list V_of))" + if "inj V_of" "range V_of \ elts A" + for V_of :: "'a \ V" and A + proof - + have "range (V_of_list V_of) \ (UNIV :: 'a list set)" + using that by (simp add: inj_V_of_list) + also have "\ \ lists (UNIV :: 'a set)" + by simp + also have "\ \ (UNIV :: 'a set) \ (UNIV :: nat set)" + proof (cases "finite (range (V_of::'a \ V))") + case True + then have "lists (UNIV :: 'a set) \ (UNIV :: nat set)" + using countable_iff_lepoll countable_image_inj_on that(1) uncountable_infinite by blast + then show ?thesis + by (blast intro: lepoll_trans [OF _ lepoll_times2]) + next + case False + then have "lists (UNIV :: 'a set) \ (UNIV :: 'a set)" + using \infinite (range V_of)\ eqpoll_imp_lepoll infinite_eqpoll_lists by blast + then show ?thesis + using lepoll_times1 lepoll_trans by fastforce + qed + finally show ?thesis + by (simp add: lepoll_imp_small) + qed + then show "OFCLASS('a list, small_class)" + by intro_classes (metis inj_V_of_list order_refl small small_iff) +qed + +instance "fun" :: (small,embeddable) embeddable +proof - + have "inj (\f. VLambda A (\x. V_of2 (f (inv V_of1 x))))" + if *: "inj V_of1" "inj V_of2" "range V_of1 \ elts A" + for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A + proof - + have "f u = f' u" + if "VLambda A (\u. V_of2 (f (inv V_of1 u))) = VLambda A (\x. V_of2 (f' (inv V_of1 x)))" + for f f' :: "'a \ 'b" and u + by (metis inv_f_f rangeI subsetD VLambda_eq_D2 [OF that, of "V_of1 u"] *) + then show ?thesis + by (auto simp: inj_on_def) + qed + then show "OFCLASS('a \ 'b, embeddable_class)" + apply intro_classes + using embeddable_class.ex_inj small by auto +qed + +instance "fun" :: (small,small) small +proof - + have "inj (\f. VLambda A (\x. V_of2 (f (inv V_of1 x))))" (is "inj ?\") + "range (\f. VLambda A (\x. V_of2 (f (inv V_of1 x)))) \ elts (VPi A (\x. B))" + if *: "inj V_of1" "inj V_of2" "range V_of1 \ elts A" and "range V_of2 \ elts B" + for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A B + proof - + have "f u = f' u" + if "VLambda A (\u. V_of2 (f (inv V_of1 u))) = VLambda A (\x. V_of2 (f' (inv V_of1 x)))" + for f f' :: "'a \ 'b" and u + by (metis inv_f_f rangeI subsetD VLambda_eq_D2 [OF that, of "V_of1 u"] *) + then show "inj ?\" + by (auto simp: inj_on_def) + show "range ?\ \ elts (VPi A (\x. B))" + using that by (simp add: VPi_I subset_eq) + qed + then show "OFCLASS('a \ 'b, small_class)" + by intro_classes (meson small) +qed + +end diff --git a/thys/ZFC_in_HOL/ZFC_in_HOL.thy b/thys/ZFC_in_HOL/ZFC_in_HOL.thy new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/ZFC_in_HOL.thy @@ -0,0 +1,1021 @@ +section \The ZF Axioms, Ordinals and Transfinite Recursion\ + +theory ZFC_in_HOL + imports ZFC_Library + +begin + +subsection\Syntax and axioms\ + +hide_const (open) list.set Sum subset + +notation + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\") and + Sup ("\") + +typedecl V + +text\Presentation refined by Dmitriy Traytel\ +axiomatization elts :: "V \ V set" + where ext [intro?]: "elts x = elts y \ x=y" + and down_raw: "Y \ elts x \ Y \ range elts" + and Union_raw: "X \ range elts \ Union (elts ` X) \ range elts" + and Pow_raw: "X \ range elts \ inv elts ` Pow X \ range elts" + and replacement_raw: "X \ range elts \ f ` X \ range elts" + and inf_raw: "range (g :: nat \ V) \ range elts" + and foundation: "wf {(x,y). x \ elts y}" + +definition "small X \ (X \ range elts)" +text\Remark: the alternative is to make this an abbreviation. +However, then reasoning about @{term small} would invariably +reduce to reasoning about certain (unknown) sets containing +the elements in question. Instead we regard smallness as a primitive concept.\ + + +text\Small classes can be mapped to sets.\ +definition "set X \ (if small X then inv elts X else inv elts {})" + +lemma set_of_elts [simp]: "set (elts x) = x" + by (simp add: ext set_def f_inv_into_f small_def) + +lemma elts_of_set [simp]: "elts (set X) = (if small X then X else {})" + by (metis set_def bot.extremum down_raw f_inv_into_f small_def) + +lemma down: "Y \ elts x \ small Y" + by (simp add: down_raw small_def) + +lemma Union [intro]: "small X \ small (Union (elts ` X))" + by (simp add: Union_raw small_def) + +lemma Pow: "small X \ small (set ` Pow X)" + unfolding small_def using Pow_raw set_def down by force + +lemma replacement [intro,simp]: "small X \ small (f ` X)" + by (simp add: replacement_raw small_def) + +lemma inf: "small (range (g :: nat \ V))" + by (simp add: inf_raw small_def) + +lemma inf' [simp]: "small (g ` N)" for N :: "nat set" + by (metis (mono_tags, hide_lams) down elts_of_set image_iff inf rangeI subsetI) + +lemma UN [intro]: + assumes X: "small X" and B: "\x. x \ X \ small (B x)" + shows "small (\x\X. B x)" +proof - + have "(\ (elts ` (\x. set (B x)) ` X)) = (\ (B ` X))" + using B by force + then show ?thesis + using Union [OF replacement [OF X, of "\x. set (B x)"]] by simp +qed + +lemma countable: + assumes "countable X" shows "small X" + by (metis down elts_of_set subset_range_from_nat_into inf assms) + +lemma Finite: + assumes "finite X" shows "small X" +proof (cases "X = {}") + case True + then show ?thesis + by (simp add: down) +next + case False + then have "card X > 0" + using assms card_gt_0_iff by blast + moreover obtain h where "bij_betw h {0..k. if k < card X then h k else h 0) = X" + by (auto simp: image_def bij_betw_def set_eq_iff atLeast0LessThan) + then show ?thesis + using inf by metis +qed + +lemma small_empty [iff]: "small {}" + by (blast intro: Finite) + +lemma small_insert: + assumes "small X" + shows "small (insert a X)" +proof (cases "finite X") + case True + then show ?thesis + by (simp add: Finite) +next + case False + show ?thesis + using infinite_imp_bij_betw2 [OF False] + by (metis replacement Un_insert_right assms bij_betw_imp_surj_on sup_bot.right_neutral) +qed + +lemma small_insert_iff [iff]: "small (insert a X) \ small X" + by (metis down elts_of_set small_insert subset_insertI) + +lemma small_iff: "small X \ (\x. X = elts x)" + by (metis down elts_of_set subset_refl) + +lemma small_elts [iff]: "small (elts x)" + by (auto simp: small_iff) + +lemma small_diff [iff]: "small (elts a - X)" + by (meson Diff_subset down) + +lemma small_upair: "small {x,y}" + by simp + +lemma small_Un: "small (elts x \ elts y)" + using Union [OF small_upair] by auto + +lemma small_eqcong: "\small X; X \ Y\ \ small Y" + by (metis bij_betw_imp_surj_on eqpoll_def replacement) + +lemma big_UNIV [simp]: "\ small UNIV" + proof + assume "small UNIV" + then have "small A" for A + by (metis (full_types) UNIV_I down small_iff subsetI) + then have "range elts = UNIV" + by (meson small_iff surj_def) + then show False + by (metis Cantors_paradox Pow_UNIV) +qed + +lemma inj_on_set: "inj_on set (Collect small)" + by (metis elts_of_set inj_onI mem_Collect_eq) + +lemma set_injective [simp]: "\small X; small Y\ \ set X = set Y \ X=Y" + by (metis elts_of_set) + + +subsection\Type classes and other basic setup\ + +instantiation V :: zero +begin +definition zero_V where "0 \ set {}" +instance .. +end + +lemma elts_0 [simp]: "elts 0 = {}" + by (simp add: zero_V_def) + +lemma set_empty: "set {} = 0" + by (simp add: zero_V_def) + +instantiation V :: one +begin +definition one_V where "1 \ set {0}" +instance .. +end + +lemma elts_1 [simp]: "elts 1 = {0}" + by (simp add: one_V_def) + +lemma insert_neq_0 [simp]: "set (insert a X) = 0 \ \ small X" + unfolding zero_V_def + by (metis elts_of_set empty_not_insert set_of_elts small_insert_iff) + +instantiation V :: distrib_lattice +begin + +definition inf_V where "inf_V x y \ set (elts x \ elts y)" + +definition sup_V where "sup_V x y \ set (elts x \ elts y)" + +definition less_eq_V where "less_eq_V x y \ elts x \ elts y" + +definition less_V where "less_V x y \ less_eq x y \ x \ (y::V)" + +instance +proof + show "(x < y) = (x \ y \ \ y \ x)" for x :: V and y :: V + using ext less_V_def less_eq_V_def by auto + show "x \ x" for x :: V + by (simp add: less_eq_V_def) + show "x \ z" if "x \ y" "y \ z" for x y z :: V + using that by (auto simp: less_eq_V_def) + show "x = y" if "x \ y" "y \ x" for x y :: V + using that by (simp add: ext less_eq_V_def) + show "inf x y \ x" for x y :: V + by (metis down elts_of_set inf_V_def inf_sup_ord(1) less_eq_V_def) + show "inf x y \ y" for x y :: V + by (metis Int_lower2 down elts_of_set inf_V_def less_eq_V_def) + show "x \ inf y z" if "x \ y" "x \ z" for x y z :: V + proof - + have "small (elts y \ elts z)" + by (meson down inf.cobounded1) + then show ?thesis + using elts_of_set inf_V_def less_eq_V_def that by auto + qed + show "x \ x \ y" for x y :: V + by (simp add: less_eq_V_def small_Un sup_V_def) + show "y \ x \ y" for x y :: V + by (simp add: less_eq_V_def small_Un sup_V_def) + show "sup y z \ x" if "y \ x" "(z::V) \ x" for x y z :: V + using elts_of_set less_eq_V_def small_Un sup_V_def that by auto + show "sup x (inf y z) = inf (x \ y) (sup x z)" for x y z :: V + proof - + have "small (elts y \ elts z)" + by (meson down inf.cobounded2) + then show ?thesis + by (simp add: Un_Int_distrib inf_V_def small_Un sup_V_def) + qed +qed +end + +lemma V_equalityI [intro]: "(\x. x \ elts a \ x \ elts b) \ a = b" + by (meson dual_order.antisym less_eq_V_def subsetI) + +lemma vsubsetI [intro!]: "(\x. x \ elts a \ x \ elts b) \ a \ b" + by (simp add: less_eq_V_def subsetI) + +lemma vsubsetD [elim, intro?]: "a \ b \ c \ elts a \ c \ elts b" + using less_eq_V_def by auto + +lemma rev_vsubsetD: "c \ elts a \ a \ b \ c \ elts b" + \ \The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.\ + by (rule vsubsetD) + +lemma vsubsetCE [elim,no_atp]: "a \ b \ (c \ elts a \ P) \ (c \ elts b \ P) \ P" + \ \Classical elimination rule.\ + using vsubsetD by blast + +lemma subset_iff_less_eq_V: + assumes "small B" shows "A \ B \ set A \ set B \ small A" + using assms down small_iff by auto + +lemma smaller_than_small: + assumes "small B" "A \ B" shows "small A" + using assms subset_iff_less_eq_V by blast + +lemma small_Collect [simp]: "small A \ small {x \ A. P x}" + by (simp add: smaller_than_small) + +lemma small_Union_iff: "small (\(elts ` X)) \ small X" + proof + show "small X" + if "small (\ (elts ` X))" + proof - + have "X \ set ` Pow (\ (elts ` X))" + by fastforce + then show ?thesis + using Pow subset_iff_less_eq_V that by auto + qed +qed auto + +lemma not_less_0 [iff]: + fixes x::V shows "\ x < 0" + by (simp add: less_eq_V_def less_le_not_le) + +lemma le_0 [iff]: + fixes x::V shows "0 \ x" + by auto + + +definition VPow :: "V \ V" + where "VPow x \ set (set ` Pow (elts x))" + +lemma VPow_iff [iff]: "y \ elts (VPow x) \ y \ x" + using down Pow + apply (auto simp: VPow_def less_eq_V_def) + using less_eq_V_def apply fastforce + done + +lemma VPow_le_VPow_iff [simp]: "VPow a \ VPow b \ a \ b" + by auto + +lemma elts_VPow: "elts (VPow x) = set ` Pow (elts x)" + by (auto simp: VPow_def Pow) + +lemma small_sup_iff [simp]: "small (X \ Y) \ small X \ small Y" + by (metis down small_Un small_iff sup_ge1 sup_ge2) + +lemma elts_sup_iff [simp]: "elts (x \ y) = elts x \ elts y" + by (auto simp: sup_V_def small_Un) + +lemma trad_foundation: + assumes z: "z \ 0" shows "\w. w \ elts z \ w \ z = 0" + using foundation assms + by (simp add: wf_eq_minimal) (metis Int_emptyI equals0I inf_V_def set_of_elts zero_V_def) + + +instantiation "V" :: Sup +begin +definition Sup_V where "Sup_V X \ if small X then set (Union (elts ` X)) else 0" +instance .. +end + +instantiation "V" :: Inf +begin +definition Inf_V where "Inf_V X \ if X = {} then 0 else set (Inter (elts ` X))" +instance .. +end + +lemma V_disjoint_iff: "x \ y = 0 \ elts x \ elts y = {}" + by (metis down elts_of_set inf_V_def inf_le1 zero_V_def) + +text\I've no idea why @{term bdd_above} is treated differently from @{term bdd_below}, but anyway\ +lemma bdd_above_iff_small [simp]: "bdd_above X = small X" + proof + show "small X" if "bdd_above X" + proof - + obtain a where "\x\X. x \ a" + using that \bdd_above X\ bdd_above_def by blast + then show "small X" + by (meson VPow_iff \\x\X. x \ a\ down subsetI) + qed + show "bdd_above X" + if "small X" + proof - + have "\x\X. x \ \ X" + by (simp add: SUP_upper Sup_V_def Union less_eq_V_def that) + then show ?thesis + by (meson bdd_above_def) + qed +qed + + +instantiation "V" :: conditionally_complete_lattice +begin + +definition bdd_below_V where "bdd_below_V X \ X \ {}" + +instance + proof + show "\ X \ x" if "x \ X" "bdd_below X" + for x :: V and X :: "V set" + using that by (auto simp: bdd_below_V_def Inf_V_def split: if_split_asm) + show "z \ \ X" + if "X \ {}" "\x. x \ X \ z \ x" + for X :: "V set" and z :: V + using that + apply (simp add: bdd_below_V_def Inf_V_def split: if_split_asm) + by (metis INF_greatest INT_lower down elts_of_set equals0I less_eq_V_def that) + show "x \ \ X" if "x \ X" and "bdd_above X" for x :: V and X :: "V set" + using that Sup_V_def by auto + show "\ X \ (z::V)" if "X \ {}" "\x. x \ X \ x \ z" for X :: "V set" and z :: V + using that by (simp add: SUP_least Sup_V_def less_eq_V_def) +qed +end + +lemma Sup_upper: "\x \ A; small A\ \ x \ \A" + by (auto simp: Sup_V_def SUP_upper Union less_eq_V_def) + +lemma Sup_least: + fixes z::V shows "(\x. x \ A \ x \ z) \ \A \ z" + by (auto simp: Sup_V_def SUP_least less_eq_V_def) + +lemma Sup_empty [simp]: "\{} = (0::V)" + using Sup_V_def by auto + +lemma elts_Sup [simp]: "small X \ elts (\ X) = \(elts ` X)" + by (auto simp: Sup_V_def) + +lemma sup_V_0_left [simp]: "0 \ a = a" and sup_V_0_right [simp]: "a \ 0 = a" for a::V + by auto + +lemma Sup_V_insert: + fixes x::V assumes "small A" shows "\(insert x A) = x \ \A" + by (simp add: assms cSup_insert_If) + +lemma Sup_Un_distrib: "\small A; small B\ \ \(A \ B) = \A \ \B" + by auto + +lemma SUP_sup_distrib: + fixes f :: "V \ V" + shows "small A \ (SUP x\A. f x \ g x) = \ (f ` A) \ \ (g ` A)" + by (force simp:) + +lemma SUP_const [simp]: "(SUP y \ A. a) = (if A = {} then (0::V) else a)" + by simp + +lemma cSUP_subset_mono: + "\small (g ` B); A \ B; \x. x \ A \ f x \ g x\ \ \ (f ` A) \ \ (g ` B)" + by (rule Sup_least) fastforce + +lemma mem_Sup_iff [iff]: "x \ elts (\X) \ x \ \ (elts ` X) \ small X" + apply auto + apply (metis Sup_V_def UN_E elts_0 elts_Sup empty_iff) + by (metis Sup_V_def elts_0 empty_iff) + +lemma cSUP_UNION: + assumes ne: "small A" and bdd_UN: "small (\x\A. f ` B x)" + shows "\(f ` (\x\A. B x)) = \((\x. \(f ` B x)) ` A)" +proof - + have bdd: "\x. x \ A \ small (f ` B x)" + using bdd_UN subset_iff_less_eq_V by fastforce + then have bdd2: "small ((\x. \(f ` B x)) ` A)" + using ne(1) by blast + have "\(f ` (\x\A. B x)) \ \((\x. \(f ` B x)) ` A)" + using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd) + moreover have "\((\x. \(f ` B x)) ` A) \ \(f ` (\x\A. B x))" + using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN) + ultimately show ?thesis + by (rule order_antisym) +qed + +lemma Sup_subset_mono: "small B \ A \ B \ Sup A \ Sup B" + by auto + +lemma Sup_le_iff: "small S \ Sup S \ a \ (\x\S. x \ a)" + by auto + +lemma SUP_le_iff: "small (f ` A) \ \(f ` A) \ u \ (\x\A. f x \ u)" + by blast + +subsection\Successor function\ + +definition vinsert where "vinsert x y \ set (insert x (elts y))" + +lemma elts_vinsert [simp]: "elts (vinsert x y) = insert x (elts y)" + by (simp add: vinsert_def) + +definition succ where "succ x \ vinsert x x" + +lemma elts_succ [simp]: "elts (succ x) = insert x (elts x)" + by (simp add: succ_def) + +lemma succ_not_0 [simp]: "succ n \ 0" + by (metis elts_0 elts_succ empty_not_insert) + +instantiation V :: zero_neq_one +begin +instance by intro_classes (metis elts_0 elts_succ empty_iff insert_iff one_V_def set_of_elts) +end + +lemma mem_not_refl [simp]: "i \ elts i" + using wf_not_refl [OF foundation] by force + +lemma mem_not_sym: "\ (x \ elts y \ y \ elts x)" + using wf_not_sym [OF foundation] by force + +lemma succ_ne_self [simp]: "i \ succ i" + by (metis elts_succ insertI1 mem_not_refl) + +lemma succ_notin_self: "succ i \ elts i" + using elts_succ mem_not_refl by blast + +lemma le_succE: "succ i \ succ j \ i \ j" + using less_eq_V_def mem_not_sym by auto + +lemma succ_inject_iff [iff]: "succ i = succ j \ i = j" + by (simp add: dual_order.antisym le_succE) + +lemma inj_succ: "inj succ" + by (simp add: inj_def) + +lemma succ_neq_zero: "succ x \ 0" + by (metis elts_0 elts_succ insert_not_empty) + +definition pred where "pred i \ THE j. i = succ j" + +lemma pred_succ [simp]: "pred (succ i) = i" + by (simp add: pred_def) + + +subsection \Ordinals\ + +definition Transset where "Transset x \ \y \ elts x. y \ x" + +definition Ord where "Ord x \ Transset x \ (\y \ elts x. Transset y)" + +abbreviation ON where "ON \ Collect Ord" + +lemma Transset_0 [iff]: "Transset 0" + by (auto simp: Transset_def) + +lemma Transset_succ [intro]: + assumes "Transset x" shows "Transset (succ x)" + using assms + by (auto simp: Transset_def succ_def less_eq_V_def) + +lemma Transset_Sup: + assumes "\x. x \ X \ Transset x" shows "Transset (\X)" +proof (cases "small X") + case True + with assms show ?thesis + by (simp add: Transset_def) (meson Sup_upper assms dual_order.trans) +qed (simp add: Sup_V_def) + +lemma Transset_sup: + assumes "Transset x" "Transset y" shows "Transset (x \ y)" + using Transset_def assms by fastforce + +lemma Transset_inf: "\Transset i; Transset j\ \ Transset (i \ j)" + by (simp add: Transset_def rev_vsubsetD) + +lemma Transset_VPow: "Transset(i) \ Transset(VPow(i))" + by (auto simp: Transset_def) + +lemma Transset_Inf: "(\i. i \ A \ Transset i) \ Transset (\ A)" + by (force simp: Transset_def Inf_V_def) + +lemma Transset_SUP: "(\x. x \ A \ Transset (B x)) \ Transset (\ (B ` A))" + by (metis Transset_Sup imageE) + +lemma Transset_INT: "(\x. x \ A \ Transset (B x)) \ Transset (\ (B ` A))" + by (metis Transset_Inf imageE) + + +lemma Ord_0 [iff]: "Ord 0" + by (auto simp: Ord_def) + +lemma Ord_succ [intro]: + assumes "Ord x" shows "Ord (succ x)" + using assms by (auto simp: Ord_def) + +lemma Ord_Sup: + assumes "\x. x \ X \ Ord x" shows "Ord (\X)" +proof (cases "small X") + case True + with assms show ?thesis + by (auto simp: Ord_def Transset_Sup) +qed (simp add: Sup_V_def) + +lemma Ord_Union: + assumes "\x. x \ X \ Ord x" "small X" shows "Ord (set (\ (elts ` X)))" + by (metis Ord_Sup Sup_V_def assms) + +lemma Ord_sup: + assumes "Ord x" "Ord y" shows "Ord (x \ y)" + using assms + proof (clarsimp simp: Ord_def) + show "Transset (x \ y) \ (\y\elts x \ elts y. Transset y)" + if "Transset x" "Transset y" "\y\elts x. Transset y" "\y\elts y. Transset y" + using that small_Un sup_V_def Transset_sup by auto +qed + +lemma big_ON [simp]: "\ small ON" +proof + assume "small ON" + then have "set ON \ ON" + by (metis Ord_Union Ord_succ Sup_upper elts_Sup elts_succ insertI1 mem_Collect_eq mem_not_refl set_of_elts vsubsetD) + then show False + by (metis \small ON\ elts_of_set mem_not_refl) +qed + +lemma Ord_1 [iff]: "Ord 1" + using Ord_succ one_V_def succ_def vinsert_def by fastforce + +lemma OrdmemD: "Ord k \ j \ elts k \ j < k" + using Ord_def Transset_def less_V_def by auto + +lemma Ord_trans: "\ i \ elts j; j \ elts k; Ord k \ \ i \ elts k" + using Ord_def Transset_def by blast + +lemma mem_0_Ord: + assumes k: "Ord k" and knz: "k \ 0" shows "0 \ elts k" + by (metis Ord_def Transset_def inf.orderE k knz trad_foundation) + +lemma Ord_in_Ord: "\ Ord k; m \ elts k \ \ Ord m" + using Ord_def Ord_trans by blast + +lemma OrdI: "\Transset i; \x. x \ elts i \ Transset x\ \ Ord i" + by (simp add: Ord_def) + +lemma Ord_is_Transset: "Ord i \ Transset i" + by (simp add: Ord_def) + +lemma Ord_contains_Transset: "\Ord i; j \ elts i\ \ Transset j" + using Ord_def by blast + + +subsubsection \Induction, Linearity, etc.\ + +lemma Ord_induct [consumes 1, case_names step]: + assumes k: "Ord k" + and step: "\x.\ Ord x; \y. y \ elts x \ P y \ \ P x" + shows "P k" + using foundation k +proof (induction k rule: wf_induct_rule) + case (less x) + then show ?case + using Ord_in_Ord local.step by auto +qed + +text \Comparability of ordinals\ +lemma Ord_linear: "Ord k \ Ord l \ k \ elts l \ k=l \ l \ elts k" +proof (induct k arbitrary: l rule: Ord_induct) + case (step k) + note step_k = step + show ?case using \Ord l\ + proof (induct l rule: Ord_induct) + case (step l) + thus ?case using step_k + by (metis Ord_trans V_equalityI) + qed +qed + +text \The trichotomy law for ordinals\ +lemma Ord_linear_lt: + assumes "Ord k" "Ord l" + obtains (lt) "k < l" | (eq) "k=l" | (gt) "l < k" + using Ord_linear OrdmemD assms by blast + +lemma Ord_linear2: + assumes "Ord k" "Ord l" + obtains (lt) "k < l" | (ge) "l \ k" + by (metis Ord_linear_lt eq_refl assms order.strict_implies_order) + +lemma Ord_linear_le: + assumes "Ord k" "Ord l" + obtains (le) "k \ l" | (ge) "l \ k" + by (meson Ord_linear2 le_less assms) + +lemma union_less_iff [simp]: "\Ord i; Ord j\ \ i \ j < k \ i j Ord l \ k \ elts l \ k < l" + by (metis Ord_linear OrdmemD less_le_not_le) + +lemma le_succ_iff: "Ord i \ Ord j \ succ i \ succ j \ i \ j" + by (metis Ord_linear_le Ord_succ le_succE order_antisym) + +lemma zero_in_succ [simp,intro]: "Ord i \ 0 \ elts (succ i)" + using mem_0_Ord by auto + +primrec ord_of_nat :: "nat \ V" where + "ord_of_nat 0 = 0" +| "ord_of_nat (Suc n) = succ (ord_of_nat n)" + +lemma ord_of_nat_eq_initial: "ord_of_nat n = set (ord_of_nat ` {.. elts (ord_of_nat n) \ (\m i = \ (succ ` elts i)" + by (force intro: Ord_trans) + +lemma Ord_ord_of_nat [simp]: "Ord (ord_of_nat k)" + by (induct k, auto) + +lemma ord_of_nat_equality: "ord_of_nat n = \ ((succ \ ord_of_nat) ` {.. :: V where "\ \ set (range ord_of_nat)" + +lemma nat_into_Ord [simp]: "n \ elts \ \ Ord n" + by (metis Ord_ord_of_nat \_def elts_of_set image_iff inf) + +lemma Sup_\: "\(elts \) = \" + unfolding \_def by force + +lemma Ord_\ [iff]: "Ord \" + by (metis Ord_Sup Sup_\ nat_into_Ord) + +lemma zero_in_omega [iff]: "0 \ elts \" + by (metis (no_types) Ord_\ \_def elts_0 elts_of_set empty_iff inf' mem_0_Ord rangeI) + +lemma succ_in_omega [simp]: "n \ elts \ \ succ n \ elts \" + by (metis \_def elts_of_set image_iff inf' ord_of_nat.simps(2) rangeI) + +lemma ord_of_eq_0: "ord_of_nat j = 0 \ j = 0" + by (induct j) (auto simp: succ_neq_zero) + +lemma ord_of_nat_le_omega: "ord_of_nat n \ \" + by (metis Ord_\ Ord_def Transset_def \_def elts_of_set inf' rangeI) + +lemma ord_of_eq_0_iff [simp]: "ord_of_nat n = 0 \ n=0" + by (auto simp: ord_of_eq_0) + +lemma ord_of_nat_inject [iff]: "ord_of_nat i = ord_of_nat j \ i=j" +proof (induct i arbitrary: j) + case 0 show ?case + using ord_of_eq_0 by auto +next + case (Suc i) then show ?case + by auto (metis elts_0 elts_succ insert_not_empty not0_implies_Suc ord_of_nat.simps succ_inject_iff) +qed + +corollary inj_ord_of_nat: "inj ord_of_nat" + by (simp add: linorder_injI) + +lemma finite_Ord_omega: "\ \ elts \ \ finite (elts \)" + proof (clarsimp simp add: \_def) + show "finite (elts (ord_of_nat n))" if "\ = ord_of_nat n" for n + using that by (simp add: ord_of_nat_eq_initial [of n]) +qed + +lemma infinite_Ord_omega: "Ord \ \ infinite (elts \) \ \ \ \" + by (meson Ord_\ Ord_linear2 Ord_mem_iff_lt finite_Ord_omega) + +lemma ord_of_minus_1: "n > 0 \ ord_of_nat n = succ (ord_of_nat (n - 1))" + by (metis Suc_diff_1 ord_of_nat.simps(2)) + +subsubsection\Limit ordinals\ + +definition Limit :: "V\bool" + where "Limit i \ Ord i \ 0 \ elts i \ (\y. y \ elts i \ succ y \ elts i)" + +lemma zero_not_Limit [iff]: "\ Limit 0" + by (simp add: Limit_def) + +lemma not_succ_Limit [simp]: "\ Limit(succ i)" + by (metis Limit_def Ord_mem_iff_lt elts_succ insertI1 less_irrefl) + + +lemma Limit_eq_Sup_self: "Limit i \ i = Sup (elts i)" + apply (rule order_antisym) + apply (metis Limit_def Ord_equality Sup_V_def SUP_le_iff Sup_upper small_elts) + by (simp add: Limit_def Ord_def Transset_def Sup_least) + +lemma Ord_cases_lemma: + assumes "Ord k" shows "k = 0 \ (\j. k = succ j) \ Limit k" +proof (cases "Limit k") + case False + have "succ j \ elts k" if "\j. k \ succ j" "j \ elts k" for j + by (metis Ord_in_Ord Ord_linear Ord_succ assms elts_succ insertE mem_not_sym that) + with assms show ?thesis + by (auto simp: Limit_def mem_0_Ord) +qed auto + +lemma Ord_cases [cases type: V, case_names 0 succ limit]: + assumes "Ord k" + obtains "k = 0" | l where "Ord l" "succ l = k" | "Limit k" + by (metis assms Ord_cases_lemma Ord_in_Ord elts_succ insertI1) + +lemma non_succ_LimitI: + assumes "i\0" "Ord(i)" "\y. succ(y) \ i" + shows "Limit(i)" + using Ord_cases_lemma assms by blast + +lemma Ord_induct3 [consumes 1, case_names 0 succ Limit, induct type: V]: + assumes k: "Ord k" + and P: "P 0" "\k. \Ord k; P k\ \ P (succ k)" + "\k. \Limit k; \j. j \ elts k \ P j\ \ P k" + shows "P k" +using k +proof (induction k rule: Ord_induct) + case (step k) thus ?case + by (metis P Ord_cases Ord_linear succ_ne_self succ_notin_self) +qed + +lemma small_UN [simp,intro]: "\small A; \x. x \ A \ small (B x)\ \ small (\x\A. B x)" + by auto + + +subsubsection\Properties of LEAST for ordinals\ +lemma + assumes "Ord k" "P k" + shows Ord_LeastI: "P (LEAST i. Ord i \ P i)" and Ord_Least_le: "(LEAST i. Ord i \ P i) \ k" +proof - + have "P (LEAST i. Ord i \ P i) \ (LEAST i. Ord i \ P i) \ k" + using assms + proof (induct k rule: Ord_induct) + case (step x) then have "P x" by simp + show ?case proof (rule classical) + assume assm: "\ (P (LEAST a. Ord a \ P a) \ (LEAST a. Ord a \ P a) \ x)" + have "\y. Ord y \ P y \ x \ y" + proof (rule classical) + fix y + assume y: "Ord y \ P y" "\ x \ y" + with step obtain "P (LEAST a. Ord a \ P a)" and le: "(LEAST a. Ord a \ P a) \ y" + by (meson Ord_linear2 Ord_mem_iff_lt) + with assm have "x < (LEAST a. Ord a \ P a)" + by (meson Ord_linear_le y order.trans \Ord x\) + then show "x \ y" + using le by auto + qed + then have Least: "(LEAST a. Ord a \ P a) = x" + by (simp add: Least_equality \Ord x\ step.prems) + with \P x\ show ?thesis by simp + qed + qed + then show "P (LEAST i. Ord i \ P i)" and "(LEAST i. Ord i \ P i) \ k" by auto +qed + +lemma Ord_Least: + assumes "Ord k" "P k" + shows "Ord (LEAST i. Ord i \ P i)" +proof - + have "Ord (LEAST i. Ord i \ (Ord i \ P i))" + using Ord_LeastI [where P = "\i. Ord i \ P i"] assms by blast + then show ?thesis + by simp +qed + +\ \The following 3 lemmas are due to Brian Huffman\ +lemma Ord_LeastI_ex: "\i. Ord i \ P i \ P (LEAST i. Ord i \ P i)" + using Ord_LeastI by blast + +lemma Ord_LeastI2: + "\Ord a; P a; \x. \Ord x; P x\ \ Q x\ \ Q (LEAST i. Ord i \ P i)" + by (blast intro: Ord_LeastI Ord_Least) + +lemma Ord_LeastI2_ex: + "\a. Ord a \ P a \ (\x. \Ord x; P x\ \ Q x) \ Q (LEAST i. Ord i \ P i)" + by (blast intro: Ord_LeastI_ex Ord_Least) + +lemma Ord_LeastI2_wellorder: + assumes "Ord a" "P a" + and "\a. \ P a; \b. Ord b \ P b \ a \ b \ \ Q a" + shows "Q (LEAST i. Ord i \ P i)" +proof (rule LeastI2_order) + show "Ord (LEAST i. Ord i \ P i) \ P (LEAST i. Ord i \ P i)" + using Ord_Least Ord_LeastI assms by auto +next + fix y assume "Ord y \ P y" thus "(LEAST i. Ord i \ P i) \ y" + by (simp add: Ord_Least_le) +next + fix x assume "Ord x \ P x" "\y. Ord y \ P y \ x \ y" thus "Q x" + by (simp add: assms(3)) +qed + +lemma Ord_LeastI2_wellorder_ex: + assumes "\x. Ord x \ P x" + and "\a. \ P a; \b. Ord b \ P b \ a \ b \ \ Q a" + shows "Q (LEAST i. Ord i \ P i)" +using assms by clarify (blast intro!: Ord_LeastI2_wellorder) + +lemma not_less_Ord_Least: "\k < (LEAST x. Ord x \ P x); Ord k\ \ \ P k" + using Ord_Least_le less_le_not_le by auto + +lemma exists_Ord_Least_iff: "(\\. Ord \ \ P \) \ (\\. Ord \ \ P \ \ (\\ < \. Ord \ \ \ P \))" (is "?lhs \ ?rhs") +proof + assume ?rhs thus ?lhs by blast +next + assume H: ?lhs then obtain \ where \: "Ord \" "P \" by blast + let ?x = "LEAST \. Ord \ \ P \" + have "Ord ?x" + by (metis Ord_Least \) + moreover + { fix \ assume m: "\ < ?x" "Ord \" + from not_less_Ord_Least[OF m] have "\ P \" . } + ultimately show ?rhs + using Ord_LeastI_ex[OF H] by blast +qed + +lemma le_Sup_iff: + assumes "A \ ON" "Ord x" "small A" shows "x \ \A \ (\y \ ON. y (\a\A. y < a))" +proof (intro iffI ballI impI) + show "\a\A. y < a" + if "x \ \ A" "y \ ON" "y < x" + for y + proof - + have "\ \ A \ y" "Ord y" + using that by auto + then show ?thesis + by (metis Ord_linear2 Sup_least \A \ ON\ mem_Collect_eq subset_eq) + qed + show "x \ \ A" + if "\y\ON. y < x \ (\a\A. y < a)" + using that assms + by (metis Ord_Sup Ord_linear_le Sup_upper less_le_not_le mem_Collect_eq subsetD) +qed + +lemma le_SUP_iff: "\f ` A \ ON; Ord x; small A\ \ x \ \(f ` A) \ (\y \ ON. y (\i\A. y < f i))" + by (simp add: le_Sup_iff) + +subsection\Transfinite Recursion and the V-levels\ + +definition transrec :: "[[V\V,V]\V, V] \ V" + where "transrec H a \ wfrec {(x,y). x \ elts y} H a" + +lemma transrec: "transrec H a = H (\x \ elts a. transrec H x) a" +proof - + have "(cut (wfrec {(x, y). x \ elts y} H) {(x, y). x \ elts y} a) + = (\x\elts a. wfrec {(x, y). x \ elts y} H x)" + by (force simp: cut_def) + then show ?thesis + unfolding transrec_def + by (simp add: foundation wfrec) +qed + +text\Avoids explosions in proofs; resolve it with a meta-level definition\ +lemma def_transrec: + "\\x. f x \ transrec H x\ \ f a = H(\x \ elts a. f x) a" + by (metis restrict_ext transrec) + +lemma eps_induct [case_names step]: + assumes "\x. (\y. y \ elts x \ P y) \ P x" + shows "P a" + using wf_induct [OF foundation] assms by auto + + +definition Vfrom :: "[V,V] \ V" + where "Vfrom a \ transrec (\f x. a \ \((\y. VPow(f y)) ` elts x))" + +abbreviation Vset :: "V \ V" where "Vset \ Vfrom 0" + +lemma Vfrom: "Vfrom a i = a \ \((\j. VPow(Vfrom a j)) ` elts i)" + apply (subst Vfrom_def) + apply (subst transrec) + using Vfrom_def by auto + +lemma Vfrom_0 [simp]: "Vfrom a 0 = a" + by (subst Vfrom) auto + +lemma Vset: "Vset i = \((\j. VPow(Vset j)) ` elts i)" + by (subst Vfrom) auto + +lemma Vfrom_mono1: + assumes "a \ b" shows "Vfrom a i \ Vfrom b i" +proof (induction i rule: eps_induct) + case (step i) + then have "a \ (SUP j\elts i. VPow (Vfrom a j)) \ b \ (SUP j\elts i. VPow (Vfrom b j))" + by (intro sup_mono cSUP_subset_mono \a \ b\) auto + then show ?case + by (metis Vfrom) +qed + +lemma Vfrom_mono2: "Vfrom a i \ Vfrom a (i \ j)" +proof (induction arbitrary: j rule: eps_induct) + case (step i) + then have "a \ (SUP j\elts i. VPow (Vfrom a j)) + \ a \ (SUP j\elts (i \ j). VPow (Vfrom a j))" + by (intro sup_mono cSUP_subset_mono order_refl) auto + then show ?case + by (metis Vfrom) +qed + +lemma Vfrom_mono: "\Ord i; a\b; i\j\ \ Vfrom a i \ Vfrom b j" + by (metis (no_types) Vfrom_mono1 Vfrom_mono2 dual_order.trans sup.absorb_iff2) + +lemma Transset_Vfrom: "Transset(A) \ Transset(Vfrom A i)" +proof (induction i rule: eps_induct) + case (step i) + then show ?case + by (metis Transset_SUP Transset_VPow Transset_sup Vfrom) +qed + +lemma Transset_Vset [simp]: "Transset(Vset i)" + by (simp add: Transset_Vfrom) + +lemma Vfrom_sup: "Vfrom a (i \ j) = Vfrom a i \ Vfrom a j" +proof (rule order_antisym) + show "Vfrom a (i \ j) \ Vfrom a i \ Vfrom a j" + by (simp add: Vfrom [of a "i \ j"] Vfrom [of a i] Vfrom [of a j] Sup_Un_distrib image_Un sup.assoc sup.left_commute) + show "Vfrom a i \ Vfrom a j \ Vfrom a (i \ j)" + by (metis Vfrom_mono2 le_supI sup_commute) +qed + +lemma Vfrom_succ_Ord: + assumes "Ord i" shows "Vfrom a (succ i) = a \ VPow(Vfrom a i)" +proof (cases "i = 0") + case True + then show ?thesis + by (simp add: Vfrom [of _ "succ 0"]) +next + case False + have *: "(SUP x\elts i. VPow (Vfrom a x)) \ VPow (Vfrom a i)" + proof (rule cSup_least) + show "(\x. VPow (Vfrom a x)) ` elts i \ {}" + using False by auto + show "x \ VPow (Vfrom a i)" if "x \ (\x. VPow (Vfrom a x)) ` elts i" for x + using that + by clarsimp (meson Ord_in_Ord Ord_linear_le Vfrom_mono assms mem_not_refl order_refl vsubsetD) + qed + show ?thesis + proof (rule Vfrom [THEN trans]) + show "a \ (SUP j\elts (succ i). VPow (Vfrom a j)) = a \ VPow (Vfrom a i)" + using assms + by (intro sup_mono order_antisym) (auto simp: Sup_V_insert *) + qed +qed + +lemma Vset_succ: "Ord i \ Vset(succ(i)) = VPow(Vset(i))" + by (simp add: Vfrom_succ_Ord) + +lemma Vfrom_Sup: + assumes "X \ {}" "small X" + shows "Vfrom a (Sup X) = (SUP y\X. Vfrom a y)" +proof (rule order_antisym) + have "Vfrom a (\ X) = a \ (SUP j\elts (\ X). VPow (Vfrom a j))" + by (metis Vfrom) + also have "\ \ \ (Vfrom a ` X)" + proof - + have "a \ \ (Vfrom a ` X)" + by (metis Vfrom all_not_in_conv assms bdd_above_iff_small cSUP_upper2 replacement sup_ge1) + moreover have "(SUP j\elts (\ X). VPow (Vfrom a j)) \ \ (Vfrom a ` X)" + proof - + have "VPow (Vfrom a x) \ \ (Vfrom a ` X)" + if "y \ X" "x \ elts y" for x y + proof - + have "VPow (Vfrom a x) \ Vfrom a y" + by (metis Vfrom bdd_above_iff_small cSUP_upper2 le_supI2 order_refl replacement small_elts that(2)) + also have "\ \ \ (Vfrom a ` X)" + using assms that by (force intro: cSUP_upper) + finally show ?thesis . + qed + then show ?thesis + by (simp add: SUP_le_iff \small X\) + qed + ultimately show ?thesis + by auto + qed + finally show "Vfrom a (\ X) \ \ (Vfrom a ` X)" . + have "\x. x \ X \ + a \ (SUP j\elts x. VPow (Vfrom a j)) + \ a \ (SUP j\elts (\ X). VPow (Vfrom a j))" + using cSUP_subset_mono \small X\ by auto + then show "\ (Vfrom a ` X) \ Vfrom a (\ X)" + by (metis Vfrom assms(1) cSUP_least) +qed + +lemma Limit_Vfrom_eq: + "Limit(i) \ Vfrom a i = (SUP y \ elts i. Vfrom a y)" + by (metis Limit_def Limit_eq_Sup_self Vfrom_Sup ex_in_conv small_elts) + +end diff --git a/thys/ZFC_in_HOL/document/root.bib b/thys/ZFC_in_HOL/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/document/root.bib @@ -0,0 +1,37 @@ +%% This BibTeX bibliography file was created using BibDesk. +%% http://bibdesk.sourceforge.net/ + + +%% Created for Larry Paulson at 2019-10-24 12:42:51 +0100 + + +%% Saved with string encoding Unicode (UTF-8) + + + +@inproceedings{obua-partizan-games, + Author = {Obua, Steven}, + Booktitle = {Theoretical Aspects of Computing --- ICTAC 2006}, + Editor = {Barkaoui, Kamel and Cavalcanti, Ana and Cerone, Antonio}, + Isbn = {978-3-540-48816-3}, + Pages = {272-286}, + Publisher = {Springer}, + Title = {Partizan Games in {Isabelle/HOLZF}}, + Year = {2006}} + +@article{kirby-addition, + Author = {Kirby, Laurence}, + Date-Added = {2013-06-24 09:11:53 +0000}, + Date-Modified = {2013-06-24 09:11:53 +0000}, + Doi = {10.1002/malq.200610026}, + Issn = {1521-3870}, + Journal = {Mathematical Logic Quarterly}, + Keywords = {Ordinal arithmetic, adduction, finite set theory}, + Number = {1}, + Pages = {52-65}, + Publisher = {Wiley}, + Title = {Addition and multiplication of sets}, + Url = {https://doi.org/10.1002/malq.200610026}, + Volume = {53}, + Year = {2007}, + Bdsk-Url-1 = {https://doi.org/10.1002/malq.200610026}} diff --git a/thys/ZFC_in_HOL/document/root.tex b/thys/ZFC_in_HOL/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/ZFC_in_HOL/document/root.tex @@ -0,0 +1,61 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +\usepackage{amssymb} +\usepackage{stmaryrd} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Zermelo Frankel Set Theory in Higher-Order Logic} +\author{Lawrence C. Paulson\\ Computer Laboratory\\ University of Cambridge} + +\maketitle + +\begin{abstract} +This entry is a new formalisation of ZFC set theory in Isabelle/HOL\@. +It is logically equivalent to Obua's HOLZF~\cite{obua-partizan-games}; the point is to have the closest possible integration +with the rest of Isabelle/HOL, minimising the amount of new notations and exploiting type classes. + +There is a type \isa{V} of sets and a function +\isa{elts :: V\ {\isasymRightarrow}\ V\ set} mapping a set to its elements. +Classes simply have type \isa{V\ set}, and the predicate \isa{small} identifies those classes that correspond to actual sets. +Type classes connected with orders and lattices are used to minimise the amount of new notation +for concepts such as the subset relation, union and intersection. +Basic concepts --- Cartesian products, disjoint sums, natural numbers, functions, etc. --- are formalised. + +More advanced set-theoretic concepts, such as transfinite induction, ordinals, cardinals +and the transitive closure of a set, are also provided. +The definition of addition and multiplication for general sets (not just ordinals) follows Kirby \cite{kirby-addition}. +The development includes essential results about cardinal arithmetic. + +The theory provides two type classes with the aim of +facilitating developments that combine V with other Isabelle/HOL types: +\isa{embeddable}, the class of types that can be injected into~\isa{V} (including \isa{V} itself as well as \isa{V*V}, \isa{V\ list}, etc.), and +\isa{small}, the class of types that correspond to some ZF set. +\end{abstract} + +\newpage +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\newpage +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root.bib} + +\end{document}