src/HOL/Metis_Examples/Sets.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61076 bdc1e2f0a86a
child 63167 0909deb8059b
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Metis_Examples/Sets.thy
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Metis example featuring typed set theory.
     6 *)
     7 
     8 section {* Metis Example Featuring Typed Set Theory *}
     9 
    10 theory Sets
    11 imports Main
    12 begin
    13 
    14 declare [[metis_new_skolem]]
    15 
    16 lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
    17                (S(x,y) | ~S(y,z) | Q(Z,Z))  &
    18                (Q(X,y) | ~Q(y,Z) | S(X,X))"
    19 by metis
    20 
    21 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
    22 by metis
    23 
    24 sledgehammer_params [isar_proofs, compress = 1]
    25 
    26 (*multiple versions of this example*)
    27 lemma (*equal_union: *)
    28    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    29 proof -
    30   have F1: "\<forall>(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \<subseteq> x\<^sub>1 \<union> x\<^sub>2" by (metis Un_commute Un_upper2)
    31   have F2a: "\<forall>(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \<subseteq> x\<^sub>2 \<longrightarrow> x\<^sub>2 = x\<^sub>2 \<union> x\<^sub>1" by (metis Un_commute subset_Un_eq)
    32   have F2: "\<forall>(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \<subseteq> x\<^sub>2 \<and> x\<^sub>2 \<subseteq> x\<^sub>1 \<longrightarrow> x\<^sub>1 = x\<^sub>2" by (metis F2a subset_Un_eq)
    33   { assume "\<not> Z \<subseteq> X"
    34     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    35   moreover
    36   { assume AA1: "Y \<union> Z \<noteq> X"
    37     { assume "\<not> Y \<subseteq> X"
    38       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
    39     moreover
    40     { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
    41       { assume "\<not> Z \<subseteq> X"
    42         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    43       moreover
    44       { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
    45         hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
    46         hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
    47         hence "\<exists>x\<^sub>1::'a set. Y \<subseteq> x\<^sub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^sub>1 \<union> Z" by (metis F1)
    48         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    49       ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
    50     ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1) }
    51   moreover
    52   { assume "\<exists>x\<^sub>1::'a set. (Z \<subseteq> x\<^sub>1 \<and> Y \<subseteq> x\<^sub>1) \<and> \<not> X \<subseteq> x\<^sub>1"
    53     { assume "\<not> Y \<subseteq> X"
    54       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
    55     moreover
    56     { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
    57       { assume "\<not> Z \<subseteq> X"
    58         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    59       moreover
    60       { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
    61         hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
    62         hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
    63         hence "\<exists>x\<^sub>1::'a set. Y \<subseteq> x\<^sub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^sub>1 \<union> Z" by (metis F1)
    64         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    65       ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
    66     ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by blast }
    67   moreover
    68   { assume "\<not> Y \<subseteq> X"
    69     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
    70   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
    71 qed
    72 
    73 sledgehammer_params [isar_proofs, compress = 2]
    74 
    75 lemma (*equal_union: *)
    76    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    77 proof -
    78   have F1: "\<forall>(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \<subseteq> x\<^sub>2 \<and> x\<^sub>2 \<subseteq> x\<^sub>1 \<longrightarrow> x\<^sub>1 = x\<^sub>2" by (metis Un_commute subset_Un_eq)
    79   { assume AA1: "\<exists>x\<^sub>1::'a set. (Z \<subseteq> x\<^sub>1 \<and> Y \<subseteq> x\<^sub>1) \<and> \<not> X \<subseteq> x\<^sub>1"
    80     { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
    81       { assume "\<not> Z \<subseteq> X"
    82         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    83       moreover
    84       { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
    85         hence "\<exists>x\<^sub>1::'a set. Y \<subseteq> x\<^sub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^sub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
    86         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    87       ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1 Un_subset_iff) }
    88     moreover
    89     { assume "\<not> Y \<subseteq> X"
    90       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
    91     ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
    92   moreover
    93   { assume "\<not> Z \<subseteq> X"
    94     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
    95   moreover
    96   { assume "\<not> Y \<subseteq> X"
    97     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
    98   moreover
    99   { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
   100     { assume "\<not> Z \<subseteq> X"
   101       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
   102     moreover
   103     { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
   104       hence "\<exists>x\<^sub>1::'a set. Y \<subseteq> x\<^sub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^sub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
   105       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
   106     ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
   107   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
   108 qed
   109 
   110 sledgehammer_params [isar_proofs, compress = 3]
   111 
   112 lemma (*equal_union: *)
   113    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
   114 proof -
   115   have F1a: "\<forall>(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \<subseteq> x\<^sub>2 \<longrightarrow> x\<^sub>2 = x\<^sub>2 \<union> x\<^sub>1" by (metis Un_commute subset_Un_eq)
   116   have F1: "\<forall>(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \<subseteq> x\<^sub>2 \<and> x\<^sub>2 \<subseteq> x\<^sub>1 \<longrightarrow> x\<^sub>1 = x\<^sub>2" by (metis F1a subset_Un_eq)
   117   { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
   118     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
   119   moreover
   120   { assume AA1: "\<exists>x\<^sub>1::'a set. (Z \<subseteq> x\<^sub>1 \<and> Y \<subseteq> x\<^sub>1) \<and> \<not> X \<subseteq> x\<^sub>1"
   121     { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
   122       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
   123     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) }
   124   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
   125 qed
   126 
   127 sledgehammer_params [isar_proofs, compress = 4]
   128 
   129 lemma (*equal_union: *)
   130    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
   131 proof -
   132   have F1: "\<forall>(x\<^sub>2::'b set) x\<^sub>1::'b set. x\<^sub>1 \<subseteq> x\<^sub>2 \<and> x\<^sub>2 \<subseteq> x\<^sub>1 \<longrightarrow> x\<^sub>1 = x\<^sub>2" by (metis Un_commute subset_Un_eq)
   133   { assume "\<not> Y \<subseteq> X"
   134     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
   135   moreover
   136   { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
   137     { assume "\<exists>x\<^sub>1::'a set. Y \<subseteq> x\<^sub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^sub>1 \<union> Z"
   138       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
   139     hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) }
   140   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V::'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
   141 qed
   142 
   143 sledgehammer_params [isar_proofs, compress = 1]
   144 
   145 lemma (*equal_union: *)
   146    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
   147 by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
   148 
   149 lemma "(X = Y \<inter> Z) = (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
   150 by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym)
   151 
   152 lemma fixedpoint: "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
   153 by metis
   154 
   155 lemma (* fixedpoint: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
   156 proof -
   157   assume "\<exists>!x::'a. f (g x) = x"
   158   thus "\<exists>!y::'b. g (f y) = y" by metis
   159 qed
   160 
   161 lemma (* singleton_example_2: *)
   162      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   163 by (metis Set.subsetI Union_upper insertCI set_eq_subset)
   164 
   165 lemma (* singleton_example_2: *)
   166      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   167 by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
   168 
   169 lemma singleton_example_2:
   170      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   171 proof -
   172   assume "\<forall>x \<in> S. \<Union>S \<subseteq> x"
   173   hence "\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> \<Union>S \<and> x\<^sub>1 \<in> S \<longrightarrow> x\<^sub>1 = \<Union>S" by (metis set_eq_subset)
   174   hence "\<forall>x\<^sub>1. x\<^sub>1 \<in> S \<longrightarrow> x\<^sub>1 = \<Union>S" by (metis Union_upper)
   175   hence "\<forall>x\<^sub>1::('a set) set. \<Union>S \<in> x\<^sub>1 \<longrightarrow> S \<subseteq> x\<^sub>1" by (metis subsetI)
   176   hence "\<forall>x\<^sub>1::('a set) set. S \<subseteq> insert (\<Union>S) x\<^sub>1" by (metis insert_iff)
   177   thus "\<exists>z. S \<subseteq> {z}" by metis
   178 qed
   179 
   180 text {*
   181   From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
   182   293-314.
   183 *}
   184 
   185 (* Notes: (1) The numbering doesn't completely agree with the paper.
   186    (2) We must rename set variables to avoid type clashes. *)
   187 lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
   188       "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
   189       "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
   190       "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B"
   191       "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
   192       "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
   193       "\<exists>A. a \<notin> A"
   194       "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
   195        apply (metis all_not_in_conv)
   196       apply (metis all_not_in_conv)
   197      apply (metis mem_Collect_eq)
   198     apply (metis less_le singleton_iff)
   199    apply (metis mem_Collect_eq)
   200   apply (metis mem_Collect_eq)
   201  apply (metis all_not_in_conv)
   202 by (metis pair_in_Id_conv)
   203 
   204 end