(* 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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
