Quelle Sets.thy Sprache: Isabelle

(*  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 \<open>Metis Example Featuring Typed Set Theory\<close>

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: "\(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \ x\<^sub>1 \ x\<^sub>2" by (metis Un_commute Un_upper2)
  have F2a: "\(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \ x\<^sub>2 \ x\<^sub>2 = x\<^sub>2 \ x\<^sub>1" by (metis Un_commute subset_Un_eq)
  have F2: "\(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \ x\<^sub>2 \ x\<^sub>2 \ x\<^sub>1 \ x\<^sub>1 = x\<^sub>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\<^sub>1::'a set. Y \ x\<^sub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^sub>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\<^sub>1::'a set. (Z \ x\<^sub>1 \ Y \ x\<^sub>1) \ \ X \ x\<^sub>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\<^sub>1::'a set. Y \ x\<^sub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^sub>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\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \ x\<^sub>2 \ x\<^sub>2 \ x\<^sub>1 \ x\<^sub>1 = x\<^sub>2" by (metis Un_commute subset_Un_eq)
  { assume AA1: "\x\<^sub>1::'a set. (Z \ x\<^sub>1 \ Y \ x\<^sub>1) \ \ X \ x\<^sub>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\<^sub>1::'a set. Y \ x\<^sub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^sub>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\<^sub>1::'a set. Y \ x\<^sub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^sub>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\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \ x\<^sub>2 \ x\<^sub>2 = x\<^sub>2 \ x\<^sub>1" by (metis Un_commute subset_Un_eq)
  have F1: "\(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \ x\<^sub>2 \ x\<^sub>2 \ x\<^sub>1 \ x\<^sub>1 = x\<^sub>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\<^sub>1::'a set. (Z \ x\<^sub>1 \ Y \ x\<^sub>1) \ \ X \ x\<^sub>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\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \ x\<^sub>2 \ x\<^sub>2 \ x\<^sub>1 \ x\<^sub>1 = x\<^sub>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\<^sub>1::'a set. Y \ x\<^sub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^sub>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: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!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\<^sub>1. x\<^sub>1 \ \S \ x\<^sub>1 \ S \ x\<^sub>1 = \S" by (metis set_eq_subset)
  hence "\x\<^sub>1. x\<^sub>1 \ S \ x\<^sub>1 = \S" by (metis Union_upper)
  hence "\x\<^sub>1::('a set) set. \S \ x\<^sub>1 \ S \ x\<^sub>1" by (metis subsetI)
  hence "\x\<^sub>1::('a set) set. S \ insert (\S) x\<^sub>1" by (metis insert_iff)
  thus "\z. S \ {z}" by metis
qed

text \<open>
  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
  293-314.
\<close>

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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.