(* Title: HOL/Metis_Examples/Sets.thy Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Metis example featuring typed set theory. *) section ‹Metis Example Featuring Typed Set Theory› theory Sets imports Main begin declare [[metis_new_skolem]] lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & (S(x,y) | ~S(y,z) | Q(Z,Z)) & (Q(X,y) | ~Q(y,Z) | S(X,X))" by metis lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" by metis sledgehammer_params [isar_proofs, compress = 1] (*multiple versions of this example*) lemma (*equal_union: *) "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" proof - have F1: "∀(x⇩_{2}::'b set) x⇩_{1}::'b set. x⇩_{1}⊆ x⇩_{1}∪ x⇩_{2}" by (metis Un_commute Un_upper2) have F2a: "∀(x⇩_{2}::'b set) x⇩_{1}::'b set. x⇩_{1}⊆ x⇩_{2}⟶ x⇩_{2}= x⇩_{2}∪ x⇩_{1}" by (metis Un_commute subset_Un_eq) have F2: "∀(x⇩_{2}::'b set) x⇩_{1}::'b set. x⇩_{1}⊆ x⇩_{2}∧ x⇩_{2}⊆ x⇩_{1}⟶ x⇩_{1}= x⇩_{2}" by (metis F2a subset_Un_eq) { assume "¬ Z ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } moreover { assume AA1: "Y ∪ Z ≠ X" { assume "¬ Y ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis F1) } moreover { assume AAA1: "Y ⊆ X ∧ Y ∪ Z ≠ X" { assume "¬ Z ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } moreover { assume "(Z ⊆ X ∧ Y ⊆ X) ∧ Y ∪ Z ≠ X" hence "Y ∪ Z ⊆ X ∧ X ≠ Y ∪ Z" by (metis Un_subset_iff) hence "Y ∪ Z ≠ X ∧ ¬ X ⊆ Y ∪ Z" by (metis F2) hence "∃x⇩_{1}::'a set. Y ⊆ x⇩_{1}∪ Z ∧ Y ∪ Z ≠ X ∧ ¬ X ⊆ x⇩_{1}∪ Z" by (metis F1) hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } ultimately have "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AAA1) } ultimately have "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AA1) } moreover { assume "∃x⇩_{1}::'a set. (Z ⊆ x⇩_{1}∧ Y ⊆ x⇩_{1}) ∧ ¬ X ⊆ x⇩_{1}" { assume "¬ Y ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis F1) } moreover { assume AAA1: "Y ⊆ X ∧ Y ∪ Z ≠ X" { assume "¬ Z ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } moreover { assume "(Z ⊆ X ∧ Y ⊆ X) ∧ Y ∪ Z ≠ X" hence "Y ∪ Z ⊆ X ∧ X ≠ Y ∪ Z" by (metis Un_subset_iff) hence "Y ∪ Z ≠ X ∧ ¬ X ⊆ Y ∪ Z" by (metis F2) hence "∃x⇩_{1}::'a set. Y ⊆ x⇩_{1}∪ Z ∧ Y ∪ Z ≠ X ∧ ¬ X ⊆ x⇩_{1}∪ Z" by (metis F1) hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } ultimately have "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AAA1) } ultimately have "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by blast } moreover { assume "¬ Y ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis F1) } ultimately show "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by metis qed sledgehammer_params [isar_proofs, compress = 2] lemma (*equal_union: *) "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" proof - have F1: "∀(x⇩_{2}::'b set) x⇩_{1}::'b set. x⇩_{1}⊆ x⇩_{2}∧ x⇩_{2}⊆ x⇩_{1}⟶ x⇩_{1}= x⇩_{2}" by (metis Un_commute subset_Un_eq) { assume AA1: "∃x⇩_{1}::'a set. (Z ⊆ x⇩_{1}∧ Y ⊆ x⇩_{1}) ∧ ¬ X ⊆ x⇩_{1}" { assume AAA1: "Y ⊆ X ∧ Y ∪ Z ≠ X" { assume "¬ Z ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } moreover { assume "Y ∪ Z ⊆ X ∧ X ≠ Y ∪ Z" hence "∃x⇩_{1}::'a set. Y ⊆ x⇩_{1}∪ Z ∧ Y ∪ Z ≠ X ∧ ¬ X ⊆ x⇩_{1}∪ Z" by (metis F1 Un_commute Un_upper2) hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } ultimately have "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AAA1 Un_subset_iff) } moreover { assume "¬ Y ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_commute Un_upper2) } ultimately have "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AA1 Un_subset_iff) } moreover { assume "¬ Z ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } moreover { assume "¬ Y ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_commute Un_upper2) } moreover { assume AA1: "Y ⊆ X ∧ Y ∪ Z ≠ X" { assume "¬ Z ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } moreover { assume "Y ∪ Z ⊆ X ∧ X ≠ Y ∪ Z" hence "∃x⇩_{1}::'a set. Y ⊆ x⇩_{1}∪ Z ∧ Y ∪ Z ≠ X ∧ ¬ X ⊆ x⇩_{1}∪ Z" by (metis F1 Un_commute Un_upper2) hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } ultimately have "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AA1 Un_subset_iff) } ultimately show "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by metis qed sledgehammer_params [isar_proofs, compress = 3] lemma (*equal_union: *) "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" proof - have F1a: "∀(x⇩_{2}::'b set) x⇩_{1}::'b set. x⇩_{1}⊆ x⇩_{2}⟶ x⇩_{2}= x⇩_{2}∪ x⇩_{1}" by (metis Un_commute subset_Un_eq) have F1: "∀(x⇩_{2}::'b set) x⇩_{1}::'b set. x⇩_{1}⊆ x⇩_{2}∧ x⇩_{2}⊆ x⇩_{1}⟶ x⇩_{1}= x⇩_{2}" by (metis F1a subset_Un_eq) { assume "(Z ⊆ X ∧ Y ⊆ X) ∧ Y ∪ Z ≠ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } moreover { assume AA1: "∃x⇩_{1}::'a set. (Z ⊆ x⇩_{1}∧ Y ⊆ x⇩_{1}) ∧ ¬ X ⊆ x⇩_{1}" { assume "(Z ⊆ X ∧ Y ⊆ X) ∧ Y ∪ Z ≠ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) } ultimately show "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_commute Un_upper2) qed sledgehammer_params [isar_proofs, compress = 4] lemma (*equal_union: *) "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" proof - have F1: "∀(x⇩_{2}::'b set) x⇩_{1}::'b set. x⇩_{1}⊆ x⇩_{2}∧ x⇩_{2}⊆ x⇩_{1}⟶ x⇩_{1}= x⇩_{2}" by (metis Un_commute subset_Un_eq) { assume "¬ Y ⊆ X" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_commute Un_upper2) } moreover { assume AA1: "Y ⊆ X ∧ Y ∪ Z ≠ X" { assume "∃x⇩_{1}::'a set. Y ⊆ x⇩_{1}∪ Z ∧ Y ∪ Z ≠ X ∧ ¬ X ⊆ x⇩_{1}∪ Z" hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_upper2) } hence "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) } ultimately show "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V::'a set. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_subset_iff Un_upper2) qed sledgehammer_params [isar_proofs, compress = 1] lemma (*equal_union: *) "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) lemma "(X = Y ∩ Z) = (X ⊆ Y ∧ X ⊆ Z ∧ (∀V. V ⊆ Y ∧ V ⊆ Z ⟶ V ⊆ X))" by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym) lemma fixedpoint: "∃!x. f (g x) = x ⟹ ∃!y. g (f y) = y" by metis lemma (* fixedpoint: *) "∃!x. f (g x) = x ⟹ ∃!y. g (f y) = y" proof - assume "∃!x::'a. f (g x) = x" thus "∃!y::'b. g (f y) = y" by metis qed lemma (* singleton_example_2: *) "∀x ∈ S. ⋃S ⊆ x ⟹ ∃z. S ⊆ {z}" by (metis Set.subsetI Union_upper insertCI set_eq_subset) lemma (* singleton_example_2: *) "∀x ∈ S. ⋃S ⊆ x ⟹ ∃z. S ⊆ {z}" by (metis Set.subsetI Union_upper insert_iff set_eq_subset) lemma singleton_example_2: "∀x ∈ S. ⋃S ⊆ x ⟹ ∃z. S ⊆ {z}" proof - assume "∀x ∈ S. ⋃S ⊆ x" hence "∀x⇩_{1}. x⇩_{1}⊆ ⋃S ∧ x⇩_{1}∈ S ⟶ x⇩_{1}= ⋃S" by (metis set_eq_subset) hence "∀x⇩_{1}. x⇩_{1}∈ S ⟶ x⇩_{1}= ⋃S" by (metis Union_upper) hence "∀x⇩_{1}::('a set) set. ⋃S ∈ x⇩_{1}⟶ S ⊆ x⇩_{1}" by (metis subsetI) hence "∀x⇩_{1}::('a set) set. S ⊆ insert (⋃S) x⇩_{1}" by (metis insert_iff) thus "∃z. S ⊆ {z}" by metis qed text ‹ From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages 293-314. › (* Notes: (1) The numbering doesn't completely agree with the paper. (2) We must rename set variables to avoid type clashes. *) lemma "∃B. (∀x ∈ B. x ≤ (0::int))" "D ∈ F ⟹ ∃G. ∀A ∈ G. ∃B ∈ F. A ⊆ B" "P a ⟹ ∃A. (∀x ∈ A. P x) ∧ (∃y. y ∈ A)" "a < b ∧ b < (c::int) ⟹ ∃B. a ∉ B ∧ b ∈ B ∧ c ∉ B" "P (f b) ⟹ ∃s A. (∀x ∈ A. P x) ∧ f s ∈ A" "P (f b) ⟹ ∃s A. (∀x ∈ A. P x) ∧ f s ∈ A" "∃A. a ∉ A" "(∀C. (0, 0) ∈ C ∧ (∀x y. (x, y) ∈ C ⟶ (Suc x, Suc y) ∈ C) ⟶ (n, m) ∈ C) ∧ Q n ⟶ Q m" apply (metis all_not_in_conv) apply (metis all_not_in_conv) apply (metis mem_Collect_eq) apply (metis less_le singleton_iff) apply (metis mem_Collect_eq) apply (metis mem_Collect_eq) apply (metis all_not_in_conv) by (metis pair_in_Id_conv) end