Theory Sets

(*  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 "x X. y. 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: "(x2::'b set) x1::'b set. x1  x1  x2" by (metis Un_commute Un_upper2)
  have F2a: "(x2::'b set) x1::'b set. x1  x2  x2 = x2  x1" by (metis Un_commute subset_Un_eq)
  have F2: "(x2::'b set) x1::'b set. x1  x2  x2  x1  x1 = x2" 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 "x1::'a set. Y  x1  Z  Y  Z  X  ¬ X  x1  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 "x1::'a set. (Z  x1  Y  x1)  ¬ X  x1"
    { 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 "x1::'a set. Y  x1  Z  Y  Z  X  ¬ X  x1  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: "(x2::'b set) x1::'b set. x1  x2  x2  x1  x1 = x2" by (metis Un_commute subset_Un_eq)
  { assume AA1: "x1::'a set. (Z  x1  Y  x1)  ¬ X  x1"
    { 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 "x1::'a set. Y  x1  Z  Y  Z  X  ¬ X  x1  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 "x1::'a set. Y  x1  Z  Y  Z  X  ¬ X  x1  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: "(x2::'b set) x1::'b set. x1  x2  x2 = x2  x1" by (metis Un_commute subset_Un_eq)
  have F1: "(x2::'b set) x1::'b set. x1  x2  x2  x1  x1 = x2" 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: "x1::'a set. (Z  x1  Y  x1)  ¬ X  x1"
    { 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: "(x2::'b set) x1::'b set. x1  x2  x2  x1  x1 = x2" 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 "x1::'a set. Y  x1  Z  Y  Z  X  ¬ X  x1  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 "x1. x1  S  x1  S  x1 = S" by (metis set_eq_subset)
  hence "x1. x1  S  x1 = S" by (metis Union_upper)
  hence "x1::('a set) set. S  x1  S  x1" by (metis subsetI)
  hence "x1::('a set) set. S  insert (S) x1" 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