src/HOL/Metis_Examples/Sets.thy
 author blanchet Tue Nov 06 15:15:33 2012 +0100 (2012-11-06) changeset 50020 6b9611abcd4c parent 49918 cf441f4a358b child 50705 0e943b33d907 permissions -rw-r--r--
renamed Sledgehammer option
```     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 header {* Metis Example Featuring Typed Set Theory *}
```
```     9
```
```    10 theory Sets
```
```    11 imports Main
```
```    12 begin
```
```    13
```
```    14 declare [[metis_new_skolemizer]]
```
```    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, isar_shrink = 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\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>1 \<union> x\<^isub>2" by (metis Un_commute Un_upper2)
```
```    31   have F2a: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
```
```    32   have F2: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>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\<Colon>'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\<Colon>'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\<Colon>'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\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
```
```    48         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'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\<Colon>'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\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1) }
```
```    51   moreover
```
```    52   { assume "\<exists>x\<^isub>1\<Colon>'a set. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
```
```    53     { assume "\<not> Y \<subseteq> X"
```
```    54       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'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\<Colon>'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\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
```
```    64         hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'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\<Colon>'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\<Colon>'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\<Colon>'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\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
```
```    71 qed
```
```    72
```
```    73 sledgehammer_params [isar_proofs, isar_shrink = 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\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
```
```    79   { assume AA1: "\<exists>x\<^isub>1\<Colon>'a set. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>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\<Colon>'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\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>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\<Colon>'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\<Colon>'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\<Colon>'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\<Colon>'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\<Colon>'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\<Colon>'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\<Colon>'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\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>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\<Colon>'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\<Colon>'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\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
```
```   108 qed
```
```   109
```
```   110 sledgehammer_params [isar_proofs, isar_shrink = 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\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
```
```   116   have F1: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>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\<Colon>'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\<^isub>1\<Colon>'a set. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>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\<Colon>'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\<Colon>'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\<Colon>'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, isar_shrink = 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\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>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\<Colon>'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\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z"
```
```   138       hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'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\<Colon>'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\<Colon>'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, isar_shrink = 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\<Colon>'a. f (g x) = x"
```
```   158   thus "\<exists>!y\<Colon>'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\<^isub>1. x\<^isub>1 \<subseteq> \<Union>S \<and> x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis set_eq_subset)
```
```   174   hence "\<forall>x\<^isub>1. x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis Union_upper)
```
```   175   hence "\<forall>x\<^isub>1\<Colon>('a set) set. \<Union>S \<in> x\<^isub>1 \<longrightarrow> S \<subseteq> x\<^isub>1" by (metis subsetI)
```
```   176   hence "\<forall>x\<^isub>1\<Colon>('a set) set. S \<subseteq> insert (\<Union>S) x\<^isub>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
```