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