(* 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.

*)

header {* 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, isar_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, isar_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, isar_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, isar_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, isar_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. \<Union>S ⊆ x ==> ∃z. S ⊆ {z}"

by (metis Set.subsetI Union_upper insertCI set_eq_subset)

lemma (* singleton_example_2: *)

"∀x ∈ S. \<Union>S ⊆ x ==> ∃z. S ⊆ {z}"

by (metis Set.subsetI Union_upper insert_iff set_eq_subset)

lemma singleton_example_2:

"∀x ∈ S. \<Union>S ⊆ x ==> ∃z. S ⊆ {z}"

proof -

assume "∀x ∈ S. \<Union>S ⊆ x"

hence "∀x⇩_{1}. x⇩_{1}⊆ \<Union>S ∧ x⇩_{1}∈ S --> x⇩_{1}= \<Union>S" by (metis set_eq_subset)

hence "∀x⇩_{1}. x⇩_{1}∈ S --> x⇩_{1}= \<Union>S" by (metis Union_upper)

hence "∀x⇩_{1}::('a set) set. \<Union>S ∈ x⇩_{1}--> S ⊆ x⇩_{1}" by (metis subsetI)

hence "∀x⇩_{1}::('a set) set. S ⊆ insert (\<Union>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